  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.
