0

If we search for the proof of a theorem then, assuming that there exists a proof, it lies in the set of all proofs of all provable theorems. But since this set is infinite, this means that the shortest length of the proof can be arbitrarily large. Almost all provable theorems will thus have a minimum proof length that exceed our ability to find them by some arbitrary large margin.

How can we then explain the fact that there are many proven theorems in mathematics? These theorems cannot be typical theorems, but what makes them atypical that makes their proofs to be short?

Count Iblis
  • 10,366
  • By "bounded", do you mean something different than "finite"? – r.e.s. May 15 '18 at 04:34
  • @r.e.s. No, so the point is that the set of proofs is not a finite set, and then you can consider ordering the proofs by proof length and argue that given some arbitrary integer, almost all proofs have lengths larger than that integer. – Count Iblis May 15 '18 at 04:41
  • 3
    "How can we explain the fact that there are many proven theorems in mathematics?" Because there were (and there are) many clever mathematicians: mathematicians do not "find" theorems scanning derivations of increasing proof lenght. – Mauro ALLEGRANZA May 15 '18 at 05:49
  • 1
    What is the minimum proof length? Let's say I have proof A and proof B, then A and B is one step? Or is it $\length A+\length B+1?$ I would argue that the former is the correct, this is one reason to use Lemmas and the like – ℋolo May 15 '18 at 06:03
  • @MauroALLEGRANZA That's certainly true, but if the minimum proof length of some theorem is astronomically large, then the most clever mathematician will never be able to deduce it. – Count Iblis May 15 '18 at 06:32
  • But if the most clever mathematician will never be able to deduce that purported "theorem", we will never discover it, so it will not be a theorem at all. – Mauro ALLEGRANZA May 15 '18 at 07:02
  • @MauroALLEGRANZA It can be a conjecture that still needs to be proved, like whether it is true that $e +\pi \notin \mathbb{Q}$. – Count Iblis May 15 '18 at 12:53
  • I know mathematicians won't agree with me but for me it seems natural that this is the case. The answer has to lie within the real world and the type of questions the human brain and neurosystem likes to ask and explore. There might be statements that have proofs that are equivalent to an incompressible string of bits but I believe the structure of the brain and the type of questions it like biases what language of mathematics it develops. Thats my own conjecture, that mathematics as we see it is a reflection of our minds, since it was generated by the brain. – Charlie Parker May 15 '18 at 22:37
  • Even if real numbers have countless isomorphisms and if mathematical truths are independent of the real world my claim is not about the validity of mathematics as eternal truth but instead that the space of mathematical language that we develop is not arbitrary and has to have some structure reflected by the brain. Perhaps alien brains would think differently and if they don't it could be great evidence to falsify my hypothesis. Hope that day comes when we can verify or falsify this scientifically! – Charlie Parker May 15 '18 at 22:39
  • 1
    This question reminds me of the old Yogi Berra quote about a popular restaurant: "Nobody goes there anymore—it's too crowded." (Yogi didn't invent the line, but he certainly made the joke more popular.) The idea that because the vast majority of proofs are longer than some given threshold, it's a surprise that there are any theorems—that's a weird one. – Brian Tung May 15 '18 at 22:40
  • @ZachTeitler Statements that are conjectured to be true are going to be small enough for us to formulate, so we'll end up choosing them from a small finite subset of all possible statements. But their proofs can then have any size. – Count Iblis May 16 '18 at 04:44
  • @CharlieParker Can you formulate your hypothesis somewhat shorter and clearer ? – Peter Sep 13 '18 at 07:47
  • Almost never is a proof made by a human a formal proof. A human usually uses well known properties to show more complex or more general properties. If we would translate a random proof into, lets say , ZFC, it would almost surely get astronomically long. In no way, it is surprising that so many theorems exist. – Peter Sep 13 '18 at 07:54

1 Answers1

3

There are three problems with this question. First is the jump from the second sentence to the third. While it is true that the length of a proof can be large, that does not show that there are theorems that have a very long shortest possible proof. I believe it, but there is no proof here and I do not find it obvious. We could just fiddle around as long as we want, then prove the theorem. The second is that we can make complicated theorems by compounding simpler unrelated ones. If we have one theorem that takes $m$ steps to prove and another unrelated one that takes $n$ steps to prove, their conjunction takes $m+n+1$ steps to prove, but we haven't really learned anything new when we do that. The third, and I think the largest, is that the existence of hard theorems does not say anything about whether there are easy interesting theorems. Whether they are typical is not important. You can prove the Pythagorean theorem in a few dozens of lines, but it is important and interesting. The fact that there are theorems in Euclidean geometry that we have not found yet does not change that. Neither does the fact that it is not typical of the length of the "average theorem" (however you define that).

Ross Millikan
  • 374,822
  • There. Youre welcome. – CogitoErgoCogitoSum May 15 '18 at 04:21
  • 2
    @CogitoErgoCogitoSum: I don't understand the comment. When I first saw it I saw I had a downvote, thought it was yours and you didn't like the answer. If so, I would appreciate some explanation. Then I saw you had one, too, and I suspect the two came from the same source. I think the question is not so clear and we took different approaches to give a sensible answer. – Ross Millikan May 15 '18 at 04:26