From the source
OpenAI is releasing a broad range of new mathematical results produced by an internal frontier model.
The results are published in a GitHub repository with protocols for paper revisions and citations, and include formalizations of many proofs in the Lean programming language.
The release also provides additional details such as summaries of the model's reasoning, estimates of compute spent in terms of Pro usage on ChatGPT, and statistics about the number of attempted problems.