OpenAI recently released hundreds of proposed solutions to some of the world’s most challenging mathematical problems, saying it had consulted an advisory group of leading mathematicians to help ensure its work met the standards of the mathematical community.

 

However, questions remain about whether the release fully meets those standards—particularly the importance of human understanding and independent verification of AI-generated mathematical results.

 

The Advisory Group on Mathematics and Artificial Intelligence (AGMAI), hosted by Princeton University’s Institute for Advanced Study, consists of nine prominent mathematicians and researchers from institutions around the world. In September, the group published guidelines for frontier AI labs working on advanced mathematical problems.

 

Following OpenAI’s latest release, AGMAI said that the mathematical community ultimately needs to determine how closely the recommendations were followed.

 

One major recommendation was to avoid testing advanced mathematical problems exclusively on proprietary AI models. OpenAI, however, said it was evaluating its proprietary models using open research problems in mathematics.

 

OpenAI did follow some of the group’s recommendations, including releasing results quickly and providing information about how its models reached their conclusions. But questions remain about transparency: only 10 of the 719 manuscripts included the model’s chain-of-thought information.

 

Another concern involves formal verification. For mathematical proofs that humans cannot easily understand, AGMAI recommended formalizing the proofs so their correctness can be independently checked. Yet only around 42% of OpenAI’s released proofs had undergone this process.

 

This raises a broader question: Can AI-generated mathematical discoveries be trusted without sufficient human involvement and understanding?

 

The issue became more significant after researchers from the University of Cambridge and King’s College London published a paper examining discrepancies between AI-generated mathematical explanations and their corresponding formal proofs.

 

AI systems often produce a mathematical solution in natural language and then attempt to translate it into Lean, a formal programming language used to verify mathematical proofs computationally.

 

Researchers identified at least two discrepancies between the natural-language explanation and the Lean code associated with an OpenAI solution to a problem derived from the Navier-Stokes equations, which describe complex fluid behavior.

 

The discrepancies do not necessarily prove that the underlying mathematical result is incorrect. However, they highlight the possibility that an AI system could introduce errors while translating its own reasoning into a formal proof.

 

This is why independent human review remains important.

 

Prominent mathematician Terence Tao has also raised concerns about AI-generated mathematical work, arguing that some AI-assisted solutions are produced without researchers developing enough understanding of the underlying results to explain, defend, or build upon them.

 

Traditionally, when mathematicians discover important new results, they take responsibility for the work and engage with the broader community through papers, presentations, seminars, and peer review. This process helps validate the result, improve understanding, and uncover techniques that can be applied to other problems.

 

AI-generated mathematics introduces a different challenge. A model can produce a potentially groundbreaking solution in seconds, but human understanding may only begin after the AI has produced the result.

 

The key question is therefore not simply whether AI can solve difficult mathematical problems, but whether mathematicians can independently verify, understand, and build upon those solutions.

 

For AI-driven mathematics to become genuinely transformative, generating an answer may be only the first step. Reliable verification, transparency, and human understanding will be equally important.