OpenAI Math Release Omits Several Details Recommended by AGMAI

OpenAI’s latest release does not disclose several details recommended by the Advisory Group on Mathematics and Artificial Intelligence (AGMAI), including information that would help readers connect explanations with machine-checked proofs.

OpenAI released the results Oct. 6 from an internal frontier model. The publication includes Lean formalizations for many proofs, details about the research process, 10 summaries of model reasoning, computing-time estimates and statistics on attempted problems. OpenAI said the average result used computing equivalent to roughly three hours of ChatGPT Pro thinking.

AGMAI published its recommendations Sept. 29 after more than 600 survey responses. The group calls for laboratories to identify the model used for each result and disclose prompts, summarized reasoning, time taken and estimated computational cost.

The recommendations also call for formalizing proofs where possible and adding machine-readable metadata that links natural-language explanations with formal proof artifacts. The announcement does not state the total number of manuscripts, the number containing reasoning summaries or the percentage of proofs that were formalized.

The release’s treatment of the Navier-Stokes work highlights the verification challenge. A paper by Alexander Bastounis, Fabian Circelli and Anders C. Hansen identified discrepancies between OpenAI’s natural-language proof and its Lean formalization, including a different derivative order in one estimate. The authors did not determine whether the underlying mathematical result was correct.

Lean is a programming language for expressing mathematical statements and proofs in a form that computers can check. Successful compilation verifies the formal statement encoded in the code, but it does not by itself prove that the code faithfully represents the accompanying natural-language explanation.

OpenAI previously disclosed a result involving finite-time singularities in the Navier-Stokes equations, which describe fluid motion, along with a Lean-checked formalization. Its public repository contains Lean formalizations for the Navier-Stokes and Euler results.

AGMAI has not issued a final pass-or-fail assessment of the latest release. The group said Oct. 6 that the mathematical community must determine how fully the recommendations were followed.

The recommendations also call for peer review, independent verification, documentation of AI use and placement of results in scholarly repositories outside the control of AI laboratories. The release follows OpenAI’s earlier publication of AI-generated math manuscripts, which prompted debate over disclosure and independent review.

OpenAI will fund workshops, conferences and special programs focused on understanding major results produced by AI.