# Examples of major theorems with very hard proofs that have NOT dramatically improved over time

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.)

(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)

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.)

• I basically asked the same thing before: mathoverflow.net/questions/44593/… – arsmath Dec 20 '13 at 7:20
• Dear Arsmath, to a large extent the answers there were influenced by your specific question "I would like to believe that by 2110 the Langland's program would be reduced to a 10-page pamphlet (with complete proofs) that I could read over breakfast. Is this belief plausible?" – Gil Kalai Dec 20 '13 at 7:39
• Does the classification of finite simple groups qualify? See also my answer below. – Victor Protsak Dec 20 '13 at 8:39
• @GilKalai: It's still a duplicate. Every answer there would apply here. The only restriction is that I strongly suggested 100-year old results. You should feel free to edit the original. – arsmath Dec 20 '13 at 9:21
• Be it as it may be, let's hope that my question will lead to a good list of answers. Generally speaking, in my opinion, duplicates (certainly with a gap of 3 years) that may lead to better answers (or just good new answers) are welcome. – Gil Kalai Dec 20 '13 at 9:38

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.

• I am curious. How many work hours would it take for an average mathematician to manually recheck the computer part of the proof? Are those checks easy enough that we can trust rechecking done by undergraduates? :) (To be honest, I've never understand why people have problems with this proof. I'd better stop right here, since I don't want to start any flame war.) – Vít Tuček Dec 21 '13 at 17:29
• @VítTuček: I find it curious that you would trust a proof by undergraduates but would not trust a proof by a computer. Surely it should be the other way around!! – Matt Dec 21 '13 at 18:52
• A recent program of Kronheimer and Mrowka may lead to a new, more comprehensible proof of the four-color through instanton homology: arxiv.org/abs/1508.07205 – Sam Hopkins Sep 11 '15 at 17:18
• I actually disagree with this answer. The original computer proof of Appel-Haken has been considerably simplified. First by Robertson-Sanders-Seymour-Thomas, and further simplified by Steinberger. Yes they're still computer proofs, but they're way easier to understand than the original. – Noah Snyder Sep 12 '15 at 0:44
• The real problem with the Appel-Haken proof isn't that they used computers, but that they watched what the computer was doing and manually chose to halt branches they believed weren't going to be fruitful (because otherwise with computers at the time it would have taken too long) so that one couldn't just re-run their program to verify output. And the referees (being non-programmers; this is many years ago) weren't confident the verification code worked (this is a bad excuse). Conclusion: modern proofs are simpler because you can just let the code run..! – user36212 Oct 3 '15 at 22:58

Feit-Thompson theorem 

Edit (GK): This would also be my first answer, let me add a few details. The Feit-Thompson theorem asserts that every finite group of odd order is solvable. An equivalent formulation is that every simple nonabelian group is of even order. The theorem was proved by Feit and Thompson in 1962,1962. It was conjectured by Burnside by 1911. The theorem plays a crucial role in the classification of finite simple groups. Some parts of the proof were simplified over the years but it remained very hard.

• Apparently, my answer was too short, even after including the link! – Victor Protsak Dec 20 '13 at 8:38
• There are a bunch of other theorems that form part of CFSG that would also qualify: Thompson's classification of N-groups, Gorenstein-Walter's classification of groups with dihedral 2-groups, a whole bunch of Aschbacher's theorems (perhaps Aschbacher-Smith on the quasithin case would be the most obvious, but it doesn't satisfy the 25 year requirement), etc etc. – Nick Gill Dec 20 '13 at 10:43
• Or what about the CFSG itself? That's not getting any simpler (see my question mathoverflow.net/questions/114943/…). And let's ignore the fact the quasithin case was plugged after the cutoff. – David Roberts Dec 23 '13 at 12:17
• From a 1985 interview with Serre: "A more serious problem is the one on the "big theorems" which are both very useful and too long to check (unless you spend on them a sizable part of your lifetime ...). A typical example is the Feit-Thompson Theorem: groups of odd order are solvable. (Chevalley once tried to take this as the topic of a seminar, with the idea of giving a complete account of the proof. After two years, he had to give up.)" – Marius Kempe Dec 24 '13 at 0:14
• The proof remains long, but it no longer takes a sizable part of a lifetime to check; see research.microsoft.com/en-us/news/features/… – John Stillwell Dec 29 '13 at 23:27

A major 19th century result is the general Uniformization theorem: Every simply connected Riemann surface is conformally equivalent either to the plane or to the unit disc or to the sphere. There were improvements of the proof, and many different proofs, but simplifications are not "dramatic". It is still difficult to include a complete proof in a graduate course, unless the large part of the course is dedicated to this single theorem.

• A few years before I retired, teaching a fairly advanced graduate course in complex analysis, I foolishly promised the students that I would get Uniformization proved by the end of the semester. Hah! – Lubin Dec 20 '13 at 18:33
• I believe this is a (very early) 20-th century result, proved by Koebe and Poincaré, rather than a 19-th century result? – Lasse Rempe-Gillen Sep 24 '15 at 15:58
• This result has somewhat long history. It was first stated by Klein who published it, and since then the long story of the proof began:-) See the paper of Abikoff MR0628026 or the book of Saint-Gervais. – Alexandre Eremenko Sep 24 '15 at 17:50

A graph $H$ is a minor of a graph $G$ if it can be obtained from $G$ by a sequence of deletion and contraction edges. Roberton and Seymour's graph-minor theorem asserts that in every infinite sequence of graphs $G_1,G_2,\dots$ there is $i<j$ such that $G_i$ is a minor of $G_j$. Equivalently it asserts that every minor-closed family of graphs (examples: planar graphs) can be defined by a finite list of forbidden minors (for the example a theorem of Wegner asserts that the list is $\{K_5,K_{3,3}\}$).

The theorem was proved by Robertson and Seymour around 1984. The proof spans 20 papers (published between 1984 and 2004) and is very hard, in spite of some simplifications of some of its ingredients.

• The 2002 Perfect Graph theorem of Chudnovsky, Robertson, Seymour, and Thomas is another very hard major theorem and thus a good contender for a future answer, unless simplified dramatically before 2027. – Gil Kalai Dec 21 '13 at 15:45

This was proven by Hatcher in 1983. It states that the diffeomorphism group $\mathrm{Diff}(S^3)$ of the $3$-sphere has the homotopy type of the orthogonal group $O(4)$, which in particular implies that $\pi_0\,\mathrm{Diff}(S^3)= \pi_0 (O(4))$, or equivalently that $\Gamma_4=\pi_0\,\mathrm{Diff}(D^3\mathrm{rel}\,\partial)=0$ (this latter result, due originally to Cerf, was simplified here). The case of the $2$-sphere is even more famous and much easier, but the Smale Conjecture is a major foundational result, which implies for example that the space of smooth unknotted curves retracts to the space of great circles, i.e. there exists a way to isotope smooth unknotted curves to round circles that is continuous as a function of the curve'' (quoted from here).

Hatcher's proof is considered to be very hard, and I have heard experts say that there might be only a handful of people in the world who truly understand it. I am not aware of the proof having been substantially simplified.

• I'm confused... what is contractible? – André Henriques Dec 20 '13 at 10:01
• Dear Daniel, Is the "Dehn's lemma" proved by Christos Papakyriakopoulos (and his "loop and sphere theorems,") an example of a hard proof that was not substantially simplified? For all I know (but I am not sure) , it is still a necessary piece of the proof of Poincare conjecture. – Gil Kalai Dec 22 '13 at 5:52
• Shalom Gil! I'd say that the proofs of these theorems have been substantially simplified: ms.unimelb.edu.au/~rubin/publications/localdehn8.pdf – Daniel Moskovich Dec 22 '13 at 6:31
• Yes, Rubinstein's proof of the loop and sphere theorems is quite novel and new. In particular he gets a rather clean proof of the equivariant versions of the theorems. – Ryan Budney Apr 24 '14 at 20:28
• Hmm, I read that proof, and thought I understood it. Maybe I should revisit it to see if that was true. – Dylan Thurston Sep 11 '15 at 17:00

Look for theorems that have been, or are currently, the subject of major formalization efforts!

The two highest-rated answers as I write this [1,2] -- concerning the Four-Color and Feit-Thompson theorems -- don't mention a major point in the history of those theorems: proofs of both theorems have been completely formalized in the Coq proof assistant in the last ten years: the Four-Color Theorem in 2005 [3] and the Feit-Thompson Theorem in 2012 [4], with both developments led by George Gonthier [7] of Microsoft Research, Cambridge. I believe both of these theorems were chosen for formalization efforts precisely because the existing proofs were so large and complicated that it was considered impossible for a single individual to understand them completely and convincingly. UPDATE: as pointed out in the comments, I am wrong about the difficulty of the Feit-Thompson theorem. Rather, its original proof runs "only" about 250 pages and [12]:

“The Feit-Thompson Theorem,” Gonthier says, “is the first steppingstone in a much larger result, the classification of finite simple groups, which is known as the ‘monster theorem’ because it’s one of those theorems where belief in it resides in the belief of a few selected people who have understanding of it.”

This is particularly significant for the Four-Color Theorem: while the theorem reducing the problem to finitely many cases was peer reviewed in the original 1976 computer-assisted proof [5], the computer code which checked the finitely many cases in the 1976 proof was not peer reviewed [[6]] -- indeed the effort to peer review was abandoned after much effort, because the code was judged too long and complex [[6]]. Contrast this with the 2005 proof: going far beyond peer review, the code has been completely formalized, meaning a specification stating what the code should do has been given -- it should check the finitely many cases correctly -- and they have proven that their code meets that specification. This is an amazing achievement!

The AMS Notices article about the formalization of the Four Color Theorem -- taken from a special issue of the Notices devoted to computer-aided formal proof [9] -- provides a fascinating history of the proof and discussion of the formalization, along with an introduction to computer-aided formal proof for the non-specialist.

The Coq proof assistant [8,10] is a system for constructing and checking completely formal proofs on the computer. Another of it's major success stories is the formalization of an optimizing C compiler [11].

[[6]]: http://www.ams.org/notices/200811/tx081101382p.pdf‎ (I can't get this link to work as a footnote ???)

• I agree that the four-color theorem's proof is "so large and complicated that it was considered impossible for a single individual to understand them completely and convincingly", but is that really the case for Feit-Thompson? My impression is that Feit-Thompson was chosen as a step towards the classification of finite simple groups (for which that statement would certainly be true). – Henry Cohn Dec 23 '13 at 13:34
• I think lots of people understand the proof of Feit-Thompson, though it is a very hard theorem. Its significance is that it's a good testing ground for eventually formalizing the full classification. – arsmath Dec 23 '13 at 14:57
• @HenryCohn and arsmath: thanks for the correction, I've updated the answer. – ntc2 Dec 23 '13 at 21:55
• From my perspective, the Feit-Thompson theorem is "very hard" on its own, and it will be great if a simpler proof will be found. Strangely, I am not entirely sure if I regard the proof of the four-color theorem as "very hard" but certinly a different shorter proof that we can understand in details will be absolutely great! – Gil Kalai Dec 24 '13 at 10:12

Kolmogorov-Arnold-Moser (or KAM) theorem.

KAM theory gives conditions for persistence of invariant tori under small perturbations of a Liouville-integrable Hamiltonian system. It is one of the most important parts of the applied dynamical systems.

Although I am far from an expert, I believe that the original proofs have not been substantially simplified. In fact, later related work by M.Herman and others is likewise quite long and hard.

• John Hubbard wrote an interesting story about this which I will selectively quote: "I first heard about the KAM theorem when I was an undergraduate... It seemed to me the most beautiful result in the world... Each year, for about fifteen years, I said to myself in September: this is the year that I am going to understand the proof. Each year, as March came around, I had to admit failure once again: I no longer knew the order of the quantifiers in the technical lemmas, and so was unable to apply them. During these years, I tackled all the proofs" – Marius Kempe Dec 20 '13 at 18:13
• "that I knew: Arnold’s, Moser’s, Sternberg’s, those based on the Nash–Hamilton implicit function theorem, those of Herman... I did not succeed in mastering a single one. And I am far from being alone: I know numerous dynamicists who realize that they ought be able to prove the theorem, who even teach it sometimes, but who have never mastered the proof either. After being pointed in the right direction by Pierre Lochak, I finally discovered the article of Bennettin, Galgani, Giorgilli and Strelcyn, which I found luminous. With the help of Yulij Ilyashenko, I discovered several improvements:" – Marius Kempe Dec 20 '13 at 18:14
• "this is the proof published in [HI02]. Ilyashenko gave an exposition of it at the Moscow mathematics seminar in 2002; in the audience were some participants from Kolmogorov’s seminar in 1957; they told him that this proof was in fact the original proof." – Marius Kempe Dec 20 '13 at 18:15
• PS. It turns out the page linked above is the beginning of an article, 'The KAM Theorem', in Kolmogorov's Heritage in Mathematics, 2007. – Marius Kempe Feb 27 '15 at 1:11

The classification of finite simple groups

This theorem describes completely all finite simple groups: A finite simple group is either cyclic groups of prime order, alternating groups, groups of Lie type (included some twisted families), or one of 26 sporadic simple group. The proof extends over many paper by many people. The completion of the project was announced in 1983, but some incomplete part was replaced by a complete proof only more recently. There was a project for major revised and simplified proof but it was also very hard. Here is a link to a review paper of Solomon. (The answer was suggested by Victor Protsak.)

Gross-Zagier formula (1986) relating the heights of Heegner points on elliptic curves and the derivatives of $L$-series was a major source of progress in number theory in the last 25 years (cutting pretty close here!). Once again, it is my understanding that the original proof has not been dramatically improved.

• Hopefully, BCnrd can confirm or refute this claim. – Victor Protsak Dec 20 '13 at 11:07
• There have been substantial generalizations of this result (by Shou-wu Zhang et al.) which put it into a broader framework, making more effective use of automorphic methods to reduce the dependence on quirky facts about GL(2) and modular curves, etc. So our understanding of what underlies the theorem is much improved, though not sure any of it should be called a dramatic "simplification": still very hard stuff. – user76758 Dec 20 '13 at 22:12
• Right. Brian wrote a 97 page paper Gross-Zagier revisited giving a streamlined approach to Chapter III of Gross-Zagier. But this was published nearly 10 years ago. – Victor Protsak Dec 21 '13 at 2:40

I'm surprised no one has mentioned Freedman's Theorem from 1982 yet. Technically this theoerem says that Casson handles are standard, but more broadly this completes the classification of topological 4-manifolds, and is one of two major theorems going in to the proof of the existence of exotic 4-manifolds.

(The other half is Donaldson's work on gauge theories. That half has been somewhat simplified with the introduction of Seiberg-Witten theory.)

I have never attempted to read his proof, but it at least has a reputation for being hard.

• Dear Dylan, It is great you mentioned Freedman's theorem. I was looking for Donalsdson's theorem in the sister question and it would be very nice to mention it there. – Gil Kalai Sep 11 '15 at 17:22
• There's some discussion in this MO question mathoverflow.net/questions/87674 – j.c. Sep 24 '15 at 14:54

I'm a bit surprised not to see the Weil conjectures here since their proof by Deligne is so often mentioned as a primary example of something Very Hard. Is there a more simple recent proof that I haven't heared of?

• I vaguely remember that Deligne's proof and some new approaches/simplifications were discussed, but maybe it was in a different question. It is certainly a good answer! – Gil Kalai Dec 24 '13 at 15:17
• Indeed there were some comments (to a deleted answer) regarding major simplification by Laumon and others for Deligne's proof. – Gil Kalai Feb 3 '16 at 23:40
• Here are the old comments: 1) "Is this true? I'm not an expert in the area, but the paper arxiv.org/abs/math/0210149 by Kedlaya seems to give an alternate proof (and the first section lists others)." , 2) This is not true. The technique of ℓℓ-adic Fourier transform introduced by Laumon et al. has led to a much simpler approach to the main results of Weil II (vast and much more useful generalization of Deligne's first paper on the Weil conjectures). – Gil Kalai Feb 4 '16 at 15:51
• (cont) Not easy by any means, but conceptually more digestible. Kedlaya's contribution was to adapt that technique to the pp-adic setting once rigid cohomology had strong enough foundations; the real breakthrough in simplification was in the earlier work of Laumon et al." 3) Nick Katz provided ("Four lectures on Weil II") an alternative proof of one of the main parts of Weil II using "relatively" elementary facts on étale cohomology and the so-called Larsen alternative. – Gil Kalai Feb 4 '16 at 15:52

The proof of the Thue-Siegel-Roth theorem is still very difficult, as no substantial improvement to Roth's original argument is known.

The Thue-Siegel-Roth Theorem states that for any non-rational algebraic number $\alpha$ and $\epsilon > 0$, there exists a small constant $c > 0$ which depends on $\alpha$ and $\epsilon$ such that $$\displaystyle \left \lvert \alpha - \frac{p}{q} \right \rvert > \frac{c}{q^{2 + \epsilon}}$$ for every rational number $p/q$.

• Didn't Faltings give an alternative proof of Roth's theorem? – TKe Dec 24 '13 at 14:46
• Faltings/Wüstholz, Diophantine approximations on projective spaces, Invent. Math. 116 (1994), 109–138 prove Schmidt's subspace theorem, a generalisation of Roth's theorem. – TKe Dec 24 '13 at 15:04
• (I don't want to say that their proof is simpler than Roth's.) – TKe Dec 24 '13 at 15:06
• Is it really so much difficult? It is 15 pages long and spends about 2-3 lectures to explain it to undegraduates (own experience). There is, by the way, a lemma in original Roth's paper which proof may be shorten if we use a probabilistic viewpoint. – Fedor Petrov Sep 11 '15 at 8:59
• I don't know if it is simpler but there seems to be a more "conceptual" proof arxiv.org/abs/1305.0926 by Maculan which relates the result to GIT and Arakelov geometry. – Abdelmalek Abdesselam Sep 11 '15 at 13:45

The decomposition theorem for intersection homology

The decomposition theorem for (middle perversity) intersection homology (for algebraic varieties) was proved in 1982 by Beilinson-Bernstein-Deligne-Gabber. I don't understand it well enough to describe it (but please replace this sentence with a description if you wish). I am aware of many important applications also to the combinatorial theory of convex polytopes. Some applications are described in this MO question Examples for Decomposition Theorem with a link to the review paper: "The Decomposition Theorem and the topology of algebraic maps" by de Cataldo and Migliorini,. To the best of my knowledge there is no dramatically simpler proof (but there is another very hard proof by Saito). [Caveat: I am not an expert.]

Update (February 2, 2016): Here is, however, an abstract from the coming March Bourbaki seminar:

Geordie WILLIAMSON, The Hodge theory of the Decomposition Theorem, after M. A. de Cataldo and L. Migliorini

In its simplest form the Decomposition Theorem asserts that the rational intersection cohomology of a complex projective variety occurs as a summand of the cohomology of any resolution. This deep theorem has found important applications in algebraic geometry, representation theory, number theory and combinatorics. It was originally proved in 1981 by Beilinson, Bernstein, Deligne and Gabber as a consequence of Deligne’s proof of the Weil conjectures. A different proof was given by Saito in 1988, as a consequence of his theory of mixed Hodge modules. More recently, de Cataldo and Migliorini found a much more elementary proof which uses only classical Hodge theory and the theory of perverse sheaves. We present the theorem and outline the main ideas involved in the new proof.

More details (June 2016): The paper with the new proof is: The decomposition theorem, perverse sheaves and the topology of algebraic maps M de Cataldo, L Migliorini , Bulletin of the American Mathematical Society 46 (4), 535-633. Williamson Bourbaki's paper is The Hodge theory of the Decomposition Theorem (after de Cataldo and Migliorini)

• This one came to mind for me as well- I have no expertise at all, but somehow in my mind this is an archetype for an "intrinsically difficult theorem", whatever that means. – Daniel Moskovich Dec 23 '13 at 1:48
• "much more elementary proof which uses [...] perverse sheaves" wow. Can't get any more elementary than perverse sheaves, really. – darij grinberg Aug 19 '18 at 0:06

The Sphere packing problem in $\mathbb{R}^3$, a.k.a. the Kepler Conjecture. Although the first accepted proof was published just about 10 years ago, the conjecture is very old, and there were several unsuccessful attempts at it for quite a long time. It seems unlikely that Hales' heavily computer-aided proof will be dramatically improved in the foreseeable future.

Every $L^2$ function on $\mathbb{R}$ is almost everywhere the point-wise limit of its Fourier series. These days known as Carleson's theorem.

• The 9-page proof of Carleson's theorem by Lacey and Thiele in 2000 ams.org/mathscinet-getitem?mr=1783613 is significantly shorter than Carleson's original 22-page proof (or Fefferman's 20-page reproof), but more importantly places the theorem in a systematic time-frequency framework (of tiles, trees, forests, and mass and energy estimates) from which one can also control a large family of other operators in harmonic analysis (paraproducts, bilinear Hilbert transforms, maximal oscillatory integral operators, etc.). – Terry Tao Dec 20 '13 at 17:12
• Thanks. I'll keep my answer here as a reminder for everybody, that one should keep up with his/her subject. – Vít Tuček Dec 20 '13 at 22:56
• Dear Vit, many thanks for your answer (which was certainly correct for more than a decade). I think it is a good and useful answer (while incorrect). Like in the case of Szemeredi's theorem an even simpler proof of Carleson's theorem is much desirable. In some sense, reasonable incorrect answers to the question can be as educating as correct ones. (And we do hope that most answers will become incorrect before they fit the 100-years twin MO question.) – Gil Kalai Dec 21 '13 at 7:57

The proof of the Oppenheim conjecture by G. A. Margulis in $1986$ may qualify. It is a famous result, $27$ years ago, has a hard proof, which has not been dramatically simplified (if I am not mistaken, the simplification of Dani and Margulis not counting. Ratner's result made it possible to study the quantitative version of the Oppenheim conjecture).

• with Ratner's theorem, you are almost getting a 3 lines proof (Basically, $SO(2,1)$ is a maximal unipotent subgroup of $SL_{3}$). One might say that it builds on Ratner's MC theorem (where Margulis' proof was by purely topological dynamics in some sense), but still, I think that the people who are doing Homogeneous Dynamics would consider this a simplification, as Ratner's theorems are nowadays standard in that field and in number theory at general. – Asaf Dec 21 '13 at 15:47
• Nevertheless, the argument by Dani and Margulis is a bit more simplified, in the way that enabled Margulis and Lindenstrauss to prove an effective Oppenheim conjecture (the paper got released only in $2013$!, because of building on the famous work of Einsiedler-Margulis-Venkatesh about effective equidistribution of horospheres). – Asaf Dec 21 '13 at 15:49
• As Gil have asked me to add here, Ratner's proof of the Oppenheim conjecture relies on (the orbit closure theorem which relies on-)the measure-classification theorem for $SO(2,1)$-inv.+ergodic measures on $SL_{3}(\mathbb{R})/SL_{3}(\mathbb{Z})$, a few years ago, Manfred Einsiedler have given a simple proof of the measure classification theorem in such a case (action of a semi-simple group) here - math.ethz.ch/~einsiedl/omgsur.pdf – Asaf Jan 4 '14 at 16:01

The Restricted Burnside Problem asked whether there is a bound on the size of a finite group with $d$ generators and exponent $n$. Kostrikin proved there is a bound for $n$ a prime in the fifties. Hall-Higman theorem reduced it to prime power $n$'s. Zelmanov gave a positive answer for prime powers (the odd case appeared 1990 and the even case in 1991, so we are borderline 25 years). The proof is very difficult and as far as I know it was never simplified (or at least not substantially).

Szemerédi’s theorem, that inside a positive-density set of naturals there are arbitrarily long arithmetic progressions. To quote Terry Tao, "...the pieces of Szemerédi’s proof are highly interlocking, particularly with regard to all the epsilon-type parameters involved; it takes quite a bit of notational setup and foundational lemmas before the key steps of the proof can even be stated, let alone proved... Many years ago I tried to present the proof, but I was unable to find much of a simplification, and my exposition is probably not that much clearer than the original text."

• Dear Allen, This remarks referred to Endre's original proof. There are substantially simpler proofs available now. (But it would be great to have a proof that you can present in 4 hours, say.) – Gil Kalai Dec 20 '13 at 14:10
• Oops, I meant to include the "I'm not an expert" caveat! – Allen Knutson Dec 20 '13 at 16:15
• Furstenberg's proof is much easier than Szemeradi's, and probably much more conceptual and influential (i.e. the Green-Tao theorem). But probably Gil wanted the improved proof to be in the same "flavour", and not doing a radical change as Hillel have done. – Asaf Dec 21 '13 at 15:55
• No no, Furstenberg's proof is indeed simpler (and there is a further simplification of his approach); The proof based on hypergraph regularity is also simpler than Endre's original proof. So is the polymath1 proof. (The last two are easier than the ergodic theoretic proof) So we do have several dramatic simplifications but none that can be presented in 4 hours. – Gil Kalai Dec 21 '13 at 17:29

The Selberg Trace Formula- general case

Hejhal's original 1983 proof is 1322 pages long! As far as I know, the proof remains famously very hard.

• Well, it depends what is meant by "Selberg trace formula". If one speaks of the most general form (Arthur-Selberg trace formula), certainly it is very hard because it requires so much input. But Hejhal's book only treats the case of $SL_2(\mathbf{R})$, and although this remains tricky, it is not so far out of reach. It can be/is certainly done in introductory graduate courses on modular forms (see e.g. Iwaniec's "Introduction to the spectral theory of automorphic forms", but there are other treatments.) – Denis Chaperon de Lauzières Dec 22 '13 at 9:32

The construction of the $\Phi^4_3$ quantum field theory model. This was done in the early seventies by Glimm-Jaffe, Feldman, Feldman-Osterwalder, Magnen-Seneor.

This model is related to current research since it should provide the invariant measure for the stochastic quantization SPDE in three spatial dimensions (see e.g the work of Hairer, Catellier-Chouk and Kupiainen).

As far as I know, the Quillen equivalence between simplicial sets and topological spaces is one of such theorems.

• In "Les préfaisceaux comme modèles des types d'homotopies", Cisinski gives a alternate proof (to the standard one, presented say in Goerss-Jardine) which puts in into a more general context of model structures on presheaves on sets on small categories. – Simon Pepin Lehalleur Dec 20 '13 at 19:26
• Is this proof much simpler? If yes, do you know any English reference? I don't read French. Thank you! – Sasha Patotski Dec 20 '13 at 20:48
• While this is a very important theorem its proof doesn't really count as "very hard", at least not in comparison to the results mentioned in other answers here. Moreover, many improvements have been made over the years and you can piece together a fairly elementary proof from them. I think that the easiest published proof I know is in May, Ponto More Concise Algebraic Topology. Cisinski's proof uses quite different methods than Quillen's original proof, but it is not any easier in my opinion. – Karol Szumiło Dec 20 '13 at 22:24

The Benedicks-Carleson theorem on the existence of strange attractors for Hénon maps is an example, I would say. Over the years, there have been some attempts to give improved presentations of the proof, but I don't believe there have been any dramatic simplifications. (However, I am not an expert in this precise area of dynamics.)

Nb. The paper was published in January 1991, which date misses your 25-year rule by a few months. However, the paper was received by the journal in 1988, and revised in 1989, so I shall invoke those dates to argue for its eligibility. ☺