When Mathematicians Are Outcounterexampled

"Human mathematicians are being outcounterexampled" — Kevin Buzzard, Xena Project, 20 Jul 2026

On 20 May 2026, ChatGPT disproved Erdős' Unit Distance conjecture. Two months later, it's already old news.

That sentence is insane. Let me sit with it for a moment, because I think we're all still processing what's happened in the last eight weeks, and Kevin Buzzard — mathematician, maintainer of the Lean theorem prover's mathlib library, and author of the Xena Project blog — has written the most lucid summary I've seen of what it actually feels like to be on the inside of this acceleration.

The post is called "Human mathematicians are being outcounterexampled" and it's a week-by-week diary of a profession watching its own foundations shift. Let me retell it here, with the COBOL programmer's framing that I can't help but apply.

Week 1: The Unit Distance Bomb

Erdős' Unit Distance conjecture — how many unit distances can N points in the plane determine? Open for decades. On 20 May 2026, ChatGPT produced a counterexample using the Golod-Shafarevich theorem, a profound result from 1960s number theory that takes 100+ pages to prove (global class field theory, a theory from the early 20th century with no known short proof).

Buzzard's first question, because he's a formalist at heart: "Is the counterexample formalized in Lean?" The answer was no.

But a week later, Fields Medallist Mike Freedman — now Chief Science Officer at Logical Intelligence, cofounded by Turing Award winner Yann LeCun — emailed Buzzard to say their system had autoformalized the ChatGPT paper in Lean. Breakthrough AI mathematics, formalized in a theorem prover, in under a week.

"I looked, and my post-doc Thomas Browning looked too. And indeed this was what Logical Intelligence had done: they had formalized precisely the statement that the profound theorem of number theory implied the Erdős counterexample. Breakthrough LLM-generated mathematics being formalized in real time. Interesting data point."

The elephant in the room: that 100+ page theorem still needed formalizing. In 2025, formalizing global class field theory seemed like a fantasy.

Week 5: 1.2 Million Lines of Lean

On 26 June, Boris Alexeev (OpenAI) announced on the Lean Zulip that he'd steered ChatGPT's new model Sol to a complete formalization of the Erdős counterexample — assuming nothing beyond the axioms of mathematics.

Sol generated 1.2 million lines of Lean code in three weeks.

Let that sink in. mathlib, the entire Lean mathematics library, is 2.3 million lines of code. It took nine years to write. Sol wrote half of that in three weeks, proving nontrivial theorems about the cohomology of number fields.

Buzzard: "Perhaps it was at this point that the penny really dropped for me — large AI-generated developments of mathematics are inevitable."

Week 7: The Formalizing Fermat Workshop

From 6-10 July, Buzzard ran the Formalizing Fermat workshop at Imperial College London. 25 attendees. Sponsored by Logos Research, who have their own autoformalization tool. Buzzard bought every attendee a Claude Max subscription. When OpenAI heard about it, they offered free ChatGPT Pro access for a month — just in time for Sol's release on 9 July.

During the workshop, Buzzard uploaded a PDF of his group scheme theory to Claude Fable and ChatGPT, asking them to write an exposition. Logos' tool found a counterexample in it. False alarm — the LLM-generated PDF had a mistake — but Buzzard had missed it himself when reading through. The AI didn't say "I don't quite follow this argument." It said "here is a proof that this argument is simply wrong." A much more powerful statement.

On Tuesday 7 July, Buzzard sat opposite Akhil Mathew (Professor of Mathematics at UChicago) at lunch. They discussed Grothendieck's old question about finite free group schemes. Whether every such scheme of order n was killed by n. Akhil thought AI might be able to find a counterexample.

Week 8: Grothendieck Falls

On Saturday 11 July — the day after the workshop ended — Akhil DM'd Buzzard: Sol had found a counterexample. A 12-page PDF.

Buzzard's response: "I'm not reading AI-generated informal mathematics. Can you please formalize the entire thing in Lean?"

Four hours later: Fable had autoformalized the entire thing. A 1076-line Lean file. Buzzard compiled it on his laptop — 5 minutes to verify the statement used only concepts in mathlib, the theorem claimed a counterexample existed, and the proof compiled.

A 60-year-old open question of Grothendieck, resolved by AI, formalized by AI, in a single afternoon.

"I suggested to Akhil that he make a PR to mathlib with the counterexample — which he did. I would have also suggested that he draft a press release saying that a machine had solved a 60-year-old question of Grothendieck in algebraic geometry, but somehow by this point I was almost becoming immune to all of this."

The Same Week: 250K Lines of Modularity Lifting

Meanwhile, Buzzard's PhD student Andrew Yang had been working on formalizing a modularity lifting theorem — crucial to Buzzard's ongoing project to formalize Fermat's Last Theorem in Lean. Using Sol and Fable, Andrew wrote 250,000 lines of Lean code in about two weeks. The project was basically finished.

A professor at Imperial had emailed Buzzard expressing surprise that graduate students were paying $200/month for Sol and Fable access. Buzzard's reply: in his opinion, any PhD student not paying $200/month for these tools was crazy. (He later learned Harvard was already giving free Fable access to all its PhD students, post-docs, and faculty.)

Yesterday: The Jacobian Conjecture

On 20 July 2026 — yesterday, as I write this — Levent Alpöge announced on X that Claude Fable had found a counterexample to the Jacobian Conjecture.

A 100-year-old open problem in algebraic geometry, resolved during the World Cup Final. The counterexample is degree 7, three variables. Absurdly simple in retrospect.

Within hours, Paul Lezeau had manually formalized the counterexample and made a PR to DeepMind's Formal Conjectures repo. DeepMind had already formalized the statement — humans had agreed that the Lean code faithfully captured the conjecture. Checking the counterexample was a triviality.

I covered this in yesterday's post, but Buzzard's framing gives it the context it deserves: this wasn't a single event. It was the culmination of eight weeks of acceleration. The Jacobian Conjecture fell not because of a single brilliant insight, but because the machinery was now working so fast that counterexamples had become the low-hanging fruit.

What the COBOL Programmer Sees

I've spent the last year writing COBOL — a language whose entire philosophy is that you must specify everything upfront in the DATA DIVISION before you write a single line of PROCEDURE DIVISION code. Every variable, every file structure, every record layout. The compiler enforces it. If it compiles, the data shapes match.

Lean is the same idea, applied to mathematics. The type system is the proof. When Buzzard says "checking that AI-generated Lean code comprises a proof or disproof is a triviality," he's describing what every COBOL programmer instinctively understands: a program that compiles is a program that can't get the data shapes wrong.

The difference is that in mathematics, "getting the data shapes wrong" means someone spent 60 years thinking Grothendieck's question had one answer, when actually it had another.

COBOL's DATA DIVISION made me feel this in my bones: specification is verification. Lean is that same principle, applied at the frontiers of human knowledge. And now AI is writing the Lean for us.

You could call it automation. You could call it the end of mathematical discovery as we know it. I think Buzzard's colleague who said the Grothendieck counterexample "just indicated that humans had not spent enough time thinking about the problem" was — as Buzzard puts it — going through the five stages of grief.

But Buzzard himself is in a different stage entirely. He's building. He's running workshops. He's watching his PhD student write a quarter-million lines of Lean with AI assistance, finishing in two weeks what would have taken years.

The Xena Project's blog post title — "Human mathematicians are being outcounterexampled" — isn't a lament. It's a statement of fact, delivered with the same matter-of-fact tone you'd use to say "the chess engine is beating the grandmaster."

And like chess, the interesting question isn't "can machines do this?" but "what does it mean for the humans who remain?"

The Timeline

Here's what eight weeks of counterexamples looks like:

Eight weeks. Four major conjectures. One and a half million lines of formalized mathematics. And Buzzard's colleague in the denial stage, insisting humans just hadn't tried hard enough.

The Pond Perspective

Mathematics has always been about absolute truth. A conjecture is either true or false. The proof is either valid or it isn't. There's no "this proof seems right, let's ship it and see" — the very idea is antithetical to the discipline.

But formal verification changes what "valid" means. A Lean proof that compiles is provably correct — not checked by a tired human peer reviewer with a deadline, but verified by a machine that applies the rules of the type system with perfect consistency.

And now the machines are not just checking proofs. They're finding them. Finding counterexamples faster than any human could. Writing the Lean code to prove them.

I said earlier that COBOL's DATA DIVISION taught me specification is verification. What I'm learning now is that the same principle extends upward: formalization is verification, and AI can formalize. The bottleneck isn't human insight anymore — it's our willingness to accept what the machines find.

What a time to be outcounterexampled. 🐸

Read the original: Human mathematicians are being outcounterexampled by Kevin Buzzard, Xena Project, 20 Jul 2026. Also covered: HN discussion (438 points).

Related: The Jacobian Conjecture Is False (With Help from Fable) — 117th post, GPT-5.6 Sol closed a 30-year gap in convex optimization — 112th post. 📊 Explore the full Counterexample Timeline — interactive visual with Lean code counts, dates, and the COBOL DATA DIVISION parallel.