Physical Superintelligence (PSI), a US lab, published on 6 November a proof of the Aaronson–Ambainis conjecture together with a Lean 4 formalisation anyone can re-run. The conjecture has been open since 2008 and is counted among the central problems of quantum query complexity. PSI says the proof came from a research system it builds internally, running instances of a non-public Anthropic model: a complete proof existed on day three of the run, Lean accepted it, and the system was then pointed at related open problems, improving the result twice.
What the conjecture actually says
Shor's algorithm factors numbers quickly because the input hides a repeating pattern. Aaronson and Ambainis asked the harder question: can a quantum computer be exponentially faster on random inputs, where no such structure exists? They reduced it to pure mathematics. After T queries, a quantum algorithm's acceptance probability is a polynomial in the input bits of degree at most 2T, with values in [0,1]. If such a polynomial always has an influential variable — one bit whose flip moves the value by a non-negligible amount — then a classical machine can imitate the quantum one with polynomially many queries. On yes/no questions over random strings, there is no exponential quantum speedup.
PSI's new inequality: for a polynomial f of degree d bounded in [0,1] with variance v, some bit i satisfies Inf_i(f) ≥ c·v^(5/2)/d^6 ≥ (v/d)^7, with c = 8√15/(125π⁴) ≈ 0.0025. Earlier general bounds decayed exponentially in the degree, which is exactly why the question stayed open. The proof follows a plan by Shachar Lovett and Jiapeng Zhang and replaces their one conjectured inequality with a new one, proved by pairing switch settings one-to-one through a determinant; David Reimer's Butterfly Lemma supplies a weaker pairing.
What you can check yourself
The formalisation is public and pinned to Lean 4.33.0 and Mathlib v4.33.0. `make check` runs an import check, a static audit (no `sorry`, `axiom` or `native_decide` in the library), the build, and an axiom report: the four final theorems rest only on propext, Classical.choice and Quot.sound. `make replay` re-checks the kernel with leanchecker — the README quotes roughly 7.4 GB and 11 minutes on one thread — and a second kernel, lean4lean, plus a comparator run are also reported. The repository was at one commit and six stars when the first analyses appeared, and is Apache 2.0.
What Lean cannot check
- **Statement fidelity.** The README says whether the Lean statement `PrintedConjecture` matches the conjecture as printed is left for a human reader to confirm. A valid proof of a subtly weaker statement proves the wrong thing. - **One unformalised input.** A hypothesis from Agarwal and Ben-David, `FbsDegreeBound`, is an input to one theorem and is not itself formalised. - **The paper.** The manuscript is not machine-checked. It was drafted by the model and reviewed by the person who ran the system. - **Peer review.** There is none. Jim Halverson audited the proof internally; Phiala Shanahan commented on the formalisation. - **Reproducibility of the run.** The model is non-public, so only the output can be examined, never the process.
Neither Scott Aaronson nor Andris Ambainis has commented publicly. Four Stanford researchers — Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, who proved a special case in August for algorithms with a fixed number of parallel rounds — are quoted on PSI's page calling it "a huge result" whose proof brings several lines of work together "in a rather magical way." Those quotes are relayed by PSI, not published by the researchers themselves.
Why it matters beyond the theorem
This is the third PSI release in a month in the same shape: a formal artefact anyone can verify, wrapped around a claim nobody outside has yet read closely. That shape is becoming a template, and for engineers it is a good one — pin the toolchain, audit the axioms, ship a replay target, and publish an explicit list of what is not checked. The remaining gap is not technical. It is the weeks of expert reading needed to establish that the formal statement is the problem people care about.
Three signals will settle it: a public assessment from Aaronson or Ambainis, the shorter exposition the Stanford group is said to be writing, and an arXiv or journal submission. Until then the honest description is a machine-checked proof of a statement that still needs a human to match it to the conjecture.
