Mathematicians are questioning whether OpenAI's 719 AI-generated math manuscripts can be trusted, after a paper said the company's earlier Navier-Stokes proof does not match its computer-checked version.
Key Points:
- OpenAI's catalogue shrank from 722 to 719 manuscripts after the company pulled three papers over a sign error.
- Three U.K.-based mathematicians documented two places where the written Navier-Stokes proof and its Lean code diverge.
- The authors do not call the proof wrong, but say machine checks cannot replace peer review.
OpenAI Math Release
The company posted the collection on Oct. 6, and a report published Thursday found that it strayed from guidelines an independent panel of mathematicians wrote for AI labs. The catalogue opened with 722 manuscripts. OpenAI withdrew three of them a day later, after a sign error broke one argument and two papers that relied on it.
Those guidelines, issued Sept. 29 by the nine-member Advisory Group on Mathematics and Artificial Intelligence, open with a request that labs stop testing advanced math problems on proprietary models. OpenAI's repository says the papers came from evaluating an unreleased internal model on open research problems.
Summaries of the model's reasoning accompany only 10 results, and about 42% of the top-line results have been formalized in Lean, a programming language that lets a computer check a proof.
Also Read: How Much Does Anthropic's CEO Make? IPO Filing Has The Answer
Navier-Stokes Proof Gaps
Alexander Bastounis of King's College London and Fabian Circelli and Anders Hansen of the University of Cambridge examined the Navier-Stokes proof that OpenAI announced in September. They documented two places where the written argument and the Lean code diverge, including one where the code proves a weaker estimate than the paper states.
The authors said they make no claim about whether the written proof is correct. Their point is narrower. Lean confirms that the final theorem holds, they wrote, but it cannot show that the intermediate steps a human reads are sound, so such proofs still need peer review.
Fields Medalist Terence Tao wrote on Oct. 6 that problems are being solved by "AI prompters" who do not understand the output well enough to answer questions or give talks on it. Harvard professor Melanie Matchett Wood, a member of the advisory group, said no human understands such results when they are released, "and now the work begins."
OpenAI Proof Dispute
The advisory group has said only the wider mathematical community can judge how closely OpenAI followed its recommendations. That scrutiny follows a tense month. OpenAI announced the Navier-Stokes result on Sept. 8, which set off a credit dispute with New York University mathematician Tristan Buckmaster, and 25 Fields Medalists launched a declaration three days later warning that mass-produced AI results could harm the field.
Read Next: OpenAI's 722 AI Math Papers Are Public, Now Mathematicians Must Judge Them
