AI 中文总结
本文针对具有二元边际的单调成本函数，构造18智能体、53个chore的反例，证实不可分割chore的EFX分配不存在，并在Lean 4中形式化验证结果。
AI 中文摘要
我们研究智能体拥有二元边际的单调成本函数时，不可分割chore的无妒忌（EFX）分配的存在性。对于不可分割goods，一般单调函数加二元边际的情况已证实存在EFX分配；但对于chore，此前仅在更受限类别中证实存在EFX分配，二元边际的一般情况仍未解决。本文基于同一个18智能体、53个chore的word小工具构造了两个反例，分别对应二元XOS成本和二元超模成本的成本分布，两种情况下均不存在完整的EFX分配。最后，我们在Lean 4中形式化并验证了主要结果。
英文摘要
We study the existence of envy-free up to any item (EFX) allocations of indivisible chores when agents have monotone cost functions with binary marginals. For indivisible goods, the corresponding existence question is known to have an affirmative answer for general monotone functions with binary marginals. For chores, however, the existence of EFX allocation was previously known only for more restricted classes, while the general binary-marginal case remained unresolved. In this paper, we provide two counterexamples based on the same 18-agent, 53-chore word gadget, with one cost profile for binary XOS costs and another for binary supermodular costs. In both cases, a complete EFX allocation need not exist. Finally, we formalize and verify our main results in Lean 4.
