On Tuesday October 6, 2026 at approximately 12:00 UTC, OpenAI published a research post titled Sharing AI progress in mathematics and simultaneously pushed openai/math, a public GitHub repository containing 719 AI-generated mathematical manuscripts grouped into 372 problem families. The repo is MIT-adjacent and Apache 2.0 licensed. It has no author list. The README explains that most of the results came from a single "unreleased internal OpenAI model" at roughly three hours of ChatGPT Pro thinking per attempted problem, across approximately 4,000 problems in all (OpenAI, GitHub README).

The field has been counting ever since. The number that matters is not 719. It is ten and forty-two.

Ten is the count of manuscripts in the release that include the model's chain of thought — the actual reasoning the model produced on its way to a result — per TechCrunch's reading of the repository (TechCrunch). The other 709 ship only with a final write-up. 42 percent is the share of top-line results that have a corresponding Lean formalisation — a machine-checkable proof an independent verifier can run against the natural-language text — per the repository's own README. The remaining 58 percent are claims a human mathematician has to grade by hand, in prose produced by a model nobody outside OpenAI can call back for clarification.

That is the shape of the story. The mathematical substance of the proofs is being evaluated at the speed of mathematical evaluation, which is weeks and months. The publication model is being evaluated at the speed of a weekend group chat, which is where the fight is.

The guidelines OpenAI partly followed

Late in September 2026, the Advisory Group on Mathematics and Artificial Intelligence (AGMAI) — a nine-researcher body hosted at the Institute for Advanced Study — published guidelines on how frontier labs should release AI-generated mathematical work. The first recommendation was to stop testing advanced mathematical problems on proprietary models. OpenAI's release attempts exactly that, with an unreleased internal model nobody can audit. AGMAI also asked for machine-readable metadata linking each natural-language proof to its formal counterpart; the openai/math repository does not supply it (TechCrunch). AGMAI did not respond to TechCrunch's request for comment on the release.

OpenAI, to its partial credit, did not ignore AGMAI entirely. The release includes a Lean library and partial formalisations for 42 percent of the results, which exceeds a reasonable floor by exactly whatever amount you think zero exceeds. It also includes abbreviated reasoning traces for nine problem families, which rounds to the ten the trade press counted. The company's framing on the OpenAI post describes the release as a demonstration that saturated benchmarks have been replaced by open-problem evaluation, which is the kind of sentence that doubles as an engineering milestone and a procurement document.

A grad student's thesis, proven over the weekend

The most-cited consequence of the drop is not any particular theorem. It is a specific graduate student. Tristan Humbert, a PhD candidate whose central thesis problem is represented in the openai/math repository, surfaced in the compiled reactions. His problem was listed as proven (Proofs and Prompts).

He is not alone. Ben Green — a Fields-adjacent name in additive combinatorics — reported that roughly three-quarters of the research goals of a European grant he was awarded in June are now in the repository. Jake Boggan, who had worked on Barnette's Conjecture for approximately 24 years and had briefly thought the summer before that he had cracked it, saw problem 180 in the repository claim a solution; he wrote on Hacker News that the news made him "sad in a far-off way" (Simon Willison). Roman Sauer found a technique he had developed over years embedded in two separate solutions in the drop. None of these are retraction-worthy outcomes if the proofs hold up. All of them represent people learning on a Tuesday afternoon that the thing they had been building a career around is now in a public repository, with no co-author line and no way to ask the model what it was thinking.

What a Fields medalist writes when they don't have a verdict yet

The Proofs and Prompts blog — a two-week-old blog whose anonymous hosts collected 100+ reactions and published them on October 8, updated October 12 — gives the clearest aggregate picture of what the field is actually saying.

Terence Tao posted a measured but visibly conflicted response. On TechCrunch he is quoted directly: "Problems are being solved autonomously by AI prompters who have no interest in the broader field itself." On Proofs and Prompts the mood is softer and more elegiac: "none of the humans involved in these proofs are available to take questions" and "I mourn the path not taken." The two are not contradictory. They are the same observation in two registers.

Hugo Duminil-Copin, 2022 Fields medallist, said in two words what nobody else wanted to compress to that length: "I am paralysed." Peter Scholze asked for patience and separately warned that systems that produce proofs this fast will eventually produce the cryptographic breaks nobody has prepared for. Melanie Wood at Harvard told TechCrunch "there is not human understanding of them at the point of release, and now the work begins." That last sentence is the entire policy conversation in fifteen words.

There is a joke in the compiled reactions that does the heavy lifting better than any analysis. One contributor noted that OpenAI shipped 719 manuscripts and ten reasoning traces, and the Lean formalisation covered 42 percent — a release ratio that would get a PhD student sent back to their office with a red pen. OpenAI shipped it under Apache 2.0 and got 14,200 GitHub stars in six days.

The unreleased internal model is the reproducibility problem

The structural issue beneath the publication-norms fight is the model itself. OpenAI's post describes an unreleased internal model. It is not available in the API, not available in ChatGPT, and not available to AGMAI. Which means that even if every one of the 719 manuscripts holds up under human verification — and preprints are already being withdrawn, with Sahana Balasubramanya noting at least three on Proofs and Prompts — no outside researcher can run the same methodology against their own 4,000 problems. The reproduction unit is not a model. It is OpenAI.

A separate paper on arXiv (2610.08144), from a team at Cambridge and King's College London, has already identified at least two discrepancies between the natural-language proof and the Lean code on the Navier-Stokes solution. The authors note the discrepancies do not necessarily invalidate the solutions. They note it anyway, because that is how a verification record gets built. Over the next three months this is the work the field will do, mostly for free, for a repository they did not ask for.

What to watch

1. Formal verification coverage over the next release. OpenAI's next math drop — and there will be one — will have a Lean percentage. If it is lower than 42, the publication model is a floor and dropping. If it is higher than 70, the AGMAI guidelines are a successful lobby. The number is the proxy for whether the lab is being pulled toward verification or away from it.
2. The reasoning-trace count. Ten is the number this time. The field's one procedural ask that OpenAI could meet without changing anything about its model stack is to publish the chain of thought alongside the proof. The next release's trace count is the direct answer to that ask.
3. Whether DeepMind, Anthropic, or Mistral publish competing drops under their own publication rules. DeepMind runs Co-Scientist; Anthropic runs the biology lab; Mistral has Large 4 and a trillion parameters of unspent attention. If one of them publishes to the AGMAI standard — full reasoning, full Lean, named human co-authors — OpenAI's October release becomes a one-time move. If none of them does, it becomes the baseline.
4. A credentialed mathematical society's response. The "Association for Human Mathematics" boycott call that circulated on Proofs and Prompts is informal. The American Mathematical Society, the London Mathematical Society, or the IMU have not weighed in on the record. The first institutional statement that treats AI-generated mathematical manuscripts as a distinct publication category — with its own disclosure norms, co-authorship policy, and verification bar — sets a convention that outlasts this release.

The proofs will turn out to be mostly right or mostly wrong. That is the easiest part of the story to resolve and the one most of the trade press is writing about. The harder part — the part the field will be living with in 2027 — is that a company shipped a hundred person-decades of mathematical labour as a GitHub artifact under an Apache licence, listed no authors, released no reasoning for 709 of the 719 outputs, and will do it again. The release is the publication model. The publication model is the release.