REVIEW 4 minor 6 references
1-out-of-5 Maximin-Share Allocations Always Exist for Four Agents
T0 review · 0 major / 4 minor · reviewed 2026-08-01 · deepseek-v4-flash
Pith's one-line read For four agents, a 1-out-of-5 maximin-share allocation always exists.
desk verdict A solid, self-contained proof of 1-out-of-5 MMS for four agents; the combinatorial lemma is genuinely new, and the only real caveat is that the Lean formalization isn't yet available to inspect. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The balanced residual partition lemma (Lemma 5). Anchors are the four highest-ranked goods; a bundle is balanced if it contains exactly one anchor. The lemma guarantees that after removing k<4 rejected balanced bundles, the residual goods can be repartitioned into 4−k balanced bundles of value at least one. In its crucial 2+2 occupancy pattern, two witness cells each contain two anchors, and three anchor-free unit cells provide filler; Lemma 4 (nearest-crossing split) cuts a unit cell at a crossing point so the error is at most half the largest item value, and the third cell fixes both residual shortfalls because their combined size is bounded by the least anchor value.
What would settle it
Search for a four-agent instance with no 1-out-of-5 maximin-share allocation. Since the theorem claims universal existence, a single counterexample would falsify it; an exhaustive check over small goods sets and discretized additive valuations is the natural test. More narrowly, one can test the 2+2 repair step: construct a normalized valuation with least anchor value above 1/2 and witness cells arranged as 2+2, and see whether the repair inequalities e+f≤m0 fail.
Extended reading notes
Core claim
The central claim is Theorem 1: for every finite set of goods and every profile of nonnegative additive valuations over four agents, there exists a partition of all goods among the four agents such that each agent's bundle has value at least her 1-out-of-5 maximin share. The proof establishes a stronger single-agent structural lemma — the balanced residual lemma — which says that if up to three rejected balanced bundles (each containing exactly one of the four highest-ranked goods) have been removed, the remaining goods can always be repartitioned into the remaining number of balanced bundles with value at least one. The hardest case is the initial split, where two witness cells of an agent'
Load-bearing premise
The load-bearing premise is that in the 2+2 occupancy case, the three anchor-free unit cells can always be cut to repair both shortfalls, which requires the two shortfalls to sum to at most the least anchor value; if this fails for some valuation profile, the balanced residual lemma and hence the main theorem are not proven.
Editorial extensions
If this is right
- For four agents, a complete 1-out-of-d maximin-share allocation is guaranteed exactly for d≥5; d=4 can fail, so the new result is the sharp threshold.
- The proof is fully formalized and machine-checked in a proof assistant, giving the existence statement a high level of verification.
- The balanced-residual argument is presented as the transferable core; extending 1-out-of-(n+1) existence to more agents would require a generalized analogue that can repair many simultaneous anchor collisions.
- The construction is existential and does not yet address the computational complexity of finding such allocations.
Reading between the lines
- The 2+2 repair mechanism suggests a possible route to proving larger-denominator guarantees for more than four agents: find a multi-cell analogue of the nearest-crossing split that can handle many shortfalls with the same total budget.
- Because the proof reduces to an ordered normalized instance, a practical algorithm might sort goods by each agent's value and then repeatedly apply the residual partition; the complexity of doing so remains open.
- The four-agent characterization could serve as a test bed for conjectures about the smallest universal denominator in ordinal maximin-share guarantees for general n, with the 1/3 cutoff here hinting at a more general numerical obstruction.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper proves Theorem 1: for every finite set of goods and every profile of four nonnegative additive valuations, there is a complete allocation in which each agent receives at least her 1-out-of-5 maximin share. The proof first normalizes each positive target to five unit witness cells, reduces the instance to a common ordered instance, and then establishes a Balanced Residual Lemma (Lemma 5) that allows rejected balanced bundles to be removed while preserving enough balanced unit-valued bundles for the remaining agents. An envy-free matching argument converts this single-agent lemma into the four-agent existence theorem. The paper also records Corollary 7, the full characterization for four agents: the universal guarantee holds exactly for d >= 5, using known exact-MMS counterexamples for d <= 4. The authors additionally claim a sorry-free Lean 4 formalization of the theorem.
Significance. If correct, the result closes the last open denominator for four-agent ordinal maximin share, improving the previous 1-out-of-6 guarantee to the optimal 1-out-of-5. The main technical contribution, Lemma 5, is a genuinely combinatorial balanced-residual partition lemma, and its intricate 2+2 occupancy case is handled by a neat nearest-crossing split argument. The proof is self-contained and uses only standard tools (Hall's theorem, envy-free matching). The claimed Lean 4 formalization is a potentially strong correctness certificate, but the artifacts are not yet available in the text; this is an external-verification concern rather than a mathematical gap. Overall, the paper is significant and, on reading, both the central theorem and its proof appear sound.
minor comments (4)
- [Section 4] The machine-verification claim is stated without the Lean source files being available in the arXiv text. Please include the Lean development, or a persistent link to it, in the final version so the sorry-free claim can be checked.
- [Lemma 5, case k=2] The sentence 'would give v(R)<2' is correct but understated: the contradiction is with v(R)>3. Rewording to make this explicit would improve readability.
- [Lemma 5, pattern 2+2] The sentence 'Use U for the two complementary demands x, 1-x' could be expanded to note that the two demands sum to exactly the value of U, which is why Lemma 4 is applicable to the unit cell U.
- [Section 3.1] The phrase 'All agents now agree that g1 is the highest rank' is potentially misleading because the agents still have different cardinal values. Consider clarifying: each agent's value is nonincreasing in the common rank order.
Circularity Check
No circularity identified; derivation is self-contained.
full rationale
I find no circularity. The central derivation is self-contained: Lemma 2 constructs a dominated unit-witness normalization from a witness partition and does not presuppose the theorem; Lemma 5 is proved directly using Lemmas 3 and 4 and unit-witness accounting; Lemma 6 is stated as a standard matching result but is also proved in the paper; and Theorem 1 follows from a maximal-feasible-partial-allocation argument with no fitted parameter or renamed prior result. The cited external results ([1], [5], [6]) provide architecture and known counterexamples, but none of the load-bearing steps reduces to a self-citation or to an input by construction. I also considered the Section 4 statement that the Lean sources 'will accompany the arXiv submission': this is an external-verification limitation rather than a circularity, since the mathematical derivation does not depend on the machine-checked artifacts. Accordingly, the score is 0.
Assumptions & free parameters
assumptions (4)
- standard math Hall's marriage theorem
- standard math Existence of finite maxima and basic real arithmetic
- domain assumption Nonnegative additive valuations
- domain assumption Known exact-MMS counterexample for four agents (Kurokawa, Procaccia, Wang 2018)
Cite this review
Pith. "Pith review of 1-out-of-5 Maximin-Share Allocations Always Exist for Four Agents." pith.science (2026). https://pith.science/paper/IPUR3Z6P
@misc{pith2026260718139,
author = {Pith},
title = {Pith review of: 1-out-of-5 Maximin-Share Allocations Always Exist for Four Agents},
year = {2026},
howpublished = {\url{https://pith.science/paper/IPUR3Z6P}},
note = {Machine review of arXiv:2607.18139}
}
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.
Reference graph
Works this paper leans on
-
[1]
Elad Aigner-Horev and Erel Segal-Halevi. Envy-free matchings in bipartite graphs and their applications to fair division.Information Sciences, 587:164–187, 2022. arXiv:1901.09527
arXiv 2022
-
[2]
Improving approximation guarantees for maximin share
Hannaneh Akrami, Jugal Garg, Eklavya Sharma, and Setareh Taki. Improving approximation guarantees for maximin share. InProceedings of the 25th ACM Conference on Economics and Computation, 2024. arXiv:2307.12916
arXiv 2024
-
[3]
Simultaneous ordinal maximin share and envy-based guarantees,
Hannaneh Akrami and Timo Reichert. Simultaneous ordinal maximin share and envy-based guarantees,
-
[4]
The combinatorial assignment problem: Approximate competitive equilibrium from equal incomes.Journal of Political Economy, 119(6):1061–1103, 2011
Eric Budish. The combinatorial assignment problem: Approximate competitive equilibrium from equal incomes.Journal of Political Economy, 119(6):1061–1103, 2011
2011
-
[5]
Ordinal maximin share approximation for goods
Hadi Hosseini, Andrew Searns, and Erel Segal-Halevi. Ordinal maximin share approximation for goods. Journal of Artificial Intelligence Research, 74:353–391, 2022. arXiv:2109.01925
arXiv 2022
-
[6]
Procaccia, and Junxing Wang
David Kurokawa, Ariel D. Procaccia, and Junxing Wang. Fair enough: Guaranteeing approximate maximin shares.Journal of the ACM, 65(2), 2018. 8
2018
Reviewed August 1, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.