Alkassar, Fouz & Mehlhorn: Complete EFX allocations exist for 4 agents, 9 goods

In a new arXiv preprint (2608.08590), Eyad Alkassar, Mahmoud Fouz, and Kurt Mehlhorn establish that complete EFX allocations always exist for four agents with additive valuations and up to nine indivisible goods (m = 9 = n + 5). EFX, or envy-free up to any good, requires that no agent envies another after removing any single good from the other's bundle. The prior known bound for four agents was m ≤ n + 3 = 7, making this a significant jump. The result is the strongest unconditional guarantee to date for complete fair division of indivisible goods.

The proof strategy is notable for its hybrid approach. The authors partition the valuation polytope into smaller cells; for each cell, they construct a finite family of allocations that provably contains an EFX allocation for every valuation in that cell. Each covering check is reduced to a quantifier-free linear-arithmetic unsatisfiability query, independently re-verified by a separate certifier implementation and per-clause evidence. The m = 8 case is recovered both by an earlier independent project and as a one-paragraph padding corollary of the m = 9 theorem. The authors also offer a structural explanation for why larger cases are hard: near-identical valuations admit only ~0.14% of all 4^9 allocations that are EFX, and certain valuation pairs force opposite mandatory allocation structures.