Mechanisation of AKS algorithm: Part 1 - The main theorem

Loading...
Thumbnail Image

Date

Authors

Chan, Hing Lun (Joseph)
Norrish, Michael

Journal Title

Journal ISSN

Volume Title

Publisher

Springer International Publishing Switzerland

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.

Description

Keywords

Citation

Source

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Book Title

Entity type

Access Statement

License Rights

Restricted until

2037-12-31