OpenAI's Math Proof Release Draws Scrutiny Over Human Understanding

OpenAI released hundreds of claimed solutions to hard math problems this week, drawing criticism from mathematicians for not meeting standards on human understanding and formalization. The release explicitly says the company is evaluating its proprietary models using open research problems in mathematics.

OpenAI said it consulted an advisory group of elite mathematicians to avoid the controversy from a previous model solving a long-standing problem. However, the Advisory Group on Mathematics and Artificial Intelligence (AGMAI) said OpenAI fell short of its standards, especially on the need for human understanding of mathematical results.

AGMAI's first request was for labs to stop testing advanced math problems on proprietary models. Just 10 of the 719 manuscripts OpenAI released included the model's chain of thought, according to TechCrunch.

A new paper by mathematicians at the University of Cambridge and King's College London documents at least two discrepancies between the natural language proof and the Lean code behind OpenAI's solution to a problem derived from the Navier-Stokes equations. Terence Tao wrote on social media that problems are being solved autonomously by AI prompters who do not understand the AI output well enough to answer questions, give talks, or interact with the field.

In late September, AGMAI released guidelines for frontier labs solving math problems. OpenAI previously faced controversy when one of its models solved a long-standing problem in the field.