Aaronson-Ambainis Conjecture Proof: What PSI Claims

On November 6, a small lab called Physical Superintelligence (PSI) published a note with a flat opening line: “The Aaronson-Ambainis conjecture is now a theorem.” It says a research system it built, running instances of a non-public Anthropic model, produced the proof. TechCrunch picked it up on November 9, and Anthropic hasn’t said which model was used.

I read the PSI note and the abstract of the paper. Here are the questions I’d ask first.

What was the conjecture, in plain words?

Scott Aaronson and Andris Ambainis wrote it down around 2008, according to PSI. It’s a statement about polynomials, and the polynomial part is the stand-in for a quantum algorithm. PSI says that if the statement is true, a quantum computer can’t be exponentially faster than an ordinary one on random inputs, only on inputs with a rare pattern, which is what Shor’s factoring algorithm relies on.

Put differently, it’s a limit on quantum speedups, not a new quantum algorithm. Nothing here makes quantum hardware faster or slower.

What exactly is claimed?

PSI says the system had a complete proof on the third day of a run on its own infrastructure, and that Lean, a proof assistant that checks every logical step, accepted it. The company then pointed the system at related open problems, and says it improved the result twice, with Lean accepting the final version. The paper is on arXiv under David Turturean’s name, and the Lean code is public on GitHub.

The abstract gives the bound: some variable has influence of at least c times Var(f)^(5/2) divided by d^6. In the original formulation that works out to (ε/d)^7. The paper calls its proof elementary.

Claim	Who says it	Checked by
A complete proof exists	PSI	Lean, per PSI
An unreleased Anthropic model found it	PSI	Not confirmed by Anthropic
It’s “a huge result”	Stanford’s Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, quoted by PSI	They are still reading it
The proof is correct as mathematics	Nobody yet in print	Peer review hasn’t started

Who else has looked at it?

The Stanford group had proved a special case in August 2026, for quantum algorithms that read their input in a fixed number of parallel rounds. PSI says they’ve been reading the full proof, sent comments, and are writing a shorter version for experts. The quote, “This is a huge result,” comes from that group via PSI’s own page, so it’s a company-supplied endorsement. WebProNews, citing the same post, adds that PSI advisor Jim Halverson audited the proof. I couldn’t find a public reaction from Aaronson or Ambainis themselves.

Does Lean settle it?

Mostly, and I’d say so carefully. A Lean-accepted proof means the logic follows from the written statements, with no gaps. PSI’s repository, per WebProNews, lists four theorems with no placeholders or added axioms. What Lean can’t tell you is whether the formal statement says what the conjecture meant. Humans have to read that part, and that’s the work the Stanford group is doing.

My read: the Lean check makes a wrong proof much less likely than usual, but the “is this the right statement” question is still open until experts sign off. I’d call it very promising, not settled.

Is this the same model as the one in Anthropic’s launch?

Unknown. TechCrunch reported that Anthropic neither confirmed nor denied that Fable 5.2 was the model. Anthropic’s own announcement the same day, covered in our post on Fable and Mythos 5.2, made its own math claims, and I haven’t seen those independently checked either.

It also fits a pattern. OpenAI made a similar announcement in October, which we looked at in the post on its Exponential Time Hypothesis claim, where reviewers took care to say their involvement wasn’t an endorsement. Two labs making research-level math claims within weeks of each other is new.

My read: this one is stronger than most because the full proof and its formal check are public from day one. Anyone can run the Lean files today.

Sources

Note on sources: I read PSI’s note in full, plus the arXiv abstract and introduction as shown in search results. I did not read the Lean files or the full proof, and I can’t judge the mathematics myself. WebProNews and Quantum Zeitgeist are secondary and used only for details that match PSI’s own page.