AN AI DUMPED 722 MATH PROOFS NOBODY CHECKED — NOW SOMEONE HAS TO READ THEM

On October 6, OpenAI released 722 manuscripts, organised into 372 families of results, produced by an internal frontier model that had tackled roughly 4,000 problems at an average of about three hours of intensive compute per result. Only 162 carried full Lean formalisations allowing computer verification of the main claim; the rest remain provisional, some already required corrections, and three were withdrawn shortly after release.

In response to that flood, the Simons Foundation, together with Anthropic and OpenAI, announced on October 15 a $15 million commitment, including $5 million from OpenAI plus model access and computing, to help mathematicians absorb and test AI-produced results. The money will flow through an open call for proposals funding workshops, conferences and programmes focused on verification, community standards and human interpretation.