Voting Theory in the Lean Theorem Prover

TL;DR

This paper presents a framework for formalizing voting theory in the Lean theorem prover, enabling verification of various voting properties and theorems, bridging logic and social choice with computer-aided proof methods.

Contribution

It introduces a novel formalization of voting theory in Lean, covering a range of results from impossibility theorems to properties of specific voting methods.

Findings

Verified properties of voting methods such as Condorcet consistency

Formalized voting axioms involving candidate and voter changes

Developed a variable-election formalization using dependent types

Abstract

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.