Physical Superintelligence says its research system proved the Aaronson-Ambainis conjecture, a long-standing question about when quantum computers can outperform classical ones. The reported result is a negative one: it rules out a particular kind of exponential quantum advantage, not quantum advantage across the board.
Watch Desk analysis
What happened
Crypto Briefing reports that the Cambridge startup announced the proof on 6 November, after its system worked on the problem for three days. The company says the work used an internal research system alongside a non-public Anthropic model. It has published a 13-page paper and a Lean formalisation, which the report describes as 9,454 lines and 648 theorems, with no added axioms or placeholders.
The reported proof concerns the Aaronson-Ambainis conjecture, which relates to quantum advantage on random-oracle decision problems. Crypto Briefing says Scott Aaronson, one of the researchers who posed the problem, believes the proof is correct despite saying he does not fully follow it. That is a notable endorsement, not a substitute for readers treating the result as the company’s claim and examining the proof.
Why it matters
If the proof holds, it closes off one route to exponential quantum speed-ups on unstructured inputs. That can help researchers focus their effort, which is useful progress even when it does not make a quantum computer faster tomorrow. The report says the result does not affect structured speed-ups such as Shor’s algorithm, so this is a boundary around one class of advantage, not a verdict on quantum computing as a whole.
It is also an unusually concrete claim about AI-assisted research: the company says its system contributed to a formal proof of a difficult mathematical result. The public account describes both a paper and a machine-checkable Lean formalisation, giving researchers material to inspect rather than asking them to applaud a demo.
Our read
This is a serious research claim with an unusually useful audit trail. The Lean formalisation matters because it allows proof-checking software to verify the formal steps, but it does not make the broader interpretation or the AI system’s contribution self-evident. The interesting test now is whether specialists can check the formalisation and agree that it establishes the conjecture as stated.
What to watch
- Whether independent researchers validate the Lean formalisation and its connection to the stated conjecture.
- How much of the result’s proof work can be attributed to the AI system rather than the human team.
- Whether the result changes research priorities around quantum advantage on unstructured inputs.
Discussion spark: If a machine-checkable proof is correct but its authors cannot yet explain every step intuitively, is that enough to close a major research question?
Sources and evidence
- Physical Superintelligence uses AI to crack a two-decade-old quantum computing puzzle – Crypto Briefing (10 November 2026, 19:08 UTC)
Watch Desk is operated by WittyWires as an independent cross-cutting AI news tracker. It does not speak for the organisations or people it covers.