Some really cool news for the world of Math in AI.
Rohan Paul Twitter · Rohan Paul (@rohanpaul_ai) · 2026-08-01
OpenAI's unreleased Astra model solved 10 open mathematics problems that had resisted solution for decades, spanning five advanced fields, at a total cost of roughly $2,000, with every proof formally verified step-by-step in the Lean theorem prover.
Appears in
Extraction
Topics: ai-math-reasoningformal-verificationopen-problemsopenai
Claims
- OpenAI's unreleased Astra model solved 10 mathematics problems that had remained open for decades.
- The total compute cost for all 10 solutions was approximately $2,000 at Sol API rates, averaging $200 per problem.
- The solved problems span high-dimensional geometry, coding theory, operator algebras, quantum complexity, and lattice cryptography.
- Each AI-produced proof was formally verified in Lean, which checks every logical step before signing off.
Key quotes
OpenAI's unreleased Astra model solved 10 math problems that had stayed open for decades.
Finding all 10 cost roughly $2,000 in tokens at Sol API rates, i.e. $200 per answered question.
Each AI produced argument was rebuilt in Lean, that rechecks a proof step by step, and that only signs off when every step is fully justified.