On October 6, OpenAI pushed 719 mathematical papers produced by an unreleased internal model to GitHub. The release came one week after its own advisory body called on AI laboratories to stop testing advanced mathematics problems on proprietary models. The week-apart sequence frames the tension now running through AI-driven mathematics research: laboratories use open problems to measure model progress, while parts of the mathematical community press for disclosure and conventional peer review before AI-generated results circulate.

Over 600 survey responses shaped the IAS panel's September 29 guidance

The Advisory Group on Mathematics and Artificial Intelligence, based at the Institute for Advanced Study in Princeton, New Jersey, published its recommendations on September 29, drawing on more than 600 survey responses. "We want to state clearly from the start: we do not endorse this practice, and we ask them to stop testing advanced mathematical problems on proprietary models," the group wrote in its guidance.

The same document warns that privately held internal models risk creating a two-tier system in which a handful of laboratories outr the rest of the field.

According to its repository, OpenAI tests its models on open research problems as part of model development, and it extended those tests after its existing math benchmarks became saturated — the point at which models score at or near the top of current tests. The company said it conferred with the advisory group and drew on its recommendations for the release. In a statement issued October 6, the group said its advisory role does not constitute "an endorsement of the process by which OpenAI obtained them," and it left the verdict on compliance to the wider mathematical community.

The Navier-Stokes Lean code proves weaker claims than the written paper

OpenAI organized the 719 papers into 372 mathematics families, each built around a main result and its related proofs. The proprietary model was given roughly 4,000 problems, and each result required about three hours of ChatGPT Pro thinking compute on average.

The advisory group has asked AI laboratories to publish, for each result, the model name, the prompts used, a summarized chain of thought, the time taken, and the compute cost. OpenAI published 10 reasoning summaries, and about 42% of its top-line results carry Lean formalizations. How closely the release matches that per-result checklist is among the questions the group has left for the mathematical community to settle.

Lean is a programming language that allows a computer to check a proof. If the code compiles, that does not mean the code and the written argument are identical; it only establishes that the formal statement is true. Converting written arguments into machine-checkable code this way is what researchers call autoformalization.

That gap was examined in a paper posted on October 6 by Alexander Bastounis, Fabian Circelli, and Anders C. Hansen. They find that OpenAI's written Navier-Stokes paper makes stronger claims than what its Lean code proves, with one estimate changing the order of the input derivatives. The authors also detected similar mistranslations in OpenAI's Euler proof, writing that OpenAI's written proof and other autoformalized Lean proofs "should not prima facie be trusted without the same peer review process and scrutiny that other proofs are subjected to."

OpenAI announced the Navier-Stokes result on September 8. The equations are the subject of one of the Clay Mathematics Institute's Millennium Prize Problems, each of which carries a $1 million prize. NYU mathematician Tristan Buckmaster subsequently disputed the company's description of the minimal human input involved in the work, as Cryptopolitan reported. The company has pledged funding for workshops, conferences, and special programs tied to major AI results. On October 6, mathematician Terence Tao wrote that people who prompt AI systems often solve problems and then lose interest in the field, adding that many cannot answer questions or give talks on the resulting work; his post did not name OpenAI.

The company has said its advisers have no say over the pace of its research, Cryptopolitan reported in September. With the compliance verdict now in the mathematical community's hands, the markers to watch are whether peer review upholds or challenges the written-to-Lean translations, and whether future releases itemize the disclosures — model name, prompts, summarized chains of thought, timing, and compute cost — the group has asked of every result.