Ten advances in mathematics and theoretical computer science
Points and comments are a snapshot, not live.
OpenAI claims a next-gen model solved 10 long-standing math and CS problems.
OpenAI reports that an internal version of its Astra model produced proofs for ten open problems in mathematics and theoretical computer science spanning high-dimensional geometry, coding theory, group theory, and more. The total token cost was roughly $2,000 at Sol API rates. OpenAI helped prepare human-readable manuscripts and formalized each proof in Lean, releasing certificates. The company states it takes responsibility for correctness. Results include new bounds on sphere packing, a disproof of Connes's rigidity conjecture, and resolution of multiple Erdős problems. OpenAI acknowledges concerns about AI's role in mathematics and the Leiden declaration.
What commenters are saying
Commenters split sharply. One camp sees AI as mainstreaming math and generating new directions; another fears mathematics becoming like chess, where human careers vanish and only a few stars benefit. A specific objection: math has paid careers, while chess does not. Skeptics question transparency around costs, arguing $50M for a single proof would be hard to justify versus traditional grants. Others note that Lean formalization does not guarantee correctness if the model cheats via 'sorry' or kernel bugs. A minor thread points out a recent sensationalized LLM bug in Lean was not a real vulnerability.