Published March 8, 2022 | Version v1
Publication Metadata-only

Primality Tests and Prime Certificate

Théry, Laurent
Other:
Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)

Description

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.

Additional details

Identifiers Origin repository
Created:
December 3, 2022
Modified:
November 28, 2023