BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formalising (part of) the Diagonal Ramsey Paper - Professor Lawren
 ce Paulson (University of Cambridge)
DTSTART:20240307T170000Z
DTEND:20240307T180000Z
UID:TALK210400@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:Last March\, a paper appeared on arXiv announcing a dramatic a
 dvance in Ramsey theory: an exponential reduction in the upper bound for R
 amsey numbers. Last November\, Bhavik Mehta announced that he had formalis
 ed the paper (in Lean)\, even before the referees had finished checking it
 . This talk describes a partial formalisation of the same paper within Isa
 belle. It includes a quick review of Ramsey's theorem\, an outline of the 
 paper and comments on the mathematics therein\, and some notes on the form
 alisation itself.  \n\n---\n\nWATCH ONLINE HERE: https://www.microsoft.com
 /en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 370 771 279 261 Pa
 sscode: iCo7a5
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR