I think that's making it sound a little more fragile than it actually is. Within a system like Isabelle, the formalisation of each piece of the proof must rema

I think that's making it sound a little more fragile than it actually is. Within a system like Isabelle, the formalisation of each piece of the proof must remain relatively consistent with both the built-in proofs about fundamental mathematical structures, as well as the proofs that you have written. I say "relatively consistent" because I don't have enough experience with the internals of Isabelle to say with certainty as to exactly how consistency is enforced. I know that types are enforced in a globally consistent way, for example. That said, I have a high degree of confidence in the correctness of machine-checked proofs. So I understand that your point is that you're taking some leaps of faith, and I agree to a point, but I think they are much more reasoned and considered leaps than you suggest.