A “proof” of Fermat’s Last Theorem that fits the margin
Trail of Bits
—
09/09/2026
This is a lighthearted article about formal verification in software and mathematics. Formal verification takes a mathematical statement or a software program as input. In this article, that statement is Fermat's last theorem: a^n + b^n != c^n. You then add the constraints you want verified, in this case that all numbers must be natural numbers greater than 0, and that n must be greater than 2. Lean, the formal verification program, then tries to construct a proof of why this is true. For Fermat's last theorem, the proof is usually very long, but due to a bug in Lean, you can produce a surprisingly short one. This shows that trusting provers is not always straightforward, and that the provers themselves need to be verified!