4 ms·

They don't do it because the technology just isn't there yet. Automated theorem checking is typically very difficult for any nontrivial theorem; automated theor

They don't do it because the technology just isn't there yet. Automated theorem checking is typically very difficult for any nontrivial theorem; automated theorem generation is so extraordinarily difficult, it's generally infeasible. The steps to construct a proof of a theorem are as follows: 1. Formally define a language specification which will ostensibly contain the theorem statement and a proof. 2. Search the language space (the set of all strings of the language) for a proof of the theorem statement. 3. If step 2 fails, change the language specification to include prerequisite mathematics or an alternative statement of the theorem. Even when you exploit clever structural properties of the theorem statement and the language definition, it's extremely easy to encounter a combinatorial explosion when you search for a proof. On the other hand, suppose you already have a proof and simply want to verify it using a proof assistant. In order to do so, the language you define must be able to automatically verify all prerequisite mathematics which your proof depends on. Encoding that mathematics into a language is difficult and tedious, and dependency checking is itself vulnerable to combinatorial explosion. It's a very active area of research in its own right, but it can't obviate this problem for the foreseeable future.

andrewla 7y ago
> Automated theorem checking is typically very difficult for any nontrivial theorem I'm not sure this is true -- I thought the whole idea of these theorem systems was to make the kernel of the proof system as simple as possible (to allow a manual proof, or at least high confidence of correctness). If your program can produce an instance of a type, and it type-checks, then it true. Type inference can be tricky, and a lot of what makes the systems usable is the fact that you can omit types and allow the compiler to infer them, but a fully-expressed typed proof outline is enough to quickly verify correctness of the proof.
- throwawaymath 7y ago
  > but a fully-expressed typed proof outline is enough to quickly verify correctness of the proof. Yes, implementing that is the difficult part. I'm not saying it's infeasible - I'm saying it's very difficult. Writing provably correct software is also very difficult. This kind of theorem checking is becoming more common for theorems in e.g. combinatorics, but it's still very uncommon due to the added effort.
- danharaj 7y ago
  Encoding a proof to check it is the hard part.
- deleted 7y ago
  [deleted]
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 ago
  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.

andrewla 7y ago

> Automated theorem checking is typically very difficult for any nontrivial theorem I'm not sure this is true -- I thought the whole idea of these theorem systems was to make the kernel of the proof system as simple as possible (to allow a manual proof, or at least high confidence of correctness). If your program can produce an instance of a type, and it type-checks, then it true. Type inference can be tricky, and a lot of what makes the systems usable is the fact that you can omit types and allow the compiler to infer them, but a fully-expressed typed proof outline is enough to quickly verify correctness of the proof.

throwawaymath 7y ago
> but a fully-expressed typed proof outline is enough to quickly verify correctness of the proof. Yes, implementing that is the difficult part. I'm not saying it's infeasible - I'm saying it's very difficult. Writing provably correct software is also very difficult. This kind of theorem checking is becoming more common for theorems in e.g. combinatorics, but it's still very uncommon due to the added effort.
danharaj 7y ago
Encoding a proof to check it is the hard part.
deleted 7y ago
[deleted]

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 ago
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.