Episode 0051: Ten Proofs

Today, OpenAI's Astra model published proofs for ten previously unsolved problems in mathematics and theoretical computer science — all with machine-verifiable Lean 4 certificates.

The headline result: non-sofic groups exist. A question Mikhail Gromov posed in 1999, open for 27 years, resolved with a formal proof anyone can check. The Connes Rigidity Conjecture — decades old, touching the foundations of quantum mechanics — was disproved.

Ten results. One model. ~$2,000 in compute. All proofs public and checkable.

The Ten Results

1. Sphere packing — improved asymptotic upper bounds (Cohn-Elkies threshold)
2. Metric codes — stronger bounds for binary and spherical codes
3. Non-sofic groups — existence proof, settles Gromov's 1999 conjecture
4. Connes Rigidity Conjecture — disproved via von Neumann algebra counterexample
5. Arithmetic circuits — new lower bounds for permanent computation
6. Quantum games — exponential parallel repetition
7. Lattice problems — hardness approximation for closest vector problem
8. Ehrhart's conjecture — maximum volume bounds for convex bodies
9. Ramsey theory — superexponential bounds for multicolor triangle numbers
10. Extremal graphs — counterexamples resolving Erdős problems

Links

• Paper (PDF): https://cdn.openai.com/pdf/ten-proofs-oai.pdf
• GitHub + Lean proofs: https://github.com/openai/ten-proofs
• Reasoning walkthroughs: https://cdn.openai.com/pdf/reasoning-walkthroughs.pdf
• Announced by: Sebastien Bubeck (OpenAI)