README

Readme

This repository contains mathematical manuscripts and supporting proof artifacts produced by an unnamed internal OpenAI model. 

As part of model development, we evaluate our models on open research problems. We expanded these evaluations after performance on our existing mathematical evaluations saturated. Some outputs build upon earlier results produced by the models.

This collection includes results at different stages of verification. Not all have accompanying Lean formalizations. We will continue to update this repository with Lean formalizations as we obtain them. 

Some of the unformalized results could have issues. We will endeavor to fix any such issues quickly.
We are also exploring community-hosted repositories for these materials. 

In our view, these manuscripts are best understood as a form of raw research data, rather than polished academic papers. We defer to the math community completely on matters of credit, precedence, and concurrent work.

 Navigating the collection

The current catalogue contains 721 manuscripts organized into 373 families. A family groups related papers, which may include a principal result, companion arguments, consequences, or alternative proofs. Each family is classified by mathematical discipline.

- Start with the overview for descriptions of the families.
- Use the manuscript map to find individual papers and their supporting materials.
- The preprints/ directory contains PDFs, source files, and manuscript-specific citation and build instructions.
- The Lean library and formalization catalogue describe the available formal proofs, their associated papers, and verification configurations. See the Comparator instructions for additional checking instructions. The repository has ~42% top-line results formalized.
- Updates to the repo are described in the history.

 Reasoning summaries

We are also releasing abridged summaries of the model's reasoning, covering the following results:

| Family | Subject |
|---|---|
| 007 | Ordinary two-point correlations of multiplicative functions |
| 017 | The irrationality exponent of π |
| 087 | Symmetric and general Mahler conjectures |
| 102 | Ordinary NP-hardness at the basic semidefinite threshold |
| 159 | Quasipolynomial bounds for arithmetic progressions |
| 197 | Kaplansky's direct-finiteness conjecture in characteristic two |
| 221 | The Mézard–Parisi formula for diluted spin glasses |
| 271 | Spontaneous magnetization in the quantum Heisenberg ferromagnet |
| 287 | Isomorphism of free group factors |
| 362 | The three-dimensional relativistic Vlasov–Maxwell system |


 How the results were produced

The vast majority of results were obtained with the same procedure using an unreleased internal OpenAI model. On average, each result used three hours of ChatGPT Pro thinking compute with that model. Over the course of the evaluation, the model was posed approximately 4,000 problems. Aggregating the output into result families and manuscripts and requiring