A startup called PSI (Physical Superintelligence) says its research system, running an unreleased Anthropic model, found a proof of the Aaronson-Ambainis conjecture — a quantum computing question that’s been open since 2008. Complete proof on day three of the run, and Lean, the proof-checking software, accepted every step. They then had the system keep going and it improved the result twice. Paper and the full Lean formalization are public on GitHub.
The part I keep going back and forth on: this is genuinely the kind of thing people said AI couldn’t do yet — original math, not just summarizing papers — but the model itself is unnamed and nobody else can use it, so nobody can rerun the experiment. And Lean checks that the formal proof is internally consistent, which is a big deal, but humans still have to confirm the formal statement actually matches the conjecture as printed. No peer review yet, and Scott Aaronson himself hasn’t publicly weighed in as of this morning.
So… does a machine-checked proof count as ‘solved’ before the experts have had their say? Or is that just the new normal for how math gets done?
Hmm, this is a thoughtful moment for math and tooling alike. A machine-checked proof that passes Lean is a strong signal, but the ultimate validation still sits with human experts confirming the statement matches the conjecture’s formulation. It’s the chain-of-trust: machine-verified steps, human-verified statement alignment, and then peer review. In practice, I’d treat it as “proof sketch solidified by formalization,” pending independent replication and peer scrutiny.
If you want a concrete angle to go after here: explore how to assess the gap between a formalized proof and the original mathematical claim. For example, a tight checklist could be:
Ensure the Lean formalization exactly encodes the conjecture as stated in the source.
Identify any extra lemmas introduced by the formalization and verify they’re globally valid for the claimed statement.
Check whether the formalization requires nontrivial assumptions (e.g., specific axioms) beyond what the conjecture assumes.
Confirm reproducibility: can others run the same Lean script and arrive at the same conclusion without access restrictions?
If you’d like, I can draft a quick mapping table from a public write-up to a Lean encoding checklist you can reuse when evaluating such claims.
Yeah, that chain-of-trust framing is the part that stuck with me too. Lean saying the steps check out is one thing — the interesting question is whether the thing it checked is actually the conjecture as stated, and that’s not something the checker can tell you.
Your checklist gets at exactly that, especially the bit about extra lemmas and hidden assumptions sneaking in during formalization. That’s where these claims usually get wobbly, if they do at all.
I think “proof sketch solidified by formalization” is about the right label for now. Impressive, and the three-day turnaround is wild, but still waiting on someone independent to reproduce it and on the experts to sign off that the statement actually matches up.
