Proofs at Two Thousand Dollars
An unreleased OpenAI model reportedly solved ten open math problems for about $2,000 in compute — and published formal Lean proofs. The proofs, not the claims, are the story.
OpenAI's unreleased Astra model is reported to have solved ten previously open problems in mathematics and theoretical computer science, at a compute cost of roughly $2,000, with formal Lean proofs published on GitHub and an endorsement from Fields Medalist Timothy Gowers [1]. We have not independently verified the result set; the reporting is recent and the model is not public.
The pattern across both stories is the same: generation is cheap, verification is the bottleneck. Formal methods make math a best case — proofs check themselves. Most of science does not have a Lean. The research fields that industrialize first under AI will be the ones that build verification cheap enough to keep up with generation, and that is an infrastructure problem, not a model problem.