I feel like the four-color theorem automated proof is much more 'human-readable' than the proofs done with automated theorem provers. Because with the four-color theorem, there is a human readable proof that says "if this finite set of cases are all colorable, then all planar graphs are colorable". And then there is some rather concrete code that generates all the finite cases, and finds a coloring for them. Every step in there makes sense, and is fully understandable. The fact that the exhaustive checking wasn't done by hand doesn't mean its hard to understand how the proof works, or what is 'actually going on'.
For a general theorem prover, reading the code doesn't explain anything insightful about why the theorem is true. For the 4 color theorem, the code that proved it actually gives insight in how the proof works.
For a general theorem prover, reading the code doesn't explain anything insightful about why the theorem is true. For the 4 color theorem, the code that proved it actually gives insight in how the proof works.