REVIEW 2 major objections 5 minor 12 references
Complete EFX Allocations Exist for Four Additive Agents and Up to Nine Goods
T0 review · 2 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash
Pith's one-line read The paper proves that every four-agent additive fair-division instance with at most nine goods admits a complete $\mathrm{EFX}_0$ allocation.
desk verdict Real frontier result with an unusually honest machine-checked proof; the theorem is only as strong as Z3's unsat verdicts, so treat the boundary as conditional until an independent re-solve or proof objects appear. 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 central device is a certified cover of the valuation polytope. The normalized space of valuations is covered by a fail-closed tree of regions: branches record each non-pivot agent's argmax good, cubes record second favorites, and sub, tri-sub, and rank-grid layers pin third and fourth favorites. For a region $R$, the certified statement is that a short stored list $S(R)$ of allocations contains an $\mathrm{EFX}_0$ allocation for every $v\in R$, and the check is an unsatisfiability query in quantifier-free linear real arithmetic: $F_R \wedge \bigwedge_{A\in S(R)}\Phi_A$, where $\Phi_A$ says $A$ is not $\mathrm{EFX}_0$. Two lemmas make the computation tractable: Lemma 6 canonicalizes the branch where all agents share the same top good by fixing an agent that maximizes the top-two sum, and Lemma 7 deletes dominated envy disjuncts using only the region's known partial order, with every deletion re-proved. The search that found the allocation menus is untrusted; the unsat verdicts and the region enumeration are the trusted base.
What would settle it
Re-solve every certificate from scratch under exact rational arithmetic with two independent SMT solvers; any satisfiable formula yields a concrete normalized valuation for which the region's allocation menu fails, refuting Theorem 1. Then run the packaged but unexecuted full solve pass of the third independent implementation: its from-scratch census must reproduce 165/56/109/36,152 and close all 109 solver branches, and a single gap invalidates the coverage claim.
Extended reading notes
Core claim
Stated as Theorem 1, the paper's central claim is that every $n=4$ additive instance with $m\le9$ goods admits a complete $\mathrm{EFX}_0$ allocation. To prove this, valuations are normalized so each agent's total is one, agent 0's goods are sorted in descending order, and the argmax goods of the other three agents split the space into 165 branch types. The 56 branch types with four distinct nonzero favorite goods are handled by a direct construction; the remaining 109 are certified by a region tree. For every leaf region the certificate says that a finite stored list of allocations already contains an $\mathrm{EFX}_0$ allocation for every valuation in the region, which is verified by refuting the contrary linear-arithmetic formula. The paper reports all 122,553 certificates solved as unsatisfiable in exact arithmetic, with zero failures across 141,878,161 per-clause checks, and it presents the eight-good case both as an earlier independent certification and as a padding corollary of the nine-good theorem.
Load-bearing premise
The whole theorem rests on the machine verification being exactly as reported: the 122,553 unsat verdicts, the independent certifier's region enumeration, and the per-clause reduction re-proofs, and the paper does not supply fully formal proof objects that a reader could check without trusting a solver.
Editorial extensions
If this is right
- For any four-agent additive instance with at most nine goods, the archived certificate corpus gives a concrete lookup procedure: normalize the input, find its region, and output one of the region's stored allocations, with exact arithmetic verifying that it is $\mathrm{EFX}_0$.
- Because $\mathrm{EFX}_0$ and ordinary EFX existence coincide, the theorem also gives complete EFX allocations under the standard definition, not only in the zero-tolerant variant.
- The eight-good case is certified twice: directly by the earlier project at that size and as a one-paragraph padding corollary of the nine-good theorem, so the two independent routes can be checked against each other.
- The paper's certified-cover method applies to larger $m$ and $n$ unchanged, at increased computational cost, so the next step is to run the same pipeline at $m=10$ or with five agents to see where the obstacle moves.
Reading between the lines
- The hardness analysis suggests a targeted strategy for counterexample searches at $m=10$: concentrate on the near-identical diagonal in branch $(0,0,0)$, where the shared top good changes from singleton to paired bundles between nearby valuations; a counterexample, if one exists, is most likely to live there.
- The paired valuations inside a single region indicate that no simple potential-function argument can prove the general four-agent conjecture, because any uniform measure of progress fails at one of the two points; a proof may need allocation rules that depend on finer region structure than second favorites.
- A natural external check is to have a proof-producing SMT solver emit independent refutation objects for the corpus, since the paper's declared trust base currently accepts solver unsat verdicts without fully formal proof objects.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper proves (Theorem 1) that every fair-division instance with four additive agents, non-negative real valuations, and at most nine indivisible goods admits a complete EFX0 allocation. The proof combines a hand-written reduction layer—normalization, sorted-agent branching, and a hand proof for 56 of 165 branch families—with a machine-certified region tree for the remaining 109 branches, covering 36,152 canonical regions. Each region carries a finite menu of allocations, and the claim that this menu contains an EFX0 allocation for every valuation in the region is reduced to a quantifier-free linear-arithmetic unsatisfiability check. The paper reports 122,553 certificates, all solved by Z3 4.16.0, a per-clause re-proof of the dominance reduction with 141,878,161 checks, and a third implementation whose coverage pass is complete. It also documents the computational hardness concentration near identical valuations and the absence of proof objects.
Significance. If Theorem 1 is correct, it extends the known complete-EFX frontier for additive four-agent instances from m ≤ n+3 to m = n+5, a genuine advance. The region-certificate method, which certifies continuous valuation regions rather than discrete combinatorial objects, is novel and plausibly reusable at larger sizes. The paper is unusually transparent about its verification: fail-closed gates, negative controls, from-scratch re-solving, and an explicit statement of the trusted base are all strengths. The hardness anatomy may be useful for future attacks on the general conjecture. The significance is conditional on the soundness of the machine verification, because the theorem rests on solver unsat verdicts for which no independently checkable proof objects are supplied.
major comments (2)
- [Section 5 (Trusted Base) and Section 6 (Outcome)] The theorem depends on 122,553 QF LRA unsat verdicts produced by Z3 4.16.0, and the paper explicitly places these verdicts in the trusted base without producing independently checkable proof objects. The independent verify_min.py implementation's coverage pass checks that every required region is present, but not that every emitted formula is genuinely unsatisfiable; its full solve pass was 'packaged as resumable rather than executed.' A single erroneous unsat verdict, or a systematic encoding error shared by certify9.py and verify_min.py, would falsify Theorem 1 while leaving the paper's prose unchanged. I request that the authors execute the verify_min.py full solve pass over the final corpus and report the outcome, and/or emit cvc5 proof objects verified by an external proof checker, and include the results in the run record.
- [Section 3, Lemma 5] The allocation construction in Lemma 5 is incompletely specified. The text fixes an agent k and says the other three agents 'each take a favorite good among the remaining goods' and k 'receives the two final remaining goods,' which does not visibly allocate all nine goods. The subsequent proof sentence refers to 'the triple owned by k,' contradicting the two-good description. Since Lemma 5 establishes existence for 56 of the 165 branch families, the construction must be rewritten as a precise allocation of all goods, including the initial assignment of each agent's favorite good, and the EFX0 verification, including k's envy, must be spelled out.
minor comments (5)
- [Abstract and Section 1] The abstract and Section 1 contain the grammatical error 'by a independent small third implementation'; it should read 'by an independent.' Also, the phrase 'Organization, Arithmetic, T ools' in Section 1 contains an errant space in 'Tools.'
- [Section 4 (Cube layer)] The notions of 'second favorite,' 'third favorite,' and 'fourth favorite' are used throughout the census and the certificates but are not formally defined for valuations with ties; a fixed tie-breaking convention should be stated so that the region census is deterministic, even if over-coverage is harmless for the existence argument.
- [Section 8] The padding argument that Theorem 1 for m = 9 implies the result for all m ≤ 9 is asserted but not written out; please state explicitly that adding zero-valued goods preserves EFX0 for the original goods.
- [Section 7] The narrative around the two exhibited valuations vA and vB says a 'typical point' has about 370 EFX0 allocations, while vA and vB have 1,680 and 5,544 respectively; this is not contradictory, but the distinction between the typical point and the exhibited points should be made explicit to avoid confusion.
- [Section 5 and Section 6] The evidence archive is hosted on Google Drive; a permanent archival repository or DOI would be more appropriate for a paper whose central claim depends on a large certificate corpus.
Circularity Check
No significant circularity: the proof is a hand-reduction plus machine-certificate corpus, re-derived and re-solved from scratch, with no claim reducing to its own inputs.
full rationale
I walked the paper's derivation chain carefully. Theorem 1 is reduced by hand-proven lemmas (normalization, sorted agent 0, argmax branching, C0 canonicalization, Lemma M clause reduction, promotion completeness) to a finite cover of 36,152 regions, each carrying a finite allocation menu. The crucial check that a menu F suffices for a region P is a QF LRA unsatisfiability verdict on the region constraints plus the negation of the EFX0 condition; these verdicts are re-derived from the stored allocation lists and re-solved from scratch by an independent certifier, with per-clause soundness checks and a separate third implementation's coverage pass. No parameter is fitted to the target result, no quantity called a prediction is defined in terms of the output, and no allocation menu is accepted merely because the search produced it. The C0 canonicalization chooses a prefix length K=2, but this is a free proof choice justified by an explicit EFX0-preserving relabeling argument, not a fitted input; the paper even documents the hazard of mixing different prefix lengths. Self-citations to prior EFX work are contextual rather than load-bearing: the EFX/EFX0 reduction is reproduced in a footnote, and the m=8 result is not needed for Theorem 1 because the m=9 theorem has a padding corollary. The genuinely soft spot is exposed by the paper itself: the trusted base includes the SMT solvers' unsat verdicts, independently checkable proof objects were not produced, and the third implementation's full solve pass was packaged but not executed. That is a verification gap and a correctness risk, not circularity: the derivation is not equivalent to its inputs by construction, and no specific equations reduce to one another.
Assumptions & free parameters
free parameters (1)
- C0 canonicalization prefix length K =
2
assumptions (2)
- domain assumption Z3 4.16.0 (with smt.arith.solver=2) is sound for the QF LRA formulas it reports unsat.
- domain assumption The certifier certify9.py correctly enumerates all required regions, reconstructs formulas from allocation lists, and applies the cover recursion.
Cite this review
Pith. "Pith review of Complete EFX Allocations Exist for Four Additive Agents and Up to Nine Goods." pith.science (2026). https://pith.science/paper/CN33CKQV
@misc{pith2026260808590,
author = {Pith},
title = {Pith review of: Complete EFX Allocations Exist for Four Additive Agents and Up to Nine Goods},
year = {2026},
howpublished = {\url{https://pith.science/paper/CN33CKQV}},
note = {Machine review of arXiv:2608.08590}
}
abstract
We prove that every fair-division instance with four agents, additive valuations over the non-negative reals, and at most nine indivisible goods admits a \emph{complete} allocation that is envy-free up to any good in the strong, zero-tolerant sense ($\EFXo$). The case $m=9=n+5$ lies beyond the previously known frontier for complete EFX with four agents ($m\le n+3$). The proof combines a small set of hand-proven reduction lemmas with a machine-verified certificate corpus. The valuation polytope is covered by a collection of smaller polytopes. For each smaller polytope $P$, a family $F$ of allocations is found that contains an $\EFXo$ allocation for every valuation in $P$. The check that $F$ suffices for $P$ is a quantifier-free linear-arithmetic unsatisfiability verdict, re-derived and solved from scratch by an independent certifier, corroborated per clause, and re-verifiable by a independent small third implementation. The $m=8$ case is established twice: by an earlier independent project at that size and as a one-paragraph padding corollary of the $m=9$ theorem. We additionally give a possible explanation why the problem is hard: difficulty concentrates on near-identical valuations, where only ${\approx}0.14\%$ of all $4^9$ allocations are $\EFXo$, and explicit valuation pairs inside a single region force opposite mandatory allocation structure, evidence relevant to the general conjecture independently of any solver stack.
Reference graph
Works this paper leans on
-
[1]
Hannaneh Akrami, Noga Alon, Bhaskar Chaudhury, Jugal Garg, Kurt Mehlhorn, and Ruta Mehta. EFX : A Simpler Approach and an (Almost) Optimal Guarantee via Rainbow Cycle Number https://doi.org/10.1287/opre.2023.0433 . Operations Research , 2024. a preliminary version was presented at EC 2023
arXiv 2023
-
[2]
Hannaneh Akrami, Alexander Mayorov, Kurt Mehlhorn, Shreyas Srinivas, and Christoph Weidenbach. A Counterexample to EFX; n 3 Agents, m n + 5 Items, Submodular Valuations via SAT-Solving arXiv.org:2604.18216 . arXiv , April 2026
arXiv 2026
-
[3]
B. Berger, A. Cohen, M. Feldman, and A. Fiat. Almost Full EFX Exists for Four Agents https://doi.org/10.1609/aaai.v36i5.20410 . In Proceedings of the AAAI Conference on Artificial Intelligence , page 4826–4833, 2022
-
[4]
The satisfiability modulo theories library (smt-lib), 2016
Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The satisfiability modulo theories library (smt-lib), 2016
work page 2016
-
[5]
Bhaskar Ray Chaudhury, Jugal Garg, and Kurt Mehlhorn. EFX Exists for Three Agents https://arxiv.org/abs/2002.05119 . JACM , 71:1--27, 2024. a preliminary version appeared in EC '20
work page Pith review arXiv 2002
-
[6]
A Little Charity Guarantees Almost Envy-Freeness
Bhaskar Ray Chaudhury, Tellikepalli Kavitha, Kurt Mehlhorn, and Alkmini Sgouritsa. A Little Charity Guarantees Almost Envy-Freeness http://arxiv.org/abs/1907.04596 . SIAM J. Comput. , 50(4):1336--1358, 2021
work page Pith review arXiv 1907
-
[7]
Improved maximin fair allocation of indivisible items to three agents
Uriel Feige and Alexey Norkin. Improved maximin fair allocation of indivisible items to three agents. CoRR , abs/2205.05363, 2022
arXiv 2022
- [8]
Show all 12 references
-
[9]
Computer-aided methods for social choice theory
Christian Geist and Dominik Peters. Computer-aided methods for social choice theory. In Ulle Endriss, editor, Trends in Computational Social Choice , pages 249--267. AI Access, 2017
2017
-
[10]
Extension of additive valuations to general valuations on the existence of EFX
Ryoga Mahara. Extension of additive valuations to general valuations on the existence of EFX . Mathematics of Operations Research , 49(2):1263--1277, 2023
2023
-
[11]
Counterexamples to EFX for Submodular and Subadditive Valuations arXiv.org:2605.06451
Simon Mackenzie and Mashbat Suzuki. Counterexamples to EFX for Submodular and Subadditive Valuations arXiv.org:2605.06451 . arXiv , May 2026
2026 arXiv
-
[12]
Almost envy-freeness with general valuations
Benjamin Plaut and Tim Roughgarden. Almost envy-freeness with general valuations. SIAM J. Discret. Math. , 34(2):1039--1068, 2020
2020
Reviewed August 14, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.