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

Question

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.

Answer 1

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.

Answer 2

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.

Answer 3

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.

Answer 4

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

Answer 5

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

Answer 6

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

Answer 7

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.

Answer 8

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.

Answer 9

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.

Answer 10

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.

Answer 11

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?

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

Answer 13

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

Answer 14

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)

Answer 15

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.

Answer 16

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

Answer 17

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.

Answer 18

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

Answer 19

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

Answer 20

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

Answer 21

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.

Answer 22

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

Answer 23

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.

Answer 24

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