6 ms·

If 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

If 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?

timjver 1mo ago
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.
- RandomLensman 1mo ago
  Doesn't Lean also have libraries? Anyway, there could also be hardware errors, I suppose.
  - rowanG077 1mo ago
    Lean does have libraries, but since they are also in lean they are subject to the same rules. It's basically a super strong type checker. If it compiles the proof is valid. Unless there is a bug in the type checker.
- gowld 1mo ago
  Why should you trust that the relatively small core of Lean is correct? The core of Lean got a lot less correct when a well-meaning AI system probed Lean for corner cases (bugs) that would "prove" a false conjecture. Corner cases so arcane that no human exploit in a proof. Basically, humans are too stupid to break human-created Lean, but the AI is not.
- raincole 1mo ago
  I don't think Lean is as rigorous as you implied here. https://en.wikipedia.org/wiki/Collatz_conjecture#In_proofs_of_correctness https://en.wikipedia.org/wiki/Collatz_conjecture#In_proofs_o... > In July 2026, a disproof of the Collatz conjecture was verified not only by Lean, but another formal verification system Nanoda. However, investigation quickly revealed that the proof exploited bug(s) in these verifiers.
patcon 1mo ago
Sincere question, as a non-expert trying to situate your comment: are you a mathematician with experience in proofs?
- RandomLensman 1mo ago
  My time proving things is long in the past and any systems way back when I was studying (some math among other things) certainly were different and usually quite narrow. My point was rather more motivated by having seen so many weird ways for machines to fail/not work as expected that I wonder how to deal with that if the output were to be incomprehensible to humans.
Jblx2 1mo ago
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-kernel-soundness-bug-14576/ https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke... (N.B. from August 2026)

If 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?

timjver 1mo ago

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.

RandomLensman 1mo ago
Doesn't Lean also have libraries? Anyway, there could also be hardware errors, I suppose.
- rowanG077 1mo ago
  Lean does have libraries, but since they are also in lean they are subject to the same rules. It's basically a super strong type checker. If it compiles the proof is valid. Unless there is a bug in the type checker.
gowld 1mo ago
Why should you trust that the relatively small core of Lean is correct? The core of Lean got a lot less correct when a well-meaning AI system probed Lean for corner cases (bugs) that would "prove" a false conjecture. Corner cases so arcane that no human exploit in a proof. Basically, humans are too stupid to break human-created Lean, but the AI is not.
raincole 1mo ago
I don't think Lean is as rigorous as you implied here. https://en.wikipedia.org/wiki/Collatz_conjecture#In_proofs_of_correctness https://en.wikipedia.org/wiki/Collatz_conjecture#In_proofs_o... > In July 2026, a disproof of the Collatz conjecture was verified not only by Lean, but another formal verification system Nanoda. However, investigation quickly revealed that the proof exploited bug(s) in these verifiers.

patcon 1mo ago

Sincere question, as a non-expert trying to situate your comment: are you a mathematician with experience in proofs?

RandomLensman 1mo ago
My time proving things is long in the past and any systems way back when I was studying (some math among other things) certainly were different and usually quite narrow. My point was rather more motivated by having seen so many weird ways for machines to fail/not work as expected that I wonder how to deal with that if the output were to be incomprehensible to humans.

Jblx2 1mo ago

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-kernel-soundness-bug-14576/ https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke... (N.B. from August 2026)