---
title: "OpenAI's 722 math papers on GitHub: what Lean didn't prove"
description: "OpenAI posted 722 math papers from an unreleased model to GitHub and withdrew 3. Only 42% of main results are in Lean; some Lean code proves less than claimed."
url: https://udon-dev.com/en/notes/openai-math-release-agmai/
lang: en
published: 2026-10-09
topic: [ai]
tags: ["openai", "math", "lean", "ai-research"]
---

# OpenAI's 722 math papers on GitHub: what Lean didn't prove

- On October 6, OpenAI posted math papers written by an unreleased internal model on GitHub. It withdrew 3 the next day, leaving 719 papers in 372 families. The model was given about 4,000 problems
- OpenAI consulted an advisory group of mathematicians at the Institute for Advanced Study (AGMAI). But the release does not meet several of the guidelines AGMAI issued on September 29, such as not testing on non-public models and giving a reasoning summary for each result
- About 42% of the main results were formalized in Lean. In the Navier–Stokes proof, researchers at the University of Cambridge and elsewhere showed that the Lean code proves a weaker claim than the paper in places
- AGMAI stated that its advice does not mean it endorses how OpenAI obtained the results. Terence Tao points to a different problem: people who have AI solve problems often cannot explain the results afterward

On October 6, 2026, OpenAI published a batch of math papers written by its internal model in the GitHub repository [openai/math](https://github.com/openai/math). In [its post on X](https://x.com/OpenAI/status/2107596713791767021), OpenAI said it had consulted an advisory group of mathematicians at the Institute for Advanced Study (IAS) in Princeton and incorporated their advice. Two days later, TechCrunch reported that "[OpenAI's math solutions aren't meeting the field's standards yet](https://techcrunch.com/2026/10/08/openais-math-solutions-arent-meeting-the-fields-standards-yet/)."

（図: GitHub preview image for the openai/math repository: the repository name and description, contributor and star counts, and the organization's icon）
Source: [openai/math README (GitHub)](https://github.com/openai/math)

In this post, I look at what was actually released, then compare the release with the main points of the advisory group's guidelines. I also check, against the papers and primary sources, what problems remain in proofs that are "verified in Lean."

## What was released

According to the [README](https://github.com/openai/math), the release consists of papers written by an unreleased internal model and the proof materials behind them. OpenAI explains that its models' scores on existing math benchmarks had plateaued, so it expanded evaluation to open research problems.

There are 719 papers, grouped into 372 families. A family collects a main result together with its supporting arguments and alternative proofs. The model was given about 4,000 problems. On average, the compute per result equals 3 hours of ChatGPT Pro thinking time. Most results came out of the same process. The exceptions are work on zero-free regions of the Riemann zeta function and a proof of the Hodge conjecture for CM abelian varieties. Part of the former was rewritten by people to make it easier to read.

Summaries of the model's reasoning were published for only 10 families. 300 of the main results (about 42%) were formalized in Lean.

Early reports put the count at 722 papers. According to the [history file](https://github.com/openai/math/blob/main/history.md), on October 7 OpenAI withdrew 3 papers: 1 whose argument collapsed because of a sign error, and 2 that relied on its construction. It also corrected proofs, statements or outdated citations in 14 papers, and updated citations to newer versions in 13. The README itself admits that unformalized results may contain problems.

## What AGMAI's guidelines asked for

The advisory group is the Advisory Group on Mathematics and Artificial Intelligence (AGMAI), hosted by the IAS. According to [AGMAI's site](https://agmai.org/), it began when OpenAI approached some mathematicians about forming an external advisory board. After discussion, it became a group independent of any AI company. It has 9 members, who are unpaid. The site states that the group has no authority over AI companies' decisions, and that responsibility for those decisions lies with the company.

On September 29, based on more than 600 responses from the mathematical community, AGMAI issued [guidelines for releasing AI-generated mathematics](https://agmai.org/general-sep29/). They open by asking companies to stop testing advanced math problems on proprietary models that outsiders cannot use, and state plainly that AGMAI does not support this practice. For releasing papers that people do not yet understand, the pillars are per-result disclosure, formalization, where results are hosted, and funding for efforts to help people understand them. The table in the next section compares these with this release.

## The guidelines versus this release

Here is the comparison, based on what the README and press reports show.

| What the guidelines ask | This release |
|---|---|
| Do not test on proprietary models | The README says it tested on an unreleased internal model |
| For each result, give the model name, prompts and a summary of the reasoning | Summaries for only 10 families |
| Disclose time and compute cost | Only an overall figure: an average of 3 hours of ChatGPT Pro thinking time |
| Formalize as much as possible | About 42% of the main results |
| Show the correspondence between natural language and the formalization in machine-readable form (worded as helpful to have) | According to TechCrunch, not provided |
| Disclose the number of unsolved problems and how problems were selected | Only the number given to the model, about 4,000. No count of unsolved problems and no description of how they were selected. It does say the published results were limited to those with some significance |
| Host results in a repository not controlled by an AI company | Hosted on OpenAI's GitHub. The README says a community-managed home is under consideration |
| Fund efforts to advance human understanding in proportion to a result's importance and complexity (examples: workshops, long-term research groups, funding for postdocs and students). Existing nonprofits, not the AI company, decide where the money goes | [OpenAI's blog](https://openai.com/index/sharing-ai-progress-in-mathematics/) says it will fund workshops and special programs, with details to be announced soon |

Some points were met. TechCrunch writes that OpenAI did release results as early as possible and attached information on how the model reached its conclusions. Keeping withdrawals and corrections as versioned history also follows the guidelines.

AGMAI issued a statement on October 6, the same day as the release. It says its advice does not mean it judged the significance of the results, nor that it endorses how OpenAI obtained them. Its position is that the math community should judge how well the guidelines were followed. When TechCrunch asked for a more detailed assessment, AGMAI did not respond.

## Problems that remain even when Lean verifies a proof

A [paper](https://arxiv.org/abs/2610.08144) posted on October 6 by three researchers at the University of Cambridge and King's College London shows that formalized proofs can still have problems. Its subject is the proof OpenAI announced in September of blow-up for solutions of the Navier–Stokes equations (a solution diverging in finite time).

The paper deals with a step called autoformalization. An AI translates a proof that an AI wrote in natural language into code for Lean, a proof assistant. If the Lean code checks without errors, a machine has confirmed that the theorem the code states is true. But Lean cannot check whether the translation faithfully captures the meaning of the original proof.

The paper shows that this gap actually occurs in OpenAI's proof. For example, equation (8.19) in Lemma 8.6 of the paper bounds the derivatives of the output by the input's derivatives up to order m+4. The corresponding Lean code uses derivatives up to order m+5 as a hypothesis, so it proves a weaker claim than the paper. The authors write that the same kind of gap appears throughout the Lean code and give 2 concrete examples.

The authors do not say OpenAI's natural-language proof is wrong. Their point is that passing Lean verification does not guarantee the natural-language proof is correct. They conclude that neither OpenAI's proofs nor any other autoformalized proofs should be trusted as is until they go through the same peer review as any other proof. They consider it very likely that the Euler equations proof announced at the same time has the same kind of gap, but they have not shown that yet.

The guidelines say a machine-readable correspondence between the natural language and the formalization would help. With that correspondence, gaps like these would be easier to find, but this release does not include it.

The Navier–Stokes proof has another backstory. Tristan Buckmaster of New York University was also working on the same problem. According to [a TechCrunch article from September](https://techcrunch.com/2026/09/08/openai-fought-dirty-on-career-making-math-problem-says-nyu-mathematician/), Buckmaster claimed that OpenAI started its effort after word of his team's progress reached it. OpenAI says it never saw their work before it was published.

## What mathematicians object to

Behind AGMAI's guidelines is a norm in mathematics: the authors of a paper understand its content, verify its correctness themselves and take responsibility for it. Mathematicians who produce major results explain them at seminars and conferences and answer questions. The guidelines say that if an AI company releases a large number of results that no one understands, it is the company's responsibility to make sure understanding catches up later.

Terence Tao raised this point in [a post on Mathstodon](https://mathstodon.xyz/@tao/117395268130901862) on the day of the release. He did not name OpenAI. He writes that people who have AI solve problems tend to lose interest in the field itself once the target problem is solved, and do not understand the output well enough to answer questions or give talks about the results. As a result, compared with major results in the past, far fewer seminars and collaborations come out of it, and few people join the field. A problem that has been solved never becomes open again, so if problems are harvested in bulk, the field itself withers. That is his view.

Melanie Wood of Harvard University is also a member of AGMAI. She told TechCrunch that the model's solutions were not understood by anyone at the time of release, and that the work starts there.

## What is still unknown, and what to watch

It is not yet known how many of the 719 papers people can understand and take responsibility for. The day after the release, 3 papers were withdrawn and 14 were corrected, so errors are turning up even before peer review.

There are 3 signs of whether the release moves closer to the guidelines: whether the share of formalized results rises, whether a correspondence table between natural language and formalization appears, and whether the papers move to a community-managed home.