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

-
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
@VítTuček: please see my answer below. It does not address the amount of time it would take to manually check the finitely many cases, but explains why that's unnecessary with the current (2005) proof: the current computer code has been proven correct! –  ntc2 Dec 23 '13 at 12:06
@Matt: the peer reviewers for the original 1976 proof could not convince themselves to trust the computer code which checked the finitely many cases, because it was long and complex. So, it should be emphasized that "proof by computer" can mean either "proof involving a computer calculations" or "formal proof checked by a computer". The 1976 proof was the former, and hard to trust; the 2005 proof was the latter, and easy to trust. –  ntc2 Dec 23 '13 at 12:11
@VítTuček: according to page 10 of this the current proof reduces the problem to about 600 "configurations". According to page 12, "a longhand demonstration [of the example configuration] would need to go over 20 million cases". I have no idea what a "case" is here, but assuming one minute per case, your undergraduate would need about 40 years to check that one configuration! –  ntc2 Dec 23 '13 at 22:00

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

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
Thanks! Edited to clarify. –  Daniel Moskovich Dec 20 '13 at 10:21
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 at 20:28

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

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

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

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

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? –  Timo Keller 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. –  Timo Keller Dec 24 '13 at 15:04
(I don't want to say that their proof is simpler than Roth's.) –  Timo Keller Dec 24 '13 at 15:06

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

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

-
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

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.

-

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

-

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 at 16:01

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

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

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

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