OpenAI posts 700-plus math manuscripts on GitHub

OpenAI on October 6 published a broad collection of AI-generated mathematics work in a public GitHub repository, releasing manuscripts, proof artifacts and formalization materials from an internal frontier model. The company said the catalog spans 372 related result families and sits at the center of a larger research push to make model-produced mathematical results easier for researchers to inspect, check and extend.

The release is notable for both its scale and its caution. OpenAI’s repository says the current catalog contains 719 manuscripts, while the company’s October 6 community post said the public repository currently contained 722 manuscripts organized into 372 related result families. The difference indicates the collection changed around launch. OpenAI also said the results are at different stages of verification, and that not every manuscript has a formal proof package attached.

What did OpenAI actually release?

OpenAI released manuscripts, supporting proof artifacts and Lean formalizations for many of the results, plus abridged reasoning summaries for 10 named result families. The company said the materials are organized by family, where a family groups related papers such as a principal result, consequences, companion arguments or alternative proofs, and each family is classified by mathematical discipline.

The repository also includes a preprints directory with PDFs, source files and manuscript-specific citation and build instructions, along with a Lean library and formalization catalogue describing available formal proofs, associated papers and verification configurations. OpenAI said the release was designed so builders and researchers can inspect or extend the materials, and that it is exploring community-hosted repositories for the math work. In its announcement, OpenAI said it consulted the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study and drew on the group’s advice and public recommendations when planning the release.

Among the 10 result families with abridged reasoning summaries are results on pi, Mahler conjectures, direct-finiteness, spin glasses, free group factors and Vlasov, according to the repository.

How much of the work is formally checkable?

OpenAI said about 42% of top-line results are formalized, meaning they have Lean proof artifacts that a computer can check for consistency with the encoded proof steps. Lean is a programming language used for theorem proving, so these formalizations matter because they let outside readers verify parts of the math mechanically rather than relying only on prose papers.

The company said Lean formalizations are available for many, but not all, of the manuscripts, and that additional formalizations may be added later. OpenAI’s repository also warns that the collection spans different verification stages and that some unformalized results could have issues. One independent verifier reported that all 2,924 modules in one proof compiled with no errors or warnings, though that check covered the Lean proof rather than the paper itself and was only one run on one machine using an AI agent at his request.

OpenAI said the release also came with protocols for paper revisions and citations, and that previous versions will remain accessible while corrections are recorded as new versions. The repository says readers should cite individual manuscripts using the BibTeX block in each manuscript directory.

How did OpenAI evaluate the model behind the papers?

OpenAI said the vast majority of the results were obtained with the same procedure using an unreleased internal model. The company said the model was posed about 4,000 problems during evaluation and that each result used roughly three hours of ChatGPT Pro thinking compute on average.

The repository says the catalogue was created by aggregating outputs into result families and manuscripts and requiring an appropriate level of significance. It also notes exceptions to the fixed production procedure for work on a zero-free region for the Riemann zeta function and a proof of the Hodge Conjecture for CM abelian varieties. OpenAI said some outputs in the release build on earlier results produced by its models. Its repository also says it expanded mathematical evaluations after performance on existing math benchmarks saturated.

In its community post, OpenAI said it had consulted the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study and used the group’s advice and public recommendations to inform the release. The company also said the published materials include papers, supporting proof artifacts, Lean formalizations for many results and 10 abridged summaries of the model’s reasoning, with the mathematical areas spanning fields such as algebra, geometry, number theory and mathematical logic, according to reporting that cited OpenAI’s announcement and the company’s release.

What happens next for researchers and builders?

OpenAI said it will preserve public release history and keep older versions accessible while recording corrections and revisions as new versions. That makes the repository more like a living research archive than a one-time dump, which could matter for mathematicians trying to track which statements are still under review and which have formal checks attached.

The company said it will support workshops, conferences and other programs to help researchers examine the findings. For founders and AI builders, the practical significance is less about a single benchmark score and more about the release format: source manuscripts, proof artifacts and formal verification materials are all available in one place, making the collection inspectable and extensible by outsiders.

OpenAI said it expanded mathematical evaluations after its performance on existing math benchmarks saturated, suggesting the project is also part of a broader effort to find harder, more informative tests for frontier models. In that sense, the release is both a research publication and a signal about where AI evaluation is headed in technical domains where correctness can be checked step by step.

A separate community update said OpenAI’s public repository also included 10 abridged reasoning summaries and that the release process would continue to incorporate revisions as they are identified. The company’s repository says corrections and revisions will be recorded as new versions, while previously released versions remain accessible, and readers are directed to cite the relevant manuscript directly from its own BibTeX block.