OpenAI Math Repository: AI Proofs, Lean Formalization, and 4000 Problems

I. Background: How to View AI-generated Mathematical Achievements

In October 2026, OpenAI publicly released the openai/math repository on GitHub. The repository contains not training code or model weights, but mathematical manuscripts and Lean formal proofs generated by internal advanced models. OpenAI’s rationale is to share the results produced by models during internal evaluations with the academic community for digestion. This move is seen as an example of “AI accelerating science” as well as a question about “publishing unpeer-reviewed results.”

II. Technical Principles: What Lean Formalization Can and Cannot Do

The core technology in the repository is Lean 4, an interactive theorem proving language based on dependent type theory. It allows mathematical propositions to be written as formal code and enables computers to check each step of the proof for validity. In other words, as long as the Lean check passes, the proof is error-free at the formal level.

However, formal correctness does not equate to mathematical insight. Lean can only verify whether “the reasoning from A to B is rigorous,” but cannot determine “whether the theorem is important.” A formally correct proof may simply repeat itself or use simple combinations of existing conclusions. Therefore, the value of Lean formalization lies in “guaranteeing no errors” rather than “automatically discovering new mathematics.”

The manuscripts in the repository cover fields such as harmonic analysis, complexity theory, and quantum field theory. OpenAI stated that about 4,000 questions were posed during evaluation, and only some results and formal proofs were released. In other words, this is a subset selected from the output of numerous models.

III. Key Data and Repository Structure

According to public information, the repository mainly includes the following:

• lean/ directory: Lean 4 formal proofs.
• Mathematical manuscripts: Model outputs stored in PDF or Markdown format.
• Reasoning summaries: OpenAI has published 10 model reasoning summaries to show how the models think.
• Computational cost estimates: Based on ChatGPT Pro usage, these provide an approximate cost of the models’ problem-solving.
• Attempt statistics: Records the distribution of the number of problems attempted by the models.

Some media reports claim that the repository contains approximately 722 mathematical manuscripts, but OpenAI did not specify this number in the repository README, so it can only be used as “reported” information.

IV. Value: What It Changes

First, it makes the process of AI-generated results transparent. In the past, model outputs were often only presented as final answers in papers; now, researchers can see the original manuscripts, reasoning processes, and formal code. Second, it provides academia with a new “pool of materials for review.” Mathematicians can choose topics they are interested in to verify, rather than passively waiting for publication. Finally, it promotes the popularization of “formalized mathematics.” More researchers may become familiar with Lean through this repository, thereby improving the level of formalization in the entire field.

V. Controversies and Risks

The biggest controversy lies in academic attribution and verification responsibility. OpenAI claims not to seek academic honors, but this does not solve the issue of “who will be responsible for errors.” If a proof that passes the Lean check later reveals that it uses invalid premises, who is responsible: OpenAI, the model, or the verifier?

The next issue is reproducibility. Results generated in the repository by an unnamed internal OpenAI model cannot be replicated by outsiders. This means researchers can only verify the final outputs, but cannot determine how the model arrived at these results.

Thirdly, there is misalignment in incentives. Formal verification is a time-consuming and labor-intensive task, but under OpenAI’s model, the academic rewards for validators are unclear. In the long term, only a few volunteers may be willing to invest.

VI. Conclusion and Outlook

openai/math is an experimental infrastructure. It demonstrates that AI models can produce formal mathematical content in bulk, but it also exposes institutional gaps in the current academic system when receiving such content. In the short term, its most valuable use may be as practice material for Lean exercises and research clues. In the medium term, if OpenAI can disclose more details about generation and evaluation protocols, its credibility will greatly increase. In the long term, for AI-generated results to be accepted by the academic community, four core issues must be addressed: attribution, verification, incentives, and reproducibility. Otherwise, it will be more like a “wholesale market for mathematical results” rather than true collaboration among scientific communities.