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 exercises for first-year graduate courses, provable in a couple pages by 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.)
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
This is the stuff you could use to cut down on requests for extra credit.
Are there examples of homework problems today that were quite difficult to prove 100 years ago?
Interesting ideas here.
Another possibility is that there will be a proof assistant that is user-friendly and ubiquitous enough and has enough background theorems pre-programmed into it that undergraduate students will be able to work through these proofs themselves via computer, rather than by hand. Presumably there is still something valuable about understanding where the cases come from and what needs to be checked about each one.
This citation, form Grothendieck himself, to me shows a little bit why, a part from him being exceptionally gifted, his approach to problems was radically different. He describes the process of solving a math problem as that of opening a nut:
*The … analogy that came to my mind is of immersing the nut in some softening liquid, and why not simply water? From time to time you rub so the liquid penetrates better, and otherwise you let time pass. The shell becomes more flexible through weeks and months—when the time is ripe, hand pressure is enough, the shell opens like a perfectly ripened avocado! A different image came to me a few weeks ago. The unknown thing to be known appeared to me as some stretch of earth or hard marl, resisting penetration … the sea advances insensibly in silence, nothing seems to happen, nothing moves, the water is so far off you hardly hear it … yet it finally surrounds the resistant substance.”
In this paper you may find some description of the intellectual environment and the ideas that allowed such approach to problems to work incredibly well.
http://www.cwru.edu/artsci/phil/RisingSea.pdf
Aaron Meurer — most if not all of a first course in real analysis consists in theorems that were very hard 1-200 years ago.