AI Solves 17-Year-Old Quantum Computing Puzzle: Unreleased Anthropic Model Proves the Aaronson-Ambainis Conjecture

An artificial intelligence system has solved a maths problem that had been open for 17 years — one that sits at the heart of a basic question about quantum computing: when can a quantum computer be enormously faster than an ordinary one?

The proof was announced on 6 November 2026 by Physical Superintelligence, known as PSI, a research lab in Cambridge, Massachusetts. PSI said a research system it built, running an unreleased model from Anthropic, the company behind the Claude chatbot, found a complete proof of the Aaronson-Ambainis conjecture during the third day of a run. A computer program called Lean then checked every step of the proof and accepted it.

The conjecture, posed in 2008 by computer scientists Scott Aaronson and Andris Ambainis, is one of the central questions in quantum computing theory. Its answer sets a limit on quantum speed: for many kinds of problems, a quantum computer can be faster than an ordinary computer, but not enormously faster. Truly dramatic speed-ups, the proof shows, need problems with special structure.

This article explains what the conjecture says, how the AI found the proof, what the result does and does not mean, and why it matters beyond the world of theoretical computer science.

What is the Aaronson-Ambainis conjecture?

To understand the result, it helps to start with the question behind it. Quantum computers work in a fundamentally different way from ordinary computers. Where an ordinary computer stores information as bits — each one a 0 or a 1 — a quantum computer uses qubits, which can exist in a mixture of states at once. For certain problems, this lets a quantum computer explore many possibilities in parallel and arrive at an answer far faster than any ordinary machine could.

That promise has driven billions of dollars of investment into quantum computing. But for years, researchers have asked a simple question: how often is that enormous advantage actually available? Is a quantum computer faster at everything, or only at some things?

In 2008, Scott Aaronson, now at the University of Texas at Austin, and Andris Ambainis, of the University of Latvia, connected that question to a statement about polynomials — the mathematical expressions, built from variables and powers, that school students meet in algebra.

Their argument ran like this. When a quantum algorithm looks at its input a certain number of times and gives a yes-or-no answer, the probability of each answer can be written as a polynomial in the input bits. Aaronson and Ambainis conjectured that every such polynomial has at least one variable with a large “influence” — one input bit that matters a lot to the outcome.

If that conjecture is true, a surprising conclusion follows. An ordinary computer can predict the quantum computer’s answer, for most random inputs, without looking at the input vastly more times than the quantum computer did. The ordinary computer’s extra work grows in a manageable, polynomial way — not exponentially. In plain terms: on random, unstructured inputs, a quantum computer is at most modestly faster, not enormously faster.

Exponential speed-ups would still be possible, but only for problems with special structure — a pattern in the problem that the quantum algorithm can exploit. The conjecture, in other words, draws a line between the problems where quantum computers can be dramatically better and the problems where they cannot.

How the proof was found

PSI describes itself as an AI-native physics laboratory, a public benefit corporation building AI systems it calls “virtual physicists”. It launched in September 2026 with 58 million dollars in seed funding, and the Aaronson-Ambainis proof is its second major announcement in about two weeks.

The proof was found by a research system PSI developed internally, running instances of a model from Anthropic that has not been released to the public. PSI has not identified which model was used, and Anthropic did not respond to a request for comment from Business Insider.

According to PSI, the system had a complete proof of the conjecture during the third day of a run on the company’s own computers. Lean, a proof assistant in which a computer checks every logical step, accepted it. PSI then set the system to work on related open problems. Along the way, the system improved the result twice, and Lean accepted the final version.

The work was led by David Turturean, a member of PSI’s technical staff, who developed the research system, chose the problem, ran the system on it, and reviewed the resulting paper. He is responsible for the paper’s correctness, according to PSI. Jim Halverson audited the proof, and Phiala Shanahan commented on the formalisation.

The proof builds on a plan laid out by mathematicians Shachar Lovett and Jiapeng Zhang, who had left one key inequality as a conjecture of their own, and on ideas from David Reimer and others. It also follows work published in August 2026 by four Stanford University researchers — Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan — who had settled the conjecture’s prediction in a special case, for quantum algorithms that examine their input in a fixed number of parallel rounds. Those four researchers have been reading PSI’s proof and are writing a shorter explanation of it for experts.

Why a computer-checked proof matters

A mathematical proof is only as good as its weakest step, and long proofs can contain subtle errors that humans miss. That is why the Lean check matters.

Lean is a proof assistant: software that verifies a mathematical argument step by step, using only the rules of logic. If Lean accepts a proof, every step follows from the ones before it. PSI says both the manuscript and the Lean 4 formalisation are public, and that the formal development contains no proof placeholders and no added axioms — no steps taken on trust.

The checks went further than a single run of Lean. The proof was replayed through Lean’s kernel, the core software that verifies the logical steps, and through lean4lean, an independent implementation of Lean’s type checker. Two separate checkers agreeing gives extra confidence that the verification itself was not fooled by a bug in one program.

There are limits, and PSI’s own repository states them openly. The human-readable paper is not itself machine-checked — only the formal version in Lean is. A reader must still confirm that the formal statement in Lean matches the conjecture as Aaronson and Ambainis originally wrote it. And the checking relies on a trusted base: Lean’s kernel and compiler, the definitions in its Mathlib library, and the computers used to run the checks. None of that removes the need for expert human review, which is now under way.

What the result does — and does not — mean

The result is a theorem about theory, not a new machine. It does not make today’s quantum computers any faster, and it does not say when quantum computers will become practically useful. What it does is clarify where the advantage of quantum computing can be found.

First, it limits the advantage on random inputs. For yes-or-no questions on most randomly generated inputs, an ordinary computer can estimate a quantum computer’s answer without needing exponentially more looks at the input. The result concerns the number of times an algorithm reads its input, known as query complexity, rather than total running time.

Second, it does not rule out exponential speed-ups. Problems with suitable structure — the kind of structure that algorithms like Shor’s algorithm for factoring large numbers exploit — can still give quantum computers a dramatic edge. The theorem says the advantage needs that structure; it does not say the advantage is impossible.

Third, it does not change the race to build useful quantum computers. Companies such as IonQ, Rigetti and D-Wave, and giants such as IBM and Google, are working on hardware that can run real calculations. Their progress depends on engineering — better qubits, lower error rates, more of them — not on this theorem. But the theorem helps everyone, from investors to researchers, judge more honestly which problems are worth aiming quantum computers at.

AI is now doing mathematics

The Aaronson-Ambainis proof is part of a wider and fast-moving shift: AI systems are beginning to solve problems in mathematics and science that humans have not been able to crack.

In September 2026, OpenAI said its systems had solved a 90-year-old problem in mathematics, the Navier-Stokes equations, which it called “one of the deepest problems at the frontier of mathematics”. PSI’s announcement follows the same pattern — an AI system working on a hard, well-defined problem, with its output checked by software rather than taken on trust.

The pattern matters because it answers the obvious objection to AI-generated mathematics: how do we know the machine did not make a mistake? When a proof is formalised in Lean, the machine’s work can be checked by another machine, and the check is independent of how the proof was found. That makes AI a plausible collaborator in mathematics in a way that would have been hard to trust even a few years ago.

It also changes who can work on hard problems. A small lab with a good research system and access to a powerful model can now attack questions that once required years of work by specialists. David Turturean’s role — scoping the problem, running the system, reviewing the draft — looks like a new kind of research job: part scientist, part supervisor of an AI colleague.

That said, the human element has not disappeared. The proof followed a plan devised by Lovett and Zhang, built on Reimer’s ideas, and was audited by Halverson. The Stanford team that solved the special case is now writing the expert explanation. AI found the proof, but humans framed the problem, checked it and are explaining it.

Why it matters beyond computer science

For most people, quantum computing is still an abstract idea. But the question this proof settles — where can a new technology be dramatically better, and where can it not — is one that matters every time a powerful new technology appears.

Quantum computers are expected, eventually, to break some of today’s encryption, design new drugs and materials, and solve optimisation problems that are currently out of reach. Governments and companies are spending billions on that promise. A clear map of where the advantage lies helps that money go to the right problems — and helps the rest of us judge the claims made for the technology more calmly.

There is also a simpler reason the story matters. A problem posed in 2008, worked on by some of the best minds in the field, was solved in three days by a system built to do research. Whether that is exciting or unsettling depends on your point of view. But it is a sign of how quickly AI is moving from answering questions to discovering answers.

What happens next

Several things will decide how this result is received.

First, independent experts need to confirm that the statement proved in Lean is the same statement Aaronson and Ambainis conjectured. That is the one step no computer can do for us, and it is under way: the Stanford researchers who solved the special case are reading the proof and writing a shorter exposition for experts.

Second, the mathematical community will examine the bounds. The proof gives a specific guarantee — in PSI’s words, some input bit has influence at least roughly 0.0025 times the variation raised to the power 5/2, divided by the degree raised to the power 6 — and researchers will ask whether that guarantee can be improved, and what it implies for real algorithms.

Third, PSI will be watched for what it does next. The lab says it is building a “factory for physical superintelligence”, and this proof is its second major announcement in a fortnight. If its research system can repeat this kind of result, AI-assisted mathematics may become routine faster than anyone expected.

For now, the headline stands: a 17-year-old question about the limits of quantum computing has an answer, found by an AI, checked by a computer, and now waiting for the judgement of human experts.

Frequently asked questions

What is the Aaronson-Ambainis conjecture?

It is a mathematical statement, posed in 2008 by Scott Aaronson and Andris Ambainis, about when quantum computers can be exponentially faster than ordinary computers. It says that on random inputs, quantum computers can be at most polynomially faster — meaning modestly faster, not enormously faster.

Who proved it?

Physical Superintelligence (PSI), a research lab in Cambridge, Massachusetts, announced the proof on 6 November 2026. Its research system, running an unreleased Anthropic model, found the proof during the third day of a run, and the Lean proof assistant checked and accepted it.

What is Lean?

Lean is a proof assistant — software that checks a mathematical argument step by step, using only the rules of logic. If Lean accepts a proof, every step follows from the ones before it.

Does this mean quantum computers are not useful?

No. The result says exponential speed-ups need special structure in the problem. For structured problems, quantum computers can still be dramatically faster. The result concerns the number of times an algorithm reads its input, not total running time, and it says nothing about when quantum hardware will become practical.

Has the proof been verified by humans?

The proof was machine-checked in Lean and replayed through an independent checker, lean4lean. Human expert review is under way: the Stanford researchers who solved a special case of the conjecture in August 2026 are reading the proof and writing a shorter explanation for experts.

What is PSI?

Physical Superintelligence Inc. is a Cambridge, Massachusetts-based public benefit corporation that describes itself as an AI-native physics laboratory building AI systems it calls “virtual physicists”. It launched in September 2026 with 58 million dollars in seed funding.

Sources

• Physical Superintelligence (PSI), “A proof of the Aaronson-Ambainis conjecture”, 6 November 2026: https://psi.inc/research/aaronson-ambainis/
• Unite.AI, “PSI Reports Machine-Checked Proof of Aaronson-Ambainis Conjecture”, 6 November 2026: https://www.unite.ai/psi-reports-machine-checked-proof-of-aaronson-ambainis-conjecture/
• The Quantum Insider, “AI-Assisted Proof Settles Longstanding Question About Quantum Speedups”, 6 November 2026: https://thequantuminsider.com/2026/11/06/ai-assisted-proof-settles-longstanding-question-about-quantum-speedups/
• OfficeChai, “US Startup Physical Superintelligence Proves Aaronson-Ambainis Conjecture, A Key Open Problem In Quantum Computing”, 6 November 2026: https://officechai.com/ai/us-startup-physical-superintelligence-proves-aaronson-ambainis-conjecture-a-key-open-problem-in-quantum-computing/
• AIStockWire, “What is the Aaronson-Ambainis conjecture? PSI proof”, 6 November 2026: https://aistockwire.com/blog/what-is-aaronson-ambainis-conjecture-anthropic-ant-psi-proof-november-2026

This article is for general information and education only. It is not legal or financial advice.