PSI Says AI System Solved an 18-Year-Old Quantum Computing Conjecture

An AI-assisted mathematical proof could settle a longstanding question about quantum computing, but independent scientific scrutiny remains essential.

On November 6, 2026, Physical Superintelligence (PSI) announced that its internal AI research system had found a proof of the Aaronson–Ambainis conjecture, an important unresolved problem in quantum computing theory dating back to 2008. The company says the discovery was made using a non-public Anthropic model and accompanied by a formal mathematical verification in Lean, a software tool designed to check proofs.

The announcement could represent a significant achievement for AI-assisted scientific research. However, the result has not completed independent peer review, and PSI's work does not establish that publicly available versions of Claude can reproduce the discovery.

The Aaronson–Ambainis conjecture addresses a fundamental question: When can quantum computers achieve an enormous speed advantage over conventional computers?

Quantum computers exploit principles of quantum mechanics to process information differently from classical machines. Certain quantum algorithms can solve particular mathematical problems using dramatically fewer computational steps.

One famous example is Shor's algorithm, which can factor large integers efficiently on a sufficiently capable quantum computer. The algorithm exploits mathematical structure within the problem.

But researchers have long wondered whether quantum computers could achieve similarly dramatic advantages when their inputs lack recognizable patterns.

Computer scientists Scott Aaronson and Andris Ambainis developed a mathematical conjecture to investigate that question. Their work, published in The Need for Structure in Quantum Speedups, connects quantum computing to a mathematical property of polynomials.

The central idea is that a quantum algorithm's behavior can be represented using mathematical functions whose complexity is related to the number of times the algorithm examines its input.

The conjecture predicts that certain relatively simple functions must contain at least one input variable with a measurable influence on their output.

If that property holds, it becomes possible to show that classical computers can approximately reproduce the behavior of quantum algorithms on most randomly selected inputs without requiring exponentially more input queries.

In simpler terms, large quantum speedups generally require useful structure in the problem being solved, at least within the mathematical framework considered.

That does not mean quantum computers are ineffective or that every quantum advantage disappears.

The result concerns quantum query complexity, which measures how often an algorithm needs to access its input. It does not establish equivalent limits on every aspect of practical computing, including runtime, hardware performance or energy consumption.

According to PSI's research announcement, the company developed an internal research system that used instances of a non-public Anthropic model.

PSI says the system produced a complete proof during the third day of a research run conducted on the company's infrastructure.

The research system subsequently worked on related mathematical problems and improved the original result twice. PSI reports that Lean accepted the final formulation.

The work was not an independent chatbot answering a mathematics question without human involvement.

PSI researcher David Turturean led the project. The company credits him with developing the research system, selecting the problem, directing the research process and reviewing the resulting manuscript.

Turturean also prompted the model to prepare an initial draft of the paper and accepted responsibility for its correctness.

Two additional contributors provided specialist scrutiny. PSI advisor Jim Halverson audited the proof, while advisor Phiala Shanahan commented on its Lean formalization.

The distinction matters because modern AI research systems combine model capabilities with software infrastructure, specialized workflows, verification tools and human judgment.

The announcement provides evidence about this particular research setup, not a general demonstration that any user can obtain an equivalent result through a standard commercial chatbot.

The inclusion of a formal Lean proof is one of the most important aspects of PSI's announcement.

Large language models can generate convincing mathematical explanations containing subtle logical errors. A polished argument is not necessarily a valid argument.

Lean addresses a different problem.

It is a formal proof assistant that checks whether mathematical conclusions follow from explicitly defined assumptions and established logical rules.

Instead of evaluating whether a proof sounds persuasive, Lean checks its formal structure.

PSI has published the paper, Lean formalization and supporting verification materials on GitHub.

The repository identifies formal theorems covering the central mathematical influence bound. According to PSI, these proofs contain no unfinished placeholders or additional axioms and have also been checked using separate implementations of the Lean verification kernel.

This makes the research unusually open to technical examination. Other mathematicians can inspect the definitions, examine the code and attempt to reproduce the verification.

However, formal verification and scientific peer review answer different questions.

A proof assistant checks whether a formal statement follows logically from its assumptions. Researchers must still determine whether that formal statement accurately captures the original mathematical problem and whether the broader interpretation is justified.

In this case, the Lean development covers the central polynomial theorem, while the paper separately explains its consequences for quantum computing.

A successful formal check does not automatically constitute independent validation of every scientific claim surrounding the proof.

The Aaronson–Ambainis conjecture had already attracted substantial attention before PSI's announcement.

In August 2026, researchers Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan published Quantum Speedups Require Structure or Depth.

Their work established the predicted limitation for an important special case involving quantum algorithms that access their inputs in a fixed number of parallel rounds.

PSI says the Stanford researchers have been examining its broader proof, offering feedback and preparing a shorter explanation for specialists.

Their earlier result is an important point of comparison because it demonstrates that the mathematical question has been an active research priority, independent of the latest AI announcement.

As of November 7, PSI's newly released full proof has not completed conventional external peer review. Its publicly available formalization offers an opportunity for independent verification, but publication of code should not be confused with a completed review process.

The broader significance of PSI's work extends beyond quantum computing.

AI companies increasingly aim to develop systems capable of contributing to scientific research rather than simply summarizing existing knowledge or assisting with routine tasks.

If PSI's result withstands independent examination, it would provide a substantial example of an AI-assisted system contributing to the resolution of a longstanding mathematical problem.

The most interesting development may be the combination of three capabilities: generating original mathematical ideas, refining those ideas through repeated research cycles and checking the resulting arguments using formal methods.

Such workflows could influence how researchers approach difficult problems in mathematics, theoretical computer science and other fields where conclusions can be expressed in rigorous symbolic form.

Significant limitations remain.

PSI has not disclosed the precise Anthropic model used, making direct comparisons with publicly available Claude models impossible. The company's infrastructure and research methodology may also have contributed substantially to the outcome.

And even when formal verification succeeds, scientific acceptance still depends on transparent assumptions, reproducibility and expert examination.

For now, PSI has presented a potentially important research result with an unusually detailed technical record. Whether it becomes a recognized landmark in quantum computing will depend on how the mathematical community evaluates that record.