Mechanisation of the AKS algorithm

DOI10.1007/s10817-020-09563-yzbMath1465.68301OpenAlexW3081717911MaRDI QIDQ2031415

Michael Norrish, Hing-Lun Chan

Publication date: 9 June 2021

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-020-09563-y

zbMATH Keywords

computational complexityfinite fieldsautomated reasoningnumber theorymachine modeltheorem-provingAKS algorithmwriter monad

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) 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)

Uses Software

• Isabelle
• Isabelle/HOL
• PURRS
• HOL
• ACE
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• FST TCS 2002: Foundations of software technology and theoretical computer science. 22nd conference, Kanpur, India, December 12--14, 2002. Proceedings
• Verification of the Miller-Rabin probabilistic primality test.
• Proof pearl: Bounding least common multiples with triangles
• PRIMES is in P
• Automated higher-order complexity analysis
• Primality testing in polynomial time. From randomized algorithms to ``PRIMES is in P.
• Classification of finite fields with applications
• Hoare logics for time bounds. A study in meta theory
• Proving divide and conquer complexities in Isabelle/HOL
• Modern Computer Algebra
• Mechanisation of AKS Algorithm: Part 1 – The Main Theorem
• Analysing the complexity of functional programs: higher-order meets first-order
• Proving Pearl: Knuth’s Algorithm for Prime Numbers
• Four primality testing algorithms
• On Chebyshev-Type Inequalities for Primes
• A String of Pearls: Proofs of Fermat's Little Theorem
• Automated Reasoning

This page was built for publication: Mechanisation of the AKS algorithm