OpenAI releases multiple new math results and Lean formal proofs from internal frontier model

OpenAI released a series of new mathematical results produced by an internal frontier model, stored in a GitHub repository, with Lean formalizations of some proofs provided. The repository also contains 10 model reasoning summaries, compute estimates, and other transparency details; on average each result is about equivalent to three hours of ChatGPT Pro thinking compute, and OpenAI stated it is working to responsibly release the model that produced these results.