THE ESSENTIALS IN 30 SECONDS

  • Physical Superintelligence (PSI) announced on 6 November that its research system, which it says ran a non-public Anthropic model, found a proof of the Aaronson–Ambainis conjecture.
  • The public Lean 4 code contains no unproven placeholders or added axioms, but whether its formal statement matches the original conjecture is left to human readers.
  • No journal peer review has been reported; four researchers quoted by PSI are reading the full proof and preparing a shorter exposition.

Physical Superintelligence (PSI), a start-up that applies AI to physics research, announced on 6 November that its internal research system had produced a complete proof of the Aaronson–Ambainis conjecture. According to Unite.AI and Silicon Report, PSI says the system ran instances of a non-public Anthropic model and reached the proof on the third day of a run, after which it was pushed to two further improvements. The public repository credits "AI models" with the statements, first draft and Lean code but does not name a provider, so the Anthropic link rests on PSI's announcement.

What the conjecture says

Quantum computers deliver dramatic speedups on some problems, such as factoring, that have hidden structure. The conjecture, which Scott Aaronson and Andris Ambainis formulated in 2008, concerns the opposite case. In mathematical terms, it says that every bounded, low-degree polynomial on Boolean inputs has at least one variable with substantial influence on its output. Aaronson and Ambainis showed that this would imply that any quantum algorithm making a given number of queries can be imitated on most inputs by a classical algorithm needing only polynomially more queries. In plain language: no exponential quantum advantage on random, unstructured data. It is a hard problem: a 2019 preprint claiming a proof was withdrawn after a flaw was found, as Aaronson reported on his blog.

What has been checked, and what has not

The repository, which pins Lean 4.33.0 and Mathlib, states that the library uses no "sorry" placeholders or extra axioms and that its kernel replays passed independent checkers. The README is explicit about limits: readers must confirm that the formal statement, called PrintedConjecture, faithfully captures the conjecture, and the human-readable paper is not machine-checked. One variant giving a sharper constant relies on an external result that is not formalized; the README says the main theorems do not depend on it.

David Turturean of PSI built the system and is named as responsible for the paper's correctness. PSI's materials quote Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, who proved a related special case in August, calling the work "a huge result"; they are preparing a shorter write-up. No journal review or public response from Aaronson or Ambainis had been reported by the time of writing. The argument builds on a strategy by Shachar Lovett and Jiapeng Zhang, replacing an inequality their plan had left unproven.