OpenAI's recent math proof releases fall short of advisory group guidelines
OpenAI disclosed hundreds of AI-generated mathematical proofs, but an expert advisory panel says the lab did not fully meet recommended standards for human verification and formalization.
OpenAI announced the release of 719 AI-generated manuscripts that claim solutions to a range of challenging mathematical problems. The papers were evaluated by the Advisory Group on Mathematics and Artificial Intelligence (AGMAI), a panel of nine senior researchers hosted by Princeton University’s Institute for Advanced Study.
AGMAI’s September guidelines advise frontier labs to halt testing advanced problems on proprietary models and to ensure that any released results are accompanied by clear human-understandable explanations and formal verification. While OpenAI provided some information about model reasoning, only ten of the manuscripts included a detailed chain-of-thought, and just 42% of the proofs were formally verified in the Lean proof language.
"Problems are being solved autonomously by AI prompters who have no interest in the broader field itself once their initial target is ‘solved’, and do not understand the AI output well enough to answer questions on the result, give talks, or otherwise interact with the rest of the field," wrote mathematician Terence Tao on social media.
A recent study by researchers at the University of Cambridge and King’s College London identified mismatches between natural-language explanations and the corresponding Lean code for a problem related to the Navier-Stokes equations, highlighting the risk of mistranslations when models auto-formalize proofs. The authors concluded that such automatically generated proofs should not be trusted without the same peer-review scrutiny applied to traditional results.
AGMAI noted that the responsibility for ensuring human comprehension of AI-generated proofs remains with the mathematical community and suggested that OpenAI fund human mathematicians to validate and contextualize the findings. Harvard mathematics professor Melanie Wood emphasized that, unlike human-derived results, AI-produced solutions often lack immediate human understanding, requiring additional work after release.