Verifying Randomised Social Choice

by Manuel Eberl

In: Proceedings of FroCoS 2019

Best Paper by a Junior Researcher




This work describes the formalisation of a recent result from Randomised Social Choice Theory in Isabelle/HOL. The original result had been obtained through the use of linear programming, an unverified Java program, and SMT solvers; at the time that the formalisation effort began, no human-readable proof was available. Thus, the formalisation with Isabelle eventually served as both independent rigorous confirmation of the original result and led to human-readable proofs both in Isabelle and on paper.

This presentation focuses on the process of the formalisation itself, the domain-specific tooling that was developed for it in Isabelle, and how the structured human-readable proof was constructed from the SMT proof. It also briefly discusses how the formalisation uncovered a serious flaw in a second peer-reviewed publication.

Download preprint PDF (452 KiB)


author="Eberl, Manuel",
title="Verifying Randomised Social Choice",
booktitle="Frontiers of Combining Systems"

Download BibTeX (153 Bytes)