BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Comparative Formalisation of Kneser's theorem in Isabelle/HOL and 
 Lean - Mantas Bakšys and Yaël Dillies (University of Cambridge)
DTSTART:20240201T170000Z
DTEND:20240201T180000Z
UID:TALK210160@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:We will discuss the formalisation of the Cauchy-Davenport theo
 rem and the Kneser addition theorem\, two central results in additive comb
 inatorics\, in two interactive theorem provers: Isabelle/HOL and Lean. The
  parallel formalisation in two systems allows us to highlight their differ
 ences relevant to combinatorial arguments. We will compare the design deci
 sions made in both cases and mention potential improvements. Our work has 
 been accepted into Isabelle's Archive of Formal Proofs and is currently be
 ing incorporated into Lean's mathlib. The presented work was jointly carri
 ed out by the speakers and Angeliki Koutsoukou-Argyraki.\n\nThe slides for
  the talk are available at https://mantasbaksys.github.io/slides/Kneser_Pr
 esentation_updated.pdf.
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR