A research system built by the startup Physical Superintelligence, known as PSI, has produced a complete proof of a quantum computing conjecture that had stood open since 2008, the company announced on 6 November 2026. The system, running instances of an Anthropic model that has not been released to the public, reached the proof on the third day of a single run, and the Lean proof assistant accepted every step of it.

The conjecture was posed by computer scientists Scott Aaronson and Andris Ambainis. It asks a precise question about the limits of quantum speedups: for yes-or-no problems with no hidden structure in the input, can a quantum computer be exponentially faster than an ordinary computer? The conjecture says no. If it holds, dramatic quantum advantages such as Shor's algorithm for factoring numbers depend on structure in the data, and do not extend to unstructured problems.

How the proof was produced

PSI describes the work as the output of a research system it developed internally, rather than a single prompt to a chatbot. The system scoped the problem, generated candidate mathematical statements and checked each step against Lean 4, a proof assistant whose kernel verifies every logical step of an argument. According to PSI, the system had a complete proof by the third day of the run. It was then pointed at related open problems and improved its own result twice, with Lean accepting each stronger version.

The published formal proof contains 648 machine-checked theorems across 84 Lean files, with 761 declarations and no placeholder steps or added axioms, according to an independent summary of the repository. The final theorem gives an explicit bound: in any non-constant bounded polynomial of degree d with variance v, some single input bit has influence of at least about 0.0025 times v to the power 2.5, divided by d to the power 6. The paper itself is 60 pages long and has a single author, PSI researcher David Turturean, who scoped the problem and built the research harness. PSI adviser Jim Halverson audited the proof, and the company has published both the paper and the full formal proof on GitHub.

What Lean checking does and does not settle

Lean guarantees that the theorem as written in Lean is true. That is a strong check, but it is not the whole story. Experts still need to confirm that the formal statement in the code, a definition of about twenty lines, says exactly what Aaronson and Ambainis conjectured. If that definition drifted from the original problem, the theorem would be true but about a different problem. The human-readable paper is not itself machine-checked, so its informal sections also need expert reading.

The result is also narrower than a blanket ruling on quantum advantage. It counts reads of the input, not total computing time, and it applies to the specific class of functions in the conjecture. As of 7 November, neither Aaronson nor Ambainis had published an assessment, and the paper had not been through journal peer review.

Why the claim is being taken seriously

The Stanford team that proved a special case of the conjecture in August 2026, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, has reviewed the proof and is preparing a shorter exposition for specialists, according to PSI. That team called the result a huge one. An earlier public proof attempt, by Keller and Klein, was withdrawn, which is one reason outside confirmation matters here.

PSI, a public benefit corporation based in Cambridge, Massachusetts, calls itself an AI-native physics laboratory. The model behind the run was Anthropic's, and Anthropic has not named it. Whether the achievement marks a turning point for machine-led mathematics or a one-off success on a problem that was nearly ready to fall will depend on what independent experts find when they read the formal statement and the paper in full.