There is a classical approach by Birkhoff and Lewis, which remained dormant for decades. It was recently revived by Cautis and Jackson (start here [“The matrix of chromatic joins and the Temperley-Lieb algebra”, J. Combin. Theory 89 (2003), 109–155] and proceed here [“On Tutte's chromatic invariant”, Trans. Amer. Math. Soc. 362 (2010), 491–507]), using the Temperley-Lieb algebra.
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.
Best Answer
This is too long for a comment, so I am placing it here.
In this article of the Notices of the AMS, Gonthier describes a full formal proof of the four-color theorem, which makes explicit every logical step of the proof.
Although this formal proof has been checked by the Coq proof system, it would seem to be a category error to view this proof as a computer-based proof of the same kind as Appel and Haken's. The situation with Gonthier's proof is that we essentially have a full written text constituting a verified formal proof of the four-color theorem in first order logic.
And that is a state of certainty that most theorems in mathematics, including many of the classical results, have not yet attained.