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!