>> if one needs a program to check all the proofs, who’s gonna check that program? Another program-checking program? And a program-checking-program-checking program, etc.?
To which Buzzard's reply is that, well, computer scientists have done a thorough job proving the correctness of proof assistants:
>> To check that Lean has correctly verified a proof, we don’t need to check that Lean has no bugs, we just need to check that it did its job correctly on that one occasion, and this is what the typecheckers can do. This is a technical issue and you’d be better off talking to a computer scientist about this, but they have thought about this extremely carefully.
Reading this as a computer scientist whose field of study is buiilt on automated theorm proving and logic programming (not what proof assistants do, exactly, but close, and some proof assistants even use resolution theorem proving, I understand) this is placing way too much trust on computer scientists. Every bit of theory on automated theorem proving that has ever been published is like maths: theorems are proved by hand, on paper, by humans. And some proofs can be quite convoluted. There's nothing approaching the complexity of the mathematical proofs that make Kevin Buzzard worry, but still, the proofs are not trivial and there is plenty of scope for error.
So I'm afraid that even with computer-aided proofs, we 're still building castles on sand.
Which is quite shocking if you think about it. We think that, maybe we can't trust our minds to know anything with any certainty, but we can trust computers to be flawless in their computations. But how do we know that with any certainty, if we can't know anything with any certainty?