4 ms·

Houshalter is pointing out that your definition of "just complicated" is not sufficient (in the usual way we mathematicians do, with counterexamples). He's show

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

by j2kun 10y ago

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.