OpenAI's math proofs don't yet meet mathematicians' standards

OpenAI released hundreds of claimed solutions to hard math problems, 719 manuscripts in all, and said it had consulted an advisory group first to avoid the backlash that followed an earlier model's work on a famous problem. TechCrunch reports that the release still fell short of what that group had asked for.

The Advisory Group on Mathematics and Artificial Intelligence, hosted at Princeton's Institute for Advanced Study, published guidelines in late September. One recommendation was to stop testing advanced math on proprietary models, yet OpenAI evaluates its proprietary models on open problems. The group also asked for machine-readable metadata linking each natural-language proof to its formal version, and OpenAI did not provide it. Only 10 of the 719 manuscripts came with chain-of-thought traces. Mathematicians at Cambridge and King's College London found at least two discrepancies between OpenAI's natural-language proof and its Lean code for a problem derived from the Navier-Stokes equations. The gaps do not disprove the solution, but they raise doubt about models formalizing their own proofs with no human in the loop.

The sharper objection is about understanding, not correctness. Terence Tao has criticized problem-solving by people who lose interest once something is "solved" and cannot discuss the output with the field. Melanie Wood, a Harvard mathematician, put it plainly: at release there is no human understanding of these solutions, and "now the work begins."

Why it matters

If you are tempted to treat a model's proof as settled because it compiles or reads well, the Lean discrepancies are a warning. A result becomes trustworthy only once a mathematician has understood it, and for these 719 manuscripts that work has barely started.