OpenAI Releases Math Manuscript Repo: 719 Results, ~42% Lean-Formalized
OpenAI open-sourced 719 AI-generated math manuscripts, with about 42% of top-line results accompanied by machine-verifiable Lean 4 proofs.
ImportanceMaterialEvidenceE3 inspectableWrite-upQuick
OpenAI released the openai/math repository on GitHub on October 6, publishing 719 mathematical manuscripts generated by an unreleased internal model.
The manuscripts are organized into 372 result families across 17 fields including number theory and geometry. Each family groups principal results with companion arguments or alternative proofs.
According to the README, approximately 42% of top-line results have been formalized in Lean 4, making them machine-verifiable. Unformalized results may contain errors, which OpenAI states it will fix and update over time.
The archive uses the Apache-2.0 license and aims to provide reproducible evidence of AI-generated mathematical conclusions, though not all results have undergone peer review or full verification.