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$

You should use the latex command \pmod for the congruence relation (rather than mod operation).
Also, the "given" relation (step 1) could be seen as restatement of $d \mid M(n)$ which is what is really given in the first place. Writing this in front of $2^n-1 = 0\pmod d$ might help to understand when a reader comes here for the first time. (I speak for myself.)
Final remark: rigorously speaking, the Definition of a pseudo-prime includes the condition that the number is composite, since one does not want all primes in the list of pseudoprimes.

Thanks for the suggestions.

If you want to help even more, we could collaborate on a Lean4 proof. I can do most of that, but get stuck on trivialities due to lack of practical experience.

I can try to help but I also don't have experience with Lean4

I added a link to the beginnings of the proof. There are, no doubt, many improvements to be made and even random comments are welcome.

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.)