OpenAI Publishes 719 Math Manuscripts From an Unreleased Model

OpenAI has published a public GitHub repository of mathematical manuscripts and proof artifacts produced by an internal model that it has not released.

What’s in the repo

According to the repository’s README, as checked on October 11, 2026, the catalogue holds 719 manuscripts organized into 372 families. A family groups related papers: a principal result plus companion arguments, consequences, or alternative proofs. Each family is classified by mathematical discipline.

The collection includes an overview PDF describing the families, a manuscript map, a preprints/ folder with PDFs and source files, and a Lean library with a formalization catalogue. OpenAI also released abridged summaries of the model’s reasoning for ten families, on topics including the irrationality exponent of π, the Mahler conjectures, and Kaplansky’s direct-finiteness conjecture in characteristic two.

How the results were produced

OpenAI says it evaluates its models on open research problems, and expanded those evaluations after its models saturated its existing math benchmarks. Some outputs build on earlier results the models produced.

The README says the vast majority of results came from the same procedure, using an unreleased internal OpenAI model. On average, each result used about three hours of ChatGPT Pro thinking compute. Over the course of the evaluation, the model was posed roughly 4,000 problems. OpenAI grouped the output into families and manuscripts and kept only results meeting a significance bar, producing the current catalogue.

There are exceptions. OpenAI says work on a zero-free region for the Riemann zeta function and a proof of the Hodge Conjecture for CM abelian varieties did not follow the fixed procedure, and that one Riemann zeta write-up was edited by humans for readability.

How much is verified

The README states that about 42% of top-line results are formalized in Lean, a proof assistant that checks every logical step by machine. OpenAI says it will keep adding Lean formalizations as it gets them.

OpenAI is explicit about the rest: “Some of the unformalized results could have issues.” It says it will try to fix any problems quickly, record corrections as new versions while keeping earlier versions accessible, and is exploring community-hosted repositories for the material.

What we don’t know

The model itself is not available, and the README does not name it or describe it beyond calling it an unreleased internal model. Individual results, especially the ones without Lean proofs, will still need checking by outside mathematicians.

Why it matters

Machine-checked proofs offer a level of verification that’s rare in AI announcements: anyone with Lean can confirm those results without trusting OpenAI. For the remaining manuscripts, the release hands the mathematical community a large pile of claims to review, produced by a system outsiders can’t inspect.