October 9, 2026
Mathematicians will be checking OpenAI's proofs for years: about 42% have Lean verification
OpenAI has posted 719 manuscripts with math results to a public repository (per GitHub as of Oct 6; secondary sources say 722). They are grouped into 372 result families, and about 42% of them have a formal Lean verification.
Complexity theorist Dana Moshkovitz, reading part of OpenAI’s proofs, said: “It’s as if someone wrote them on psychedelics.”
More than three dozen mathematicians the journalists spoke with called the situation “stunning” and “pure madness.” The reason is volume: the flood of results hit the field in a single week, and it will take years to work through it.
What was released. The openai/math repository contains 719 manuscripts, grouped into 372 families. Start with overview.pdf, which describes the families. To find a specific paper, use CONTENTS.md, and the verification instructions are in ComparatorChallenges/README.md. Lean is the language a computer uses to check a proof step by step.
How it was produced. DataCamp writes that the models were given about 4,000 open problems. Each result took on average about three hours of ChatGPT Pro thinking time, and most results came from one fixed procedure. The prompts, the compute spent on each problem, and the model name were not disclosed, which contradicts the advisory group’s recommendations.
Such problems used to take years. Buckmaster and Alpöge spent almost a year on a proof for Navier–Stokes. According to MIT Technology Review, OpenAI solved the problem in a few days by running 10,000 agents at once, at a cost of millions of dollars.
The contested part. Terence Tao (UCLA) described the preliminary solution of the problem with purely AI methods, without full transparency of the process, as something that may “contaminate this process to such an extent that it becomes a pure net negative for progress in mathematics as a whole.”
The next question is how many of the 372 result families will get machine verification in Lean.