24
$\begingroup$

Terms like "impractical" and "unfeasible" are used to say the Robertson, Sanders, Seymour, and Thomas proof of the four color theorem needs computer assistance. Obviously no precise measure is possible, for many reasons.

But is there an informed rough estimate what a graph theorist would need to verify the 633 reducible configurations in that proof? $10^4$ hours? $10^8$ years?

I am not asking if other proofs are known. I want to know if graph theorists have an idea what scale of practicality we are talking about when we say the Robertson, Sanders, Seymour, and Thomas proof is impractical without machine assistance.

Improve this question
$\endgroup$
5
  • 3
    $\begingroup$ I think a more realistic question would be how many graph theorists would be needed to verify the proof, given that human beings, after spending a certain amount of time (which depends on the individual) on a boring task start to suffer from demotivation, increasing error rate, or going mad. If a graph theorist can do one configuration without hitting this limit, that would be positive. Then compare with the number of graph theorists one is willing to spend on the problem. $\endgroup$
    – Marc van Leeuwen
    Commented Sep 16, 2013 at 8:16
  • 5
    $\begingroup$ If you allow probabilistically checkable proofs as acceptable, it may be possible to first use a computer to convert the computational component of the 4CT into a PCP format, and then any human armed with a couple of dice could verify the proof with, say, 99% confidence in a very short amount of time (maybe even minutes). I'm not sure what the state of the art is though on actually implementing a PCP. $\endgroup$
    – Terry Tao
    Commented Sep 16, 2013 at 22:50
  • $\begingroup$ I am pretty sure the formalization of the four-color theorem by Gonthier et al. can produce the exact number of examples, or whatever statistics you are interested in. There is no need to do any guesswork. Is that what you're interested in? $\endgroup$
    – Andrej Bauer
    Commented Oct 30, 2020 at 16:24
  • $\begingroup$ @AndrejBauer I would be surprised if it can say how long a human would take to find, or complete, the requisite cases. $\endgroup$
    – Colin McLarty
    Commented Nov 17, 2020 at 1:45
  • $\begingroup$ I thought you were asking about the number of cases, sorry. Is there any particular reason why you're interested in humans? $\endgroup$
    – Andrej Bauer
    Commented Nov 17, 2020 at 7:11

2 Answers 2

Reset to default
36
$\begingroup$

To answer the question it is important to disentangle the proof as follows.

Theorem 1. Every minimum counterexample to the 4CT is an internally 6-connected triangulation.

Theorem 2. If $T$ is a minimum counterexample to the 4CT, then no good configuration appears in $T$.

Theorem 3. For every internally 6-connected triangulation $T$, some good configuration appears in $T$.

See the actual paper for the definitions of these terms. Theorem 1 does not require computer assistance, while Theorem 2 and Theorem 3 both do require computer assistance. According to this version of the paper, Theorem 3 can in principle be checked by hand. Indeed it is explicitly mentioned that

It can be checked by hand in a few months, or a few minutes by computer (this was about 15 years ago though).

I quote more on Theorem 3:

For each of these five cases we have a proof. Unfortunately, they are very long (altogether about 13000 lines, and a large proportion of the lines take some thought to verify), and so cannot be included in a journal article.

Theorem 2, on the other hand really requires a computer. From the same paper,

The proof of Theorem 2 takes about 3 hours on a Sun Sparc 20 workstation and the proof of Theorem 3 takes about 20 minutes.

Thus, given that it took a computer 9 times longer to verify Theorem 2 than Theorem 3, and Theorem 3 apparently can be verified by hand in a few months (let us define few=3), then under some very dubious assumptions we have the ballpark answer of

Ballpark Answer. 30 months.

Improve this answer
$\endgroup$
10
  • 9
    $\begingroup$ 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.) $\endgroup$
    – Brendan McKay
    Commented Sep 16, 2013 at 2:06
  • 4
    $\begingroup$ @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. $\endgroup$
    – Brendan McKay
    Commented Sep 16, 2013 at 9:51
  • 5
    $\begingroup$ None of the estimations made in the answer are as flagrantly misguided as assuming that all uses of 'few' refer to a single constant. $\endgroup$
    – jwg
    Commented Sep 16, 2013 at 11:01
  • 6
    $\begingroup$ 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. $\endgroup$
    – Colin McLarty
    Commented Sep 16, 2013 at 14:08
  • 4
    $\begingroup$ 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. $\endgroup$
    – Noah Snyder
    Commented Sep 16, 2013 at 15:12
8
$\begingroup$

As explained in Tony's answer, in order to answer this question you need to separately answer how long it would take to prove reducibility of the configurations (Theorem 2) and how long it would take to prove unavoidability of the configurations (Theorem 3).

There's an interesting alternate proof of the 4-color theorem due to John Steinberger, which differs from RSST in that the proof of reducibility only uses the easier notion of "D-reducibility" rather than the more elaborate "C-reducibility." The cost is that the unavoidable set is much longer and the proof of unavoidability is also longer. As Tony explained, unavoidability was the "easy" part, so it's possible that for a human Steinberger's proof would be easier to verify. Even if it is not easier, he provides some additional detail of the estimate of "a few months" from RSST.

In discussing the proof of unavoidability, Steinberger discusses the files which serve as certificates of unavoidability. That is, there's a file which tells the computer how to prove this particular case. Of these files, in verbose human readable form, Steinberger writes:

While the resulting output may be readable at a normal pace it is also quite large: over 3’000’000 lines for the Robertson et al. proof, over 13’000’000 lines for our proof. A mathematician checking these proofs at the rate of one line per second and working 9 hours a day would take over 3 months to read the Robertson et al. proof and over a year to read ours.

This makes much more precise the "few months" estimate of RSST.

Unfortunately he does not give a human estimate for the reducibility portion. Instead he says it takes a 2010 personal computer "around 10 hours." If I understand things correctly, the problem here is that in order to check D-reducibility, you need to check something for every choice of 4-coloring on the boundary of your configuration. For large configurations this is an enormous number of cases. The computer time here large, which suggests that a human might prefer to do the RSST proof.

As discussed in the comments, a plausible estimate is that the Steinberger proof of reducibility would likely take somewhere between $10^4$ and $10^6$ hours (i.e. somewhere between a year and a lifetime).

Improve this answer
$\endgroup$
9
  • $\begingroup$ This helps answer both of my questions: Graph theorists do have ideas, within an order of magnitude or maybe two, of they mean in calling the problem infeasible without machines. It is much more like $10^4$ hours than $10^8$ years. $\endgroup$
    – Colin McLarty
    Commented Sep 16, 2013 at 15:21
  • 1
    $\begingroup$ Yeah, I'd be surprised if the answer isn't something in between $10^4$ hours and $10^6$ hours with current techniques. $\endgroup$
    – Noah Snyder
    Commented Sep 16, 2013 at 15:32
  • 1
    $\begingroup$ It surely takes at least second to glance at a 4-coloring and see that it is valid. $10^{11}$ seconds $\approx 3 \times 10^7$ hours. (One also has to check that the list of boundary colorings contains all possible boundary colors, but we can circumvent that by having the computer give them to us in lexicographic order; I can check that one coloring is the lex successor of another in under a second, and then just check $3 \times 10^3$ times that the first and last elements of the list are what they should be.) $\endgroup$
    – David E Speyer
    Commented Sep 16, 2013 at 16:20
  • 1
    $\begingroup$ I think it's actually $3^{14}$ and not $4^{14}$ because they translate the question into 3-coloring edges instead of 4-coloring vertices. That saves you a factor of 100. $\endgroup$
    – Noah Snyder
    Commented Sep 16, 2013 at 16:42
  • 1
    $\begingroup$ THANK YOU. That is a much bigger error in what I am doing than the one I noticed. (The $3$ coloring of edges is equivalent to saying they have pre-eliminated all boundary colorings where two adjacent vertices have the same color, but doing it in terms of edge colorings makes it easy to see that they have done the complete list without dedicating more thinking time to it.) Also, I should be dividing by $12$, not $6$ above. And now my estimate comes back into your $(10^4, 10^6)$ range. $\endgroup$
    – David E Speyer
    Commented Sep 16, 2013 at 16:46

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .