A repository, not a paper
OpenAI published a catalogue of mathematical results on 6 October produced by what it calls an internal frontier model, and put the whole thing in a GitHub repository rather than submitting it to journals. The catalogue holds 722 manuscripts organised into 372 result families, where a family groups a principal result with companion arguments, consequences or alternative proofs.
The company says the work came out of model development rather than a dedicated research programme. “As part of model development, we evaluate our models on open research problems,” the repository’s readme says. “We expanded these evaluations after performance on our existing mathematical evaluations saturated.”
What the numbers say about the compute
OpenAI disclosed more about method than it usually does. Over the evaluation the model was posed approximately 4,000 problems. The average published result used the equivalent of roughly three hours of ChatGPT Pro thinking compute. Aggregating the output into families and manuscripts, and requiring what OpenAI calls an appropriate level of significance, produced the 722 figure.
Two items were handled differently. Work on a zero-free region for the Riemann zeta function and a proof of the Hodge Conjecture for CM abelian varieties fell outside the fixed procedure, and OpenAI says the write-up of the zeta-function result — covering the region where the real part of s exceeds 11/12 — was edited by a human for readability.
The caveats are in the readme, not the blog post
The collection includes results at different stages of verification. Many manuscripts carry formalisations in Lean, a language that lets a computer check a proof, but not all of them do. OpenAI states plainly that “some of the unformalized results could have issues” and says it will fix any it finds quickly, adding formalisations to the repository as it obtains them.
That framing matters because it is the company itself, rather than a referee, deciding what counts as significant enough to publish. OpenAI says it consulted the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study on best practices, and drew on the group’s advice and public recommendations in deciding how to release the results.
Ten reasoning summaries
Alongside the manuscripts, OpenAI released abridged summaries of the model’s reasoning for ten results, including the irrationality exponent of pi, the symmetric and general Mahler conjectures, quasipolynomial bounds for arithmetic progressions, Kaplansky’s direct-finiteness conjecture in characteristic two, and the three-dimensional relativistic Vlasov-Maxwell system. It also published per-manuscript citation instructions and said it will preserve the release history, recording corrections as new versions.
What to watch
The model that produced all of this is not available. OpenAI says it is “working to responsibly release the model that produced these results” and that it will fund a series of workshops, conferences and special programmes aimed at understanding major results produced by AI, with details to come.
The practical test is now the Lean library. Formalised proofs can be machine-checked by anyone; unformalised manuscripts have to be read by mathematicians, and 722 of them is a lot of reading. How quickly the formalisation catalogue fills in — and how many of the unformalised results survive contact with the field — will say more than the headline count does.
