Physical Superintelligence claims unreleased Anthropic model proved Aaronson-Ambainis conjecture

A Cambridge, Massachusetts lab says an AI did in three days what mathematicians have chased since 2008/2009. Physical Superintelligence (PSI) claims its research system, running on a non-public Anthropic model, produced a complete proof of the Aaronson-Ambainis conjecture.

The catch is that the model doing the heavy lifting is unnamed and unreleased. Outsiders cannot verify the result the way they would normally check a breakthrough, which leaves the math world in a familiar posture: interested, but holding its applause.

What PSI says it did

PSI, which describes itself as an AI physics research lab, announced the result on November 6, 2026. According to the lab, its internal system paired the unreleased Anthropic model with PSI’s own proprietary infrastructure.

The lab says the system generated a full proof within three days. That proof was then accepted by Lean, an interactive theorem prover.

PSI says the system did not stop at the first proof. It reportedly went on to improve the proof’s bound twice after the initial output.

The final result, per PSI, shows a variable with influence of at least roughly ~0.0025 · ε^{5/2} / d^6.

PSI has published a paper on the work under the authorship of David Turturean. It also released the Lean formalization on GitHub, totaling 9,454 lines of code.

The lab says that formalization contains no added axioms or placeholders. In theorem-prover terms, that means no hidden assumptions slipped in and no steps left as “trust me, this part works.”

Why this conjecture matters

The Aaronson-Ambainis conjecture sits in quantum complexity theory, a field that asks what quantum computers can and cannot do better than ordinary ones. It has been open since 2008/2009.

Technically, the conjecture concerns the influence of variables in bounded low-degree polynomials. Put another way, it asks whether certain well-behaved mathematical functions must always have at least one input that meaningfully moves the output.

The practical stakes come from what follows if the conjecture holds. It suggests quantum algorithms cannot universally beat classical ones when the input has no structure to exploit.

The question had already seen partial progress. A Stanford group made up of Blanc, Docter, Strassle, and Tan proved a special case of the conjecture in August 2026.

That same group is now among those examining PSI’s claimed proof. Independent verification is underway.

The lab behind the claim

PSI is not a household name, and it is a young company. It raised $58 million in seed funding in September 2026, roughly two months before this announcement.

What this means

The interesting tension here is between what can be checked and what cannot. The Lean formalization is public, so in principle the final proof can be inspected line by line. The process that produced it, however, runs on a model no one outside the arrangement can access.

There is also the question of whether the formal statement in Lean faithfully captures the original conjecture. A machine checker confirms that a proof proves its stated theorem. It cannot confirm that humans encoded the right theorem in the first place, which is one reason the Stanford group’s review will carry weight.

The things to watch are straightforward. First, whether the Stanford researchers and other independent reviewers sign off on the formalization and the paper. Second, whether Anthropic says anything about the model involved. Third, whether PSI’s system produces further results that others can examine on similar terms.

Until then, the claim sits in an awkward middle ground. The proof is public enough to be scrutinized, but the machine behind it is private enough that the full story remains PSI’s to tell.