An AI System Found a Proof of a Quantum Computing Question Open Since 2008
A research system built inside the AI company Physical Superintelligence has produced a proof of the Aaronson-Ambainis conjecture, an unproved claim about the limits of quantum computers dating to 2008. The company published it on its own research page Nov. 6, 2026, and says the Lean proof assistant, software that checks every step of a proof, accepted it.
The conjecture concerns when quantum computers can be exponentially faster than ordinary ones. On PSI's account, proving it rules out an exponential advantage on random inputs: a quantum computer cannot answer a yes-or-no question about a random input with exponentially fewer reads of it than an ordinary computer, so big speedups need a rare pattern in the problem. The bound is on reads of the input, not on running time.
The work is self-published and has not been peer-reviewed. PSI says that the system had a complete proof during the third day of the run, that Lean accepted it, that the system then improved the result twice, and that Lean accepted the final version. A Lean check confirms that every step of a formal proof follows, which is not what peer review does. The run used instances of a non-public Anthropic model on the company's own hardware.
In August 2026, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan of Stanford University settled the conjecture's prediction in a special case. PSI says they have since read its proof of the full conjecture, sent comments, and are writing a shorter exposition for experts. They wrote to the company: "This is a huge result. It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups."
PSI credits David Turturean, a member of its technical staff, with developing the research system, scoping the problem, running it, prompting the model to package the results into a first draft of the paper, reviewing that draft, and being responsible for its correctness. An adviser, Jim Halverson, audited the proof; another, Phiala Shanahan, commented on the Lean version.
The page links the manuscript and the Lean proofs and code.
