BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formalising Erdős and Larson: Ordinal Partition Theory - Professo
 r Lawrence C. Paulson FRS (University of Cambridge)
DTSTART:20230525T160000Z
DTEND:20230525T170000Z
UID:TALK196744@talks.cam.ac.uk
CONTACT:Angeliki Koutsoukou-Argyraki
DESCRIPTION:A long-standing question in mathematics is the relevance of fo
 rmalisation to practice. Rising awareness of fallibility among mathematici
 ans suggests formalisation as a remedy. But are today's proof assistants u
 p to the task? And what is the right formalism?\n\nA wide variety of mathe
 matical topics have been formalised in simple type theory using Isabelle/H
 OL. The partition calculus was introduced by Erdős and R. Rado in 1956 as
  the study of “analogues and extensions of Ramsey’s theorem”. Highly
  technical results were obtained by Erdös-Milner\, Specker and Larson (am
 ong many others) for the case of ordinal partition relations\, which is co
 ncerned with countable ordinals and order types. Much of this material was
  formalised recently\, with the assistance of Džamonja and Koutsoukou-Arg
 yraki. \n\nSome highlights of this work will be presented along with gener
 al observations about role of type theory in the formalisation of mathemat
 ics.
LOCATION:  Centre for Mathematical Sciences MR12\, CMS
END:VEVENT
END:VCALENDAR