What 722 AI math papers actually prove

Everything below comes from the repository itself (its README, its change history, the withdrawal notices and its formal-proof catalogue, read at the version current on 19 October) plus Decrypt's 7 October report on the reaction. I am not a research mathematician and I did not check any proof. What I can check is what the release claims about its own verification, and that turns out to be the interesting part.

What was released

The README says the manuscripts were "produced by an internal OpenAI model" as part of evaluating models on open research problems. Over the evaluation the model was posed "approximately 4,000 problems," and each result used on average "three hours of ChatGPT Pro thinking compute." Aggregating the output and "requiring an appropriate level of significance" produced the catalogue: at first release, 722 manuscripts in 372 families, where a family groups a main result with companion arguments, consequences or alternative proofs.

Two exceptions are named. Work on a zero-free region for the Riemann zeta function and a proof of the Hodge conjecture for CM abelian varieties did not follow the fixed procedure, and the writeup for the zeta result "was human edited for readability."

The README also carries a warning that is easy to skim past: "Some of the unformalized results could have issues."

The sign error

The repository's history file, dated 7 October, reports that in "Algebraicity of Weil classes on split abelian eightfolds" a sign error "invalidates a stabilization-trace cancellation argument and the construction used by two dependent papers." All three were withdrawn: that paper, "Algebraicity of Kuga–Satake Correspondences for K3 Surfaces," and "The rational Hodge conjecture for products of K3 surfaces." (The notices on the papers themselves give the withdrawal date as 6 October.)

The withdrawal notice is unusually specific, and it is worth reading because it shows how small the error was. The proof needed a signed count of double points to come out to zero so that a cancellation theorem (credited to Eliashberg and Murphy) would apply. Starting from a count of minus m, the proof assigned each added correction a sign of plus one, so adding m of them gave zero. Accounting for orientation, each one should have counted minus one, so the total is minus 2m, not zero. The theorem's hypothesis is not met, and in the notice's words "the paper does not establish its claimed algebraicity theorem."

The notice adds a line that matters: "This withdrawal concerns the proof; it does not assert that the mathematical statement is false." The claims are now unproved, not disproved.

Anyone who has done quantitative lab work knows this failure mode. A flipped sign convention does not look wrong. Every step reads correctly in isolation, and the error only shows up when someone recomputes the one number the whole argument depends on.

None of the three had a machine-checked proof

Some of these results come with formal proofs in Lean, a proof assistant where a computer checks every logical step. The repository keeps a catalogue of them (lean/formalization.yaml), which describes itself as a "Catalog of papers with a formalized main result."

I searched both the original release's catalogue and the current one. Neither lists any of the three withdrawn papers. That is the most useful fact in the whole episode: the error surfaced in the part of the release that a computer had not checked, which is exactly where the README said issues could be.

22 percent or 42 percent?

Coverage has quoted two very different figures for how much is formalized, and both trace to the repository.

Decrypt reported that "Only 162 of the 722 papers have a Lean-formalized main result," about 22 percent. The original catalogue does list 162 papers. After the 7 October update, the current catalogue lists 173.

The README now says instead that the repository "has ~42% top-line results formalized," and the history file gives the arithmetic as "300 / 719 = ~42%." That numerator counts top-line results and the denominator counts manuscripts, so it is not the same measure as papers with a formalized main result. The repository files I read do not define a top-line result or explain how 300 of them map onto 173 papers. Both numbers can be accurate. They answer different questions, and anyone quoting either should say which.

What a formal check does and doesn't cover

Even the formalized share is narrower than "verified" sounds. As Decrypt put it, "A passing Lean check confirms only that the proof follows from the statement as written in Lean." Whether that statement matches the original problem, and whether the result is new or important, is still a human judgment. The repository's own instructions for its Comparator checks include a section of setups that "verify supporting results, not the corresponding papers' main theorems."

The 7 October update shows the boundary in practice. "Taming implies compatibility on four-manifolds" is in the formal catalogue, with a Comparator configuration for its main theorem. The same update lists, among 14 revised manuscripts, a fix that "corrected the cone-equality claim in Taming implies compatibility." The files do not say how that claim relates to the formalized theorem, and I have not compared the Lean file to the paper. But it is a clean reminder that a formal proof certifies one stated theorem, not every sentence in the PDF around it.

Who checks the rest

Through the GitHub API, the repository shows issues disabled, and its second pull request, merged 12 October, was titled "Automatically lock new PR conversations." Corrections arrive as OpenAI's own updates, which the README promises to record as new versions with earlier ones kept accessible. That is good version hygiene. It is not the same as an open channel for the people best placed to find the next sign error.

MIT mathematician Andrew Sutherland, quoted by Decrypt from an interview with Scientific American, said claims of one-shot solving by a single agent should be treated as unverified until the model is released and results can be replicated. His short version: "We should ask for receipts."

The signal

This is not a story about an AI being bad at math. A few hundred results with formal proofs attached is a real thing, and three withdrawals out of 722 in the first day is a small fraction. The story is about what "released" means. The repository already contains the honest description: some results machine-checked, many not, and a warning that the unchecked ones "could have issues." The first error landed precisely there.

So when you see "AI proved X" from this collection, ask one question first: is X in the formal catalogue? If yes, a computer has checked that the stated theorem follows. If no, it is a manuscript waiting for a referee, like any other. (Report 040 traced the same pattern in OpenAI's earlier math claims: what changed the outcome was who checked the work. Report 141 did the same for a Navier-Stokes headline.)