Startup researcher uses Anthropic's Fable 5.2 to prove the 18-year-old Aaronson-Ambainis conjecture
The proof was checked automatically in the Lean proof language. Scott Aaronson says he believes it is correct, even though he does not fully understand it.
David Turturean, a recent MIT graduate on the technical staff of the startup lab Physical Superintelligence (PSI), used early access to Anthropic's Fable 5.2 model to solve the Aaronson-Ambainis conjecture, an 18-year-old problem about when quantum computers can solve problems faster than classical ones. Scott Aaronson, who posed the problem with Andris Ambainis, writes that he does not quite understand the proof but believes it is correct. His reasons are that it was autoformalized in Lean, a programming language for mathematics, and explained by a team of top researchers with whom PSI shared it. Aaronson called a full proof one of the last remaining open problems in quantum query complexity that everyone agreed was centrally important. The result is negative: it appears to rule out one route by which quantum computers might solve certain hard problems at high speed, though not all such routes. Turturean said this tells researchers where they no longer need to look. He also said he is "totally accepting the idea that this might be the last paper I ever put out." PSI is trying to build a business around AI-driven scientific discovery.