PSI Says AI System Produced Lean-Checked Proof of 2008 Quantum Conjecture

A conjecture that has shaped arguments about quantum speedups since 2008 now has a machine-checked proof, Physical Superintelligence said Friday. The physics research lab reported that an internal research system, running instances of a non-public Anthropic model on PSI's own infrastructure, produced a complete proof of the Aaronson-Ambainis conjecture on the third day of a run — and that the Lean proof assistant accepted it.

That's the headline. Underneath it sits a claim about what AI can now do at the frontier of theoretical computer science, and a stack of caveats about what still needs human eyes. Here's how the pieces fit.

What exactly was proved?

The Aaronson-Ambainis conjecture, posed by Scott Aaronson and Andris Ambainis in 2008, connects quantum computing to the mathematics of polynomials. The two researchers linked the question to polynomials and argued that, if their conjecture held, quantum computers would have at most a polynomial advantage in the number of input queries needed for yes-or-no questions on random inputs that lack rare structure.

PSI put its claim in the bluntest possible terms in its research post: "The Aaronson-Ambainis conjecture is now a theorem."

The stakes are about limits, not miracles. Dramatic speedups such as Shor's factoring algorithm still depend on promised patterns in the input, PSI wrote, summarizing the longer-running debate. In other words, the famous quantum wins exploit structure. On unstructured, random inputs, the conjecture says the quantum edge stays polynomial, not exponential.

The takeaway: the result draws a line around where quantum speedups can and cannot explode, at least for random inputs.

Who did the work, and how?

David Turturean, a member of technical staff at PSI, led the effort. He built the research system, scoped the problem, and ran it. After the system produced its proof, he prompted the model to turn the output into a first draft of the paper, which he reviewed and for which he is responsible.

The timeline is short. On day three of the run, Lean accepted the proof. PSI then pointed the system at related open problems. The system improved the result twice, and Lean accepted the final version.

Two outside advisors were involved on the verification side. Jim Halverson audited the proof, and Phiala Shanahan commented on the Lean formalization, according to the post.

So the division of labor matters here: the AI system generated the mathematics, and humans checked that the checking held up. Lean is a proof assistant — software that verifies each logical step mechanically. If Lean accepts a proof, no step in it depends on human intuition or trust.

The takeaway: the machine did the proving, but the process leaned on named humans at every gate.

What's public, and what isn't?

The manuscript and a Lean 4 formalization are public. The Lean code, scripts and documentation are released under Apache 2.0; the paper remains copyright of its author.

The repository lists four theorems proved with no placeholders or added axioms, and says they were re-checked with two independent Lean kernel implementations. That's a strong verification standard — running the check twice with separate kernels rules out a bug in any single implementation of Lean itself.

But one job remains open, and PSI assigns it to readers: confirming that the formal statement labeled PrintedConjecture matches the conjecture as printed. The human-readable paper is not itself machine-checked. This is the classic gap in formalization work — the machine verifies the chain of reasoning, but someone still has to confirm the formal statement says what the original conjecture meant.

There's also an open question about the model itself. Business Insider's Kelsey Vlamis reported that Anthropic did not respond to a request for comment on which unreleased model was used. PSI has said only that it ran instances of a non-public Anthropic model on its own infrastructure.

The takeaway: the proof artifacts are open for anyone to inspect, but the model behind them is not, and one formal-statement check still falls to the community.

What does the proof actually establish?

PSI's write-up walks through the influence bound the team says it proved for bounded, low-degree polynomials on the discrete cube, including an explicit constant of about 0.0025 in one form of the inequality.

The practical consequence, as PSI frames it: with the conjecture in hand, an ordinary computer can estimate a quantum algorithm's acceptance probability, up to a small error, for all but a small fraction of random strings. And it can do so using a number of looks that grows like a fixed power of the quantum look count rather than exponentially.

That last clause is the whole point. Polynomial growth is manageable; exponential growth is not. The result means classical machines can, in this random-input setting, simulate the behavior of quantum algorithms without drowning in computation.

The boundary still holds, though. Structured problems — Shor's algorithm among them — sit outside that "random input" story. The conjecture doesn't touch the factoring speedups that made quantum computing famous.

The takeaway: for random inputs, classical computers can now provably approximate quantum behavior at polynomial cost.

How does this fit the research trail?

This proof didn't appear in a vacuum. In August, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan of Stanford proved there is no exponential speedup on random inputs for quantum algorithms that read their input in a fixed number of parallel rounds.

That was a partial result — it covered a restricted class of algorithms. The full conjecture, the one PSI's system now claims, removes that restriction.

The Stanford group hasn't stayed on the sidelines. PSI says the same four researchers have been reading the full-conjecture proof and are writing a shorter exposition for experts. Relayed through PSI's post, they wrote: "This is a huge result." They added: "Everything is brought together in a rather magical way."

When the people who proved the nearest partial result call your proof huge and start writing a digest of it for the field, that's a meaningful signal of how the community is receiving the work.

The takeaway: the researchers closest to the problem are engaging with the proof directly rather than dismissing it.

Why the AI angle matters

The mathematics is the result, but the method is the story for anyone tracking AI capabilities. A research system built around an unreleased Anthropic model produced a proof, on day three of a run, that survived Lean's mechanical scrutiny — and then improved it twice on follow-up attempts.

That pattern — generate, verify, iterate — is exactly where AI systems have struggled in mathematical research. Verification tools like Lean close the trust gap: the model can't bluff its way past a proof assistant. Formal methods give AI a hard referee.

PSI closed its announcement with a line that doubles as the field's scoreboard: "Quantum computing still has plenty of mysteries, but now there is one fewer."

With the Lean formalization public under Apache 2.0 and the Stanford group preparing an expert exposition, the next test is community scrutiny — starting with whether PrintedConjecture matches the conjecture Aaronson and Ambainis actually printed in 2008.