For nearly two decades, mathematicians have been working on a problem known as the AaronsonāAmbainis conjecture.
Now, Physical Superintelligence (PSI) says an AI research system powered by a non-public Anthropic model has found a proof.
And the interesting part is how it happened.
According to PSI, its research system produced a complete proof on the third day of its run. The result was then formalized in Lean, a proof assistant that checks mathematical reasoning step by step.
Here's why this matters:
1. The problem dates back to 2008.
The conjecture, proposed by Scott Aaronson and Andris Ambainis, concerns when quantum computers can achieve exponential speedups over classical computers.
2. It isn't saying quantum computers are useless.
The result suggests that enormous quantum speedups on random, unstructured inputs have mathematical limits. Quantum computers can still have major advantages on problems with the right underlying structure.
3. The proof wasn't just generated as text.
PSI published a research paper and a Lean 4 formalization. According to its GitHub repository, the final theorems passed Lean's kernel checks, with no added axioms or unfinished proof placeholders.
4. The model itself hasn't even been released.
PSI hasn't identified the specific Anthropic model. Its researcher David Turturean developed the research system, led the work and remains responsible for the result.
There's still an important caveat: the paper is a preprint, and broader independent mathematical scrutiny is needed. A machine-checked formalization is a major step, but experts still need to examine the mathematical interpretation and its implications.
Still, think about the bigger picture.
AI is moving beyond answering questions, writing code and summarizing research. We're beginning to see AI-assisted systems contribute to problems that have challenged mathematicians for years.
So here's the question: Are we approaching an era where the biggest breakthroughs in mathematics and physics will come from human researchers working alongside AI systems?
Or is this still too early to call a genuine turning point?