An AI system proved an 18-year-old quantum conjecture in three days

Physical Superintelligence, a company that goes by PSI, says a research system it built proved the Aaronson-Ambainis conjecture. The conjecture is a question in quantum computing. It was open since 2008. The company posted the proof on its own site on 6 November. TechCrunch reported the result on 10 November.

The conjecture asks whether a quantum computer can be much faster than a classical one on random inputs. PSI says the answer is no. On random inputs, the gap can only be polynomial in size. A larger, exponential gap is ruled out. In the company's words, the conjecture "is now a theorem".

How the proof came out

PSI says it ran "instances of a non-public Anthropic model" inside a research system on its own infrastructure. TechCrunch reports the model is Fable 5.2, with early access before release. PSI's own page does not name it.

The system had a complete proof on the third day of the run. It then wrote the proof as a Lean file. Lean is a proof assistant. It checks every step of a proof on a computer. Lean accepted the file. The system then kept running and improved the result twice. Each new version was accepted the same way.

Who checked it

PSI's advisor Jim Halverson audited the proof. Four researchers at Stanford, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, reviewed it. In a quote on the PSI page they call it "a huge result" that settles a decades-old conjecture.

David Turturean led the work at PSI. The company says he is responsible for the correctness of the result.

What PSI sells

CEO Matt Pines told TechCrunch the company is a "frontier research laboratory". PSI's current paying work is a side business. It simulates data centres: heat flow, power use and water. That revenue funds the research. TechCrunch did not report a customer count, a funding figure or a headcount.

The scope of the result

PSI describes the proof as "a negative result". The conjecture only covered random inputs. For inputs with structure, such as factoring a number, quantum computers can still be much faster. Those problems are a separate question.

A reader in software can take two facts from this. First, the hard step was writing the proof in Lean. Lean is where a human can check the work, step by step. Second, the output is reviewable code that anyone can rerun. A team buying AI work can ask for the same shape. The model gives an answer. A second tool checks every step before anyone acts on it. That pattern turned a three-day run into a result Stanford researchers were willing to review.

Source

• The Aaronson-Ambainis Conjecture, Physical Superintelligence.
• PSI is trying to make a business out of AI-driven scientific discovery, TechCrunch, Tim De Chant.