Motivation

A committee that chooses one alternative by voting would like a voting procedure under which no member can gain by misreporting their preferences. Such a procedure is called strategy-proof. Gibbard (Econometrica 41, 1973) and Satterthwaite (J. Econ. Theory 10, 1975) proved independently that, once at least three outcomes are possible, the only strategy-proof procedures are dictatorial. The result is the starting point of the theory of strategy-proof mechanisms: it is why mechanism design restricts preference domains (single-peaked preferences, quasi-linear utilities) or allows randomization.

This mission formalizes Theorem 1 of Satterthwaite's paper, in the version circulated as Northwestern University CMS-EMS Discussion Paper No. 122 (revised December 12, 1974). Its formulation has one feature that the textbook version lacks: the hypothesis is on the range of the procedure, not on the whole alternative set, and the dictatorship is accordingly relative to that range.

Setting

A committee has a finite set $I_n$ of $n\ge 1$ individuals and a finite set $S_m$ of $m$ alternatives. In a strict committee every individual's ballot $B_i$ is a strong order on $S_m$, a ranking without ties; $x\,\bar B_i\,y$ means that $B_i$ ranks $x$ strictly above $y$. The set of strong orders is $\rho_m$, and a ballot set is $B=(B_1,\dots,B_n)\in\rho^n_m$.

A strict voting procedure $v^{nm}$ assigns to each ballot set a single alternative $v^{nm}(B)\in S_m$. Its range $T_p$ is the set of alternatives it selects at some ballot set, and $p=|T_p|$, so $1\le p\le m$.

Individual $i$ can manipulate $v^{nm}$ at $B$ if some ballot $B_i'$ gives

$$v^{nm}(B_1,\dots,B_i',\dots,B_n)\ \bar B_i\ v^{nm}(B_1,\dots,B_i,\dots,B_n),$$

an outcome $i$ strictly prefers by the standard of the original ballot. The procedure is strategy-proof if no individual can manipulate it at any ballot set.

The procedure is dictatorial if some individual $i$ exists such that, at every ballot set $B$, $v^{nm}(B)$ is the element of the range $T_p$ that $B_i$ ranks highest. It is fully dictatorial if in addition $T_p=S_m$ and partially dictatorial if $T_p\subsetneq S_m$.

The proof uses three further notions. Condition U requires that if every $B_i$ ranks the same $x\in T_p$ above all other elements of $T_p$, then $v^{nm}(B)=x$. The procedure is weak alternative-excluding if $T_p\subsetneq S_m$, and strong alternative-excluding if in addition it satisfies Condition U. Finally $\theta_T(B_i)$ is the restriction of $B_i$ to a subset $T$.

Formalization targets

Goal: Theorem 1 (p. 11)

For a strict committee with $n\ge 1$ and $m\ge p\ge 3$,

$$v^{nm}\ \text{is strategy-proof}\iff v^{nm}\ \text{is dictatorial}.$$

Milestones

1. Lemma 1 (p. 13): a strategy-proof strict procedure satisfies Condition U.
2. Lemma 2 (p. 15): with one individual and three alternatives, a strategy-proof procedure is fully dictatorial or strong alternative-excluding.
3. Lemma 3 (pp. 16–17): for $n+1$ individuals and three alternatives, individuals $1,\dots,n$ cannot manipulate $v^{n+1,3}$ if and only if each of the procedures $B\mapsto v^{n+1,3}(B,B_{n+1})$, one for each ballot of individual $n+1$, is strategy-proof.
4. Lemma 4 (p. 22): the induction step from $n$ to $n+1$ individuals for three alternatives.
5. Lemma 5 (p. 25): for $n\ge 1$, $m\ge 3$, a strategy-proof procedure is fully dictatorial or strong alternative-excluding.
6. Lemma 6 (p. 26): for $n\ge 2$, if $\theta_{T}(C_i)=\theta_{T}(D_i)$ for all $i$, with $T=T_p$, then $v^{nm}(C)=v^{nm}(D)$.
7. Proof of Theorem 1, (27)–(28) (p. 27): in the case of a strategy-proof, strong alternative-excluding $v^{nm}$ with $m>p\ge 3$, it induces a strategy-proof procedure $v^{np}$ on the alternatives of its range with $v^{np}[\theta_T(B_1),\dots,\theta_T(B_n)]=v^{nm}(B)$.

Significance

Theorem 1 characterizes the strategy-proof strict voting procedures completely: given $p\ge 3$, they are exactly the procedures that let one individual pick, from a fixed menu $T_p$, their favourite element. The classical statement assumes the procedure can select every alternative; Theorem 1 shows that excluding alternatives from the menu does not help, since a procedure with any menu of at least three alternatives is still governed by one individual. The paper's correspondence theorem with Arrow's social welfare functions (its Theorem 2) and its extension to ballots with indifference (Theorem 1') build on this statement.

The full-range case is on the platform already: AGT.gibbard_satterthwaite (Theorem 9.8 of Nisan–Roughgarden–Tardos–Vazirani, Algorithmic Game Theory) is proved and states that an incentive compatible social choice function onto at least three alternatives has a dictator; it is included here as a reference item and is exactly the case $T_p=S_m$ of Lemma 5. The open item MechanismDesign.SocialChoice.gibbard_satterthwaite (Börgers, Proposition 8.1) poses the full-range equivalence. Theorem 1 contains both as the special case $T_p=S_m$. What this mission adds is the range-restricted statement and the paper's own route to it: the induction on the number of individuals for three alternatives (Lemmas 2–4) and the reduction of a procedure with a proper range to its range (Lemma 6 and (27)–(28)). The paper only sketches Lemma 4 and defers the induction on $m$ to Satterthwaite's dissertation, so the formal development fills these gaps.

Difficulty

The "if" direction is immediate. For the "only if" direction the natural first idea is to apply the full-range theorem to the procedure viewed as a map into $T_p$. This fails as stated: the procedure is still defined on rankings of all $m$ alternatives, and nothing yet says that its choice ignores how individuals rank alternatives outside $T_p$. That is the content of Lemma 6, which needs strategy-proofness and Condition U; only after it does the procedure factor through rankings of $T_p$, and only then is the factor itself strategy-proof. The full-range case itself is the classical theorem, whose known proofs (via Arrow's theorem, or by pivotal-voter arguments) are combinatorial and long.

Formalization scope

• Individuals and alternatives are finite types ι and A; $n$ = Fintype.card ι, $m$ = Fintype.card A, and the $n+1$ individuals of Lemmas 3–4 are Option ι, with none the individual $n+1$.
• Strict ballots and strategy-proofness come from the published definition agt_social (namespace AGT): a ballot is a relation r with IsStrictTotalOrder A r, r x y is the paper's $x\,\bar B_i\,y$, and strategy-proofness is AGT.IncentiveCompatible, which is the paper's definition (1) on $\rho^n_m$.
• The range is taken over strict ballot sets only, and $p$ is its Set.ncard. Theorem 1 assumes $n\ge 1$ and $p\ge 3$; $m\ge p$ holds automatically, so $m\ge 3$ is not a separate hypothesis.
• Dictatorial reads the paper's dictator function $f^i_T$ as "the $B_i$-maximal element of $T_p$", which for strong orders is unique.
• $\theta_T(C_i)=\theta_T(D_i)$ is encoded as agreement of the two strict relations on $T\times T$, and the procedure $v^{np}$ of (28) lives on the subtype of the range.
• Lemmas keep their printed hypotheses ($m\ge 3$, $p\ge 1$, Lemma 6's $n\ge 2$), even where the conclusion would hold without them. The range restriction milestone keeps the proof's case assumptions of strong alternative exclusion and $m>p\ge 3$.

Two encodings would trivialize the goal and are excluded: a range taken over all relation profiles (junk values would make $p\ge 3$ meaningless), and a dictatorship that only constrains ballot sets at which the dictator's overall favourite lies in $T_p$, or that asks for the dictator's favourite in all of $S_m$ (false whenever $T_p\subsetneq S_m$). The bound $p\ge 3$ is needed: a procedure with two possible outcomes, such as majority vote between two fixed alternatives, is strategy-proof and not dictatorial, and an imposed procedure ($p=1$) is dictatorial only vacuously.

Contributions are welcome at every milestone, and the restriction-to-range step (Lemma 6 and (27)–(28)) is reusable for any statement that transfers results from full-range to range-restricted procedures.

Selected references

• M. A. Satterthwaite, Strategy-proofness and Arrow's Conditions: Existence and Correspondence Theorems for Voting Procedures and Social Welfare Functions, Northwestern University CMS-EMS Discussion Paper No. 122, rev. Dec. 12, 1974; published in J. Econ. Theory 10(2) (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
• A. Gibbard, Manipulation of Voting Schemes: A General Result, Econometrica 41(4) (1973) 587–601. https://doi.org/10.2307/1914083
• N. Nisan, Introduction to Mechanism Design (for Computer Scientists), Chapter 9 of N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007. https://doi.org/10.1017/CBO9780511800481
• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Chapter 8. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001

Motivation

Algorithmic mechanism design asks for algorithms whose inputs are held by self-interested parties. Each party reports its private data, the algorithm computes an outcome, and payments are arranged so that no party gains by misreporting. Nisan and Ronen introduced the field in Algorithmic Mechanism Design (Games Econ. Behav. 35, 2001). Their running example is task scheduling on unrelated machines: $k$ tasks are distributed among $n$ machines owned by different agents, each agent knows only its own processing times, and the designer wants to minimize the make-span.

Without incentives the problem is classical: minimizing make-span on unrelated machines is NP-hard and admits a polynomial 2-approximation (Lenstra, Shmoys, Tardos, 1990). With selfish agents the question changes: which approximation ratios can a truthful mechanism guarantee? This mission formalizes the paper's upper bound, the MinWork mechanism, which is the benchmark every later lower bound for truthful scheduling is compared with.

Timeline.

• 1961: Vickrey introduces the second-price auction (J. Finance 16).
• 1971–1973: Clarke and Groves generalize it to the VCG family of truthful mechanisms for utilitarian objectives (Groves, Econometrica 41, 1973).
• 1999/2001: Nisan and Ronen show MinWork is a strongly truthful $n$-approximation, and that no truthful mechanism beats ratio 2.
• 2007: Christodoulou, Koutsoupias and Vidali raise the deterministic lower bound to $1+\sqrt2$ for $n \ge 3$; Koutsoupias and Vidali later raise it to $1+\varphi \approx 2.618$.
• 2023: Christodoulou, Koutsoupias and Kovács prove the Nisan–Ronen conjecture: no deterministic truthful mechanism achieves a ratio below $n$ (STOC 2023, arXiv:2301.11905), so MinWork is optimal among deterministic truthful mechanisms.

Setting

There are $n$ agents and $k$ tasks. Agent $i$'s type is the vector $t^i = (t^i_1,\dots,t^i_k)$ of positive times, $t^i_j > 0$ being the time agent $i$ needs to perform task $j$. A type vector is $t = (t^1,\dots,t^n)$. An allocation $x$ sends each task $j$ to one agent; $x^i$ is the set of tasks agent $i$ receives. The make-span of $x$ is

$$g(x,t) = \max_{i} \sum_{j \in x^i} t^i_j ,$$

and agent $i$'s valuation is $v^i(x,t^i) = -\sum_{j \in x^i} t^i_j$.

A direct mechanism asks every agent to declare a type, computes an allocation $x(d)$ from the declared vector $d$, and hands agent $i$ a payment $p^i(d)$. Agent $i$'s utility is $p^i(d) + v^i(x(d), t^i)$, with $t^i$ its true type. The mechanism is truthful if declaring $t^i$ maximizes agent $i$'s utility for every declaration of the others, and strongly truthful if truth-telling is the only such dominant strategy. An allocation rule is a $c$-approximation if $g(x(t),t) \le c \cdot g(y,t)$ for every type vector $t$ and every allocation $y$.

The MinWork mechanism allocates each task to an agent with minimal declared time for it, breaking ties arbitrarily. For each task it wins, an agent receives the second-best declared time $\min_{i' \ne i} d^{i'}_j$:

$$p^i(d) = \sum_{j \in x^i(d)} \min_{i' \neq i} d^{i'}_j .$$

The Lean development uses the same names: load, makespan, IsTruthful, IsStronglyTruthful, IsApprox, IsMinWorkAlloc, secondBest, minTime, minWorkPay.

Formalization targets

Goal: Theorem 4.1

For $n \ge 2$ and every MinWork allocation rule $x$ with payments $p$ as above,

$$(x,p)\ \text{is strongly truthful} \quad\text{and}\quad g(x(t),t) \le n \cdot g(y,t)\ \ \text{for all positive } t \text{ and all allocations } y .$$

Milestones

1. Theorem 3.1 (Groves): a VGC mechanism is truthful. This is an existing platform theorem, used as a reference.
2. MinWork belongs to the VGC family. Its allocation maximizes $\sum_i v^i(t^i,x)$, and its payment is $\sum_{i'\ne i} v^{i'}(t^{i'},x(t)) + h^{-i}$ with $h^{-i} = \sum_j \min_{i'\ne i} t^{i'}_j$.
3. Claim 4.2: MinWork is strongly truthful.
4. $g(x(t),t) \le \sum_{j} \min_i t^i_j$.
5. $g(y,t) \ge \frac1n \sum_j \min_i t^i_j$ for every allocation $y$.
6. Claim 4.3: MinWork is an $n$-approximation.

Significance

The theorem gives the first positive result for truthful scheduling: a mechanism that is truthful in the strongest sense and is within a factor $n$ of optimal, whatever the tie-breaking rule. Every lower bound in the paper (Theorems 4.6, 4.10 and 4.12) and in the later literature measures itself against this ratio. Since the 2023 resolution of the Nisan–Ronen conjecture, the ratio $n$ is known to be tight for deterministic truthful mechanisms.

The result is proved in the paper; it is not known to be formalized in any proof assistant. The platform already has Groves' theorem in an abstract form (AGT.vcg_incentive_compatible). This mission connects that abstract statement to a concrete combinatorial mechanism, and it adds the strict part of strong truthfulness for any number of tasks and agents, which the paper proves only for one task and two agents. The vocabulary (make-span over unrelated machines, direct scheduling mechanisms, strong truthfulness) is shared with the seven later missions of this series.

Difficulty

Truthfulness follows from Groves' theorem once MinWork is identified as a VGC mechanism. The identification requires the payment identity at every declared vector and under every tie-breaking rule, including ties at the winning time. The main difficulty is the strict part of strong truthfulness. A misreport that differs from the truth only on one task must still be shown to lose strictly for some declarations of the others. Those declarations must stay positive, and on every other task they must leave the outcome unchanged. The paper's proof covers only one task and two agents and leaves the general case as "similar". Its printed inequality also has the two utilities in the wrong order (see below), so it cannot be transcribed directly.

Formalization scope

• Agents are Fin n and tasks are Fin k. An allocation is a function Fin k → Fin n, and an agent may receive no task. Types are positive reals, and every truthfulness and approximation quantifier ranges over positive true types, positive misreports and positive declarations of the others.
• Payments are handed to the agent, so utility is the payment minus the true time spent. Payments are computed from the declared vector, never from true types.
• The allocation rule is a parameter satisfying the MinWork specification (IsMinWorkAlloc). Every result holds for every tie-breaking rule, including rules that depend on the whole declared vector. No particular argmin is fixed.
• $n \ge 2$ is a hypothesis of the goal and of the truthfulness items: with a single agent the paper's second-best minimum is undefined. The approximation items need only $n \ge 1$. There is no hypothesis on $k$.
• The make-span and both minima are Finset.sup' / Finset.inf' over nonempty finite sets, so they are true maxima and minima with no default values.
• Strong truthfulness is formalized as truthfulness plus: every misreport $d^i \ne t^i$ is strictly worse than the truth for some positive declarations of the others. Given truthfulness this is equivalent to Definition 5. A formalization that states only that truth-telling is dominant, or proves strictness only for single-task instances, does not meet the goal. Neither does an existential ratio in place of $n$.
• Printed slip: in the proof of Claim 4.2 (p. 177) the case $d^i > t^i$ reads "the utility for agent $i$ is $t^i - d^i < 0$, instead of 0 in the case of truth-telling". With the Definition 11 payments the misreporting agent loses the task (utility 0), and the truthful agent wins it with utility $d^{3-i} - t^i > 0$. The milestone text keeps the paper's words; the Lean statements assert what the argument establishes.
• Out of scope: running time ("polynomial time"), and the paper's general revelation-principle framework (Proposition 2.1).
• Welcome contributions: proofs of the milestones, and a reusable lemma connecting the local VGC milestone to AGT.vcg_incentive_compatible.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• T. Groves, Incentives in Teams, Econometrica 41 (1973) 617–631. https://doi.org/10.2307/1914085
• W. Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16 (1961) 8–37. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
• G. Christodoulou, E. Koutsoupias, A. Kovács, A Proof of the Nisan-Ronen Conjecture, STOC 2023. https://arxiv.org/abs/2301.11905

Motivation

In a combinatorial auction a seller offers several indivisible items at once, and bidders value bundles of items rather than items one at a time. Allocating the items to maximize total value is the central optimization problem of the area, and it arises in spectrum licensing, procurement and transport contracting (Cramton, Shoham and Steinberg, Combinatorial Auctions, MIT Press, 2006). Two obstacles meet. Computationally, a valuation has $2^m$ numbers, so an algorithm can only query it, and even then optimization is hard. Strategically, the valuations are private: a bidder reports whatever maximizes its own utility, so an algorithm that is a good approximation on true inputs may be useless on reported ones.

The classical answer to the strategic obstacle is the VCG payment scheme, which makes truthful reporting a dominant strategy but requires the exact optimum. Nisan and Ronen (2007) showed that an approximation algorithm becomes truthful under VCG payments essentially only when it is maximal in range: it fixes a restricted set of allocations in advance and optimizes exactly over that set. Dobzinski, Nisan and Schapira (Math. Oper. Res. 35(1), 2010, §5) give such an algorithm for complement-free (subadditive) bidders that uses only value queries and loses a factor of order $\sqrt m$. For general valuations in the value-query model the paper cites a lower bound of order $m/\log m$ (Dobzinski and Schapira, working paper 2005; Blumrosen and Nisan, Hebrew University Discussion Paper 381, 2005; see the paper's references [7] and [2]), and the same paper (Theorem 6.1) shows that even XOS bidders cannot be approximated within $m^{1/2-\epsilon}$ with polynomially many value queries.

Setting

A set $M=\{1,\dots,m\}$ of items is sold to $n$ bidders. Bidder $i$ has a valuation $v_i$ that assigns a real number $v_i(S)$ to every bundle $S\subseteq M$. Throughout, valuations are normalized, $v_i(\emptyset)=0$, and monotone, $S\subseteq T\Rightarrow v_i(S)\le v_i(T)$. A valuation is complement free (CF) if $v(S\cup T)\le v(S)+v(T)$ for all bundles $S,T$. An allocation $A=(A_1,\dots,A_n)$ gives the bidders pairwise disjoint bundles (items may stay unallocated), and its social welfare is $\sum_i v_i(A_i)$.

The mechanism receives reports $b=(b_1,\dots,b_n)$ and runs the following algorithm $\mathrm{ALG}$:

1. query $b_i(M)$ and $b_i(\{j\})$ for every bidder $i$ and item $j$;
2. compute a maximum-weight matching $P$ in the complete bipartite graph between items and bidders, where the edge between item $j$ and bidder $i$ costs $b_i(\{j\})$;
3. if the bidder $t$ maximizing $b_i(M)$ has $b_t(M)$ strictly larger than the weight $|P|$, give all items to $t$; otherwise give every item matched by $P$ to its matched bidder.

Its range $R$ is the set of allocations that give all of $M$ to one bidder, together with the allocations in which every bidder receives at most one item. Under VCG payments bidder $i$ receives $\sum_{k\ne i}b_k(\mathrm{ALG}(b)_k)$, so its utility is $v_i(\mathrm{ALG}(b)_i)+\sum_{k\ne i}b_k(\mathrm{ALG}(b)_k)$. The mechanism is incentive compatible on a class of valuations if no bidder can raise its utility by misreporting within that class, whatever the others report.

Formalization targets

Goal: Theorem 5.1 (p. 11)

For every choice of the maximum-weight matching and of the top bidder as functions of the reports, for every profile $v$ of normalized, monotone, CF valuations and every allocation $O$,

$$\sum_{i=1}^n v_i(O_i)\;\le\;2\sqrt m\,\sum_{i=1}^n v_i\big(\mathrm{ALG}(v)_i\big),$$

and the mechanism $(\mathrm{ALG},\text{VCG payments})$ is incentive compatible on the CF valuations.

Milestones, in attack order

1. §5.1, VCG. Welfare maximization with Groves payments is incentive compatible (a published platform theorem, AGT.vcg_incentive_compatible).
2. §5.1, maximal in range. Any allocation rule that optimizes reported welfare exactly over a fixed range is incentive compatible under VCG payments on the same domain.
3. ALG is maximal in range with range $R$ on normalized reports.
4. The CF single-item bound. For a CF valuation and $c\in T$ maximizing $v(\{j\})$ over $T$: $v(T)\le\sum_{j\in T}v(\{j\})\le|T|\,v(\{c\})$.
5. First case. If bidders with $|O_i|\ge\sqrt m$ carry at least half the welfare of $O$, then $\sum_i v_i(O_i)\le 2\sqrt m\,v_t(M)$ for the top bidder $t$.
6. Second case. Otherwise some allocation in which every bidder gets at most one item has welfare at least $\sum_i v_i(O_i)/(2\sqrt m)$.

Significance

The theorem shows that, for subadditive bidders, the $\sqrt m$ barrier known for general valuations can be matched by a truthful mechanism that asks each bidder only $m+1$ value queries. It is one of the early examples of maximal-in-range mechanism design, a template later used for many truthful approximation mechanisms in combinatorial auctions, and it sits against Theorem 6.1 of the same paper, which shows that for XOS bidders no value-query algorithm with polynomially many queries does better than $m^{1/2-\epsilon}$.

The result is proved in the paper. What this mission adds is a machine-checked proof: a formal model of VCG-based mechanisms over a restricted range, a proof that the §5.2 algorithm is maximal in range for every tie-breaking of its two optimization steps, and the explicit constant $2$ in the $O(\sqrt m)$ bound. To our knowledge neither half of Theorem 5.1 is formalized elsewhere; the general VCG theorem exists on the platform in the setting of arbitrary outcome sets.

Difficulty

The approximation argument partitions the bidders of a reference allocation by whether their bundles have at least $\sqrt m$ items, and the two cases need different facts: disjointness bounds the number of large bundles by $\sqrt m$, and subadditivity bounds each small bundle by its size times its best item. A naive transcription breaks at degenerate inputs: the page divides by $|T_i|$ and writes strict inequalities, both of which fail when a bundle is empty or all values are zero, so the formal statement must be organized around non-strict bounds.

Incentive compatibility has a different obstacle. It holds only if the allocation rule depends on the reports alone and optimizes exactly over its range, including at ties between the grand bundle and the matching. The matching and the top bidder are not unique, so the proof must work for an arbitrary but fixed tie-breaking, and the welfare of the matching allocation must be identified with the matching weight, which uses normalization of every bidder who receives nothing.

Formalization scope

Bidders are Fin n, items Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ. Normalization and monotonicity (the paper's standing assumptions, p. 1) and complement freedom are hypotheses; IsCFValuation bundles all three. An allocation is a family of pairwise disjoint bundles; unallocated items are allowed. A matching is a partial map Fin m → Option (Fin n) with no bidder matched twice.

Conventions the formalization commits to:

• Explicit constant. The paper writes $O(\sqrt m)$; its proof yields $2\sqrt m$ (both cases end with $|OPT|/(2\sqrt m)$), and the goal states $2\sqrt m$ with Real.sqrt m.
• Oracles and ties. The maximum-weight matching and the top bidder enter as functions mat, top of the report profile, each with a specification hypothesis; the goal is stated for every such pair. The algorithm reads only the reports; the tie between $b_t(M)$ and $|P|$ goes to the matching, as on the page.
• Payments. The mechanism pays each bidder $\sum_{k\ne i}b_k(\cdot)$, the paper's convention (footnote 2, p. 11); incentive compatibility is stated on the CF domain, the paper's. The local definition mirrors AGT.MechIncentiveCompatible on outcomes $a\mapsto v_i(a_i)$.
• Reference allocation. The approximation is stated against every allocation $O$, not only an optimal one; this is equivalent and avoids a junk maximum.
• Printed slips. The strict inequalities and the division by $|T_i|$ in the second case are replaced by non-strict, multiplied forms; the first case concludes for a bidder maximizing $v_i(M)$ rather than $v_i(O_i)$.
• Degenerate sizes. At $m=0$ everything is zero and the bound holds trivially; with $n=0$ no top-bidder rule exists.
• Out of scope. "In polynomial time" is a running-time claim and is not modelled.

A trivializing formalization is ruled out: the ratio is the explicit $2\sqrt m$ rather than an existential constant, incentive compatibility is over the full CF domain (not additive reports only) for a rule that cannot see true valuations, and the rules mat, top are satisfiable (a maximum over the finitely many matchings exists; a top bidder exists when $n\ge1$).

Useful infrastructure: finite maximum-weight matchings on complete bipartite graphs, subadditivity bounds over Finset sums, and a reusable lemma that maximal-in-range rules with VCG payments are truthful. Contributions of any milestone are welcome; milestones 2 and 4 are self-contained.

Selected references

• S. Dobzinski, N. Nisan, M. Schapira, Approximation Algorithms for Combinatorial Auctions with Complement-Free Bidders, Mathematics of Operations Research 35(1):1–13, 2010. https://doi.org/10.1287/moor.1090.0436
• N. Nisan, A. Ronen, Computationally Feasible VCG Mechanisms, Journal of Artificial Intelligence Research 29:19–47, 2007. https://doi.org/10.1613/jair.2046
• S. Dobzinski, M. Schapira, Optimal Upper and Lower Approximation Bounds for k-Duplicates Combinatorial Auctions, working paper, The Hebrew University of Jerusalem, 2005 (reference [7] of the paper).
• L. Blumrosen, N. Nisan, On the Computational Power of Iterative Auctions I: Demand Queries, Discussion Paper 381, Center for the Study of Rationality, The Hebrew University of Jerusalem, 2005 (reference [2] of the paper).
• N. Nisan, Introduction to Mechanism Design (for Computer Scientists), in N. Nisan, T. Roughgarden, E. Tardos, V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, pp. 209–242.
• P. Cramton, Y. Shoham, R. Steinberg (eds.), Combinatorial Auctions, MIT Press, 2006.

Motivation

A buyer and a seller negotiate over a single indivisible good. Each knows how much the good is worth to them, but not how much it is worth to the other side. Whether the two will trade, and at what price, then depends on how each party shades its offer to exploit the other's uncertainty. Chatterjee and Samuelson (Bargaining under Incomplete Information, Operations Research 31(5), 1983) modelled this situation as a one-shot game in which both parties submit sealed offers simultaneously, and characterised its Bayesian equilibria.

The model became the standard reference point for bilateral trade with two-sided private information. Myerson and Satterthwaite (J. Econ. Theory 29, 1983) showed that no mechanism can guarantee efficient trade in this setting, and that the equilibrium of the Chatterjee–Samuelson game with $k = 1/2$ and uniform values attains the second-best efficiency bound. Later work on the $k$-double auction (Satterthwaite and Williams, J. Econ. Theory 48, 1989; Leininger, Linhart and Radner, J. Econ. Theory 48, 1989) studies the continuum of equilibria of exactly this game. The object of the present mission, a pair of linked differential equations, is the tool these papers use to construct and classify equilibria.

Setting

A seller has reservation price $v_s \in [\underline v_s, \bar v_s]$ and a buyer has reservation price $v_b \in [\underline v_b, \bar v_b]$. Each knows their own value. The buyer's belief about $v_s$ is a probability measure $\mu_b$ with distribution function $F_b$; the seller's belief about $v_b$ is $\mu_s$ with distribution function $F_s$. The subscript names the player who holds the belief, not the variable. Each belief is regular: $F(\underline v) = 0$, $F(\bar v) = 1$, and $F$ is strictly increasing and differentiable on the value interval, with density $f_b$ (respectively $f_s$).

Under the Bargaining Rule, the seller asks $s$ and the buyer offers $b$ simultaneously. If $b \ge s$ the good is sold at $P = kb + (1-k)s$ for a fixed $k \in [0, 1]$; otherwise nothing happens. Profits are $P - v_s$ for the seller and $v_b - P$ for the buyer on trade, and zero otherwise.

An offer strategy is a function $S$ (for the seller) or $B$ (for the buyer) from values to offers. Against $S$, a buyer with value $v$ offering $b$ earns in expectation

$$\pi_b(b, v) = \int \mathbf 1\{S(v_s) \le b\}\,\bigl(v - kb - (1-k)S(v_s)\bigr)\,d\mu_b(v_s),$$

and symmetrically $\pi_s(s, v) = \int \mathbf 1\{s \le B(v_b)\}\,(kB(v_b) + (1-k)s - v)\,d\mu_s(v_b)$. The pair $(S, B)$ is an equilibrium if $B(v)$ maximises $\pi_b(\cdot, v)$ over all real offers for every buyer value $v$, and $S(v)$ maximises $\pi_s(\cdot, v)$ for every seller value $v$.

A strategy is of class $A$ if its offers are bounded, it is nondecreasing, it is strictly increasing except where it sits at its lowest offer $m$ or its highest offer $M$, and it is differentiable wherever its offer lies strictly between $m$ and $M$. A class $A$ equilibrium is an equilibrium in which both strategies are of class $A$.

Formalization targets

Goal: Theorem 2, the linked differential equations

In a class $A$ equilibrium, wherever the seller's strategy is strictly increasing around $y$ and the buyer value $x$ offers $B(x) = S(y)$,

$$k F_b(y) S'(y) + f_b(y) S(y) = x\, f_b(y), \tag{3a}$$

and wherever the buyer's strategy is strictly increasing around $x$ and the seller value $y$ asks $S(y) = B(x)$,

$$(1-k)\bigl(1 - F_s(x)\bigr) B'(x) - f_s(x) B(x) = -\,y\, f_s(x). \tag{3b}$$

The paper writes $x = B^{-1}(S(y))$ in (3a) and $y = S^{-1}(B(x))$ in (3b).

Milestones: the displays of the proof

1. $G_b(S(y)) = F_b(y)$: the buyer's probability that the seller asks at most $S(y)$ equals $F_b(y)$.
2. The buyer's first-order condition: $\partial \pi_b / \partial b = (v - b) g_b(b) - k G_b(b)$ at $b = S(y)$, with offer density $g_b(S(y)) = f_b(y)/S'(y)$, and it vanishes at an equilibrium offer.
3. The seller's first-order condition: $\partial \pi_s / \partial s = (v - s) g_s(s) + (1-k)(1 - G_s(s))$ at $s = B(x)$, and it vanishes at an equilibrium ask.

The milestones assume $S'(y) > 0$ (respectively $B'(x) > 0$), which the paper's formula for the offer density needs. The goal does not assume it.

Significance

Theorem 2 reduces the search for equilibria to the analysis of a pair of ordinary differential equations. Every explicit equilibrium in the paper and in the later $k$-double-auction literature is found as a solution of (3a)–(3b) with suitable boundary conditions: the linear equilibrium for uniform beliefs (the paper's Example 1), the one-parameter families of Satterthwaite–Williams, and the non-linear equilibria of Leininger–Linhart–Radner. The equations also expose how the split parameter $k$ distributes bargaining power: at $k = 1$ equation (3b) forces the seller to ask their own value, and at $k = 0$ equation (3a) forces the buyer to bid theirs.

The result is proved in the paper. To the best of a search of the platform, no formalization of it or of the bargaining model exists. This mission produces a machine-checked version of the necessary conditions. Its definitions of beliefs, expected profits, equilibrium and class $A$ are also the basis for companion missions on the uniform linear equilibrium and its trade probability.

Difficulty

The paper's proof is four lines: differentiate the expected profit, set the derivative to zero, substitute. Three steps of that argument do not survive a careful reading.

First, the paper differentiates under an offer density $g_b$ that exists only if $S$ is strictly increasing and has a positive derivative. Class $A$ allows $S$ to be flat at its bounds, to jump between them, and to have zero derivative. The formal goal assumes none of this. It must handle the case $S'(y) = 0$, where the offer distribution has an infinite density at $S(y)$ and the first-order condition becomes a one-sided argument.

Second, identifying $G_b(S(y))$ with $F_b(y)$ requires that no seller value outside a neighbourhood of $y$ makes the same offer. That is a global statement about $S$, and it is where monotonicity on the whole interval and the "flat only at the bounds" clause of class $A$ enter.

Third, the first-order condition needs the equilibrium offer $S(y)$ to be an interior maximiser of a function of $b$ that is differentiable there. The profit $\pi_b$ is an integral over the belief, and its differentiability at $S(y)$ must be derived from the differentiability of $S$ at the single point $y$ and of $F_b$. Neither $S$ nor $\pi_b$ is assumed continuous elsewhere.

Formalization scope

Values, offers and $k$ are real numbers. Beliefs are probability measures on $\mathbb R$, with distribution function Mathlib's ProbabilityTheory.cdf. Expected profits are Bochner integrals over the opponent's value, not over an offer density. The two agree whenever the density exists, and the integral form needs none. Integrability is not assumed: for a class $A$ strategy and a regular belief supported on the value interval, the integrand is bounded and almost everywhere measurable. Ties ($b = s$) trade. Deviations range over all real offers. Strategies are arbitrary functions $\mathbb R \to \mathbb R$ whose values outside the value interval play no role.

The derivative $S'(y)$ is deriv S y. The paper's inverses $B^{-1}$ and $S^{-1}$ are not introduced as functions. The matching value is a universally quantified variable $x$ with $B(x) = S(y)$, so no junk value of an inverse can make an equation true or false. The equations are asserted only at values $y$ interior to an open subinterval on which $S$ is strictly increasing. A formalization that assumed the first-order condition, or restricted to strategies with $S' > 0$ everywhere, would be a different and weaker theorem.

A complete development needs: differentiation of parametric integrals of indicator type (the derivative of $b \mapsto \int \mathbf 1\{S \le b\}\,h\,d\mu$), the change of variables from values to offers under a strictly increasing strategy, and Fermat's rule (IsLocalMax.hasDerivAt_eq_zero). The first two are reusable for auctions and other Bayesian games with monotone strategies. Proofs of the milestones, alternative proofs of the goal, and general lemmas about monotone strategies are welcome.

Selected references

• K. Chatterjee and W. Samuelson, Bargaining under Incomplete Information, Operations Research 31(5):835–851, 1983. https://doi.org/10.1287/opre.31.5.835
• R. B. Myerson and M. A. Satterthwaite, Efficient Mechanisms for Bilateral Trading, Journal of Economic Theory 29(2):265–281, 1983. https://doi.org/10.1016/0022-0531(83)90048-0
• M. A. Satterthwaite and S. R. Williams, Bilateral Trade with the Sealed Bid k-Double Auction: Existence and Efficiency, Journal of Economic Theory 48(1):107–133, 1989. https://doi.org/10.1016/0022-0531(89)90120-8
• W. Leininger, P. B. Linhart and R. Radner, Equilibria of the Sealed-Bid Mechanism for Bargaining with Incomplete Information, Journal of Economic Theory 48(1):63–106, 1989. https://doi.org/10.1016/0022-0531(89)90121-X

Motivation

Fair division of indivisible goods asks how to split a set of items among agents with different tastes so that nobody has a strong reason to complain. Fairness notions such as envy-freeness up to any good (EFX) and the maximin share (MMS) have been studied extensively as algorithmic targets: given the agents' valuations, compute an allocation satisfying the notion. In practice the valuations are private, and an agent may misreport them to obtain a better bundle. Truthful mechanisms are too weak for this setting: for two agents, no truthful mechanism without payments produces EFX (or even EF1) allocations when there are more than four goods (Amanatidis, Birmpas, Christodoulou, Markakis, EC 2017).

Amanatidis, Birmpas, Fusco, Lazos, Leonardi and Reiffenhäuser (arXiv:2109.08644, Mathematics of Operations Research 2024) take a different route. They let agents bid strategically and ask how fair the pure Nash equilibria of a non-truthful mechanism are with respect to the agents' true valuations. For two agents they study a modified version of the classical cut-and-choose protocol, due in this form to Plaut and Roughgarden (SIAM J. Discrete Math. 2020). They show that it always has equilibria and that all of them are MMS, and hence EFX. As an algorithm run on truthful values, the same mechanism guarantees no more than a $5/6$ fraction of the maximin share.

Setting

There are two agents $N=\{1,2\}$ and a set $M=\{g_1,\dots,g_m\}$ of $m$ indivisible goods. Agent $i$ has a non-negative value $v_i(g)$ for each good and values a bundle $S\subseteq M$ additively, $v_i(S)=\sum_{g\in S}v_i(g)$. There is no free disposal, so an allocation $(A_1,A_2)$ is a partition of $M$.

• EFX (Definition 2.1): for all $i,j$ and every good $g\in A_j$ with $v_i(g)>0$, $v_i(A_i)\ge v_i(A_j\setminus\{g\})$.
• Maximin share (Definition 2.3): $\mu_i=\max_{(X_1,X_2)}\min\{v_i(X_1),v_i(X_2)\}$, the maximum over partitions of $M$ into two bundles. An allocation is MMS if $v_i(A_i)\ge\mu_i$ for both agents.
• Bids: each agent reports a bid vector $\mathbf b_i\in\mathbb R^m_{\ge0}$, and $\mathbf b_i(S)=\sum_{h\in S}\mathbf b_i(h)$.
• Pure Nash equilibrium (Definition 2.7): a bid profile $\mathbf b$ is a PNE of a mechanism $\mathcal M$ if no agent $i$ has a bid $\mathbf b'_i\in\mathbb R^m_{\ge0}$ with $v_i(\mathcal M(\mathbf b'_i,\mathbf b_{-i}))>v_i(\mathcal M(\mathbf b))$.

Mod-Cut&Choose (Mechanism 2) works as follows:

1. It sorts the goods in non-increasing order of agent 1's bid, breaking ties by index.
2. It builds two bundles $E_1,E_2$ greedily: each good goes to the bundle with the smaller $\mathbf b_1$-value, ties to $E_1$.
3. Agent 2 receives the bundle with the larger $\mathbf b_2$-value (ties to $E_1$), and agent 1 receives the other.

In the Lean development these objects are val, IsBestResponse, IsPNE and rank (namespace StrategicAlloc.RRFair, shared with the sibling missions) and IsEFX, mu, IsApproxMMS, cut and modCutChoose (namespace StrategicAlloc.CutChoose).

Formalization targets

Goal: Theorem 4.3 (p. 18)

For every instance with two agents and non-negative additive valuations,

$$\exists\,\mathbf b:\ \mathbf b\text{ is a PNE of Mod-Cut\&Choose},\qquad\text{and}\qquad \forall\,\text{PNE }\mathbf b:\ \mathcal M(\mathbf b)\text{ is MMS and EFX w.r.t. } v_1,v_2 .$$

Both halves are part of the goal. Existence alone, or fairness of equilibria alone, is a weaker statement.

Milestones

1. Theorem 2.5 (p. 5): for two agents every MMS allocation is EFX.
2. §2.1, p. 5: $n\cdot\mu_i(n,S)\le v_i(S)$. This is the published open statement LittleCharity.MMS.mms_le_average, used here as a reference.
3. Lemma 4.1 (p. 17): for every partition $(X_1,X_2)$ of $M$, agent 1 has a non-negative bid under which the cut is $\{E_1,E_2\}=\{X_1,X_2\}$.
4. Corollary 4.2 (p. 18): agent 1 can force a $\mu_1$-partition, i.e. a cut with $\min\{v_1(E_1),v_1(E_2)\}=\mu_1$.
5. Proof of Theorem 4.3, p. 18: agent 2's truthful bid is a best response to every bid of agent 1.
6. Proof of Theorem 4.3, p. 18: with her truthful bid, agent 2 receives at least $v_2(M)/2$.

Significance

The theorem identifies a simple mechanism whose strategic outcomes are as fair as the best allocations that exist for two agents: every MMS allocation is EFX, and an MMS allocation always exists for two agents. The mechanism achieves this without any truthfulness requirement. It is the positive counterpart to the impossibility results for truthful mechanisms. It is also the starting point of §4.2 of the same paper, which asks how much of this guarantee survives for every mechanism whose equilibria are always EFX (Theorems 4.5 and 4.7).

The result is proved in the paper. As far as the platform's catalogue shows, none of it is formalized. This mission produces:

• a machine-checked model of strategic fair division with bids, in which deviations range over all non-negative real bid vectors;
• an executable definition of Mod-Cut&Choose with its exact tie-breaking;
• formal proofs of the "agent 1 can force any cut" lemma and of MMS ⇒ EFX for two agents.

Difficulty

The fairness half is short once its ingredients are available. The weight lies in Lemma 4.1: the cut phase is a greedy procedure over a bid-sorted order, and showing that every partition of $M$ can be produced requires explicit bids and an invariant along the greedy loop. The case where both sets have at least two goods needs carefully calibrated values. The tie-breaking rules (lexicographic sorting, ties to $E_1$ in both phases) enter the argument, and the formalization fixes them exactly.

A natural shortcut is to restrict agent 1's strategies to orderings of the goods, or to assume that any cut is reachable. Either one turns Lemma 4.1 into an assumption. The existence half needs no compactness argument: the set of possible cuts is finite, so a best cut for agent 1 exists, but this has to be connected with deviations over the continuum of real bid vectors.

Formalization scope

• Agents are Fin 2 (agent 1 is 0) and goods are Fin m, indexed in the order $g_1,\dots,g_m$ that lexicographic tie-breaking refers to.
• Valuations and bids are functions Fin 2 → Fin m → ℝ. Non-negativity of $v$ is a hypothesis of every theorem, and every bid in a profile or deviation is required to be non-negative.
• mu v i reuses the published LittleCharity.MMS.mms with two bundles and $S=M$.
• EFX is the paper's Definition 2.1, which removes only goods of positive value. The every-good variant LittleCharity.MMS.IsEFX is not used.
• Disclosed correction: line 2 of Mechanism 2 on the page sorts "w.r.t. $v_1$". A mechanism reads only bids, and the proof of Lemma 4.1 sorts by the declared bids, so the formal mechanism sorts by agent 1's bid $\mathbf b_1$.

The statements rule out the trivializing formalizations. Deviations are not restricted to a subset of bids (rankings, truthful bids, a finite menu). MMS and EFX are measured with the true valuations, never with the bids. The mechanism's tie-breaking is fixed rather than arbitrary.

A complete development needs basic finite-sum and finite-supremum facts and a proof that the greedy cut covers $M$ with disjoint bundles. The model layer (val, IsEFX, IsPNE over all non-negative bids) is shared with the four sibling missions on Round-Robin and on mechanisms with EFX equilibria. Proofs of any milestone, and of mms_le_average, are welcome.

Selected references

• G. Amanatidis, G. Birmpas, F. Fusco, P. Lazos, S. Leonardi, R. Reiffenhäuser, Allocating Indivisible Goods to Strategic Agents: Pure Nash Equilibria and Fairness, Mathematics of Operations Research, 2024; arXiv:2109.08644v2. https://arxiv.org/abs/2109.08644
• B. Plaut, T. Roughgarden, Almost Envy-Freeness with General Valuations, SIAM Journal on Discrete Mathematics 34(2), 2020. https://doi.org/10.1137/19M124397X
• I. Caragiannis, D. Kurokawa, H. Moulin, A. D. Procaccia, N. Shah, J. Wang, The Unreasonable Fairness of Maximum Nash Welfare, ACM Transactions on Economics and Computation 7(3), 2019. https://doi.org/10.1145/3355902
• G. Amanatidis, G. Birmpas, G. Christodoulou, E. Markakis, Truthful Allocation Mechanisms Without Payments: Characterization and Implications on Fairness, EC 2017. https://doi.org/10.1145/3033274.3085147

Motivation

Markets for indivisible goods, in which each participant owns one unit and wants one unit (houses, kidneys in paired donation, dormitory rooms, school seats), cannot be analysed with the convexity assumptions of classical general equilibrium theory. Shapley and Scarf (1974) introduced the housing market to ask whether the two central solution concepts of exchange economies survive indivisibility: the core (allocations no coalition can improve upon by trading among itself) and competitive equilibrium (allocations supported by prices at which every trader optimizes within his budget). Their paper (doi:10.1016/0304-4068(74)90033-0) gives two proofs that the core is nonempty. The first (Section 4) shows that the associated game without side payments is balanced and invokes Scarf's theorem; that is the companion mission of this series. The second (Section 6) is a constructive argument the authors attribute to David Gale, the top trading cycles method, which also produces competitive prices. This mission formalizes the second.

Timeline.

• 1967: Scarf proves that balanced games without side payments have nonempty cores (doi:10.2307/1909383).
• 1974: Shapley and Scarf define the housing market, prove that it has a nonempty core by both arguments, and give Gale's top-trading-cycle construction with competitive prices, allowing indifferences.
• 1977: Roth and Postlewaite show that with strict preferences the competitive allocation is unique and is the unique allocation in the strong core (doi:10.1016/0304-4068(77)90004-0).
• 1982: Roth shows the top-trading-cycles mechanism is strategy-proof under strict preferences (doi:10.1016/0165-1765(82)90003-9).
• 2003: Abdulkadiroğlu and Sönmez adapt top trading cycles to school choice (doi:10.1257/000282803322157061).

Setting

A finite set $N$ of traders each brings one indivisible good; "item $j$" is the good of trader $j$. Preferences are a real matrix $A = (a_{ij})_{i,j\in N}$: trader $i$ prefers item $j$ to item $k$ when $a_{ij} > a_{ik}$ and is indifferent when $a_{ij} = a_{ik}$. Ties are allowed, and only comparisons matter.

An allocation is a bijection $\sigma : N\to N$; trader $i$ receives item $\sigma(i)$. For a coalition $S$, an $S$-permutation $\tau$ reshuffles the items of $S$ among the members of $S$. The allocation $\sigma$ is a core allocation if there is no nonempty $S$ and $S$-permutation $\tau$ with $a_{i\tau(i)} > a_{i\sigma(i)}$ for every $i \in S$.

Prices $\mathrm{price}: N \to \mathbb R$ are competitive for $\sigma$ if each trader $i$, selling his own item for $\mathrm{price}(i)$, can afford $\sigma(i)$, i.e. $\mathrm{price}(\sigma(i)) \le \mathrm{price}(i)$, and no item $k$ with $\mathrm{price}(k) \le \mathrm{price}(i)$ is better for him than $\sigma(i)$.

For $R \subseteq N$, a top trading cycle for $R$ is a nonempty $S \subseteq R$ whose members can be arranged in a cycle $i_1 \to i_2 \to \cdots \to i_s \to i_1$ so that each $i_r$ likes the good of $i_{r+1}$ at least as well as any other good in $R$. A top-trading-cycle partition is

$$N = S^1 \cup S^2 \cup \cdots \cup S^p,$$

with $S^1$ a top trading cycle for $N$ and each $S^j$ a top trading cycle for $N - (S^1\cup\cdots\cup S^{j-1})$. In Lean the partition carries stage : N → Fin p and the successor map next : N → N.

Formalization targets

Goal: Section 6, assertions (1) and (2), p. 114

For every market $A$ and every top-trading-cycle partition with successor map $\mathrm{next}$, the allocation $i \mapsto \mathrm{next}(i)$ is a core allocation, and for every choice of prices

$$\pi^1 > \pi^2 > \cdots > \pi^p > 0$$

on the goods of $S^1,\dots,S^p$ it is competitive. The paper asserts that "a set of competitive prices exists"; its argument works for every such choice, and the goal states that.

Milestones (Section 6, p. 114)

1. Every nonempty $R\subseteq N$ has a top trading cycle.
2. A top-trading-cycle partition of $N$ exists (so the goal is not vacuous and every market has a competitive core allocation).
3. If $j$ is the first index with $S \cap S^j \ne \emptyset$ and $i \in S\cap S^j$, then $a_{ik} \le a_{i\,\mathrm{next}(i)}$ for all $k \in S$.
4. Under the prices $\pi^{\mathrm{stage}(k)}$, the successor's item costs the same as one's own, and every affordable item lies in one's own cycle or a later one.

Example (Section 7, pp. 115–116)

For the matrix $\begin{pmatrix}0&1&2\\1&0&-1\\-1&1&0\end{pmatrix}$ the unique competitive payoff is $(2,1,1)$ at equal prices, while the allocation with payoff $(1,1,0)$ is a core allocation that is competitive at no prices.

Significance

The result gives the existence of a core allocation of every housing market by an explicit construction, and shows that this allocation is competitive, so the competitive solution is nonempty even though goods are indivisible and preferences may have ties. The Section 7 example shows that the inclusion of competitive allocations in the core is strict in general. Under strict preferences, the outcome of the construction is the basis of the matching-market literature: uniqueness of the strong core (Roth–Postlewaite), strategy-proofness (Roth), and the school-choice and kidney-exchange mechanisms built on top trading cycles.

The mathematics is classical and proved. The formalization adds a machine-checked statement of the weak-preference version with the paper's strict blocking notion and its price argument, which existing formal developments do not cover. The closest platform items are AGT.house_core_unique, the strict-preference refinement (Roth–Postlewaite: with strict preferences and weak blocking the core is exactly one allocation), and the school-choice items SchoolChoice.TTC.*. Neither is this statement: the first assumes strict total orders and a different blocking notion, under which the core can be empty once ties are allowed, and says nothing about prices; the second concerns another model with priorities.

Difficulty

Each step is short on paper; the work is in the bookkeeping. The cycle allocation must be shown to be a bijection of $N$ from the stage-by-stage cycle structure; the "chain of best-liked goods that eventually must come back to some earlier element" must be turned into a cycle whose members each get a best good in $R$, with ties handled by a choice rather than by a unique top choice; and the first-stage argument must be carried out with the coalition's reshuffling restricted to its own goods. A tempting shortcut, assuming strict preferences or using a union of cycles at a stage, proves a different statement and is ruled out by the definitions.

Formalization scope

• Traders form an arbitrary finite type N with decidable equality; no nonemptiness is assumed (the empty market has the empty partition). The matrix A : N → N → ℝ has no hypothesis, so ties are allowed.
• Allocations are bijections σ : N → N rather than zero-one matrices. This loses nothing: a coalition in which all members are strictly better off gives each member exactly one item of the coalition (owning nothing is ranked below everything), and an allocation leaving a trader without an item is blocked by that trader alone.
• Blocking is strict for every member of the coalition, as on p. 107; the weak notion (all weakly, one strictly better off) makes assertion (1) false with ties.
• The paper gives no displayed definition of competitive prices. The Lean notion is: $\sigma$ is a bijection, $\mathrm{price}(\sigma(i)) \le \mathrm{price}(i)$, and $\mathrm{price}(k)\le\mathrm{price}(i) \Rightarrow a_{ik}\le a_{i\sigma(i)}$. This transcribes "can sell his own item for $\pi^j$ dollars", "cannot afford", and "his utility is maximized" (p. 114).
• A top trading cycle is a single cycle of the successor map: nonempty, inside $R$, closed under next, every member reaching every other by iterating next. A one-trader cycle with next i = i is allowed (footnote, p. 114).
• Explicit readings of loose phrases: "it is evident" (milestone 1) is an existence statement; "the highest possible payoff available to him in $S$" (milestone 3) is $a_{ik} \le a_{i\,\mathrm{next}(i)}$ for all $k\in S$; "cannot afford any items from $S^1,\dots,S^{j-1}$" (milestone 4) is: price at most $\pi^j$ implies stage at least $j$; "a set of competitive prices exists" (goal) is strengthened to every strictly decreasing positive $\pi$, as the proof gives.
• Trivializing formalizations are ruled out: the partition is quantified over all choices and its existence is a milestone, cycles are required to be nonempty and single, and the budget clause is part of the price notion, so competitiveness does not reduce to "everyone gets a best good".
• Contributions welcome: proofs of the milestones, a computable top-trading-cycle algorithm with a proof that it produces a partition, and a proof of the paper's remark that no other competitive prices exist up to ties.

Selected references

• L. Shapley and H. Scarf, On cores and indivisibility, Journal of Mathematical Economics 1 (1974) 23–37. https://doi.org/10.1016/0304-4068(74)90033-0
• H. Scarf, The core of an N person game, Econometrica 35 (1967) 50–69. https://doi.org/10.2307/1909383
• A. E. Roth and A. Postlewaite, Weak versus strong domination in a market with indivisible goods, Journal of Mathematical Economics 4 (1977) 131–137. https://doi.org/10.1016/0304-4068(77)90004-0
• A. E. Roth, Incentive compatibility in a market with indivisible goods, Economics Letters 9 (1982) 127–132. https://doi.org/10.1016/0165-1765(82)90003-9
• A. Abdulkadiroğlu and T. Sönmez, School choice: a mechanism design approach, American Economic Review 93 (2003) 729–747. https://doi.org/10.1257/000282803322157061

Motivation

Myerson's optimal auction (Myerson 1981) maximizes a seller's expected revenue when buyers have independent private values, but it is a sealed-bid mechanism: every buyer reports a value, and the allocation and payments are computed from all reports at once. Real sellers more often post prices: buyers arrive, each sees a take-it-or-leave-it price, and buys or leaves. Chawla, Hartline, Malec and Sivan (arXiv:0907.2435) ask how much revenue such simple mechanisms lose. Their strongest notion is the order-oblivious posted-price mechanism (OPM): the prices are fixed in advance, and the guarantee must hold whatever order the buyers arrive in, even an adversarial one.

The tool behind the guarantee for sellers of $k$ identical units is a prophet inequality. In the single-choice version, a gambler inspects independent random rewards one at a time and must accept or reject each on the spot; Krengel and Sucheston, and Samuel-Cahn (Ann. Probab. 1984), showed that a single fixed threshold earns at least half of what a prophet who sees all rewards earns. The paper extends Samuel-Cahn's threshold rule to $k$ choices (Appendix D.2) and turns it into a revenue guarantee (Theorem 10).

Setting

There are $n$ agents $[n]$. Agent $i$'s value $v_i$ for being served is drawn independently from a distribution $F_i$ with density $f_i$; the virtual valuation is $\phi_i(v) = v - (1 - F_i(v))/f_i(v)$ (Definition 1), and $F_i$ is regular if $\phi_i$ is non-decreasing (Definition 2). The seller may serve any set of agents in a downward-closed set system $\mathcal J$; this mission uses the $k$-uniform matroid, where a set is feasible exactly when it has at most $k$ members.

A mechanism $M$ maps reported values $\mathbf v$ to an allocation $M(\mathbf v) \in \mathcal J$ and payments $\pi_i(\mathbf v)$. It is truthful if reporting the true value is a dominant strategy and no agent ever gets negative utility. Its expected revenue is $\mathcal R^M = \mathbb E_{\mathbf v}[\sum_i \pi_i(\mathbf v)]$, and $\mathcal R^{\mathcal M}$ denotes the revenue of Myerson's mechanism, the largest over truthful mechanisms (Theorem 19).

Given prices $\mathbf p$ and values $\mathbf v$, agent $i$ desires service if $v_i \ge p_i$. Let $\mathcal S_{\mathbf v}$ be the class of maximal feasible sets of desiring agents. When agents arrive in an arbitrary order and each buys if it desires service and can still be feasibly served, the set of buyers lies in $\mathcal S_{\mathbf v}$. The paper's pessimistic revenue estimate is

$$\mathcal R^{\mathrm{obl}}_{\mathbf p} = \mathbb E_{\mathbf v \sim \mathbf F}\ \min_{S \in \mathcal S_{\mathbf v}} \sum_{i \in S} p_i .$$

For the prophet inequality, $X_1, \dots, X_n$ are independent nonnegative random variables with order statistics $X_{(1)} \ge \dots \ge X_{(n)}$, and $(x)^+ = \max(0, x)$. The threshold rule with threshold $c$ picks indices $t_1(c), \dots, t_k(c)$, where $t_i(c)$ is the lesser of $n-k+i$ and the $i$-th smallest index $j$ with $X_j \ge c$ (or $n - k + i$ if there is none). The numbers $a^*$ and $b^*$ are the unique solutions of

$$a = \sum_{i=1}^k \mathbb E\big(X_{(i)} - a/k\big)^+, \qquad b = \sum_{i=1}^n \mathbb E\big(X_i - b/k\big)^+ .$$

Formalization targets

Goal: Theorem 10 (p. 9)

$$\exists\, \mathbf p\ \ \forall M \text{ truthful}:\qquad \mathcal R^M \le 2\, \mathcal R^{\mathrm{obl}}_{\mathbf p}$$

for every instance with regular distributions and a $k$-uniform matroid constraint. The prices are chosen once, before the mechanism it is compared with; this is the paper's "$\mathcal R^{\mathrm{obl}}_{\mathbf p}$ 2-approximates $\mathcal R^{\mathcal M}$".

Milestones

1. Proposition 1 (p. 5): under regularity, the expected revenue of a truthful mechanism equals its expected virtual surplus $\mathbb E[\sum_{i \in M(\mathbf v)} \phi_i(v_i)]$ (with the lowest type receiving zero utility).
2. $a^*$ and $b^*$ exist and are unique (App. D.2, p. 18).
3. The claim $a^* \le b^*$ (App. D.2, p. 18).
4. Theorem 24 (p. 18), the $k$-choice prophet inequality: for $a^* \le k c \le b^*$,

$$\sum_{i=1}^k \mathbb E\big[X_{(i)}\big] \le 2 \sum_{i=1}^k \mathbb E\big[X_{t_i(c)}\big].$$

Significance

The theorem says that a seller of $k$ identical units can fix one price per buyer, ignore the arrival order entirely, and still collect half of the optimal revenue. The factor 2 is tight: Appendix D.2 gives a single-item example with two buyers where no order-oblivious pricing does better. Corollary 11 extends the result to partition matroids, and Theorem 24 is reused for the graphical-matroid result (Theorem 12, App. D.3). Theorem 24 is a statement in optimal stopping independent of mechanism design, and $k$-choice prophet inequalities are now a standard tool for online allocation.

The results are proved in the paper (preprint arXiv:0907.2435v2; a conference version appeared at STOC 2010). To our knowledge none of them, nor any prophet inequality, has a machine-checked proof; Mathlib has independence of random variables but no order statistics, stopping-rule prophet inequalities, or Myerson's revenue characterization in this multi-agent dominant-strategy form. A related single-unit, Bayesian-incentive-compatible form of Proposition 1 exists on the platform (MechanismDesign.Auctions.revenue_eq_virtual_surplus), in a different model.

Difficulty

The threshold rule picks the first values above $c$, not the largest, and its picks are dependent random indices; the expectation $\mathbb E[X_{t_i(c)}]$ does not factor. The obvious comparison of the gambler with the prophet term by term fails, because the gambler can exhaust its $k$ picks on early, small values. The bound has to balance two events: either at least $k$ values reach $c$, or a value is picked whenever it exceeds $c$; independence enters exactly in the second. The rule also has forced picks at the end of the sequence, which must be handled as stated.

On the mechanism side, $\mathcal R^{\mathrm{obl}}_{\mathbf p}$ is a minimum over an adversarially chosen family, not the revenue of one run, so it cannot be read off from a single sequential mechanism. Proposition 1 needs the full revenue-equivalence argument: monotone allocations, the payment identity, and an integration by parts against the density.

Formalization scope

• Distributions: each $F_i$ has a bounded support $[\underline v_i, \overline v_i]$ with $0 \le \underline v_i$, and a measurable density positive on it (a pinned convention; the paper says only "with density $f_i$"). Regularity is required on the support. The prior is the product of the marginals.
• Mechanisms: deterministic, dominant-strategy incentive compatible and ex-post individually rational on the type space, with measurable allocation events and measurable, integrable payments. Payments of unserved agents are not forced to be zero.
• $\mathcal R^{\mathcal M}$ is not constructed. The goal is stated against every truthful mechanism, which by Theorem 19 is equivalent. Quantifier order matters: "for every mechanism there are prices" is a weaker statement and is not the goal.
• Proposition 1 carries the normalization that an agent of the lowest type gets zero utility, which the paper presupposes on p. 12.
• $\mathcal R^{\mathrm{obl}}_{\mathbf p}$ is a genuine minimum over the finite, nonempty family $\mathcal S_{\mathbf v}$; maximality is essential, since without it the empty set makes the estimate $0$ and the goal false. Prices are arbitrary reals.
• $a^*$ and $b^*$ are characterised by their equations as hypotheses, not defined by an infimum. Order statistics count multiplicity. Lean indices are 0-based. The threshold rule includes the page's forced picks $t_i(c) = n - k + i$; it is not replaced by a pure threshold rule. Theorem 24 and the claims about $a^*, b^*$ assume $1 \le k \le n$; the goal assumes nothing about $k$.
• Out of scope: non-regular distributions (ironing), Corollary 11, and the p. 19 identity rewriting $\mathcal R^{\mathrm{obl}}_{\mathbf p}$ as a sum of virtual values (a proof step, not a milestone).

Useful reusable infrastructure: order statistics and their measurability, Samuel-Cahn-type threshold rules, and Myerson's payment identity for dominant-strategy mechanisms. Proofs of any milestone, and supporting lemmas on these objects, are welcome.

Selected references

• S. Chawla, J. D. Hartline, D. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, arXiv:0907.2435v2, 2010 (STOC 2010). https://arxiv.org/abs/0907.2435
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• E. Samuel-Cahn, Comparison of Threshold Stop Rules and Maximum for Independent Nonnegative Random Variables, Annals of Probability 12(4), 1984. https://doi.org/10.1214/aop/1176993150

Motivation

A seller who knows the distributions of buyers' values can maximise expected revenue with Myerson's optimal mechanism (Myerson 1981): collect bids, compute virtual values, serve a feasible set of maximum virtual surplus, and charge threshold payments. Real sellers seldom run such auctions. They post prices: a buyer is offered a take-it-or-leave-it price and either accepts or walks away. Posted prices need no bidding, involve no competition between buyers, and are trivially truthful. The question is how much revenue they give up.

Chawla, Hartline, Malec and Sivan (arXiv:0907.2435, STOC 2010) answer this for a range of feasibility constraints with a single construction, the sequential posted-price mechanism (SPM) $\mathcal S$. For general matroids it loses at most a factor $2$ (Theorem 5). For uniform and partition matroids, that is, multi-unit sales and unions of multi-unit sales, it loses at most a factor $e/(e-1)\approx1.58$ (Theorem 6), and the paper shows this factor is tight for its mechanism. This mission targets Theorem 6.

Timeline. Myerson (1981) characterised the optimal single-parameter mechanism. Blumrosen and Holenstein (2008) showed that the best single-unit SPM can be a factor $\sqrt{\pi/2}$ below Myerson's revenue even with i.i.d. buyers. Chawla, Hartline and Kleinberg (EC 2007) used posted prices to approximate multi-parameter unit-demand pricing. Chawla, Hartline, Malec and Sivan (2010) gave the matroid, partition-matroid and matroid-intersection bounds. Yan (SODA 2011) explained the $e/(e-1)$ factor through the correlation gap of submodular functions and sharpened it for $k$ units to $1-k^ke^{-k}/k!$.

Setting

There are $n$ agents. Agent $i$ has a private value $v_i$ for being served, drawn independently from a distribution $F_i$ with density $f_i$. The virtual value is $\varphi_i(v)=v-\frac{1-F_i(v)}{f_i(v)}$, and $F_i$ is regular if $\varphi_i$ is non-decreasing. The seller may serve any set in a downward-closed family $\mathcal J\subseteq2^{[n]}$.

A partition matroid assigns each agent $i$ to a part $\mathrm{part}(i)$ and each part $b$ a capacity $\mathrm{cap}(b)\in\mathbb N$. A set is feasible iff it contains at most $\mathrm{cap}(b)$ agents of every part $b$. With one part of capacity $k$ this is the $k$-uniform matroid: at most $k$ agents are served.

A truthful mechanism $M$ maps a value vector $\mathbf v$ to a feasible set $M(\mathbf v)$ and payments $\pi_i(\mathbf v)$. It is dominant-strategy incentive compatible and individually rational. Its expected revenue is $\mathcal R^M=\mathbb E[\sum_i\pi_i(\mathbf v)]$, and $q^M_i=\Pr[i\in M(\mathbf v)]$ is its service probability for agent $i$.

The sequential posted-price mechanism $\mathcal S$ built from $M$ sets the price $p_i=F_i^{-1}(1-q^M_i)$ for agent $i$, so that agent $i$ accepts with probability exactly $q^M_i$. It approaches the agents one at a time in decreasing order of price ($\sigma$ is the ordering). It offers agent $i$ the price $p_i$ if adding $i$ to the agents already served keeps the set feasible. The agent accepts iff $p_i\le v_i$. Its expected revenue is $\mathcal R^\sigma_{\mathbf p}$.

Formalization targets

Goal: Theorem 6, partition matroids

For every partition matroid, every truthful $M$, and $\mathcal S$ built from $M$ as above,

$$\mathcal R^M\le\frac{e}{e-1}\,\mathcal R^\sigma_{\mathbf p}.$$

Taking $M$ to be Myerson's mechanism gives the paper's statement.

Milestones

1. Lemma 2 (regular case): $\mathcal R^M\le\sum_ip^M_iq^M_i$ with $p^M_i=F_i^{-1}(1-q^M_i)$.
2. Rank bound (§4): $\sum_{i\in S}q^M_i\le\operatorname{rank}(S)$ for every set $S$; for a part $b$ this reads $\sum_{\mathrm{part}(i)=b}q^M_i\le\mathrm{cap}(b)$.
3. Single-unit revenue formula (App. C.2): $\mathcal R^{\mathcal S}=\sum_kc_kp_kq_k$ with $c_k=\prod_{j<k}(1-q_j)$, positions in offer order.
4. Lemma 20: with $p$ defined by $\sum_kp_kq_k=p\sum_kq_k$ (equation (2)) and prices decreasing, $p\sum_kc_kq_k\le\sum_kc_kp_kq_k$.
5. Display (3): if $\sum_kq_k=s\le1$, then $p\sum_kc_kq_k=p(1-\prod_k(1-q_k))\ge p(1-(1-s/n)^n)\ge(1-1/e)ps$.
6. Theorem 21: the goal for the $1$-uniform matroid.
7. Theorem 22: the goal for the $k$-uniform matroid, every $k$.

Significance

The theorem shows that a mechanism with no bidding loses at most about $37\%$ of the optimal revenue when the constraint is a union of multi-unit supplies. That covers selling several kinds of goods, each in limited stock, to single-minded buyers. The prices are computed once from the distributions. The order is fixed before any value is seen. No agent's payment depends on another agent's report. The factor is tight for this mechanism (App. C.2), and the same template (prices from service probabilities, decreasing order) gives factor $2$ for all matroids and $m+1$ for intersections of $m$ matroids.

On the formal side, the paper's results are proved but none is machine-checked as far as we know. The platform has Myerson-type results for a single unit with Bayesian incentive compatibility and a common support (Börgers), and for i.i.d. buyers with a fixed number of units (Talluri and van Ryzin). Neither covers independent, non-identical buyers under a set-system constraint with dominant-strategy truthfulness. A complete development would include the ex-ante revenue bound of Lemma 2 for regular distributions, which is reusable for any posted-price or prophet-inequality argument, and the $1-1/e$ correlation-gap inequality.

Difficulty

The obvious argument compares $\mathcal S$ with Myerson's mechanism one agent at a time. That fails, because $\mathcal S$ may stop offering to an agent once the units of its part are gone, and the agents blocked this way can be the ones Myerson's mechanism serves. The loss has to be bounded in aggregate, using only the ex-ante constraint $\sum_{\mathrm{part}(i)=b}q_i\le\mathrm{cap}(b)$. The single-unit case reduces to an inequality about products $\prod(1-q_j)$. For $k$ units, the printed proof (pp. 15–16) is an induction that compares the run with a hypothetical single-unit instance with probabilities $q_i/k$. Its second case is informal, so a formal proof needs its own argument for the $k$-unit bound. Passing from uniform to partition matroids needs the observation that with a global order the run inside each part depends only on that part's agents. Lemma 2 needs the revenue-curve concavity that regularity gives, stated through densities rather than derivatives.

Formalization scope

• Values. Each $F_i$ has a density that is measurable and strictly positive on a bounded interval $[\underline v_i,\bar v_i]$ with $0\le\underline v_i$, integrates to $1$ there, and has no mass outside. The paper says only "with density $f_i$". This pin rules out point masses, so the randomised-price variant of $\mathcal S$ never arises. The prior is the product of these laws.
• Regularity is $\varphi_i$ non-decreasing on the support, assumed for every agent in the goal, as in the paper's §4 analyses. The non-regular extension (second paragraph of Lemma 2, Appendix E) is out of scope.
• Truthful means deterministic, dominant-strategy incentive compatible over the support, ex-post individually rational, feasible, with measurable allocations and integrable payments.
• Prices are arguments tied to $M$ by $p_i\in[\underline v_i,\bar v_i]$ and $F_i(p_i)=1-q^M_i$. No inverse distribution function is defined.
• Order. The order $\sigma$ is a permutation with $\sigma(0)$ first, decreasing in price, and ties are arbitrary. It is global across parts. Parts of capacity $0$ are allowed.
• Constant. The constant is exactly $e/(e-1)$.
• No free prices. The theorem is not stated with free or existentially chosen prices. Prices are pinned to $M$'s service probabilities, and $\mathcal S$ uses the same constraint as $M$. A statement in which the prices could be chosen after the fact, or in which $M$ were not required to be individually rational, would be a different or false theorem.
• Every truthful $M$. The comparison is with every truthful $M$, not with a constructed Myerson mechanism. This form is at least as strong as the paper's, and it is what the paper's proof shows.

Welcome contributions: proofs of the algebraic milestones (Lemma 20, display (3)), the revenue formula, Lemma 2 (reusable payment-identity infrastructure for dominant-strategy mechanisms), and a correlation-gap argument for $k$ units.

Selected references

• S. Chawla, J. D. Hartline, D. L. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, STOC 2010; arXiv:0907.2435v2, 2010. https://arxiv.org/abs/0907.2435
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• L. Blumrosen, T. Holenstein, Posted Prices vs. Negotiations: An Asymptotic Analysis, ACM EC 2008.
• Q. Yan, Mechanism Design via Correlation Gap, ACM-SIAM SODA 2011.