  There is a long tradition of fruitful interaction between logic and social
choice theory. In recent years, much of this interaction has focused on
computer-aided methods such as SAT solving and interactive theorem proving. In
this paper, we report on the development of a framework for formalizing voting
theory in the Lean theorem prover, which we have applied to verify properties
of a recently studied voting method. While previous applications of interactive
theorem proving to social choice (using Isabelle/HOL and Mizar) have focused on
the verification of impossibility theorems, we aim to cover a variety of
results ranging from impossibility theorems to the verification of properties
of specific voting methods (e.g., Condorcet consistency, independence of
clones, etc.). In order to formalize voting theoretic axioms concerning adding
or removing candidates and voters, we work in a variable-election setting whose
formalization makes use of dependent types in Lean.
