OpenAI announced that its internal Astra model — the company’s next major release — has independently solved 10 mathematical problems that had resisted human effort for decades. Among the results: the first explicit construction of a non-solvable group (a problem in abstract algebra previously only approachable indirectly), a disproof of Conn’s rigidity hypothesis in functional analysis, a proof of Erhart’s volume conjecture in lattice geometry, and the first improvement since 1978 in the general upper bound for sphere-packing density. Astra also proved a quantum parallel repetition theorem for general two-player games.

All proofs were formally verified in Lean and published alongside a 249-page manuscript. OpenAI estimates the successful Sol API runs cost roughly $2,000. The model is not yet publicly released and is not branded as GPT-6.

Ten Advances in Mathematics

Related: OpenAI Model Autonomously Solves 80-Year-Old Geometry Conjecture, Terence Tao Warns of a Crisis in Mathematics Driven by AI