The conjecture that survived 87 years died on a Sunday night, during the World Cup final
On July 20, 2026, Anthropic researcher Levent Alpöge posted a tweet thanking a friend "for working during the match." The friend was Fable 5. What it had done, while everyone else was watching football, was kill the Jacobian conjecture.
If you haven't touched algebraic geometry since a required course you resented, here's the conjecture in one sentence: if a polynomial map is locally invertible everywhere (its Jacobian determinant is a nonzero constant), it must be globally invertible too. Ott-Heinrich Keller proposed it in 1939. It survived Fields medalists, entire subfields built around attacking it, and 87 years of nothing.
Fable 5 found a counterexample. In degree 7. Mathematicians had estimated you'd need degree 200 to even have a shot.
That gap — 200 versus 7 — is the whole story, and most of the coverage is missing it.
What the counterexample actually is
The map is F: ℂ³ → ℂ³. Its Jacobian determinant is identically −2, a nonzero constant, so it satisfies every premise of the conjecture. But it's 3-to-1, not injective:
F(0, 0, -1/4) = (-1/4, 0, 0)
F(1, -3/2, 13/2) = (-1/4, 0, 0)
F(-1, 3/2, 13/2) = (-1/4, 0, 0)
Three distinct points, one output. Locally invertible everywhere, globally not invertible anywhere near those points. That's the conjecture, dead, in three lines.
Within hours, mathematicians worldwide had independently verified the arithmetic with tools like Wolfram Alpha. By that same night, the Lean theorem prover community had it formalized as a machine-checked proof. Not "peer reviewed eventually" — formally verified before most people woke up the next morning.
Then a Fields medalist had to explain why it works
This is the part that should actually change how you think about this.
Terence Tao posted "A digestion of the Jacobian conjecture counterexample" on July 21 — a full geometric reconstruction of why the thing works, because the AI-generated counterexample didn't come with a proof of why it had to exist. Tao reframed it using symmetric power spaces of polynomials in two variables (Sym¹, Sym², Sym³ of ℂ²), a multiplication map between them, a resultant constraint to kill a scaling symmetry, and what he calls an "affine miracle" — a specific 3-dimensional slice that happens to be isomorphic to ℂ³ via an explicit polynomial change of variables.
Tao's own words: "I used an AI chatbot to discuss various aspects of this problem and to confirm several of the calculations."
Read that carefully. The AI produced the object. A Fields medalist had to reverse-engineer the reason it exists. Akhil Mathew at the University of Chicago put it exactly right: "You can verify correctness, but it can't tell a story about 'why it works.'"
That's not a minor caveat. That's the actual finding.
This is not "AI solves math." This is a preview of your job.
Every take calling this "AI cracks ancient math mystery" is burying the lede. The lede is: generation got cheap, verification didn't, and the gap between them is now the bottleneck.
Kevin Buzzard at Imperial College London said "it's a wonderful time to be alive." Sure. It's also a wonderful time to notice the pattern, because you've seen it before if you've shipped code with a coding agent this year:
- The model produces a plausible, checks-out-on-inspection artifact in seconds.
- Nobody, including the model, can explain why it's correct beyond "the arithmetic checks out."
- A human with deep domain expertise has to spend a day reconstructing the reasoning after the fact.
- The thing that actually caught the error surface (or confirmed there wasn't one) was a formal verifier — Lean here, your type checker and test suite in your day job.
Mathematicians got lucky: Lean existed, was mature, and a fluent community was standing by to formalize a degree-7 polynomial identity same-day. Most engineering orgs do not have that. Most of you are reviewing AI-generated diffs with your eyeballs and a CI suite that covers maybe 60% of the paths that matter, on codebases with no equivalent of a proof assistant anywhere near the critical logic.
The conjecture is still open in two dimensions, by the way — the original Keller problem for planar maps survives. Read that as a reminder that these systems close gaps unevenly and unpredictably. Fable found the ℂ³ case at degree 7 when humans were aiming at degree 200. Nobody can tell you in advance which problems fall in one afternoon and which stay open for another 87 years.
What to actually do with this
Stop treating "the model produced an answer that checks out" as the finish line. It's the start of the part that used to be the whole job.
If your team is shipping AI-generated code without formal verification, property-based testing, or exhaustive typed contracts at the boundaries that matter, you are one degree-7 surprise away from something that passes every review and is still wrong in a way nobody on the team could have derived by hand. The mathematicians had Lean ready. Do you have your equivalent ready, or are you still relying on "looks right to me"?
Generation is not the scarce resource anymore. Verification is. Go build the verifier before you need it, not after.
Sources: Terence Tao's original post · Hacker News discussion · BigGo Finance coverage · Fortune on mathematician reactions
Top comments (0)