On November 6, 2026, the startup PSI (Physical Superintelligence) announced a proof of the Aaronson-Ambainis conjecture. The conjecture, about the limits of quantum computers, had been unsolved since 2008. PSI says its research system, running a non-public Anthropic model, produced a complete proof on the third day of its run. Lean, a program that checks every step of a proof, accepted it.
The same day, PSI posted the paper and the formal proof, written in Lean, on GitHub, a code-sharing site. The formal proof holds 648 machine-checked theorems, with no step left as a placeholder and no added axiom, or unproved assumption. No journal has reviewed the paper yet. PSI says the Stanford team that proved a special case in August is now writing a shorter version for experts.
The question behind the conjecture
Quantum computers beat ordinary ones by huge margins on some problems. In 1994, Peter Shor found a quantum algorithm that breaks large numbers into prime factors far faster than any known method for ordinary computers. Like most dramatic quantum speedups, it relies on structure: the input is guaranteed to hide a repeating pattern.
Computer scientists Scott Aaronson and Andris Ambainis asked what happens without that guarantee. They counted cost in reads: how often a computer must look at its input, a string of 0s and 1s, to answer a yes-or-no question. On structured inputs, a quantum computer can need exponentially fewer reads than an ordinary one. Nobody knew if the same held for random strings, which almost never carry a pattern.
They turned the question into pure math. A quantum algorithm’s chance of answering yes can be written as a polynomial, a formula built from the input bits. In their paper, they “conjecture that every bounded low-degree polynomial has a ‘highly influential’ variable.”
Bounded means the value stays between 0 and 1, and low-degree means each term multiplies only a few bits. An influential bit is one whose flip moves the value noticeably, on average. If the conjecture holds, an ordinary computer can imitate the quantum one on most inputs by reading the influential bits first, with only polynomially more reads. So on random inputs, a quantum computer could not save exponentially many reads.
Eighteen years of attempts
“I never managed to solve this problem,” Aaronson wrote on his blog, Shtetl-Optimized, about the random-input question. “Around 2008, though, I noticed that a solution would follow from a perhaps-not-obviously-related conjecture.” PSI’s paper traces the idea to a lecture he gave that year at the Banff International Research Station. The paper with Ambainis went up on arXiv, an open archive, on November 5, 2009, and appeared in the journal Theory of Computing in 2014.
Aaronson wrote that the problem had “acquired a life of its own” among experts on Boolean functions, the math of such yes-or-no questions. “Ryan O’Donnell, Guy Kindler, and many others had a stab,” he added, and he once got Terry Tao to spend “an hour or two on the problem.”
The post, titled “The Aaronson-Ambainis Conjecture (2008-2019),” went up on November 17, 2019, about a week after Nathan Keller and Ohad Klein posted a claimed proof. An update at the top reports that they retracted it because of “what currently looks like a fatal flaw in Lemma 5.3, uncovered by Paata Ivanishvili.” A lemma is a step inside a proof.
On August 19, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan of Stanford University settled the problem for parallel quantum algorithms. These read their input in a fixed number of rounds.
On September 28, Uma Girish, Kunal Mittal, Barak Nehoran and Ran Raz showed that variants of the question, with inputs drawn at random in other ways, all stand or fall with the original. They called it “a longstanding conjecture in quantum complexity theory.”
Three days, then two improvements
PSI ran the search on its own infrastructure, with a research system built by staff member David Turturean. The paper’s AI disclosure says copies of a non-public Anthropic model, called instances, worked inside it “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.”
A timeline in the paper’s appendix says the first complete proof was written down on the third day, then checked in Lean. That version proved the conjecture, but weakly. In Aaronson and Ambainis’s terms, it guaranteed the influential bit an influence of at least (ε/d) to the power 22. Here ε measures how much the polynomial varies and d is its degree.
The conjecture only asks for some fixed power, and a smaller power is a stronger result. PSI then set the instances on related open problems. Along the way, the result was tightened twice: to a power of 11, then 7. Lean checked each version.
The proof follows a plan by Shachar Lovett and Jiapeng Zhang, who had left one inequality unproved, and supplies a new one in its place. It also builds on the Butterfly Lemma, a tool from David Reimer’s 2000 proof of the van den Berg-Kesten conjecture.
PSI says people ran the project: Turturean scoped the problem and ran the search. He also prompted the model to draft the paper, reviewed it and “is responsible for the paper’s correctness.” Advisor Jim Halverson audited the proof, and advisor Phiala Shanahan commented on the Lean files.
On October 23, PSI had already posted results on five open problems in quantum information theory, obtained with its AI research system. At least one of them is partial.
How the proof was checked
Lean accepts a proof only if a small core program, the kernel, verifies every step. The company Axiom Math used Lean in October to turn a 15,000-page proof into computer-checked code.
PSI’s repository holds 84 Lean files, called modules, with 761 declarations, the named definitions and results. Of those, 648 are theorems. A static audit of the library’s source code found no “sorry”, Lean’s placeholder for a missing proof.
A checker called leanchecker re-ran every declaration through the Lean kernel, and lean4lean, an independent version of Lean’s checker, did the same. A tool called Comparator matched the four final theorems against the formal statement, the conjecture as written in Lean. It had them re-run by nanoda, a checker written in Rust.
The checks have stated limits. The formal statement is a short definition called PrintedConjecture. The “Trust boundary” section of the README, the repository’s guide page, says that whether it “says what the conjecture says is for a reader to confirm.”
The README prints the definition in full, and a separate file sets the original wording beside it. The paper written for human readers “is not itself machine-checked.”
Mostly one source, and a narrow result
Almost everything here comes from PSI: the announcement, the paper and the code. The paper is a preprint, posted without peer review. PSI is a venture-backed public benefit corporation, a for-profit company with a stated public mission. It reports more than $58 million raised, and the result comes from its own system.
The Stanford group’s verdict also reached the public through PSI, which quotes the four researchers as writing: “This is a huge result. It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups.” We found no statement from them on their own channels.
The paper thanks Aaronson for referring PSI to that team. As of the morning of November 7, his blog had no post about the proof.
The result is also narrow. It counts reads of the input, not total computing time, as Matt Swayne noted on November 6 in The Quantum Insider. It covers yes-or-no questions on random inputs, so structured problems such as Shor’s factoring are untouched.
Swayne also wrote that the account “does not establish how consistently the system could solve other longstanding problems.” Outsiders can inspect the proof but cannot rerun the search: the model is not public.
What it means
The proof arrived on the third day of a run, after 18 years of human effort. How it was checked matters as much as how fast it came. The 2019 proof collapsed over one flawed lemma, the kind of hidden error a Lean proof re-run by independent checkers is built to catch.
That leaves experts a narrower question: does one short formal definition say what Aaronson and Ambainis meant? They must also trust Lean, its math library and the machines that ran the checks.
Other AI claims of this kind came in October. OpenAI said its AI had disproved the Exponential Time Hypothesis, an assumption about how hard certain problems are. Anthropic said its model Claude had designed quantum circuits up to 39 times cheaper than the best published ones. Like OpenAI’s claim, this one comes with its formal proof in public.
The Stanford group’s shorter write-up for experts has not appeared yet. Any specialist can already compare the formal statement with the conjecture. We found no public comment from Aaronson or Ambainis as of November 7. PSI has not said whether the paper will go to a journal, or which model ran the search.
Sources
- A proof of the Aaronson-Ambainis conjecture, PSI, November 6, 2026
- The Aaronson-Ambainis conjecture: paper and Lean 4 formalization, PSI on GitHub, November 6, 2026
- The Need for Structure in Quantum Speedups, Scott Aaronson and Andris Ambainis, arXiv, November 5, 2009
- The Aaronson-Ambainis Conjecture (2008-2019), Shtetl-Optimized, November 17, 2019
- Quantum Speedups Require Structure or Depth, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, arXiv, August 19, 2026
- Distributional Variants of the Aaronson-Ambainis Conjecture, Uma Girish, Kunal Mittal, Barak Nehoran and Ran Raz, arXiv, September 28, 2026
- Five results on Open Quantum Problems, PSI, October 23, 2026
- AI-Assisted Proof Settles Longstanding Question About Quantum Speedups, The Quantum Insider, November 6, 2026
Header image: timeline by MACCUS, data from Aaronson (Shtetl-Optimized, 2019), arXiv and PSI (October 23 and November 6, 2026)
