Voting Theory in the Lean Theorem Prover

Wesley H. Holliday, Chase Norman, Eric Pacuit

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 SA…