OpenAI Publishes Lean Proofs for Ten Math Claims

OpenAI posted Lean 4 proofs for ten math and computer science results on August 1, per GitHub.

That's the shift the Solution Hacking paper says AI evaluation needs: a claim only counts if something besides a human grader can confirm it. The repo had drawn 459 stars and 41 forks by August 4, per GitHub.

The proofs accompany OpenAI's paper Ten advances in mathematics and theoretical computer science.

The results include an improved sphere-packing bound reaching the Cohn-Elkies threshold, formalized in SpherePacking.lean. Permanent.lean sets a lower bound of n⁴/log n for an arithmetic formula computing the permanent. NonSoficGroup.lean and ConnesRigidity.lean cover two more of the ten claims.

This breaks from how math papers normally get vetted, where a PDF stands alone until reviewers work through the argument by hand. Publishing the Lean certificates next to the paper lets anyone run OpenAI's own checker over the argument instead of taking the abstract on faith.