This article formalizes two proofs of Arrow's impossibility theorem due to Geanakoplos and derives the Gibbard-Satterthwaite theorem as a corollary. One formalization is based on utility functions, the other one on strict partial orders.
- Nipkow, T. (2009). Social Choice Theory in HOL. Journal of Automated Reasoning, 43(3), 289–304. https://doi.org/10.1007/s10817-009-9147-4
- author's copy