OpenAI’s AI Math Proofs Raise Concerns Over Verification and Research Standards

OpenAI’s release of hundreds of AI-generated mathematical proofs has raised concerns among researchers about verification, transparency and whether the results meet established academic standards. Although the company consulted an independent mathematical advisory group before publication, several aspects of its release fall short of the group’s recommendations.

Published October 6, the collection contains 719 manuscripts covering 372 groups of mathematical results. OpenAI made the papers available in its public GitHub repository, along with supporting material and some machine-checked proofs, but much of the work still requires independent assessment.

OpenAI’s Math Proofs Face Questions Over Verification

The Advisory Group on Mathematics and Artificial Intelligence (AGMAI), based at the Institute for Advanced Study in Princeton, published research publication guidelines on September 29. The nine-member group urged AI laboratories to prioritise human understanding, independent verification and transparent disclosure when presenting mathematical discoveries.

One recommendation explicitly discouraged companies from testing advanced mathematical problems using proprietary AI models unavailable to researchers. OpenAI nevertheless generated its latest results with an unreleased internal model and acknowledged that evaluating such models on open mathematical problems remains part of its research.

The company followed some recommendations by promptly publishing manuscripts, documenting its research process, and providing formalised proofs. However, it formalised only about 42% of its main results in Lean, and the release included just 10 summaries of the model’s reasoning rather than documentation for every manuscript.

AGMAI also recommended disclosing the models, prompts, computation costs, and the reasoning behind the results. OpenAI provided estimated computing requirements and information about its evaluation process but did not fully disclose the proprietary model or its individual reasoning process for every result.

Researchers Identify Discrepancies in Lean Proofs

Separate research published October 6 examined problems that can arise when researchers translate AI-generated mathematical arguments into Lean, a formal programming language used to verify proofs. The paper, written by Alexander Bastounis, Fabian Circelli, and Anders C. Hansen, identified discrepancies in OpenAI’s previously announced work on the Navier-Stokes equations.

The researchers found that parts of the formalised Lean argument did not faithfully represent the corresponding natural-language proof. In one example, the Lean code established a result under stronger assumptions than those stated in the written mathematical argument.

Such differences matter because a successful Lean verification establishes the validity of the formal statement being checked, not necessarily the correctness of every claim or intermediate argument in the original paper. The researchers emphasised that their findings do not establish whether OpenAI’s natural-language proof is correct or incorrect.

The study reinforces AGMAI’s recommendation that AI laboratories provide machine-readable information connecting natural-language mathematical arguments with their formalised versions. It also supports continued human review rather than treating successful code verification as sufficient evidence that an entire mathematical manuscript is reliable.

Mathematicians Call for Greater Human Understanding

Prominent mathematician Terence Tao has raised concerns about AI-generated solutions being released without researchers who fully understand the underlying mathematics. He warned that people prompting models to solve difficult problems may be unable to explain the resulting arguments, answer technical questions or participate in the academic discussions needed to establish their significance.

AGMAI has emphasised that mathematical discoveries require more than producing a seemingly valid proof. Researchers must examine the reasoning, identify connections with existing work and determine how new results can contribute to further mathematical understanding.

The advisory group recommended that AI companies provide financial and institutional support for mathematicians undertaking this work, including workshops, research programs and other scholarly activities. OpenAI said it plans to fund conferences, workshops, and special programs focused on understanding important AI-generated mathematical results.

In its response, AGMAI acknowledged OpenAI’s engagement but declined to endorse the findings or declare that OpenAI had met its recommendations. The group maintained that assessing the results and determining their mathematical significance remains the responsibility of the wider research community.

OpenAI has acknowledged that some results without formal verification may contain errors and says it will continue updating the collection. The outstanding task is not simply to check whether the proofs are computationally valid, but to establish whether their arguments can withstand independent scrutiny and become part of mathematics that researchers understand and can build upon.