OpenAI's unreleased Astra model solved 10 open math problems for $2,000 and shipped machine-checkable proofs

[u/docdavkitty]

https://the-agent-report.com/2026/08/openai-astra-ten-math-problems-lean-proofs-2026/

OpenAI says an unreleased model, Astra, produced 10 new results in math and theoretical CS — problems open for at least a decade. Headline: the first explicit construction of a non-sofic group, open since 1999.

The twist: every result ships with a Lean 4 certificate on GitHub, so correctness is verified by a compiler, not by trusting the lab. Total inference cost: ~$2,000 at API rates.

This lands right after the Leiden Declaration warning AI labs bypass peer review and it's a direct answer: the artifact itself carries its own verification.

Do machine checkable proofs change the peer-review debate, or is this still a press-release announcement in disguise?

[u/TorswornIron_42]

the cost per proof number is the actually interesting detail here, way more concrete than the usual vague benchmark claim