Skip to main content

TS

Mechanisation of AKS algorithm: Part 1 – the main theorem

Authors

Joseph Chan and Michael Norrish

Australian National University

NICTA

Abstract

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.

BibTeX Entry

  @inproceedings{Chan_Norrish_15,
    author           = {Chan, Joseph and Norrish, Michael},
    month            = {aug},
    year             = {2015},
    keywords         = {interactive theorem proving, number theory, mechanised mathematics},
    title            = {Mechanisation of {AKS} Algorithm: Part 1 – the Main Theorem},
    booktitle        = {International Conference on Interactive Theorem Proving},
    pages            = {117-136},
    address          = {Nanjing, China}
  }

Download