Core Existence in Approval-Based Committee Elections with up to Seven Voter Types
Patrick Becker, Matthias Greger, Dominik Peters
cs.GT
May 7, 2026 · v2
TL;DR
The core existence result for up to five voters was formalized in Lean 4 by an autonomous AI agent (GPT-5.5 in Codex) in about 10 hours.
Abstract
In an approval-based committee election, the task is to select a committee of up to $k$ candidates from a set of $m$ candidates based on the preferences of $n$ voters, each of whom approves a subset of the candidates. A central open question is whether there always exists a committee in the core, a stability notion capturing proportional representation. We prove core non-emptiness for all approval-based committee elections with at most seven voters. The proof is based on affine monoid methods and shows that, for $n\le5$, every fractional committee admits a deterministic rounding to an integral committee that preserves each voter's utility up to floors. This no longer applies for larger $n$. However, for $n \in \{6,7\}$, we show that a Lindahl equilibrium can be adapted and rounded to obtain a core committee. For $n \le 5$, we further provide a polynomial-time algorithm for computing a committee in the core. Our arguments work for the weighted voter setting, which implies core existence for instances with up to seven distinct approval sets. We conclude by providing examples where our methods fail for more general models with additive valuations, non-unit candidate costs, or the related Droop core.
Problem
It is a central open question whether every approval-based committee election has a committee in the core, a stability notion that captures proportional representation. Previously, core existence was known only for bounded committee size (k ≤ 8) or few candidates (m ≤ 15).
Approach
Elections are encoded as an affine monoid of instance-utility pairs. Normality of this monoid, checked with Normaliz, implies that for n ≤ 5 every fractional committee can be rounded deterministically while preserving each voter's utility up to floors. For n ∈ {6,7}, where normality fails, a Lindahl equilibrium is adapted and rounded instead. The existence result for n ≤ 5 was also formalized in Lean 4 by an AI agent.
Results
The core is non-empty for every weighted instance with at most seven voters, and hence for any instance with at most seven distinct approval sets. A polynomial-time algorithm computes a Pareto-optimal core committee for n ≤ 5. Counterexamples show the monoid method fails for non-unit costs, additive valuations and the Droop core, already at n = 3.
