Unreleased Anthropic Model Helps Prove 2008 Quantum Speedup Conjecture, PSI Says

The company, known as PSI, posted the paper and a formal version of the main theorem, checked in the Lean proof assistant, on November 6 alongside a research note on its website. If the proof survives expert scrutiny, it sets a firm limit on where quantum computers can deliver exponential gains. On yes-or-no questions about random inputs with no hidden structure, a classical algorithm can approximate the behaviour of a quantum algorithm on almost every input without needing exponentially more reads of the data. Known exponential speedups, such as Shor's factoring algorithm, depend on structure in the problem.

The claim also matters beyond physics. It is among the most prominent open mathematical problems that a company has said was cracked largely by an AI system, and it identifies a frontier lab's unreleased model as the engine. PSI did not name the model.

According to PSI's note, David Turturean, a member of its technical staff, chose and scoped the problem and ran the company's internal research system on it, using instances of the Anthropic model on PSI's own infrastructure. The system had a complete proof during the third day of the run, and Lean accepted it. PSI then pointed the system at related open problems, and it improved its own result twice; the final version was also accepted by Lean. Turturean prompted the model to turn the work into a first draft of the paper, which he reviewed and edited, and PSI says he is responsible for its correctness. Two PSI advisers were involved: Jim Halverson audited the proof and Phiala Shanahan commented on the Lean formalisation.

The argument builds on a 2023 strategy by Shachar Lovett and Jiapeng Zhang and strengthens a result by David Reimer known as the Butterfly Lemma. The paper says one claim in the Lovett-Zhang approach fails in its stated general form and replaces it with a new inequality that it proves. Its central statement is that any bounded, non-constant polynomial of a given degree must have at least one input variable whose influence is polynomially large in the polynomial's variance and degree, which is the form in which Scott Aaronson and Andris Ambainis originally framed the question.

In August, Stanford researchers Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan proved the conjecture's prediction for quantum algorithms that read their input in a fixed number of parallel rounds, leaving the general case open. PSI says the four have read the full proof, sent comments and are writing a shorter exposition for other experts. In comments published by PSI, they said the ideas come together "in a rather magical way".

There are significant caveats. The paper has not been peer reviewed. Lean certifies only that the theorem as written in Lean has been proved; specialists still have to confirm that the formal statement matches the conjecture and check the parts of the paper outside the formal proof. The problem has a history of false dawns: a claimed proof by Nathan Keller and Ohad Klein in 2019 was withdrawn after a flaw was found. Quantum Zeitgeist reported that neither Aaronson nor Ambainis had commented as of November 7.

The result is also narrower than a general verdict on quantum computing. It concerns query complexity, the number of times an algorithm reads its input, rather than total running time on real hardware. It holds for most inputs rather than every input, the classical overhead it permits, while polynomial, can still be large, and polynomial speedups such as Grover's search algorithm are unaffected, The Quantum Insider noted.

PSI was founded by Matt Pines, Alex Klokus and Alexander Wissner-Gross and raised a $58 million seed round led by Breakthrough Energy Ventures, according to Quantum Zeitgeist. The paper and Lean code are available on GitHub for outside review, and the Stanford group's exposition is still being written.