Mechanisation of AKS algorithm. I. The main theorem

DOI10.1007/978-3-319-22102-1_8MaRDI QIDQ2945627zbMATH OpenOpenAlexFDO

Authors Hing-Lun Chan, Michael Norrish

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

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

Recommendations

• Mechanisation of the AKS algorithm
• PRIMES is in P
• scientific article; zbMATH DE number 2123628
• Primality testing in polynomial time. From randomized algorithms to ``PRIMES is in P.
• scientific article; zbMATH DE number 5902091

Cites work

• A String of Pearls: Proofs of Fermat's Little Theorem
• scientific article; zbMATH DE number 2206373 (Why is no real title available?)
• Primality testing in polynomial time. From randomized algorithms to ``PRIMES is in P.
• Primality testing: variations on a theme of Lucas
• PRIMES is in P

Cited in

(9)

• Proof pearl: Bounding least common multiples with triangles
• From types to sets by local type definition in higher-order logic
• Mechanisation of the AKS algorithm
• Exploring the structure of an algebra text with locales
• Classification of finite fields with applications
• Proof pearl: Bounding least common multiples with triangles
• From types to sets by local type definitions in higher-order logic
• Proving pearl: Knuth's algorithm for prime numbers
• scientific article; zbMATH DE number 7556735 (Why is no real title available?)

This page was built for publication: Mechanisation of AKS algorithm. I. The main theorem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945627)