{"id":"palomar/PALOMAR-2026-09-01-000011","url":"https://github.com/roos-j/lean-booleanfun/tree/62125550b3dbaca60028e266be19397c2ef027ee","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-01-000011-v1.json","repo":"https://github.com/roos-j/lean-booleanfun","tags":["cs.DM","msc:68R01","social-choice","arrow-theorem","lean","boolean-functions"],"score":0,"title":"Arrow's theorem via Fourier analysis","trust":"high","domain":"cs.DM","source":"palomar","authors":["Joris Roos"],"reviews":0,"subject":"cs.DM","summary":"This is a formalization in Lean 4 of Arrow's theorem for three-candidate elections as stated in Ryan O'Donnell's book \"Analysis of Boolean Functions\", Sec. 2.5, with a single voting rule applied to every pairwise election. The theorem states that every unanimous voting rule that always admits a Condorcet winner must be a dictatorship, i.e. there must exist a voter that alone determines the outcome. Here voting rules are encoded by Boolean-valued functions on the Hamming cube. The proof follows the exposition given there, which is based on Gil Kalai's Fourier-analytic argument using the…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-09-01","reactions":{},"formalized":true,"formalizes":[{"title":"Analysis of Boolean Functions","identifier":"doi:10.1017/CBO9781139814782","relationship":"formalizes"}]}