The human dramas behind the mathematics: the margin, the staircase, the suspicious parcel, one biscuit of rehearsal, the empty room, and the owl that does not applaud. No equations required; some are hidden underneath, and every story links to the pages that check it.
Proof stories · 1 / 6
The margin
1637: one sentence in a book margin starts the longest waiting room in mathematics.
Fermat is reading Diophantus and writes, beside a problem, that no cube can be split into two cubes, no fourth power into two fourth powers, and in general no power beyond the second into two of the same power — adding that he has a truly marvellous proof which this margin is too narrow to contain.
He never publishes it. For three and a half centuries the note is either the most famous promise in mathematics or its most famous joke, and nobody can tell which.
What survives is a method, not the sentence: to rule out a whole infinite family, assume one member exists, choose the smallest, and derive a smaller one. Fermat used it for the fourth power. Euler found the crack that made it work for cubes, at the price of one new number — the cube root of unity.
The modern ending is a bridge: the semistable modularity theorem proved in the work of Wiles and Taylor–Wiles, published in 1995, meets Ribet’s theorem that an FLT counterexample would give a nonmodular curve. The later 2001 theorem covers all elliptic curves over the rationals; it is not the date of the semistable result.
To prove a thing cannot exist, build a staircase that must go down forever — then notice it cannot start.
Infinite descent is the most polite contradiction on the shelf. Assume a counterexample exists. Among all of them, choose the smallest — well-ordering permits it. From that one, construct another that is strictly smaller. Repeat forever. A staircase of natural numbers has a bottom, so the descent was impossible from the start.
The craft is in the construction, not the contradiction. Fermat’s fourth-power step finds two new right triangles inside one; Euler’s cube step needs a new ring where the sum of cubes factorises; both must show the new witness is nonzero, or the staircase politely stops one step too late.
In a proof assistant the smallest witness is a real object with a real rank, and “strictly smaller” is checked, not gestured at. The staircase becomes a machine you can inspect: every step, every inequality, every nonzero witness.
1985: a failed equation is repackaged as a geometric object — and that object looks guilty.
Gerhard Frey’s idea was almost rude in its simplicity: take a hypothetical FLT counterexample aᵖ + bᵖ = cᵖ, and use it to build an elliptic curve whose arithmetic is too strange to be true. The curve inherits the counterexample’s fingerprints — its conductor, its discriminant, its semistability story.
Jean-Pierre Serre supplied the precise recipe in a letter; Ken Ribet turned it into a theorem. The parcel was guilty: any curve built from such a counterexample would be non-modular. Frey’s observation was not yet a proof, but it was a dossier with every field filled in — which is exactly what this site’s frey-package page pins down.
The direction of the argument is what makes it strange and beautiful: nobody proves the equation has no solutions directly. Instead, a solution would be evidence that one specific curve exists; geometry then refuses to host that curve. The counterexample is dissolved by its own paperwork.
A conjecture about two kinds of mathematics becomes a plan with a deadline — and the deadline nearly wins.
The modularity theorem gives an elliptic curve over the rationals a modular partner. At every prime p of good reduction, the matching coefficient is aₚ = p + 1 − #E(𝔽ₚ), with the point at infinity included. The form has the appropriate weight and level, and the match is exact.
Wiles’s strategy compares a deformation ring R with a Hecke algebra T. The notation R = T expresses an isomorphism through the comparison map, not literal equality of their Lean types. Establishing this comparison was central to the argument, including the repair with Richard Taylor after the 1993 gap.
The rest is drama with dates: seven years of secret work, three lectures in Cambridge in June 1993 ending with “I think I’ll stop here,” a fatal gap found that autumn, a year of repair with Taylor, and two papers in Annals in 1995. The duet was real. The biscuit budget was never enough.
The finale is deliberately anticlimactic: a witness walks into a room the theorem has already certified empty.
Level lowering is the quiet miracle. From the suspicious curve one obtains a modular form of weight 2 and level 2 — an extremely small space. The same procedure certifies that the form is nonzero: the guest arrives alive. That nonzero witness is the whole point; without it there is nothing to contradict.
And the room is already known to be empty: the space of weight-2, level-2 cusp forms has dimension zero. Every form in it equals zero — a theorem about a vanishing space, proved by counting a subgroup index and comparing with a weight-6 level-1 space where the silence is on record.
Put the two certificates side by side and the case collapses: f ≠ 0 and f = 0, same f, same space. No infinities, no limits, no drama — just a nonzero stone beside a certified empty box. It is the shortest contradiction on record, and it took the longest road to reach.
A machine does not applaud. It lists assumptions — and that list is the humblest sentence in the story.
The final scene is not in the margin, the lecture hall, or the courtroom of history. It is a terminal: a proof assistant reads every line, checks every inference, and refuses to take anything on reputation — including Wiles’s.
When the formalization finally imports the theorem, the honest question is not “is it true?” but “what did we assume?” The answer is short: propext, Classical.choice, Quot.sound. Three foundations of the checking system, not extra beliefs about Fermat. That distinction is the entire ethics of the enterprise.
The owl does not applaud. Lean checks a proof term against its statement and assumptions. Here we read a pinned source checkpoint; this website does not recompile the complete FLT development, and we have not measured its checking time. The readers still sit at one table, arguing about the margin.
Start with the cake-scale story. You only need to read one small piece at a time. If you are in the Fermat story, start with Story depth, then the words listed before the chapter.
In simpler words
You do not need to know Lean, symbols or university mathematics to begin. Definitions come first in the small stories.
A small clue
Look at the small example before the general formula. Ask what changed and what stayed the same.
Close this panel to return to the exact place you were reading. These are prepared hints for this page.