Did OpenAI's AI solve hundreds of open math problems?

The claim. On Oct 6, OpenAI released 722 manuscripts in 372 “result families” from an internal model, each billed as resolving or advancing an open problem (It Does What Now?).

Line item	Number
Problems posed	~4,000
Manuscripts published	722
Failures disclosed	none
Manuscripts in Lean catalogue	162 (~22%)
Families with some Lean check	235 of 372
Catalogue review status	“unchecked”
Peer-reviewed	0
Model name	not disclosed

Sources: The Frontier, It Does What Now?

Lean is a proof language where a computer checks every step. The catch: humans still have to confirm the Lean statement says what the paper claims.

Plasma AI counts 40 Erdős problems touched, with claimed complete solutions to 17. It rebuilt the 12 that came with full Lean proofs and now lists those as solved (Plasma AI). OpenAI’s own README warns that “some of the unformalized results could have issues.”

Verdict: ⚠️ Partly. “Hundreds of results” is a fair paper count. “Solved” is premature: under a quarter of manuscripts have catalogued Lean proofs, the catalogue is unreviewed, and nothing is peer-reviewed. And the most telling number, how many of ~4,000 attempts failed, is missing.

Show your work. It’s literally math.

First published in AI Receipts #1.