The Note in the Margin

A story about proofs, language models, and why every claim needs a receipt.

In about 1637, in the margin of a book, Pierre de Fermat wrote that he had found a truly marvelous proof that no cube is the sum of two cubes, nor any higher power the sum of two like powers, and that the margin was too narrow to contain it. Then he died, and for three hundred and fifty years nobody could say whether the sentence in the margin was knowledge or just a sentence. It read exactly like a fact. Generations of the best mathematicians alive could not tell if it was one.

The book itself is gone. Fermat’s copy did not survive him; the page reproduced below is his son’s 1670 reprint of the note, not the note. No one alive has seen it in Fermat’s hand. The most famous claim in the history of mathematics is a copy of a claim, with no original left to check it against.

Diophantus, Arithmetica (1670 edition), the page carrying Fermat marginal note. Public domain, via Wikimedia Commons.

“Cuius rei demonstrationem mirabilem sane detexi. Hanc marginis exiguitas non caperet.”

“I have discovered a truly marvelous proof of this, which this margin is too narrow to contain.”

Pierre de Fermat, in the margin of his Diophantus, as printed in the 1670 edition

I keep coming back to that gap, because I think it is the most important distinction there is, and the one we are least equipped to make right now: the difference between something that is true and something that is merely well formed. A sentence can obey every rule of its language, name real objects, sound exactly like the truth, and still have nothing behind it. Fermat’s note sat in the margin for three and a half centuries, indistinguishable in form from knowledge.

This is not an old problem anymore. It is the problem. A language model produces sentences the way Fermat produced that note: fluently, plausibly, in the exact register of someone who knows. When a model tells you a fact, you are back in the margin. The words are well formed, and you cannot tell from the words alone whether anything stands behind them. We have built the greatest engine of well-formed sentences ever made, and we turned it loose in the one century that most needs to tell form from truth.

I met the same gap from the other side, in physics, long before the models. I spent years simulating how heat moves through crystals, and for a stretch of months two independent codes gave two different answers for the thermal conductivity of the same material. We treated it as physics, of course. We went looking for the effect that would explain the discrepancy, the subtle mechanism one code captured and the other missed (the kind of hunt a computational physicist secretly enjoys). We wrote it up as a puzzle. It was not physics. The two codes meant different things by the words “thermal conductivity”: one had computed a part, the other the whole. Once we spelled the quantity out completely, all the way down, the disagreement did not resolve so much as evaporate. There had never been a discrepancy. There had been two well-formed sentences we mistook for one.

Months. That is the real cost of not being able to tell a claim from its ground. Not embarrassment; time. Sometimes centuries of it, spent chasing a phantom the grammar invented. And staring harder at the sentences gets you nowhere. Fermat’s note could not be read into truth or falsehood. Our two numbers could not be compared into agreement. The ground had to come from somewhere else.

There is an old technology for part of this, older than Fermat, and I will admit to a moment of national pride here. In 1494 a Franciscan friar named Luca Pacioli wrote down the method Venetian merchants had used for two centuries to keep their books: every transaction entered twice, once as debit and once as credit, so that the books themselves could be made to confess an error. A number in a double-entry ledger is never alone. It carries the transaction that produced it, and the whole book has to balance. Merchants demanded receipts from their numbers five hundred years before scientists did. In my day job the word for a number that travels with its receipt is lineage. My two codes disagreed for months precisely because their numbers traveled without it. The most unaccompanied numbers of all now come out of models; the ledger has not caught up to that factory yet.

Producing the ground is what a proof is. In 1994 Andrew Wiles finally supplied Fermat’s, and it did not fit in a margin: it ran to more than a hundred pages and leaned on machinery Fermat could not have dreamed of. What closed the question was not eloquence. Other people could follow the proof step by step and confirm that each step held. A sentence asks to be believed; a proof offers to be checked.

Fermat’s tools were a century of elementary number theory. Wiles needed elliptic curves and modular forms, machinery nobody had for another three hundred years. The mainstream guess among historians (and it can only be a guess) is that Fermat had talked himself into an argument that looked sound and was not, probably one that leaned on factoring in a setting where factoring does not behave the way it does for ordinary whole numbers. That is the same trap that caught Gabriel Lamé in 1847, when he announced a general proof to the French Academy built on exactly that assumption, three years after Kummer had already shown the assumption false. Nobody had told Lamé, or he had not listened. Fermat’s note was not a lie. It was a mistake wearing the grammar of a fact, and you cannot catch that kind of mistake by rereading it. People tried for two centuries.

Andrew Wiles. Photograph copyright C. J. Mozzochi, Princeton N.J., used by permission (attribution-only license), via Wikimedia Commons.

Even when a proof existed, someone still had to judge it, and judges have interests. Newton and Leibniz spent decades arguing over who had invented the calculus, and when the Royal Society convened a committee to settle it, the committee found for Newton. The Royal Society’s president at the time was Newton. He picked the committee, and the report that carried its name was largely his own drafting; two years later he wrote an anonymous review of that same report, praising its rigor. The verdict may even have been right. That is not the point. For most of history, checking a claim has meant asking a person, and a person can hold the pen and have a stake in the answer at the same time. Newton did.

The same derivative in two grammars. Left: Newton’s pointed letters in the Method of Fluxions (1736 printing), with a reader’s own marginal note repeating the notation. Right: Leibniz’s dx and dy in Nova Methodus, Acta Eruditorum (1684). Both public domain, via Wikimedia Commons.

There is now a way to take the person out of it. In Lean, a proof assistant, a statement is a shape and a proof is an object that must fit that shape exactly. A small trusted kernel checks the fit, and there is no such thing as a plausible proof: only one that compiles, or one that does not exist. Nobody has to stay vigilant. The language simply has no way to write the lie. Mathlib, its community library, now holds on the order of two hundred thousand machine-checked theorems (I checked that number twice, because I did not believe it either), built over a decade by people who were not thinking about language models at all. They were building ground for its own sake. It turned out to be the one thing the models cannot make for themselves.

The footnote is that Wiles’s proof itself is not yet among those theorems. A project led by Kevin Buzzard at Imperial College is formalizing Fermat’s Last Theorem in Lean, funded into 2029, and Buzzard himself has said he has no real sense of how long the whole thing will take. Three and a half centuries after the note, the ground under the most famous theorem in the world is still being poured.

The truss carries its own constraints: the Golden Gate Bridge understructure. Jet Lowe, Historic American Engineering Record (HAER CA-31-14), U.S. National Park Service. Public domain, via the Library of Congress.

Physics is starting to build the same floor. Physlib, which grew out of Joseph Tooby-Smith’s HepLean, formalizes physical results so the compiler is the referee: the entropy of an ideal gas, tight-binding chains, relativity, quantum information, each one a claim with its ground attached. I sent the project a small contribution last week, the thermoelectric figure of merit. My first attempt did not compile, and I can report that the compiler is the strictest referee I have ever written for. There is also a boundary here worth stating plainly, the one my two codes should have taught me sooner: a proof that compiles buys consistency, not reality. It guarantees the sentence has ground of the kind it claims, not that the claim matches the world. The bridge still needs its load test, and a formalized law is only as true as the model inside it.

The money is starting to see it. In July 2025, Alex Gerko, the founder of XTX Markets, gave ten million dollars through Renaissance Philanthropy, half to the Lean FRO and half to Mathlib, toward natural-language interfaces to Lean and datasets for machine-assisted proof. Pricing the gap between what is claimed and what is true is Gerko’s day job. I read the ten million as a position on where that gap closes next.

Fermat’s note was wrong to write and right to make. It was a promise of ground he could not deliver, and it cost three centuries, but it named the thing exactly: a marvelous claim, and no room in the margin. We are about to be handed margins without end, filled at machine speed with sentences in the perfect register of the truth. So the question the note asked is now the only question that matters, and not only for mathematics. A confident answer from a model and a number pulled from a materials database are both notes in someone’s margin, well formed and waiting for their ground. Not whether a claim is well formed. Whether anyone can check it.