Mechanisation of the AKS Algorithm

Date

2020

Authors

Chan, Hing Lun
Norrish, Michael

Journal Title

Journal ISSN

Volume Title

Publisher

Kluwer Academic Publishers

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”.

Description

Keywords

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

Citation

Source

Journal of Automated Reasoning

Type

Journal article

Book Title

Entity type

Access Statement

License Rights

DOI

10.1007/s10817-020-09563-y

Restricted until

2099-12-31