This question complement a previous MO question: Examples of theorems with proofs that have dramatically improved over time.
I am looking for a list of
Major theorems in mathematics whose proofs are very hard but was not dramatically improved over the years.
(So a new dramatically simpler proof may represent a much hoped for breakthrough.) Cases where the original proof was very hard, dramatical improvments were found, but the proof remained very hard may also be included.
To limit the scope of the question:
a) Let us consider only theorems proved at least 25 years ago. (So if you have a good example from 1995 you may add a comment but for an answer wait please to 2020.)
b) Major results only.
c) Results with very hard proofs.
As usual, one example (or a few related ones) per post.
A similar question was asked before Still Difficult After All These Years. (That question referred to 100-years old or so theorems.)
Answers
(Updated Oct 3 '15)
1) Uniformization theorem for Riemann surfaces( Koebe and Poincare, 19th century)
2) Thue-Siegel-Roth theorem (Thue 1909; Siegel 1921; Roth 1955)
3) Feit-Thompson theorem (1963);
4) Kolmogorov-Arnold-Moser (or KAM) theorem (1954, Kolgomorov; 1962, Moser; 1963)
6) Weil conjectures (1974, Deligne)
7) The four color theorem (1976, Appel and Haken);
8) The decomposition theorem for intersection homology (1982, Beilinson-Bernstein-Deligne-Gabber); (Update: A new simpler proof by de Cataldo and Migliorini is now available)
9) Poincare conjecture for dimension four, 1982 Freedman (NEW)
10) The Smale conjecture 1983, Hatcher;
11) The classification of finite simple groups (1983, with some completions later)
12) The graph-minor theorem (1984, Robertson and Seymour)
13) Gross-Zagier formula (1986)
14) Restricted Burnside conjecture, Zelmanov, 1990. (NEW)
15) The Benedicks-Carleson theorem (1991)
16) Sphere packing problem in R 3 , a.k.a. the Kepler Conjecture(1999, Hales)
For the following answers some issues were raised in the comments.
The Selberg Trace Formula- general case (Reference to a 1983 proof by Hejhal)
Oppenheim conjecture (1986, Margulis)
Quillen equivalence (late 60s)
Carleson's theorem (1966) (Major simplification: 2000 proof by Lacey and Thiele.)
Szemerédi’s theorem (1974) (Major simplifications: ergodic theoretic proofs; modern proofs based on hypergraph regularity, and polymath1 proof for density Hales Jewett.)
Additional answer:
Answer about fully formalized proofs for 4CT and FT theorem.
Best Answer
The Four Colour Theorem might perhaps be a canonical example of a very hard proof of a major result which has improved, but is still very hard- no human-comprehensible proof exists, as far as I know, and all known proofs require computer computations.