Hacker News Reader

Comment by Houshalter | Hacker News Reader

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.

View on HN

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.

> That isn't a proof, it's a procedure for finding a proof.

That's exactly my point. I wasn't being serious.

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.

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.

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

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

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

I think there are some proofs that are /just/ complicated. I'm certainly not an expert on this subject but for example a few years ago, Deolaikar's (ultimately erroneous) P/=NP proof paper was 66 pages. 66 full, information dense pages.

Also, can't there be a measure of complexity without the absurd extreme of "in my special language, there is a single function call that proves X"?

In your example, it's not the proofs that can be reduced to a few lines of code, it's the thing that generates the proofs. That little program wouldn't contain information about which proofs are "interesting" or "correct", since that's the reason it exists in the first place. Adding in that information would make it much larger.

Anyway, it just seems disingenuous to call that proof 200 terabytes. You don't need most of those 200 terabytes to understand the proof, and neither do you have to even store those 200 terabytes to know that none of the numbers you went through worked.

Houshalter is pointing out that your definition of "just complicated" is not sufficient (in the usual way we mathematicians do, with counterexamples). He's showing that once you know a theorem is true (even if it's P != NP), every proof has essentially constant Kolmogorov complexity. Kolmogorov complexity does not take into account computational complexity of the program outputting the target string. There is time-bounded Kolmogorov complexity, but I don't know if I'd call it a standard measure.

There is also a measure called "proof complexity" that compares the length of a proof to the length of the statement being proved. If the relationship is polynomial then the proof is considered "interesting." If it's exponential, uninteresting. You also need a parameter, which in this case there isn't since it's a specific n, but you can extrapolate the proof technique to asymptotic n and call it exponential from that perspective and I don't think anyone would argue with you.

Admittedly, once you know that statement P is true it's proof is even easier: P =>P.

Right, yes, I should have been clearer, Kolmogorov complexity was just an example of the kind of thing I'm going for. I understand that Kolmogorov complexity doesn't quite cover it, though I don't think this precludes the notion of a measure that /does/ cover the idea of the fundamental complexity of a proof. It sure feels like there's something different about a proof that repeats the same functional form over and over again for 200TB vs 200TB of more complex statements.

For example, perhaps there exists somewhere a language that includes the most basic atoms of mathematics, and when you express a proof in that language - like the Principia Mathematica, perhaps - then maybe it's guaranteed to be in irreducable canonical-form, and then you can go on the complexity of that.

But I do now see that the 200TB should be considered part of the proof because you haven't verified the proof until you've tried every single item, versus when you've gone through normal short proof you're certain of the result by the end of it.

> You don't need most of those 200 terabytes to understand the proof,

I believe that you do. I would argue no human "understands" a 200 terabyte proof. Maybe they understand the procedure that arrived at the proof, but my point is that isn't a proof itself, or understanding why it is true.

Maybe we could define the Kolmogorov complexity of a proof as the number of lines of code, PLUS the size of the proof that the proof-generating program halts.

Or the total number of lines of code in a sequence of programs, where the first program generates a proof of the original theorem, and every other program generates a proof that the preceding program halts, PLUS the size of a proof that the final program halts.

Reply on news.ycombinator.com