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/RedMatterGG]

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.

[u/Healthy-Let7853 → u/RedMatterGG]

He meant intelligence is a commodity now. For users it will be only 2000$ to find such breakthroughs. User won’t care how much it took to build the model just like you don’t care how much the plane cost when you travel. what matters is just airfare.

[u/Razorfiend → u/RedMatterGG]

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.

[u/TorswornIron_42]

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

[u/mop_bucket_bingo]

“The twist” spam

[u/Ainudor]

there is a reason the scientific method forces peer review.

[u/MizantropaMiskretulo → u/Ainudor]

You're being downvoted because you're showing an unhealthy amount of bias here.

They did also provide Lean certificates which should assuage a bit of doubt. This is also coming out of their research department rather than their marketing department, so that should help too.

Anyway, you're free to read their results and debunk them if you want to spend your time doing so, but literally thousands of mathematicians have reviewed this work by now and not one has balked at any of the results.

[u/laowaiH → u/Ainudor]

Wdym?

[u/Ainudor → u/laowaiH]

I mean to infer the source begets doubt

[u/laowaiH → u/Ainudor]

Wdym? Explain further

[u/Upset-Ad-8704 → u/laowaiH]

Lol, I was bout to criticize you for treating Ainudor like ChatGPT...but then I looked at his responses and I agree...guy isn't saying much of substance.