A conjecture that has shaped arguments about quantum speedups since 2008 now has a machine-checked proof, Physical Superintelligence said Friday. The physics research lab reported that an internal research system, running instances of a non-public Anthropic model on PSI’s own infrastructure, produced a complete proof of the Aaronson-Ambainis conjecture on the third day of a run, and that the Lean proof assistant accepted it.

In a research post , PSI put the claim bluntly: “The Aaronson-Ambainis conjecture is now a theorem.” Scott Aaronson and Andris Ambainis linked the question to polynomials and argued that, if their conjecture held, quantum computers would have at most a polynomial advantage in the number of input queries needed for yes-or-no questions on random inputs that lack rare structure.…