PSI says its system proved the Aaronson-Ambainis conjecture with Lean verification

Physical Superintelligence (PSI) said on November 6 that an internal research system, running a non-public Anthropic model on PSI infrastructure, found a proof of the Aaronson-Ambainis conjecture (open since 2008) that Lean accepted. The conjecture bears on when quantum computers can be exponentially faster than classical ones on random inputs; with it proven, for yes-or-no questions a quantum computer cannot save exponentially many queries unless the input has rare structure. Stanford's Blanc and colleagues who earlier settled a special case are reading the full proof and called it a huge result. PSI posted the paper and Lean artifacts on GitHub.

Written by dalao.ai: the title, summary and why it matters are our own words. The original reports are the record; their publishers keep authorship.