Comparative Formalisation of Kneser's theorem in Isabelle/HOL and Lean

Add to your list(s) Download to your calendar using vCal

• Mantas Bakšys and Yaël Dillies (University of Cambridge)
• Thursday 01 February 2024, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

We will discuss the formalisation of the Cauchy-Davenport theorem and the Kneser addition theorem, two central results in additive combinatorics, in two interactive theorem provers: Isabelle/HOL and Lean. The parallel formalisation in two systems allows us to highlight their differences relevant to combinatorial arguments. We will compare the design decisions made in both cases and mention potential improvements. Our work has been accepted into Isabelle’s Archive of Formal Proofs and is currently being incorporated into Lean’s mathlib. The presented work was jointly carried out by the speakers and Angeliki Koutsoukou-Argyraki.

The slides for the talk are available at https://mantasbaksys.github.io/slides/Kneser_Presentation_updated.pdf.

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.