PSI says AI system produced machine-checked proof of quantum conjecture

Physical Superintelligence said November 6 that an internal AI research system found a proof of the Aaronson-Ambainis conjecture, a quantum-computing problem open since 2008. The system used instances of a non-public Anthropic model; the manuscript and Lean 4 formalization are public. PSI says the Lean proof assistant accepted the argument, which concerns limits on quantum speedups for unstructured inputs. The formal declarations were also replayed through an independent implementation of Lean's type checker. A human researcher scoped the problem, ran the system and reviewed its draft. Experts must still confirm that the encoded statement matches the conjecture; the human-readable paper itself is not machine-checked.