PSI reports an AI-assisted proof of a quantum speedup conjecture PSI reports an AI-assisted proof of a quantum speedup conjecture

A research system with a human author

PSI says its internal system reached a complete proof during the third day of a run, then improved the result twice. The manuscript describes multiple model instances searching existing work, proposing ideas and coordinating other instances. David Turturean developed the research harness and selected the problem. He also reviewed and edited the model-produced paper and accepts responsibility for its correctness. This is a reported research workflow with a named author, rather than a benchmark score or a public model release. The published materials make the output available even though the model behind the work remains private.

The result measures access to inputs

The underlying question concerns how often a computer must inspect its input to answer a yes-or-no question. Aaronson and Ambainis linked that question to the influence of individual variables in bounded, low-degree polynomials. Their original paper appeared on arXiv in November 2009. The new manuscript presents a bound that would let an ordinary algorithm approximate a quantum algorithm’s acceptance probability on most uniformly random inputs. The required number of input queries grows polynomially with the quantum query count, for fixed error parameters. That is a statement about access to information; it is not a measurement of a computer’s total running time.

The release includes a verification route

The repository separates the mathematical statement from the larger proof development. Its statement file imports Mathlib alone, giving reviewers a compact place to compare the encoded claim with the original conjecture. It also supplies source audits, axiom reports and recorded kernel checks. PSI reports that independent implementations of the proof checker accepted its declarations. Those are different checker implementations, not a claim that an outside research group has reproduced the release. Published comparator records identify a private staging repository as the origin of the recorded November 6 runs.

A proof package, not a hardware result

The comparison with familiar quantum examples matters. Shor’s algorithm exploits periodic structure; the original conjecture examines why special structure enables dramatic query savings. PSI’s package targets the mathematical boundary underlying that distinction. For developers building research agents, the useful artifact is the combination of a precise claim, proof code and a documented replay path. A reader can inspect what was proved before relying on the surrounding explanation. The release also records a deliberately invalid control that a normal build accepted and the replay checkers rejected. That example explains why a successful compilation alone is a weaker check.