An Anthropic AI reportedly solved a quantum computing question open since 2008

On November 6, a young company in Cambridge, Massachusetts, announced that a question posed in 2008 in quantum computing had been answered. Physical Superintelligence (PSI) says it has proved the Aaronson-Ambainis conjecture, named after researchers Scott Aaronson and Andris Ambainis.

The most unusual part is who wrote the proof. According to PSI, it was produced by an in-house research system that ran several instances of a non-public Anthropic model. The company does not say which one. The system reportedly delivered a complete proof on day three, accepted by Lean, software that checks the steps of a proof one by one. It then reportedly improved the result twice. No publication in a peer-reviewed journal has been announced at this stage.

Do quantum computers need structure?

The question is this: can a quantum computer be exponentially faster than a classical computer on randomly drawn data, with no particular organization? The spectacular speedups we know of rely on structure in the problem. This is the case for Peter Shor's factoring algorithm (1994), which exploits periodicity.

Aaronson and Ambainis had shown that the answer depended on a statement about polynomials: any bounded, non-constant, low-degree polynomial would have at least one input variable that significantly influences its output. If this statement is true, then for most random inputs, a classical algorithm can approximate the result of a quantum algorithm without having to read the data exponentially more times. PSI says it obtained a bound that decreases only polynomially with the degree. The general bounds known until now decreased exponentially.

The scope of the result is narrow. According to The Quantum Insider, it concerns the number of reads of the data, not computation time. It holds for most inputs, not all. And it does not mean that a classical computer can reproduce any quantum computation. For those following the post-quantum migration, it does not affect Shor's algorithm, which threatens RSA encryption precisely by relying on structure.

A machine-verified proof, but not end to end

PSI's GitHub repository is more cautious than the headlines it has generated. It reports four theorems proved in Lean, with no “placeholder” and no “added axiom,” and checked by two independent verifiers. But it states that it is up to the reader to check that the formalized statement matches the published conjecture. One of the four theorems relies on a result by other researchers (Agarwal and Ben-David) that has not been formalized. Finally, the paper written for humans has not been machine-verified.

Humans also worked on this proof. David Turturean, of PSI's technical team, designed the system, framed the problem, had the model write a first draft of the paper, then reviewed it. He takes responsibility for its accuracy. Two advisers were involved: Jim Halverson audited the proof and Phiala Shanahan commented on the formalization. The proof follows an outline by Shachar Lovett and Jiapeng Zhang, who had left one inequality unproved. PSI replaces it with a new inequality.

In 2019, a first proof collapsed

There is a reason for this caution. In November 2019, Scott Aaronson hailed a proof by Nathan Keller and Ohad Klein on his blog. The authors later withdrew it: mathematician Paata Ivanisvili had found a “fatal flaw” in a lemma. Aaronson left the post online for the historical record.

This time, a Stanford team (Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan) is reviewing the proof. It had proved a special case in August. It has sent comments and is preparing a shorter presentation. PSI reports its reaction: “This is a huge result.” As of November 8, we found no public reaction from Aaronson or Ambainis.

Such announcements are becoming more frequent, as when OpenAI and Anthropic claimed their AIs had refuted a key hypothesis in computer science. Each time, they raise the question of verification and of how much credit goes to humans. This is one reason why OpenAI and Anthropic are funding, with the Simons Foundation, a program that helps mathematicians verify these results. One unknown remains: which Anthropic model did this work, and when will others be able to use it?