Physical Superintelligence, or PSI, has published a proposed resolution of the Aaronson–Ambainis conjecture, a longstanding problem connected to the limits of quantum speedups. Its November 6 announcement says an internally developed research system found a proof using instances of a non-public Anthropic model.
According to PSI’s account, a complete proof emerged during the third day of a run, and the Lean proof assistant accepted it. The system subsequently strengthened the result. PSI also says a Stanford group has been reading the proof and providing comments. Those statements describe the company’s reported process; this article has not independently rebuilt or checked the formalization.
The mathematical result and its scope
The conjecture concerns properties of bounded polynomials and their implications for quantum query complexity. The relevant question asks when a quantum algorithm can use exponentially fewer queries to its input than a classical algorithm. It is a theoretical result about a defined computational setting, rather than a claim that quantum hardware has become unnecessary.
PSI has published a repository containing the paper and formal proof artifacts. Those materials let outside researchers examine the theorem statement, proof and assumptions rather than relying solely on a natural-language announcement.
Why formal artifacts change the discussion
Our analysis is that the interesting AI development is the combination of open-ended search and a mechanically checkable target. A model can propose many plausible arguments, but a proof assistant imposes a much stricter acceptance condition than persuasive prose. Releasing the artifacts allows scrutiny to move from whether the explanation sounds convincing to what the formal system actually established.
That still leaves several layers of review. Researchers can check whether the formal statement faithfully captures the intended conjecture, which assumptions it uses and whether the build reproduces in a clean environment. Mathematical exposition also matters: a proof may be accepted by software while remaining difficult for people to understand or reuse.
The reported use of a non-public model limits what outsiders can reproduce about the discovery process. Public proof artifacts make the claimed result inspectable without making the exact research system available. Those are different forms of transparency, with different scientific value.
For AI research, the release adds a substantial case study in long-running mathematical work. For quantum computing, its importance rests on the exact theorem and how specialists assess it. The next useful evidence is careful independent examination of the public proof and a clearer account of the ideas that make it work.