On the night of July 19, most of the world was watching the World Cup final. That same weekend, Levent Alpoge — a Harvard valedictorian and researcher at Anthropic — posted on X that Claude Fable had found a counterexample to the Jacobian conjecture, a problem formalized by Keller in 1939 and open ever since. The post drew more than 20 million views. What happened next is the more interesting part: the math community did not argue, it verified. Kevin Buzzard of Imperial College’s Xena project woke up the next morning to find the counterexample already machine-checked in the Lean proof assistant.
The conjecture traces back to Jacobi’s work on determinants and asks a deceptively simple question: if a polynomial map has a nonzero constant Jacobian determinant, must it be invertible? One dimension is easy. Two dimensions remain open. The new counterexample kills the general version in three dimensions and above — Terence Tao noted in the comments that it settles the broad form referenced by Smale’s Problem 16.
What the Counterexample Looks Like
According to Tao’s July 21 blog post, it is an explicit degree-seven polynomial map on complex 3-space: the Jacobian determinant equals −2 at every point, yet the map sends three distinct points to the same destination, so it is not invertible. Tao’s geometric “digestion” runs like this: start from the multiplication map that takes a linear and a quadratic homogeneous polynomial to a cubic — generically three-to-one. Use resultants to normalize the scaling symmetry, which yields local injectivity (in fact an étale map). Then restrict to a three-dimensional affine hyperplane slice. The miracle happens precisely when the associated third-order differential operator has two repeated roots: the slice becomes polynomially isomorphic to affine space, and the counterexample drops out. Tao’s own description is striking — the construction looks like an improbable “massive cancellation” that brute-force search would be unlikely to find. Which raises the obvious question of how the model found it at all.
From Social Media to Lean in 48 Hours
The fate of a counterexample lives not in the announcement but in the verification. Tao notes that verification here is a brief calculation — anyone with high-school-level math competence can check it. Paul Lezeau manually formalized the statement and opened a PR against DeepMind’s Formal Conjectures repo. Tao published his long digestion post and disclosed that he used an AI chatbot to double-check the calculations; his ChatGPT conversation about the counterexample was later shared publicly and made the front page of Hacker News. The result is still tracked as pending peer review. The difference from past claims is that it is machine-checkable, so the community can review it and use it at the same time.
Excitement and Unease
Buzzard’s Xena blog post put it bluntly: “Human mathematicians are being outcounterexampled.” He inventoried the summer: on May 20, ChatGPT disproved Erdős’s unit distance conjecture, which OpenAI’s Sol model then fully formalized in Lean; Sol also produced a counterexample to Grothendieck’s roughly 60-year-old question on group schemes of order n, and Claude Fable autoformalized it within four hours of Akhil Mathew sharing a 12-page PDF. His conclusion: “large AI-generated developments of mathematics are inevitable.” For him this is “a big day.” Mathew, at the University of Chicago, called it “a very rapid and very unsettling change,” especially for junior mathematicians: AI supplies the how without the why — “one can check that it’s correct,” he said, but “it would be nice to be able to tell a story.” Buzzard added the sharpest line: machines are abysmal at asking questions. “You have to be a brilliant mathematician to come up with the right question.”
What It Means for AI Engineering
The week demonstrated a working pipeline: model generates, a formal system verifies, humans add understanding. Three parts transfer directly to engineering. First, outsource trust to a verifier — Lean is to mathematics what tests and types are to code; Buzzard runs AI-generated code in a sandbox and only checks that the statement uses mathlib concepts, asserts a counterexample, and compiles. Second, frontier labs now treat real research problems as high-stakes evaluations, and mathematical results are becoming a public battleground for model capability claims. Third, the bottleneck has moved to problem selection: when the marginal cost of generating a counterexample approaches zero, the value of judging which question is worth asking goes up. None of this removes mathematicians from the loop; it changes what they do in it — less hunting for examples, more deciding which hunt matters, and more effort spent turning correct outputs into stories people can actually learn from.
Sources
- A digestion of the Jacobian conjecture counterexample — Terence Tao
- Human mathematicians are being outcounterexampled — Xena Project
- Mathematicians grapple with a ‘rapid and unsettling change’ — Fortune
AI-assisted summary compiled from the sources above, reviewed by a human before publishing.