PSI announces a Lean proof of the Aaronson–Ambainis conjecture, with a non-public Anthropic model
On 06/11/2026 Physical Superintelligence (PSI), a public benefit corporation, published that its internal research system, running a non-public Anthropic model, found a proof of the Aaronson–Ambainis conjecture (open since 2008) on when quantum computers can be exponentially faster. PSI says the full proof appeared on day 3 of the race and was accepted by the Lean assistant; the system then improved the result twice. Stanford researchers (Blanc, Docter, Strassle, Tan), who had solved a special case in Aug/2026, sent comments and are writing a shorter exposition; in the published quote: “This is a huge result.” Work led by David Turturean (MTS); audit by Jim Halverson.