Will we ever see a soundness bug in the lean kernel again?
To a software developer the question seems insane. There were bugs in the past, of course there will be more.
When we see those bugs, what will it mean for AI lean proofs? Can we trust them?
This whole thing boils down to trust.
We can trust human verifications highly because of community and reputation and human proof-of-work. Humans sometimes lie about math results but it's rare because of this. They make mistakes and those mistakes are discovered by communities who are themselves largely trustworthy because of this.
LLMs don't care about reputation. They hallucinate and fabricate often. In harnesses they literally try to cheat and bend rules, which is a disaster for knowledge that is encoded in rules. So we have to rely on proof checkers.
The problem is, how trustworthy are proof checkers? Are there bugs? And is the underlying theory itself free of paradoxes and unknowables and mathematical "bugs" that can be exploited? Imagine a human mathematician hell bent on deceiving other mathematicians - would we trust their breakthroughs, even with a verifier?
Because of these properties, the final backstop has to be humans, and rooted in the community and proof-of-work based human trust system. At the moment people are trusting the tools too much.
Prediction: bugs will be found by humans using AI tools that call into question the Navier-Stokes proof.
JonChesterfield [3 hidden]5 mins ago
> Autoformalization has become a practical reality in 2026
Uh, _maybe_. I've been translating papers into lean for the last week and the correlation between the formalized result and the papers is extremely poor. The cycle seems to be "have a go at the paper, it's a bit hard, prove something different, proclaim success". It's still faster than doing it all by hand but paper in -> lean out in no way ensures a correspondence between the two.
gus_massa [3 hidden]5 mins ago
> prove something different
I'm not sure but do you mean "prove the final end result using a [¿slightly?] different path"?
Retric [3 hidden]5 mins ago
No, prove something else could mean proving something very trivial thus making the proof meaningless on its own.
IE a proof can be true, rigorous, and not at all what was asked for.
HN.zip
To a software developer the question seems insane. There were bugs in the past, of course there will be more.
When we see those bugs, what will it mean for AI lean proofs? Can we trust them?
This whole thing boils down to trust.
We can trust human verifications highly because of community and reputation and human proof-of-work. Humans sometimes lie about math results but it's rare because of this. They make mistakes and those mistakes are discovered by communities who are themselves largely trustworthy because of this.
LLMs don't care about reputation. They hallucinate and fabricate often. In harnesses they literally try to cheat and bend rules, which is a disaster for knowledge that is encoded in rules. So we have to rely on proof checkers.
The problem is, how trustworthy are proof checkers? Are there bugs? And is the underlying theory itself free of paradoxes and unknowables and mathematical "bugs" that can be exploited? Imagine a human mathematician hell bent on deceiving other mathematicians - would we trust their breakthroughs, even with a verifier?
Because of these properties, the final backstop has to be humans, and rooted in the community and proof-of-work based human trust system. At the moment people are trusting the tools too much.
Prediction: bugs will be found by humans using AI tools that call into question the Navier-Stokes proof.
Uh, _maybe_. I've been translating papers into lean for the last week and the correlation between the formalized result and the papers is extremely poor. The cycle seems to be "have a go at the paper, it's a bit hard, prove something different, proclaim success". It's still faster than doing it all by hand but paper in -> lean out in no way ensures a correspondence between the two.
I'm not sure but do you mean "prove the final end result using a [¿slightly?] different path"?
IE a proof can be true, rigorous, and not at all what was asked for.