The veterans’ cabinet
The prerequisites are included before the words that depend on them. Skip what you already know.
Start with step one → Return to the storyReading a Lean statement
High school
Separate the objects, their conditions, and the conclusion.
Powers and positive integers
Middle school
A power repeats multiplication; positive integers start at one.
Prime numbers
Middle school
A prime is at least two and has no positive divisors except one and itself.
Even, odd, and case splits
High school
Splitting numbers into even and odd is the proof’s own first case distinction.
A hypothetical counterexample
High school
Assume a forbidden solution exists, then keep its evidence together.
Contradiction with the same object
High school
Evidence for f ≠ 0 and f = 0 cannot both hold for the same f.
The fourth power folds into a square
High school
A fourth power is a square of a square, so the case of four asks one equation lower down.
The dossier equation, packed once
University
Fermat42 names the suspect once: non-zero a, b and a⁴ + b⁴ = c².
Comparing remainders
Middle school
Two integers can differ while having the same remainder.
Clock arithmetic
Middle school
Computing inside a fixed finite set of residues is a number world of its own.
Cubes on the mod-nine clock
High school
Every cube lands on 0, 1 or 8 of the nine-residue clock: the first case of the case-of-three story.
Common factors and coprimality
Middle school
Coprime numbers share no positive divisor larger than one.
A wider net with a unit
University
To descend, first prove more: a³ + b³ = u·c³ with an arbitrary unit u.
Addition and multiplication together
Middle school
A shared set of rules for two operations describes many different number worlds.
How big is a signed number?
Middle school
The absolute value |c| keeps only the size: how far the number sits from zero.
Pick the smallest solution
University
Rank the hypothetical solutions by how often λ divides c: one must be smallest.
Choose the smallest suspect, again
University
Rank Fermat42 solutions by |c|: a smallest badge must exist.
Squares on the four-clock
Middle school
A whole-number square sits at 0 or 1 on the four-hour clock — never at 2.
Right triangles with whole-number sides
High school
A Pythagorean triple: three whole numbers where x² + y² = z² — the 3-4-5 family.
Tidy triangles share no factor
High school
Primitive triples have coprime legs — and a recipe: m² − n² and 2mn.
Two right triangles inside every suspect
University
The Pythagorean classification turns a⁴ + b⁴ = c² into chains of smaller squares.
The smaller suspect appears
University
m, r, s all become squares: i² = j⁴ + k⁴ with |i| < |c|. Contradiction.