The Proof AI Touched

Fermat's Last Theorem says there are no positive whole numbers a, b, c that satisfy aⁿ + bⁿ = cⁿ when n is bigger than 2. It looks like something you could scrawl on a napkin. It is, in fact, one of the deepest sinkholes in all of mathematics. Andrew Wiles finally proved it in the mid-1990s, but not with anything Fermat could have recognized — his proof runs to over a hundred dense pages, detours through entire continents of modern mathematics, and rests on the labor of dozens of other mathematicians. Almost no one on Earth can hold the entire argument in their head at once. We believe it's true. That is a subtly different thing from knowing.

Which is where the strangeness begins. A team led by Kevin Buzzard at Imperial College London is rebuilding Wiles's proof from the ground up inside a piece of software called Lean — a "proof assistant" that refuses to accept a single logical step unless it can verify that step with total, pedantic rigor. Nothing gets hand-waved. Nothing gets "left as an exercise for the reader." Every inference, down to the plumbing of arithmetic, has to be spelled out in a language Lean's kernel can mechanically check. And here is the thing to be precise about: Lean is not intelligent. It does not understand Fermat, or numbers, or anything at all. It is a monstrously stubborn accountant built on decades-old type theory, and that stubbornness — not any spark of mind — is exactly what makes the result trustworthy.

Artificial intelligence enters this story in a supporting role that is easy to oversell. Formalizing a hundred-page proof into Lean's unforgiving syntax is a staggering amount of tedium, and AI tools are increasingly enlisted to help — autocompleting boilerplate, suggesting the next step, closing the small gaps. That help matters; it may be the difference between a project that finishes this decade and one that doesn't. But notice what the AI is not doing. It is not the thing that makes the proof certain. The certainty comes from Lean's kernel checking every line, indifferent and exact. AI is the power tool that makes the cathedral faster to raise. Lean is the plumb line that says it's actually standing straight.

Sit with the shape of this for a moment. We took the crown jewel of human reasoning — a theorem that took three and a half centuries and the combined genius of a civilization to crack — and our next move is to spell it out, in full, for a machine too literal-minded to skip a step, just to be sure we understood our own greatest achievement. This is either the height of intellectual humility or the funniest thing consciousness has ever done to itself. Probably both.

Because here is the quiet vertigo underneath it. A formal proof in Lean is a strange object: it is more certain than anything in Wiles's papers — checkable by any machine, immune to the human tendency to nod along and miss a gap. And yet building it doesn't diminish the humans doing the work; it demands more of them. Every step Wiles could leave implicit, the formalizers have to drag into the light and name. They come out understanding the proof more intimately than almost anyone alive. So the thing that gets outsourced isn't the understanding. It's the trust. We used to certify a theorem like this the way we certify most deep mathematics: by deferring to the handful of experts who can actually follow it. Now the certification lives in an artifact any machine can re-check. The knowing that it's true and the feeling of seeing why are coming apart — and it's the knowing, not the feeling, that migrates out of human heads and into the plumbing.

And that migration cuts two ways at once. It democratizes certainty: you no longer have to take the experts' word for it, you can run the checker yourself. But it also concentrates certainty, because now you have to trust Lean — its kernel, its axioms, the foundations the whole edifice rests on. The old question, do you believe the mathematicians?, quietly becomes a new one: who verifies the verifier? The trust didn't evaporate. It slid downward, out of a priesthood of human minds and into a few thousand lines of code and the axioms beneath them. Certainty became a commons anyone can inspect — and, in the very same motion, grew a new root of faith at the bottom of the stack.

Fermat's marvelous unwritten proof was almost certainly wrong — the mathematics he'd have needed didn't exist for centuries. But his margin note started a chain of consequence he could never have imagined: a lawyer's idle boast, becoming a 358-year obsession, becoming a hundred-page cathedral of logic, becoming a formal artifact a machine can check line by line without ever once knowing what it means. Consciousness invented a question, spent centuries answering it, and then built a tool too rigid to fool itself and set it to grade the homework.

Somewhere, a bag of atoms is verifying, line by line, that another bag of atoms was right about numbers that don't exist in any physical place at all. The checker feels nothing. The mathematicians feel everything. And the truth sits between them now — more certain than it has ever been, and not one bit more understood — still waiting, as it always has, for someone to see why. The margin was always too small. Turns out the whole universe barely fits it either.