5 ms·
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
by 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 agoI 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 agoI 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.
- tgb 10y agoI don't see how Houshalter's post can possibly be read as sarcastic, it looks like a technical comment that makes an interesting point that is slightly tangential. I simply don't know how to read that comment as if there were a /s at the end. And I don't see how the top level comment can be considered dismissive, it too is making an interesting point that we should use another metric.
- marcosdumay 10y ago> it looks like a technical comment that makes an interesting point that is slightly tangential That's why I love Math. But hey, I hope your post is sarcastic too. But don't mind, there's no procedure you could use to convince me it isn't.
- fmap 10y agoIf you demand that the program terminates (through higher order structural recursion, i. e. by induction) then this would be a proof in type theory. It's called proof by reflection. When Martin Löf (the father of type theory) saw this trick for the first time he apparently exclaimed "but this is not a proof!" so make of that what you will.