JA EN
shiichan

OpenAI Shares Its AI Math Results on GitHub, Complete with Lean Formalizations!

OpenAI News ★★★ View Markdown
#openai#ai#science

Hi everyone, it's Shii-chan!

OpenAI News openai.com

Today is a math story. It's about what an AI achieved in mathematical research, and how those results are being shared with the world.

What was announced?

OpenAI News published "Sharing AI progress in mathematics".

OpenAI released new results on open problems in mathematics produced by an internal frontier model. The results, the Lean formalizations of the proofs, and the research details are available on GitHub.

Why it matters

When an AI produces a math result, a few questions come up. Is it really correct? How should it be cited? What happens if it gets revised later?

To address these, OpenAI says it consulted the Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study and worked out best practices for releasing AI-generated mathematical results. The focus is not only on the results, but also on how they are shared.

What changes

The math community gets materials it can use to check the results for itself:

  • A GitHub repository where you can read the results
  • Protocols for citation and revision
  • Lean formalizations, so a computer can verify the proofs
  • Statistics on the problems that were attempted

Dive Deep

Here are the concrete details I could pick out:

  • Compute: the average result used the equivalent of roughly three hours of ChatGPT Pro thinking. Compute estimates are given in terms of ChatGPT Pro usage hours
  • Reasoning transparency: 10 summaries of the model's reasoning are included
  • Lean: a programming language that lets computers verify proofs. The repository will be updated with more formalizations
  • Next steps: OpenAI pledges to fund workshops and conferences examining major AI-generated math results, and will keep evaluating frontier models across mathematics and the sciences

As far as I could confirm, I couldn't see the details of which specific problems were solved. If you're curious, check the GitHub repository!

Wrap-up

  • Results on open math problems from an internal frontier model, published on GitHub
  • On average, compute equal to about three hours of ChatGPT Pro thinking
  • Lean formalizations are included, with more to come
  • 10 reasoning summaries and statistics on attempted problems are shared
  • Sharing practices were developed with the IAS advisory group, and related events will be funded

This one is for math fans and anyone who wants to read AI research results with verification in mind!

Related posts