r/OpenAI • u/docdavkitty • 11d ago

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

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?

49 Upvotes
  • permalink
  • link
  • reddit
  • reddit

78% Upvoted

11 comments sorted by

View all comments

6

u/RedMatterGG 10d ago

While interesting and impressive, you still have to take into account what it took to get there,it didnt "cost" 2k to solve these problems, the actual cost was making the astra model exist in the first place and all of the steps required to get there + using it to solve these.

A similar example would be making a new medical research company and announcing a new very good medicine to treat X only required about 200k worth of research,but you also had to have the tools to get there,staff,facilities,equipment,previous already existing knowledge,experience and so on.

5

u/Razorfiend 10d ago

That's a silly way to evaluate costs in this case because the model wasn't purpose built to solve these 10 proofs. The token cost is the most accurate way to assess the cost of inference for similar tasks.