Trustworthy Systems

Mechanisation of the AKS algorithm

Authors

Michael Norrish and Hing-Lun Chan

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

Download