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

The company puts the compute cost at about $2,000 and released machine-checkable certificates. No result has been through refereed review, and OpenAI is judging the novelty of its own work.

- Published: 2026-08-04T06:16:46.804Z
- Canonical: https://polylog.news/ai/2026-08-04/openai-publishes-lean-checked-proofs-for-ten-open-mathematic
- Publisher: Polylog (AI desk)
- Section: tech
- Sources: [Polylog editors](https://polylog.news)

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](https://thenextweb.com/news/openai-astra-model-ten-math-proofs-non-sofic-groups). 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](https://www.forbes.com/sites/jonmarkman/2026/08/03/openais-astra-solved-10-decades-old-math-problems-for-just-2000/).

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](https://kingy.ai/news/openai-astra-ten-math-results-evidence/), 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](https://t.me/aipost/7723). 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](https://t.me/aipost/7722) that the Astra release does not support. Ten formalized theorems is a research result, not evidence that a system is improving itself.

## What this means

The binding constraint on machine mathematics has moved from generating candidate proofs to certifying that the formal statement is the interesting one, which shifts scarce human effort from verification to problem curation. Formal-methods tooling and Lean-adjacent infrastructure gain, and so does any lab that can convert a $2,000 compute run into publishable research. The open question is whether independent mathematicians confirm that all ten statements were genuinely open, or whether several turn out to be known results in unfamiliar notation, which would make the announcement a strong systems demonstration rather than a research event.

## What to watch

- Whether working group theorists publicly confirm that the non-sofic group construction resolves the question as the field understood it, the single check that decides how much of this claim survives.
- Whether OpenAI ships Astra to outside researchers rather than only publishing its outputs, since a model no one can run cannot be tested on problems OpenAI did not pick.
- Whether competing labs answer with their own Lean-certified results, which would turn formal verification into the default currency for capability claims in mathematics.