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}
}
BibTeX