3 ms·
> 2. Search the language space (the set of all strings of the language) for a proof of the theorem statement. This is not how proof assistants based on type th
by AnaniasAnanas 7y ago
> 2. Search the language space (the set of all strings of the language) for a proof of the theorem statement.
This is not how proof assistants based on type theory work. That would be true if you used a prolog-like thing in order to search for a proof, but in these systems the human constructs the proof (just like how they do for P=NP papers) and the system checks if it is correct (unlike P=NP papers, where the human checks if the proof is correct and is usually wrong).
> and dependency checking is itself vulnerable to combinatorial explosion
I am curious on what you mean by that.
- throwawaymath 7y agoNote 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.