COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

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 theoremAdd to your list(s) Download to your calendar using vCal - Georges Gonthier, MSRC
- Thursday 08 November 2012, 14:00-15:00
- Large lecture theatre, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge.
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. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Cambridge Big Data
- Cambridge University Engineering Department Talks
- Centre for Smart Infrastructure & Construction
- Featured lists
- Guy Emerson's list
- Large lecture theatre, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge
- Methodology in design research
- Microsoft Research Cambridge, public talks
- PMRFPS's
- School of Technology
- ndk22's list
- rp587
Note that ex-directory lists are not shown. |
## Other listsPerspectives on Inclusive and Special Education The Cambridge University City Seminar at CRASSH Extragalactic Gathering## Other talksMachine Learning for Sounds Compact Rank Models and Optimization The Fyodorov-Bouchaud conjecture and Liouville conformal field theory Stop. Think. Click. How satellite imagery is transforming conservation science A V HILL LECTURE - The cortex and the hand of the primate: a special relationship |