Birth of a Theorem: A Mathematical Adventure (30 page)

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.