Mechanisation of the AKS Algorithm

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”.