@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",

}