Primality Tests and Prime Certificate
Logic in Computer Science
2022-03-31 v1
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.
Cite
@article{arxiv.2203.16341,
title = {Primality Tests and Prime Certificate},
author = {Laurent Théry and Sophia Antipolis},
journal= {arXiv preprint arXiv:2203.16341},
year = {2022}
}