A Note on EFX Inapproximability for Chores
Vasilis Christoforidis
cs.GT
May 20, 2026 · v2
TL;DR
The main 255-agent EFX inapproximability construction and the three-agent results are formalized in Lean 4 with Mathlib, produced with help from the Aristotle system.
Abstract
We study the approximability of envy-free up to any item (EFX) allocations for indivisible chores under complement-free cost functions. Our main result is an instance with $255$ agents and $764$ chores with binary XOS cost functions, in which no $α$-EFX allocation exists for any $1\leα<2$. The construction is based on a combinatorial expansion property of binary labels, obtained using Sidon sets and Reed–Solomon codes. We formalize the main result in Lean 4. We also study the special case of three agents. We construct a six-chore instance with monotone subadditive cost functions for which no $α$-EFX allocation exists for any $1\leα< 2^{1/3}$, and a six-chore instance with monotone submodular cost functions for which no $α$-EFX allocation exists for any $1\leα<20/19$. These constructions are obtained by refining the original counterexample of \cite{CS24}.
Problem
How large an approximation gap can explicit constructions show for the non-existence of envy-free up to any item (EFX) allocations of indivisible chores under complement-free cost functions?
Approach
Each chore is labeled with a binary word, one coordinate per agent, and each agent's cost is the maximum of the zero-bit count and the one-bit count in its coordinate. A pair expansion property of the labels, built from Sidon sets (via x↦(x,x^3)) and Reed–Solomon codes, forces every α-EFX candidate allocation into a contradiction. For three agents, the counterexample of [CS24] is refined and an ordinal compression lemma converts its costs into subadditive ones. The main result is formalized in Lean 4 and checked with Mathlib, with Aristotle used to generate the formalization.
Results
An instance with 255 agents and 764 chores and binary XOS costs admits no α-EFX allocation for any 1≤α<2. For three agents, six-chore instances rule out α-EFX for α<2^{1/3} under subadditive costs and for α<20/19 under submodular costs.
