OpenAI said on October 6 that it was publishing mathematical results from an internal frontier model on GitHub, following advice from the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study.

The repository includes Lean formalizations of many proofs, 10 summaries of the model’s reasoning, estimates of computing power used, and statistics on attempted problems.

OpenAI said the average result used computing power equivalent to roughly three hours of ChatGPT Pro thinking.

Lean is a programming language and theorem prover that enables machine-checkable proofs.

At least one mathematical society has a publication-related AI policy.

DeepMind previously reported silver-medal-level performance on International Mathematical Olympiad problems.

OpenAI said it would add more formalizations over time, explore community-hosted alternatives that meet the advisory group’s guidelines, and fund workshops, conferences, and special programs to help researchers understand mathematical results produced by AI.

🔗 Source: OpenAI

Recent OpenAI developments