Mechanisation of the AKS Algorithm

Hing Lun Chan; Michael Norrish

doi:10.1007/s10817-020-09563-y

Mechanisation of the AKS Algorithm

Hing Lun Chan^*, Michael Norrish

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

2 Citations (Scopus)

Abstract

The AKS algorithm (by Agrawal, Kayal and Saxena) is a significant theoretical result, establishing “PRIMES in P” by a brilliant application of ideas from finite fields. This paper describes an implementation of the AKS algorithm in our theorem prover HOL4, together with a proof of its correctness and its computational complexity. The complexity analysis is based on a conservative computation model using a writer monad. The method is elementary, but enough to show that our implementation of the AKS algorithm takes a number of execution steps bounded by a polynomial function of the input size. This establishes formally that the AKS algorithm indeed shows “PRIMES is in P”.

Original language	English
Pages (from-to)	205-256
Number of pages	52
Journal	Journal of Automated Reasoning
Volume	65
Issue number	2
DOIs	https://doi.org/10.1007/s10817-020-09563-y
Publication status	Published - Feb 2021

Access to Document

10.1007/s10817-020-09563-y

Cite this

@article{fac542456618430a95c530c8bc679e67,

title = "Mechanisation of the AKS Algorithm",

abstract = "The AKS algorithm (by Agrawal, Kayal and Saxena) is a significant theoretical result, establishing “PRIMES in P” by a brilliant application of ideas from finite fields. This paper describes an implementation of the AKS algorithm in our theorem prover HOL4, together with a proof of its correctness and its computational complexity. The complexity analysis is based on a conservative computation model using a writer monad. The method is elementary, but enough to show that our implementation of the AKS algorithm takes a number of execution steps bounded by a polynomial function of the input size. This establishes formally that the AKS algorithm indeed shows “PRIMES is in P”.",

keywords = "AKS algorithm, Automated reasoning, Finite fields computational complexity, Machine model, Number theory, Theorem-proving, Writer monad",

author = "Chan, \{Hing Lun\} and Michael Norrish",

note = "Publisher Copyright: {\textcopyright} 2020, Springer Nature B.V.",

year = "2021",

month = feb,

doi = "10.1007/s10817-020-09563-y",

language = "English",

volume = "65",

pages = "205--256",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "2",

}

TY - JOUR

T1 - Mechanisation of the AKS Algorithm

AU - Chan, Hing Lun

AU - Norrish, Michael

PY - 2021/2

Y1 - 2021/2

N2 - The AKS algorithm (by Agrawal, Kayal and Saxena) is a significant theoretical result, establishing “PRIMES in P” by a brilliant application of ideas from finite fields. This paper describes an implementation of the AKS algorithm in our theorem prover HOL4, together with a proof of its correctness and its computational complexity. The complexity analysis is based on a conservative computation model using a writer monad. The method is elementary, but enough to show that our implementation of the AKS algorithm takes a number of execution steps bounded by a polynomial function of the input size. This establishes formally that the AKS algorithm indeed shows “PRIMES is in P”.

AB - The AKS algorithm (by Agrawal, Kayal and Saxena) is a significant theoretical result, establishing “PRIMES in P” by a brilliant application of ideas from finite fields. This paper describes an implementation of the AKS algorithm in our theorem prover HOL4, together with a proof of its correctness and its computational complexity. The complexity analysis is based on a conservative computation model using a writer monad. The method is elementary, but enough to show that our implementation of the AKS algorithm takes a number of execution steps bounded by a polynomial function of the input size. This establishes formally that the AKS algorithm indeed shows “PRIMES is in P”.

KW - AKS algorithm

KW - Automated reasoning

KW - Finite fields computational complexity

KW - Machine model

KW - Number theory

KW - Theorem-proving

KW - Writer monad

UR - https://www.scopus.com/pages/publications/85090236039

U2 - 10.1007/s10817-020-09563-y

DO - 10.1007/s10817-020-09563-y

M3 - Article

SN - 0168-7433

VL - 65

SP - 205

EP - 256

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 2

ER -

Mechanisation of the AKS Algorithm

Abstract

Access to Document

Other files and links

Fingerprint

Cite this