Interesting. I've thought about this exact topic before and I think his point shouldn't be dismissed so lightly. What got me thinking about this was an occasio

Interesting. I've thought about this exact topic before and I think his point shouldn't be dismissed so lightly. What got me thinking about this was an occasion (years ago) when I read a proof in which I didn't understand the jump from one assertion to the next one. It occurred to me then that the atomicity in these proofs (on which the entire structure stands) boils down to steps which are considered to be obvious. However "obvious" is a relative term, not an absolute one. So, at least as most proofs are concerned (and most proofs are not machine generated), his point is valid. As for systems like Metamath - how rigorous are the proofs that the software is bug free ? If you really want to philosophise over this, I'd even suggest that ultimately one can't really prove anything. At most, you can believe some assertion is correct to the degree you trust your senses, memory and logic - but I'll stop before this devolves into metaphysics...