The editorial argues that counterexample construction is categorically different from the proof-adjacent output LLMs have been producing. It sits in the 'search' regime — hunting for rare objects in enormous polynomial spaces guided by intuition — which is precisely where language models have historically been weakest, making this a meaningful qualitative shift.
The editorial explicitly cautions readers that verification is still in progress, noting the long history of Jacobian Conjecture 'proofs' that were withdrawn — including a 1994 attempt that embarrassed peer reviewers. A counterexample is checkable in Mathematica, but until that check is public, the claim is unconfirmed.
Alpoge is careful to describe the output as an explicit polynomial map he believes violates the conjecture's conclusion, not as a proof that Claude Fable discovered anything. This distinction — concrete candidate object versus argumentative sketch — is what makes the claim verifiable rather than a rehash of prior AI-math hype.
The submitter's chosen headline preserves Alpoge's precise phrasing ('produced a counterexample') rather than sensationalizing it to 'AI solved the Jacobian Conjecture,' which helped the thread reach 434 points with a fact-first framing that the HN audience rewarded.
On July 19, mathematician Levent Alpoge (@__alpoge__) posted that an AI system he's been working with — referred to as Claude Fable — produced a candidate counterexample to the Jacobian Conjecture. The thread hit HackerNews at 434 points within hours, which is roughly what you'd expect when a 87-year-old open problem in algebraic geometry shows up next to a Rust release note.
The Jacobian Conjecture, first posed by Ott-Heinrich Keller in 1939, is deceptively simple to state. Take a polynomial map F: C^n → C^n. Compute its Jacobian determinant. If that determinant is a nonzero constant, the conjecture says F must have a polynomial inverse. Smale put it on his list of problems for the 21st century. Dozens of "proofs" have been announced and quietly withdrawn over the decades — most famously a 1994 attempt that survived peer review long enough to embarrass several journals.
The claim from Alpoge is not that Claude Fable *proved* anything — it's that the system produced an explicit polynomial map that Alpoge believes violates the conjecture's conclusion. That's a categorically different kind of output than a proof sketch. A counterexample is a concrete object. You can hand it to Mathematica and check.
As of this writing, community verification is in progress. Treat the specific claim as pending.
The temptation is to file this under "AI does math" and move on. That framing misses what's actually interesting.
Language models have been producing proof-adjacent output for a couple years now — IMO problems, Lean tactics, informal sketches that mostly hold up. What they've been noticeably bad at is search — the part of research math where you're not proving a known target but hunting for structure in a space nobody has mapped. Counterexample construction sits squarely in that regime. You're looking for a rare object in an enormous polynomial space, guided mostly by intuition about which symmetries and degree combinations are worth trying.
If Claude Fable's output verifies, the meaningful takeaway is that a language model plus a symbolic backend can now do exploratory algebraic search well enough to produce novel objects, not just reconstruct known ones. That's a threshold the field has been circling for a while.
There's a second, quieter implication. Counterexamples to famous conjectures are historically produced by mathematicians who spent years building intuition for the specific problem — Milnor on the Poincaré-in-dimension-7 story, Enflo on the approximation problem, and so on. If AI can shortcut the "build a decade of intuition" step and jump straight to plausible candidates, the bottleneck moves. It's no longer *finding* candidates; it's *filtering* them. Alpoge's role in the thread is telling — he's not the discoverer so much as the domain expert who can tell the system its first three attempts were nonsense and its fourth might not be.
The community reaction has been split in a way that's worth paying attention to. The camp saying "cool, let's verify" is doing the right thing. The camp already writing think-pieces about the end of mathematics is embarrassing themselves — this has happened before with far weaker results. And the camp dismissing it as "just symbolic manipulation" is missing that symbolic manipulation, done well, is what a large chunk of research mathematics actually is.
For most working developers, none of this changes what you'll do on Monday. But there are a few threads worth pulling.
Formal verification tooling is about to get a lot more attention. If AI-generated counterexamples become common, the bottleneck in mathematics shifts from "can a human construct this" to "can we mechanically check it," and that's a tooling problem devs can actually work on. Lean, Coq, and the symbolic computer algebra ecosystem (SageMath, Macaulay2, Singular) are the layer where this verification happens. If you've been on the fence about learning Lean, the fence is getting shorter.
Symbolic + LLM hybrids are the interesting architecture right now. The naive read on this result is "the LLM did it." The accurate read is "an LLM proposed candidates, a symbolic engine filtered them, a human directed the search." That three-part loop — generation, verification, direction — is the pattern showing up in every interesting AI-for-science result of the last twelve months. If you're building agentic systems, this is the shape to steal.
Be skeptical of the announcement cycle. The Jacobian Conjecture has a long history of premature announcements. In 2005, Carolyn Dean's proof attempt made rounds before a gap was found. Wang Yucai's 1980 attempt was similar. The mechanical checkability of a counterexample makes this claim different in kind — it's either right or it isn't, and you can find out in an afternoon — but the meta-lesson holds: on high-profile open problems, wait for verification before rewriting your worldview.
The next 72 hours will tell you what actually happened. If the polynomial map verifies, expect a wave of follow-on attempts — not just on the Jacobian Conjecture's remaining cases, but on the dozens of open problems in algebraic geometry, combinatorics, and number theory that share the same shape: construct an object with property X. Erdős-style problems, Kakeya-adjacent constructions, extremal graph theory. Any conjecture where the negation is a witness you can hand to a computer becomes newly interesting.
If it doesn't verify, this joins a long list of instructive near-misses, and the more honest headline becomes "AI systems are now producing output that looks like it might be a counterexample to famous conjectures, and that alone is enough to move the field." Either outcome tells you something real about where math research is going; only one of them tells you the Jacobian Conjecture is false. Worth watching either way.
> The incredible Yitan Zhang (https://newyorker.com/magazine/2015/02/02/pursuit-beauty) worked on proving this conjecture for 7 years. Moh, his advisor, wrote that Zhang "failed miserably" in proving the Jacobian conjecture, "never published any p
This is a rare instance where feeding this groundbreaking information into an LLM gives _them_ psychosis. I fed this to claude code and watched it verify the result in 7 different ways to be 100% certain, and it was just flabbergasted. Quite remarkable.
The great thing about these mathematical mopping up type operations is that no person will waste their time trying to prove it to be true anymore. If anything that’s a win.It would be great if an LLM could settle the Collatz conjecture next, god knows how many man-years have been burned on that by u
I’ve been math-vibe coding a few months now.It’s surprisingly easy to do with AI. The hard part has been manually verifying and validating the results. I took one of the smaller findings (disproving a conjecture) and wrote a paper as my first endeavor into publishing.Because the next few findings i
Top 10 dev stories every morning at 8am UTC. AI-curated. Retro terminal HTML email.
A little over 10 years ago I remember meeting a postdoc who believed he had something close to a counterexample to the Jacobian Conjecture. He and another person was bruteforcing polynomials in about 16 variables, something like 80 - 700 terms each, using binary trees for mapping coefficients.They w