When OpenAI released hundreds of manuscripts this week claiming solutions to difficult mathematical problems, the lab said it had consulted an advisory group of prominent mathematicians to avoid controversies that followed its previous high-profile claims. Still, critics say the releases fell short of the advisory group's standards—especially regarding human understanding of mathematical results.
AGMAI guidance and OpenAI’s disclosures
The Advisory Group on Mathematics and Artificial Intelligence (AGMAI), hosted by the Institute for Advanced Study at Princeton University, comprises nine noted researchers from institutions around the world. AGMAI published guidelines at the end of September on how frontier labs should approach mathematical problems. In a statement about OpenAI’s recent bundle of proofs, AGMAI said that "it is ultimately up to the mathematical community to assess the extent to which our recommendations were followed successfully."
One of AGMAI’s first requests was that labs stop testing advanced mathematical problems on proprietary models. OpenAI’s release explicitly states it is evaluating its proprietary models on open research problems in mathematics, which runs contrary to that recommendation.
Numbers: 719 manuscripts, few chains of thought, and incomplete formalization
OpenAI made 719 manuscripts public. While the lab followed some AGMAI principles—such as publishing results quickly and sharing information about how models reached conclusions—implementation was incomplete. Only 10 of the 719 manuscripts included the model’s chain-of-thought traces.
AGMAI and other mathematicians also urged that proofs which are not humanly comprehensible be formalized into machine-checkable form. According to OpenAI’s release data, 42% of the proofs had not undergone such formalization, meaning formal verification was missing for a substantial portion of the material.
"Lost in translation": mismatches between natural-language proofs and Lean code
A paper published this week by mathematicians at the University of Cambridge and King’s College London highlights problems with the way frontier labs are approaching these tasks. Typically, AI models produce a natural-language (NL) explanation of a result and then attempt to express that reasoning in Lean, a formal language that can be compiled and checked as code.
The Cambridge–King’s paper documents at least two discrepancies between the NL proof and the Lean code underlying OpenAI’s solution to a problem derived from the Navier–Stokes equations governing fluid behavior. Those discrepancies do not automatically invalidate either artifact, but they raise doubts about relying on models to autoformalize their own solutions without human oversight.
AGMAI had asked OpenAI to include machine-readable metadata linking natural-language and formal artifacts; OpenAI did not provide such metadata in these releases. The Cambridge–King’s authors conclude that because of mistranslations, "the NL proof by OpenAI and other autoformalised Lean proofs should not prima facie be trusted without the same peer review process and scrutiny that other proofs are subjected to."
Responsibility, community engagement, and the human role
Mathematicians note that when humans discover new results, they take responsibility for them and engage the community through papers, talks, and seminars. That engagement increases understanding, reveals techniques applicable to other problems, and enables practical applications.
Terence Tao, who has previously criticized OpenAI’s approach, wrote on social media that 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."
Melanie Wood, professor of mathematics at Harvard University, told TechCrunch that when a model is prompted to solve a hard problem and outputs a solution, "there is not human understanding of them at the point of release, and now the work begins." In other words, significant human effort is required after publication to verify, interpret, and integrate these results into the mathematical community.
Implications and recommendations
The episode shows that while AI models can generate sophisticated candidate solutions, scientific acceptance depends on formalization, transparency (including chain-of-thought traces and linking metadata), and human mathematicians taking responsibility for understanding and validating results. AGMAI recommended that OpenAI help fund the work of human mathematicians needed to make the lab’s solutions meaningful in practice.
For now, a gap remains between the technical capabilities demonstrated by the models and the procedural, social, and epistemic requirements of mathematical practice—especially when mismatches arise between informal and formalized proofs. AGMAI, independent researchers, and the broader mathematical community will need to review the materials and determine to what extent the publications advance reliable mathematical knowledge.
