Aaronson offered praise with, "Congratulations." But a few days later, the situation changed abruptly. A researcher named Paata Ivanishvili found a fatal logical error in the paper's core section, "Lemma 5.3," and the paper was ultimately retracted. Professor Aaronson wrote, "Sadly (retracted)," and "I leave this posted for historical reasons."

PSI's research system completed the proof in three days of execution, and a computer directly verified each written step using a proof verification language called "Lean." The 60-page paper and verification code were made public via GitHub 12.

Why is this three-day proof likely to stand this time, unlike the 2019 example? The key is the structural difference in the "verification method." Previously, subtle flaws could be missed during the process where humans read and judged the logic. In contrast, Lean verification takes an approach where the computer catches errors at each step as the logic is written. However, it has not been clearly confirmed through public data whether this proof has completely passed traditional peer review, or what mathematical insights led the AI to the solution.

Quantum Computer Advantages Come from 'Structure'

Advantages of Quantum Computers Come from 'Structure'

To understand the Aaronson-Ambainis conjecture, we must look at when quantum computers are vastly faster than classical ones. Quantum computers achieve exponential speedups in specific problems such as factoring. But these accelerations do not apply to all problems. Professor Aaronson has long wondered, "When inputs are completely random, are quantum computers really faster than classical ones?"

Professor Aaronson's reasoning is this: If a quantum algorithm accesses the input with T queries, then based on the 1998 result by Beals et al., the outcome can be represented by a polynomial of degree 2T or less. If there always exists a variable with high influence in this polynomial, a classical computer could also mimic the quantum algorithm with a polynomial number of queries by focusing its questions on that variable. In other words, the true advantage of a quantum computer only arises when there is 'hidden structure' in the input data itself. Professor Aaronson and Andris Ambainis proposed this conjecture around 2008 to mathematically prove this idea, and it was formalized in their 2011 paper, "The Need for Structure in Quantum Speedups" 3.

The conjecture concerns properties of a polynomial pp over nn variables. Here, it is necessary to easily understand two key concepts.

  1. Variance: This represents how widely polynomial pp's value is dispersed based on the inputs. If the value fluctuates widely between 0 and 1, the variance is considered high.
  2. Influence: This represents how much polynomial pp's value changes on average when a specific variable is changed from 0 to 1 (or vice versa).

The conjecture states, "If a polynomial's values are widely dispersed (high variance), there must be a single variable responsible for a significant portion of that change (high influence)." Mathematically, it states that the influence of some variable ii (InfiInf_i) must be at least a certain level expressible by variance (VarVar) and degree (dd).

This connects to quantum computers due to the 1998 research results by Beals et al. The results of T queries from a quantum computer to the inputs can be represented as a "low-degree polynomial." If the Aaronson-Ambainis conjecture is true, a classical computer could mimic the behavior of the quantum computer by analyzing the polynomial through intensive queries about "high-influence variables." As a result, it is proven that specific mathematical structure in the input data is essential for a quantum computer to be exponentially faster than a classical computer 3.

In 2019, One Line of Logic Was the Start of Collapse

Professor Aaronson read the 19-page paper closely and evaluated it positively, saying, "It's great!" But on November 20, after Professor Aaronson finished reading, Keller and Klein contacted him to say they were retracting the paper due to the Lemma 5.3 error discovered by Paata Ivanishvili 3.

The problem is that such subtle logical flaws are difficult to detect. When humans read complex math papers, they often "trust" the validity of each line and move on. Even Professor Aaronson recalled, "I trusted and passed over content involving noise operators and hypercontractivity" 3. Specifically, the Keller-Klein proof went through a complex process simplifying a function by analyzing the influence of certain variables; during this process, a specific lemma was a weak link that caused the logic to collapse.

As a result, with the 2019 retraction, the hoped-for proof fell through again, and the conjecture remained unresolved for some time.

The New Rules Created by Lean Verification

The New Rules Created by Lean Verification

The biggest reason the 2026 proof is expected not to repeat the 2019 failure is the use of "Lean." Lean is a tool that translates mathematical papers into code computers can understand and mechanically verifies every step of the logic. A human reviewer might read a paper and judge that it seems "roughly correct," but Lean allows no violation of a single logic rule.

PSI is an AI physics research firm established in September 2026 that uses the 'Emmy' platform, which decomposes physics problems into hypothesis trees and verifies them in parallel 4. In reports of previous projects by the company, it emphasized performing an "adversarial audit." In this proof process, the structure was such that when the AI system wrote the logic, Lean checked it step by step 12.

The table below compares the major differences between the 2019 and 2026 proof attempts.

Category2019 (Keller-Klein)2026 (PSI)
Proving AgentHuman mathematicianAI system (based on proprietary Anthropic model)
Time RequiredAttempt on conjecture open for about 11 yearsDerived in 3 days of execution
Verification MethodReliance on human reviewer judgmentStep-by-step mechanical verification via the Lean language
OutcomeRetracted due to lemma errorMachine verification complete (peer review status undisclosed)

Sources: 123

Gaps Narrowed by Machines, Remaining Tasks

The Aaronson-Ambainis conjecture was an important key to clarifying the inherent limits of quantum computing power. Considering that a single lemma error in 2019 reset the proof attempts for this conjecture, which had remained open for 18 years since 2008, the current proof that completed machine verification in three days is highly meaningful.

PSI's AI configured the logic by running proprietary Anthropic models in parallel, and the results passed Lean's strict step-by-step verification. Complex mathematical intuition comparing polynomial variance and influence was converted into computer code, confirming there are no logical errors.

However, it is still premature to say this proof represents a consensus of the academic community. How traditional peer review proceeds regarding the paper's content and interpretation, and the specific mathematical strategies the AI used to find this solution, are areas outside the public domain. What is important is that a new standard of machine verification has become a powerful tool that narrows "logical gaps," preventing the repetition of past failures.

References

  1. ↩
  2. ↩
  3. ↩
  4. ↩