Reduction to \(n\geq5\) and prime

LemmaFermatLastTheorem.of_odd_primes #

If there is a counterexample to Fermat's Last Theorem, then there is a counterexample \(a^p+b^p=c^p\) with \(p\) an odd prime.

Proof

Note: this proof is in mathlib already; we run through it for completeness' sake.

Say \(a^n + b^n = c^n\) is a counterexample to Fermat's Last Theorem. Every positive integer is either a power of 2 or has an odd prime factor. If \(n=kp\) has an odd prime factor \(p\) then \((a^k)^p+(b^k)^p=(c^k)^p\) is the counterexample we seek. It remains to deal with the case where \(n\) is a power of 2, so let's assume this. We have \(3\leq n\) by assumption, so \(n=4k\) must be a multiple of 4, and thus \((a^k)^4=(b^k)^4=(c^k)^4\), giving us a counterexample to Fermat's Last Theorem for \(n=4\). However an old result of Fermat himself (proved as fermatLastTheoremFour in mathlib) says that \(x^4+y^4=z^4\) has no solutions in positive integers.

Lean

Formalized as FermatLastTheorem.of_odd_primes.

Sources

Fermat's Last Theorem (Imperial) blueprint: chapter/ch02reductions.tex, line 19

LeanFermatLastTheorem.of_odd_primes

Used by 1

Used byFermatLastTheorem.of_p_ge_5

Euler proved Fermat's Last Theorem for \(p=3\);

LemmafermatLastTheoremThree #

There are no solutions in positive integers to \(a^3+b^3=c^3\).

Proof

The proof in mathlib was formalized by a team from the “Lean For the Curious Mathematician” conference held in Luminy in March 2024 (its dependency graph can be visualised here).