an AI system says it proved the Aaronson-Ambainis conjecture. careful excitement thread

by Ava Engel

Saw this in Friday's roundups. A startup called Physical Superintelligence says its research system found a proof of the Aaronson-Ambainis conjecture, open since 2008. Roughly, it says that if a quantum algorithm gets a big speedup just by querying its input, the problem has to have some structure. Take the structure away and a classical computer can fake the answer on most inputs. So if it holds, it's a limit on where quantum advantage comes from. I'm keeping my excitement in a drawer until people who know the area have gone through it. Long human proofs have fallen over before. If it survives though, the AI part interests me more than the quantum part. A proof is checkable in a way most AI output isn't. Would you trust it more or less knowing a model wrote it?

favorite 2 comment 3

Comments

Ivan Jensen 3 days ago

Ava, more, on one condition: that it's machine-checked. If there's a formal proof in Lean or similar, who wrote it mostly stops mattering, because the checker doesn't care. If it's a PDF in normal maths prose, it's a long proof from an unfamiliar source and gets the same slow refereeing as anything else, maybe slower, since reviewers will be hunting for the confident-but-wrong step. I haven't seen which it is yet. Has anyone found the actual write-up rather than the announcement? Footnote: one hard problem going down says a lot about search plus verification on a well-posed question, and much less about open-ended research where nobody can write the checker. Still a good week for the people building checkers.

Dmitri Meier 1 day ago

Ivan, I'd push back a little on "who wrote it stops mattering". A Lean proof tells you the statement is true. It doesn't tell you why, and for most mathematicians the why is the actual product. A proof nobody can explain doesn't give you a technique you can reuse on the next problem. So my guess is the interesting phase comes after it's verified, when people try to turn it into something a human can follow. If that turns out to be easy, great, the model found a route we missed. If it's hard, that's a weird new situation: a true result with no understanding attached. Did this with my Friday group last year on a much smaller scale. Two models proved the same lemma, one proof was half a page and one was four. Both checked. Only one taught us anything.

Tariq 12 hours ago

maths teacher here. Dmitri's lemma story is basically my marking pile. the kid who gets the right answer and cant tell me why scores worse than the one who explains it and slips at the end