alt Hacker NewsIf the proof is formally verified but impossible to understand how would anyone be able to be sure the formal verification is correct? Complex software is bound to have bugs, no?
Replies
Jblx2 • yesterday at 10:42 PM
Yes, you still need to be careful, especially if you have reason to think that the proof was from a malicious actor.
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
(N.B. from August 2026)
patcon • yesterday at 10:29 PM
Sincere question, as a non-expert trying to situate your comment: are you a mathematician with experience in proofs?
➕ show 1 reply
The whole point of Lean is that you don't need to understand the entire proof to be sure that it's correct. You only need to understand the definition of the theorem being proven, and you need to trust that the relatively small core of Lean is correct.