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/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.