openai/math: 722 AI-generated mathematics manuscripts (GitHub repository)
B · Useful, limited Primary OpenAI release of AI-generated mathematics with a stated production procedure, but self-reported, only partly formalised in Lean and without independent review at release.
Summary based on the abstract only·Original: about 5 minutes to read
In short
OpenAI's public GitHub repository "openai/math" holds mathematical manuscripts and proof artifacts produced by an unreleased internal model. OpenAI says it began posing open research problems after its existing math evaluations saturated. This digest is based on the repository README, not on the manuscripts themselves. The scale is the news: hundreds of claimed results across many fields, released at different stages of verification.
Key numbers
- 719manuscripts in the catalogue, organised into 372 families (README at time of reading)
- ~4,000open problems posed to the internal model over the evaluation
- 3 hoursaverage ChatGPT Pro thinking compute per result
- ~42%share of top-line results formalised in Lean
As reported by the source.
English·Web page·opens github.com
What it reports
- The README lists 719 manuscripts in 372 families (the Library title says 722); a family groups a principal result with companion arguments, consequences or alternative proofs, classified by discipline.
- The model was posed approximately 4,000 problems; results used on average three hours of ChatGPT Pro thinking compute each.
- About 42% of top-line results have Lean formalisations; OpenAI says unformalised results "could have issues" and will be fixed.
- Abridged reasoning summaries are released for ten families, including the irrationality exponent of π, the Mahler conjectures, Kaplansky's direct-finiteness conjecture in characteristic two, isomorphism of free group factors and the 3D relativistic Vlasov-Maxwell system.
- Exceptions to the fixed procedure: a zero-free region for the Riemann zeta function (writeup human-edited) and the Hodge Conjecture for CM abelian varieties.
- At reading the repo had 13.3k stars and 1.5k forks; Apache-2.0 licence; corrections will be released as new versions.
How they got it
A single fixed procedure with one internal model for most results, then aggregation into families and a significance filter by OpenAI. Verification is partial: Lean for some results, none stated for the rest.
Limits
- Self-selected and self-assessed by the lab that built the model; no external peer review at release.
- Lean compilation does not guarantee the written proof is faithful (see the Bastounis, Circelli and Hansen critique of OpenAI's Navier-Stokes formalisation).
- Manuscript count differs between the Library title (722) and the README read (719).
Why it matters for companies
Frontier models are now producing research-grade output faster than experts can review it. In any domain, the bottleneck moves to verification, curation and explanation. Organisations adopting AI for analysis or engineering should budget for checking capacity, not just generation, and treat "formally verified" claims with care.
Summary based on the abstract only. Read the original for the full argument and data.Read the original on github.com
- Tags
- Verification