> Additionally, I'm consider two types of "bugs". (1) bugs in software or hardware that the stack relies on; Then run the Lean proof on a non-x86 computer and

> Additionally, I'm consider two types of "bugs". (1) bugs in software or hardware that the stack relies on; Then run the Lean proof on a non-x86 computer and on both Windows and Linux. The possibility that two independent computer architectures and two independent operating systems converge on some buggy behaviour that just so happens to allow a buggy proof through is so remote it's not worth considering further. > (2) "bugs" in the conceptual sense of a Lean construction being something different than what was meant or what people thought it was, which is effectively the same problem that regular mathematics runs into. A specification is orders of magnitude shorter than proofs, on average. So if you're saying they managed to reduce the amount of manual verification work and possible human error by orders of magnitude, that sounds like an uncontroversial win for correctness.