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.
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>. If you’d rather read an entertaining paper, try <http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-....
This is a simple mechanization of the proof steps, on par with using a calculator for arithmetic.
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
soundness : forall n, (f n = false)
-> forall x y z,
(x < n) -> (y < n) -> (z < n)
-> (x^5 + y^5 ≠ z^5)
soundness 100000000 eq_refl
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.
(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's exactly my point. I wasn't being serious.
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.
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.
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.
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.
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.
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.
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.
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.