Physical Superintelligence (PSI) says an internal research system using a non-public Anthropic model found a complete proof of the Aaronson–Ambainis conjecture during the third day of a run. The conjecture, open since 2008, concerns a fundamental question in quantum computing: under what conditions can quantum algorithms gain exponential advantages over classical ones?
In its November 6, 2026 announcement, PSI says the system subsequently improved the result twice and that the Lean proof assistant accepted the final version. The company has released a paper, proof source code and a Lean 4 formalization.
That makes this a substantial, inspectable claim. It remains a self-published result without completed conventional peer review. The key distinction is between checking a formal mathematical proof, confirming that its statement captures the original conjecture, and establishing the claimed quantum-computing consequence. Those are connected tasks, but they are separate parts of the verification process.
What PSI Says Happened in Three Days
PSI describes a research system developed internally and run on its own infrastructure, using instances of an unreleased Anthropic model. The announcement credits earlier mathematical ideas from Shachar Lovett, Jiapeng Zhang, David Reimer and others.
The public repository identifies David Turturean of PSI as the paper’s author and says AI models produced the proof, paper and formalization. Business Insider’s November 7 report identifies Turturean as the developer of the research system.
The three-day claim belongs to that whole setup. It should not be read as evidence that an ordinary chat session with a publicly available Anthropic model can reproduce the result. The underlying model is unidentified, and the public materials do not provide a reproducible version of the discovery system.
Business Insider reported that Anthropic did not respond to its request for comment. This is therefore PSI’s research announcement, not an Anthropic announcement about a released product.
My view is that the elapsed time is interesting, but the published artifacts matter more. Three days describes one reported run, without enough information to compare its resources or reliability against other research systems. A precise theorem and inspectable proof give outsiders something much more useful to evaluate.
The Mathematical Claim, in Plain Language
The conjecture concerns polynomials evaluated on strings of bits. A polynomial combines input variables through terms such as x₁, x₂x₃ or x₁x₂x₄. Its degree is the largest total degree of any term.
PSI’s claimed theorem starts with three conditions:
- The polynomial has degree at most d.
- Its value stays between 0 and 1 on every possible bit string.
- Its output has variance of at least ε when inputs are chosen uniformly at random.
Variance measures how much the output changes across inputs. If the output barely moves, there is little variation to explain.
The conclusion is that at least one input bit must have a quantifiable influence. Here, influence means the squared change in the polynomial’s value when that bit is flipped, averaged over all inputs.
The repository’s explicit bound is:
[ \operatorname{Inf}_i[p] \geq \frac{8\sqrt{15}}{125\pi^4} \frac{\varepsilon^{5/2}}{d^6} \geq \left(\frac{\varepsilon}{d}\right)^7. ]
The crucial feature is the absence of the number of input bits from the lower bound. Even if a polynomial depends on an enormous input, bounded degree and meaningful output variation guarantee an influential coordinate.
That is the useful intuition: a low-degree polynomial cannot spread all of its variation so thinly across its inputs that every individual bit becomes arbitrarily unimportant. The conjecture asked for a polynomial relationship between influence, variance and degree. PSI claims to have supplied an explicit one.
Why This Matters for Quantum Computing
Quantum query complexity counts how many times an algorithm accesses its input. A classical query reads an input bit. A quantum query can act on a superposition of input positions.
This model helps researchers separate the cost of obtaining information from the computation performed between queries.
As PSI explains, an established result connects quantum algorithms to polynomials: after T queries, a quantum algorithm’s probability of answering “yes” is a polynomial of degree at most 2T in the input bits. That probability lies between zero and one.
This creates a bridge to the influence conjecture:
- Represent the quantum algorithm’s acceptance probability as a bounded, low-degree polynomial.
- Use the influence guarantee to identify informative input bits.
- Build a classical query procedure that approximates that probability on most uniformly random inputs.
For fixed approximation accuracy and a fixed allowed fraction of exceptions, the claimed consequence is that the classical procedure needs a number of queries polynomial in T, instead of exponentially more.
That would resolve a central question about the role of input structure in dramatic quantum query advantages. Uniformly random strings usually lack the special promises or patterns exploited by many famous quantum algorithms.
Queries Are Not Total Running Time
A guarantee about input accesses is narrower than a guarantee about overall computational cost. A classical algorithm could make relatively few queries while still doing expensive work between them.
State of Proof’s analysis emphasizes this distinction. The result supplies neither a general fast classical replacement for quantum computers nor a hardware performance measurement.
Structured problems remain relevant, as do other forms of quantum advantage outside this particular statement. PSI uses Shor’s factoring algorithm as an example of how structure can enable dramatic quantum improvements.
For anyone assessing a quantum application, I’d treat this result as a reason to ask a more precise question: what structure does the workload exploit, and what does the full classical comparison cost? The theorem could sharpen that discussion. It cannot answer an investment or engineering question by itself.
Inside the Lean Formalization
Lean is a proof assistant. Researchers express mathematical definitions and proofs in a formal language, and a small checking component, called the kernel, verifies that the proof follows the system’s rules.
PSI’s repository exposes four main theorem declarations. Their different roles are worth understanding:
| Lean declaration | What it states | Status reported by PSI |
|---|---|---|
aaronson_ambainis | The conjecture in its original 0/1 normalization, with the bound (ε/d)^7 | Proved without a placeholder or added axiom |
aaronson_ambainis_explicit | The explicit influence bound involving ε^(5/2)/d^6 | Proved without a placeholder or added axiom |
aaronson_ambainis_pm | The corresponding explicit bound on inputs represented as −1 and +1 | Proved without a placeholder or added axiom |
aaronson_ambainis_of_fbsDegreeBound | A stronger constant, assuming an additional mathematical statement | Proved as a conditional theorem |
The fourth declaration needs careful reading. It assumes FbsDegreeBound, which the repository identifies as a theorem from work by Agarwal and Ben-David that has .
Frequently Asked Questions
3 questions
1Did Anthropic Announce This Result?
No. PSI announced it and says its internal research system used a non-public Anthropic model. The model’s identity has not been disclosed.
