Primality Tests and Prime Certificate

2022/03/09 by Laurent Théry, Théry, Laurent, Sophia Antipolis +1
Mathematics · #FOS: Computer and information sciences #History and Theory of Mathematics #Logic in Computer Science (cs.LO)

paper · pdf · doi:10.48550/arxiv.2203.16341

openalex publication_date 2022/03/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Related

• A LLT-like test for proving the primality of Fermat numbers
• Primality of numbers of the form ap^k+1
• Primality tests for Fermat numbers and 2^(2k+1)±2^(k+1)+1
• A new characterization of prime Fermat's numbers
• Four primality testing algorithms