Aaronson-Ambainis conjecture: PSI says an Anthropic model proved it, Lean-checked

A small research company says an AI system built on a non-public Anthropic model has proved the Aaronson-Ambainis conjecture, a question about when quantum computers can be exponentially faster than ordinary ones that has been open since 2008. The company, Physical Superintelligence (PSI), published the result on 6 November 2026 together with a paper, and says Lean, a proof assistant, accepted the formal proof. The claim is new, it has not been through peer review, and the paper's own scope is narrower than the headlines may suggest.

Key points

• PSI says a research system it built, running instances of a non-public Anthropic model, produced a complete proof of the Aaronson-Ambainis conjecture "during the third day of the run" (PSI, 6 November 2026).
• The main theorem and the formulation of the original conjecture were formalized in Lean and checked by its kernel, according to the paper as described by The Quantum Insider.
• The result concerns queries, meaning how many times an algorithm reads its input. It does not bound total computing time.
• It has not been peer reviewed. Researchers at Stanford who had proved a special case in August 2026 are reading it and are writing a shorter exposition, PSI says.
• David Turturean, a PSI staff member, led the work and, per PSI, "is responsible for the paper's correctness".

What happened

On 6 November PSI posted a research note titled "A proof of the Aaronson-Ambainis conjecture". It says "a research system developed internally at Physical Superintelligence (PSI), running a non-public Anthropic model" found the proof. According to the note, instances of the model were used in a run on PSI's own infrastructure, the system had a complete proof on the third day, and Lean accepted it. PSI then set the system to work on related open problems; it says the system improved the result twice and that Lean accepted the final version.

The people involved are named in the note. Turturean developed the research system, scoped the problem, ran the system and then prompted the model to package the results into a first draft of the paper, which he reviewed. Jim Halverson, listed as an advisor, audited the proof, and Phiala Shanahan, also an advisor, commented on the Lean formalization. The Quantum Insider, which covered the announcement the same day, reports that the paper was posted on GitHub.

PSI also quotes the Stanford group of Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, who in August 2026 had proved the conjecture's prediction for algorithms that look at their input in a fixed number of parallel rounds. PSI says they have been reading the new proof, sent comments, and are writing a shorter exposition for experts. It quotes them calling it "a huge result". That is PSI's account of a private exchange; we have not seen a statement from the Stanford researchers themselves. We also found no public comment from Scott Aaronson or Andris Ambainis at the time of writing.

Background

In 1994 Peter Shor found a quantum algorithm that factors large numbers far faster than any known method on ordinary computers. It works because the problem hides a repeating pattern, and a quantum computer can find how often the pattern repeats. Most dramatic quantum speedups known rely on structure of this kind: a promise that the input has a rare regularity.

The open question was what happens without that promise. Can a quantum computer be exponentially faster on random inputs, which almost never have structure? Aaronson and Ambainis approached this with pure mathematics. They stated a conjecture about bounded low-degree polynomials and showed that, if it is true, quantum algorithms get at most a polynomial advantage on random inputs. Researchers have counted it among the central open problems of quantum complexity theory, and PSI's paper traces it to a 2008 lecture by Aaronson.

Progress had come in pieces. The note lists special cases proved by Ashley Montanaro, by Paata Ivanisvili, by Nikhil Bansal, Makrand Sinha and Ronald de Wolf, and by Francisco Escudero Gutierrez, as well as the work of Shachar Lovett and Jiapeng Zhang, whose plan PSI says its proof follows. Because the question stayed open for 18 years despite that work, expert checking of a new proof will matter, even with a formal check behind it.

How it works

Quantum speedups are measured in "looks", the number of times an algorithm has to read its input, a long string of 0s and 1s. An ordinary computer reads one bit per look. A quantum computer's look can be spread in superposition over many positions. When the input is promised to repeat, as in Shor's algorithm, a quantum computer needs exponentially fewer looks than any ordinary computer.

After T looks, the probability that a quantum computer answers "yes" is a polynomial in the input bits of degree at most 2T, with values between 0 and 1. That was shown by Beals, Buhrman, Cleve, Mosca and de Wolf. So an ordinary computer that wants to imitate the quantum one has to estimate the value of such a polynomial while reading only a few bits.

The conjecture is about influence. The influence of a bit is how much the polynomial's value changes, on average, when that bit is flipped. Aaronson and Ambainis conjectured that some bit always has influence at least a fixed power of v/d, where v measures how much the polynomial varies across inputs and d is its degree. An ordinary computer can then repeatedly look at an influential unread bit until the remaining variation is small, and output the average as its prediction.

PSI states the bound it proves as Inf_i(f) at least c v^(5/2) / d^6, which is at least (v/d)^7, with c = 8^15 / (125 pi^4), about 0.0025. It says earlier bounds for general polynomials decayed exponentially in the degree. Its proof follows the Lovett and Zhang plan, replacing one inequality they had left as a conjecture with a new inequality proved in the manuscript, using a pairing of input settings produced by a determinant.

What it means

The headline consequence is about structure. On yes-or-no questions about random inputs, a quantum computer cannot save exponentially many looks. PSI puts it as: "an ordinary computer can predict the quantum computer's probability of saying yes, up to a small error, for all but a small fraction of strings", with the number of looks growing as a fixed power of T rather than exponentially. For quantum algorithm research that points effort toward problems whose structure offers an advantage, which The Quantum Insider notes the theorem supports without deciding which applications will deliver useful speedups.

The limits matter as much as the result. The theorem is about queries, not running time. It does not say conventional computers can efficiently reproduce what quantum computers do, and it does not touch the commercial case for quantum machines. It covers acceptance probabilities on most inputs, for a fixed accuracy and a fixed allowance for exceptional inputs.

For AI, this is another case where a lab or company reports a model contributing to a hard mathematical result. We have covered Anthropic and Theorem's Claude-driven proofs and OpenAI's claim about the exponential time hypothesis. What is different here is the formal check. A Lean kernel accepting a proof means each logical step has been verified by software, so reviewers can focus on whether the formal statement matches the conjecture people mean, rather than on every line of the argument. The Quantum Insider's report makes the same point: humans still have to confirm that the formalized statement matches the original conjecture, and the prose of the paper is not itself machine-checked.

What we don't know yet

• Which Anthropic model was used. PSI calls it non-public and gives no name, and we have not seen a statement from Anthropic.
• How much of the work was the model's and how much the system's design and the researchers' prompting. PSI describes the system as its own and credits Turturean with scoping the problem and drafting the paper, but gives no breakdown.
• Whether experts accept it. The paper is not peer reviewed, and the Stanford exposition PSI mentions has not appeared.
• Whether the Lean statement is a faithful rendering of the conjecture, which is the part human reviewers must check.
• How much compute the three-day run used. PSI's note does not state a cost in the parts we read.

What to watch next

Watch for the shorter exposition PSI says the Stanford group is writing, for any statement from Aaronson or Ambainis, and for an arXiv or conference submission that starts formal review. Watch also for a public Lean repository others can build and inspect, and for any improvement to the exponent in the bound, which The Quantum Insider says remains open to strengthening. If Anthropic comments on the model, that will say more about what such systems can do.

Sources

• PSI: A proof of the Aaronson-Ambainis conjecture (primary source)
• The Quantum Insider: AI-Assisted Proof Settles Longstanding Question About Quantum Speedups
• Girish, Mittal, Nehoran and Raz, Distributional Variants of the Aaronson-Ambainis Conjecture (arXiv 2402.13952), background on why the conjecture matters