OpenAI publishes 722 math manuscripts from an unreleased model, with Lean proofs for part of the set

OpenAI on October 6 released new results on open mathematics problems produced by an internal frontier model it has not released. The company published 722 manuscripts, grouped into 372 families, on GitHub under an Apache-2.0 license. The release includes a library of proofs formalized in Lean, the proof assistant that checks each step by machine. Interesting Engineering reports that the model attempted roughly 4,000 problems across pure mathematics, theoretical computer science and mathematical physics.

The important detail for verification is coverage. Lean formalization covers "many, but not all" of the results, and the repository warns that unformalized results could contain errors. One independent count of the repository's Lean scope pages matched 235 of the 372 families, about 63%. That figure counts families with associated Lean documentation. It does not count fully checked theorems. Even a complete Lean proof only verifies the formal statement, so a reviewer still has to confirm that the formal statement matches the claim in the paper. The same analysis says each accepted result used about three hours of ChatGPT Pro thinking compute on average.

The release follows OpenAI's September claim of a solution to the Navier-Stokes Millennium Prize Problem. With that claim the company announced a mathematics advisory group hosted by the Institute for Advanced Study. NPR reported that mathematicians said they had learned little from that result. Early reaction to this release has been skeptical about refereeing capacity and credit. No group of human referees can review 722 manuscripts quickly, and mathematician Terence Tao has warned that machine-generated proofs can appear correct while containing subtle errors.

What is verified is narrow. Any Lean file that compiles against the stated definitions is a checked proof of that formal statement. The significance, novelty and correctness of the remaining results are OpenAI's assertions until mathematicians review them.