Primality Testing is Polynomial-time: A Mechanised Verification of the AKS Algorithm

Abstract

We present a formalisation of the Agrawal-Kayal-Saxena (AKS) algorithm, a deterministic polynomial-time primality test. This algorithm was first announced by the AKS team in 2002, later improved in 2004. Our work is based on the improved version, with Parts 1 and 2 aim at a formal proof of the correctness of the algorithm, and Part 3 aims at a formal analysis of the complexity of the algorithm. The entire work is carried out in the HOL4 theorem prover.

The correctness of the AKS algorithm relies on a main theorem developed by the AKS team, based on the theory of finite fields. To achieve the goal for Parts 1 and 2, we start by building up a hierarchy of HOL4 libraries for algebraic structures: from monoids, to groups, then rings and fields. Equipped with this foundation, we develop an abstract algebra library covering subgroups, quotient groups, ideals, and vector spaces. We extend the algebra library with polynomials, quotient rings, quotient fields, and finite fields. With all these we can formulate the AKS main theorem, which gives the correctness of the algorithm. For the formal proof, we need to dive into several advanced topics in finite field, in particular the existence and uniqueness of finite fields, and properties of cyclotomic polynomials.

Although algebraic structures, including finite fields, have been formalised in other theorem provers, our work is the first such comprehensive library in HOL4, covering also the uniqueness of finite fields up to isomorphism. Furthermore, by casting the AKS main theorem in the context of finite fields, we can see clearly the inter-relationship of various parts of the proof. As a result, we can make slight adjustments to the published version of the AKS algorithm. These slight adjustments are minor in terms of the significance of the AKS achievement, answering the challenge "Is Primes in P?" in the affirmative, but they simplify the implementation and analysis of the AKS algorithm.

The AKS algorithm consists of several loops: loops for checking if a condition still holds, and loops for searching if a condition will hold. Thus for the goal of Part 3, we embark on an analysis of such loops: formalising their behaviour, in particular the bound on the number of iterations. The AKS algorithm mostly involves modular computations, using numbers or manipulating polynomials. We develop tools and techniques to formally assert the recurrence properties of loop computations, with emphasis on the analysis of the time complexity behaviour. As far as we know, this approach to complexity analysis has not been done in other theorem provers.

Many offshoots from this work are interesting, even new to published proofs of the AKS algorithm. We have an elegant proof to a key result that enables us to slightly improve the bound on the AKS parameter. We present the relationship between the AKS algorithm and the AKS main theorem. We distill a picture to visualise the logic behind the proof of the AKS main theorem. We show in detail an implementation of the AKS algorithm that is suitable for loop analysis of complexity. We introduce an approach to study the time complexity of simple loops. Show more