An AI system has produced a proof of the Aaronson-Ambainis conjecture, a question about quantum computers that two computer scientists posed in 2008 and that nobody had been able to answer. The start-up Physical Superintelligence built the system and ran it on an Anthropic model that is not public. It had a complete proof on the third day of its run, and Lean, a program that checks every step of a mathematical proof, accepted it.
What the conjecture decides
Quantum computers are known to be exponentially faster at a few jobs. The best known is Shor's method for factoring large numbers, which works because the numbers hide a repeating pattern that a quantum computer can find. The open question was whether a quantum computer can also be exponentially faster when the data has no pattern, so that a yes-or-no answer depends on a long string of random 0s and 1s.
Aaronson and Ambainis showed that this comes down to a fact about a kind of formula. Think of the quantum computer's chance of saying yes as a dial wired to one switch for each bit of the data. Their conjecture was that unless the dial barely moves, some switch always moves it by a noticeable amount. If that holds, an ordinary computer can imitate the quantum one. It looks at the switch that matters most, then the next one, and stops when none of the rest changes the answer much. For almost every input, that takes only somewhat more looks at the data than the quantum computer needs, not exponentially more. The proof shows the conjecture holds.
What it leaves alone
The result closes one door and leaves the others as they were. Shor's method works on patterned data, so it is untouched, and the threat it poses to current encryption is the same as before. Simulating molecules does not depend on this kind of setup at all. Even for random data, quantum computers can still be exponentially faster at some search problems, where the job is to find an answer instead of saying yes or no. Scott Aaronson's own account goes through each of these.
None of that stopped a widely shared post from declaring quantum supremacy dead within a day. For a business reader, the useful question about any quantum pitch is whether the problem has a hidden pattern, as factoring does. A pitch that promises an exponential speedup on a yes-or-no question about patternless data now has a proof against it, at least when speed is counted in how many times the data must be read.
The machine checks, the people decide what it means
The 2019 attempt shows what checking used to cost: specialists reading line by line for weeks. Here the check came with the proof, so the people now reading it, including a group at Stanford and MIT writing a shorter explanation for other specialists, can spend their time understanding it instead of hunting for mistakes.
The same split will show up in ordinary work. A finance team could ask an AI to match 5,000 invoices to bank payments, and a short script can confirm that every matched total adds up. That check settles whether the answer is right. It does not show whether the team asked the right question. We saw the same pattern when AI formalized Fermat's Last Theorem: where a program can certify the answer, you can use the AI's output without trusting the AI, and deciding what the answer means stays with you.
These results are going to arrive often. In October, OpenAI and Google DeepMind each published batches of open problems their systems had solved, with Lean-checked proofs. Aaronson thinks humans would very likely have solved this one given more years, and he may be right, but the AI did it in three days of running and then improved the result twice. Each new headline will need the same two questions: did a program check it, and what exactly does it cover?
The proof is a landmark for mathematicians. For anyone planning around quantum computers, from encryption to new materials, the plan is the same as it was before the proof.