7 ms·

OK look, running a^2 + b^2 = c^2 a few trillion times and calling that a "long proof" is disingenuous - it's really long if you include every single operation,

OK look, running a^2 + b^2 = c^2 a few trillion times and calling that a "long proof" is disingenuous - it's really long if you include every single operation, but must you? I just described it here in a few sentences. I guess what's more interesting is a sort of kolmogorov complexity of the proof, perhaps.

doesnotexist 10y ago
Isn't that just a fancy way of asking "does there exist a more concise proof for this theorem?" That is to say wouldn't we rather assign a kolmogorov complexity to a theorem instead of a specific proof for that theorem. I'm not even sure what we would mean by assigning a complexity to a specific proof. The proof is the proof. Would it basically mean "is this specific proof compressible?" But then I think thats essentially the same as asking "is there a shorter proof?" As the new shorter proof is the compressed representation + the decompression program. But what we're really interested in, is what is the shortest representation that proves the theorem as thats what we're ultimately interested in, right? This specific proof is a large case-analysis, though much smaller than brute force of all possible cases. There may however be a simpler more beautiful and shorter proof. If so, then that demonstrates that the theorem has a lower kolmogorov complexity than the current best known proof suggests.
- tprice7 10y ago
  "As the new shorter proof is the compressed representation + the decompression program." A proof is a sequence of deductions, not a program that generates a sequence of deductions.
  - doesnotexist 10y ago
    You might be interested in reading about the Curry Howard Correspondence. From wikipedia: "In other words, the Curry–Howard correspondence is the observation that two families of formalisms that had seemed unrelated—namely, the proof systems on one hand, and the models of computation on the other—were, in the two examples considered by Curry and Howard, in fact structurally the same kind of objects." https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
    - tprice7 10y ago
      Yes, I've encountered one form of the Curry-Howard correspondence before. Are you claiming that, via the Curry-Howard correspondence or some related phenomenon, the corresponding proof of a program used to compress a proof is the same (or at least, proves the same theorem) as the original proof that the program was meant to compress? That is interesting and I would appreciate if you could expand on it.
      - mietek 10y ago
        If you’re using the right language, proofs are programs; it’s as simple as that. “Compressing” a proof, then, amounts to doing what good programmers are already doing — noticing patterns and eliminating redundancy. I’ll refer you to an authority on the subject, Phil Wadler. If you like watching videos, try <https://www.youtube.com/watch?v=IOiZatlZtGU> https://www.youtube.com/watch?v=IOiZatlZtGU>. If you’d rather read an entertaining paper, try <http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf> http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-....
        sedachv 10y ago
        The Curry-Howard correspondence does not apply here though. The coloring theorem is not encoded in the type of the program that enumerates and checks the possible colorings. The program itself is a restatement of the coloring theorem, with the result type being boolean (all the enumerated colorings satisfy the property, or not). So the proof would consist of proving that the program must terminate with a true value. Of course that is not actually useful as it does not simplify anything. This is a simple mechanization of the proof steps, on par with using a calculator for arithmetic.
        vilhelm_s 10y ago
        Depending on what programming language you use for your Curry-Howard correspondence, there is actually a related thing. Probably the most well known realization of C-H is dependent type theories like Coq and Agda. And those support a proof method called "proof by reflection". The idea is that in those languages, types can contain program terms as subexpressions, and two types are considered "the same" if they evaluate to the same expression. Because the languages enforce that all expressions terminate, it's still decidable whether a program is well-typed or not, so the language can still be considered a proof system, but the type checker can take almost arbitrarily long time to check a program because it has to evaluate subexpressions to values in order to check type equality. Anyway, the point is that this can be used to write down short programs that act as proofs. For example, suppose you want to prove there are no counterexamples to Fermat's last theorem for exponent 5 and numbers less than 100000000. In this case, you would write down a function f : nat -> bool which evaluates the expression for all numbers less than the argument and returns whether there is a counterexample, then you would prove a lemmma soundness : forall n, (f n = false) -> forall x y z, (x < n) -> (y < n) -> (z < n) -> (x^5 + y^5 ≠ z^5) and then the proof of the final theorem is just soundness 100000000 eq_refl In order to check the eq_refl part, the type checker would evaluate (f 100000000) and verify that it evaluated to false. But all that computation is not recorded in the proof term. So the program that represents the proof is very small, and constant size in the bound. This is actually very useful in practice, because storing and manipulating big proof terms is slow and memory-hungry, so it's useful to be able to push the computation under the carpet in this way. On the other hand, it is sometimes considered a little philosophically dubious.
Houshalter 10y ago
Yes, in fact every single mathematical proof can be reduced to a few lines of code! You just write a program that verifies a proof, and another program that brute forces through the space of all possible proofs. It should fit onto a page or two. So the kolmogorov complexity of any proof has a pretty small upper bound.
- rntz 10y ago
  That isn't a proof, it's a procedure for finding a proof. The procedure might fail, and whether it will fail or not cannot be checked without running it - which is not guaranteed to halt! Of course, to guarantee that it halts, you could include an upper bound on the size of the proofs it searches in your program. So then at least your "proof" is checkable. However, it is not in general efficiently checkable - that is, checkable in polynomial time. If it were, it could only produce polynomial compression! (Though admittedly, polynomial compression is pretty good, practically speaking.) As for Kolmogorov complexity, there are infinitely many distinct proofs, so their Kolmogorov complexity cannot possibly be bounded.
  - Houshalter 10y ago
    > That isn't a proof, it's a procedure for finding a proof. That's exactly my point. I wasn't being serious.
    - tgb 10y ago
      I think you're missing an important point though. The article's proof is guaranteed to be verifiable in a known finite amount of time. Your example does not so it's hard to take commentary from it onto the article's subject.
      - sparky_z 10y ago
        I think you're missing the important point that Houshalter was being sarcastically critical of makmanalp's dismissive top-level comment, not the proof in the article.
apalmer 10y ago
Ehhh what you are describing is an algorithm for evaluating the truth of a statement. Which is not the same thing as a proof at all.
- RGamma 10y ago
  In classical logic your statement entails that there is a proof that cannot be checked (marked "true") by an algorithm (note, that the proof itself cannot be checked, not a fact, for which there is no proof) or that there is an algorithm marking something "true" that doesn't constitute a proof (trivially the thing that is marked "true" is proven). I doubt you'll find counterexamples to either of them, as an infinite, yet valid, proof is hardly believable (nobody of us could ever finish reading it) and a terminating ("marking true") algorithm always computes something.
rntz 10y ago
Many folks would say that's not a proof, because it's not efficiently checkable. To tell whether it actually proves the thing, I have to go off and check every number, which takes an enormous amount of time compared to the length of the "proof". Of course, the solution of listing every single case seems about equally unhelpful. The whole thing leads one to question whether proofs are really the goal of mathematics, or just a useful proxy.
- jobigoud 10y ago
  I think it's checkable. You just have to write another program to check the proof, and maybe a meta program that checks that your proof-checking program is correct. I think there is a good chance that in the future we have computers coming up with and proving theorems that we don't fully understand (but for which we understand the practical value) and the human contribution will be to write a program that verifies that the proof is indeed correct.
Chinjut 10y ago
You've described a very short algorithm for finding a very long proof. But what the algorithm finds is indeed a very long proof, not a short one, and the reason I say that is because the short algorithm description you gave doesn't convince me of the truth of the statement "Every coloring of positive integers up through 7825 contains a monochrome Pythagorean triple"; you could give similarly short descriptions of algorithms searching for hypothetical proofs of any number of false claims. It's only the long-ass step-by-step completed execution of that algorithm which does the convincing.

doesnotexist 10y ago

Isn't that just a fancy way of asking "does there exist a more concise proof for this theorem?" That is to say wouldn't we rather assign a kolmogorov complexity to a theorem instead of a specific proof for that theorem. I'm not even sure what we would mean by assigning a complexity to a specific proof. The proof is the proof. Would it basically mean "is this specific proof compressible?" But then I think thats essentially the same as asking "is there a shorter proof?" As the new shorter proof is the compressed representation + the decompression program. But what we're really interested in, is what is the shortest representation that proves the theorem as thats what we're ultimately interested in, right? This specific proof is a large case-analysis, though much smaller than brute force of all possible cases. There may however be a simpler more beautiful and shorter proof. If so, then that demonstrates that the theorem has a lower kolmogorov complexity than the current best known proof suggests.

tprice7 10y ago
"As the new shorter proof is the compressed representation + the decompression program." A proof is a sequence of deductions, not a program that generates a sequence of deductions.
- doesnotexist 10y ago
  You might be interested in reading about the Curry Howard Correspondence. From wikipedia: "In other words, the Curry–Howard correspondence is the observation that two families of formalisms that had seemed unrelated—namely, the proof systems on one hand, and the models of computation on the other—were, in the two examples considered by Curry and Howard, in fact structurally the same kind of objects." https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
  - tprice7 10y ago
    Yes, I've encountered one form of the Curry-Howard correspondence before. Are you claiming that, via the Curry-Howard correspondence or some related phenomenon, the corresponding proof of a program used to compress a proof is the same (or at least, proves the same theorem) as the original proof that the program was meant to compress? That is interesting and I would appreciate if you could expand on it.
    - mietek 10y ago
      If you’re using the right language, proofs are programs; it’s as simple as that. “Compressing” a proof, then, amounts to doing what good programmers are already doing — noticing patterns and eliminating redundancy. I’ll refer you to an authority on the subject, Phil Wadler. If you like watching videos, try <https://www.youtube.com/watch?v=IOiZatlZtGU> https://www.youtube.com/watch?v=IOiZatlZtGU>. If you’d rather read an entertaining paper, try <http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf> http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-....
      - sedachv 10y ago
        The Curry-Howard correspondence does not apply here though. The coloring theorem is not encoded in the type of the program that enumerates and checks the possible colorings. The program itself is a restatement of the coloring theorem, with the result type being boolean (all the enumerated colorings satisfy the property, or not). So the proof would consist of proving that the program must terminate with a true value. Of course that is not actually useful as it does not simplify anything. This is a simple mechanization of the proof steps, on par with using a calculator for arithmetic.
        vilhelm_s 10y ago
        Depending on what programming language you use for your Curry-Howard correspondence, there is actually a related thing. Probably the most well known realization of C-H is dependent type theories like Coq and Agda. And those support a proof method called "proof by reflection". The idea is that in those languages, types can contain program terms as subexpressions, and two types are considered "the same" if they evaluate to the same expression. Because the languages enforce that all expressions terminate, it's still decidable whether a program is well-typed or not, so the language can still be considered a proof system, but the type checker can take almost arbitrarily long time to check a program because it has to evaluate subexpressions to values in order to check type equality. Anyway, the point is that this can be used to write down short programs that act as proofs. For example, suppose you want to prove there are no counterexamples to Fermat's last theorem for exponent 5 and numbers less than 100000000. In this case, you would write down a function f : nat -> bool which evaluates the expression for all numbers less than the argument and returns whether there is a counterexample, then you would prove a lemmma soundness : forall n, (f n = false) -> forall x y z, (x < n) -> (y < n) -> (z < n) -> (x^5 + y^5 ≠ z^5) and then the proof of the final theorem is just soundness 100000000 eq_refl In order to check the eq_refl part, the type checker would evaluate (f 100000000) and verify that it evaluated to false. But all that computation is not recorded in the proof term. So the program that represents the proof is very small, and constant size in the bound. This is actually very useful in practice, because storing and manipulating big proof terms is slow and memory-hungry, so it's useful to be able to push the computation under the carpet in this way. On the other hand, it is sometimes considered a little philosophically dubious.

Houshalter 10y ago

Yes, in fact every single mathematical proof can be reduced to a few lines of code! You just write a program that verifies a proof, and another program that brute forces through the space of all possible proofs. It should fit onto a page or two. So the kolmogorov complexity of any proof has a pretty small upper bound.

rntz 10y ago
That isn't a proof, it's a procedure for finding a proof. The procedure might fail, and whether it will fail or not cannot be checked without running it - which is not guaranteed to halt! Of course, to guarantee that it halts, you could include an upper bound on the size of the proofs it searches in your program. So then at least your "proof" is checkable. However, it is not in general efficiently checkable - that is, checkable in polynomial time. If it were, it could only produce polynomial compression! (Though admittedly, polynomial compression is pretty good, practically speaking.) As for Kolmogorov complexity, there are infinitely many distinct proofs, so their Kolmogorov complexity cannot possibly be bounded.
- Houshalter 10y ago
  > That isn't a proof, it's a procedure for finding a proof. That's exactly my point. I wasn't being serious.
  - tgb 10y ago
    I think you're missing an important point though. The article's proof is guaranteed to be verifiable in a known finite amount of time. Your example does not so it's hard to take commentary from it onto the article's subject.
    - sparky_z 10y ago
      I think you're missing the important point that Houshalter was being sarcastically critical of makmanalp's dismissive top-level comment, not the proof in the article.

apalmer 10y ago

Ehhh what you are describing is an algorithm for evaluating the truth of a statement. Which is not the same thing as a proof at all.

RGamma 10y ago
In classical logic your statement entails that there is a proof that cannot be checked (marked "true") by an algorithm (note, that the proof itself cannot be checked, not a fact, for which there is no proof) or that there is an algorithm marking something "true" that doesn't constitute a proof (trivially the thing that is marked "true" is proven). I doubt you'll find counterexamples to either of them, as an infinite, yet valid, proof is hardly believable (nobody of us could ever finish reading it) and a terminating ("marking true") algorithm always computes something.

rntz 10y ago

Many folks would say that's not a proof, because it's not efficiently checkable. To tell whether it actually proves the thing, I have to go off and check every number, which takes an enormous amount of time compared to the length of the "proof". Of course, the solution of listing every single case seems about equally unhelpful. The whole thing leads one to question whether proofs are really the goal of mathematics, or just a useful proxy.

jobigoud 10y ago
I think it's checkable. You just have to write another program to check the proof, and maybe a meta program that checks that your proof-checking program is correct. I think there is a good chance that in the future we have computers coming up with and proving theorems that we don't fully understand (but for which we understand the practical value) and the human contribution will be to write a program that verifies that the proof is indeed correct.

Chinjut 10y ago

You've described a very short algorithm for finding a very long proof. But what the algorithm finds is indeed a very long proof, not a short one, and the reason I say that is because the short algorithm description you gave doesn't convince me of the truth of the statement "Every coloring of positive integers up through 7825 contains a monochrome Pythagorean triple"; you could give similarly short descriptions of algorithms searching for hypothetical proofs of any number of false claims. It's only the long-ass step-by-step completed execution of that algorithm which does the convincing.