Startup Says an Unreleased Anthropic Model Cracked a Long Open Quantum Computing Conjecture
Physical Superintelligence says a research system running a non-public Anthropic model proved the Aaronson-Ambainis conjecture, and Lean checked the result. Scott Aaronson believes the proof is correct but says it changes far less about quantum computing than the hype suggests.
A startup with a very large name just took down a very specific problem. Physical Superintelligence (PSI) said on November 6 that a research system it built in house, running instances of a non-public Anthropic model, produced a proof of the Aaronson-Ambainis conjecture, a question about the limits of quantum computing that PSI says has been open since 2008. The man whose name comes first on the conjecture thinks the proof holds up. Neither PSI nor Anthropic will say which model did the work.
According to PSI's announcement, the system had a complete proof during the third day of a run, and Lean, a proof assistant that checks every step by computer, accepted it. Pointed at related problems, the system then improved the result twice, and Lean accepted the final version too.
The conjecture, posed by Scott Aaronson and Andris Ambainis, is pure math with a quantum payoff. It says every bounded, low degree polynomial on the discrete cube has at least one variable that moves its output by a meaningful amount. Aaronson and Ambainis showed that if this is true, a classical computer can imitate any quantum algorithm on most random inputs without needing exponentially more looks at the data. PSI says its proof shows exactly that: no exponential speedup on yes or no questions unless the input has a rare pattern.
Who actually did the math
The paper, posted to arXiv under the name of PSI's David Turturean, is unusually blunt about authorship. Its AI disclosure says "the mathematical statements in this paper were produced by AI models." Turturean scoped the problem and built and ran the harness, in which model instances searched for existing ideas, proposed new ones and supervised each other. He then prompted the model to write a first draft, reviewed and edited it, and says he is responsible for its correctness.
The machine also stood on a lot of human shoulders. PSI says the proof follows a plan by Shachar Lovett and Jiapeng Zhang, who left one key inequality as an open conjecture. The proof replaces it with a new inequality, built on a stronger pairing than David Reimer's Butterfly Lemma provides. In August, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan had settled a special case. PSI says the same group has been reading the full proof and is writing a shorter version for experts. Their verdict, as quoted by PSI:
"This is a huge result. It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups." Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan
Aaronson himself weighed in on his Shtetl-Optimized blog, admitting he has not yet understood the proof but believes it is correct because there is a Lean certificate and human experts have already gone over it. Among his feelings: "disappointed that humans didn't get to snag this conjecture before the robots did." Posting in the comments, Blanc wrote that the result felt like something humans could have reached within a few years, but that this particular proof "feels hard to find."
Aaronson also swatted down the hype, writing that the result rules out a kind of quantum speedup most researchers already doubted existed, and that it has "zero effect" on Shor's algorithm or on simulating physics and chemistry. The result lands weeks after OpenAI said its AI toppled a bedrock assumption of computer science.
The verification has edges worth naming. According to an audit in PSI's repository, as summarized by Silicon Report, the Lean code contains no placeholders or added axioms and was rechecked with an independent type checker. But Lean's kernel and the Mathlib library remain trusted, humans still have to confirm the formal statement matches the original conjecture, and the written paper is not machine checked.
Then there is the model. PSI calls it only "a non-public Anthropic model." Aaronson describes it as an internal Claude model and says he does not know how much of the work came from PSI's harness versus the model itself. TechCrunch reported that Anthropic would not confirm or deny whether Fable 5.2, launched Monday, was the model PSI used. The proof is public. The engine that found it stays private.
