BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Big Conjectures - Thomas Hales (University of Pittsburgh)
DTSTART:20170710T090000Z
DTEND:20170710T100000Z
UID:TALK73196@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:Proof assistants have been used to verify complicated proofs s
 uch as the Kepler conjecture in discrete geometry and the odd-order theore
 m in group theory.  Can formalization technology help us to understand the
  statements of complicated conjectures such as Millennium (million-dollar)
  problems of the Clay Institute\, the geometric Langlands conjecture\, or 
 the Kelvin problem for optimal partitions of space?&nbsp\;
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR