Mechanisation of AKS Algorithm: Part 1 – The Main Theorem

DOI10.1007/978-3-319-22102-1_8zbMath1465.68302OpenAlexW2158957970MaRDI QIDQ2945627

Michael Norrish, Hing-Lun Chan

Publication date: 14 September 2015

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-22102-1_8

Mathematics Subject Classification ID

Number-theoretic algorithms; complexity (11Y16) Mechanization of proofs and logical operations (03B35) Factorization; primality (11A51) Primality (11Y11) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (8)

Exploring the structure of an algebra text with locales ⋮ Proof pearl: Bounding least common multiples with triangles ⋮ From types to sets by local type definition in higher-order logic ⋮ Unnamed Item ⋮ Mechanisation of the AKS algorithm ⋮ Proof Pearl: Bounding Least Common Multiples with Triangles ⋮ From Types to Sets by Local Type Definitions in Higher-Order Logic ⋮ Classification of finite fields with applications

Cites Work

• Unnamed Item
• Unnamed Item
• PRIMES is in P
• Primality testing in polynomial time. From randomized algorithms to ``PRIMES is in P.
• A String of Pearls: Proofs of Fermat's Little Theorem

This page was built for publication: Mechanisation of AKS Algorithm: Part 1 – The Main Theorem