Like me, Dave Altman (who works at the climbing gym I frequent) is a former mathematician. Between 5.12C lead climbs, we often chat about Math (in my case this is like Al Bundy talking about his high school football career).
I recently asked Dave about theorems that have the long proofs, and to what extent these proofs have been shortened from their original versions. He sent me the following mail:
When are two knots equivalent? In particular, when is a given knot the unknot? That's what Haken's theorem is about. While some progress has been made recently on it's implementation, the algorithm's complexity has limited its usefulness. The original paper is Haken, W. "Theorie der Normalflachen." Acta Math. 105, 245-375, 1961. The state of recent research can be found in the December 8, 2001 issue of Science News. The online version, unfortunately, requires a subscription. I'll send you a copy, if you want. A list of Haken's papers related to the Four-Color Theorem can be found at http://www.cs.columbia.edu/~sanders/graphtheory/people/Haken.W.html. A shorter claimed new proof can be found at http://www.math.gatech.edu/~thomas/FC/fourcolor.html. As noted on this page, though, there is a long history of famous mathematicians publishing false proofs that weren't debunked for many years. Feit, W. and Thompson, J. G. "Solvability of Groups of Odd Order." Pacific J. Math. 13, 775-1029, 1963: Every finite simple group (which is not cyclic) has even order, and the order of every finite simple noncommutative group is doubly even, i.e., divisible by 4. As far as I know, there is no proof shorter than their 254 page paper (algebraicists tend to terseness). A great resource to further delve into these and other topics is Eric Weisstein's World of Mathematics http://mathworld.wolfram.com/. Beware: It's really easy to get sucked into following links on this site and burning up way too much time. The classification of finite simple groups has a REALLY long proof, ~15,000 journal pages. The result, http://mathworld.wolfram.com/ClassificationTheoremofFiniteGroups.html, looks deceptively simple. This proof can be shortened considerably by just eliminating the redundancy in the various articles, but Gorenstein's classic book "Finite Simple Groups", which contained the state of knowledge a few years before the completion of the proof, and a lot of the eventual proof, is already about 300 pages long. While it might not take thousands of pages, but the proof is going to be long. Even Michael Aschbacher's little summary, "The Finite Simple Groups and Their Classification", consumes 61 pages.