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:Formalisation of mathematics with interactive theo
rem provers
SUMMARY:Formalising Erdős and Larson: Ordinal Partition Th
eory - Professor Lawrence C. Paulson FRS (Universi
ty of Cambridge)
DTSTART;TZID=Europe/London:20230525T170000
DTEND;TZID=Europe/London:20230525T180000
UID:TALK196744AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/196744
DESCRIPTION:A long-standing question in mathematics is the rel
evance of formalisation to practice. Rising awaren
ess of fallibility among mathematicians suggests f
ormalisation as a remedy. But are today's proof as
sistants up to the task? And what is the right for
malism?\n\nA wide variety of mathematical topics h
ave been formalised in simple type theory using Is
abelle/HOL. The partition calculus was introduced
by Erdős and R. Rado in 1956 as the study of “anal
ogues and extensions of Ramsey’s theorem”. Highly
technical results were obtained by Erdös-Milner\,
Specker and Larson (among many others) for the cas
e of ordinal partition relations\, which is concer
ned with countable ordinals and order types. Much
of this material was formalised recently\, with th
e assistance of Džamonja and Koutsoukou-Argyraki.
\n\nSome highlights of this work will be presented
along with general observations about role of typ
e theory in the formalisation of mathematics.
LOCATION: Centre for Mathematical Sciences MR12\, CMS
CONTACT:Angeliki Koutsoukou-Argyraki
END:VEVENT
END:VCALENDAR