On November 6, 2026, the startup Physical Superintelligence (PSI) said a research system it developed internally, "running a non-public Anthropic model," had found a proof of the Aaronson-Ambainis conjecture. PSI's post opens with one sentence: "The Aaronson-Ambainis conjecture is now a theorem." The paper is on arXiv, with David Turturean as sole author. (PSI post, arXiv paper)
What is the Aaronson-Ambainis conjecture?
The conjecture was posed by Scott Aaronson and Andris Ambainis, and PSI describes it as open since 2008. In plain terms, PSI says, it concerns when quantum computers can be exponentially faster than ordinary ones. Most dramatic known speedups rely on structure in the input. Shor's 1994 factoring algorithm, for example, exploits a repeating pattern. The open question was whether quantum computers can be exponentially faster on random inputs with no such structure.
Speed here is measured in "looks," how many times a computer reads its input. With the proof, PSI says, "on yes-or-no questions, a quantum computer cannot save exponentially many looks unless the string has a rare pattern."
According to the paper's abstract, superpolynomial quantum speedups in the query model "require structure, such as a promise on the inputs." The paper calls the proof "elementary."
How the AI found the proof
The paper's AI disclosure states: "The mathematical statements in this paper were produced by AI models." Instances of a non-public Anthropic model served within a harness, according to the paper, "to search for existing ideas, to propose new ideas, to combine and test these ideas, and to supervise the work and the communication between other instances." Turturean scoped the problem, built the harness, ran it on PSI's infrastructure, prompted the model to write a first draft, and reviewed and edited it. He "is responsible for its correctness," the paper says.
PSI says the system had a complete proof during the third day of the run, and that Lean, a proof assistant in which a computer checks every step, accepted it. The system then improved the result twice, and Lean accepted the final version. Per On The Wire's reading of the paper's timeline, the exponent in the bound went from 22 to 11 to 7. In the paper's statement of the original conjecture, the final bound says some variable has influence of at least (ε/d) to the seventh power. PSI says the proof follows a plan of Shachar Lovett and Jiapeng Zhang and builds on David Reimer's Butterfly Lemma. (On The Wire)
What the proof does not show
Aaronson addressed the reach of the result in a blog post on November 8, 2026. The proof "doesn't kill quantum supremacy, or change how we build quantum computers," he wrote. It "has zero effect, for example, on Shor's factoring algorithm" and "zero effect on the simulation of quantum physics and chemistry." It rules out a class of quantum speedups, he said, "that most of us didn't believe would exist anyway." (Aaronson's blog)
The Quantum Insider's summary notes similar limits. The result lets a conventional computer estimate a quantum algorithm's probability of answering yes for most random inputs, within a chosen margin of error. It does not guarantee an accurate estimate for every input, and it counts how often a computer reads its data, not all the work required. (The Quantum Insider)
Is the proof correct?
The preprint has not been peer reviewed, On The Wire reports. The Lean formalization is public on GitHub, and On The Wire reports that its README says whether the Lean statement matches the conjecture "is for a reader to confirm." The same README, per On The Wire, says the paper itself is not machine-checked. (GitHub repository)
Aaronson wrote that he has not yet followed the argument himself. "I haven't yet understood the proof, although I hope to. In the meantime, though, I believe the proof is correct for two reasons. Firstly, there's a Lean certificate, and secondly, human experts ... have already gone over it and understood it." He also wrote that he was "Disappointed that humans didn't get to snag this conjecture before the robots did."
Four researchers who in August 2026 settled a special case, covering algorithms that look at their input in a fixed number of parallel rounds, have read the proof and are writing a shorter exposition for experts, PSI says. PSI names them as Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan. They told PSI: "This is a huge result. It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups." In comments on Aaronson's blog, Blanc wrote that this felt like something humans could have done in coming years, but "this particular proof of AA feels hard to find: Personally, I doubt I would have arrived at it even if I knew every relevant result in the literature."
PSI credits advisor Jim Halverson with auditing the proof and advisor Phiala Shanahan with commenting on the Lean formalization.
Why it matters for Anthropic
PSI says only that "instances of a non-public Anthropic model were used in the run," so readers cannot try the model that did the work. PSI has not named the model, CuriousLM reports. Aaronson's blog calls it "an internal Claude model" and says "What role the harness played, compared to the internal model, is something I don't know." (CuriousLM)
Aaronson wrote that longstanding open problems in quantum computing theory and math "are dropping like flies" in the current era of AI. He also wrote that he was surprised the conjecture was missing from "OpenAI's Mathocalypse dump a few weeks ago." For Anthropic, it is a public example of an outside company using one of its unreleased models for frontier research, with a human taking responsibility for the result.
Earlier llms.blog coverage includes Claude helping solve a phage vault particle structure and Axiom's Lean proof of the finite simple groups theorem. See also Anthropic's recent agent memory research.
Sources
- PSI: the Aaronson-Ambainis conjecture is now a theorem
- arXiv paper by David Turturean
- On The Wire on PSI's Lean-checked proof claim
- Lean formalization on GitHub
- Scott Aaronson's blog post, November 8, 2026
- The Quantum Insider on the AI-assisted proof
- CuriousLM on the unnamed model
- llms.blog: Claude and the phage vault particle structure
- llms.blog: Axiom's Lean proof of the finite simple groups theorem
- llms.blog: Anthropic's agent memory research
