Scott Aaronson just posted the transcript from a very interesting talk he gave at Google a few weeks ago on his blog. He discusses various issues related to computational complexity, especially quantum computation and the ramifications of P=NP and why it would be a great surprise were it to be true. I find his claim about P=NP allowing the other six millenium problems to be solved by just doing a polynomial-time search through the possible proofs up to a certain length to be slightly suspicious (but only slightly, fortunately). Is there some way we could place a bound on the maximal possible length of the shortest proof of a given conjecture, should it be true? That seems to be very tricky, since some problems that can be stated fairly easily have very long proofs (for example, the four-color theorem). But I wonder if expressing the four-color theorem (just the statement, not the proof) in terms of ZFC formalism would actually require a large number of symbols. Still, a bound on the length of the shortest proof of a theorem requiring n characters to state seems very difficult to compute. It sounds faintly busy beaver-like.


About Simon

Hi. I'm Simon Rubinstein-Salzedo. I'm a mathematics postdoc at Dartmouth College. I'm also a musician; I play piano and cello, and I also sometimes compose music and study musicology. I also like to play chess and write calligraphy. This blog is a catalogue of some of my thoughts. I write them down so that I understand them better. But sometimes other people find them interesting as well, so I happily share them with my small corner of the world.
This entry was posted in Uncategorized. Bookmark the permalink.

2 Responses to

  1. Still, a bound on the length of the shortest proof of a theorem requiring n characters to state seems very difficult to compute.
    It ought to be uncomputable, right? Such a function would yield a finite algorithm for checking whether statements are provable or not, which seems like something that should not be allowed to exist (although I don’t know exactly what the official name of the theorem is that says this).
    Indeed, I think you can Godelize: if you had a computable expression for such an f, you can construct a statement G that says that “G has no proof of length < f(N)." where N can be taken large enough so that it is larger than the length of the statement. As in Godel's argument, if G is provable, G has (by assumption) a proof of length < f(N), which implies that ~G is also provable, so mathematics (or at least your formal system) is inconsistent. On the other, if G is unprovable, then in particular, G has no proof of length < f(N) — since this fact can be checked by a finite search, it can be proved, hence G is provable, which is a contradiction.

    • So, fortunately, Godel’s theorem is still true — regardless of P = NP, finite computations are still finite, and infinite computations are still infinite.
      On the other hand, if P=NP were true, it doesn’t seem too outlandish to imagine that humanity could build a supercomputer capable of searching for all proofs of RH short enough for a human to reasonably be able to understand in a lifetime — which I think is what Scott Aaronson had in mind (although there would clearly be some technical difficulties — one of them would be determining the “compression factor” of human-expressed mathematics relative to computer-checkable proofs — i.e. if you have a page of mathematics that a human mathematician can understand in an hour, can you put an upper bound on how long a formal machine-checkable proof of the results of that page would have to be? — this is like your question about the statement of the four-color theorem, although I doubt that ZFC is the ideal way to encode mathematics in a machine-checkable form. One might have a human-understandable proof of RH which depended upon some sort of human intuition but such that a formal computer-understandable proof would be forbiddingly long.)
      But if a computer search for all human-understandable proofs of RH turned up nothing, and RH were still true (and provable! albeit with a proof too vast for humans to comprehend), /then/ it would be pretty deep 🙂
      I could say more on metamathematics and what it means to be “deep”, but I think I’ll hold off, because dinner’s ready 🙂

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s