skip to content

Department of Computer Science and Technology

Date: 
Thursday, 1 February, 2024 - 17:00 to 18:00
Speaker: 
Mantas Bakšys and Yaël Dillies (University of Cambridge)
Venue: 
MR14 Centre for Mathematical Sciences

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 is currently being incorporated into the respective mathematical libraries of each system.

Seminar series: 
Formalisation of mathematics with interactive theorem provers

Upcoming seminars