@inproceedings{ba06456fe45c4aff88f8c3d060c447f5,
title = "Mechanisation of AKS algorithm: Part 1 – The main theorem",
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 mechanization of the AKS Main Theorem, which justifies the correctness (but not the complexity) of the AKS algorithm.",
author = "Chan, {Hing Lun} and Michael Norrish",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2015.; 6th International Conference on Interactive Theorem Proving, ITP 2015 ; Conference date: 24-08-2015 Through 27-08-2015",
year = "2015",
doi = "10.1007/978-3-319-22102-1_8",
language = "English",
isbn = "9783319221014",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "117--136",
editor = "Xingyuan Zhang and Christian Urban",
booktitle = "Interactive Theorem Proving - 6th International Conference, ITP 2015, Proceedings",
address = "Germany",
}