OpenAI released hundreds of purported solutions to difficult mathematical problems this week, in an attempt to demonstrate its models’ ability to handle advanced problems. But the release did not fully comply with the guidelines set by an advisory group of mathematical researchers, reopening the fundamental question: Is it enough for models to produce a solution that can be expressed computationally, or must it also be understandable and auditable by mathematicians?
The Advisory Group on Mathematics and Artificial Intelligence (AGMAI) comprises nine prominent researchers and is hosted by the Institute for Advanced Study at Princeton University. At the end of September, the group published guidelines for laboratories developing advanced models to solve mathematical problems.
Partial compliance with the researchers’ guidelines
AGMAI noted that assessing compliance with its recommendations ultimately belongs to the mathematical community. Among its most prominent recommendations is to stop testing advanced mathematical problems on commercially owned models, while OpenAI explicitly stated that it uses open research problems to evaluate its own models.
OpenAI followed some of the principles, such as publishing the results quickly and providing information about how the models reached their conclusions. However, only 10 of the 719 manuscripts included the model’s chains of thought. In addition, 42% of the published proofs had not undergone formalization.
The group believes that proofs that are difficult for humans to understand should be converted into a formal format. But it also emphasized the laboratory’s responsibility to ensure that the release of results is accompanied by human understanding of them, and suggested funding mathematicians to help make these results genuinely meaningful from a scientific perspective.
A gap between natural language and Lean code
Models typically begin by generating an explanation in natural language, then attempt to convert it into Lean, a programming language whose compiler can confirm the consistency of a proof in an executable format. However, automated conversion can change the substance of a proof or create a disconnect between what the explanation says and what the code proves.
A paper published by mathematicians from the University of Cambridge and King’s College London documented at least two differences between a natural-language proof and the Lean code associated with a solution OpenAI provided to a problem derived from the Navier-Stokes equations concerning the behavior of complex fluids. These differences do not necessarily prove that either solution is wrong, but they raise doubts about allowing models to formally formulate their solutions without human intervention.
AGMAI also requested the inclusion of machine-readable metadata linking the textual proof to the formal version, which OpenAI did not provide in these releases. The paper’s authors, known as “lost in translation,” concluded that textual proofs and automatically converted Lean proofs should not initially be accepted without peer review and scrutiny comparable to that applied to other proofs.
Why does this matter?
The issue is not merely about proving that the code compiles successfully, but about proving that the code actually represents the mathematical idea explained by the text. In traditional research, scientists bear responsibility for their results and discuss them through papers, lectures, and seminars, a process that helps uncover errors and understand reusable methods.
When models produce a solution to a difficult problem, however, this human understanding may not be available at the time of publication. Therefore, OpenAI’s current results appear closer to the beginning of the scientific verification process than to the end of the problem; human review and linking the textual and formal outputs remain outstanding requirements before these proofs can be accepted within the mathematical community.