Well, the author's point is probably still generally correct - in almost all fields proofs are not presented from axioms, and you could easily go your whole lif

Well, the author's point is probably still generally correct - in almost all fields proofs are not presented from axioms, and you could easily go your whole life as a mathematician without encountering such a proof, except perhaps by accident. His point was that formal proofs are "hypothetical", not that they are rarely encountered. What part of > The trouble is, no one has ever carried out that filling-in process. It’s purely hypothetical. don't you understand? I'm currently writing my undergraduate project in a proof assistant, and you end up with tonnes of unreadable garbage like ASM_SIMP_TAC (srw_ss ()) [DETERMINACY_LEMMA, simp_expand_def] THEN1 METIS_TAC [] THEN RW_TAC (srw_ss ()) [ss_ecases] THEN FULL_SIMP_TAC (srw_ss ()) []. which has no real relation to any normal thought. The syntax you describe bears very little relation to formal system like Metamath in which proofs are readily checkable by people and machines. I also think that his line (it almost certainly is not, but more pertinent, how could you ever be sure it is?) is still a good point - you're trusting your correctness to a computer program, and all of the libraries built on top of it. No. Metamath proofs can easily be verified by hand.