Skip to main content
1 of 3
Noah Snyder
  • 28.1k
  • 4
  • 94
  • 170

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.

Noah Snyder
  • 28.1k
  • 4
  • 94
  • 170