HEXAGONbeta

Arrow and Gibbard Satterthwaite Theorems in Lean

Primarily AI-generated textHuman understanding: some partsmath.LO — Logiccs.LO — Logic in Computer Science

Contributed by Arthur ↗, David Barros Hulak ↗, Ruy J. G. B. de Queiroz ↗

SubmitterArthur

Version 1 / Oct 01, 2026 / CC BY 4.0

Abstract

We give a source-aligned account of two Lean 4 formalizations of classical finite social-choice impossibility theorems. For a finite nonempty electorate and a finite alternative set containing three distinct alternatives, Arrow’s theorem derives dictatorship from unanimity and independence of irrelevant alternatives. Its proof expands a weakly decisive coalition from one ordered pair to all pairs, then contracts decisive coalitions to a singleton. The Gibbard–Satterthwaite development proves that every onto strategy-proof choice function on the unrestricted strict-ranking domain is dictatorial by constructing a social welfare function and applying that Arrow implementation. We explain the essential construction in full: top-two profiles define pairwise comparisons; strategy-proof monotonicity and three-top profiles establish a strict total order; predecessor counts provide injective natural-number ranks. Exact hypotheses, vendored dependencies, pinned source identities, prior formalizations, and the distinction between historical registry verification and the present source audit are recorded. The contribution is an exposition and audit of reusable formalization artifacts, not a new social-choice theorem or a claim of first formalization.

Provenance statement

The manuscript names Arthur Freitas Ramos (submitting contributor; ORCID 0009-0003-3568-0325), David Barros Hulak (0009-0002-8056-1774), and Ruy J. G. B. de Queiroz (0000-0003-1482-0977). The submitting contributor reports understanding some parts, but not all, of the work. OpenAI GPT-6.1 assisted with manuscript generation, inspection of the pinned source, exposition, source alignment, and bibliography and consistency review. Pinned formalization metadata separately records gpt-6-luna via Codex CLI for historical proof engineering. The exact Palomar records report historical verification on September 25, 2026. No fresh Lean build or fresh kernel or axiom audit was performed for this manuscript. The Gibbard-Satterthwaite development vendors byte-identical Arrow modules from the pinned Arrow source, so these linked artifacts are treated together in one paper. Arthur Freitas Ramos is the repository author and responsible maintainer; source attribution is separate from the three-author manuscript byline. This is an exposition and source audit of classical results and existing formal artifacts, without a claim of mathematical novelty or formalization priority.
FormalizationsPalomarPalomar

Tools used

OpenAI
ChatGPTVersion GPT 6.1 (manuscript)
OpenAI
CodexVersion gpt-6-luna (historical proof engineering)
Lean
LeanVersion 4.35.0-rc2 (registered artifacts)

References

  1. Arrow, Kenneth J. A Difficulty in the Concept of Social Welfare. Journal of Political Economy, vol. 58, no. 4, pp. 328–346. 1950. \urlhttps://doi.org/10.1086/256963DOI
  2. Gibbard, Allan. Manipulation of Voting Schemes: A General Result. Econometrica, vol. 41, no. 4, pp. 587–601. 1973. \urlhttps://doi.org/10.2307/1914083DOI
  3. Nipkow, Tobias. Social Choice Theory in HOL: Arrow and Gibbard–Satterthwaite. Journal of Automated Reasoning, vol. 43, no. 3, pp. 289–304. 2009. \urlhttps://doi.org/10.1007/s10817-009-9147-4DOI
  4. Palomar Registry. Arrow's impossibility theorem (general finite version). 2026. PALOMAR-2026-09-25-000024, version 1. Registered September 25, 2026 \urlhttps://palomar-registry.org/entry?id=PALOMAR-2026-09-25-000024&version=1link
  5. Palomar Registry. Gibbard–Satterthwaite theorem (strategy-proof social choice). 2026. PALOMAR-2026-09-25-000028, version 1. Registered September 25, 2026 \urlhttps://palomar-registry.org/entry?id=PALOMAR-2026-09-25-000028&version=1link
  6. Peters, Dominik. SocialChoiceLean: Gibbard–Satterthwaite in Lean. 2026. Public repository snapshot, July 21, 2026. Consulted as source; not rebuilt for this manuscript \urlhttps://github.com/DominikPeters/SocialChoiceLean/tree/94a4c650b6a3ef14df801a613c3b46169dbd754dlink
  7. Ramos, Arthur Freitas. Arrow's Impossibility Theorem in Lean 4. 2026. Pinned repository snapshot. BSD-3-Clause \urlhttps://github.com/Arthur742Ramos/arrow-impossibility-lean/tree/4f405d27d0b244574bbee5d3d79bae0c66bda16elink
  8. Ramos, Arthur Freitas. Gibbard–Satterthwaite Theorem in Lean 4. 2026. Pinned repository snapshot. BSD-3-Clause \urlhttps://github.com/Arthur742Ramos/gibbard-satterthwaite-lean/tree/8398e65a99cd3d5e973c64963c4bab8c0491947clink
  9. Roos, Joris. Arrow's theorem via Fourier analysis. 2026. Palomar record PALOMAR-2026-09-01-000011, version 1 \urlhttps://palomar-registry.org/entry?id=PALOMAR-2026-09-01-000011&version=1link
  10. Satterthwaite, Mark A. Strategy-proofness and Arrow's conditions: Existence and correspondence theorems for voting procedures and social welfare functions. Journal of Economic Theory, vol. 10, no. 2, pp. 187–217. 1975. \urlhttps://doi.org/10.1016/0022-0531(75)90050-2DOI

Version history

  1. v1Initial depositCurrentOct 01, 2026