Timeline for Can one measure the infeasibility of four color proofs?
Current License: CC BY-SA 3.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 17, 2013 at 10:22 | vote | accept | Colin McLarty | ||
| Sep 16, 2013 at 15:53 | comment | added | Tony Huynh | @NoahSnyder I was dangerously venturing into the realm of mathematical philosophy and claiming that extremely long ''proofs'' are not proofs. For example, a proof that takes a human longer than a lifetime to verify is not a proof. I think this is consistent with what RSST assert. Indeed, here is the continuation of the quote regarding the 13000 line proof of Theorem 3. Moreover, although any line of the proofs can be checked by hand, the proofs themselves are not ''really'' checkable by hand because of their length. | |
| Sep 16, 2013 at 15:12 | comment | added | Noah Snyder | In some sense, the proof is already "written down" (or at any rate, it wouldn't be hard to modify the existing code to produce a human readable proof). What the human would need to do is actually read it. In particular, when the proof says "The following configuration is D-reducible, as can easily be seen by checking all cases of colorings of the boundary. Since this is routine we leave it as an exercise to the reader." the human reader has to actually do the routine check of all the cases. So I don't understand Tony's last comment. The proof already convinces anyone willing to read it. | |
| Sep 16, 2013 at 14:08 | comment | added | Colin McLarty | TonyHuynh explains his basis for estimating, so it cannot be called misguided. It is necessarily very rough. Brendan McKay's alternative is also well grounded. To me, estimates of the time to within a factor of less than 10 are pretty helpful. | |
| Sep 16, 2013 at 11:01 | comment | added | jwg | None of the estimations made in the answer are as flagrantly misguided as assuming that all uses of 'few' refer to a single constant. | |
| Sep 16, 2013 at 9:51 | comment | added | Brendan McKay | @FFF : Roughly the same task has to be performed a very large number of times on different data. A human would surely notice patterns and design lemmas to facilitate common subtasks. | |
| Sep 16, 2013 at 8:56 | comment | added | Tony Huynh | @BrendanMcKay Finally, for some psychological reason, I feel that 15 years is of the same order of magnitude as 2.5 years. So I think your answer is the same as mine in some big-O (human notion of running time). | |
| Sep 16, 2013 at 8:53 | comment | added | Tony Huynh | @BrendanMcKay Good point. There are other issues like whether we get to eat or sleep during the verification process; diminishing returns; etc. So I am not necessarily claiming that they claim a proof can be written down by a human in say 30 months. Furthermore, even if it could be written down, the human who wrote it may be convinced that it is correct, but it still wouldn't really be a proof (since it would be too long to reasonably verify). A proof is not written just to convince oneself of the veracity of a result, but to convince others. But I digress. | |
| Sep 16, 2013 at 7:50 | comment | added | user39297 | @BrendanMcKay Why it is obvious that there are shortcuts to be found? (I'm not familiar with the subject) | |
| Sep 16, 2013 at 2:06 | comment | added | Brendan McKay | I'm dubious. Here is another take (based solely on your quotations). Since they count "20 minutes" as "a few minutes" for Thm 3 by computer, maybe they count 20 months as "a few months" by human. That gives 15 years for Thm 2 by human, which is closer to what I'd expect a human to need to reproduce the result of about $10^{12}$ machine instructions. (Of course a clever human would discover shortcuts.) | |
| Sep 16, 2013 at 1:31 | comment | added | Colin McLarty | Wow. Very nice detail, with beautifully stated caution, nice answer. | |
| Sep 16, 2013 at 0:34 | history | answered | Tony Huynh | CC BY-SA 3.0 |