Sites Inria

Version française

Computer-assisted proof

Françoise Breton - 22/11/2012

A major success for computer-assisted proof

© Inria / Photo Kaksonen

Six years after the computer-assisted proof of the four colour theorem, Georges Gonthier and his team have successfully proven the far more complex Feit-Thompson theorem, a central theorem in group theory and group classification. This is a significant step forward for mathematicians, who are increasingly utilising computer-assisted proof. Moreover, it is a success for computer science, which as a result of this endeavour has shown its ability to deploy advanced tools and techniques to codify mathematics.

Six years after the computer-assisted proof of the four colour theorem, Georges Gonthier and his team have successfully proven the far more complex Feit-Thompson theorem, a central theorem in group theory and group classification. This is a significant step forward for mathematicians, who are increasingly utilising computer-assisted proof. Moreover, it is a success for computer science, which as a result of this endeavour has shown its ability to deploy advanced tools and techniques to codify mathematics.
Following the validation of the four colour theorem by the Coq certification software in 2005, it was the Feit-Thompson theorem's turn to come under the scrutiny of computer-assisted proof. However, the difficulty of the task in these two cases was worlds apart. Whereas the four colour theorem only uses elementary combinatorial mathematics, the Feit-Thompson theorem utilises virtually the length and breadth of the mathematics world. It is also longer, with 250 pages of proof, and the stakes were far higher, with applications in numerous fields of modern science, from quantum mechanics to cryptography and crystallography.

Successfully demonstrating that this proof is correct and complete was therefore a huge undertaking that Georges Gonthier and his team, made up of Laurent Théry, Laurence Rideau, Assia Mahboubi, Enrico Tassi and many others, took six years to conclude. The goal was to get the computer to "understand" the proof, and for that to happen it had to be "taught" all of the mathematics it would need: theorems, proofs, etc. It also had to be taught how to use them, a skill that only becomes apparent in the notations written in the exercise sections of textbooks. The main difficulty lay in codifying this operational part. The researchers were aided in this task by their training as computer scientists with experience using languages that can describe the procedures used, as well as the hidden rules that they identified behind the mathematical notations. As such, one line of mathematics can correspond to implicit content running to two pages in length!

The outcome was an impressive mathematical computer library and a richer Coq toolbox and environment. In the process, the researchers developed a language beyond Coq that describes complicated proofs. The proof also enabled the certification software's capabilities to be tested. It takes 1 hour 40 minutes to compile the 170,000 lines of the proof.

The theorem that founded modern algebra

The Feit-Thompson theorem is the cornerstone of modern group theory and therefore of the classification of simple groups, which is itself the cornerstone of modern algebra. Group theory studies reversible operations, something that quickly becomes complicated as the number of dimensions increases. It has applications in a huge variety of fields, the historically oldest of which is crystallography: group theory is used to interpret the interferences caused when a crystal is lit up by X-rays in order to identify the crystal's structure. In the consumer domain, group theory is behind puzzles such as Rubik's Cube in which each move is reversible.

Mathematical research into groups progressed during the middle of the 20th century, when it became apparent that they were very useful. Mathematicians wanted to study their properties by using a method consisting of factorising groups, i.e. breaking them down into elementary (or simple) group factors in a similar way to integers broken down into factors of prime numbers (30=2x3x5). This method allows the analysis of properties to be restricted to the analysis of simple groups, which can be systematically conducted using a classification that lists all of the possible forms of simple groups (3 generic types and 26 exceptions). In 1955, Brauer demonstrated that it is possible to classify a group by studying its involutions, although this technique does not work for groups of uneven order. This is where the work by Feit and Thompson came in. By showing that uneven groups are solvable, it paved the way for the study of even groups. They also came up with entirely new methods and were behind a change of perspective in mathematics. The publication of the theorem in 1963 came in the form of a 250-page article, which was unprecedented at a time when the longest mathematical elegant proofs were no more than 20 pages long. Indeed, this fuelled doubts about the reliability of the work. Meanwhile, the classification of simple groups of even order, which continued until 2003, ran to 10,000 pages.

Keywords: Inria Saclay - Île-de-France Georges Gonthier Inria - Microsoft Research joint laboratory Feit-Thompson theorem Proof Inria Sophia Antipolis - Méditerranée

Top