Physical Superintelligence (PSI) said on November 6 that a research system it built internally, running a non-public Anthropic model, produced a proof of the Aaronson-Ambainis conjecture, a problem in quantum computing theory that had been open since 2008. PSI says the proof comes with a complete formalization in Lean, the proof assistant, and now describes the conjecture as a theorem.
The conjecture was posed by Scott Aaronson and Andris Ambainis in their paper "The Need for Structure in Quantum Speedups." It asks whether quantum computers can be exponentially faster than ordinary computers on random inputs. Aaronson and Ambainis stated a conjecture about polynomials and showed that if it held, quantum computers would be at most polynomially faster on random inputs.
In plain terms, PSI says the result means that on yes-or-no questions about random strings, a quantum computer cannot save exponentially many input reads unless the string contains a rare pattern. Exponential quantum speedups, in other words, need structure in the problem.
Key facts
- 01PSI published a proof of the Aaronson-Ambainis conjecture on November 6, 2026, with a complete formalization in Lean.
- 02The conjecture, posed by Scott Aaronson and Andris Ambainis, had been open since 2008.
- 03PSI's internal research system ran instances of a non-public Anthropic model and had a complete proof on the third day of the run.
- 04Stanford's Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan are reading the proof and writing a shorter exposition for experts.
The proof builds on a plan laid out by Shachar Lovett and Jiapeng Zhang, which left one inequality as an open conjecture. PSI's proof replaces that step with a new inequality. Its main bound says that if a bounded, non-constant polynomial of degree d has variance v, then some input bit has influence of at least c times v to the 5/2 power divided by d to the sixth, where the constant c is about 0.0025.
PSI ran the work on its own infrastructure using instances of the unnamed Anthropic model. According to PSI, the system had a complete proof of the conjecture during the third day of the run, and Lean accepted it. PSI then pointed the system at related open problems. Along the way it improved the result twice, and Lean accepted the final version.
David Turturean, a Member of Technical Staff at PSI, led the project. He developed the research system, scoped the problem, ran the system, prompted the model to write a first draft of the paper and reviewed it, and PSI lists him as responsible for the paper's correctness. PSI advisor Jim Halverson audited the proof, and advisor Phiala Shanahan commented on the Lean formalization.
Four Stanford University researchers, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, have been reading the proof, have sent PSI comments, and are writing a shorter exposition of it for experts. Their August 2026 paper, "Quantum Speedups Require Structure or Depth," settled the conjecture's prediction only in a special case: quantum algorithms with a fixed number of parallel query rounds. In a note PSI published, the group called the new proof a huge result that resolves a decades-old conjecture.
PSI's announcement does not say the proof has been peer reviewed or accepted by a journal; the Lean formalization is the formal check it cites. PSI has not named the Anthropic model it used, and the model is not publicly available.
Working on something we should cover, or seeing a story we missed? Send leads, documents, or feedback to hello@aichatdaily.com. For sensitive tips, see our secure tips page for Signal and PGP options.
Spotted an error? Email hello@aichatdaily.com with the URL and the issue, or read our full corrections policy.
