OpenAI released 372 mathematical results, including a Lean-verified proof of Subhash Khot's Unique Games Conjecture, one of the most important open problems in complexity theory. While the formal certificate validates the proof, human mathematicians have not yet been able to understand most of the results, marking a landmark moment in AI-assisted mathematics.
Background
The Unique Games Conjecture, proposed by Subhash Khot in 2002, is a central open problem in theoretical computer science related to NP-hardness and approximation algorithms. Scott Aaronson is a prominent complexity theorist and his wife Dana Moshkovitz has spent years working toward its proof.
- Source
- Lobsters
- Published
- Oct 8, 2026 at 06:48 AM
- Score
- 9.0 / 10