OpenAI has published a range of new mathematical results produced by an internal frontier model, placing them in a GitHub repository rather than only describing them in a blog post. The release includes formalisations in Lean, a proof assistant, so the proofs can be checked by a computer instead of taken on trust.
This follows the company’s claim in late September that an internal model had resolved more than 100 open maths problems, which at the time arrived without artefacts attached. The repository now carries protocols for paper revisions and citations, ten summaries of the model’s reasoning, and statistics on the number of problems attempted.
The figure worth noting is the cost. OpenAI says the average result used the equivalent compute of roughly three hours of ChatGPT Pro thinking. That is a claim about the going rate for a research-grade mathematical result, and it is the sort of number that will be argued over once others can test it.
OpenAI says it consulted the Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study on release practice, will fund workshops and programmes on understanding results produced by AI, and intends to release the model that produced them. No date is given for that, so for now the proofs can be verified but the work cannot be repeated.
Source: OpenAI, Sharing AI progress in mathematics.