Summary: Levent Alpoge said Claude Fable found a counterexample to the Jacobian conjecture, and Kevin Buzzard reported it machine-checked in Lean. The degree-seven map on complex 3-space has Jacobian determinant −2 yet is non-invertible, disproving the general case in three or more dimensions. The result remains pending peer review, but community verification moved within about 48 hours.
On the evening of July 19, the World Cup final held most of the world’s attention. Across that same weekend, Levent Alpoge — a Harvard valedictorian who works as a researcher at Anthropic — posted on X that Claude Fable had found a counterexample to the Jacobian conjecture, a problem that Keller formalized in 1939 and that had stayed open ever since. The post drew more than 20 million views. What came next is the more interesting part: the math community did not argue, it verified. When Kevin Buzzard of Imperial College’s Xena project woke the following morning, the counterexample had already been machine-checked in the Lean proof assistant.
The conjecture goes back to Jacobi’s work on determinants, and it 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. What the new counterexample kills is the general version in three dimensions and above — and, as Terence Tao noted in the comments, it settles the broad form referenced by Smale’s Problem 16.
What the Counterexample Actually Is
Tao’s July 21 blog post lays it out: an explicit degree-seven polynomial map on complex 3-space whose Jacobian determinant equals −2 at every point, and which nevertheless carries three distinct points to the same destination, making it non-invertible. The geometric “digestion” Tao performs unfolds in stages. It starts from the multiplication map that takes a linear and a quadratic homogeneous polynomial to a cubic, a map that is generically three-to-one. Resultants then normalize the scaling symmetry, which delivers local injectivity — an étale map, in fact. From there, restrict to a three-dimensional affine hyperplane slice. The miracle arrives precisely when the associated third-order differential operator has two repeated roots: the slice turns out to be polynomially isomorphic to affine space, and out drops the counterexample. Tao’s own description is striking — the construction looks like an improbable “massive cancellation” that brute-force search would be unlikely to find. That leaves the obvious question of how the model found it at all.
From a Social Post to Lean in 48 Hours
Whether a counterexample matters depends not on the announcement but on the verification. Verification in this case, Tao notes, is a brief calculation — anyone with high-school-level math competence can check it. Paul Lezeau formalized the statement by hand and opened a PR against DeepMind’s Formal Conjectures repo. Tao, for his part, published his long digestion post and disclosed that he had used an AI chatbot to double-check the calculations; the ChatGPT conversation he had about the counterexample was later shared publicly and made the front page of Hacker News. The result is still tracked as pending peer review. What sets it apart from past claims is that it is machine-checkable, so the community can review it and use it at the same time.
Two Moods Among Mathematicians: Excitement and Unease
Buzzard’s Xena blog post put it bluntly: “Human mathematicians are being outcounterexampled.” He then inventoried the summer. On May 20, ChatGPT disproved Erdős’s unit distance conjecture, which OpenAI’s Sol model went on to fully formalize 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.”
The Lesson for AI Engineering
The week demonstrated a working pipeline: model generates, a formal system verifies, humans add understanding. Three parts of it 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.