4 ms·

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

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.

j2kun 10y ago
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.
- tgb 10y ago
  Admittedly, once you know that statement P is true it's proof is even easier: P =>P.
- makmanalp 10y ago
  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.
Houshalter 10y ago
> 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.

j2kun 10y ago

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.

tgb 10y ago
Admittedly, once you know that statement P is true it's proof is even easier: P =>P.
makmanalp 10y ago
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.

Houshalter 10y ago

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