PSI says Anthropic-powered AI proved quantum conjecture

Physical Superintelligence (PSI), a physics-focused AI startup, said on Friday, Nov. 6, that a research system it built proved the Aaronson-Ambainis conjecture, a quantum complexity problem open since 2008, using instances of a non-public Anthropic model. The company said the system had a complete proof on the third day of a run on its own infrastructure, and the Lean proof assistant accepted it. The result has not yet passed journal peer review. For now it is a company claim, but the paper and the machine-checked proof are public, so outside experts can test it.psi.inc

What the proof claims

The conjecture asks whether quantum computers can be exponentially faster than ordinary ones on random inputs, which almost never contain the hidden patterns that algorithms like Shor's factoring method exploit. Aaronson and Ambainis showed that if their statement about bounded low-degree polynomials held, quantum speedups on random inputs would be at most polynomial. PSI's announcement framed the result this way: "a quantum computer cannot save exponentially many looks unless the string has a rare pattern". The theorem limits how many times an algorithm reads its input, not total computing time, which leaves room for practical quantum advantages.thequantuminsider.com+1

The first proof gave a weaker bound. After PSI set the system on related open problems, it improved the result twice, and Lean accepted the final version. The argument follows a plan by Shachar Lovett and Jiapeng Zhang. It replaces an inequality they had left as a conjecture with a new one, proved by pairing input settings through a determinant.psi.inc

Human roles and checks

PSI staff member David Turturean built and ran the system, prompted the model to draft the paper, and is responsible for its correctness. Advisers Jim Halverson and Phiala Shanahan audited the proof and commented on the formalization. The project's GitHub repository says the proof, paper and formalization were produced by AI models. It also says the Lean theorems contain no placeholders or added axioms and were re-checked by two independent kernel implementations. Readers still need to confirm that the formal statement matches the original conjecture.github.com+1

Stanford researchers Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan settled a special case in August. They have been reading the full proof and, in a statement published by PSI, called it "a huge result" in which "everything is brought together in a rather magical way".psi.inc

Unanswered questions

PSI has not said which Anthropic model it used, and Anthropic did not respond to a request for comment. The announcement follows OpenAI's September claim that it had solved a problem involving the Navier-Stokes equations, and it adds to a debate over what AI means for mathematicians' careers.businessinsider.com