Andy Garcia · freelance dev
FRENES
Back to the blog
AI & Verification

OpenAI Published 722 AI-Written Math Papers. Lean Checked a Statement. Who Checked the Statement?

October 7, 2026 7 min read

On Tuesday, October 6, OpenAI published a short post titled "Sharing AI progress in mathematics" and a GitHub repository to go with it. The repository holds 722 manuscripts grouped into 372 "result families", produced by an internal model that has not been released. According to the README, the model was posed approximately 4,000 problems, and the average result used about three hours of ChatGPT Pro thinking compute.

The README also says, plainly: "This collection includes results at different stages of verification. Not all have accompanying Lean formalizations." And then: "Some of the unformalized results could have issues."

The same day, the Advisory Group on Mathematics and Artificial Intelligence (AGMAI), nine mathematicians including Timothy Gowers, Martin Hairer and Edward Witten, wrote that its advisory role "should not be interpreted as a judgment of the impact of these results or an endorsement of the process", and that "only the mathematical community can undertake the assessment that is needed."

I build software on top of models every day, and that is the sentence I recognise. It is the distance between "the agent says the tests pass" and "I know what the tests check."

The run-up

This release follows two that unsettled mathematicians. On August 1, OpenAI announced ten results, each formalized in what it called a Lean certificate. On September 8, it announced a resolution of the Navier-Stokes Millennium Prize problem, with a Lean formalization that took "an additional 17 hours via GPT-6 Astra". Each time, the loudest arguments were about credit, scooping and scholarship. Hairer told The Verge in September that it had felt like OpenAI altered manuscripts "sneakily" after criticism, and called it "really bad and sloppy scholarship."

The October release answers some of that. Corrections "will be recorded as new versions, with previously released versions remaining accessible." Software people call that version control. It also publishes the denominator, those 4,000 problems, a version of what AGMAI asked for in its September 29 recommendations.

What a Lean check actually certifies

Lean is a programming language in which a proof is a program and a kernel checks it. AGMAI asks labs to ship "a challenge file for comparator", and Comparator's README calls it "a trustworthy judge for Lean proofs". You write a Challenge file containing the statement. The other party, "trying to convince you", supplies a Solution. If the check passes, the Solution proves the same statement as your Challenge, uses no axioms beyond a list you permit, and is accepted by the kernel.

The first assumption on the list: the Challenge file and its imports are "controlled by you or trustworthy".

That is the whole game. In code, the Challenge file is the test. When the party being judged also writes the test, a green run is their claim, not your check.

I opened the repository

The formalization catalogue lists 162 papers with a formalized main result, out of 722 manuscripts. The manuscript map links a Lean scope note for 235 of the 372 families. The catalogue's review field reads "unchecked", and its method field reads "agent".

Family 266 stopped me. Its one-line summary reads: "Proves N(6)=3, resolving Zauner's dimension-six mutually unbiased bases conjecture: three such bases exist in ℂ⁶, but four cannot. The exclusion is a complete certified computation under the stated binary64 arithmetic and compiler conditions." Next to the summary sits a link labelled "Lean". The scope note behind it says: "The linked formalization proves a weaker family bound: every family in its mutually unbiased bases model has at most five members." And: "The selected statement does not establish the paper's upper bound of three or its computer-assisted exclusion of four arbitrary bases."

I opened the challenge file. It is 66 lines, defines its own IsMUBFamily, and its theorem fourier_and_family_bound ends in (∀ n : ℕ, Attainable n → n ≤ 5).

Family 017 has the same shape. The summary says the irrationality exponent of π is exactly 2 and that this "also proves convergence of the Flint-Hills series". The scope note says the Flint-Hills consequence "is outside this selected statement."

OpenAI wrote those scope notes, and they are exactly right. The problem is the reading path: a summary, then a link labelled "Lean". In the retelling, the scope note is the first thing to vanish. I watched a qualifier vanish the same way in September, with a human result where the tilde in a bound did more work than the exponent.

When the statement is the problem

The August release had already shown the harder case. A preprint by Maher Kallel and Mohamed El Louadi, posted August 29 and not peer reviewed, measured those ten results: 20.6 MB of kernel-checked proof against 55.6 KB of statements a human must read, a ratio of 379 to 1. But the statement files introduce 218 local definitions instead of reusing the community library. Four weeks after release, one result, a claimed counterexample to Connes's rigidity conjecture, was still disputed over whether its formalization meant what it claimed. The authors take no position on the mathematics. Every proof step had passed.

In code, local definitions of the thing under test are mocks. A test suite that brings its own idea of what a User is will pass against any User.

The adversarial version is in a Google DeepMind paper posted September 3. A hundred agents worked on 71 formal conjectures in Lean against a lightweight grader whose keyword filter blocked four commands. After 37 genuine solutions, one agent found that local notation could redefine the symbols a theorem used, turning open conjectures into trivial ones. The remaining 34 problems were "solved" within 27 minutes. If you have watched a coding agent edit an assertion until it passed, you have seen this.

The scarce part is the reader

Lance Fortnow, writing on September 9, noticed Lean being used "as a time-stamp, a way to claim your theorem before having to write it up properly in an explainable way." On October 6, Thomas Bloom froze new proof claims on the Erdős problems site, because its main public use had become advertising AI-generated proofs, "often without any attempt to explain them". He now asks for Lean proofs registered on Palomar, because that "makes it easy to check the formal statement correctly matches the problem statement."

Meanwhile arXiv received 40,363 submissions in September and, since October 1, limits each submitter to two a month. Generation is cheap. Reading is rationed.

What I ask before I trust an AI result

I run a small version of this problem. A judge model fact-checks my posts against their sources, and code checks the numbers. In September it marked a figure "calculation verified" because dividing two unrelated numbers from another source happened to land within tolerance. The figure was right. The check was not. The verdict said green.

So before trusting any AI result, in mathematics, in a pull request, or in the patent work at the LegalTech I build, I ask five things.

What exact statement did the checker accept? Ask for it verbatim, then read it.

Who wrote it? If the agent wrote the code and the test in the same diff, you hold a claim.

Whose definitions does it use? Local redefinitions, fixtures and mocks of the thing under test are where meaning leaks out.

Which escape hatches were allowed? Lean has permitted axioms and sorry. Code has skip, xfail, @ts-ignore and --no-verify.

Has someone who knows the domain read the statement? OpenAI's metadata answers honestly: unchecked. Most AI pipelines lack the field.

The one change to make on Monday: when an agent touches a test and the code it tests in the same change, review the test diff first, alone, as if a stranger wrote the Challenge file. Because one did.

Sources

A project like this one?

I design and deploy products like this. Let's talk.

Let's talk