OpenAI Publishes Hundreds of Lean-Verified Math Results From an Unreleased Frontier Model

A catalog the size of a journal archive

On October 6, 2026, OpenAI published one of the strangest research releases in modern mathematics: not a single breakthrough paper, but an entire research catalog—372 result families spread across 722 manuscripts, posted to the public GitHub repository openai/math. The drop landed during the opening week at the Institute for Advanced Study’s School of Mathematics in Princeton, where rumors had circulated for weeks that the company was sitting on a large batch of machine-generated proofs. When the files appeared, many senior researchers were left juggling excitement, skepticism, and a practical question that has only grown louder since: what is a mathematician supposed to do with hundreds of PDFs and millions of lines of formal code dropped at once?

The collection is explicitly tied to model development. OpenAI states that the vast majority of results came from the same evaluation procedure using an unreleased internal frontier model, with each result consuming on average about three hours of “ChatGPT Pro thinking” compute. The model was posed roughly 4,000 open problems; outputs were aggregated into families, filtered for significance, and packaged with preprints, build instructions, and—where available—Lean 4 formalizations checked through the company’s Comparator pipeline.

This is not a press release claiming that AI “solved mathematics.” It is closer to a bulk export of an internal benchmark carried to its extreme, with the academic community invited to sort the wheat from the chaff.

Families, manuscripts, and the overview map

OpenAI’s organizing unit is the family: a cluster of related manuscripts that may include a principal theorem, companion lemmas, alternative proofs, or downstream corollaries. The overview.pdf research catalog reads like a phone book of conjectures—harmonic analysis sitting next to ergodic theory, PDEs beside group theory, logic beside combinatorics. Entry numbers follow catalog order; they are not rankings of importance.

Disciplines represented in the overview include convex and metric geometry, theoretical computer science, dynamical systems, algebra, probability, logic, group theory, functional analysis, differential geometry, and partial differential equations, among others. Some headlines are century-old named conjectures; others are technical refinements intelligible mainly to specialists. The breadth is the point: the unreleased model was not tuned to a single Olympiad-style trick domain but to a wide slice of open research.

For navigators, OpenAI provides:

• overview.pdf and CONTENTS.md for family-level summaries.
• A manuscript map linking PDFs, TeX sources, and citation metadata under preprints/.
• A Lean library with a formalization.yaml catalog mapping declarations to comparator configs.

The repository is living: commits through late October increased manuscript counts, file totals, and formalization coverage. Treat any single snapshot as provisional.

Lean, the Comparator, and what “verified” really means

Mathematics has a gift for AI evaluation: proofs are checkable. Lean is a proof assistant and programming language; when a proof term type-checks in Lean’s kernel, the logical steps are mechanically validated modulo the axioms Lean allows (typically including choice and propositional extensionality). OpenAI’s Comparator challenge files define statements and configurations so that solutions can be re-checked in isolation—community projects such as MathVet and independent verification efforts have re-run those checks at scale.

By late October, independent reviewers reported on the order of 245 of 372–373 families with some Lean formalization, 121,000–163,000+ Lean files, and tens of millions of lines of formal code—numbers unprecedented for a single release. The README’s rough figure of ~42% of top-line results formalized is not the same as “42% of mathematics settled”; it measures how many headline theorems have a machine-checked Lean counterpart in the catalog.

Here is the distinction every headline about “AI proved X” must carry:

1. Kernel truth: If Lean accepts a proof, the formal statement in the challenge file is logically established (subject to Lean’s axioms).
2. Semantic alignment: Lean does not prove that the formal statement matches the English theorem in the PDF abstract.

MathVet’s October 2026 review articulated this gap in the vocabulary of the community’s formalization standards. Of families with Lean, a substantial fraction had headlines that were machine-checked as stated; another fraction was checked only in a narrower form than the manuscript claims; roughly a third relied on the prose proof alone, with the README acknowledging that unformalized results “could have issues.” Terence Tao had earlier warned that dumping unverified prose proofs onto the community resembled leaving “carcasses of raw meat” on a communal table—harsh, but it captured the workload shift onto human referees.

Science and New Scientist coverage amplified the nuance: formalization is incomplete; mapping errors exist; withdrawn and revised manuscripts appeared early in the cleanup process. Verification of the proof and verification of the problem statement are separate jobs.

Kakeya, Riemann, and the headlines that travel

Among the families that traveled farthest outside specialist circles were advances in Fourier analysis and analytic number theory—not because the public understands Hausdorff dimension or zero-free regions, but because the names Kakeya and Riemann carry mythic weight.

The catalog includes a manuscript resolving the three-dimensional Kakeya maximal conjecture, with a formalization path registered in formalization.yaml under local smoothing comparators (kakeya_maximal, kakeya). Separately, family 074 addresses four-dimensional Kakeya sets and full Hausdorff dimension—a result that attracted intense Lean community attention, including independent re-verification projects documenting multi-day kernel checks and fidelity audits comparing theorem statements to paper theorems.

On the number theory side, the overview highlights progress on quasi-Riemann hypothesis formulations—zero-free regions for Dirichlet L-functions with explicit half-planes, companion proofs for related regions, and uniform exclusion results tied to Landau–Siegel zeros in the family summaries. These are not claims that the classical Riemann Hypothesis for the zeta function has been proved in full; they are precisely stated theorems in the PDFs whose strength must be read from the statements, not from social media shorthand.

That gap between viral headline and literal theorem statement is where the OpenAI release will succeed or fail reputationally. A Kakeya maximal estimate in three dimensions is a monumental result if the proof is correct and correctly formalized. A quasi-Riemann zero-free region is major progress if the constants and hypotheses match what analysts expect. The catalog gives experts the materials to decide; it does not decide for them.

What the unreleased model implies

OpenAI has not named the internal model that produced the bulk of the manuscripts. Externally, that opacity matters for reproducibility: other labs cannot run the same prompt distribution, search budgets, or tool access. Internally, it signals that mathematics served as a capability probe—a domain where wrong answers can be caught, unlike open-ended creative writing.

The disclosed procedure—thousands of problems, heavy compute per hit, filtering for “appropriate significance”—sounds less like a single eureka moment and more like industrialized conjecture mining. Some families likely extend lines of reasoning the same model explored in earlier internal runs; the README notes that some outputs build on prior model-generated results.

For competitors, the strategic lesson is uncomfortable. If a frontier model can draft hundreds of publishable-looking manuscripts, the bottleneck moves from generation to verification and attribution. Journals, arXiv moderators, and grant panels were not designed for thousand-paper bursts from one sponsor.

Community response: cleanup, collaboration, and caution

Reaction split along predictable lines. Optimists saw a new era where formalization throughput explodes and human mathematicians curate rather than alone discover. Pessimists warned of citation pollution, student confusion, and the reputational risk of embedding errors in Mathlib-scale dependency graphs. Pragmatists got to work:

• Running Comparator checks in sandboxes.
• Auditing statement fidelity (MathVet’s headline-vs-challenge comparisons).
• Formalizing missing families.
• Trying to disprove or shrink theorems—still the fastest way to validate bold claims.

OpenAI’s own maintenance—withdrawals, revisions, growing Lean coverage—admits that the first drop was a starting point. That humility is necessary; without it, the release would be pure theater.

Independent efforts on high-profile problems (Kakeya in four dimensions, Navier–Stokes related formalizations mentioned in press coverage) illustrate both strengths and pitfalls. When fidelity audits pass, confidence in the formal theorem rises even if the prose proof remains unread by most humans. When a formalization matches a weaker statement than the paper advertises, the community learns something embarrassing but valuable about the pipeline.

Epistemology for the post-dump era

The OpenAI catalog forces a discipline-wide conversation about evidence standards:

Claim type	What would convince experts
Prose proof only	Traditional peer review, expert refereeing, gradual acceptance
Lean proof, unmapped headline	Kernel check plus independent statement audit
Lean proof, faithful headline	High confidence in stated theorem; prose still read for technique
Repeated across families	Pattern of model capability, not automatic truth

Students should be taught that “on GitHub with Lean” is not a single rung on that ladder but a bundle of rungs—some families clear the top, others stop halfway.

Incentives and the business of mathematical truth

OpenAI benefits if the release reframes frontier models as research instruments rather than chat toys. The reputational cost of high-profile errors is equally real: one falsely advertised resolution of a Millennium Problem would haunt years of credibility. The hybrid strategy—mass release plus partial formalization plus ongoing updates—spreads risk. Correct formalized gems become showcases; errors in unformalized prose get blamed on the filtering step.

Mathematicians benefit if the Lean library becomes a durable public good. They lose if their time is hijacked by refuting sloppily generated noise. The equilibrium depends on OpenAI continuing to fund cleanup, on journals adapting review norms, and on funding agencies rewarding verification labor as much as novelty.

How to read the repository without drowning

For practitioners who want utility without hype, a disciplined reading order helps:

1. Skim overview.pdf for families in your subfield only.
2. Open the principal PDF; read the theorem statements and dependencies, not the polish of the introduction.
3. Check formalization.yaml for that family—if absent, treat as provisional.
4. If Lean exists, read the challenge statement, not just the manuscript abstract.
5. Watch the repo history for withdrawals or revisions before citing.

Cite carefully. “OpenAI’s model proved X” is almost never accurate; “OpenAI released a manuscript claiming X with partial Lean formalization Y” is.

Looking forward

The 372 families and 722 manuscripts are a stress test for mathematics in the age of generative AI. They do not end the human role in proof; they redistribute it toward specification, auditing, and integration into the living literature. Progress on Kakeya and quasi-Riemann-type results, if confirmed, will enter textbooks regardless of whether the first draft came from silicon or chalk. If disconfirmed, the episode still teaches something about where frontier reasoning fails.

OpenAI has not “changed mathematics forever” on October 6—exactly how it changed is unknown, as Science’s headline conceded. What is certain is that the release set a new scale for machine-generated mathematical output, and that Lean verification—complete or partial—will be the hinge on which acceptance turns. The community’s next move is not applause or dismissal, but the slow, unglamorous work of matching statements to proofs, one family at a time.