OpenAI has published 722 machine-generated mathematical manuscripts across 372 research families, alongside selected Lean formalizations that allow computers to check parts of the underlying proofs.
OpenAI has placed 722 machine-generated mathematical manuscripts in public view and paired some of them with formal proofs that computers can check. The release is not a claim that every paper is correct. It is a rare attempt to expose machine-produced research to inspection while separating plausible mathematical output from arguments that have survived formal verification. The public mathematics repository is presented as an evolving catalogue, with additional Lean formalizations expected over time.
The collection is organized into 372 research families covering pure mathematics, theoretical computer science, and mathematical physics. It includes work on number theory, complexity theory, geometry, and problems involving quantum Heisenberg ferromagnets and relativistic Vlasov-Maxwell equations. The grouping is important: the 722 manuscripts are not 722 completely independent discoveries, but a set of related results assembled into broader families for examination.
The important advance is therefore not simply volume. OpenAI has made the generated manuscripts available alongside source files, revision records, citation guidance, a catalogue of formalizations, and selected reasoning summaries. The repository's configuration and Lean code link available machine-checkable proofs to specific manuscripts, giving mathematicians material to examine, reproduce, challenge, and potentially extend.
Several research families address questions where progress depends on long chains of technical reasoning. One concerns the irrationality exponent of pi, a measure of how closely rational numbers can approximate pi. Another examines NP-hardness within computational complexity theory. Other groups of manuscripts concern Mahler conjectures, arithmetic progressions, and free group factors.
These subjects are not interchangeable benchmarks. A result about approximation to pi does not test the same capabilities as a result in complexity theory or mathematical physics, and a manuscript that appears novel still requires scrutiny of its definitions, assumptions, proof strategy, and relationship to earlier work. The collection provides breadth, but breadth alone does not establish reliability. As with submissions to established scientific venues such as Nature, the significance of a claim depends on technical checking and expert assessment rather than on the scale of the submission.
OpenAI says the model attempted roughly 4,000 problems during the research process. The published 722 manuscripts are an organized and selected catalogue, not a complete record of every attempt. An accepted result consumed about three hours of equivalent ChatGPT Pro thinking compute on average. The company has also released additional statistics about attempted problems and research outputs, while identifying 10 research families with abbreviated summaries of the model's reasoning.
Those summaries should not be confused with full proof records. OpenAI's public discussion describes them as condensed accounts for 10 result families, published separately from the Lean artefacts. They may help readers understand the model's approach, but they do not replace a formal proof, independent reproduction, or expert review.
Lean is a proof assistant: a programming language and verification environment in which mathematical statements and their proofs can be expressed as formal code. Its role is narrower and more demanding than asking a language model to explain why an answer seems convincing. A Lean checker tests whether the formal steps follow from the stated assumptions inside the formal system.
That distinction matters because fluent mathematical prose can hide gaps, ambiguous definitions, or an invalid inference. A computer-checked proof can expose some of those problems, but only when the relevant result has actually been formalized. Many manuscripts in the collection do not yet have Lean versions, and OpenAI plans to add more as researchers complete the verification work. The company explicitly warns that unformalized results may contain errors.
Formal verification also has boundaries. It does not decide whether a theorem is important, whether its assumptions describe an interesting problem, or whether the result is genuinely new. It checks the encoded argument; it does not replace mathematical judgment about the choice of definitions, the interpretation of the result, or its place in existing research. This distinction resembles the broader separation in computational science between validating an implementation and deciding whether the model captures the phenomenon of interest, a concern familiar across institutions including MIT and CERN.
The release is best understood as a research archive rather than a finished body of independently validated mathematics. The source material does not establish that the manuscripts have been peer reviewed, independently reproduced, or accepted by the wider mathematical community. It does establish that OpenAI has made the work public and that some proofs are being translated into a form suitable for computer checking.
OpenAI developed the release process with advice from the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study. That advice adds institutional context to the disclosure process, but it does not turn every manuscript into a verified result. The distinction between advisory input and mathematical validation remains essential.
Reasoning summaries provide a view of how the model approached selected problems, but they are separate from Lean proofs. A persuasive explanation of a solution is not itself evidence that the explanation accurately describes the process that produced the answer. Nor does a successful formal proof show that the model can reliably solve a broad class of new problems without human selection, correction, or formalization work.
The release also shows where the human research process remains embedded. Researchers must assess candidate results, organize related manuscripts, decide which claims merit further work, translate proofs into Lean, inspect failures, and track revisions. The system generated the manuscripts, but the public record does not describe an independent machine-only pipeline that removes those judgments. In that respect, the workflow is closer to computer-assisted research than to an autonomous replacement for mathematical laboratories or universities.
OpenAI plans to support workshops, conferences, and special programs focused on major mathematical results generated by AI. Feedback from mathematicians is expected to influence future disclosures. That approach is more credible than treating generated papers as self-authenticating discoveries: the value of the collection will depend on whether specialists can test the claims and make the verification process consequential.
For researchers, the repository offers a substantial set of candidate problems and proof attempts in one place. For readers outside mathematics, it offers a more grounded way to assess AI reasoning claims. The relevant question is not whether the prose sounds like a research paper. It is whether a result survives formal checking, expert examination, comparison with prior work, and repeated attempts to find a flaw.
Lean formalization is a form of machine-assisted verification rather than a general certificate of scientific truth. The checker can confirm that a formal proof follows from its formal premises, while human mathematicians still determine whether the premises capture the intended problem and whether the theorem contributes something meaningful. OpenAI's release is therefore significant because it connects generation with auditability, but its strongest evidence applies only to the subset of work that has been formally encoded and checked. That makes the repository a serious test of AI-assisted mathematics rather than proof that an internal model has replaced mathematical research.
The next stage will be especially important for reproducibility. As further formalizations are added, readers will be able to distinguish more clearly between manuscripts that remain conjectural, arguments that have been partially translated, and proofs accepted by the Lean checker under explicit formal assumptions. The catalogue's value will therefore grow not merely through additional manuscripts, but through transparent links between claims, code, verification status, and subsequent expert assessment.
