🧮 An AI produces 719 novel mathematical proofs: a revolution?

An experimental artificial intelligence model has produced hundreds of mathematical research manuscripts, now accessible to specialists around the world.

On October 6, 2026, OpenAI made public a catalog of work produced with an internal model that is still experimental. The repository, hosted on GitHub, contains 719 manuscripts organized into 372 families of results. A family may bring together several proofs, alternative methods, or consequences of the same proposed discovery.

A transparent board covered with mathematical symbols and equations.

A transparent board covered with mathematical symbols and equations. Mathematical work proposed by an AI must be verified before it can be considered proven.
Photo: Preply.com Images, Creative Commons Attribution license, via Wikimedia Commons.
Wikimedia image

These documents cover very different branches of mathematics: number theory, geometry, algebra, and mathematical physics. They therefore do not resemble a series of school exercises solved automatically. Some address research problems that have been studied for many years.

How was such a large quantity of text produced? OpenAI says it submitted approximately 4,000 problems to the model during its evaluation. On average, each selected result reportedly required the equivalent of around three hours of intensive computation in ChatGPT Pro. Researchers then organized the work and its documentation to make it available for consultation.

But a manuscript is not a confirmed discovery. A proof may contain a subtle error, use an overly strong assumption, or establish a result that is already known. Specialists must therefore verify the reasoning, the scientific significance, and the novelty of each proposal.

The repository already provides a concrete example. On October 7, OpenAI removed three manuscripts after a sign error was identified in a proof. Fourteen other texts were revised to correct arguments, clarify conditions, or repair proofs. The catalog is thus presented as a collection of evolving work.

To facilitate verification, some proofs have been transcribed into Lean, a language that enables a computer to verify the steps of a formal proof. Approximately 42% of the main results currently have a formalization. This helps verify their logical consistency, but it is not enough to establish their novelty or the importance of the questions they resolve.

The key question is whether AIs can now contribute to genuine mathematical advances and then produce arguments precise enough to be examined by researchers. Open publication makes it possible to put these proposals to the scientific community for scrutiny.

OpenAI plans to add more formal proofs and organize meetings dedicated to evaluating this work. The repository also preserves the history of corrections and removals. The next independent reviews will determine which proposals withstand scrutiny and which still need to be modified.

LE
lexpert

The figure of 719 is impressive, but these are manuscripts, not 719 validated theorems. Formalization in Lean is a real asset for controlling the reasoning. It remains to be established what is truly new, which can take much longer than the generation of the texts.