# Theory Pratt_Certificate

section ‹Pratt's Primality Certificates›
text_raw ‹\label{sec:pratt}›
theory Pratt_Certificate
imports
Complex_Main
Lehmer.Lehmer
begin
text ‹
This work formalizes Pratt's proof system as described in his article
``Every Prime has a Succinct Certificate''\<^cite>‹"pratt1975certificate"›.
The proof system makes use of two types of predicates:
\begin{itemize}
\item $\text{Prime}(p)$: $p$ is a prime number
\item $(p, a, x)$: ‹∀q ∈ prime_factors(x). [a^((p - 1) div q) ≠ 1] (mod p)›
\end{itemize}
We represent these predicates with the following datatype:
›