University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Comparative Formalisation of Kneser's theorem in Isabelle/HOL and Lean

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

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

Download to your calendar using vCal

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:

Note that ex-directory lists are not shown.

Other lists

Main Lecture Department of Engineering, James Dyson Building Seminar Room Winstanley Lecture Hall (http://www.acs-cam.org.uk/CRSS/venue/venue_CRSS.html)

Other talks

The Inaccessible Game Group Work Title to be confirmed Morning Tea and Coffee CSaP Annual Cleevely Lecture 2026 TBC
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity