Comment by mrob

>Indeed there are theorems that say the tool must malfunction at least sometimes.

Gödel's incompleteness theorem only states that there are true statements that can never be proved to be true. That limits what tools can do, but it's not a "malfunction". The exact same limitation applies to humans. A genuine malfunction would be if the tool "proved" a false statement to be true. That actually has happened before because of bugs in proof checkers, but software bugs can be found and fixed, and proof checkers are simple enough that it's possible to write many different implementations. It's extraordinarily unlikely that the same malfunction occurs in all of them.