SocialChoiceLean

A Lean 4 formalization of single-winner voting theory, including classical impossibility theorems and axiomatic properties of voting rules.

This library formalizes key results in social choice theory, where:

• Input: Preference profiles (each voter submits a complete linear ordering over candidates)
• Output: A set of tied winners (nonempty subset of candidates)

The formalization covers foundational definitions, axiomatic properties of voting rules, specific voting rule implementations, and several landmark impossibility theorems.

This package is a "vibe-proving" effort; the code is written mostly by by gpt-5.2, gpt-5.2-codex, and gpt-5.1-codex-max, under the supervision of Dominik Peters, with occasional input from Claude Opus 4.5 and Gemini 3 Flash.

Theorems about the Split Cycle rule were translated from the Formalized-Voting lean3 package (https://github.com/chasenorman/Formalized-Voting) described in the paper "Voting Theory in the Lean Theorem Prover" by Wesley H. Holliday, Chase Norman, and Eric Pacuit.

This project requires Lean 4 and Mathlib. To build:

lake exe cache get   # Download Mathlib cache
lake build

SocialChoice/
├── Profile.lean              # Core definitions: profiles, preferences, voting rules
├── Meta.lean                 # Meta-level predicates and custom attributes
├── Rank.lean                 # Ranking and position utilities
├── Margin.lean               # Pairwise margin calculations
├── Cycles.lean               # Cycle detection in preference relations
├── ListBallot.lean           # Computational ballot infrastructure
├── Examples.lean             # Concrete profile examples
├── Axioms/                   # Axiomatic properties of voting rules
├── Rules/                    # Specific voting rule implementations
│   ├── ScoringRules/         # Positional scoring rules
│   ├── ScoringElimination/   # Iterated elimination rules
│   ├── SplitCycle/           # Split Cycle rule
│   └── Minimax/              # Minimax rule
└── Impossibilities/          # Impossibility theorems
    ├── GibbardSatterthwaite/ # Gibbard-Satterthwaite theorem
    ├── DugganSchwartz/       # Duggan-Schwartz lemmas
    └── ...                   # Other incompatibility results

structure Profile (V A : Type) [Fintype V] [Fintype A] where
  pref : V → LinearOrder A

abbrev VotingRule :=
  ∀ {V A : Type} [Fintype V] [Fintype A], Profile V A → Finset A

def IsVotingRule (f : VotingRule) : Prop :=
  ∀ {V A : Type} [Fintype V] [Fintype A] (P : Profile V A), (f P).Nonempty

Key predicates:

• Prefers P v a b: Voter v prefers a to b in profile P
• TopRank P v c: Candidate c is ranked first by voter v
• BottomRank P v c: Candidate c is ranked last by voter v
• StrictMajority S: Voter set S has more than 50% of all voters

Profile operations:

• permuteVoters: Relabel voters by a permutation
• permuteCandidates: Relabel candidates by a permutation
• addVoter: Add a voter to a profile
• unionProfiles: Combine disjoint electorates
• restrictCandidates: Restrict to a subset of candidates

def margin (P : Profile V A) (a b : A) : Int :=
  (votersPreferring P a b).card - (votersPreferring P b a).card

def margin_pos (P : Profile V A) (a b : A) : Prop :=
  0 < margin P a b

Key properties proven:

• margin_antisymmetric: margin(a,b) = -margin(b,a)
• self_margin_zero: margin(a,a) = 0
• margin_pos_asymm: margin positivity is asymmetric

The library formalizes the following axiomatic properties of voting rules:

The library provides predicates for reasoning about relationships between rules and axioms:

Custom attributes @[scAxiom] and @[scRule] tag definitions for documentation tooling.

Three variants of strategyproofness are formalized:

-- For resolute rules: no voter can benefit by misreporting
def ResoluteStrategyproofness (f : VotingRule) (_hf : Resolute f) : Prop :=
  ∀ P v ballot x y,
    f P = {x} → f (updateProfile P v ballot) = {y} → ¬ Prefers P v y x

-- For multi-winner rules (Duggan-Schwartz):
def OptimistStrategyproof (f : VotingRule) : Prop :=
  -- No voter can make their best outcome strictly better

def PessimistStrategyproof (f : VotingRule) : Prop :=
  -- No voter can make their worst outcome strictly better

Generic positional scoring rules where each position earns points:

Properties proven for scoring rules:

• Anonymity
• Neutrality
• Pareto efficiency
• Monotonicity (for strictly decreasing scores)
• Reinforcement

Iterative elimination rules with parallel-universe tie-breaking:

Theorem: IRV satisfies the Condorcet loser criterion (irv_condorcet_loser_criterion)

Split Cycle (SplitCycle/): A defeats B if margin(A,B) > 0 and there's no cycle containing A and B where all margins are at least margin(A,B). Winners are undefeated candidates.

Properties proven:

• Condorcet consistency
• Condorcet loser avoidance
• Pareto efficiency
• Monotonicity
• Reversal symmetry
• Clone independence

Minimax (Minimax/): Winner minimizes their maximum pairwise loss.

Properties proven:

• Condorcet consistency

File: Impossibilities/GibbardSatterthwaite/Main.lean

theorem gibbard_satterthwaite
    (hcardA : 3 ≤ Fintype.card A)
    (f : VotingRule)
    (hf_res : Resolute f)
    (hf_unan : Unanimity f)
    (hf_sp : ResoluteStrategyproofness f hf_res) :
    ∃ d : V, ∀ P : Profile V A, f P = {topChoice P d}

Statement: With at least 3 candidates, any resolute, unanimous, strategyproof voting rule must be dictatorial.

Proof structure (strong induction on number of voters):

• Base case (BaseCase.lean): 1 voter case
• Inductive step via voter cloning technique
  • Case 1 (InductionStepCase1.lean): Dictator in cloned rule is not the cloned voter
  • Case 2 (InductionStepCase2.lean): Dictator is the cloned voter

File: Impossibilities/CondorcetStrategyproofness.lean

theorem no_resolute_condorcet_strategyproof_3x3
    (f : VotingRule) (hf : Resolute f) :
    CondorcetConsistency f → ResoluteStrategyproofness f hf → False

Statement: With 3 voters and 3 candidates, no resolute rule can satisfy both Condorcet consistency and strategyproofness.

Proof: Explicit construction using the Condorcet cycle profile.

File: Impossibilities/CondorcetParticipation.lean

theorem no_resolute_condorcet_participation_m4_n12 :
    ¬ ∃ (f : VotingRule) (hf : Resolute f),
      CondorcetConsistency f ∧ ResoluteParticipation f hf

Statement: No resolute rule can satisfy both Condorcet consistency and participation.

Proof: Computer-aided proof using explicit 12-voter, 4-candidate profiles (following Brandt et al. 2016 / Peters 2019).

File: Impossibilities/CondorcetReinforcement.lean

theorem no_condorcet_subset_reinforcement_9
    (f : VotingRule) (hf : IsVotingRule f)
    (hcond : CondorcetConsistency f) (hsub : SubsetReinforcement f) : False

Statement: No voting rule can satisfy both Condorcet consistency and (subset) reinforcement.

Proof: Explicit construction using 9-voter, 3-candidate profiles.

File: Impossibilities/DugganSchwartz/DownMonotonicity.lean

theorem downMonotonicity_of_opt_pess_sp (f : VotingRule)
    (hf_total : IsVotingRule f)
    (hf_opt : OptimistStrategyproof f)
    (hf_pess : PessimistStrategyproof f) :
    DownMonotonicitySingleton f

Statement: Any voting rule satisfying both optimist and pessimist strategyproofness has down-monotonicity for singleton winners.

This is Lemma 2.4 from Taylor's "The Manipulability of Voting Systems" (2002).

Provides decidable ballot representations for computational verification:

structure ListBallot (n : Nat) where
  ranking : Fin n → Nat
  isPermutation : ranking.Bijective

Key operations:

• isTopOfList: Check if candidate is at top
• prefersInList: Check pairwise preference
• countPrefers: Count voters with given preference
• marginList: Compute pairwise margin

Bridge lemmas connect abstract definitions to computational ones:

• prefers_iff_prefersInList
• topRank_iff_isTopOfList
• margin_eq_marginList

Concrete profile constructions demonstrating:

• 3-voter, 3-candidate Condorcet cycle
• 3-voter, 4-candidate Condorcet winner example
• Computational verification using the decide tactic

The formalization follows results from:

• Gibbard, A. (1973). Manipulation of voting schemes: A general result. Econometrica.
• Satterthwaite, M. (1975). Strategy-proofness and Arrow's conditions. Journal of Economic Theory.
• Taylor, A.D. (2002). The manipulability of voting systems. The American Mathematical Monthly.
• Brandt, F., Geist, C., & Peters, D. (2016). Optimal bounds for the no-show paradox via SAT solving. AAMAS.
• Peters, D. (2019). Proportionality and Strategyproofness in Multiwinner Elections. DPhil thesis, Oxford.

MIT License