Abstract

The Odd Order theorem states that all finite groups of odd order are solvable. Due to Feit and Thompson, this very important and useful result in Group Theory is also historically significant because it initiated the large collective effort that lead to the full classification of finite simple groups twenty years later. It is also one of the first proofs to be questioned by prominent mathematicians because of its sheer length (255 pages) and complexity.

These qualities make the Odd Order theorem a prime example for demonstrating the applicability of computer theorem proving to graduate and research-level mathematics.

Six years we set out to do just this, using the Coq system, and last September we succeeded.

As the Feit-Thompson proof draws on an extensive set of results spanning most of undergraduate algebra and graduate finite group theory, most of our work consisted of developing a substantial library of mathematical results covering summations, algebra, linear spaces, groups, group morphisms, characters, algebraic numbers, finite fields, etc.

This talk will give a broad survey of the proof and the techniques used to conquer its formalization, in particular the component-based design of the supporting library, and the ssreflect formal proof language.