four color proof Has four color proof been proved without the help of computer?Where can I find the paper?
 A: No, but the proof has been formalized into computer-checkable form, using the proof-assistant Coq. As far as I know, the proof still relies on enumeration of cases and is therefore quite tedious.
For a paper, see Gonthier, Georges (2008), "Formal Proof--The Four-Color Theorem", Notices of the American Mathematical Society 55 (11): 1382–1393
A: Just as background, definitely not an answer to your question: You are probably aware of
the paper, 
"A new proof of the four colour theorem,"
by N. Robertson, D. P. Sanders, P. D. Seymour and R. Thomas, in Electron. Res. Announc. Amer. Math. Soc. 2 (1996), 17-25 (electronic).
It is still a computer proof, but simpler than Appel and Haken's: 
"Our unavoidable set has size 633 as opposed to the 1476 member set of Appel and Haken, and our discharging method uses only 32 discharging rules, instead of the 300+ of Appel and Haken."
A: from review http://www.ams.org/mathscinet-getitem?mr=1403921 of a survey paper by Paul Seymour, we find...

In 1993, Seymour, Neil Robertson, Daniel Sanders, and Robin Thomas, after trying to read the Appel-Haken proof, decided to supply their own proof, in which the data are available in electronic form, which can be checked by hand or computer. They confirmed that the four-color theorem is true and provable by the approach used by Appel and Haken. 

