The Easy Part Was Checking It: AI and the Jacobian Counterexample

A reported AI-assisted counterexample to the Jacobian conjecture is simple to verify once you see it. The harder story is how anyone found it in the first place.

Audio overview

Listen to the audio overview

A narrated audio overview of this article.

15 15

0:00 / 0:00

Speed 1× 1.25× 1.5× 2×

View full size

Open asset Close

A nonzero Jacobian determinant prevents local singularities. It does not, by itself, guarantee that distant points have different outputs.

What happened

On July 20, 2026, mathematician Levent Alpöge publicly announced an explicit polynomial map in three complex variables. Fable was publicly credited with work leading to the example.¹² The striking claim was not a long proof. It was a compact object that could be tested directly.

The map has a constant, nonzero Jacobian determinant, yet it sends three different inputs to exactly the same output. That combination makes it a counterexample to the classical Jacobian conjecture in dimension three. Keeping any extra coordinates unchanged extends the failure to every dimension above three.²³

The algebraic certificate is now public and reproducible. The discovery record is not. As of July 22, 2026, the checked public sources did not include a complete Fable prompt, transcript, tool trace, candidate history, or official Anthropic case study of this run.⁴ That gap is not a reason to doubt the displayed calculation. It is a reason to separate two questions that arrived bundled together: does the map work, and how was it found?

What the Jacobian conjecture claimed

A polynomial map takes coordinates in and returns polynomial expressions out. In one variable, that might look like $x \mapsto x^3+x$ . In several variables, each output coordinate can depend on every input coordinate.

The Jacobian matrix collects all the first derivatives of those output coordinates. Its determinant tells us whether the map behaves like an invertible change of coordinates near a point. If the determinant is nonzero, the map does not crush a tiny neighborhood flat. When the determinant is nonzero at a point, the inverse function theorem gives a local inverse near that point.

The Jacobian conjecture asked whether a much stronger conclusion follows for polynomial maps over characteristic-zero fields: if that determinant is the same nonzero constant everywhere, must the entire map have a polynomial inverse?⁵

The trap is the jump from local to global. A road map can be perfectly readable in every neighborhood while two distant roads still arrive at the same address. Local invertibility says the map behaves well under a microscope. Global injectivity says no two points anywhere share an output. Those are different promises.

The explicit counterexample

The announced map is $F=(P,Q,R):\mathbb{C}^3\to\mathbb{C}^3$ , with

Its first certificate is short:

The determinant is constant and never zero. The second certificate is even more decisive:

Those are three distinct input points with one exact output. A function with that collision cannot have a global inverse, polynomial or otherwise. The public verification note verifies both identities, and MathWorld and Zihan Zhang’s technical note reproduce the same map and consequence.²³⁵

View full size

Open asset Close

The counterexample needs only two finite checks: the determinant is the same nonzero constant everywhere, and three distinct inputs share one output.

For this article, a separate exact-arithmetic check reran the finite certificate in SymPy 1.14.0. The determinant simplified to -2, and all three substitutions returned (-1/4, 0, 0). This check establishes the displayed algebra. It does not establish who deserves discovery credit, whether the construction is new up to equivalence, or what happened inside an AI session.

Why the easy part was checking it

Once the map is written down, verification is a bounded task. Differentiate three polynomials, take a determinant, simplify, and substitute three rational points. A computer algebra system can do that without interpretation. A patient reader could also check it by hand.

Finding the map is a different kind of problem. The candidate has to satisfy competing constraints: a determinant that stays constant, enough global structure to create a collision, and formulas simple enough to express exactly. Aaron Lou’s public derivation reconstructs one route through cubic factorization, resultant normalization, and a polynomial affine chart.⁶ The note is explicit that it is a reproducible mathematical summary, not a transcript of private model reasoning.

This is why the object looks obvious only after it exists. Verification evaluates one explicit candidate. Discovery has to generate that candidate from a huge constrained space.

The reported human-AI workflow

The public record supports a careful sequence, not the slogan “AI solved an 87-year-old problem.” Alpöge announced the map. The verification note says the original post credited Akhil Mathew with asking the question and Fable with work leading to the example.¹² Anthropic markets Fable as a system for long-running agentic and complex knowledge work, but its product page does not document this Jacobian run.⁴

There is also a separate OpenAI-side claim. Aaron Lou publicly reported that an internal Codex run, without web search, found essentially the same counterexample.⁷ His derivation note makes the mathematical route inspectable, but the checked public record does not contain a replayable trace of that internal run. It should not be merged with the Fable attribution or used to prove that Fable worked autonomously.

What can we safely say? Fable was publicly credited, and Lou separately reported a Codex reproduction. Mathew was credited with asking the question. Subsequent public artifacts announced, checked, explained, and formalized the construction, but the original search’s division of labor remains unknown.

Discovery versus verification

Three verification layers followed quickly, and each answers a different question.

Symbolic verification checks identities. A CAS can confirm the determinant and evaluate the three points. Zihan Zhang published a public SymPy checker, and the local Brain Bytes reproduction reached the same exact result.³⁸

Formal verification checks whether a precise theorem follows inside a proof assistant’s trusted kernel. A public external Lean 4 repository reports formalizations of the determinant identity, collision, and noninjectivity.⁹ Brain Bytes has not independently rebuilt that repository, it is not an Anthropic artifact, and the checked record does not establish a mathlib merge. Lean verified an encoded construction. It did not discover the construction.

Conceptual explanation tells us why the object has this shape and what it means. The longer mathematical notes explain the structure of the sets that map to one output and why the map can behave regularly nearby while failing globally.²⁶ That layer turns a certificate into mathematics a person can reason about.

Together, the layers suggest a governed workflow. The public evidence is strongest from the candidate onward and weakest inside the search box.

View full size

Open asset Close

A useful working model for this episode. It separates the reported search contribution from the public verification artifacts that followed.

What remains unresolved

First, the plane case remains open.⁵ The three-dimensional counterexample extends upward by adjoining identity coordinates:

That preserves the determinant and the collision for every $n\ge 3$ . It does not run backward and produce a two-dimensional example.

Second, provenance remains incomplete. The checked sources do not settle autonomy, original tool use, human steering, or how many candidates were considered.

Third, the checked sources do not yet settle whether an equivalent construction appeared earlier in another normal form. A MathOverflow discussion asked whether the cubic structure or an equivalent normal form was already known.¹⁰ That forum question is evidence of an open priority issue, not proof of either novelty or prior discovery.

Finally, a July 22 arXiv search did not surface a paper devoted to the announced counterexample.¹¹ That is a time-bounded search result, not evidence that no submission exists. Archival and peer-review status must be checked again before publication.

Broader implications

The most interesting AI lesson is not that proof writing suddenly became easy. It is that counterexample search may be unusually compatible with machine assistance.

A universal statement can be destroyed by one exceptional object. If candidates can be generated inside a structured algebraic space and rejected cheaply, then scale matters. Most candidates may fail. One surviving candidate can change the theorem. This is closer to guided search with a strong verifier than to composing a long, conceptually unified proof from scratch.

That interpretation is still an inference. Lou’s reconstruction suggests a structured search space, but it does not reveal the original Fable process.⁶ What the episode establishes more clearly is an emerging trust stack. Candidate generation can be fast and messy. Symbolic algebra filters exact identities. Formal systems lock down carefully stated claims. Human mathematicians determine meaning, provenance, and importance.

That last step cannot be treated as cleanup. Credit becomes harder when a question, an agent run, a selected candidate, a CAS check, a formal proof, and a conceptual explanation come from different contributors. If this kind of search is to become repeatable and trustworthy, its prompts, tools, candidate histories, selection decisions, and artifact hashes need an auditable provenance record.

Final takeaway

The announced map gives a compact, reproducible counterexample in dimension three and therefore in every dimension above it. Dimension two remains open. The calculation is no longer the mystery. The mystery is the search process that made this particular object appear, and whether AI can make that kind of search repeatable without making its provenance disappear.

Footnotes

1. Levent Alpöge, original announcement, July 20, 2026 UTC. ↩ ↩²

2. A Counterexample to the Jacobian Conjecture, July 20, 2026. ↩ ↩² ↩³ ↩⁴ ↩⁵

3. Zihan Zhang, “Direct Consequences of the Three-Dimensional Counterexample to the Jacobian Conjecture”, July 20, 2026. ↩ ↩² ↩³

4. Anthropic, “Claude Fable”, checked July 22, 2026. ↩ ↩²

5. Eric W. Weisstein, “Jacobian Conjecture”, MathWorld, checked July 22, 2026. ↩ ↩² ↩³

6. Aaron Lou, Deriving an Explicit Polynomial Counterexample to the Jacobian Conjecture, July 20, 2026. ↩ ↩² ↩³

7. Aaron Lou, public statement about an internal Codex reproduction, July 20, 2026. ↩

8. Zihan Zhang, public SymPy checker for the three-dimensional counterexample, July 20, 2026. ↩

9. headllesslulu, “Constant-Jacobian-Noninjective-Polynomial-Map-in-Lean”, GitHub, checked July 22, 2026. ↩

10. “Galois structure of the new counterexample to the Jacobian conjecture”, MathOverflow, July 20, 2026. ↩

11. arXiv, current search for “Jacobian Conjecture,” sorted by submission date, checked July 22, 2026. ↩