PSI reports an AI proof of a quantum computing mystery
A problem open for eighteen years and the challenge of keeping AI discoveries understandable
Published November 8, 2026Intelligence / Artificial Intelligence / Generative Models
For 18 years, a question has challenged researchers studying the promise of quantum computers: when do they need a special pattern in a problem to gain an enormous advantage? Physical Superintelligence, or PSI, says its AI research system has found a proof that answers an important version of that question.
The company announced the result on November 6. Its system, using a non-public Anthropic model, produced a complete proof during the third day of a research run, PSI says. It also produced a version written in Lean, software that checks whether each step of a mathematical argument follows from precisely stated rules.
The result concerns how much information computers must read to answer yes-or-no questions. For most randomly chosen inputs, it would establish that an ordinary computer can approximate a quantum computer’s answer probability without reading exponentially more information. That would clarify a boundary researchers have long suspected between problems where quantum machines can achieve spectacular advantages and those where their advantages are more limited.
PSI has made the paper, formal proof and verification records public. That gives other researchers something concrete to examine, while leaving important human work ahead: confirming exactly what the computer checked, understanding the argument and assessing what it means. As AI contributes more to scientific discovery, this combination of accessible evidence and accountable judgment will matter well beyond quantum computing.
Counting the information a computer needs
The Aaronson–Ambainis conjecture takes its name from computer scientists Scott Aaronson and Andris Ambainis. Their work explores quantum computation in the query model, a deliberately simplified setting that counts accesses to an input. An ordinary computer can inspect one bit, a zero or a one, with a query. A quantum query can act on a superposition of input positions.
This lets researchers isolate the value of quantum access to information. The accounting leaves out the work performed between queries, so a small query count alone does not guarantee a fast or practical program.
Aaronson and Ambainis connected this question to polynomials, the familiar mathematical expressions built from sums and products. A quantum algorithm’s probability of answering “yes” can be represented by a polynomial in its input bits. The number of queries limits the polynomial’s degree, a measure of its complexity.
The conjecture asks whether such a bounded, low-degree polynomial must have at least one influential input bit whenever its output varies appreciably. Influence measures how much the output changes, on average, when that bit is flipped. The proposed bound depends on the degree and the amount of variation, rather than on how many bits the input contains.
An influential bit gives an ordinary algorithm somewhere useful to look. It can read that bit, narrow the possibilities and repeat, until the remaining uncertainty is small enough to estimate the quantum algorithm’s answer probability. Aaronson and Ambainis had already shown how a proof of their conjecture would make this strategy work on most inputs.
The scope is specific. The conclusion allows a small fraction of inputs to be difficult, and it concerns approximate answers under a stated distribution of inputs. It leaves room for large quantum advantages on specially structured problems. It also leaves sampling tasks and other kinds of quantum computation requiring their own analysis.
The work behind the result
PSI’s release credits David Turturean with choosing the problem, developing the research system and running it. The paper describes model instances searching existing research, proposing and testing ideas, combining them and coordinating other instances. Turturean then asked a model to prepare a first draft of the paper, which he personally reviewed and edited. He takes responsibility for its correctness.
The mathematical approach draws on earlier human research. In particular, it follows a program developed by Shachar Lovett and Jiapeng Zhang, replacing a conjectured step with a new inequality. It also builds on work by David Reimer and others. The discovery sits within a long chain of mathematical ideas whose sources are identified in the paper.
The paper’s timeline records further improvements after the first proof. In one formulation, the exponent in the bound improved from 22 to 11 and then to 7, with the versions checked in Lean. Those changes strengthened the mathematical result. The public account does not document changes to the underlying AI model’s weights or an AI system redesigning itself.
That distinction matters when considering recursive self-improvement, the possibility that AI could improve the systems used to build more capable AI. This case offers evidence about AI-assisted mathematical research. Evaluating a self-improvement loop would require additional evidence about what changed in the AI system and how those changes affected its capabilities.
What the checks establish
Lean checks a formal argument against its definitions and logical foundations. PSI reports that the main results contain no unfinished proof placeholders or additional axioms, and that the proofs passed rechecking through multiple implementations of the checking machinery. Its repository supplies commands, software versions and records intended to let others repeat the work.
Those checks are valuable because mathematical plausibility can be deceptive. A long argument can look convincing while concealing a gap. A formal proof makes each required step explicit enough for software to examine.
The release also describes its limits. Readers must confirm that the formal statement matches the conjecture Aaronson and Ambainis actually posed. The prose paper is not itself machine-checked. Its discussion of quantum-computing consequences draws on existing mathematical results and has no corresponding Lean proof in this release.
There is a further distinction within the formal work. The main conjecture and the stated explicit bound are proved without an extra hypothesis. A separate, stronger numerical constant is conditional on another mathematical result that the repository has not formalized. Keeping those claims separate prevents an optional improvement from being mistaken for an assumption behind the central result.
The verification records describe checks performed by the author’s tooling and project workflows. Different checking implementations offer protection against some software errors, but outside reproduction is another step. JetsonsAge’s review did not locate a published independent rerun of the complete checks or a peer-reviewed publication of PSI’s proof as of November 8.
Making the mathematics understandable
Researchers who know the problem are already engaging with the argument. Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan had reported a related result in August for quantum algorithms operating in a fixed number of parallel rounds. PSI says they have been reading the new proof, sending comments and preparing a shorter explanation for experts.
“This is a huge result. It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups,” the four researchers wrote in a statement reproduced by PSI. The quotation is part of PSI’s announcement, rather than a separate interview with JetsonsAge.
Human understanding adds something a successful software check cannot supply on its own: a clear account of why the proof works, which ideas are reusable and how far its conclusions reach. A shorter exposition could help other mathematicians inspect the result and apply its methods to new questions.
For public oversight of AI-assisted science, this release offers a useful example of what can be preserved: explicit claims, a checkable argument, named human responsibilities and records of the checks performed. There are also limits to the visibility. The Anthropic model is non-public, and the released proof does not reveal the internal neural processes that produced it.
The next stage will be visible in the work other researchers do with these materials: reproducing the checks, explaining the reasoning and testing its reach. A discovery becomes more useful when people can carry it forward with confidence in what has actually been established.
Reporting note
This article is based on the public announcement, paper, repository, verification documentation and earlier research reviewed on November 8, 2026. JetsonsAge has not rerun the Lean formalization or independently certified the proof. Claims about the research run and its timing are attributed to PSI. No researchers were contacted for this article.
Sources
1. Physical Superintelligence, A proof of the Aaronson–Ambainis conjecture, November 6, 2026. Announcement, reported researcher comments and contributions.
2. David Turturean, A proof of the Aaronson–Ambainis conjecture, November 2026 preprint. AI disclosure, mathematical statement and discovery timeline.
3. Public proof repository. Main result, conditional improvement, verification scope and disclosure.
4. Verification documentation. Methods, software versions, recorded runs and limits.
5. Release preparation checks. November 6 records and captured outputs.
6. Scott Aaronson and Andris Ambainis, The Need for Structure in Quantum Speedups. Theory of Computing 10, 133–166, 2014.
7. Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, Quantum Speedups Require Structure or Depth. August 19, 2026.
8. Mordechai Rorvig, Quantum Algorithms Conquer a New Kind of Problem. Quanta Magazine, July 11, 2022. Background on decision problems and other quantum tasks.