5 ms·

Just wondering, why do people not use Coq/Isabelle/Agda/etc in order to check such proofs? Wouldn't that save them from the "shame" of producing yet-another-inc

Just wondering, why do people not use Coq/Isabelle/Agda/etc in order to check such proofs? Wouldn't that save them from the "shame" of producing yet-another-incorrect P(!)=NP proof?

throwawaymath 7y ago
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.
Strilanc 7y ago
Because that's an extremely large amount of work to do, even if you're already familiar with the tools. It wouldn't be quite so bad if there were a huge repository of already proven theorems you could pull from. But in reality you'll probably find yourself defining what a Turing machine is, what asymptotic complexity is, deriving results like the master theorem, and a thousand other trivialities you would just skip over in a paper. It is especially problematic that there isn't a common repository of reference implementations of well-known unproved propositions. It would be so easy to make a subtle mistake in your definitions that allowed an existence proof to go through in a way that wouldn't generalize to the actual definition. For example, when you define probabilistic computation, if you declare that a probabilistic gate is a stochastic matrix with real number entries, you will incorrectly find that there exists probabilistic programs that solve the halting problem.
- throwawaymath 7y ago
  > For example, when you define probabilistic computation, if you declare that a probabilistic gate is a stochastic matrix with real number entries, you will incorrectly find that there exists probabilistic programs that solve the halting problem. Great example! Do you have an outline of this proof? I can see the error in defining a unitary matrix over R instead of C, but I'm not immediately seeing how you can exploit that error to bypass the halting problem. I'm guessing the concrete error would be introduced by overlooking that the real-valued matrix won't preserve the correct probability amplitude? If so, what's the next step to (falsely) deciding that a given algorithm will complete?
  - zielmicha 7y ago
    Maybe the problem is that you can use uncomputable numbers in the matrix? (e.g. https://en.wikipedia.org/wiki/Chaitin%27s_constant https://en.wikipedia.org/wiki/Chaitin%27s_constant)
    - throwawaymath 7y ago
      Unless I’m misunderstanding the parent commenter’s definition of a probabilistic gate - I’m assuming a unitary matrix - then that shouldn’t be an issue. Chaitin’s constant is in both R and C. More generally, all uncomputable real numbers are also in C, because C is complete over R. In other words that shouldn't be the issue, because the correct "setting" for the stochastic matrix still allows for that possibility. It's not something you introduce by using real entries.
kd0amg 7y ago
Most of the ones I've encountered have not put in the time to learn computation theory (not even a careful reading of Sipser), so I doubt they're up for learning to use that sort of tooling. Most also always think they're almost there and just need to refine a couple of minor details, which would make the time spent bringing those guns to bear seem hard to justify.

Just wondering, why do people not use Coq/Isabelle/Agda/etc in order to check such proofs? Wouldn't that save them from the "shame" of producing yet-another-incorrect P(!)=NP proof?

throwawaymath 7y ago

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.

Strilanc 7y ago

Because that's an extremely large amount of work to do, even if you're already familiar with the tools. It wouldn't be quite so bad if there were a huge repository of already proven theorems you could pull from. But in reality you'll probably find yourself defining what a Turing machine is, what asymptotic complexity is, deriving results like the master theorem, and a thousand other trivialities you would just skip over in a paper. It is especially problematic that there isn't a common repository of reference implementations of well-known unproved propositions. It would be so easy to make a subtle mistake in your definitions that allowed an existence proof to go through in a way that wouldn't generalize to the actual definition. For example, when you define probabilistic computation, if you declare that a probabilistic gate is a stochastic matrix with real number entries, you will incorrectly find that there exists probabilistic programs that solve the halting problem.

throwawaymath 7y ago
> For example, when you define probabilistic computation, if you declare that a probabilistic gate is a stochastic matrix with real number entries, you will incorrectly find that there exists probabilistic programs that solve the halting problem. Great example! Do you have an outline of this proof? I can see the error in defining a unitary matrix over R instead of C, but I'm not immediately seeing how you can exploit that error to bypass the halting problem. I'm guessing the concrete error would be introduced by overlooking that the real-valued matrix won't preserve the correct probability amplitude? If so, what's the next step to (falsely) deciding that a given algorithm will complete?
- zielmicha 7y ago
  Maybe the problem is that you can use uncomputable numbers in the matrix? (e.g. https://en.wikipedia.org/wiki/Chaitin%27s_constant https://en.wikipedia.org/wiki/Chaitin%27s_constant)
  - throwawaymath 7y ago
    Unless I’m misunderstanding the parent commenter’s definition of a probabilistic gate - I’m assuming a unitary matrix - then that shouldn’t be an issue. Chaitin’s constant is in both R and C. More generally, all uncomputable real numbers are also in C, because C is complete over R. In other words that shouldn't be the issue, because the correct "setting" for the stochastic matrix still allows for that possibility. It's not something you introduce by using real entries.

kd0amg 7y ago

Most of the ones I've encountered have not put in the time to learn computation theory (not even a careful reading of Sipser), so I doubt they're up for learning to use that sort of tooling. Most also always think they're almost there and just need to refine a couple of minor details, which would make the time spent bringing those guns to bear seem hard to justify.