{"id":"8495405a-c59e-41ed-b480-1ad880e492ea","arxiv_id":"2608.08590","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"Every instance with four additive agents and up to nine indivisible goods admits a complete, zero-tolerant EFX allocation.","lead":"This paper proves a fair-division result: with four people, simple item values, and up to nine items, there is always a way to split all items so that nobody strongly envies anyone else. It extends what was known from seven items to nine, using hand proofs together with a large computer-checked case analysis.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 1 is only as secure as Z3 4.16.0's unsat verdicts: no proof objects exist and the independent full solve pass was not run, so a single erroneous solver verdict could invalidate the claim.","rationale":"I went through the two-layer proof structure. The hand layer (normalization, argmax branching, Lemma 5, C0 canonicalization, Lemma M, promotion) is internally consistent: the 165-branch count is correct, the non-strict child covers are weak covers, and the reduction deletions of Lemma 7 are re-proved per clause. The machine layer is a genuine existential certificate: for each region, the stored allocation list is checked by an unsat formula over the region's linear constraints. The critical dependence is the trust base declared in Section 5: solver unsat verdicts are trusted, no formal proof objects were produced, and the independent implementation's full solve pass was deliberately not run. This is not a mathematical inconsistency but a load-bearing verification gap: if any of the 122,553 emitted unsat verdicts is wrong, or if the certifier and solver share a systematic error, Theorem 1 falls while the prose remains intact. The paper's own limitation statements (Section 5 and the Section 6 outcome list) make exactly this point. I therefore keep the reader's conditional verdict; a full independent/cvc5 solve pass with proof validation would turn the condition into acceptance.","tokens_in":10282,"tokens_out":20647,"duration_ms":238733,"concrete_test":"Execute the packaged verify_min.py full solve pass on the entire archived corpus (all 122,553 certificates) under certify9.py's dual mode, running both Z3 4.16.0 and cvc5 on each formula and, where possible, extracting and validating cvc5 proof objects. The theorem is confirmed only if every formula is unsat under both solvers with zero sat/unknown verdicts and all proof objects check.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The main theorem is established by machine certificates: 122,553 QF LRA unsat formulas covering all 36,152 canonical regions (Section 6). Section 5 places 'the SMT solvers' unsat verdicts on QF LRA' in the trusted base and explicitly states that independently checkable proof objects were not produced and that the independent implementation's full solve pass was 'packaged as resumable rather than executed'. The in-family certifier re-derives and re-solves each formula, and the independent verify_min.py has a complete coverage pass, but coverage checks presence, not truth: no from-scratch pass over the final corpus verifies that every emitted formula is actually unsat. A single wrong unsat answer, or a systematic encoding/reduction error shared by the certifier and Z3, would falsify Theorem 1 with no visible change in the paper. The hand reductions and census arithmetic check out, so the residual risk is this verification gap, not a discovered mathematical inconsistency.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":10458,"tokens_out":15251,"duration_ms":157453,"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":[{"comment":"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":"Section 5 (Trusted Base) and Section 6 (Outcome)"},{"comment":"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.","section":"Section 3, Lemma 5"}],"minor_comments":[{"comment":"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":"Abstract and Section 1"},{"comment":"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":"Section 4 (Cube layer)"},{"comment":"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":"Section 8"},{"comment":"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":"Section 7"},{"comment":"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.","section":"Section 5 and Section 6"}],"recommendation":"major_revision","confidential_remarks":"The mathematical architecture is coherent and the verification effort is unusually serious, but the missing proof objects and the unexecuted independent full-solve pass leave the central claim exposed to a single solver bug. I believe the authors can address this within the manuscript's scope by running the resumable independent pass and/or adding checked proof objects; if they do, I would support acceptance."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this paper deserves to be read, and it deserves a serious referee. If the certificates are right, it settles complete EFX0 for four additive agents up to nine goods, pushing past the m ≤ n+3 frontier; the m=9=n+5 case is genuinely new, and the m=8 padding corollary is a free bonus. The region-certificate method—covering the continuous valuation polytope with linear regions, each carrying a finite allocation menu whose sufficiency is a QF LRA unsat check—is a real methodological contribution, not just a bigger search.\n\nWhat the paper does well: the hand layer is clean. Lemma 5 handles the four-distinct-favorites branch, Lemma 6 spots and solves a genuine symmetry issue in the common-top branch rather than silently choosing a representative, and Lemma M is a sensible clause-reduction discipline with per-clause re-proofs. The verification protocol is unusually careful: fail-closed gates, negative controls, self-tests, an independent certifier that re-derives regions from the combinatorics, and 141,878,161 per-clause checks with zero failures. The paper reports the gaps it caught and the retracted completion claim; that is honest evidence the gates work.\n\nSoft spots, in proportion: the load-bearing step is a single solver's unsat verdicts. There are no independently checkable proof objects, and the independent implementation's full solve pass over the final corpus was packaged as resumable but not run. The in-family certifier re-solves every formula from scratch, but that is still the same solver family and same encoding; a shared systematic error in the reduction or a single wrong Z3 verdict would invalidate Theorem 1 without changing the prose. The reviewer cannot inspect the artifact from the page; I did not. That is a verification gap, not a discovered contradiction. The hand reductions and census arithmetic check out, and I saw no circular fit. The K=2 choice in Lemma 6 is a free parameter, but the paper explains why a nested family is safe and fixes K in the run configuration; it is not a fitted constant in the mathematical statement.\n\nWho it's for: fair division people working on EFX, and anyone interested in computer-assisted existence proofs over continuous domains. I would send it to a strong referee, but I would ask the authors to either run the independent solve pass or produce cvc5/proof-object corroboration for the corpus before final acceptance. With that, the result is the new frontier.","headline":"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.","tokens_in":11043,"tokens_out":2905,"would_cite":true,"duration_ms":30896,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["91B32"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proves that every four-agent additive fair-division instance with at most nine goods admits a complete $\\mathrm{EFX}_0$ allocation.","keywords":["fair division","EFX","envy-free up to any good","additive valuations","indivisible goods","complete allocation","machine-verified proof","quantifier-free linear real arithmetic"],"falsifier":"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.","tokens_in":10061,"feed_emoji":"⚖️","tokens_out":12846,"duration_ms":128728,"temperature":0.7,"pith_summary":"This paper proves that every instance with four agents, additive valuations over at most nine indivisible goods, and arbitrary non-negative real valuations admits a complete allocation that is envy-free up to any good in the strong, zero-tolerant sense $\\mathrm{EFX}_0$. The case $m=9=n+5$ moves past the known frontier for complete EFX with four agents, which was $m\\le n+3$. The proof is a hybrid: a small set of hand-proven lemmas organizes the normalized valuation space into 36,152 linear regions, and each region carries a finite menu of allocations whose sufficiency is certified by exact quantifier-free linear real arithmetic. Because the $\\mathrm{EFX}_0$ and standard EFX existence questions coincide, the same result covers the usual definition, and the eight-good case follows by padding. This matters because complete EFX existence for additive valuations with $n\\ge4$ is open in general, and the method gives a concrete certified route past a frontier that hand proofs had not crossed.","feed_headline":"Nine goods, four agents: a complete envy-free allocation always exists","feed_subtitle":"Machine-checked proof extends the four-agent additive fair-division frontier from seven to nine goods.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the previous frontier $m\\le n+3$ for complete EFX with four agents that this theorem extends.","marker":"[Mah23]"},{"why":"Supplies the three-agent EFX theorem and the perturbation argument that identifies EFX and $\\mathrm{EFX}_0$ existence.","marker":"[CGM24]"},{"why":"Establishes four-agent EFX with at most one unallocated good, the state this paper strengthens to completeness at $m\\le9$.","marker":"[BCFF22]"},{"why":"Provides two-agent EFX existence and the easy identical-valuations case used as a baseline in the hardness analysis.","marker":"[PR20]"},{"why":"Documents the SMT-LIB standard and the QF LRA decision procedure relied on by the solver-based certificates.","marker":"[BFT16]"}],"fun_headline_variants":["Complete EFX proven for 4 agents and 9 goods, machine-verified","Machine-checked proof: complete EFX for 4 agents, 9 goods","Zero-tolerant EFX complete allocation exists for 4 agents, 9 goods","Fair division: complete EFX now proven for 4 agents, 9 goods","Envy-free up to any good: complete allocation for 4 agents, 9 goods"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Complete EFX proven for 4 agents and 9 goods, machine-verified","Machine-checked proof: complete EFX for 4 agents, 9 goods","Zero-tolerant EFX complete allocation exists for 4 agents, 9 goods","Fair division: complete EFX now proven for 4 agents, 9 goods","Envy-free up to any good: complete allocation for 4 agents, 9 goods"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000876,"raw_usage":{"total_tokens":3847,"prompt_tokens":1058,"completion_tokens":2789,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":674,"completion_tokens_details":{"reasoning_tokens":2682}},"tokens_in":674,"tokens_out":2789,"duration_ms":23413,"temperature":1.0,"reasoning_tokens":2682,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T04:31:02.585003+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}