In his 1990 article “Has progress in mathematics slowed down?” Paul Halmos mentions two of the longest proofs in mathematics: the Four Color Theorem and the classification of finite simple groups.

The proof of the **Four Color Theorem** appeared in 1976. The authors manually broke the problem into 1,936 cases which were then verified using a computer. The **classification of finite simple groups** was the culmination of many journal articles totaling around 10,000 pages.

Halmos believed that these were not “good” proofs. They establish the truth of their claims, but they are so large and tedious that they don’t give much insight into their subjects. He also believed that over time the proofs of both theorems would be simplified.

A hundred years from now

both theorems(maps and groups)will be exercisesfor first-year graduate courses,provable in a couple pagesby means of the appropriate concepts, which will be completely familiar by then.

(Emphasis added.)

So where do we stand, 23 years later? The number of special cases required for the Four Color Theorem has been reduced to 633, about one third of the original number. The proof has been verified via the Coq proof assistant software but is still requires a computer. There is an ongoing effort to produce a “second generation” proof of the classification of finite simple groups. This effort is expected to fill around 5,000 pages, half the original count, and also to be easier to read.

Halmos said that over time,

… mathematics shortens proofs, gives insight, and deepens understanding by the discovery of new concepts and by the subsumption of old ones under a suitably general theory that took years, decades, and sometimes centuries of labor to construct.

This has happened for the two theorems under discussion here, but not yet to a very large extent. If we assume the size of the classification of finite simple groups is decreasing exponentially, it will still be 625 pages in the year 2090. But progress in mathematics isn’t so predictable. The proof may hover at 5000 pages for decades, then suddenly collapse to 100 pages after some brilliant breakthrough. A two-page proof by 2090 seems unlikely. I doubt Halmos meant his prediction literally, but it would be interesting to see where things stand by then. (Someone mark your calendar to write a follow-up blog post in 77 years in case I stop blogging before then.)

**Related posts**:

Interesting theorem, interesting comment and nice article. Thanks!

(by the way: You are using “over time” twice in the same sentence — “He also believed that over time the proofs of both theorems would be simplified over time.”)

I wrote a truly marvelous Python script that solves this, I’d post it but your comment form has a character limit.

Alternative: we’ll develop greater understanding of the nature of proofs in these domains explaining why there’s some lower bound on the “length” of such proofs.

See, e.g. boolos on cut elimination