On July 20, 2026, Kevin Buzzard, a mathematics professor at Imperial College London, wrote a blog post with a line so blunt it stung his peers: human mathematicians are being “outcounterexampled.” The reason? In just two months, AI had overturned three mathematical conjectures that had stood for decades — one of which had remained unsolved for nearly a century.
Buzzard himself said: “It took me less than five minutes to verify a counterexample to a 60-year-old open problem in algebraic geometry. I downloaded the Lean code to my laptop, it compiled, and I nodded and said, ‘Yes, that is indeed a counterexample.’”
Five minutes. That is the dividing line between human mathematics and AI mathematics. This article explores when that line was drawn — and what it means.
Counterexamples: A Sharper Knife Than Proofs
Let’s start with a basic concept. In mathematics, proving a statement true is hard — you need a rigorous derivation where every step is correct. But proving a statement false is relatively “simple”: you only need to find a counterexample — a concrete construction that satisfies all the premises but violates the conclusion.
If someone claims “all swans are white,” you don’t need to check every swan on the planet. You just need to find one black swan.
A single counterexample can end a mathematician’s life’s work. That is precisely why counterexamples have always played a creative role in mathematics — they reveal the boundaries of a theory, forcing mathematicians to re-examine assumptions, refine definitions, and push theory forward. In a sense, counterexamples are fuel for mathematical progress.
AI is now pushing the art of “finding black swans” to an unprecedented scale.
May to July 2026: The AI Triple Strike
Here is a timeline of what happened over those three months.
First strike: Erdős unit distance conjecture (proposed 1946, refuted May 20, 2026)
A discrete geometry problem posed by the legendary Paul Erdős in 1946. ChatGPT produced a counterexample construction. Buzzard’s first reaction was to ask: “Has it been verified in Lean?” It hadn’t. But within a week, Fields Medalist Mike Freedman (now Chief Scientist at Logical Intelligence, an AI company) emailed him — their system had automatically translated the argument into Lean code.
A month later, OpenAI’s Boris Alexeev used the new Sol model to do a more thorough job: starting from mathematical axioms, he fully formalized the entire counterexample. Sol generated 1.2 million lines of Lean code in the process.
For context: mathlib, the core mathematics library that the Lean community spent nine years building, contains only 2.3 million lines of code. In three weeks, AI generated more than half of what humans had produced in nine years. Buzzard’s verdict was simple: “Large-scale AI-generated mathematics is now inevitable.”
Second strike: Grothendieck’s group scheme problem (proposed 1960s, refuted July 11, 2026)
Grothendieck was one of the greatest mathematicians of the 20th century. Sixty years ago, he asked: is a finite free group scheme of order n necessarily killed by n? Deligne proved the commutative case; Grothendieck himself proved the case where the base ring is reduced — but the full result had remained open.
Sol found a counterexample. The entire proof is only 1,076 lines of Lean code. Buzzard verified it in under five minutes. He suggested that mathematician Akhil Mathew submit the counterexample to the mathematics library — and then joked, “Maybe try the Hodge conjecture next?”
Third strike: Jacobian Conjecture (proposed 1939, refuted July 19, 2026)
This was the heaviest blow. The Jacobian Conjecture is an inverse problem about polynomial maps: if the Jacobian determinant of a polynomial map is a nonzero constant, must the map be invertible? The question had been open since 1939, widely regarded as one of the most seductive yet stubborn conjectures in algebraic geometry.
This time, the strike came from Anthropic’s Claude Fable. It found the counterexample during the 2026 World Cup final. The next day, Terence Tao — one of the most respected mathematicians alive — published a blog post carefully “digesting” the mathematical implications of this counterexample.
Tao’s calculations revealed: the counterexample is a polynomial map in three variables with maximum degree seven. Its Jacobian determinant is -2 — satisfying the nonzero constant condition — yet the map maps three distinct input points to the same output point, failing to be injective and therefore not invertible. Even more remarkable, the AI used 120 adjustable parameters to control the 1,329 coefficients that could theoretically appear in the Jacobian determinant, causing all non-zero terms to cancel out exactly. In Tao’s words: “This looks like a huge miracle.”
Lean + LLM: When Creativity Meets Irrefutable Proof
Let’s step back and examine the technical logic.
Lean is a “mathematics compiler.” When you write a mathematical proof in Lean, every line of reasoning must pass strict type-checking. There is no “the omitted step is obvious” — everything obvious must be expanded down to the atomic level. If the code compiles, your proof is mathematically absolutely correct — no human referee’s trust required.
The LLM handles the “ideation,” and Lean handles the “adjudication.” The inherent weakness of LLMs in mathematics is that they hallucinate — they produce plausible-looking reasoning even when they don’t know the answer. Lean addresses this at the root: the LLM generates Lean code, and the compiler checks it immediately. If compilation fails, the LLM receives the error message and can revise. Iterate until the code compiles — and at that point, the AI-generated mathematical result has rigorous correctness guarantees.
In March 2026, a paper titled “Learning to Disprove” systematically laid out this methodology. The core insight: instead of asking an LLM to “prove” a proposition (easy to hallucinate), ask it to “find counterexamples” — because once a counterexample compiles in Lean, it is ironclad. The authors used a “signature mutation” strategy, systematically removing conditions from known theorems to generate training data requiring counterexamples, then trained the LLM with a multi-reward mechanism. The result: a 49% improvement in accuracy on counterexample-generation tasks.
This is the technical foundation of “outcounterexampling”: LLMs provide the creativity, Lean provides the proof, and human mathematicians become spectators — at least in the verification stage.
The Five Stages of Grief in Mathematics
Buzzard candidly recorded his colleagues’ reactions. At an Imperial College lunch, he heard a fellow mathematician say: “If counterexamples are so easy to find, it just means humans haven’t spent enough time thinking about the problem.” Buzzard smiled bitterly to himself — he had once spent an entire week on that very “not-worth-the-time” problem.
That is textbook denial.
Then came the bargaining. A professor emailed Buzzard, astonished that graduate students would pay $200 a month for Sol and Fable subscriptions. Buzzard’s reply was direct: “Any PhD student who does not spend $200 a month on these tools is being irrational.” Harvard had already given free Fable access to all its mathematics PhD students, postdocs, and faculty.
Whatever one’s emotional response, one fact is clear: in mathematical research, the capability gap between those who wield AI tools and those who don’t is widening by the month.
The Direction Tao Set
Among all the responses, Tao’s stance is perhaps the most instructive. He did not question AI’s capabilities, nor did he fall into philosophical debates about “whether this still counts as mathematics.” He sat down, wrote a detailed blog post, computed the weighted homogeneity of the polynomial, offered a geometric reconstruction, and even published the full transcript of his conversation with GPT-5.
This is the attitude of a working mathematician: the results are on the table — understand them first, then put them to use.
In the HN discussion, Tao noted: “It tells us that some seemingly impossible mathematical constructions can be found if the search space is large enough.” The crucial subtext is: the search space may be enormous, but AI has taught us how to search. And this is only the beginning.
What’s Left for Mathematicians?
If AI can find counterexamples, verify proofs, and automatically formalize entire theories, what’s left for human mathematicians?
Buzzard’s answer: understanding and interpretation. “The real value of these extraordinary examples,” he wrote, “lies in the deeper understanding they can bring to human mathematics.” Akhil Mathew is already trying to understand the structure behind the Grothendieck counterexample at a deeper level — asking “what is really going on here” rather than stopping at “it’s a random construction and a coincidental computation.”
AI can tell you “it doesn’t hold,” but it often cannot tell you “what this means for our mathematical picture.”
Throughout history, mathematicians have repeatedly outsourced “computation” to machines, then focused on higher-level “understanding” and “construction.” Now, “finding counterexamples” and “verifying proofs” can be outsourced too. What remains for humans is arguably the very core of mathematics: when the machine puts a counterexample on the table, truly understanding why it matters — and what we can learn from it.
This is not the end of mathematics. But the mathematician’s role is undergoing an irreversible evolution.
Reference links:
- Xenaproject — Kevin Buzzard’s original blog post “Human mathematicians are being outcounterexampled”
- HN discussion (id: 48998362) — Community discussion around Tao’s Jacobian Conjecture post
- Lobsters discussion (s/wfmpqr) — Technical community’s deep commentary on AI math counterexamples
- Terry Tao’s blog — Digestion and mathematical reconstruction of the Jacobian Conjecture counterexample
- SBSeminar — Mathematical details of the new Jacobian Conjecture counterexample
- arXiv 2603.19514 — Learning to Disprove: formal counterexample generation with LLMs
- New Scientist report — AI’s solution to an 87-year-old mathematical problem
- GitHub DeepMind Formal Conjectures — Formal conjecture repository containing the Jacobian counterexample
