Mechanisation of the AKS algorithm
Authors
DATA61
Australian National University
Abstract
The AKS algorithm (by Agrawal, Kayal and Saxena) is a significant theoretical result, establishing “PRIMES in P” by a brilliant application of ideas from finite fields. This paper describes an implementation of the AKS algorithm in our theorem prover HOL4, together with a proof of its correctness and its computational complexity. The complexity analysis is based on a conservative computation model using a writer monad. The method is elementary, but enough to show that our implementation of the AKS algorithm takes a number of execution steps bounded by a polynomial function of the input size. This establishes formally that the AKS algorithm indeed shows “PRIMES is in P”.
BibTeX Entry
@article{Norrish_Chan_21, author = {Norrish, Michael and Chan, Hing-Lun}, date = {2021-2-23}, doi = {https://doi.org/10.1007/s10817-020-09563-y}, issue = {2}, journal = {Journal of Automated Reasoning}, month = feb, pages = {205--256}, publisher = {Springer}, title = {Mechanisation of the {AKS} Algorithm}, volume = {65}, year = {2021} }