OpenAI Math Repo: What the Lean Proofs Do and Don't Verify

Last updated: October 8, 2026 - checked against the repository README and OpenAI's post two days after release. The repo is changing daily, so counts will drift.

The openai/math repository is OpenAI's biggest dump of model-written mathematics so far: hundreds of manuscripts from an unreleased internal model, with Lean formalizations for only some of them. Search interest for "openai math" jumped from a baseline in the low single digits to the top of its one-month range on October 7, per Google Trends. The part worth a developer's time is not the theorems. It is the verification design: what a machine-checked proof guarantees, and what it quietly leaves to a human.

What OpenAI actually released#

OpenAI's research post from October 6 says the company is releasing "a broad range of new mathematical results produced by an internal frontier model," published in a GitHub repository with protocols for paper revisions and citations. It adds Lean formalizations of "many" of the proofs, 10 summaries of the model's reasoning, compute estimates in ChatGPT Pro terms, and statistics on attempted problems. The average result used roughly three hours of ChatGPT Pro thinking.

The repository README fills in the numbers, and they have already moved since launch coverage:

• It currently counts 719 manuscripts in 372 families. Launch-day coverage said 722, so treat any single count as a snapshot.
• About 42% of top-line results are formalized in Lean. The README says plainly that the collection "includes results at different stages of verification" and that "some of the unformalized results could have issues."
• The model was posed about 4,000 problems, and "requiring an appropriate level of significance" filtered the output down to the catalogue. Most results used one fixed procedure with the unreleased model.
• Two exceptions are called out: a zero-free region for the Riemann zeta function, whose writeup was human-edited for readability, and a Hodge Conjecture result for CM abelian varieties.

Earlier in the year OpenAI shipped a smaller version of the same idea with ten decade-open proofs, each with a Lean certificate. This release trades that all-certified bar for volume, and that trade is the story.

How the Lean check works, and its blind spot#

Lean is a proof assistant: a proof only compiles if every step type-checks. The Lean README in the repo warns that the formalizations form one large library, recommends compiling small portions at a time, and points to a Comparator README for verification. It also notes that a full build can fail on Linux if vm.max_map_count is too low, with a workaround involving building Lean with -DMMAP=OFF.

The Hacker News thread surfaced the design detail that matters. Challenge files state a theorem with sorry, a Lean placeholder meaning "unproved," and the proof lives elsewhere; one commenter explained that the tool checks every sorry is covered so the model cannot quietly rewrite the specification it is trying to prove. A reader who opened the Barnette's Conjecture challenge file saw only the statement and a bare sorry and briefly thought the proof was missing. Another commenter pointed to the JSON file beside it, which says where the solution starts.

That design closes one attack, a model changing the question. It does not close the other one: a proof can be perfect for a statement that is subtly weaker than the real conjecture. Lean certifies the proof against the formal statement. Whether the formal statement means what the paper says is still a human reading job. For the unformalized majority, nothing is machine-checked at all.

The angle: what changes for people shipping agents#

You will not review 719 manuscripts. The transferable lesson is about where trust goes when agents produce more than anyone can read.

1. Pin the spec, let the agent write the proof. The setup HN commenters described separates the fixed statement from the agent-written solution. The coding analogue is a test suite or contract the agent cannot edit. If your agent can modify the tests it is graded on, you have a model grading itself - the same failure that agent evals without baseline receipts describe.
2. Label the verification tier on every artifact. The README is honest that results sit at different stages. Do the same for agent pull requests: "tests pass and a human read the diff" is a different claim from "tests pass." The review bottleneck gets worse when every output looks equally trustworthy.
3. Budget for the checker, not just the generator. About three hours of Pro compute per result is a generation cost. The expensive part, as Anthropic's Lean formalization of Fermat's Last Theorem also showed, is the repo-scale verification layer around it.

This also tells you where frontier labs are heading. The model is unreleased; OpenAI says it is "working to responsibly release" it. Meanwhile the shipping models developers can actually use are covered in the GPT-6 Astra guide.

What people are actually saying#

The Hacker News thread was at 1,284 points and 1,457 comments when I read it, and it split three ways:

• Awe and loss. One commenter who spent 24 years on and off on Barnette's Conjecture wrote that seeing it listed as solved felt like a quiet bereavement, and that the paper's approach looked like one they had abandoned long ago. Notably it has no Lean proof, so they were still reading it.
• Access and concentration. Another commenter argued that this progress is not reproducible with technology ordinary people can use, and that withheld proprietary models are a concentration-of-power problem. A reply quoted the Institute for Advanced Study advisory group, which says it does not endorse testing advanced problems on inaccessible proprietary models and asks labs to stop. The reply's point: the group's members are pro-AI, and the objection is about access, not about going back.
• Mining or growth. The "open problem strip miner" jab drew a counter that solved problems still create work for humans - exposition, alternative proofs, new directions - and a counter-counter that the career incentives for doing that work are what disappears.

The counter-case worth keeping in mind: a commenter who is glad about the Lean work said they are not convinced these models write good English explanations, and pointed at the dense opening of the Unique Games paper as hard to parse. Formal proofs make that survivable. For the unformalized results, readability is a real limit on how fast the community can check them.

What I could not verify#

I did not compile any of the Lean library, and I have not checked any individual theorem. The counts above come from the README as of this writing. Claims that a specific result is correct or wrong belong to the mathematicians reading the papers, not to this post.

Continue Reading#

• OpenAI Publishes Ten Decade-Open Math Proofs, Each Formalized in Lean - the smaller, fully certified predecessor release
• Anthropic's Fermat Proof Is an Autoformalization Milestone - Claude formalizing Fermat's Last Theorem in Lean
• Agent Evals Need Baseline Receipts - why a score without a baseline proves little
• The Code Review Bottleneck in AI Coding - what happens when output outruns reading
• GPT-6 Astra Release Guide - the shipping frontier model from OpenAI

Sources#

• Sharing AI progress in mathematics - OpenAI
• openai/math repository README
• openai/math Lean formalizations README
• Hacker News discussion
• Google Trends interest over time, "openai math" vs "claude code skills", one month to October 8, 2026