OpenAI publishes ten advances on long-standing open problems in mathematics and theoretical computer science

On August 1, 2026, OpenAI released a 249-page collection of ten results — spanning sphere packing, coding theory, a non-sofic group construction, and two Erdős problems — attributed to an internal version of its next major model, with human-polished manuscripts and machine-checkable Lean 4 certificates published alongside. OpenAI puts the token cost of the work at about $2,000.

What it means Formal Lean certificates make these the rare frontier-capability claims a reader can check without trusting the vendor — and a marker for where model-driven research is this quarter.