small-proof.md

We want to show that any divisor $d | M(n) = 2^n-1$ is a Fermat pseudo-prime for base $2^{n/2}$. That would mean that $\big( 2^{(n/2)} \big)^{d-1} \equiv 1 \pmod d$. Assume $n$ is even and $n>4$.

1. $M(n) \equiv 2^n - 1 \equiv 0 \pmod d$ (given)
2. $2^n \equiv 1 \pmod d$ (restatement of step (1))
3. $\left( 2^{(n/2)}\right)^{d-1} \equiv 2^{\left(\frac {n(d-1)} 2 \right)} \equiv \left(2^n\right)^{\left( \frac {d-1} 2 \right)} \equiv 1 \pmod d$ (step (2), $d-1$ is even)
4. $(2^{n/2})^{d-1} \equiv 1 \pmod d \rightarrow$ $d$ is pseudo-prime in base $2^{n/2}$ (definition)

Thus, $d$ is a Fermat pseudo-prime for base $2^{n/2}$

Lean4 formalization

I am working on a formalization of this argument at https://gist.github.com/tdunning/346e058011badd6b90f0b35e04aa91ef

Comments and suggestions welcome since I know soooo little about coding up proofs in Lean4.

Definition

A number $x$ is a Fermat pseudo-prime for the base $b$ iff

$b^{x-1} \equiv 1 \pmod x$

OK, I'll have a look. (actually I already tried, but... it says I should buy some book ... I found the old Lean3 documentation and "try it" available online, but that did not seem to work, so... Also somewhat busy right now... but I'm interested and will certainly manage to learn it sooner or later.)