19 February 2026, Computational Social Choice Seminar, Patrick Lederer

In rank aggregation, the goal is to combine multiple input rankings into a single output ranking. In this paper, we analyze rank aggregation methods, so-called social welfare functions (SWFs), with respect to strategyproofness, which requires that no agent can misreport his ranking to obtain an output ranking that is closer to his true ranking in terms of the Kemeny distance. As our main result, we show that no anonymous SWF satisfies unanimity and strategyproofness if there are at least four alternatives. This result is proven by SAT solving, a computer-aided theorem proving technique, and verified by Isabelle, a highly trustworthy interactive proof assistant. Moreover, we show by hand that strategyproofness is incompatible with majority consistency, a variant of Condorcet-consistency for SWFs. Lastly, we demonstrate for two large classes of SWFs that all SWFs within these classes have a high incentive ratio and are thus severely manipulable. This is joint work with Manuel Eberl.