OpenAI Publishes Lean-Checked Proofs for Ten Open Mathematics Problems From an Unreleased Model

OpenAI said on August 1 that an internal version of its next model family, Astra, produced new results on ten open problems in mathematics and theoretical computer science. It published a 249-page manuscript with certificates for every result, written in Lean 4, software that checks a proof step by step. The central claim is an explicit construction of a non-sofic group, a question open since the mathematician Mikhail Gromov introduced soficity in 1999. Other results cover sphere-packing bounds, coding theory, quantum complexity and lattice cryptography. OpenAI puts the compute bill at roughly $2,000.

The formalization matters because it removes the usual objection to machine-generated proofs. A Lean certificate can be checked by anyone with a laptop, and the identity of its author is irrelevant to that check. What Lean cannot check is whether the formal statement faithfully renders the problem mathematicians actually considered open, whether the definitions match the field's intent, or whether the historical framing is correct. Those are judgement calls OpenAI is currently making about its own output, and none of the ten results has cleared a journal.

Commentary around the release has gone well beyond the evidence. A widely shared post relayed a claim from Emad Mostaque, the former chief executive of Stability AI, that a one-billion-parameter model trained only on pre-1911 material rederived general relativity on its own. No paper, weights or reproduction accompany that claim, and it does not carry the evidentiary weight of the Lean artifacts. The same channel is circulating recursive self-improvement framing that the Astra release does not support. Ten formalized theorems is a research result, not evidence that a system is improving itself.