Mechanisation of AKS Algorithm: Part 1 – the Main Theorem

Select |


Chan, Joseph; Norrish, Michael

Chan, Joseph; Norrish, Michael


Conference Material

Interactive Theorem Proving

Nanjing, China


The AKS algorithm (by Agrawal, Kayal and Saxena) is a significant theoretical result proving “PRIMES in P?, as well as a brilliant application of ideas from finite fields. This paper describes the first step towards the goal of a full mechanisation of this result: a mechanisation of the AKS Main Theorem, which justifies the correctness (but not the complexity) of the AKS algorithm.

interactive theorem proving, number theory, mechanised mathematics


Chan, Joseph; Norrish, Michael. Mechanisation of AKS Algorithm: Part 1 – the Main Theorem. In: Interactive Theorem Proving; Nanjing, China. 2015-08-24. 117-136.

Loading citation data...

Citation counts
(Requires subscription to view)