Prominent theorist says AI-found quantum computing proof is "probably correct"

A proof of an open problem in quantum computing, reportedly found by AI, has received its first positive assessment from a prominent outside expert. Scott Aaronson, a quantum computing theorist and professor at the University of Texas at Austin, and one of the two people the conjecture is named after, wrote on his blog that the proof is probably correct. He added, however, that he does not yet understand the proof. What has been shown is a narrow result rather than the full conjecture, and it has not been formally peer-reviewed. On the question of who verifies mathematical results produced by AI, and how, the proof has cleared only half of the first hurdle.

For Japanese companies: This does not affect most companies. It matters to R&D departments, in manufacturing, pharmaceuticals and other industries, that use AI for research, analysis or checking designs. Before using AI-generated results in public announcements, patents or explanations to business partners, check this month whether your company has a rule requiring a record of who in-house verified them independently. As this case shows, passing a machine check, or even being called probably correct by a prominent expert, does not on its own make a result settled.

What happened

The story goes back to November 6. An organization called PSI claimed on its website that it had proved the Aaronson-Ambainis conjecture using an unreleased Anthropic model. It also said the proof had passed a check in Lean, a tool that verifies proofs by machine. At that point, however, there was no third-party confirmation.

Aaronson has now given his assessment in a new post. His conclusion is that the proof is probably correct. It is the first time a prominent expert outside PSI has put their name to a judgment on the proof. A related paper has also been posted on arXiv, the repository for papers that have not yet been peer-reviewed.

Why his word carries weight

The Aaronson-Ambainis conjecture was posed more than a decade ago by Aaronson and Andris Ambainis, a computer scientist at the University of Latvia. Broadly speaking, it puts in mathematical form the idea that, for problems without some structure to exploit, quantum computers cannot achieve an exponential speedup over ordinary computers. It is one of the field's basic questions about how much advantage quantum computing can offer.

The person who posed the conjecture and has thought about it for years has written that the proof is probably correct. That makes his assessment one of the most qualified in the field. Aaronson is also not a reviewer picked by the company or organization behind the proof. In AI mathematics, mathematicians' organizations have objected to the practice of labs announcing results after having them checked by mathematicians the labs chose themselves. An independent expert writing his own judgment on his own blog carries a different kind of weight.

Three reasons it is not yet settled

First, Aaronson himself says he does not yet understand the proof. His "probably correct" is not a judgment made after working through the details line by line himself. Because his name carries weight, his assessment should be taken at its literal word.

Second, what has been shown is a narrow result. It does not mean the conjecture itself has been solved in full. Reading only the headlines and concluding that the limits of quantum computing have been settled would be going too far.

Third, there has been no formal peer review. There is a claim that the proof passed a Lean check, but what the machine verifies is whether the stated proposition follows correctly. It does not guarantee that the proposition correctly captures what people mean to claim. In October, after OpenAI and Anthropic each claimed to have used AI to disprove separate complexity conjectures, experts pointed out cases where the claims written in Lean were weaker than those in the papers.

What to watch next

There are three things to watch. First, Stanford researchers are reportedly preparing a summary for other experts. If it comes out, the number of people checking the proof could grow quickly. Second, what Ambainis, the conjecture's other namesake, has to say. Finally, whether other experts independently check the details and the work moves on to peer review at an academic journal.

This fall has brought a string of stories about AI tackling open problems in mathematics. In each case, the speed at which humans can verify has not kept up with the speed at which AI produces answers. This time, things have gone as far as an outside expert writing that a proof is probably correct. They have not yet reached the point where humans understand and fully verify it.

What this article could not confirm

Which parts of the result Aaronson considers narrow; the authors of the arXiv paper and the exact scope of its claims; the name of the Anthropic model PSI says it used. This article was unable to confirm these in detail. Anthropic has made no announcement as a company about the model. We also could not find any response from Ambainis himself.