OpenAI has published 722 mathematical manuscripts produced by an unreleased internal model, describing the work as the output of a largely one-prompt, single-agent process. The papers are organized into 372 families of related results, but mathematicians say the claims cannot be fully assessed until the model, prompts and additional evidence are made available.

The release arrives as AI labs increasingly use mathematics as a proving ground for frontier model reasoning, and it is shaping up as an early test of how AI-generated research should be published, checked and disclosed.

An OpenAI spokesperson said almost everything came from a single prompt given to a single AI agent, although some results may have required multiple attempts. The company said it presented the model with roughly 4,000 problems and selected the outputs it considered significant enough to publish.

Andrew Sutherland, a mathematician at MIT, told Scientific American that the one-shot claim should be treated cautiously. “Until and unless they release the model and people can replicate their results, I think you should treat any claims about one-shotting problems with a single agent as unverified,” Sutherland said. “We should ask for receipts.”

The 722 figure represents manuscripts rather than solved problems. A result family can contain a main theorem along with companion arguments, consequences or alternative proofs. OpenAI said the average result used the equivalent of roughly three hours of ChatGPT Pro thinking compute. That differs from the company’s Navier-Stokes claim last month, which involved 10,000 coordinating agents working for 88 hours.

OpenAI released abridged reasoning summaries for 10 results. However, a formalization catalog in the GitHub repository shows that only 162 of the 722 manuscripts currently include a computer-checked main result. That amounts to about 22% of the collection and means the result has been translated into Lean, software that mechanically checks each logical step. Lean has become the working standard for machine-checked proofs in mathematics, which is why the roughly 560 still-unformalized manuscripts represent the collection’s main open question.

OpenAI said not all of the manuscripts have Lean formalizations and warned that “some of the unformalized results could have issues.” A successful Lean check confirms that a proof follows from the statement as written in Lean. It does not establish that the statement corresponds to the original problem, or that the result is new or important. Those questions still require review by mathematicians.

Researchers have already raised concerns about the material and the way it was released. Dmitry Rybin wrote on X:

I was trying to read the OpenAI proof that chromatic number of a plane is >= 6. But it is totally unbelievable alien math? Somehow the model found that any K-coloring <=> "weakly measurable" K-coloring, which seems out of nowhere 1/2 pic.twitter.com/W13ScT3nel — Dmitry Rybin (@DmitryRybin1) October 7, 2026

Keith Adler wrote on X:

The openai/math repo has Issues turned off and has never accepted a pull request. That's disappointing. If you publish 722 manuscripts and ask for Lean formalisations, you need somewhere for people to send them. I'm formalising OpenAI's Saxl's Conjecture proof in Lean 4 against… — Keith Adler (@keithadler) October 7, 2026

The Institute for Advanced Study in Princeton, New Jersey, also questioned the implications of AI-generated mathematical work. “It is now the case that AI can output mathematical arguments in situations without the human who prompted it being able to understand the arguments, verify them, or take responsibility for them,” the institute said in a statement. “We believe that human understanding of mathematics remains of paramount importance. How, in this new era, can we work towards a new paradigm that includes human understanding of mathematics as part of responsible scholarly output?”

Professor Abhishek Saha took a more positive view, writing, “It is a very big day for mathematics.” He said most of the results fell into categories including “exceptional advances within existing program” and “surprising breakthroughs.” In his assessment, the collection contains interesting problems but not results comparable to the millennium problems, the Clay Mathematics Institute’s seven $1 million prize questions. He identified the Quasi-Riemann Hypothesis as the only one of the 722 that occupied that level of significance.

Saha wrote on X:

Some further thoughts on the 372 results released by OpenAI today, across 722 manuscripts. If I were to classify theorems that mathematicians prove and publish according to their groundbreaking nature, I would (very roughly) divide them into four categories: A) Non-breakthrough… — Abhishek Saha (@ObhishekSaha) October 7, 2026

The release also did not meet the recommendations issued by an advisory group at the Institute for Advanced Study on September 29. The group recommended disclosing the model’s name, the prompts, a summarized chain of thought, the time taken and the compute cost for every result. OpenAI provided average compute figures and 10 reasoning summaries, but not the prompts. The company said it is still working to release the model responsibly.

Daniel Litt, a mathematician at the University of Toronto, took the opposite position and argued that there was no reason to ask OpenAI to keep the answers to the mathematical questions secret.

Anthropic used a different approach last month when it published all 13 million lines of a Lean-checked proof of Fermat’s Last Theorem on GitHub. That work formalized a theorem published by Andrew Wiles in 1995 rather than presenting new mathematical results. The two releases illustrate a split in disclosure strategy across the industry: a complete, machine-checked proof of a known theorem on one side, and a large batch of new claims with partial formal verification on the other.

OpenAI said it would add Lean formalizations as they become available. For now, 162 of the 722 manuscripts have a formalized main result. The standing of the rest now hinges on what researchers say they need most: the model’s release, the underlying prompts, and independent formalizations of the remaining manuscripts.