Tobias Nipkow has written an article about mechanising some recent proofs of Arrow's Theorem and Gibbard-Satterthwaite in Isabelle, and has kindly cited my clumsy attempts at similar things. In an attempt at differentiation I have polished up my proofs from Sen's magnum opus and added one of May's Theorem. As one might expect from a positive result in social choice theory there are endless reworkings of the original conditions in the literature since 1952, and I am not entirely sure what the state of the art is.
The proof itself is fairly straightfoward, although Sen makes an
uncharacteristic slip by unnecessarily arguing by contradiction in his
proof of my anonymous_neutral_indifference
. When I'm next
bored and idle I'll see if that makes any difference in the bigger
scheme of things.
The hope is to get all of this into the Archive of Formal Proofs and obtain some feedback on the nastier parts of the mechanisation.
An interested soul has written a great overview of May's life work.