BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A computer-checked proof of the Odd Order theorem - Georges Gonthi
 er\, MSRC
DTSTART:20121108T140000Z
DTEND:20121108T150000Z
UID:TALK41078@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:The Odd Order theorem states that all finite groups of odd ord
 er are solvable. Due to Feit and Thompson\, this very important and useful
  result in Group Theory is also historically significant because it initia
 ted the large collective effort that lead to the full classification of fi
 nite 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.\n\nThese qualities make the Odd Order theorem a
  prime example for demonstrating the applicability of computer theorem pro
 ving to graduate and research-level mathematics.\n\nSix years we set out t
 o do just this\, using the Coq system\, and last September we succeeded.\n
 \nAs 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 res
 ults covering summations\, algebra\, linear spaces\, groups\, group morphi
 sms\, characters\, algebraic numbers\, finite fields\, etc.\n\nThis talk w
 ill give a broad survey of the proof and the techniques used to conquer it
 s formalization\, in particular the component-based design of the supporti
 ng library\, and the ssreflect formal proof language.\n
LOCATION:Large lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR