AI system reports proof of 2008 Aaronson-Ambainis quantum computing conjecture, verified in Lean

Physical Superintelligence announced on November 6, 2026 that its internal research system, running a non-public Anthropic model, produced a proof of the Aaronson-Ambainis conjecture, which has been open since 2008. The Lean proof assistant accepted the argument, including a final version refined twice by the system, and the manuscript and formalization have been made public. The conjecture concerns whether quantum computers can be exponentially faster than classical ones on random inputs, lacking the structure that enables speedups like Shor's algorithm. The proof has not yet been peer reviewed, and experts still need to confirm that the formal statement checked in Lean matches the original conjecture.