Note that my comment distinguishes between automated theorem proving and automated proof checking. I made remarks for each; I admit it may have been unclear, bu

Note that my comment distinguishes between automated theorem proving and automated proof checking. I made remarks for each; I admit it may have been unclear, but my point about searching a language space refers to automated theorem proving in particular. My second point about the requirement to verify "dependencies" for a theorem is a comment on why automated verification is difficult. As for what I meant by that last point - there is a huge amount of mathematics to encode, almost all of which has not been formally specified into types, and much of which is structurally redundant. Not only is it difficult to encode necessary prerequisite mathematics for a theorem, but that requires its own effort and care, which multiplies the effort required for a given nontrivial proof to be checked. Also note that I'm distinguishing between the general infeasibility of automated theorem proving and the otherwise great (but ordinarily feasible) difficulty of automated proof checking.