90

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)

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

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.

Community
  • 1
Gil Kalai
  • 24,218
  • 3
    I basically asked the same thing before: http://mathoverflow.net/questions/44593/still-difficult-after-all-these-years – arsmath Dec 20 '13 at 07:20
  • 5
    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 07:39
  • 1
    Does the classification of finite simple groups qualify? See also my answer below. – Victor Protsak Dec 20 '13 at 08:39
  • Dear Victor, Yes – Gil Kalai Dec 20 '13 at 08:57
  • 8
    @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 09:21
  • 8
    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 09:38
  • Also, arsmath, your question specifically referred to 100-years old or so theorems: "Are there results from a hundred years ago that have not appreciably simplified over the years? From the point of view of a modern mathematician, what is the hardest theorem proven a hundred years ago (or so)?" – Gil Kalai Dec 20 '13 at 10:03
  • I have to confess that even with 3 answers, I still cannot pin down the reference "non-technical description of a major theory; the proofs are quite hard" that's swirling in my head – Victor Protsak Dec 20 '13 at 11:12
  • 3
    The proof of the classification of finite simple groups has actually gotten harder. – Andrés E. Caicedo Dec 21 '13 at 07:32
  • 1
    One way to regard this question is as a wish list: "A hard major theorem I would like to be simplified!" – Gil Kalai Dec 24 '13 at 16:31
  • 1
    5 years to wait until someone posts Fermat's last theorem... – Manuel Bärenz Sep 11 '15 at 11:28
  • I think Kepler's conjecture should be deleted from the list, since its proof is less than 25 years old. – GH from MO Sep 25 '15 at 00:25
  • 2
    I hope someone knowledgeable sees this and can answer: what is the status of the proof of Thom's isotopy lemmas, since Mather's 1970 Harvard notes? (reprinted here: http://www.ams.org/journals/bull/2012-49-04/S0273-0979-2012-01383-6/S0273-0979-2012-01383-6.pdf) – Todd Trimble Aug 19 '18 at 01:09

24 Answers24

48

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.

sds
  • 165
Daniel Moskovich
  • 21,887
  • 3
    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
  • 17
    @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
  • 2
    @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
  • 7
    @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
  • 1
    @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
  • 7
    A recent program of Kronheimer and Mrowka may lead to a new, more comprehensible proof of the four-color through instanton homology: http://arxiv.org/abs/1508.07205 – Sam Hopkins Sep 11 '15 at 17:18
  • 14
    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 00:44
  • 9
    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 03 '15 at 22:58
  • 2
    This raises an interesting question: what makes a proof 'hard'? I think of the proof of the 4CT as frankly pretty straightforward; the key elements are all at an undergrad or low-graduate level at worst (probably lower now than they were at the time, since they're so algorithmic). The time-consuming part is just a massive block of case-checking, and while getting that formally verified is time-consuming, it doesn't seem at all 'hard' in the way that things like KAM do. – Steven Stadnicki Aug 19 '18 at 15:44
37

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.

Gil Kalai
  • 24,218
Victor Protsak
  • 14,347
  • Apparently, my answer was too short, even after including the link! – Victor Protsak Dec 20 '13 at 08:38
  • 2
    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 http://mathoverflow.net/questions/114943/where-are-the-second-and-third-generation-proofs-of-the-classification-of-fin). And let's ignore the fact the quasithin case was plugged after the cutoff. – David Roberts Dec 23 '13 at 12:17
  • 3
    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 00:14
  • 3
    The proof remains long, but it no longer takes a sizable part of a lifetime to check; see http://research.microsoft.com/en-us/news/features/gonthierproof-101112.aspx – John Stillwell Dec 29 '13 at 23:27
26

The Graph-Minor Theorem.

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.

Gil Kalai
  • 24,218
  • 6
    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
25

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.

See also this MO question: Uniformization theorem for Riemann surfaces

Community
  • 1
Alexandre Eremenko
  • 88,753
  • 10
    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
  • 1
    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 Sep 24 '15 at 15:58
  • 3
    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
  • 2
    A simple proof as Theorem VIII.11.12 is in Demailly's book. First do the case of domains of the plane, which is elementary. Then compact surfaces, using for instance Riemann-Roch. For a noncompact surface $U$, take an exhausting sequence of relatively compact connected open sets with smooth boundary $\Omega_k$. The connected sum $\Omega_k \cup \overline{\Omega_k}$ has a complex structure by reflection, and by the previous case you embed $\Omega_k \subset\mathbb{C}$. Up to subsequences, these converge to an embedding of $U$ – Andrea Ferretti Feb 10 '20 at 13:11
  • It seems to me that this proof could be covered in full detail in a couple of hours max, once Riemann-Roch for Riemann surfaces is done – Andrea Ferretti Feb 10 '20 at 13:14
  • @Andrea Ferretti: a) It depends on your students background, b) How much time is required for Riemann-Roch? c) Riemann-Roch is for compact surfaces, and the Uniformisation theorem is for all surfaces. – Alexandre Eremenko Feb 10 '20 at 13:18
  • @AlexandreEremenko of course it depends, but Riemann Roch is a pretty standard result proved in many courses. Once that is known, obtaining the uniformization theorem for all surfaces is pretty easy, and I tried to give a hint of how to do it in my comment above. I mean, of course the comment does not have many details, but the fact that the outline of the proof + reference can fit in a single Mathoverflow comment makes me classify this as pretty simple. – Andrea Ferretti Feb 10 '20 at 13:23
21

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 its 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 ???)

Greg Martin
  • 12,685
ntc2
  • 101
  • 4
    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
  • 2
    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
  • 1
    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
21

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

Gil Kalai
  • 24,218
  • For this example, just stating the theorem (i.e., defining all sequences of groups of Lie type, and all sporadic ones) takes a while — this can make a whole book. – YCor Oct 06 '22 at 08:16
20

The Smale Conjecture.

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.

Community
  • 1
Daniel Moskovich
  • 21,887
  • 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 05:52
  • 5
    Shalom Gil! I'd say that the proofs of these theorems have been substantially simplified: http://www.ms.unimelb.edu.au/~rubin/publications/localdehn8.pdf – Daniel Moskovich Dec 22 '13 at 06:31
  • 1
    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
  • 5
    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
  • 1
    There is a new proof of the Smale conjecture due to Bamler and Kleiner. https://arxiv.org/abs/1909.08710 I don't think that this is an "easier" proof - it is a very different relying on analytic, instead of combinatorial, techniques. – Sam Nead Dec 17 '21 at 08:34
17

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.

Jairo Bochi
  • 2,411
Victor Protsak
  • 14,347
  • 10
    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
  • 9
    "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
  • 13
    "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
  • 2
    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 01:11
14

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.

Victor Protsak
  • 14,347
  • 3
    Hopefully, BCnrd can confirm or refute this claim. – Victor Protsak Dec 20 '13 at 11:07
  • 2
    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
  • 2
    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 02:40
14

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.

Dylan Thurston
  • 10,033
  • 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
  • 2
    There's some discussion in this MO question http://mathoverflow.net/questions/87674/ – j.c. Sep 24 '15 at 14:54
13

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?

Vincent
  • 2,437
  • 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 03 '16 at 23:40
  • 2
    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 04 '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 04 '16 at 15:52
12

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.

Wlodek Kuperberg
  • 7,256
12

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

Gil Kalai
  • 24,218
Stanley Yao Xiao
  • 25,509
  • 1
    Didn't Faltings give an alternative proof of Roth's theorem? –  Dec 24 '13 at 14:46
  • 1
    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. –  Dec 24 '13 at 15:04
  • (I don't want to say that their proof is simpler than Roth's.) –  Dec 24 '13 at 15:06
  • 3
    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 08:59
  • 3
    I don't know if it is simpler but there seems to be a more "conceptual" proof http://arxiv.org/abs/1305.0926 by Maculan which relates the result to GIT and Arakelov geometry. – Abdelmalek Abdesselam Sep 11 '15 at 13:45
10

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’s Bourbaki paper is The Hodge theory of the Decomposition Theorem (after de Cataldo and Migliorini)

Zach Teitler
  • 6,197
Gil Kalai
  • 24,218
  • 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 01:48
  • 4
    "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 00:06
9

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.

Vít Tuček
  • 8,159
  • 25
    The 9-page proof of Carleson's theorem by Lacey and Thiele in 2000 http://www.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
  • 2
    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
  • 5
    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 07:57
6

The Restricted Burnside Problem asked whether there is a bound on the size of a finite group with $d$ generators and exponent $n$. In the 1950s, Kostrikin proved there is a bound for $n$ a prime. 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).

darij grinberg
  • 33,095
Yiftach Barnea
  • 5,208
  • 2
  • 36
  • 49
6

Chazelle's linear time algorithm for the triangulation of a polygon has not been improved upon since its creation in 1991.

Technically, this is a computer science theorem, but I think it belongs here for a couple reasons. It's complicated. No actual code implementation of the algorithm has ever been made. While it is linear time, the constant factor makes the algorithm useless for any practical purposes, beyond its theoretical use in other papers.

Larry B.
  • 101
5

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

Dietrich Burde
  • 11,968
  • 1
  • 32
  • 65
  • 2
    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
  • 2
    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
  • 2
    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 - http://www.math.ethz.ch/~einsiedl/omgsur.pdf – Asaf Jan 04 '14 at 16:01
5

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

Abdelmalek Abdesselam
  • 21,801
4

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

Allen Knutson
  • 27,645
  • 8
    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
  • 3
    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
  • 3
    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
4

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.

Daniel Moskovich
  • 21,887
  • 5
    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 09:32
4

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

Lasse Rempe
  • 6,455
2

Hadwiger's conjecture for $K_6$-free graphs.

This paper shows the equivalence of Hadwiger's conjecture for graphs with no $K_6$ minor and the four-colour theorem. The reduction to 4CT (that every minimal counterexample to the main result would be an apex graph) is a tour de force that takes well over 80 pages.

user160393
  • 123
  • 5
1

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

Sasha Patotski
  • 1,266
  • 2
    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
  • 16
    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