Physical Superintelligence (PSI), a research company, says its in-house research system has proved the Aaronson-Ambainis conjecture, a problem in quantum complexity theory that had been open since 2008. The system ran instances of a non-public Anthropic model on PSI’s own infrastructure, and Lean, a proof assistant that checks every step by computer, accepted the proof. PSI published the result on November 6 in a research post.
What the conjecture is about
Quantum computers are known to be exponentially faster than ordinary computers on some problems, but almost always when the input has a hidden structure. Shor’s factoring algorithm, the reason a large quantum computer would threaten today’s public-key cryptography, works because the problem hides a repeating pattern. Whether a quantum computer can be exponentially faster on random inputs, which almost never have such a pattern, was an open question.
Scott Aaronson and Andris Ambainis turned that question into a statement about polynomials. A quantum algorithm that reads its input T times says yes with a probability that is a polynomial of degree at most 2T, with values between 0 and 1. They conjectured that every such polynomial has at least one input bit with large influence, meaning that flipping that bit moves the polynomial’s value noticeably on average. If the conjecture holds, an ordinary computer can imitate the quantum algorithm on most random inputs with only polynomially more reads.
According to PSI, that is now settled: on yes-or-no questions, a quantum computer cannot save exponentially many reads unless the input has a rare pattern. The proved bound includes an explicit constant of about 0.0025. Earlier general bounds decayed exponentially with the polynomial’s degree.
How PSI says the proof was found
PSI says the system had a complete proof during the third day of its run and that Lean accepted it. PSI then set the system on related open problems, and it improved the result twice; Lean accepted the final version as well. The proof follows a plan by Shachar Lovett and Jiapeng Zhang and replaces the one inequality they had left as a conjecture with a new one, proved through a one-to-one pairing of inputs that a determinant produces. It strengthens a weaker pairing from David Reimer’s Butterfly Lemma.
David Turturean of PSI built the system, chose the problem and ran it. He then prompted the model to draft the paper, reviewed the draft and is responsible for its correctness. Advisor Jim Halverson audited the proof, and advisor Phiala Shanahan commented on the Lean formalization.
What is still unchecked
A Lean check is strong evidence that the formal proof is valid, but it covers the formal statement, not the prose paper. Experts still have to confirm that the Lean statement matches the conjecture as Aaronson and Ambainis wrote it. The paper has not been through peer review. PSI does not name the Anthropic model, so outsiders can check the output but cannot repeat the search.
There is early outside support. Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan of Stanford, who proved a special case in August 2026, have read the proof and are writing a shorter version for experts. PSI quotes them calling it “a huge result.”
For anyone worried about encryption, nothing changes. The result is about random, unstructured inputs, and Shor’s algorithm relies on structure. Our explainer on Q-Day covers that threat, and how quantum computing works explains the basics.
