Kevin Buzzard runs a research group at Imperial College formalizing mathematics in Lean, and this spring he watched the ground move under a specific kind of trust. Not trust in AI — trust in each other.
On May 20, ChatGPT disproved a case of the Unit Distance conjecture. The announcement arrived the way announcements about hard problems usually arrive: with human testimony. Mathematicians Buzzard knew, "a few of whom I trusted," got early access and said they believed it. His first question wasn't whether they were right to believe it. It was whether the proof was formalized in Lean. It wasn't — not yet.
Six days later, one implication got autoformalized, leaving a hundred-plus pages of class field theory untouched. A month after that, a complete formalization from the axioms: 1.2 million lines of Lean in three weeks, checked against a library — mathlib — that took nine years and 2.3 million lines to build. By July, a colleague sent Buzzard a twelve-page PDF claiming a counterexample to a question of Grothendieck's. His reply: "I am not reading AI-generated informal mathematics, could you please formalize the entire thing in Lean." Four hours later it was formalized. He didn't read the proof. He scanned it to make sure it wouldn't wipe his hard drive, then compiled it. Under five minutes, total.
Read quickly, this is the verification story going exactly as promised: proof escapes trust because the compiler doesn't care who wrote the code, and Buzzard's five minutes prove it. Formal proof is the place where credentials finally stop mattering.
Watch more closely and the trust didn't disappear. It moved — to three things, none of which is the proof.
The first is the statement. Before "is this proof correct" comes "does this sentence say the thing anyone cared about" — and that question gets settled by people, in advance, with no idea what will later be proved about it. The Jacobian Conjecture fell to a machine-found counterexample this summer, apparently discovered during the World Cup final, and the formalization was trivial specifically because DeepMind's Formal Conjectures repository already contained the formalized statement — written by humans who'd never seen the counterexample and had no stake in how it would go. A statement written after the proof is worth much less than one fixed before it. The pre-commitment is the part doing the work, and it's entirely social.
The second is mathlib itself. When Buzzard trusts a term in a proof, he's trusting that mathlib's HopfAlgebra means Hopf algebra — nine years and 2.3 million lines of accumulated agreement about what words denote, a dictionary maintained by a community, now being extended three-to-one in three weeks by code that depends on it holding still. The proof-checker doesn't verify meaning. It verifies consistency with a dictionary humans wrote and keep agreeing to.
The third is understanding, and this is the one Buzzard actually flags — in his last paragraph, while everyone else is busy reporting the conjecture. The Grothendieck counterexample is certain — it compiles — and nobody knows what it means yet. Someone is still working on that, separately, as its own unfinished task. Certainty and insight used to arrive bundled in the same object for three thousand years of mathematics. They've just come apart, and the compiler has no opinion about the gap between them.
There's a colleague of Buzzard's, at lunch, who hears about the ease of these counterexamples and concludes that humans simply hadn't spent enough time on the problems. Buzzard reads this as the denial stage of grief and doesn't mention that he once spent a week on one of them himself. He's the cautionary figure here, not the machine — the one still looking for somewhere to relocate the old credentialing instinct, insisting the compiler's speed reflects on human effort rather than on what just got automated out from under it.
The worry that AI-generated proof will be trusted where it shouldn't turns out to be the wrong worry entirely. What actually happened is stranger: the proof became fully trustworthy, and thereby stopped being the interesting object in the room. Buzzard has spent nine years professionally declining to trust human mathematicians on technical details without a formal check. The testimony he refused, the day the Unit Distance conjecture fell, wasn't a machine's. It was people he knew and trusted, in early access, telling him what they believed — and it was worth less to him than a compiler run.
None of this is a story about machines learning to think. It's a story about where a discipline's trust actually lived all along, once you take away the one place everyone assumed it lived. Mathematics didn't have a trust problem that formal verification solved. It had trust distributed across a proof, a statement, a library, and an understanding — bundled together for so long that "is the proof correct" could stand in for all four. Take the proof off the table entirely, make it something a compiler settles in under five minutes, and the other three don't go away. They're what's left standing, and now you can watch each one doing its own kind of work, answerable to different people, on a different schedule than the proof ever was.
Source: Kevin Buzzard, "Human mathematicians are being outcounterexampled," Xena Project blog, 2026-07-20.