OpenAI claims to have solved ten long-standing mathematical problems using an internal version of its Astra model at GPT-5.6 token prices, spending under $2,000 per problem. The results include Lean 4 formalizations and a paper, though the prompts used remain undisclosed. This follows Anthropic's recent discovery of cryptographic weaknesses with Claude, reigniting debate about AI's role in mathematical research.
Background
OpenAI and Anthropic are increasingly using large language models to tackle formal mathematical problems, with results verified in proof assistants like Lean 4. This trend has sparked both excitement and concern in the mathematics community about AI's growing role in research.
- Source
- Simon Willison
- Published
- Aug 2, 2026 at 04:34 AM
- Score
- 7.0 / 10