Did AI prove the Aaronson-Ambainis conjecture? What was checked

On 6 November 2026 the startup Physical Superintelligence (PSI) announced a proof of the Aaronson-Ambainis conjecture, a statement about polynomials, open since about 2008, that limits how much faster quantum computers can be on random inputs.¹ If the proof stands, then for yes-or-no questions a quantum computer without special structure in its input can save only polynomially many reads of that input, never exponentially many. PSI says a research system running a non-public Anthropic model found the proof. Its repository records that Lean, a proof assistant, accepted a formal version.³ Scott Aaronson, who posed the conjecture with Andris Ambainis, wrote on 8 November that he has not yet understood the proof but believes it is correct.⁴ The paper is a preprint and has not been peer reviewed, and PSI has not named the model.

The result would not touch Shor's factoring algorithm or the quantum simulation of chemistry, whatever some posts have said since. It concerns one specific kind of advantage, which Aaronson says researchers had already conjectured did not exist.

Below: what the conjecture says, why it limits quantum speedups, what it leaves alone, what PSI reports, what the Lean check does and does not establish, what a reader can tell about how the proof was made, and who is responsible for what. Every source was checked on 9 November 2026.

What is the Aaronson-Ambainis conjecture?#

PSI's own picture is a good one: a polynomial is a dial wired to on-off switches.¹ Each switch is one bit of an input string. Each small group of switches adds a fixed amount to the reading when all of its switches are on, and the largest group has d switches, where d is the polynomial's degree. The reading is guaranteed to stay between 0 and 1 at every setting.

The influence of a switch measures how much it matters. Flip it, square the change in the reading, and average over all settings. PSI's example on four bits is f = 0.1 + 0.5·x4 + 0.2·x1·x2 + 0.1·x3. Flipping bit 4 always moves the reading by 0.5, so its influence is 0.25. Flipping bit 3 moves it by 0.1, for an influence of 0.01. Bit 1 matters only when bit 2 is on, which gives 0.02.

The conjecture says that a bounded dial of low degree always has a switch that matters. Precisely: if the reading has variance at least ε, then some variable has influence at least a fixed power of ε/d, however many variables there are.⁵

The variance condition is needed. Take the average of N bits. It has degree 1 and stays between 0 and 1, and every bit has the tiny influence 1/N². But its variance is also tiny, 1/(4N), so the conjecture asks little of it. What the conjecture rules out is a polynomial whose reading swings widely while each switch stays almost irrelevant.

Before this announcement, the known bounds for general bounded polynomials were exponential in the degree, and the conjecture had been proved only for special classes of polynomials.² Aaronson and Ambainis listed the main evidence in their paper as similar theorems, "besides the fact that all the Fourier analysis experts we asked were confident of it!"⁵

PSI claims the bound in a specific form. A polynomial of degree at most d with values in [0, 1] and variance at least ε has a variable of influence at least (ε/d)^7. A sharper form gives about 0.0025 · ε^(5/2) / d^6.

When was it posed? Reports say 2008 or 2009, and both have a basis. Aaronson wrote in 2019 that "Around 2008, though, I noticed that a solution would follow from a perhaps-not-obviously-related conjecture", and titled that post with the years 2008 to 2019.⁶ The new paper says "The conjecture goes back to a lecture of Aaronson in 2008".² The written paper reached arXiv on 5 November 2009 and appeared in Theory of Computing in 2014, as Conjecture 1.7 there and Conjecture 6 in the arXiv version.⁵ On 8 November Aaronson described it as a conjecture "which Andris and I posed back in 2009".⁴

Why would it limit quantum speedups?#

Quantum algorithms are often measured by queries: how many times they read their input. In 1998 Beals and colleagues showed that after T queries, the probability that a quantum algorithm says yes is a polynomial in the input bits, of degree at most 2T, with values between 0 and 1.⁴ That is exactly the kind of dial the conjecture describes, and it gives an ordinary computer a way to imitate the quantum one:

The paper works out the cost with its exponent of 7: at most (4T)^8 · ε^-14 · δ^-8 classical queries to estimate the probability to within ε on all but a δ fraction of inputs.² That is a large polynomial in T, but it is a polynomial. PSI's summary is that "on yes-or-no questions, a quantum computer cannot save exponentially many looks unless the string has a rare pattern."¹

The older question behind this is one Fortnow and Rogers asked in 1998: can P be separated from BQP relative to a random oracle?⁴ A random oracle is, roughly, a black box of random data. Aaronson and Ambainis showed that their conjecture has a consequence here: separating BQP from AvgP relative to a random oracle would require proving P ≠ P^#P, itself a major open problem.²

What does it not rule out?#

Quite a lot, and this is where commentary went wrong fastest. On 7 November Pedro Domingos of the University of Washington posted on X: "The dream of quantum supremacy is dead."¹⁷ The same day, Ashley Montanaro of the University of Bristol wrote of being "depressed to see the amount of completely incorrect commentary on its implications".¹⁶

Aaronson's reply is that the result "rules out one particular type of quantum supremacy (namely, for yes-or-no problems relative to random oracles) that we'd already conjectured didn't exist anyway."⁴ His post and the papers name what stays untouched:

• Shor's algorithm. Factoring reduces to finding the period of a function, and a periodic input is about as far from random as an input can be. Aaronson: "It has zero effect, for example, on Shor's factoring algorithm".
• Structured problems in general. Exponential speedups with a promise on the input, such as Simon's problem, are consistent with the conjecture. The paper's abstract says speedups of this size "require structure, such as a promise on the inputs."²
• Simulating physics and chemistry. These, Aaronson writes, generally do not depend on oracle algorithms at all.
• Problems that are not yes-or-no. Yamakawa and Zhandry showed in 2022 that, relative to a random oracle, there are NP search problems that quantum computers can solve and classical ones cannot.¹¹ Their abstract notes that this does not appear to contradict the conjecture.
• Running time. The theorem counts reads of the input. It does not bound the total work, and the simulation above may spend enormous effort deciding which bit to read next.

What exactly did PSI report?#

PSI's post opens: "The Aaronson-Ambainis conjecture is now a theorem."¹ That is PSI's claim. The account it gives, with the paper posted to arXiv as 2611.09773² the same day, runs as follows.

The research system ran on PSI's own infrastructure and used instances of a non-public Anthropic model. In the paper's AI disclosure, those instances served "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."² PSI says the system "had a complete proof of the conjecture during the third day of the run". Appendix A of the paper adds that this proof gave a weaker exponent, 22 where the final version has 7. The exponent then improved to 11 and to 7, each step checked in Lean, after the instances were asked to push on related open problems.

The people are named too. The arXiv listing has one author, David Turturean of PSI. According to PSI, he developed the system, scoped the problem, ran the system on it and prompted the model to write a first draft. The paper states: "The mathematical statements in this paper were produced by AI models." Jim Halverson, a PSI advisor, "audited the proof", and Phiala Shanahan, also an advisor, "commented on the Lean formalization".¹ Aaronson describes the effort as led by Turturean and Halverson;⁴ PSI gives Turturean the lead and Halverson the audit.

PSI's proof draws heavily on human work. PSI says it "follows a plan of Shachar Lovett and Jiapeng Zhang", who left one inequality as a conjecture, and it replaces that inequality with a new one. It also uses David Reimer's Butterfly Lemma from his work on the van den Berg-Kesten conjecture, and results of Agarwal and Ben-David, Kulkarni and Tal, and Filmus, Hatami, Keller and Lifshitz. Appendix A says instances of the model brought in Reimer's work and the dual inequality of Kahn, Saks and Smyth from the literature before any of the paper's main statements was proposed.²

What about the Stanford group? Some coverage blurred this. In August 2026 Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan posted a paper settling the conjecture's prediction for a special case, quantum algorithms working in a limited number of parallel rounds.⁸ They did not claim the full conjecture. After PSI shared its proof with them, they wrote an exposition dated 7 November, whose note says the proof "was then shared with the authors, who worked to understand it and prepare this exposition."⁹ It also says Anthropic's public models were used in that process, and that the authors "did not receive financial compensation from Anthropic or PSI." Aaronson says the new proof "didn't specifically use this summer's proof of AA for small-depth quantum algorithms".⁴

How have experts reacted so far?#

The public reaction we found is short, and it is recent.

Aaronson's post of 8 November is the most detailed. "I haven't yet understood the proof, although I hope to," he writes. "In the meantime, though, I believe the proof is correct for two reasons. Firstly, there's a Lean certificate, and secondly, human experts ( I'm no longer an expert on my own conjecture!) have already gone over it and understood it."⁴ He has reason for care on this problem: in 2019 he blogged about a claimed proof by Nathan Keller and Ohad Klein, who withdrew it weeks later, writing "Unfortunately, our proof contains a serious flaw."⁷ His feelings now, he says, are mixed: satisfied, fatigued, and "Disappointed that humans didn't get to snag this conjecture before the robots did".

Under the post, Sreejata Kishor Bhattacharya, who wrote of giving much of a PhD to the conjecture, knew the Lovett-Zhang approach but not Reimer's lemma, and guessed that AI gains here from knowing the whole literature. Aaronson replied that someone familiar with Reimer's lemma and Agarwal-Ben-David "could plausibly have completed" it.

Blanc and his coauthors told PSI, in a statement PSI published: "This is a huge result."¹ Their exposition, which reworks the proof in four main steps with weaker exponents, is the most substantial outside reading we found. Montanaro's phrase was that the conjecture "has apparently been proved".¹⁶

We found no public comment from Andris Ambainis as of 9 November, and no statement from Anthropic about the model or the run.

What does the Lean check establish?#

Lean is a language in which every step of a proof is checked by a small program, its kernel. The repository³ documents its checks at length. We read the code and the records. We did not rebuild it.

The negative test is worth pausing on. The audit note says "An axiom report is only as reliable as the compiled files that it reads",¹² and the project shows why by building a fake proof that an ordinary build accepts. That is the reason for the replays by separate checkers.

Four things stay outside the check.

Whether the formal statement is the conjecture. A kernel can confirm a proof of whatever statement it is given. The README says that this match "is for a reader to confirm".³ The statement is short and uses only Mathlib definitions,¹⁵ so here is the comparison:

Clause by clause they line up. The two changes are ones the file explains: "degree d" is read as "at most d", and O(1) becomes the number 7. That is our reading of two short texts, and it is no substitute for specialists doing the same. On 8 November an outside contributor opened a pull request that restates the conjecture independently in Lean and derives it from PSI's theorem. Its author calls this "one-way statement entailment under an explicit interpretation". It had not been merged when we checked.

The link to quantum computing. Lean checks the statement about polynomials. The step to quantum algorithms comes from the 2009 paper and from the new paper's Section 1.3, which the repository lists among the parts with no Lean counterpart.¹⁴ Aaronson sums up that argument in a few sentences, but the machine did not check it.

The paper. The README says it "is written for human readers and is not itself machine-checked." A human can follow a text that a kernel never read, and a text can differ from the proof it describes. The map between paper and Lean is, in the audit's words, a guide on which "no machine has checked it".

The foundations and the records. The README lists as trusted "Lean's kernel and compiler, the definitions of Mathlib, and the machines on which the checks ran". The recorded runs are PSI's own, from 22 October and 6 November. "Matching hashes identify the checked inputs; the outputs record what the checkers reported."¹³ Anyone can rerun them with the repository's commands.

What can a reader tell about how the proof was made?#

A formal proof can be judged without knowing where it came from. Credit, cost and how far the method reaches are other questions, and for those the origin matters.

PSI's disclosure is specific in places, above all Appendix A's table of the order in which statements were proposed and proved. Still, a reader cannot tell how much of the direction came from the person who scoped the problem, how much from the system around the model, and how much from the model itself. Since the model is not available to the public, no outsider can run it again.

Two other papers on the conjecture from August show what fuller notes can look like. Blanc and colleagues wrote: "ChatGPT 5.4 was used for literature search, conversions of handwritten notes into electronic ones, proof checking, and copyediting."⁸ Qipeng Liu and Saachi Mutreja, who proved a related parallel-query result, described the prompting that helped, then added that "more open-ended attempts without this direction were not successful."¹⁰ That sentence tells other researchers something about how the result was reached. We have written about why those failures tend to go missing.

Who is responsible for what?#

The documents are clear about this, and the division is worth keeping in view.

• The paper's correctness: David Turturean, who according to the disclosure "reviewed and edited the draft personally, and is responsible for its correctness."²
• The audit: Jim Halverson, by PSI's account. Neither document describes what the audit covered.
• The formal statement's fidelity: whoever reads it. The repository says so.
• The claim that an Anthropic model was used: PSI.
• The model: nothing. A model can be named in a disclosure; it answers for nothing claimed.

Papex's part in this story is small. The Aaronson-Ambainis conjecture page lists PSI's announcement as one AI-assisted claim, with the claimant's own words and the model as the source gives it, as with every entry on /ai-claims. The status shown there is OPEN, because Papex takes status from a named source, here the 2014 paper, and does not judge proofs. A listing is a pointer to a claim. It says nothing about whether the claim is right.

The gap in this story is a record of the making: which version of the work was fixed when, who stood behind it, and what each person and tool is said to have done. No signed Papex record exists for this proof, so everything above rests on PSI's documents. And no record of that kind, on any system, would show that the mathematics is right. Lean and the people reading the proof are doing that work.

What would add to this picture: written checks by specialists or errors found by them, peer review, an independent check of the formal statement, a comment from Ambainis, and a model name and version from PSI or Anthropic.

A note on interests: the model PSI reports using is Anthropic's, and this post was drafted with Claude, an Anthropic model. Readers should weigh it with that in mind and check the sources below.

Sources#

1. PSI, A proof of the Aaronson-Ambainis conjecture (6 November 2026), checked 9 November 2026 ↩ a b c d e f
2. David Turturean, A proof of the Aaronson-Ambainis conjecture, arXiv:2611.09773 (6 November 2026), 60 pages, checked 9 November 2026 ↩ a b c d e f g h i
3. physical-superintelligence/aaronson-ambainis on GitHub, README, commit 2a6ceae, checked 9 November 2026 ↩ a b c
4. Scott Aaronson, Aaronson-Ambainis Conjecture proved! (By AI, of course), with comments (Shtetl-Optimized, 8 November 2026), checked 9 November 2026 ↩ a b c d e f g h
5. Scott Aaronson and Andris Ambainis, The Need for Structure in Quantum Speedups, arXiv:0911.0996, version 3; Theory of Computing 10 (2014), checked 9 November 2026 ↩ a b c
6. Scott Aaronson, The Aaronson-Ambainis Conjecture (2008-2019) (Shtetl-Optimized), checked 9 November 2026 ↩
7. Nathan Keller and Ohad Klein, Quantum speedups need structure, arXiv:1911.03748 (withdrawn 2 December 2019), checked 9 November 2026 ↩
8. Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, Quantum Speedups Require Structure or Depth, arXiv:2608.19158 (19 August 2026), checked 9 November 2026 ↩ a b
9. Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, Proof of the Aaronson–Ambainis Conjecture: An Exposition (7 November 2026), checked 9 November 2026 ↩
10. Qipeng Liu and Saachi Mutreja, Parallel Quantum Advantage with Limited Adaptivity Requires Structure, arXiv:2608.20297 (20 August 2026), checked 9 November 2026 ↩
11. Takashi Yamakawa and Mark Zhandry, Verifiable Quantum Advantage without Structure, arXiv:2204.02063, checked 9 November 2026 ↩
12. Repository note, Axiom audit, checked 9 November 2026 ↩
13. Repository note, Verification, checked 9 November 2026 ↩
14. Repository note, Paper to Lean, checked 9 November 2026 ↩
15. Repository file, Conjecture.lean, checked 9 November 2026 ↩
16. Ashley Montanaro on X (7 November 2026), read through a public mirror of the post, checked 9 November 2026 ↩ a b
17. Pedro Domingos on X (7 November 2026), read through a public mirror of the post, checked 9 November 2026 ↩