OpenAI's October 2026 release of 722 AI-generated preprints, as reported by Science: a ledger of what is claimed, what is checked, and what is not.
On 6 October 2026, according to Science (Tom Howarth, 13 October 2026), OpenAI posted 722 preprints covering 372 distinct results on a website. This chapter is a ledger of that release. Its only source is that one article, whose text the project's owner supplied after the journal's site refused our fetch. OpenAI's own page was not retrieved. So nothing below is a finding of this book. It is a record of what one reporter says was claimed, said by whom, and what state each claim is in.
The chapter uses a three-way distinction that Science attributes to Olga Holtz of UC Berkeley: a claimed result, an independently verified result, and a result understood and absorbed into mathematical culture. These are different states and the ledger keeps them apart.
| Claim or event | Whose | State |
|---|---|---|
| 722 preprints, 372 distinct results, from about 4000 problems attempted | OpenAI, via Science | Claimed. Count not independently audited here. |
| Most results took about 3 hours of ChatGPT Pro "thinking" on average, using an unreleased model | OpenAI, via Science | Claimed. The model is not available to outsiders. |
| Navier–Stokes result, September: 10,000 agents for 88 hours | OpenAI, via Science | Claimed. A later preprint reports the Lean file does not match the paper's proof. |
| 3 manuscripts withdrawn, 14 revised | OpenAI, via Science | Reported at press time. |
| 300 of the remaining 719 formalized in Lean | OpenAI, via Science | Claimed. Faithfulness of each formal statement is open. |
| Some formalizations state "something weaker" than the main theorem | Steven Sivek, via Science | An expert's report on some papers. Which ones, Science does not say. |
| Proof of the exact overlaps conjecture inside the release | OpenAI; Constantin Kogler's own proof posted 4 hours later | Two claims to the same result. Kogler calls his paper much better than OpenAI's. |
| A cluster of papers claiming to resolve a 1975 conjecture of Polyakov | OpenAI; Edward Witten is examining them | Under examination. Witten has not, in this article, said whether they are right. |
| Independent verification of the whole release | — | None reported. Mathematicians are forming groups to work through the claims. |
Science states the point plainly: Lean can confirm that a proof establishes the statement given to it in code, but cannot confirm that this statement is the one the paper states in English. That is the gap between "compiles" and "proves what it says it proves", the gap this series has fallen into itself. A formalized paper is better than an unformalized one on the question "is each step valid", and no better on "is this the right theorem". The report of a mismatch in the Navier–Stokes formalization is the clearest example in the article, and the researchers quoted do not conclude from it that the result is wrong, only that computer verification carries less weight than is often assumed.
Presentation is the loudest complaint. Witten is quoted as confident that a human who understood the results could write them more clearly. Sivek describes the paper closest to his own work as 140 pages and unreadable, and says it did not improve on a second look. Whether a result can be understood is a separate question from whether it is correct, and a proof nobody can read is hard to check, formal or not.
Access is the second. An advisory group that has counseled OpenAI asked it to stop testing open problems on unreleased models that mathematicians cannot use. Science says OpenAI has so far declined, while agreeing in spirit with other recommendations: depositing results in independent repositories and disclosing the prompts behind each result. A result that others cannot reproduce on the same tool is, in practice, a result they can check only by reading.
The third is the human side. Science reports a researcher whose own result was announced the same evening, others who fear sharing work in progress, and a department chair who sees an opening to rethink what the discipline is for. This book takes no side in that argument. It records the three claims and checks the arithmetic.
It does not know whether any of the 372 results is correct. It does not know how many of the 300 formalizations are faithful. It has not read any of the papers. It has not seen OpenAI's own account, only Science's. A related Science article on the Riemann hypothesis, listed alongside this one, was not opened. Other outlets have written about OpenAI's math claims in 2026, some about earlier announcements; this chapter has not opened them and does not rely on them.
The companion verifier, ch-claims-awaiting-verification-verify.py, checks that the reported counts and dates are consistent with each other (722 minus 3 is 719; 300 of 719 is 41.7 percent; 6 to 13 October is 7 days), with controls that fail on perturbed values. It deliberately refuses to compute a ratio between the 88-hour agent run and the 3-hour typical result, because the units are not comparable.
The 26 October releases (Kakeya, Yang–Mills existence, and the Exponential Time Hypothesis, with a competing claim from Anthropic) are recorded in Dueling Proofs.
When a claim in the ledger changes state (a paper is checked, a formalization is shown unfaithful, a result is withdrawn), change its row and the date, and cite the new source. Do not add rows from sources that were not opened.