> I can sit down and prove something using a tool like Isabelle, and I will be as sure of its "truth" as I can possibly be, and it really doesn't matter what other people, mathematicians or not, think about it. That's the beauty of it.
But I guess the point is that almost no-one does this. I would guess that if someone tried to formally verify every published paper out there (or even every textbook), they would uncover a large number of gaps. Very few of those gaps would be unfixable, and very few results would turn out to be incorrect, but the possibility exists.