AI System Produces Machine-Checked Proof of 18-Year-Old Quantum Conjecture

PSI says an Anthropic model instance proved the 2008 Aaronson-Ambainis conjecture in three days, with the Lean proof assistant accepting the full formalization.