This repository contains a formalization of the theory of approval-based committee voting (ABC voting) in the Lean 4 proof assistant. It includes definitions and proofs of various voting rules, axioms, and their relationships.
Duality/vendors the Lean sources from https://github.com/madvorak/duality at base commitb0787cb7a97bc7bc27e230e7dc1f06a62608ced7, with local compatibility edits for this repository's Lean toolchain. It is used by the Dong-Lederer rational cone development viaDuality.FarkasBasic.
- JR, PJR, EJR, EJR+, FJR, FPJR
- Priceability, weak and Lindahl priceability
- Core, disjoint core, sub-core
- Pareto-optimality
- Strategyproofness
- Committee monotonicity
- Implications between axioms (e.g., Core implies FJR, EJR+ implies EJR, Priceability implies PJR+)
- Proportional Approval Voting (PAV)
- satisfies EJR+
- satisfies disjoint core
- satisfies core up to k=7
- may fail core for k=8
- fails priceability
- satisfies Pareto-optimality
- Method of Equal Shares (MES), uncompleted
- satisfies EJR+
- Sequential Phragmén
- satisfies priceability, therefore PJR+
- satisfies committee monotonicity
- Greedy Cohesive Rule (GCR)
- satisfies FJR, therefore FJR always exists
- Peters' impossibility: No resolute ABC rule can satisfy strategyproofness, weak efficiency, and proportionality.
- Kluiving–de Vries–Vrijbergen–Boixel–Endriss impossibility: Analog of Peters' impossibility for irresolute rules.
- Formalize various counterexamples (MES failing core; Phragmen failing EJR, PO-failures for MES and Phragmen)
- GJCR?
- Stuff from Janson (e.g. monotonicity properties)
- perhaps: PAV intersects core for k = 8
- Proportionality degree (definition, EJR => 1/2, l-1 => EJR, extreme stretch goal: prop degree of Phragmen, and seqPav results)
- CC and utilitarian approximations?
- Approximations to the core, disjoint core => 2-utility approximation, extreme stretch goal: show 32-Kamesh result
- Peters-Skowron welfarism impossibilities, Pigou-Dalton lower bound on core approximation
- log k core approximation by MES