What was actually proved

The conjecture is a statement about polynomials that turns out to govern quantum speedups. A quantum algorithm that reads its input T times answers yes with a probability that is a polynomial in the input bits, of degree at most 2T, with values between 0 and 1. Aaronson and Ambainis conjectured in 2008 that any such non-constant polynomial has at least one bit with large influence: flipping that bit moves the polynomial's value substantially on average. If that is true, an ordinary computer can imitate the quantum one by reading influential bits one at a time and stopping once the remaining bits barely matter, and the number of reads grows polynomially rather than exponentially.

PSI's announcement states the bound it proved. With v measuring how much the polynomial's value varies and d its degree, some bit has influence at least c·v^(5/2)/d^6, where c is about 0.0025. Earlier general bounds decayed exponentially in the degree, which is why the conjecture stayed open through a series of special cases, most recently the Stanford group's August 2026 result for algorithms that read their input in a fixed number of parallel rounds. PSI says its proof follows the route Lovett and Zhang laid out, and closes the one inequality they had left unproved.

What Lean settles, and what it does not

The Lean acceptance is the reason this announcement deserves more weight than a benchmark screenshot. A proof assistant does not grade on plausibility. It checks each step of a formal argument, and PSI says the final version, improved twice after the first complete proof, passed. The conjecture has attracted an unsuccessful proof attempt before: a claimed proof posted in 2019 was withdrawn within weeks after a flaw was identified, according to the historical account cited by MadRobot. A machine-checked formalization is specifically the kind of evidence that history argues for.

The machine check still leaves an important question outside the proof itself. Lean verifies the formal statement placed in front of it. Confirming that PSI's formal statement faithfully captures the original Aaronson-Ambainis conjecture is a reading task for human experts, not a kernel task. PSI says the Stanford group that proved the special case has been reading the proof, has sent comments and is preparing a shorter exposition for experts. That is meaningful external scrutiny, but it is not yet independent publication or formal acceptance by the wider research community.

The second limit is simpler. The model used in the research run is described only as non-public. Nobody outside PSI and Anthropic can identify or independently run that model from the information published. PSI's contribution statement also makes clear that this was not an autonomous discovery: a human designed the research system, scoped the problem, operated it and reviewed the resulting paper. This is evidence about what an unreleased Anthropic model can contribute inside a purpose-built research system, not a capability any reader can independently reproduce this week.

Sources

  1. [1] Physical Superintelligence (PSI), "A proof of the Aaronson-Ambainis conjecture", research announcement, published November 6, 2026 (the proof claim, the third-day timeline, Lean acceptance and two improvements, the stated bound with c about 0.0025, the Lovett-Zhang plan and determinant-based pairing, the contributions, and the Stanford group's reading and exposition)Read source
  2. [2] Physical Superintelligence, public repository "aaronson-ambainis", GitHub, read November 6, 2026 (the manuscript and Lean 4 formalization; the repository's recorded static audit finds no "sorry" placeholders and no added axioms in the library sources — the only "sorry" instances sit in a comparator challenge file that no library file imports; "#print axioms" for the four final theorems lists only the standard Lean principles propext, Classical.choice and Quot.sound; declarations replayed through the Lean kernel and, as a second implementation, lean4lean; the repository itself states that confirming the formal statement matches the printed conjecture is a reader's task)Read source
  3. [3] Unite.AI, "PSI Reports Machine-Checked Proof of Aaronson-Ambainis Conjecture", November 6, 2026 (repository audit details as reported: no proof placeholders or added axioms, replay through Lean's kernel and lean4lean, and the stated limit that a reader must still confirm the formal statement matches the printed conjecture)Read source
  4. [4] MadRobot, "Anthropic AI proved Aaronson-Ambainis conjecture, startup says", November 6, 2026, 20:18 UTC (no peer review yet; manuscript and formalization public on GitHub; AI models produced the statements, first draft and formalization per the repository notes; the 2019 claimed proof and its withdrawal)Read source
  5. [5] Scott Aaronson, Shtetl-Optimized, "The Aaronson-Ambainis Conjecture (2008-2019)", November 17, 2019, with updates (the claimed proof by Nathan Keller and Ohad Klein was announced there and then retracted, after Paata Ivanishvili uncovered a fatal flaw in Lemma 5.3 — the primary record of the 2019 withdrawal)Read source