Skip navigation
Skip navigation

Primality Testing is Polynomial-time: A Mechanised Verification of the AKS Algorithm

Chan, Hing Lun Joseph


We present a formalisation of the Agrawal-Kayal-Saxena (AKS) algorithm, a deterministic polynomial-time primality test. This algorithm was first announced by the AKS team in 2002, later improved in 2004. Our work is based on the improved version, with Parts 1 and 2 aim at a formal proof of the correctness of the algorithm, and Part 3 aims at a formal analysis of the complexity of the algorithm. The entire work is carried out in the HOL4 theorem prover. The correctness of the AKS algorithm...[Show more]

CollectionsOpen Access Theses
Date published: 2019
Type: Thesis (PhD)
DOI: 10.25911/5f58b06ca124e


File Description SizeFormat Image
thesis.pdfThesis Material943.06 kBAdobe PDFThumbnail

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator