Mathematical manuscripts and supporting proof artifacts produced by OpenAI

A publicly available repository collects 722 mathematical manuscripts organized into 372 families, together with supporting proof artifacts such as PDFs, source files, build instructions, a manuscript map, and a Lean formalization library. Families group related papers that may include principal results, companion arguments, consequences, or alternative proofs; an overview and catalog guide navigation. The project also publishes abridged reasoning summaries for a selection of notable results - examples include ordinary two-point correlations of multiplicative functions, the irrationality exponent of π, Mahler conjectures, NP-hardness at a semidefinite threshold, quasipolynomial bounds for arithmetic progressions, Kaplansky’s direct-finiteness in characteristic two, the Mézard-Parisi formula, spontaneous magnetization in the quantum Heisenberg ferromagnet, isomorphism of free group factors, and a three-dimensional relativistic Vlasov-Maxwell result.

Most results were produced by a single internal, unreleased OpenAI model using a standardized workflow: roughly three hours of ChatGPT Pro thinking compute per result and about 4,000 posed problems aggregated into substantive families. Verification status varies - many manuscripts have accompanying Lean proofs, others are unformalized or at intermediate verification stages - and some unformalized items may contain errors that will be corrected. A few exceptions to the standard procedure (notably work on a Riemann zeta zero-free region and a Hodge Conjecture writeup) received specialized handling. The collection is versioned, citable via local BibTeX entries, and released under an Apache-2.0 license.