4 ms·

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 reposi

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.
    - krcz 7y ago
      I don't think the issue here is requiring the matrix coefficients to be real (I don't think that complex values make sense there at all), but allowing arbitrary real numbers. In such case you can show algorithm, for which there exist matrix with real coefficients such that it solves halting problem - the trick is encoding infinite amount of information in the real constant.
      - throwawaymath 7y ago
        Complex values (a unitary matrix) make sense if the stochastic matrix is representing a probability amplitude.
- Strilanc 7y ago
  > Do you have an outline of this proof? Let p be the real number where, iff the k'th program halts, the k'th bit of p (after the decimal point, in binary) is 1. Let M be the operation "toggle a bit with probability p", which has matrix [[1-p, p], [p, 1-p]]. When given a program k to solve, keep applying M while counting up how many toggles you see. Do this until the chance that the k'th bit of the sample mean equals the k'th bit of p is greater than 2/3 or whatever other threshold you want, which will take a finite number of samples. Return the k'th bit of the sample mean. This is a probabilistic algorithm which solves the halting problem with arbitrarily high probability.
throwaway287391 7y ago
> It wouldn't be quite so bad if there were a huge repository of already proven theorems you could pull from. What about things like Metamath [1]? (Not sure if there is a more mature similar effort, Metamath is just the one I've heard of.) It seems like it has quite a lot of the "thousand other trivialiaties" you mentioned, but maybe it's still not enough to make a real dent? [1] http://us.metamath.org/index.html http://us.metamath.org/index.html
- FakeComments 7y ago
  There’s other efforts, like the UniMath project by the HoTT people. https://github.com/UniMath/UniMath https://github.com/UniMath/UniMath
joe_the_user 7y ago
The thing is, I'm not sure if it's quite a matter that most theorems haven't been proven automatically and rather a matter that using an automatically proven theorem in another theory to be automatically proven just isn't as easy as using an existing theorem in an ordinary proof. IE, one definition of a Turing machine might exist but it might not that usable for a given proof's purposes. I see a bunch of proof referenced here and I recall more elsewhere; https://madiot.fr/coq100/ https://madiot.fr/coq100/

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.
  - krcz 7y ago
    I don't think the issue here is requiring the matrix coefficients to be real (I don't think that complex values make sense there at all), but allowing arbitrary real numbers. In such case you can show algorithm, for which there exist matrix with real coefficients such that it solves halting problem - the trick is encoding infinite amount of information in the real constant.
    - throwawaymath 7y ago
      Complex values (a unitary matrix) make sense if the stochastic matrix is representing a probability amplitude.
Strilanc 7y ago
> Do you have an outline of this proof? Let p be the real number where, iff the k'th program halts, the k'th bit of p (after the decimal point, in binary) is 1. Let M be the operation "toggle a bit with probability p", which has matrix [[1-p, p], [p, 1-p]]. When given a program k to solve, keep applying M while counting up how many toggles you see. Do this until the chance that the k'th bit of the sample mean equals the k'th bit of p is greater than 2/3 or whatever other threshold you want, which will take a finite number of samples. Return the k'th bit of the sample mean. This is a probabilistic algorithm which solves the halting problem with arbitrarily high probability.

throwaway287391 7y ago

> It wouldn't be quite so bad if there were a huge repository of already proven theorems you could pull from. What about things like Metamath [1]? (Not sure if there is a more mature similar effort, Metamath is just the one I've heard of.) It seems like it has quite a lot of the "thousand other trivialiaties" you mentioned, but maybe it's still not enough to make a real dent? [1] http://us.metamath.org/index.html http://us.metamath.org/index.html

FakeComments 7y ago
There’s other efforts, like the UniMath project by the HoTT people. https://github.com/UniMath/UniMath https://github.com/UniMath/UniMath

joe_the_user 7y ago

The thing is, I'm not sure if it's quite a matter that most theorems haven't been proven automatically and rather a matter that using an automatically proven theorem in another theory to be automatically proven just isn't as easy as using an existing theorem in an ordinary proof. IE, one definition of a Turing machine might exist but it might not that usable for a given proof's purposes. I see a bunch of proof referenced here and I recall more elsewhere; https://madiot.fr/coq100/ https://madiot.fr/coq100/