BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formalising Turán's Graph Theorem in Isabelle/HOL - Nils Lauerman
 n (INRIA)
DTSTART:20230302T170000Z
DTEND:20230302T180000Z
UID:TALK194188@talks.cam.ac.uk
CONTACT:Angeliki Koutsoukou-Argyraki
DESCRIPTION:In 1941\, Paul Turán discovered that any undirected\, simple 
 graph with n vertices that does not contain a p-clique\, contains at most 
 (1-1/(p-1))n^2/2 edges. Turán’s graph theorem is considered to be a fun
 damental result in graph theory and the origin of the field of extremal gr
 aph theory. In my formalisation of Turán’s graph theorem in Isabelle/HO
 L\, I have first directly adapted Turán's original proof. Then\, I discov
 ered a seemingly small change to the textbook proof on paper which signifi
 cantly decreases the size of the formalisation and leads to an arguably mo
 re beautiful proof.\n\nWATCH ONLINE HERE : https://www.microsoft.com/en-gb
 /microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 379 992 884 209 Passcode
 : TYR8 Sh
LOCATION:  Centre for Mathematical Sciences MR12\, CMS
END:VEVENT
END:VCALENDAR