Overview
- OpenAI posted 722 manuscripts grouped into 372 result families on GitHub on Tuesday, Oct. 6, drawn from an internal, unreleased model that was given roughly 4,000 research problems.
- Many papers include Lean formalizations that check logical steps, but OpenAI says many of those Lean files were themselves written by AI and are marked 'unchecked', so experts must still confirm the formal statements match the intended mathematics.
- OpenAI disclosed compute details that show an average of about three hours of ChatGPT Pro‑equivalent 'thinking' compute per result and released short reasoning summaries for ten families, while withholding the frontier model, full prompts, and detailed chains of thought.
- The release has intensified disputes over credit and data provenance, revived complaints from prominent mathematicians including a letter from 25 Fields Medal winners, and prompted calls for independent peer review and formal community repositories.
- OpenAI says it consulted an Institute for Advanced Study advisory group, will fund workshops to help verify major results, and the flood of machine‑generated output is already spurring discussion about how peer review, attribution and careers in mathematics must adapt.