OpenAI published nearly 400 math claims, researchers must verify

OpenAI published 722 manuscripts, organized into 372 “families” of related results, in a public repository called openai/math. A family can bundle a main theorem with spin-off results or alternative proofs, so 722 counts papers, not solved problems. In all, it amounts to nearly 400 distinct AI-generated results.

The work spans a wide range of math: combinatorics, geometry, number theory, algebra, topology, probability, theoretical computer science and mathematical physics. The table of contents and abstracts alone run to roughly 40 pages, and several mathematicians said just skimming them took the better part of an hour.

OpenAI says it gave the model about 4,000 problems and kept the outputs it considered significant enough to publish. The average result used about the computing power of three hours of ChatGPT Pro thinking time. This is the same internal model behind OpenAI’s disputed Navier-Stokes claim a month earlier, a result tied to one of the famous million-dollar Millennium Prize problems.

Only some of them, and the exact share depends on how you count. Lean is a programming language and proof assistant: if a proof is written in Lean, a computer can check every logical step mechanically. That makes it the fastest way to trust a result you don’t fully understand.

OpenAI said 300 top-line results across 719 manuscripts had been formalized, around 42 percent. A separate count, based on the repository’s own formalization catalog, found only 162 of the 722 papers had a computer-checked main result, about 22 percent. OpenAI’s own README warns that some of the unformalized results could have issues, and promises to add more Lean proofs as it gets them.

Even a passing Lean check has limits. It tells you the logic holds for the exact statement typed into Lean. Whether that statement is faithful to the real problem, and whether the result is fresh or worth anything, still takes a human expert to judge. Mathematicians digging through the files said the quality of the formal proofs was uneven and didn’t always line up neatly with the claims in the papers.

Kevin Buzzard of Imperial College London said only about six theorems in his own field stood out to him, and few if any appeared to be checked in Lean. That leaves him reading possibly flawed papers, waiting for others to read them, or waiting for someone to formalize them.

More than three dozen mathematicians described the release with words like “staggering” and “surreal.” Their worries fall into a few groups:

• Volume. Researchers agree that simply understanding what was released could take years, and many fear OpenAI will release even more before they finish.
• Careers. NYU professor Tristan Buckmaster said whole research programs, many belonging to early-career mathematicians, were wiped out overnight because their planned problems now have claimed solutions.
• Accountability. Northwestern’s Bryna Kra pointed out that nobody at OpenAI could give a talk or answer technical questions about these results, the way a human author would.
• Secrecy. Kra also warned that mathematicians could stop sharing ideas informally if they fear AI will absorb them before publication.

Oxford’s Ursula Martin likened the release to handing the community a messy first draft and expecting it to clean up. The Institute for Advanced Study in Princeton said AI can now produce arguments that the person who prompted it can’t understand, verify or take responsibility for.

Not everyone is gloomy. Several mathematicians said their first impressions were better than they expected after earlier, sloppier OpenAI write-ups. Abhishek Saha called it a very big day for mathematics, while noting most results are strong advances within existing lines of research, not miracles. Rutgers professor Alex Kontorovich argued that skills math trains, like thinking clearly about hard problems for a long time, may become more valuable.

Partly. On September 29, an advisory group at the Institute for Advanced Study published recommendations after hearing from more than 600 mathematicians. It asked labs to stop testing advanced problems on private models, and to publish, for each result, the model name, the prompts, a summary of the reasoning, the time taken and the computing cost.

OpenAI released average computing figures and 10 abridged reasoning summaries, but no prompts, and the model remains private. An OpenAI spokesperson said the group’s advice had informed how the results were shared. MIT mathematician Andrew Sutherland said claims that a single AI agent solved problems from one prompt should be treated as unverified until people can test the model themselves. The repository also had its Issues feature switched off, giving outside researchers no obvious way to send in corrections or new formal proofs.

For working mathematicians, the practical effect is a huge, unsorted pile of claims that may affect their own projects. Some must decide whether to keep working on a problem an AI may have solved, or spend months checking a proof they didn’t write.

For everyone else, the lesson is about trust. AI systems can now produce expert-level work at a pace no human team can review. The math world is trying to build answers first, from Lean checks to new registries for machine-verified results. Expect the same debate in any field where AI output needs a human sign-off.

OpenAI says it is working to release the model responsibly, will keep adding Lean proofs, and will record corrections as new versions while keeping old ones visible. It also plans to fund workshops and conferences focused on AI-generated math. Until outside researchers can run the model themselves, many results will sit in limbo between claimed and confirmed.