Quantum: an AI solved a problem that has been open since 2008, what does that change?

Eighteen years. That's how long the best quantum computing specialists spent banging their heads against the same maths problem. And on Friday, November 6, a small American outfit, Physical Superintelligence, announced that it's sorted. Not by a genius locked away in an office: by an AI, in three days of computation. And not just any AI, since it's a model from Anthropic that hasn't been released yet, the cousin of the one I code with every day. Well, I'm not going to play it cool.

The problem dated back to 2008, and an AI wrapped it up in three days

Because we often hear about AIs that “solve maths”, and most of the time it's a machine quickly doing again what we already knew how to do. Here, it's the opposite: researchers at Stanford had only solved a piece of it this summer, and the AI produced a complete proof, checked by software that lets nothing through. That's exactly what I've been expecting from an AI for years: for it to find what nobody had found before.

What was the question?

In 2008, two researchers, Scott Aaronson and Andris Ambainis, made a bet. Everyone dreams of quantum computers that would go billions of times faster than ours. They ask themselves: is that true for any problem, or only for some?

Take a machine that has to answer yes or no by reading a huge pile of data. Their intuition: if this data is pure randomness, with no hidden pattern, the quantum computer might go faster, but never by an astronomical amount. The gap can be big, it never becomes insane. The real turbo boost, the gigantic gain, it only gets it when the data has a structure, a repeating pattern, a regularity it can exploit.

That's actually how Shor's famous algorithm works, the one that makes banks tremble because it could break some of the Internet's secret codes: it spots a pattern that repeats in numbers, and takes advantage of it. With a pile of data in no particular order, no miracle.

On the left, a repeating pattern: the quantum computer finds a shortcut. On the right, randomness: no miracle

The snag is that for eighteen years, nobody managed to prove it. Everyone believed in it, loads of particular cases held up, but the general proof resisted. In 2019, Scott Aaronson had even titled a post on his blog “The Aaronson-Ambainis conjecture (2008-2019)”, like a tombstone, after a proof announced by two other researchers. It didn't hold up, and the question was still open this summer.

Three days of computation, and a checker that lets nothing through

What Physical Superintelligence describes is a home-built research system that runs several copies of Anthropic's model in parallel. They rummage through papers that have already been published, suggest ideas, combine approaches, test lines of reasoning and throw out the ones that don't hold up. The researcher who was steering the whole thing, David Turturean, chose the problem, started the machine, then reread and tweaked the draft. On the third day, the complete proof was there.

And the best part came along the way: the AI started from a plan proposed by two researchers, Shachar Lovett and Jiapeng Zhang, which ran into an inequality they had never been able to prove. It discovered that this inequality was false in its general form, and found another one, true, that does the same job. Then we ran it again on related problems, and it improved its own result twice more. Pchhh. And here I am still rereading every file Claude Code gives me!

Now, a math proof written by an AI can also be a load of gibberish that looks right. I was talking about it a month ago with OpenAI's AI, which had solved 372 problems, but whose proofs nobody understood. Here, the difference is Lean, software that checks mathematical reasoning line by line, like the most annoying math teacher in the world: no “it is obvious that”, no “we assume”, every step has to be justified all the way to the end or it rejects everything. Lean accepted the proof. Then the improved version. And the team repeated the verification with a second checker, written by other people, to make sure it wasn't Lean itself that was getting it wrong.

Lean checks every step of the proof, without exception

The detail that made me smile: everything is online, on GitHub, and anyone can rerun the verification at home. You just need to allow for 173 GB of memory if you're in a hurry, roughly ten times what a good desktop PC has, or a more modest machine and eleven minutes of patience. It still takes less time than waiting for a peer review committee's opinion.

Hmm, there are still a few asterisks

Okay, let's be honest for two minutes. For now, this is a company's announcement, with a manuscript that hasn't gone before any scientific journal. Aaronson and Ambainis themselves haven't said anything publicly. The Stanford researchers who had solved the particular case in August are reading the proof and preparing a shorter version for specialists, and their first impression is enthusiastic: “Everything comes together in a fairly magical way”. But an enthusiastic reading is not validation yet.

And Lean only guarantees what it is given to check. Humans still have to confirm that the statement entered into Lean really says the same thing as the original conjecture. One of the four theorems also relies on a result published by other researchers, which hasn't been checked by the machine. Nothing suspicious there, that's how all mathematicians work, but it means that the “100% verified” claim comes with a small footnote.

One last clarification, so we don't make it say just anything: the result counts how many times the machine has to READ the data, not its total computing time. It doesn't say that quantum computers are useless, it says where to look.

Okay, and what use is that to you?

I know, a theorem about polynomials isn't going to change your family's life tomorrow morning. But there are three things that concern you.

First, your money. Quantum computers swallow billions, and some of that comes from your taxes: in France alone, the national plan announced in 2021 weighs in at 1.8 billion euros. And they are often sold to you as machines that will speed everything up. This theorem says in black and white that no: your spreadsheet, your Google search or your video game won't run a thousand times faster thanks to them. These machines will be useful where there is a structure to exploit, like the chemistry of medicines, your electric car's batteries or certain secret codes. Knowing where not to look helps avoid burning money. And that's exactly the question DARPA is asking itself, testing six machines to find out whether one of them will ever be profitable.

Next, and this is the most important thing for me, trust. The day an AI knows how to produce a proof that software checks all by itself, we can imagine programs delivered with their demonstration, not just with tests. It already exists on a small scale: the automated metro on line 14, in Paris, has been running without a driver since 1998 with safety software mathematically proven before it went into service. Except that it had cost specialists years of work. If an AI does this work in a few days, this kind of guarantee could make its way into your car's brakes, the hospital's infusion pump or your bank's software.

A driverless metro whose safety software was proven before it ran

Finally, the research itself. Problems that have been stuck for decades could fall one after another, with AI searching and humans checking. There is a reassuring precedent: in 1976, the four-color theorem (you can color any map with only four colors without two neighboring countries having the same one) was proved with the help of a computer, and a good part of the mathematicians had cried foul. In 2005, the proof was fully checked by software of the same kind as Lean, and no one contests it anymore.

The timeline, honestly? For useful quantum computers, people talk about ten years, maybe more. For everyday software shipped with its proof, I don't dare give a date. But for mathematics, it has already begun, and it was Friday.

Personally, I find that huge. A machine that proves what humans had failed to prove, and that agrees to be checked line by line, that's the dream. And to Anthropic: when are you going to release the model that did this to us? Because my three Claude Code sessions are waiting for it with their feet firmly planted!

Sources

• Physical Superintelligence, November 6, 2026: a proof of the Aaronson-Ambainis conjecture (in English)
• GitHub: the manuscript and the Lean verification, with its caveats
• The Quantum Insider, November 6, 2026: an AI-assisted proof settles an old question about quantum speedups
• Scott Aaronson, November 2019: the Aaronson-Ambainis conjecture (2008-2019)

Article written with the help of Claude Code, reread and corrected by me.