Skip to main content
SpringerLink
Log in

Mechanisation of AKS Algorithm: Part 1 – The Main Theorem

  • Conference paper
  • First Online:
Interactive Theorem Proving (ITP 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9236))

Included in the following conference series:

Abstract

The AKS algorithm (by Agrawal, Kayal and Saxena) is a significant theoretical result proving “PRIMES in P”, as well as a brilliant application of ideas from finite fields. This paper describes the first step towards the goal of a full mechanisation of this result: a mechanisation of the AKS Main Theorem, which justifies the correctness (but not the complexity) of the AKS algorithm.

M. Norrish—NICTA is funded by the Australian Government through the Department of Communications and the Australian Research Council through the ICT Centre of Excellence Program.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    The constants involved in this algorithm are based on  [10, Algorithm 8.2.1]. They are slightly different from those in the AKS papers [2, 3], but such variations do not affect the conclusion of “PRIMES is in P”.

  2. 2.

    For example, in \({\mathbb {Z}_{6}}\), \(2\times {3} = 0\), hence \((X - 2)(X - 3) = X^2 - 5X = X(X - 5)\), which shows a polynomial of degree 2 can have more than 2 roots.

  3. 3.

    The characteristic \(\mathsf{{\chi } }\) of a ring \(\mathcal{R}\) is defined as the order of \({{\mathbf {\mathsf{{1}}}}}\) in the additive group of \(\mathcal{R}\), i.e., .

  4. 4.

    For example, [3] first stated the computational identity in \({\mathbb {Z}_{ {n} }}\), then “this implies” the corresponding identity in \({\mathbb {Z}_{ {p} }}\). Only [10] proved the shifting from \({\mathbb {Z}_{ {n} }}\) to \({\mathbb {Z}_{ {p} }}\) as a lemma.

  5. 5.

    John was kind enough to share his approach with us via private communication.

References

  1. Agrawal, M.: Primality tests based on Fermat’s Little Theorem, December 2006. http://www.cse.iitk.ac.in/users/manindra/presentations/FLTBasedTests.pdf

  2. Agrawal, M., Kayal, N., Saxena, N.: PRIMES is in P, August 2002. Original paper

    Google Scholar 

  3. Agrawal, M., Kayal, N., Saxena, N.: PRIMES is in P. Ann. Math. 160(2), 781–793 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  4. Bedodi, A.: Primality tests in polynomial time. Master’s thesis, Universitá Degli Studi Roma TRE, February 2010

    Google Scholar 

  5. Campos, C., Modave, F., Roach, S.: Towards the verification of the AKS primality test in ACL2. In: Fifth International Conference on Intelligent Technologies, November 2004

    Google Scholar 

  6. Chan, H.-L., Norrish, M.: A string of pearls: proofs of Fermat’s Little Theorem. J. Formalized Reason. 6(1), 63–87 (2013)

    MathSciNet  Google Scholar 

  7. Crandall, R., Pomerance, C.: Prime Numbers: A Computational Perspective. Springer, New York (2005)

    Google Scholar 

  8. Daleson, G.: Deterministic primality testing in polynomial time. Master’s thesis, Portland State University, December 2006

    Google Scholar 

  9. de Moura, F.L. C., Tadeu, R.: The correctness of the AKS primality test in Coq. July 2008. http://www.cic.unb.br/~flavio/AKS.pdf

  10. Dietzfelbinger, M.: Primality Testing in Polynomial Time: From Randomized Algorithms to ‘PRIMES is in P’. Lecture Notes in Computer Science. Springer, Heidelberg (2004)

    Book  Google Scholar 

  11. Domingues, R.: A polynomial time algorithm for prime recognition. Master’s thesis, University of Pretoria, January 2006

    Google Scholar 

  12. Linowitz, B.: An exposition of the AKS polynomial time primality testing. Master’s thesis, University of Pennsylvania, March 2006

    Google Scholar 

  13. Pomerance, C.: Primality testing, variations on a theme of Lucas (2008). http://cm.bell-labs.com/who/carlp/PS/primalitytalk5.ps

Download references

Author information

Authors and Affiliations

  1. Australian National University, Canberra, Australia

    Hing-Lun Chan

  2. Canberra Research Laboratory, NICTA, Australian National University, Canberra, Australia

    Michael Norrish

Authors
  1. Hing-Lun Chan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Norrish
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hing-Lun Chan .

Editor information

Editors and Affiliations

  1. Department of Informatics, King's College London, London, United Kingdom

    Christian Urban

  2. PLA University of Science and Technology, Nanjing, China

    Xingyuan Zhang

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Chan, HL., Norrish, M. (2015). Mechanisation of AKS Algorithm: Part 1 – The Main Theorem. In: Urban, C., Zhang, X. (eds) Interactive Theorem Proving. ITP 2015. Lecture Notes in Computer Science(), vol 9236. Springer, Cham. https://doi.org/10.1007/978-3-319-22102-1_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-22102-1_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-22101-4

  • Online ISBN: 978-3-319-22102-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation