OpenAI Math Manuscripts: 722 Proofs, Most Without Lean Checks

What OpenAI put on GitHub

On October 6, 2026, OpenAI published 722 mathematics manuscripts to a public GitHub repository, openai/math, and attributed all of them to an internal frontier model it has neither named nor released.12 The papers are organized into 372 "families" of related results and carry an Apache-2.0 license.12 According to one account, OpenAI gave the model roughly 4,000 problems and then selected the outputs it judged significant enough to publish.3 Among the headline claims is a result described as a quasi-Riemann hypothesis.2

The release is hard to categorize. It is not a model launch, because there is no model card, identifier, pricing, API access, or benchmark table.4 It is not a conventional paper, because nothing has been peer reviewed and no human author is named.24 The repository's README says only that the manuscripts and supporting proof artifacts were "produced by an internal OpenAI model."4 OpenAI describes that model as still undergoing safety work before any public rollout.1 It also says it consulted an advisory group, but that does not substitute for independent review.4

The verification gap

The central concern is how much of the work can be checked. Only 162 of the 722 manuscripts, about 22%, include fully formalized proofs in the Lean proof assistant.2 Another 73 have partial Lean coverage.2 The remaining 487 rest on OpenAI's internal judgment.2 OpenAI does not hide this. Its README warns that "some of the unformalized results could have issues."24

The reasoning behind the proofs is also mostly hidden. Only ten manuscripts include even an abridged summary of the model's reasoning.1 Several outlets flagged this as a transparency gap.1 Readers get finished proof text, and sometimes a formal check, but not the process that produced the results.1

The sources broadly agree on these facts and differ mainly in tone. Tech-insider presents the release as a documented event and notes where coverage converged on the transparency problem.1 Byteiota is blunter, calling it a "dump" and focusing on the 78% of papers without full formal verification.2 The Currency Analytics treats it as a test case in the conflict between proprietary AI and open research.3 Orcarouter's framing is the most careful: it says the material itself is public, while the model behind it remains unexamined.4

The mathematical community responds

The reaction was immediate. The release reached the top of Hacker News and drew 751 comments.2 Twenty-five Fields Medalists signed an open letter in response.2 Terence Tao publicly invoked Goodhart's Law, which holds that a measure stops being useful once it becomes a target.2 In this setting, the concern is that volume of claimed results could crowd out the slower work of establishing that they are correct.

There is also a practical consequence. Because of the permissive license, developers can now use 722 advanced mathematical papers as training data.2 That includes the unverified ones, which means any errors could spread into other models' training sets.

Context: a fast-moving release calendar

The drop fits a pattern of escalating claims. In early September, OpenAI said one of its models had proposed a solution to the Navier–Stokes Millennium Prize Problem, with a writeup and a formal Lean proof.5 Around the same time, the company introduced GPT-6.1 Sol and described GPT-6 Astra as its first model to reach the "Critical" cybersecurity capability level under its Preparedness Framework.5 It has also published material on a Hugging Face security incident and on pacing development amid cyber-critical capabilities.5

Read together, these posts suggest a company that is showcasing capability while holding back the systems themselves for safety reasons. The math release takes that approach further: the outputs are public, but the model is not.

Our reading

OpenAI deserves some credit. Its README is candid about the limits of the release. Open-licensing the work and formalizing 162 proofs in Lean contributes something real and checkable. The Navier–Stokes post also showed the company knows formal verification is the strongest evidence it can offer.5

The rest of the package undercuts that. Publishing hundreds of unformalized results, chosen from a larger pool by undisclosed criteria and produced by a model no one outside OpenAI can study, shifts the cost of verification onto the mathematical community. It also allows the company to claim the headline achievement up front. In our view, the 162 Lean-checked manuscripts should be treated as the actual contribution. The other 560 are, for now, claims awaiting proof.

This matters beyond mathematics. If AI labs routinely release research output while withholding the systems behind it, outside scrutiny will depend on what each company chooses to disclose. Formal verification is one of the few checks that does not depend on trusting the lab, which is why its absence from most of this release is the issue to watch.