Executive Summary

On Sunday, July 19, 2026, the Harvard mathematician Levent Alpöge posted a short message on X: “hello there the jacobian conjecture is false thanx.” Between the greeting and the misspelled thanks sat a single three-variable polynomial map. That was the whole announcement. The Jacobian conjecture, which mathematicians had believed true for 87 years, became false with that one post.

You can state what the conjecture claimed without any mathematics. John D. Cook's headline about the episode is exactly the statement. Locally invertible everywhere does not imply globally invertible. Take a map defined by polynomials, and suppose that if you zoom in far enough anywhere, it can be undone at every point. That is what the condition “the Jacobian determinant is a nonzero constant” means. The conjecture said this local property lifts to a global one, so the map as a whole is one-to-one. Can a map that never folds up close still overlap when you step back? For 87 years nobody found an overlap.

This counterexample shows the overlap with three points. There is a degree-7 polynomial map F from complex 3-space to itself whose Jacobian determinant is the constant −2, so the hypothesis is met exactly. Yet three distinct points, (0, 0, −1/4), (1, −3/2, 13/2) and (−1, 3/2, 13/2), all land on the same point (−1/4, 0, 0). It is not one-to-one. Terence Tao reconstructed the map on his own blog and stated the conclusion: there exists a map F : ℂ³ → ℂ³ that has a nonzero constant Jacobian and is nevertheless not invertible.

One counterexample settles a conjecture as false. But it is worth being precise about what became false. This counterexample was built in three dimensions and extends automatically to every dimension above three by the same construction. The two-dimensional case is still open. Tao was explicit: in dimension two the conjecture remains unsolved, and in dimension one it is easy to prove. In the plane, computations have ruled out counterexamples up to degree 100. So the headline “the Jacobian conjecture has fallen” is only half right.

The history of the problem explains why 87 years is a heavy number. Ludwig Kraus treated a two-dimensional special case in 1884, and Ott-Heinrich Keller generalized it into its current form in 1939. In 1998 Stephen Smale placed it at number 16 on his list of mathematical problems for the next century. In between, mathematicians including Segre and Gröbner announced proofs and then withdrew them over subtle errors, and at least five such papers collapsed that way. Yitang Zhang, who later became famous for his work on bounded gaps between primes, took this conjecture as his doctoral topic and never published a result from it, which says something about the problem's reputation. There have also been reports that the counterexample disproves the Dixmier conjecture as well, but that comes through secondary coverage and does not appear in Tao's own write-up.

The most repeated fact about this episode is the speed. Mathematicians independently checked the Sunday afternoon post the same day, and Kevin Buzzard in London told Fortune that when he woke up the next morning, a Lean verification was already done. A problem that had held for 87 years was settled in a day. The reading that followed was that in the age of AI, verification gets this fast too. That reading has the causation backwards.

The speed came from the shape of the counterexample. Checking it means substituting three points into a polynomial to see whether they give the same value, and expanding the Jacobian determinant to see whether it really is the constant −2. That is all. It is finite, it is exact, and anyone who can drive a computer algebra system can reproduce it. The cost of verification was close to zero. Counterexamples are like that by nature: proving something true requires covering every case, while showing it false requires producing one object. What the AI produced here was the easiest kind of mathematical object to check.

So the episode should not be read as evidence that our verification machinery is ready. It is more accurate to read it as evidence of good luck. How long did other work take in the same period, with the same tools?

What separates these cases is the asymmetry of verification cost. AI has driven the cost of producing results sharply down, but the cost of checking them is set by what kind of object the result is, and we do not get to choose that kind. When a result arrives whose verification is free, like a counterexample, consensus forms in a day. When a long argument arrives, humans read for months. The Jacobian episode simply sat at the easy extreme. It is also worth adding that this result has not yet been published as a peer-reviewed paper. Comments on Tao's blog report that an open-problems tracker still lists the entry as awaiting review. Independent confirmation and completed peer review are different stages.

Two months earlier there was a similar scene. When a model disproved Erdős's unit distance conjecture in May, the nine mathematicians who checked it were reading a human-edited write-up, not the model's raw reasoning. Pebblous covered that case in a separate article, and June's Leiden Declaration, which demanded consent and attribution at the training stage, was the subject of another one. Three days ago we published a diagnosis of why LLMs cannot make the abductive leap from observation to new theory. If that piece asks an epistemological question about what discovery is, this one asks an infrastructure question about what makes an already-produced result believable.

What was released in the Jacobian case was the counterexample itself: the coefficients of the polynomial map and the three colliding points. Everything needed to verify it was there. What was not released was everything about where those coefficients came from. Which prompt was used, how many attempts it took, where the human redirected the model when it went down a blind alley, which version of the model it was. The Conversation, whose pieces are written by academics, described the situation plainly: as of writing, the details of exactly how Alpöge prompted the model and what the model's output looked like have not been made public.

The gap was just as wide on the vendor's side. No official announcement, technical blog post, or model card mention of this result has been found. The announcement itself was a personal social media post that never went through a company release, and it was read more than twenty million times. Alpöge did not respond to Fortune's requests for comment. Even the question of how to write the credit line was unsettled. A comment on Tao's blog corrected the framing: the accurate attribution is not “the model solved it” but “Levent Alpöge, working with the model.” The absence of any attribution norm showed up in the comment thread on day one.

Stop there and the conclusion looks easy: the vendor should disclose more. Two weeks later, that exact experiment ran. On August 3, OpenAI announced that an unreleased model called Astra had solved ten open problems, and this time it pushed Lean-written formal proofs to a repository and published a narrative of the model's reasoning along with human-edited manuscripts. It was incomparably more material than the Jacobian case. And here is how Henry Yuen, who had posed one of those problems, responded: it gave him no understanding at all, and would just be something that takes time. His complaint was that the manuscript buried the technically interesting parts and never explained why that approach was chosen.

The ten problems spanned unrelated fields, from sphere packing in high dimensions and Kohn's rigidity conjecture to the Ehrhard volume conjecture, multicolor Ramsey numbers, and quantum parallel repetition. The proofs went up as Lean code in a public repository, and a researcher at the company said the tokens spent finding the solutions came to roughly $2,000 at their own rates. Results, formal proofs, and even cost were all on the table. And the person who posed the problem still does not know why his problem was solved the way it was.

Across the two episodes, what closed and what stayed open divide like this.

Others pointed out that there was no control condition. Gary Marcus said that half of Astra's problems are solvable with Fable too and that OpenAI had not even set up a comparison. And in fact Alpöge, the same mathematician who found the Jacobian counterexample, independently solved five of the ten problems with a different model within 24 hours, using ordinary prompts and no internet access. Which means the announcement contained no basis for judging what was uniquely this model's capability. Jared Duker Lichtman's pushback against framing it as the most important day in the history of mathematics comes from the same place.

Right after the counterexample appeared, John D. Cook asked a model directly whether mathematicians had believed the conjecture was true before the counterexample. The answer came back: the premise of the question is inaccurate, no counterexample to the Jacobian conjecture has been found, and it remains an open problem in mathematics. That is the ordinary consequence of a training cutoff, not a lie. Cook himself framed the tool as closer to chalk or a whiteboard. But as a symbol it is exact. Even the party involved in producing the result holds no record of the event.

This is not a story about anyone hiding anything. Neither Alpöge nor any company broke a rule. There is no rule yet that says keep a record. The Astra case is the proof of that. If the same gap remains even where a party disclosed diligently, then the problem is not the attitude of an individual or a firm but the absence of an agreement about what has to be preserved.

The press consumed this moment as a replacement story: is AI pushing mathematicians out, is the profession finished. The physicist Alexander Wissner-Gross writing “mathematics is cooked” in his newsletter got widely quoted inside that frame. He wrote it in the December 31, 2025 issue on the strength of one model's score on the hardest tier of a mathematics benchmark. The number was 29.2% on the top tier of FrontierMath, and he returned to the same diagnosis in his Davos issue in January 2026. It is a form of argument that reads the end of a discipline off a single benchmark score. But that is not where mathematicians actually disagreed with each other.

The most-cited change of mind is Daniel Litt's concession of a bet. Litt, an assistant professor at the University of Toronto, took 3-to-1 odds against the AI researcher Tamay Besiroglu in March 2025 on whether AI would autonomously produce a top-journal-caliber number theory paper by 2030. In August 2026 he declared himself the loser. Strictly speaking the bet had not resolved, he wrote, but he was clearly wrong about what capabilities producing such a paper would require, and it was now a matter of time. The trigger was not the Jacobian counterexample. It was the Astra announcement in early August, and even that, he said, was not the only reason: working with several models himself had given him a feel for their capability. He also judged that he should have picked a better proxy. The one-paper metric had failed to measure what he actually cared about.

He said he had no intention of calling the bet resolved early, and he does not yet count the current results as genuine number theory papers. His condition is that two or three more papers of comparable quality would have to appear before he treats it as a complete instance. So the reversal is not a declaration that AI has already done it, but closer to an admission that the list of capabilities he thought were required was wrong.

What he actually cared about becomes visible when you lay his words next to other mathematicians'.

Mathew and Yuen were reacting to different events, and they are asking for the same thing. Confirming that a result is correct is not enough; the result has to arrive with an account of the road it traveled. The optimists do not object to this request. What delighted Buzzard was that machine verification finished in a day, not that the process could stay unknown. Harris's criticism lands in the same place: the problem is treating the reasoning process as a byproduct.

So the axis the field split on was not whether AI replaces mathematicians. It was whether output comes with its process attached. That is also what Litt meant by picking the wrong proxy. Whether or not a paper appears is easy to count, and it fails to measure what he was worried about: a field flooded with plausible, unverified results. And this demand is not satisfied by good intentions. It requires infrastructure.

Pointing at a gap is easy; looking at what is already being built takes a little more work. Over the past two years mathematics has been erecting two kinds of infrastructure at once. One is formal verification, which lets a machine confirm that a result is true. The other is the practice of recording how that result came about. The two get discussed as a single thing, and they do different jobs.

5.1What formal verification closes

Formalization is a daunting job before anything else. Mathlib, the standard formalized mathematics library, is on the order of a million lines of code built over eight years by more than 600 contributors. Translating a single theorem into machine-readable language is closer to laying a brick on top of that structure, which is why formalizing one major theorem has taken anywhere from months to years.

Formal verification, of which Lean 4 is the flagship, converts every step of a proof into a language a machine can check. The results are piling up fast. Harmonic's Aristotle passed five of the six 2025 International Mathematical Olympiad problems by automated formal verification with no human checking, matching the gold medal threshold. Math Inc.'s Gauss finished formalizing the strong prime number theorem in three weeks, on a project that had gone more than 18 months in human hands without completion. Axiom Math said proofs produced by its system had been accepted at five journals, though the specifics went unpublished: which journals, which theorems, and whether AI disclosure or authorship attribution was required.

5.2What formal verification cannot close

Machine verification has a quiet blind spot. The type checker only asks whether a proof is logically coherent. It does not ask whether the statement that proof is attached to actually captures the mathematics you meant to ask about. The Lean Atlas paper gave this phenomenon a name: semantic hallucination. A formalization type-checks, the proof completes, and its meaning still does not match the original natural language statement. The paper catalogs five patterns: mismatched definitions, hypotheses dropped or added, the goal itself substituted, quantifiers and scope misaligned, and meaning shifted by a type's default values. In practice, work translating Erdős problems into Lean has turned up a number of mis-formalized cases.

5.3A new column appeared in the comparison table

What happened on the provenance side was far quieter, and to this report it matters more. In March 2026 a mathematician published a paper formalizing an equilibrium theorem from plasma physics in Lean. He included a table comparing his work against existing formalization projects, and one of that table's columns was “logs released?” Alongside prover type, team size, and the role AI played, whether prompts and commit histories are public became a formal criterion for comparing projects.

Of those nine entries, exactly one released its logs in full: the paper that built the table. Zero lines of human-written code, 229 human prompts and 213 git commits archived in the repository, $200 in total cost, ten days elapsed, and roughly 50 hours of human supervision. That is enough for someone else to retrace the whole job from the beginning. It is the first physical specimen of what a provenance ledger actually looks like.

A similar demand surfaced on the benchmark side. First Proof, run in June 2026, gives AI systems research-level open problems and has roughly thirty mathematicians grade the submissions double-blind. Its entry conditions include a clause that outputs, logs, and code must all be releasable. Systems have to record input tokens, output tokens, and reasoning tokens. Seven of the ten problems earned a passing grade, two required substantial revision, and one failed outright. Four systems submitted answers within 24 hours in one-shot mode, and grading those answers took five days in early June. Even in a competition that wrote log disclosure into its rules, deciding whether the results are correct still costs thirty mathematicians' time. IMProofBench keeps its dataset private to avoid contamination while publishing the models, API settings, and evaluation prompts.

Mathematics started writing a provenance ledger not because anyone ordered it to, but out of its own need. That a column appeared in the comparison table is itself evidence that a practice is forming, and that eight of that column's nine boxes are empty is where we currently stand. Journal policy has not caught up either. The requirement to name the model and version and describe the verification method is tightening, but as of mid-2026 no major mathematics journal has been found to mandate full disclosure of prompt logs. Elsevier requires that records of tools and models be preserved, but stops short of requiring publication.

Mathematics has the most rigorous verification culture on earth. It has spent centuries building procedures for confirming that a result is true, and it is a community that knows to be embarrassed when a published proof later collapses. Even there, output has outrun record-keeping infrastructure. Which means that in fields with much looser verification cultures, the same condition set in long ago.

Numbers from academic publishing at large show the size of the gap. A study covering 5,114 journals and 5.2 million papers found that 70% of journals have adopted a policy on AI use, and most of those require disclosure. Yet among 75,000 papers published since 2023, only 76 explicitly disclosed AI use, about 0.1%. That study looked at AI-assisted writing rather than proof generation, so it does not sit at the same level as the Jacobian episode. But as a gauge of the distance between how fast norms are declared and how fast they are actually observed, it is more than sufficient. That is the distance between having a policy and leaving a record.

Translate this structure into the language of an ordinary data and AI pipeline and it becomes a familiar problem. Any organization that puts model-generated output into a product or a report soon gets the same question: how did this come about? To be able to answer, at minimum these five things have to be preserved alongside each output.

• • Source of the input data — what went in, and where the right to use it came from
• • Model and version — which model, at which point in time. A model with the same name is a different object a few months later
• • Generation conditions — prompts, temperature, tool access, and anything else that changes the result
• • Attempt history — how many tries it took, what was discarded, and where a human stepped in
• • Verification path — what you checked it with, and what that check does not guarantee

If that list sounds abstract, look again at the single case from the previous section. 229 prompts, 213 commits, $200 in cost, ten days, zero lines of human-written code. That is what all five items filled in actually looks like. It did not take an elaborate system either. It was one person's records in one repository.

This is why Pebblous is paying attention to the episode. What we have meant all along by AI-Ready Data is not clean data but data that carries its origin and history with it. The Jacobian case repeats that argument on the output side. A result can be correct and still fail to accumulate as an asset if nobody can reconstruct how it was produced. If what the Leiden Declaration demanded was consent and attribution at the training stage, what surfaced this time is a recording gap at the inference stage. Trust holds only when the provenance of the input and the provenance of the output are both present.

Records cannot be manufactured after the fact. Reconstructing them retroactively once an audit or a dispute has started means filling in vanished prompts, discarded intermediate outputs, and half-remembered intervention points with human testimony. Mathematics could believe the counterexample in a day because that output happened to carry its own verification inside it. Most results do not. It is safer to design as though the unlucky case is the default.

References

Primary sources and academic papers

• 1.Tao, T. (2026). A digestion of the Jacobian conjecture counterexample. terrytao.wordpress.com
• 2.Alpöge, L. (2026-07-19/20). Post announcing the Jacobian conjecture counterexample. X.
• 3.Litt, D. (2026-08). Post conceding the bet. X. x.com/littmath
• 4.Yanahama, K. & Sannai, A. (2026). Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization. arXiv:2604.16347. arxiv.org
• 5.Ilin, V. (2026). Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium. arXiv:2603.15929. arxiv.org
• 6.First Proof (2026). arXiv:2606.18119. arxiv.org
• 7.IMProofBench (2025/2026). arXiv:2509.26076. arxiv.org
• 8.Harmonic Team (2026). Aristotle / formal verification at IMO 2025. arXiv:2510.01346. arxiv.org
• 9.He, Z. & Bu, Y. (2025/2026). Academic journals’ AI policies fail to curb the surge in AI-assisted academic writing. arXiv:2512.06705. arxiv.org
• 10.Smale, S. (1998). Mathematical Problems for the Next Century (Problem 16).
• 11.Keller, O.-H. (1939). Generalized statement of the Jacobian conjecture. Original not consulted; cross-checked against secondary sources.

Commentary and press

• 12.The Conversation (2026). ‘hello there the jacobian conjecture is false thanx’: why a tiny social media post has mathematicians rethinking AI. theconversation.com
• 13.Cook, J. D. (2026-07-21). Locally everywhere does not imply everywhere. johndcook.com
• 14.Fortune (2026-07-21). Mathematicians grapple with a ‘very rapid and very unsettling change’. fortune.com
• 15.Wissner-Gross, A. (2025-12-31, 2026-01-16). The Innermost Loop. theinnermostloop.substack.com
• 16.Mowshowitz, Z. (2026-08). OpenAI’s Unreleased Model Astra Solves Ten Major Open Mathematics Problems. thezvi.substack.com

Related Pebblous articles

• 17.Pebblous (2026-06-19). AI's disproof of an Erdős conjecture. blog.pebblous.ai · (2026-06-30) The Leiden Declaration. blog.pebblous.ai · (2026-08-06) It reasons, but it does not discover. blog.pebblous.ai