Birth of a Theorem: A Mathematical Adventure

by Cédric Villani

  And yet on my first try, as if by magic, movement is restored to my feet, and once again I am whole. The break is over, ten minutes exactly. I’m a new mathematician.

  Cedric reboot (completed)

  A new Cédric. Time to embark on a fresh round of calculations. There’s also an article on Landau damping, more than fifty years old but still very relevant today, that I just got from the library. Now for two hours of intense concentration before tea …

  * * *

  The Syracuse problem (also known as the Collatz conjecture or the 3n + 1 problem) is one of the most famous unsolved enigmas of all time. Paul Erdős himself is on record as saying that mathematics is not yet ready to confront such monsters.

  Enter the expression “3n + 1” in an Internet search engine and follow the thread back to the abominable problem and its result, as simple and insistent as the refrain of a pop song:

  Take any whole number you like, say 38.

  This number is even. Divide it by 2 and you get 19.

  This last number is odd. Multiplying by 3 and adding 1 you get 19 × 3 + 1 = 58.

  This last number is even. Divide it by 2.…

  And so on. You go on from one number to the next by means of a simple rule: each time you encounter an even number, divide by 2; each time you encounter an odd number, multiply by 3 and add 1.

  Starting from 38, as in the example above, you get the following sequence: 19, 58, 29, 88, 44, 22, 11, 34, 17, 52, 26, 13, 40, 20, 10, 5, 16, 8, 4, 2, 1, 4, 2, 1, 4, 2, 1, 4, 2, 1, 4, 2, 1, 4, 2, 1 …

  Once you arrive at 1, in other words, you know what comes next: 4, 2, 1, 4, 2, 1, 4, 2, 1…, ad calculam aeternam.

  Every single time this calculation has been performed in the course of human history, it has ended up at 4, 2, 1.… Does that mean it will always turn out thus, no matter which number is chosen as the point of departure?

  Since there are infinitely many integers, obviously it’s impossible to try all of them. With all the pocket calculators, desktop calculators, computers, and supercomputers at our disposal today, it has nevertheless been possible to try billions and billions of them, and every last one has wound up leading back to the implacably repeating 4, 2, 1 pattern.

  Mathematics is democratic, of course, and anyone is free to try to show that this sequence embodies a general rule. Everyone believes the rule to be true, but since no one knows how to prove it, it remains a conjecture. Whoever succeeds in confirming or disconfirming this conjecture will be proclaimed a hero.

  I am certainly not among those who will try. Apart from the fact that it seems to be phenomenally difficult, it isn’t the sort of problem that suits the way my mind works. My brain isn’t used to thinking about such things.

  * * *

  Date: Mon, 4 May 2009 17:25:09 +0200

  From: Cedric Villani

  To: Clement Mouhot

  Subject: Backus

  So here’s Backus’s article from JMP 1960 (Vol.1 No.3, too bad it wasn’t Vol.1 No.1!)

  Fantastic! Take a look at the next-to-last section of Backus’s article, and then the last sentence of the article. It’s all the more remarkable since as far as I’m aware no one has explicitly expressed these doubts until recently, the last few years …

  Best

  Cedric

  Date: Sun, 10 May 2009 05:21:28 +0800

  From: Clement Mouhot

  To: Cedric Villani

  Subject: Re: Backus

  I read a bit of Backus’s article on the plane. It is indeed very interesting, he had a good grasp of the linear pbs and the question of the increase over time of the background term once it depends on the space, through filamentation. And for the most part he’s remarkably rigorous compared to the “standard” of articles on Landau damping … We need to cite to him, particularly his numerical discussion page 190, and the conclusion expressing his doubts regarding the nonlinear validity of the linear case: this links up with one of the conceptual difficulties of our intro as well.

  Best regards, Clement

  THIRTY-ONE

  Princeton

  A lovely evening in May 2009

  May at the Institute for Advanced Study. The trees are in bloom, it’s magnificent.

  Night has just fallen. I’m wandering alone in the half-light, savoring the encroaching darkness, the sense of peace, the softness of the air.

  When I was a student at the École Normale Supérieure, I used to love to walk the dark corridors of the dormitory at night, a few rays of light glimmering beneath the doors, like the vague luminescence one imagines passing through the portholes of the submarine in Jules Verne’s famous tale.

  But there’s no comparison with the evening here, the lawns and the breeze. You’ve got the light, too, but it isn’t the artificial illumination of civilized life, it’s the natural light emitted by fireflies—uncountably many twinkling stars covering the grass!

  Oh, wait a minute … didn’t I read an article once, applying Landau’s damping theory to the twinkling of fireflies?…

  Cédric, please! Can’t you forget about Landau damping for just a little while? Enough already—mille pompons! You’ve spent so many days and nights on it as it is. Come on, enjoy the fireflies and give Landau a rest—

  Who’s that coming toward me? Apparently I’m not the only one out for a walk after sunset … I recognize the silhouette … well, what do you know! It’s Vladimir—Vladimir Voevodsky, one of the most brilliant mathematicians of his generation, 2002 Fields medalist, one of Grothendieck’s spiritual heirs. Just the sort of person you’re apt to run into if you venture out at night at the IAS.

  Like me, Voevodsky was out walking with no particular destination in mind, just walking, walking for air—like the pedestrian in Ray Bradbury’s story.

  We got to talking. It’s hard to imagine someone whose mathematical interests are more different from mine. I don’t understand a thing about his research, and he probably doesn’t understand a thing about mine. Rather than try to explain to me what he’s doing now, Vladimir told me about what he wants to do next. He’s completely fascinated by expert languages and automated theorem proving, and plans to devote himself wholeheartedly to them in the years ahead.

  Vladimir Voevodsky

  He talked about the famous four-color theorem, and the disputed proof by Appel and Haken—disputed because, in the eyes of their critics, their proof had “dehumanized” mathematics by subjugating it to computer science. The controversy was recently dispelled (or aggravated, depending on your point of view) by French researchers who brought about a small revolution with the aid of an expert language known as Coq.

  Vladimir thinks the time isn’t far off when computer programs will be able to check long and complex arguments. In fact, he says, such programs are now being tried out in France on a number of famous results. I must admit I was skeptical at first. But the person telling me this isn’t mad; he’s quite sane, and a mathematician of the highest ability. I’ve got to take what he says seriously.

  Proof checking is the sort of problem I’ve never even looked at. Algorithmics in general is something I know very little about. It is true, of course, that so-called marriage algorithms (technically, bipartite matching algorithms), simplex algorithms, and auction algorithms play an important role in the numerical simulation of optimal transport, one of the topics that I specialize in; but in optimal transport they’re used in a way that is very different from what Vladimir’s talking about. This new field really does seem exciting. There are so many wonderful things to explore today!

  Flowers, languages, four colors, marriage—everything you need to write a fine song … unless perhaps someone’s already written it?

  * * *

  Around 1850 the mathematician Francis Guthrie colored a map of the counties of England, taking great care to ensure that no two counties sharing a boundary of any length have the same
color. How many colored pencils would he have had to use?

  Guthrie saw that four colors sufficed. What is more, he suspected that four would suffice to color any such political map (any map, that is, that does not contain counties or states or countries that are divided into noncontiguous parts).

  Three colors are plainly not enough. Look at the map of South America, for example, and you will see that in the case of Brazil, Argentina, Bolivia, and Paraguay, each of these four countries borders on three others, and so you need at least four different colors.

  The conjecture that four are all you will ever need is something that you can test yourself by coloring your favorite map. If you had enough patience, you could test it for a rather large number of examples. But how could it be shown to be true for every map? Nobody can possibly test every one, since once again there are an infinite number. There is no alternative but to construct an argument on purely logical grounds. As it turns out, this is not easily done.

  In 1879, Alfred Kempe believed he had proved the four-color theorem. But his proof was flawed, and demonstrated only that five colors suffice.

  Let’s take it one step at a time. For a map with four countries, we know what the answer is. Beyond that, it’s a simple matter to find the answer for five countries, likewise for six. How far can we go on before we run into difficulties?

  Suppose that we know all maps up to 1,000 countries can be colored using four colors and that we want to try our luck with a map representing 1,001 countries. How should we proceed? To begin with, it can be shown that among these 1,001 countries there exists at least one that has relatively few immediate neighbors, let’s say five at most. If we restrict our attention to this country and the ones adjacent to it, there’s no problem; and if we play the conqueror and do a bit of rearranging within the group as a whole, a merger here, a recombination there, we will end up with a map having fewer than 1,000 countries—and so we will be able to color it with four colors. A clever idea … but getting the local coloring and the global coloring to coincide is a complicated business. One still has to consider a great many cases—millions, indeed billions of cases!

  In 1976, Kenneth Appel and Wolfgang Haken managed to reduce the number of configurations needing to be tested to a bit less than 2,000, and went through all of them with the aid of a computer program. After running the program for two months they concluded that four colors will always suffice, thus resolving a conjecture first stated more than a hundred years earlier.

  The mathematical community was profoundly divided over this proof. Hadn’t the mind finally been vanquished by the machine? Could any human intelligence really understand an argument that had served as fodder for a monstrous creature made of silicon and integrated circuits? Supporters and opponents squared off, but no consensus emerged.

  Eventually mathematicians and computer scientists got used to living with this unsettled state of affairs. Fast forward now to the turn of the millennium and the research being conducted by an INRIA team led by Georges Gonthier, a leading authority on proof-checking languages. The fields of computer science and computational science had been pioneered in Europe by a few visionary theorists at the same time that Appel and Haken were making headlines. The languages they devised were meant to check the soundness of a mathematical proof in the same way you would check the health of a tree: branch by branch. Imagine an argument having the form of a logic tree whose branchings can be subjected to automated verification, just as the correctness of your spelling can be decided by a spell-check program.

  But whereas a spell checker is interested only in making sure that individual words are properly formed, a proof checker is designed to check the consistency of the proof as a whole, to make sure that everything hangs together—that each statement follows from the one before without contradiction.

  Gonthier and his principal collaborator, Benjamin Werner, set to work trying to prove the four-color theorem using a language called Coq (after the name of its inventor, Thierry Coquand). Unlike the programs used by Appel and Haken, Coq is “certified”—known, that is, to be bug-free. Another difference is that Coq doesn’t provide you with the actual computations, it automatically generates a proof on the basis of the algorithm that has been selected. Gonthier took advantage of this fact to rewrite the “readable” part of the proof, and in this way succeeded in obtaining a simple and effective result—a thing of beauty! What you have, then, is a proof of which 0.2% was done by a human being and the other 99.8% by a machine. But it is the human 0.2% that matters, that must be gotten right, since with Coq you can be sure that the rest is correct.

  The work of Gonthier and his team heralds the day, not as far in the future as one might suppose, when validation programs will control rocket launchings, airplanes in flight, even the microprocessors in our personal computers. The financial stakes of what was no more than wishful thinking thirty years ago are now reckoned in the billions of dollars.

  In the meantime, the indefatigable Gonthier has embarked on an extremely ambitious project aimed at verifying certain classification theorems of finite groups, whose proofs, among the longest of the twentieth century, are renowned for their complexity.

  * * *

  A word that goes against

  A word that looks askance

  A flame shall grow immense

  Throughout the universe

  Mouths opened wide as pyres

  Fine phrases sweet as rum

  Yet hides find their buyers

  Over the head of a drum

  One day will our language

  Speak truly of flowers

  And also of the marriage

  Of four brilliant colors

  Will it ever come to you

  How they speak of love’s flower

  I promise I shall wait for you

  I shall wait beneath the Tower

  Cain shall meanwhile go on chasing Abel

  But with my bare hands I built the Tower of Babel

  [Guy Béart, from “La Tour de Babel”]

  THIRTY-TWO

  Princeton

  June 26, 2009

  My last day in Princeton. Rain, nothing but rain the last few weeks—so much, in fact, it was almost comical. At night the fireflies transform the oaks and red maples into Christmas trees, romantic, impossibly tall, decorated with innumerable blinking lights. Enormous mushrooms, a small furtive rabbit, the fleeting silhouette of a fox in the night, the startling noises of stray rutting deer …

  * * *

  In the meantime a lot has happened on the Landau damping front! We were finally able to get the proof to hang together, went through the whole thing one last time to be sure. What a wonderful feeling, finally to post our article online! As it turned out, it was in fact possible to control the zero mode. And Clément discovered that we could completely do without the double time-shift, the trick I came up with on my return from the Museum of Natural History back in January. But since we didn’t have the courage to go over the whole thing yet again, and since we figured it might come in handy dealing with other problems, we left it where it was. It’s not in the way, not interfering with anything. We can always simplify later if we have to.

  By this point I’ve given quite a few talks about our work. Each time I was able to improve both the results and the exposition, so the proof is now in very good shape. There may still be a bug somewhere, of course. For the moment, however, all the pieces fit together so well that if an error is discovered, I’m confident we’ll be able to fix it.

  I was invited to speak for two hours at the Plasma Physics Laboratory in Princeton, and afterward I was treated to a marvelous tour of the lab’s facilities. A chance to see the equipment being used to decipher the mysteries of plasmas—and perhaps one day to tame nuclear fusion, who knows?

  At the University of Minnesota, in Minneapolis, my presentation seemed to impress Vladimir Šverák. I have the greatest respect for this man, who understands the mysterious notion of quasi-convexity better than anyone and
who is now one of the leading authorities on Navier–Stokes regularity. His warm words were a great source of encouragement to me.

  Following my talk, at the colloquium dinner, I won over an even tougher audience: the very young, very blond, and very shy daughter of another fine mathematician teaching at Minnesota, Markus Keel. She was delighted to show off her gymnastic skills, executing forward rolls and roaring with laughter. Markus couldn’t get over the fact that his daughter was willing to play with a total stranger—she never says a word to people she doesn’t know!

  At Rutgers I presented my results once more, this time at the spring Statistical Mechanics Conference, one of two organized every year by the indefatigable Joel. It wasn’t anything like my previous talk the end of January. This time the logic was tight.

  Finally, at the IAS, I gave a lecture to an audience almost exclusively made up of young women as part of the annual Program for Women and Mathematics. They had come here in the hope of lifting the curse that has made mathematics an overwhelmingly male discipline—less so than computer science or electrical engineering, but mostly male just the same. With luck and hard work, some of them may turn out to be worthy successors of the great female pioneers who have been the wonder of mathematics for generations, the next Sofia Kovalevskayas, Emmy Noethers, Olga Oleiniks, Olga Ladyzhenskayas. The young women taking part in the program this year have been a breath of fresh air. In the evenings they can be seen walking about the grounds of the Institute in small groups, enjoying the cool evening breezes.

  Yesterday I went with Claire and the children to say our goodbyes to the golf course. I have fond memories of walking through the course on my way home at night along the path that leads from the little train station on the edge of the Princeton campus to the Institute, all alone, under a lustrous moon that transformed the sand traps into ghostly waves.… And the kids have their own memories: with great reverence they deposited their precious offering on the grass—all the lost golf balls they’d recovered since they got here six months ago! Think of it, six months gone by already!