A $2,000 result that isn't about the money
On August 1, OpenAI said an internal model called Astra produced ten new results in mathematics and theoretical computer science. Every one had been open for at least a decade. The headline is the first explicit construction of a non-sofic group, a question that had sat unanswered since 1999. The whole run cost roughly $2,000 in API tokens.
That number is doing a lot of work in the coverage. It shouldn't be the part you remember.
What actually makes this credible
The result you can trust isn't the manuscript. It's the certificates.
OpenAI didn't just publish a 249-page write-up. It published machine-checkable Lean 4 proofs for every result on GitHub, and the repository reports a sorry count of zero. In Lean, sorry is the keyword you drop in when you want to skip a step and come back to it later. Zero sorries means nothing was hand-waved. A proof assistant checked the entire chain, top to bottom.
That is the gap between "an AI says it solved this" and "here is a proof a machine can verify in minutes." A mathematician doesn't have to trust OpenAI. They run the checker and watch it pass.
The lesson for people building software
Most teams are still trying to work out how much to trust AI-generated work. Astra points at the actual answer. You can delegate autonomous work to a model exactly as far as you can verify the output automatically. Not one step further.
When an agent writes a function and there's a test that failed before and passes now, you can accept it without reading every line. When it produces a type the compiler enforces, you can lean on that. When it hands you a paragraph claiming the migration is safe, you have nothing. You're back to reading everything yourself.
Astra worked because mathematics has the strongest verification layer we have ever built: formal proof. Your codebase can have a smaller version of the same thing. Tests, types, contracts, property-based checks, schema validation. The more of your correctness you can express as something a machine checks, the more of your work you can hand to an agent and actually trust what comes back.
What to build instead of chasing the model
A few practical moves:
- Treat the verification layer as part of the product, not a cleanup step. Before you point an agent at a task, ask what checks would prove it succeeded without you reading the diff.
- Prefer checkable outputs. A generated test suite you can run beats a generated explanation you have to believe.
- Push correctness into types and schemas wherever you can. Every invariant the compiler enforces is one an agent cannot quietly break.
The teams that get real value out of autonomous agents this next year won't be the ones running the smartest model. They'll be the ones whose systems can tell, automatically, when the model is wrong.
Astra is a research demo, not something you'll wire into your stack next sprint. But the shape of it is the takeaway. Verifiable output is what makes delegation safe, whether the delegate is a mathematician's proof assistant or your CI pipeline.
We're here to help founders and teams design and build digital products that are built to scale with you, not slow you down. If you're looking to build something, get in contact with us today!