OpenAI releases 722 math papers generated by unreleased internal AI

On Tuesday, October 6, OpenAI made public a collection of 722 mathematical papers produced by an artificial intelligence model that is not yet available to the public. The documents were published on GitHub, along with materials that allow for the examination of the presented proofs.

The collection is organized into 372 groups of related results, which may include a main theorem, corollaries, or alternative proofs. The evaluation of the papers involved approximately four thousand problems. The company cautions that the manuscripts are at different stages of verification, and some results that have not yet been formalized may contain errors.

Verification and formalization in Lean

Some of the proofs were expressed in Lean, a programming language combined with a proof assistant that enables computers to verify the validity of mathematical arguments. In this process, the proof is written in a formal language, with definitions and steps that the system can check to ensure that the conclusion follows from the premises and the rules used.

OpenAI said it will continue to add new formalizations to the repository as they are created, while keeping previous versions accessible and recording corrections. Verifying proofs is considered crucial for advancing artificial intelligence in mathematics, as confirming the correctness of a proof and understanding the underlying ideas are distinct tasks in scientific work.

Recommendations from the Mathematics and AI Advisory Group

The disclosure was guided by the Mathematics and Artificial Intelligence Advisory Group, an independent committee based at the Institute for Advanced Study. In recommendations published on September 29, the group argued that laboratories should share relevant findings with detailed documentation, references, information about the process, and formalized proofs whenever possible.

The document also called for resources to be allocated to enable researchers to understand and incorporate the results, with initiatives led by the mathematical community. However, the group does not endorse the practice of testing advanced problems on inaccessible proprietary models and calls on laboratories to stop this approach.

For committee members, the ability of machines to produce arguments does not eliminate the need for human understanding, collaborative verification, and accountability for published content.

Context and implications

Each published result required, on average, an amount of computation equivalent to approximately three hours of reasoning by ChatGPT Pro. The company says it is working to make the model publicly available and will fund workshops, conferences, and programs dedicated to analyzing the results.

The initiative marks a significant milestone in the interaction between artificial intelligence and mathematical research, but also raises questions about the reliability of proofs generated by opaque systems and how best to integrate these advances into traditional scientific work.