Big news: a proof of the Feit-Thompson Theorem (also known as the “odd order theorem”) has been completely formalized and verified by a computer, using the Coq proof assistant!
Wait, what? Huh? you’re probably thinking. Well, let me unpack that a bit for you. This is big news in my corner of the world, but you should be impressed, too. Here’s why.
The Feit-Thompson Theorem states that “every finite group of odd order is solvable”. Perhaps you’ve heard of the concept of a group before: group theory is the branch of mathematics that studies symmetry. A group is just a set of elements with certain simple operations that satisfy certain simple laws. I should write about it soon—but for now all you need to know is that the simplicity of the definition hides a rich and complex theory which is still being explored. A finite group of odd order is just a group with an odd, finite number of elements. Saying a group is solvable is much more technical; the term “solvable” is used because solvable groups have to do with “solvable” polynomials. In particular, the concept of solvable groups played an important role in the proof that there is no quintic formula. (Another thing I may write about… you are no doubt familiar with the quadratic formula for solving second-degree equations, and there are likewise cubic and quartic formulas for solving third- and fourth-degree equations, though they are much too complicated to make anyone memorize, but there is not a quintic formula!)
So, a simple theorem about odd groups. What’s the big deal? Well, the big deal is that the original proof (in 1963) by Walter Feit and John Griggs Thompson was 255 pages long!! And they were even leaving out a lot of details! Since then, others have expanded the proof and filled in some details, resulting in two entire books. That’s right, two books for just one proof. And no one has found any significant ways to make the proof shorter, either. This has turned out to be a very important theorem, but how on earth can anyone be sure that every single detail in hundreds of pages of proof are all correct? What if there is a small mistake which makes the whole thing invalid?
Enter Coq (it means “rooster” in French). It is a proof assistant: you write down formal specifications of mathematical theorems using a special programming language, and then (using another special programming language) you try to formally “convince” Coq that the theorem is true. If Coq accepts your proof, then (in a very strong sense) it must be correct. It’s amazingly cool (and yet another thing I should write about!).
So, Georges Gonthier is a researcher at Microsoft Research in Cambridge, England. He and a team of several other researchers recently finished a complete formalization of Feit and Thompson’s proof in Coq. It consists of over four thousand sub-theorems, proved using 170,000 lines of code!! You can actually see the whole thing here. This is remarkable for several reasons. First, one. hundred. seventy. thousand. lines of code! It took Georges and his team six years to finish the proof. This is quite an accomplishment in and of itself. Second, it’s remarkable that in fact, Feit and Thompson’s original proof was really correct! Coq says it’s correct, and Coq is much pickier about details than any human could ever be. It means that in all those 255 pages, Feit and Thompson really didn’t make any mistakes—at least, not any important mistakes, of course there are probably typos and things like that.
So, why did they do it? The point isn’t really that Feit and Thompson’s proof needed checking—no one really doubted it was correct before. The point is to develop new techniques and push the boundaries of what is possible in formalizing mathematics using computers. And they certainly accomplished that! Note that this same team previously formalized a proof of the four-color theorem—something else I may write about.
Anyway, there were a lot of things in there that I “might write more about”—leave a comment if you would like to see me write about one of them in particular!
The Math Less Traveled 
Very well written! It made me curious about that programming language they were using. I would love to read about the four-color theorem. It’s something I vaguely remember from my student days. So it shouldn’t be too hard to follow!
Hi –
I would be very interested in being told what is the significance of the central limit theorem.
Specifically, are there any inferences which can be made by the central limit theorem being true?
For example, in physics, when new a theory is proposed about the universe, the particle accelerator boys may be told to start looking for a new particle to verify the theory. In the case of the central limit theorem, can a good understanding of it make me a better poker player ? Does the central limit theorem explain any common physical phenomena.
My field at present is low-frequency noise, specifically 1/f noise, for which we have no good theories to explain why this happens, other than common sense. An example of 1/f noise is an occasional long line at the grocery store. Could the central limit theorem be used to explain such long lines as a function of time ? This would be very interesting to me.
thanks –
bryce halpern
Hi Bryce, unfortunately I really don’t know much at all about the central limit theorem. Statistics is not my strong area!
Brent –
Thanks for replying.
Bryce
With respect to computers solving math problems – I am assuming that the computer in question had a great deal of help from the mathematicians, and the computer did the ‘dirty work’. I am an engineer, and today computers do about 90% of the engineering work period. Engineers should nit be allowed in a union because they design and build their replacements !
There was a time, when IBM first released Big Blue, that a computer could not defeat a chess master like Gary Kasparov. I don’t know if this is still true.
Question: Brent do you feel threatened by the capability of modern computers, which accept symbolic mathematical expressions and then solve or prove them ?
Yes, indeed the mathematicians did most of the real work of writing down the theorems and encoding the proofs in Coq’s special language—though Coq can automatically discover proofs for “sufficiently simple” theorems, the vast majority of interesting theorems do not fall into that category, and there are good reasons for thinking that will always be true. This is a very different domain than, say, chess—not just more difficult but fundamentally different.
Big Blue’s successor, Deep Blue, beat Kasparov in 1997. I think the best chess-playing programs these days can beat grandmasters just running on a PC!
And no, I do not feel threatened by the capability of modern computers at all! The joy of doing mathematics is in thinking of new ideas and new connections and communicating them. It is not just about solving problems that have already been posed formally. Right now computers are nowhere near being able to do that sort of thing — but even if they are able to someday, then I will have fun communicating and exploring mathematics with them.
Pingback: A computer-checked proof of the odd order theorem « Guzman's Mathematics Weblog
Is it just me, or COQ programming looks like PROLOG?
It’s not actually all that similar. In any case Coq has powerful facilities for adding user-defined syntax, so in some sense it can look like whatever you want it to look like!
Pingback: What I Do, Part 1: Programming languages | The Math Less Traveled