OpenAI’s math proofs fall short of researchers’ guidelines

OpenAI released 719 manuscripts containing claimed solutions to difficult mathematical problems. The company said it consulted an advisory group of mathematicians after controversy over a previous model result. But the group’s recommendations called on frontier labs to stop testing advanced problems on proprietary models, while OpenAI said it was evaluating its proprietary models on open research problems.

The Advisory Group on Mathematics and Artificial Intelligence (AGMAI), hosted by the Institute for Advanced Study in Princeton, published its guidelines at the end of September. It said the mathematical community would ultimately assess whether its recommendations were followed. The group did not respond to TechCrunch’s request for a fuller evaluation.

OpenAI shared information about how its models reached conclusions, but only 10 of the 719 manuscripts included the models’ chain of thought. AGMAI also recommended formalizing proofs that people do not understand; 42% of OpenAI’s released proofs had not been formalized. The group called for machine-readable metadata linking natural-language explanations with formal proofs, which the releases did not include.

A separate paper by mathematicians at the University of Cambridge and King’s College London identified at least 2 discrepancies between an OpenAI natural-language proof and its Lean code for a problem derived from the Navier-Stokes equations. The authors said the discrepancies did not necessarily disprove either solution, but argued that such proofs need peer review. Harvard mathematics professor Melanie Wood told TechCrunch that human understanding was absent when the solutions were released, and that “now the work begins.”