Primality Tests and Prime Certificate
Laurent Th\'ery (STAMP), Sophia Antipolis
TL;DR
This paper formalizes primality testing methods, specifically Lucas-Lehmer and Pocklington certificates, in Coq, based on Fermat's little theorem and elementary group theory, providing a rigorous proof framework.
Contribution
It introduces a formal Coq implementation of primality tests and certificates derived from Fermat's little theorem, enhancing proof reliability.
Findings
Formal Coq proofs of Lucas-Lehmer and Pocklington tests
Verification of primality certificates within a proof assistant
Foundation for automated primality proof certification
Abstract
This note presents a formalisation done in Coq of Lucas-Lehmer test and Pocklington certificate for prime numbers. They both are direct consequences of Fermat little theorem. Fermat little theorem is proved using elementary group theory and in particular Lagrange theorem.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsHistory and Theory of Mathematics