OpenAI has published a broad range of new mathematical results produced by an internal frontier model, releasing them through a public GitHub repository with protocols for paper revisions and citations. The company says it consulted the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study to shape how the results are shared, and drew on the group's public recommendations to set its disclosure standards.
The release includes formalizations of many of the proofs in Lean, a programming language that lets a computer check mathematical arguments. OpenAI also published ten summaries of the model's reasoning, estimates of the compute spent in terms of ChatGPT Pro usage, and statistics on how many problems were attempted. On average, each result used the equivalent compute of roughly three hours of ChatGPT Pro thinking. Within days the repository was updated again, adding six new formalizations and nineteen modifications while withdrawing three results as errata were spotted. Roughly 42 percent of the repository's top-line results are now formalized.
OpenAI says the goal is to push the frontier of human knowledge and enable further progress in mathematics, and it plans to fund a series of workshops, conferences and special programs around understanding major results produced by AI. The company adds that it is working to responsibly release the model that produced the results. The move lands amid a live debate over how aggressively AI should be pushed into mathematics, after prominent mathematicians publicly questioned the field's alignment with AI-generated proofs.