News · 2026-07-22

AI Helped Crack a Famous Math Conjecture, and Humans Verified It in Lean

Mathematicians have produced an explicit counterexample that disproves the Jacobian conjecture in three complex dimensions, and, unusually for the current wave of AI-and-math hype, humans have already checked it. The counterexample was discovered by Levent Alpoge of Fable, with Terence Tao writing a public explanation and confirming calculations partly with an AI chatbot. The result is real and hand-checkable, which sets it apart from two other viral claims circulating the same week that are not yet verifiable.

Key facts

• The counterexample is a degree-seven polynomial map from three-dimensional complex space to itself whose Jacobian determinant is the constant -2, yet which sends three distinct inputs to the same output.
• It was found by Levent Alpoge (Fable); Terence Tao published the exposition on July 21 and disclosed using an AI chatbot to check calculations.
• A Lean formalization sits in Google DeepMind's Formal Conjectures repository, open and approved, and reportedly builds without gaps or custom axioms.
• The two-dimensional case remains open.

The Jacobian conjecture is one of those deceptively simple-sounding problems that has resisted proof for decades. Roughly, it asks whether a polynomial map that is locally reversible everywhere, in the sense that its Jacobian determinant is a nonzero constant, must be globally reversible, meaning no two different inputs ever land on the same output. In three complex dimensions the answer is now no, and the disproof is concrete rather than abstract. As Tao lays it out, the map has a Jacobian determinant that is the constant -2, so it passes the local test everywhere, yet he exhibits three distinct source points that map to one image point, which directly breaks global reversibility.

What makes the construction interesting is that it is not a brute-force search. It starts from multiplying a linear form by a quadratic one. A generic cubic factors into three linear pieces, so this multiplication is naturally three-to-one, which is exactly the kind of collapse the conjecture forbids. The hard part is making that ambiguity coexist with everywhere-nonsingular local behavior. The construction normalizes a resultant to remove a scaling freedom, then picks a special three-dimensional slice where the leftover geometry unexpectedly admits clean polynomial coordinates. Tao calls that slice's behavior the substantive insight and notes it is not yet fully satisfying conceptually.

The attribution matters, because the shorthand "Tao and an AI solved a famous conjecture" is wrong on both counts. Contemporaneous accounts, including Kevin Buzzard's writeup, credit Alpoge and Fable for the discovery, with Akhil Mathew credited for suggesting the problem. Tao's role was to digest the construction, check it with a chatbot, and publish a lucid explanation, and he openly says so. The AI here was a calculator and sounding board, not the author of a polished proof.

The verification story is the actually novel part. Beyond Tao's human-readable derivation, the counterexample has been formalized in Lean, a proof assistant that mechanically checks every logical step. The pull request in DeepMind's Formal Conjectures repository is still open and has drawn reviewer discussion about whether its formal statement precisely matches the classical wording, but an independent audit reports a clean build with no unproven placeholders. So "formally verified" here means a checked formal counterexample in an open, reviewed pull request, not yet a merged canonical formalization.

A cleaner comparator underscores why chain of custody matters. OpenAI's internal model separately disproved the planar unit-distance conjecture, after which external mathematicians checked and refined the argument in a companion paper. Its experts offered the right calibration: Thomas Bloom noted the argument imports heavy number theory rather than a new geometric tool, Tim Gowers cautioned that finding counterexamples is more search-friendly than proving positive statements, and Victor Wang stressed that one correct public result tells us nothing about unseen wrong AI proofs.

That calibration is exactly what the same week's louder claims lack. A widely-shared "six Erdos problems solved in five days" story traces to a public repository whose own README says proofs are verified "by AI or by Lean" and whose papers are labeled "Proposed Solution." Only one of the six has a visible Lean directory, one attributes its result to a different model than the circulating label, and the prompts instruct the model to assume a solution exists rather than test whether the problem is open. A separate viral claim that the Dinitz-Garg-Goemans conjecture was falsified rests on a shared chatbot transcript with no preprint, no formalization, and no specialist check.

Why it matters: the bottleneck in AI-assisted mathematics has moved from generation to verification, provenance, and attribution. The Jacobian result shows the good version, an explicit witness a human can check and a machine can formalize. The honest caveat is that a hand-checkable counterexample is not the same as a model autonomously delivering a reviewed proof, and several of this week's flashier headlines are candidate artifacts, not solved mathematics.

Primary source, verified: read the paper →

Ground Truth. (2026, July 22). AI Helped Crack a Famous Math Conjecture, and Humans Verified It in Lean. Ground Truth. https://groundtruth.day/news/ai-finds-real-jacobian-counterexample-humans-verify-it.html

@misc{groundtruth:ai-finds-real-jacobian-counterexample-humans-verify-it,
  title  = {AI Helped Crack a Famous Math Conjecture, and Humans Verified It in Lean},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {jul},
  url    = {https://groundtruth.day/news/ai-finds-real-jacobian-counterexample-humans-verify-it.html}
}

Topics: ai-for-science · mathematics · proof-assistants · verification