> It is a programming language and system, with its own bugs The cool thing about theorem provers is that an invalid proof won’t even compile (as long as the k

> It is a programming language and system, with its own bugs The cool thing about theorem provers is that an invalid proof won’t even compile (as long as the kernel is correct). There’s no such thing as a traditional software bug that happens only at runtime in these systems when it comes to proofs, because there’s no runtime at all. You can also use Lean as a “regular” programming language, with the corresponding risk of runtime bugs, but that’s not happening here.