On July 20, mathematician and Lean maintainer Kevin Buzzard published a blog post that reads like a dispatch from a war zone. The enemy is not another lab or another nation. The enemy is the speed at which large language models are now generating counterexamples to open problems in pure mathematics.
“It’s been an interesting few weeks for counterexamples,” Buzzard writes, with characteristic understatement. Since May 20, when ChatGPT disproved Erdős’ Unit Distance conjecture, the pace has accelerated beyond what most mathematicians — including Buzzard — thought possible. A 60-year-old question of Grothendieck about finite flat group schemes fell on July 11. The Jacobian Conjecture, a 100-year-old open problem in algebraic geometry, fell on July 19. All three were solved by LLMs. All three were formalized in Lean, the interactive theorem prover, within days or hours of discovery.
The pattern is not a fluke. It is a new mode of mathematical production.
What changed
The Erdős counterexample was the first shot. ChatGPT produced an argument relying on a deep theorem of Golod and Shafarevich from the 1960s, itself a 100-plus-page result in global class field theory. Human mathematicians with early access vouched for the reasoning. But the proof was not formalized. Buzzard, who has spent nine years arguing that interactive theorem provers should be central to mathematics, asked the obvious question: is the counterexample in Lean?
Within a week, Logical Intelligence — whose chief science officer is Fields Medalist Mike Freedman — had autoformalized the entire ChatGPT-generated paper. Then on June 26, OpenAI’s Boris Alexeev announced that ChatGPT’s new model, Sol, had produced a complete formalization of the Erdős counterexample from scratch, assuming nothing beyond the axioms of mathematics. The code ran to 1.2 million lines of Lean, generated in three weeks. For comparison, mathlib — the community-maintained mathematics library — is 2.3 million lines and took nine years to write.
“Perhaps it was at this point that the penny really dropped for me,” Buzzard writes. “Large AI-generated developments of mathematics are inevitable.”
The Grothendieck counterexample
The Grothendieck counterexample came next, during a workshop Buzzard was running at Imperial College London on formalizing Fermat’s Last Theorem. Attendees had access to Claude Fable and ChatGPT Sol, plus a tool from Logos Research for autoformalization. Over lunch, University of Chicago professor Akhil Mathew raised an old question of Grothendieck: whether every finite free group scheme of order n is killed by n. Deligne had proved the commutative case. Grothendieck had proved it for reduced bases. Partial results existed. The full question had been open for 60 years.
Buzzard suggested that Mathew get the AI to work on it. The day after the workshop ended, Mathew messaged Buzzard that Sol had found a counterexample, sending a 12-page PDF. Buzzard replied that he would not read AI-generated informal mathematics and asked for a Lean formalization. Four hours later, Fable had autoformalized the entire thing. The Lean file was 1,076 lines. It compiled in under five minutes.
“At this point I knew that we had a counterexample — a group scheme of order 4 which was not killed by 4,” Buzzard writes. He suggested Mathew make a pull request to mathlib, which he did.
The Jacobian Conjecture
The Jacobian Conjecture fell 12 hours before Buzzard’s post went live. Levent Alpöge posted on X that Fable had found a counterexample. Paul Lezeau formalized it manually and made a pull request to DeepMind’s Formal Conjectures repository. The conjecture had been open for 100 years. It was apparently solved during the 2026 World Cup Final.
Buzzard’s colleague at Imperial dismissed the Grothendieck result as trivial — a sign that humans had not bothered to think about the problem. Buzzard notes that he himself had spent a week on it earlier in his career. “In my mind my colleague is just going through the five stages of grief,” he writes. “Right now they seem to be in the denial phase.”
The implications
The pattern is clear. LLMs are now better at finding counterexamples than human mathematicians. The formalization pipeline — from natural-language conjecture to verified Lean proof — is now fast enough that a result can be checked, compiled, and made public in hours. The bottleneck is no longer the mathematics. It is the willingness of the community to accept what the machines produce.
Buzzard’s post contains a telling detail. A professor at Imperial expressed surprise that graduate students were paying $200 per month for access to Sol and Fable. Buzzard emailed back: “In my opinion, any PhD student who was not paying $200 per month to access these tools was crazy.” Harvard, he notes, already gives free Fable access to all PhD students, postdocs, and faculty.
The economics are shifting. The cost of generating a counterexample to an open problem is now the cost of a monthly subscription. The cost of verifying it is a few minutes of compute time. The cost of ignoring it is irrelevance.
What to watch
The next frontier is not more counterexamples. It is positive results. LLMs have shown they can find holes in conjectures. The harder question is whether they can construct proofs of deep theorems — the kind that require building new theory rather than tearing down old guesses. The Erdős counterexample relied on a 100-plus-page theorem from the 1960s. The Grothendieck counterexample was a thousand-line Lean file. Neither required the machine to invent a new subfield of mathematics.
Buzzard ends his post with a question he posed to Mathew: try the Hodge conjecture next. The Hodge conjecture is one of the seven Clay Millennium Problems. If a machine disproves it, the shock will be orders of magnitude larger than anything that has happened so far. If a machine proves it, the shock will be larger still.
The field is not ready. The formalization infrastructure is barely keeping pace. The social norms of mathematics — peer review, trust, credit — were built for human-scale discovery. They are being outcounterexampled.