PSI says a non-public Anthropic model helped prove a quantum computing conjecture open since 2008

Physical Superintelligence says an internal research system running instances of a non-public Anthropic model proved the Aaronson-Ambainis conjecture, according to a company research post. The system completed a proof during the third day of a run, and the Lean proof assistant accepted it.

The conjecture, open since 2008, concerns whether quantum computers can gain an exponential advantage over classical computers on random inputs. The proof establishes that, for yes or no questions in the query model, a classical algorithm can approximate a quantum algorithm on most random inputs with a polynomial increase in the number of input reads.

The result concerns input reads rather than total computation time, and it does not rule out exponential quantum advantages for problems with suitable structure. PSI said David Turturean developed and ran the research system, reviewed the paper draft, and is responsible for its correctness. Jim Halverson audited the proof, while Phiala Shanahan reviewed the Lean formalization.

Stanford researchers Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, who settled a special case in August, are writing a shorter exposition of the proof for experts. "This is a huge result," they told PSI. "It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups."

For quantum computing, the result points algorithm research toward problems whose structure offers an advantage, The Quantum Insider reported. Experts still need to review what the machine checks establish, Unite.AI noted. The claim follows other AI-assisted math results, including OpenAI's September claim on the Navier-Stokes equations, Business Insider reported.