Claimed AI proof of an open quantum computing problem passes a machine check but awaits independent confirmation

An organization called PSI has claimed on its research page that it used AI to prove the 'Aaronson-Ambainis conjecture', a problem in quantum complexity theory that has gone unsolved for more than 15 years. PSI says it used a model that Anthropic has not yet released. It writes that the proof passed a check by Lean, software that verifies mathematical proofs by machine. No human researchers have yet confirmed the proof independently. The situation mirrors October, when OpenAI and Anthropic announced that they had refuted ETH, a major hypothesis in complexity theory. The question is no longer whether AI can write a proof, but who decides that the proof is correct.

For Japanese companies: For most companies, this has no immediate impact. R&D and new-business teams that are considering quantum computing pilots or investments should check, the next time they hear a pitch, whether a vendor's promised "speedup" depends on special structure in the problem. Until the proof is settled, it should not be used as a basis for decisions.

What PSI says it proved

The Aaronson-Ambainis conjecture was put forward around 2009 by complexity theorist Scott Aaronson, a professor at the University of Texas at Austin, and quantum algorithms researcher Andris Ambainis of the University of Latvia. Roughly, it asks the following question: if a problem has no special structure and its inputs are random, can a quantum computer still answer dramatically faster than a classical computer?

The conjecture says the answer is no. It states that if a quantum algorithm makes T queries, a classical algorithm can simulate it on most inputs with a number of queries polynomial in T. Mathematically, it says that every low-degree polynomial whose values stay within a bounded range must have at least one highly influential variable. Until now, only partial results existed.

If the proof is correct, it would give theoretical backing to the view that dramatic quantum speedups are limited to problems with special structure, such as integer factoring. It would put a check on the pitch that "quantum makes everything faster."

What a machine check does and does not guarantee

PSI writes that its proof passed Lean's check. Lean is software that checks by machine whether every step of a proof follows the rules of logic. This year it spread rapidly as a way to check long proofs written by AI.

However, Lean guarantees only that "the statement written in Lean follows from the proof." Lean cannot say whether that statement means the same thing as the conjecture as humans understand it. This was exactly the issue in October's ETH case. Complexity theorist Lance Fortnow pointed out on his blog that OpenAI's Lean statement was slightly weaker than the claim in its paper. The proof passed the check, but what it proved was weaker than the headline claim.

Lean also has limits of its own. In July and August, a series of bugs were found in Lean's core that could let incorrect proofs through. In October, mathematician Thomas Hales, in a guest post on Terence Tao's blog, proposed checking the same proof against several independent checkers. This is why Anthropic ran its ETH proof through both Lean and a separate checker.

Following the path of the ETH refutation

On October 26–27, OpenAI and Anthropic each announced that their models had refuted ETH (the hypothesis that problems like 3-SAT take close to brute-force time no matter how clever the approach). Both proofs had passed Lean's check. Even so, Anthropic's paper itself stated that, at the time of writing, no human had verified it.

Complexity theorist Ryan Williams (MIT), who was asked to help verify the proof, said parts of it were routine but that there were "two or three parts that look alien," and said the whole research community would need to work on it. Nearly two weeks after the announcements, no one has reported that independent verification is complete.

The way verifiers are chosen has also drawn criticism. On October 25, AGMAI, an advisory group on mathematics and AI, criticized the practice of having company-selected mathematicians verify AI results in a guest post on Tao's blog. It noted that access to the materials is limited to a narrow group, and that companies can use the reputations of the people they choose as a shield. PSI's claim will be judged by the same standard.

Another barrier: an unreleased model

This claim is harder to check than the ETH result in one respect: outsiders cannot use the model PSI used. If the proof text and Lean files are made public, anyone can check the proof itself. But it is hard to verify from the outside whether the same model would produce the same result, how many attempts the result was selected from, or where humans stepped in.

It is also notable that the capabilities of a model Anthropic has not yet released came to light through an announcement by an outside organization rather than by Anthropic itself. Outside organizations claiming major results with powerful models before the labs release them looks likely to become more common.

What to watch next

There are three things to watch. First, how quantum complexity researchers judge the proof, especially Aaronson and Ambainis, who proposed the conjecture. Second, whether third parties check that the Lean statement is as strong as the standard form of the conjecture. Third, how much PSI or Anthropic discloses about the model used and the process that led to the proof.

In preparing this article, we were unable to verify the details of PSI's page. This article does not report when the announcement was made, what kind of organization PSI is, the name of the model used or how PSI obtained access to it, the length of the proof, the version of Lean used for the check, or how much humans were involved. We have treated as fact only what PSI claims and PSI's statement that the proof passed Lean's check.