The claim🔗

Fermat’s Last Theorem: for any whole number n ≥ 3, there are no positive whole numbers a, b, c with aⁿ + bⁿ = cⁿ.

Fermat wrote it in a margin around 1637. Andrew Wiles proved it in 1994, with Richard Taylor, using hundreds of pages of advanced mathematics. A full Lean proof is a large ongoing project.

So if an AI tells you “I proved Fermat’s Last Theorem in Lean, here is the file”, something is almost certainly off. Today you find out exactly what. First, the honest statement.

Step 1: Mathlib’s statement🔗

Mathlib defines the statement in three layers:

def FermatLastTheorem : Prop :=
∀ n ≥ 3, FermatLastTheoremFor n

def FermatLastTheoremFor : ℕ → Prop :=
fun n => FermatLastTheoremWith ℕ n

def FermatLastTheoremWith.{u_1} : (R : Type u_1) → [Semiring R] → ℕ → Prop :=
fun R [Semiring R] n => ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → a ^ n + b ^ n ≠ c ^ n

In short, leaving out the technical parts:

FermatLastTheorem := ∀ n ≥ 3, FermatLastTheoremFor n

FermatLastTheoremFor n := FermatLastTheoremWith ℕ n

FermatLastTheoremWith R n := ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → a ^ n + b ^ n ≠ c ^ n

Read from the bottom up: in the numbers R, nonzero a, b, c never satisfy aⁿ + bⁿ = cⁿ. Over ℕ that is the theorem for one n, and FermatLastTheorem says it for every n ≥ 3.

A definition is not a proof🔗

Lean accepted def FermatLastTheorem : Prop := …. That only means the statement is well-formed. A def of a Prop writes the claim down; it proves nothing.

What Mathlib does prove are special cases, each a real theorem:

fermatLastTheoremFour : FermatLastTheoremFor 4

'fermatLastTheoremFour' depends on axioms: [propext, Classical.choice, Quot.sound]

FermatLastTheorem.of_odd_primes : (∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p) → FermatLastTheorem

The proof for n = 4 is a few hundred lines (and there is one for n = 3). You did not read it, and you do not need to: you read its statement, its definitions, and its axioms.

The last one is honest and useful: if Fermat holds for every odd prime exponent, then it holds for all n ≥ 3. Remember it.

Fake proof 1🔗

Now the AI’s files. Each one is accepted by Lean, and each is called fermat_last_theorem. Here is the first. Here it is. The Lab’s automatic Audit has this to say about it:

The audit reports no red flags. The proof is a real Mathlib theorem. And yet…

Fake proof 2🔗

declaration uses `sorry`

'fermat_last_theorem' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]

Lean shows one yellow warning, on the helper lemma, not on fermat_last_theorem itself.

Fake proof 3🔗

No sorry, standard axioms, and the audit finds no red flags (it only notes that hn is never used). Read the statement out loud.

Fake proof 4🔗

This one uses Mathlib’s own statement, FermatLastTheoremFor n, and a one-word proof.

The verdict, and what you just did🔗

Four fakes, four different tricks, mapped to the checklist:

1. A hypothesis that carries the claim: step 4. The automatic checks saw nothing; only reading caught it.

2. A hidden `sorry`: step 1, caught by #print axioms and the audit.

3. A weaker statement (∃ instead of ∀): step 2. Only reading the statement out loud caught it.

4. Impossible hypotheses: step 3, caught by the audit.

Two of the four passed every automatic check. That is why the audit tool lists what it checked and what is your turn, and why this course taught you to read.

And the honest status, in this version of Mathlib: Fermat’s Last Theorem is stated (FermatLastTheorem), the cases n = 3 and n = 4 are proved, and it is reduced to odd prime exponents. The full proof is being formalized in a separate project.