OpenAI fell short of the mathematical community's standards when it released hundreds of claimed solutions to hard math problems this week, failing to meet guidelines set by an advisory group of elite mathematicians. The Advisory Group on Mathematics and Artificial Intelligence (AGMAI) stated that it is up to the mathematical community to assess OpenAI's compliance, noting that the lab tested advanced problems on proprietary models despite a request to stop. Furthermore, only 42 percent of the proofs were formalized, and just 10 of the 719 manuscripts included the model's chain of thought, while human understanding and machine-readable metadata correlating natural language to formal artifacts were largely missing.
A new paper by mathematicians at the University of Cambridge and King's College London highlighted concerning gaps between natural language and formally expressed solutions in an OpenAI-solved problem derived from the Navier-Stokes equations. The models translate natural language proofs into the Lean programming language, but researchers found discrepancies that question whether we can rely on models to formalize their own solutions without human involvement. Prominent mathematician Terence Tao criticized the approach on social media, pointing out that AI prompters solve problems autonomously without understanding the output well enough to interact with the rest of the field.
This matters because the mathematical community demands human understanding and rigorous verification for AI-generated proofs of complex problems, highlighting the growing friction between frontier labs and traditional scientific standards.