Physical Superintelligence says its in-house research system has proved the Aaronson-Ambainis conjecture, a question about the limits of quantum computers that has stood open since 2008. The startup, known as PSI, announced on November 6 that the system found the proof on the third day of a run on its own infrastructure, running a non-public Anthropic model, and that the Lean proof assistant accepted every step. The paper and the full Lean formalization are public, so anyone can replay the machine check.
The conjecture, in plain terms
The question starts with Peter Shor’s 1994 factoring algorithm, which showed a quantum computer could crack problems an ordinary computer finds hopeless — but only because the input hides a repeating pattern to exploit. Aaronson and Ambainis asked the opposite question: when the input is random, with no hidden pattern to find, can a quantum computer still be exponentially faster?
Their conjecture said no. They showed that if it is true, a quantum computer is at most polynomially faster on random inputs, because an ordinary computer can predict the quantum machine’s answer without reading exponentially more of the input. The claim rested on pure mathematics: every bounded low-degree polynomial, they said, must have one highly influential variable.
Proving that claim means showing an ordinary computer can estimate what a quantum computer would answer, up to a small error, for all but a small fraction of inputs. The number of looks the ordinary computer needs grows like a fixed power of the quantum machine’s looks, not exponentially. On yes-or-no questions, quantum speedups need structure.
How the proof was found
PSI says the proof came from a research system it built internally, led by member of technical staff David Turturean, who scoped the problem, ran the system and reviewed the draft it produced. The system had a complete proof during the third day of the run, and Lean, a proof assistant in which a computer checks every step, accepted it.
The team then set the system on related open problems, improving the result twice along the way; Lean accepted the final version. The bound is explicit: some bit’s influence is at least a constant, about 0.0025, times variance to the power 5/2 over degree to the power 6 — and at least the variance-over-degree ratio to the power 7.
The proof follows a plan by Shachar Lovett and Jiapeng Zhang, who had left one inequality of their plan as a conjecture. PSI replaced it with a new inequality, proved by pairing input settings one to one using a determinant. David Reimer’s Butterfly Lemma gives a weaker pairing; PSI’s version also limits how often paired settings agree on each switch.
What was checked, and what was not
The formalization is public in PSI’s GitHub repository, released under Apache 2.0. It holds four final theorems with no placeholders and no added axioms, and the declarations were replayed through Lean’s kernel and through lean4lean, an independent implementation of Lean’s type checker. A sandboxed comparator run accepted the final theorems and rejected deliberately wrong ones.
That check has stated limits. The human-readable paper is not itself machine-checked, and a reader must still confirm that the formal statement, labelled PrintedConjecture, matches the conjecture as Aaronson and Ambainis printed it. The Lean kernel, its compiler, the Mathlib library and the checking hardware all remain part of the trusted base.
No journal has reviewed the paper yet. But the four Stanford researchers who settled a special case in August — Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan — have been reading the full proof, have sent comments, and are writing a shorter exposition for experts. They called it “a huge result.”
Our Read
This is different from the usual AI-does-science announcement, and the difference is the check. OpenAI recently claimed AI-written proofs for three hard problems, and AI agents have already verified thousands of pages of pure mathematics — but a preprint is a claim, while a Lean-checked proof is an artifact anyone can replay. PSI published the artifact, not just the headline.
That matters because the model cannot be inspected. PSI says it ran instances of a non-public Anthropic model, and Anthropic has not said which model it was or what access PSI had. The proof stands on the machine check, so the opacity does not sink the result — but nobody else can rerun the discovery, only verify what it produced.
The timing also fits a pattern. Independent testing found Anthropic’s models improving about twice as fast as a year ago, and the labs’ research systems now do the work, with humans scoping problems and checking drafts. PSI’s three-day run is what that looks like when it works: a small team, a frontier model, and a problem with a checkable answer.
Why It Matters
If the proof survives expert review, it draws a firm boundary around quantum advantage. Exponential speedups will need structured inputs, like the repeating pattern in Shor’s algorithm — not random ones. That shapes where quantum hardware is worth betting on, and where classical simulation will keep up.
It also raises the bar for AI science claims. A public, machine-checked proof leaves sceptics something concrete to test, which is more than most model announcements offer. Expect other labs to be judged against that standard, and expect the next argument about AI-discovered mathematics to start with the repository, not the press release.
Background
Scott Aaronson and Andris Ambainis posed the conjecture in 2008, and it has counted among the central open problems of quantum complexity theory ever since. PSI, a Cambridge, Massachusetts-based public benefit corporation that calls itself an AI-native physics laboratory, launched in September 2026 with $58 million in seed funding. The proof is its second major announcement in about two weeks.
Source: PSI’s research announcement and the public proof repository
0 Comments