Mechanisation of AKS Algorithm: Part 1 – the Main Theorem

Select |




Print


Chan, Joseph; Norrish, Michael

Chan, Joseph; Norrish, Michael


2015-08-24


Conference Material


Interactive Theorem Proving


Nanjing, China


117-136


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


http://www.inf.kcl.ac.uk/staff/urbanc/itp-2015/


nicta:8653


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)