BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Microsoft Research Cambridge\, public talks
SUMMARY:A computer-checked proof of the Odd Order theorem
- Georges Gonthier\, MSRC
DTSTART;TZID=Europe/London:20121108T140000
DTEND;TZID=Europe/London:20121108T150000
UID:TALK41078AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/41078
DESCRIPTION:The Odd Order theorem states that all finite group
s of odd order are solvable. Due to Feit and Thomp
son\, this very important and useful result in Gro
up Theory is also historically significant because
it initiated the large collective effort that lea
d to the full classification of finite simple grou
ps twenty years later. It is also one of the first
proofs to be questioned by prominent mathematicia
ns because of its sheer length (255 pages) and com
plexity.\n\nThese qualities make the Odd Order the
orem a prime example for demonstrating the applica
bility of computer theorem proving to graduate and
research-level mathematics.\n\nSix years we set o
ut to do just this\, using the Coq system\, and la
st September we succeeded.\n\nAs the Feit-Thompson
proof draws on an extensive set of results spanni
ng most of undergraduate algebra and graduate fini
te group theory\, most of our work consisted of de
veloping a substantial library of mathematical res
ults covering summations\, algebra\, linear spaces
\, groups\, group morphisms\, characters\, algebra
ic numbers\, finite fields\, etc.\n\nThis talk wil
l give a broad survey of the proof and the techniq
ues used to conquer its formalization\, in particu
lar the component-based design of the supporting l
ibrary\, and the ssreflect formal proof language.\
n
LOCATION:Large lecture theatre\, Microsoft Research Ltd\, 7
J J Thomson Avenue (Off Madingley Road)\, Cambrid
ge
CONTACT:Microsoft Research Cambridge Talks Admins
END:VEVENT
END:VCALENDAR