OpenAI releases math results from an internal frontier model: 722 manuscripts from about 4,000 open problems, including a Hodge Conjecture case and a zeta zero-free region, with Lean proofs for about 162

Why it matters

Key points

On October 6, 2026, OpenAI published "Sharing AI progress in mathematics," releasing a batch of new results on open mathematical problems produced by an unreleased internal frontier model. The papers and proof materials are in the GitHub repository openai/math.

According to the repository README, the catalogue holds 722 manuscripts grouped into 372 result families and classified by discipline. Over the evaluation the model was posed roughly 4,000 problems; aggregating outputs and requiring a level of significance produced the catalogue. The vast majority of results came from one fixed procedure, averaging about three hours of ChatGPT Pro thinking compute per result. OpenAI says it moved to open problems because performance on its existing math evaluations had saturated.

The repository also includes abridged reasoning summaries for 10 results, covering the irrationality exponent of pi, the symmetric Mahler conjecture, a counterexample to Kaplansky's direct-finiteness conjecture in characteristic two, isomorphism of free group factors, and the three-dimensional relativistic Vlasov–Maxwell system, among others. Two headline items are explicitly listed as exceptions to the fixed procedure: work on a zero-free region for the Riemann zeta function and a proof of the Hodge Conjecture for CM abelian varieties; the Re(s) > 11/12 zero-free region writeup was human-edited for readability.

Some proofs are formalized in Lean, a language in which a computer checks each step of a proof. The repository's formalization catalogue currently lists about 162 manuscripts whose main result has a Lean proof, and OpenAI says it will add more. The release format drew on advice from the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study, with versioned revisions and citations. OpenAI also says it will fund workshops and programs around major AI-produced results and is working toward releasing the model that produced them.

Verifiable

Primary page: https://openai.com/index/sharing-ai-progress-in-mathematics

Repository: https://github.com/openai/math (README, overview.pdf, CONTENTS.md and lean/formalization.yaml)

OpenAI's RSS dates the post October 6, 2026, 12:00 GMT. Manuscript counts, problem counts and compute estimates come from OpenAI's own README, which also says some unformalized results could have issues. The formalization catalogue's review status is marked unchecked: Lean verifies that the proofs go through, but nobody has yet confirmed that each formal statement faithfully matches the paper's claim. The Hodge Conjecture work is not in the formalization catalogue. As of publication, the mathematical community has not published independent verification of the headline results.

Our take

What matters here is less any single theorem than a change in how mathematical results get produced. Roughly 4,000 problems at about three hours of compute each, filtered down to 722 manuscripts, means a frontier model can be run as a continuous research pipeline rather than an occasionally brilliant problem-solving assistant. OpenAI's own admission that its math benchmarks have saturated is itself a capability signal.

The bottleneck moves to verification. 722 manuscripts is far more than any refereeing system can absorb at once, fewer than a quarter have Lean proofs, and whether those formal statements match the papers has not been reviewed. The most striking items, the Hodge case and the zeta zero-free region, are precisely the exceptions to the fixed procedure and deserve the most caution. Three things to watch: independent checks of the headline results by mathematicians, how far Lean coverage and statement review progress, and when and in what form the underlying model is released. Until then, reading this as "AI has proved the Hodge Conjecture" overstates it; "research output is no longer scarce, verification is the new bottleneck" is closer to the facts.