University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > A computer-checked proof of the Odd Order theorem

A computer-checked proof of the Odd Order theorem

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

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.

This talk is part of the Microsoft Research Cambridge, public talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity