Papers With

← All papers
First page of 1-out-of-5 Maximin-Share Allocations Always Exist for Four Agents

1-out-of-5 Maximin-Share Allocations Always Exist for Four Agents

Christoph Schwerdtfeger

econ.TH Jul 20, 2026 · v1 cs.GT
formalization economics
Read PDF arXiv abstract
TL;DR
The four-agent 1-out-of-5 maximin-share existence theorem is machine-checked in Lean 4 against Mathlib, sorry-free.
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.
Problem

For fair division of indivisible goods among four agents with additive valuations, it was known that exact maximin-share (MMS) allocations can fail and that 1-out-of-6 MMS allocations always exist, leaving the denominator 5 case unresolved.

Approach

Instances are normalized so each MMS witness cell has value one, and goods are placed on a common rank scale. A restricted Lone Divider procedure requires every allocated bundle to contain exactly one of the four highest-ranked goods. A balanced-residual partition lemma ensures removing rejected bundles leaves enough unit-valued balanced bundles, with a central 2+2 case handled by three repairing unit bundles. The full theorem is formalized in Lean 4.

Results

Every finite four-agent instance admits a complete 1-out-of-5 MMS allocation, showing denominator five is sufficient and best possible, thus completely characterizing the four-agent case. The Lean 4 development is sorry-free, uses no project-specific axioms, and relies only on propext, Classical.choice, and Quot.sound.