Formalizing May's Theorem

TL;DR

This paper formalizes May's Theorem within the Coq proof assistant, providing a mechanized proof and discussing its implications, marking the first documented formalization of this theorem.

Contribution

It introduces the first formalization and mechanization of May's Theorem using Coq, translating the theorem into formal definitions and proving it within a proof assistant.

Findings

Successfully formalized May's Theorem in Coq

Provided a detailed proof and discussion of the formalization process

Established a foundation for further mechanized proofs of social choice theorems

Abstract

This report presents a formalization of May's theorem in the proof assistant Coq. It describes how the theorem statement is first translated into Coq definitions, and how it is subsequently proved. Various aspects of the proof and related work are discussed. To the best of the author's knowledge, this project is the first documented attempt in mechanizing May's Theorem.