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

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.