Start-Up Says Non-Public Anthropic Model Proved an 18-Year-Old Quantum Computing Conjecture

"The Aaronson-Ambainis conjecture is now a theorem," the company, known as PSI, wrote in a research post published on Friday. It said its internally built system found a complete proof on the third day of a run on its own infrastructure. The main result was then formalised in Lean, a proof assistant in which software checks every logical step.

If the proof holds, it is one of the clearest cases yet of an AI system settling a well-known open problem in theoretical computer science rather than helping with a piece of it. It also suggests that frontier labs' unreleased models are already being used for research by outside groups. PSI did not name the model or describe the terms of its access, and its post does not mention any partnership with Anthropic.

What The Theorem Says

Scott Aaronson and Andris Ambainis set out the conjecture in a 2009 paper, tracing it to a lecture Aaronson gave in 2008. It concerns whether quantum computers can be exponentially faster than ordinary ones on problems whose inputs have no special structure. The question is framed in the query model, which counts how many times an algorithm reads its input rather than every operation it performs.

Aaronson and Ambainis turned the quantum question into one about polynomials: if a quantum algorithm's chance of answering yes varies meaningfully across inputs, at least one input bit must have a measurable influence on the outcome. A classical computer could then focus its reads on the most influential bits. PSI's paper supplies the missing guarantee, a minimum influence that does not shrink as inputs grow. According to the company, the result means quantum computers are at most polynomially faster than classical ones on random yes-or-no questions, unless the inputs have special structure of the kind Shor's factoring algorithm exploits.

The proof follows a strategy proposed by Shachar Lovett and Jiapeng Zhang and strengthens an earlier lemma by David Reimer. The paper reports that one claim proposed by Lovett and Zhang does not hold in its general form and replaces it with a new inequality proved in the manuscript.

Who Checked the Work

PSI said David Turturean, a member of its technical staff, built the system, chose and scoped the problem, ran it and prompted a model to draft the paper. The paper's disclosure says he reviewed the draft and takes responsibility for its correctness. Advisers Jim Halverson and Phiala Shanahan audited the proof and commented on the Lean formalisation, the company said.

After the first proof, PSI directed model instances to related open problems, and the system twice improved the mathematical bound. Lean accepted the initial proof and both improvements, according to the paper's appendix.

Stanford researchers Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, who proved a narrower case in August 2026 covering quantum algorithms with a fixed number of rounds, have reviewed PSI's proof and are writing a shorter explanation for experts. "This is a huge result," they said, according to PSI. Paata Ivanisvili, a mathematician, wrote on X: "Congratulations — this would be a major result if it holds."

The result has limits. The guarantee applies to most random inputs within a chosen margin of error, not every input. It counts input reads only, not the computing time needed to pick which bits to read, and the permitted number of reads can still be large, so it does not rule out practical quantum advantages. The paper also does not establish the strongest possible influence bound, and its key matching step shows only that a suitable construction exists rather than building one directly.

Nor does a single run show how reliably the system could crack other long-standing problems. With the model unnamed and unreleased, other researchers cannot yet test that themselves, which leaves the Stanford group's write-up and wider expert review as the next checks on the claim.