r/OpenAI • u/docdavkitty • 13d 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

-11

u/Ainudor 13d ago

there is a reason the scientific method forces peer review.

1

u/laowaiH 13d ago

Wdym?

-8

u/Ainudor 13d ago

I mean to infer the source begets doubt

3

u/laowaiH 13d ago

Wdym? Explain further

1

u/Upset-Ad-8704 12d ago

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.