1-out-of-5 Maximin-Share Allocations Always Exist for Four Agents
2026-07-20 • Computer Science and Game Theory
Computer Science and Game Theory
AI summaryⓘ
The authors study how to fairly divide items among four people so that each one feels they got a good share. They improved the best-known guarantee, showing that everyone can get at least their maximin share if the items are divided into five parts. Their main technical idea involves carefully removing certain bundles of items without ruining fairness for the rest. They also verified their main result using a computer proof assistant called Lean 4.
maximin sharefair divisionadditive valuationsbalanced-residual partitionagentbundlemachine-checked proofLean 4fair allocationcounterexample
Authors
Christoph Schwerdtfeger
Abstract
For four agents with nonnegative additive valuations, a complete 1-out-of-5 maximin-share allocation always exists, improving the previous 1-out-of-6 guarantee. Together with known exact-MMS counterexamples, this completely characterizes the four-agent case: the guarantee holds exactly for $d\geq5$. The main technical contribution is a balanced-residual partition lemma: removing rejected bundles with one of the four highest-ranked goods apiece leaves a remainder that still admits the required number of unit-valued balanced bundles. In its central $2+2$ case, three unit bundles repair two pairs of colliding high-valued goods. The theorem is machine-checked in Lean 4.