All missions

Why the eluder dimension

A structured bandit is a repeated decision problem in which a learner picks a decision $\pi^t$ from a set $\Pi$ and observes a noisy reward. The set $\Pi$ can be large or continuous: a dosage, a price vector, a path in a graph. Treating each decision separately costs regret of order $\sqrt{|\Pi|T}$, which is useless when $\Pi$ is large relative to the horizon $T$. The learner must generalize across decisions through a function class $\mathcal F$ that is assumed to contain the true mean reward. Knowing that the mean reward is in $\mathcal F$ is not enough on its own: in Example 4.1 of the notes, a class of $A$ needle functions has $\log|\mathcal F|=\log A$, yet regret of order $A$ is unavoidable. A guarantee therefore needs a second complexity measure, one that says how much is learned about one decision from others.

The eluder dimension of Russo and Van Roy (NeurIPS 2013) is such a measure. It was introduced to analyse optimistic algorithms and posterior sampling for general function classes, and it remains the standard yardstick for optimism beyond linear models. This mission is number XI in the formalization of Foster and Rakhlin's lecture notes (arXiv:2312.16730), and it covers §4.1.1 and §4.1.2.

Setting

Let $\Pi$ be an arbitrary set of decisions. In each round $t=1,\dots,T$ the learner selects $\pi^t\in\Pi$ and observes $r^t\in[0,1]$, drawn from a fixed model $M^\star(\cdot\mid\pi^t)$. The mean reward is $f^\star(\pi)=\mathbb E[r\mid\pi]$, and regret is $\mathrm{Reg}=\sum_{t=1}^T\bigl(f^\star(\pi^\star)-f^\star(\pi^t)\bigr)$, with $\pi^\star$ a maximizer of $f^\star$. The learner knows a finite class $\mathcal F\subset(\Pi\to[0,1])$ with $f^\star\in\mathcal F$.

Generalized UCB forms the empirical minimizer $\hat f^t$ of the square loss on the first $t-1$ rounds, keeps every function whose empirical loss is within $\beta=8\log(|\mathcal F|/\delta)$ of it, in a confidence set $\mathcal F^t$, and plays a maximizer of the upper confidence bound $\bar f^t(\pi)=\max_{f\in\mathcal F^t}f(\pi)$.

A sequence $\pi^1,\dots,\pi^d$ is $\varepsilon$-elusive for $f^\star$ if for each $t$ some $f^t\in\mathcal F$ has $|f^t(\pi^t)-f^\star(\pi^t)|>\varepsilon$ and $\sum_{i<t}(f^t(\pi^i)-f^\star(\pi^i))^2\le\varepsilon^2$. The first layer of the dimension is the length $\underline{\mathrm{Edim}}_{f^\star}(\mathcal F,\varepsilon)$ of the longest such sequence. The eluder dimension is its monotone version, floored at one, maximized over the class:

$$\mathrm{Edim}_{f^\star}(\mathcal F,\varepsilon)=\sup_{\varepsilon'\ge\varepsilon}\underline{\mathrm{Edim}}_{f^\star}(\mathcal F,\varepsilon')\vee1,\qquad \mathrm{Edim}(\mathcal F,\varepsilon)=\max_{f^\star\in\mathcal F}\mathrm{Edim}_{f^\star}(\mathcal F,\varepsilon).$$

Formalization targets

Goal: Proposition 12

With probability at least $1-\delta$,

$$\mathrm{Reg}\lesssim\inf_{\varepsilon>0}\Bigl\{\sqrt{\mathrm{Edim}(\mathcal F,\varepsilon)\cdot T\log(|\mathcal F|/\delta)}+\varepsilon T\Bigr\}\lesssim\sqrt{\mathrm{Edim}(\mathcal F,T^{-1/2})\cdot T\log(|\mathcal F|/\delta)},$$

with one absolute constant. The goal fixes no constant, so it survives any sharpening of the argument.

Intermediate targets

• Lemma 10, structured form: with probability at least $1-\delta$, $f^\star$ stays in every confidence set and every function in $\mathcal F^\tau$ has cumulative squared error at most $4\beta$ against $f^\star$ on the past.
• (4.7): on that event, regret is at most the upper confidence width.
• The regret-to-width step, p. 61: $\mathrm{Reg}\le\sum_t w^t(\pi^t)$, for the width $w^t$ over functions close to $f^\star$ on the past.
• Lemma 12: $\sum_{t=1}^T\mathbb I\{w^t(\pi^t)>\alpha\}\le(\beta/\alpha^2+1)\,\underline{\mathrm{Edim}}_{f^\star}(\mathcal F,\alpha)$ for every sequence and every $\alpha>0$.
• (4.13), (4.14) and the two displays after them: the deterministic reduction of $\sum_t w^t(\pi^t)$ to the eluder dimension.

Significance

The theorem has no dependence on $|\Pi|$. For linear models the eluder dimension is of order $d\log(1/\varepsilon)$, which recovers the LinUCB rate $\sqrt{dT}$ up to logarithms, and for generalized linear models with link derivative in $(\mu,L)$ it gains a factor $L^2/\mu^2$. It also shows the limits of the approach: a single ReLU neuron has eluder dimension exponential in $d$ (Li et al.). The result is the reference point against which the Decision-Estimation Coefficient of the later chapters is compared.

The result is proved in the literature, so nothing here is open. The eluder dimension has no prior formal treatment on the platform. The mission contributes that definition, in a form usable for any class, together with a combinatorial lemma that makes no reference to probability, and a concentration statement for least-squares confidence sets under an arbitrary adaptive algorithm that the contextual and reinforcement-learning chapters can reuse. The platform's FoundationsRL.Bandits.optimism_lemma is stated for finitely many decisions, so it does not carry over to this setting.

Difficulty

The obvious argument stops at (4.7). The confidence set constrains a function on the decisions already played, while the regret is charged at the new decision $\pi^t$, and in general good fit on the past says nothing about a new point. The eluder dimension bounds the number of rounds on which the two can disagree, but its definition has a single scale: squared error $\varepsilon^2$ on the past and a surprise of $\varepsilon$. The confidence sets have a fixed radius $\beta$ which is much larger than $\varepsilon^2$ for small widths. The central step is Lemma 12, which must control the count of large widths at every scale at once, and the elliptical-potential argument for linear models has no analogue for a general class.

The confidence sets themselves need a concentration inequality for dependent data: the decisions are chosen adaptively, so the square loss differences do not form an independent sequence.

Formalization scope

Decisions live in an arbitrary type with no finiteness assumption. The class is a Set of real functions, F.Finite in the goal and arbitrary in Lemma 12. The dimension takes values in ℕ∞, with edimRaw for the underlined quantity and edimFstar, edim for the two layers built from it. The bound is stated in ℝ≥0∞, so it is vacuous, not false, when the dimension is infinite. The argmax over $\Pi$ is presupposed by the source's notation, so a run of the algorithm has the maximizer as a hypothesis, and the regret comparator is a supremum. The first clause of (4.9) is strict and the second is not. Rounds are numbered from $1$, as in the notes. The width of Lemma 12 is extended-real valued, because a real supremum would return a junk value on an unbounded class.

The conditional law of the reward is stated on measurable sets for an arbitrary filtration. The constant in the goal is existential and quantified before the types, so it cannot depend on $\Pi$, $\mathcal F$ or $T$. A trivializing reading, in which regret is measured against a fixed decision rather than the best one, or in which the supremum in the width collapses, is ruled out by these conventions.

Contributions are welcome on the eluder-dimension combinatorics, which are reusable beyond this mission, and on the concentration lemma, whose martingale argument also serves the contextual form of Lemma 10.

Selected references

• D. J. Foster, A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, lecture notes, 2023. arXiv:2312.16730v1
• D. Russo, B. Van Roy, Eluder Dimension and the Sample Complexity of Optimistic Exploration, NeurIPS 2013, pp. 2256–2264. Proceedings
• G. Li, P. Kamath, D. J. Foster, N. Srebro, Eluder Dimension and Generalized Rank, 2021. arXiv:2104.06970

Motivation

Many learning systems serve several populations at once: a recommender serves user segments, a clinical dosing rule serves patient subgroups, an online marketplace serves customer types. When these populations share the same unknown options, the exploration one population performs also informs the others. A policy that minimizes total regret decides who bears that exploration cost, and it can load the whole cost onto one group. Baek and Farias (arXiv:2106.02553v2) make this precise with the axiomatic bargaining framework of Nash (1950): each group's utility is the regret it saves relative to learning on its own, and a fair policy maximizes the Nash social welfare, the sum of the logarithms of these savings. Their Theorem 1 shows that regret-optimal policies such as KL-UCB give some group zero savings, so they are maximally unfair in this sense. Their Theorem 3, the goal of this mission, shows that a different policy, PF-UCB, attains the largest welfare any consistent policy can reach.

Setting

A grouped $K$-armed bandit has a finite set of groups $G$ and arms $\mathcal A=[K]$. Group $g$ can pull only the arms $\mathcal A^g\subseteq\mathcal A$; $G_a$ is the set of groups connected to arm $a$. At each time $t=1,2,\dots$ a group $g_t$ arrives, independently, with probability $p_g$; the decision maker sees $g_t$, pulls an arm $A_t\in\mathcal A^{g_t}$ and observes a reward drawn from $\mathrm{Normal}(\theta(a),1)$, where $\theta\in(0,1)^K$ has distinct entries and is unknown. Write $\mathrm{OPT}(g)=\max_{a\in\mathcal A^g}\theta(a)$, $\Delta^g(a)=\mathrm{OPT}(g)-\theta(a)$, $\mathrm{KL}(\alpha,\beta)=(\alpha-\beta)^2/2$ and $J^g(a)=1/\mathrm{KL}(\theta(a),\mathrm{OPT}(g))$. The group regret of a policy $\pi$ is

$$R^g_T(\pi,\mathcal I)=\mathbb E\Big[\sum_{t=1}^T\mathbf 1(g_t=g)\big(\mathrm{OPT}(g_t)-\theta(A_t)\big)\Big].$$

The disagreement point of group $g$ is $\tilde R^g_T(\mathcal I)$, the regret of the KL-UCB policy on the single-group instance $\mathcal I_g$, in which every other group can only pull a null arm of mean $0$. The utility gain and the Nash social welfare are

$$\mathrm{UtilGain}^g(\pi,\mathcal I)=\liminf_{T\to\infty}\frac{\tilde R^g_T(\mathcal I)-R^g_T(\pi,\mathcal I)}{\log T},\qquad SW(\pi,\mathcal I)=\sum_{g\in G}\log\mathrm{UtilGain}^g(\pi,\mathcal I),$$

with $\log u=-\infty$ for $u\le0$.

With $\mathcal A^g_{\mathrm{sub}}=\{a\in\mathcal A^g:\theta(a)<\mathrm{OPT}(g)\}$, $\mathcal A_{\mathrm{sub}}$ the arms optimal for no group, and $J(a)=\max_{g\in G_a}J^g(a)$, the welfare bound is the value of the concave program (13):

$$Y^*(\mathcal I)=\max_{q\ge0}\sum_{g}\log\Big(\sum_{a\in\mathcal A^g_{\mathrm{sub}}}\Delta^g(a)\big(J^g(a)-q^g(a)J(a)\big)\Big)\ \ \text{s.t.}\ \sum_g q^g(a)=1\ (a\in\mathcal A_{\mathrm{sub}}),\ q^g(a)=0\ (a\notin\mathcal A_{\mathrm{sub}}\cap\mathcal A^g).$$

Here $q^g(a)$ is the share of the exploration of arm $a$ carried by group $g$. PF-UCB solves the same program at the empirical means, takes the optimal solution of smallest Euclidean norm $\hat q_t$, and at time $t$ pulls an arm that has the highest UCB for some group and that $g_t$ has pulled at most $\hat q^{g_t}_t(a)N_t(a)$ times; if there is none, it pulls the greedy arm.

Formalization targets

Goal: Theorem 3

$$SW(\pi^{\mathrm{PF\text{-}UCB}},\mathcal I)=Y^*(\mathcal I)$$

for every instance: every finite group and arm set, every bipartite graph $(\mathcal A^g)_g$, every arrival law with $p_g>0$, every $\theta\in(0,1)^K$ with distinct entries, and every tie-breaking rule of the policies.

Milestones

In the order of the proof in Appendix E:

• the minimum-norm optimal solution of (13) exists and is unique for every parameter vector (§4.1);
• the policy-free lemmas: Lemma 1 (UCB validity) and Lemma 3 (concentration of pulled arms);
• the lower bounds: Proposition 10 (Lai–Robbins for consistent policies), Propositions 8 and 9 and Lemma 4 (log-consistent policies);
• the disagreement point: Proposition 1, $\tilde R^g_T/\log T\to\sum_{a\in\mathcal A^g}\Delta^g(a)J^g(a)$;
• the analysis of PF-UCB: Lemma 9 (log-consistency), Propositions 2 and 4 and Lemma 6 (negligible pulls), Proposition 3 (stability of the minimum-norm solution), Proposition 11 ($\mathbb E[N_T(a)]/\log T\to J(a)$);
• Theorem 9: $R^g_T(\pi^{\mathrm{PF\text{-}UCB}},\mathcal I)/\log T\to\sum_{a\in\mathcal A^g}\Delta^g(a)q^g_*(a)J(a)$.

Significance

Theorem 2 of the paper bounds $SW(\pi,\mathcal I)\le Y^*(\mathcal I)$ for every consistent policy, so Theorem 3 makes PF-UCB the Nash solution: it is proportionally fair across groups in every instance. It also makes the fairness question quantitative. The same program measures the price of fairness, the share of the regret reduction lost to fairness, which the paper bounds in Theorem 4. Theorem 9 gives an exact asymptotic description of the group regrets: who explores which arm, and at what rate.

The result is proved in the paper; nothing in this mission is open mathematics. No part of it is machine-checked. A complete formalization would give the first verified asymptotic analysis of a grouped (contextual) bandit policy, and it produces reusable components: a grouped bandit model with fixed action sets, KL-UCB for Gaussian rewards with the $\log t+3\log\log t$ exploration level, change-of-measure lower bounds of Lai–Robbins type, and a stability result for minimum-norm solutions of a parametric concave program. Shorter proofs of any milestone, and a proof of Proposition 1 by reduction to a published KL-UCB analysis, are welcome.

Difficulty

The welfare is a sum of logarithms of liminfs, so the goal needs exact first-order constants: every group's regret must be pinned to $\log T$ times the right constant, not bounded by it. Two parts of the argument resist the obvious approach.

First, the program (13) need not have a unique optimal solution, and PF-UCB tracks the minimum-norm one. Proposition 3 says the minimum-norm solutions at nearby parameters are close. This is not a consequence of continuity of the optimal value, and it fails for an arbitrary choice of optimal solutions. The proof in the paper goes through a polytope-distance argument whose uniform bound needs care where the constraint matrix loses rank.

Second, the paper's proofs of Lemma 9 and Proposition 2 cite each other: Proposition 2 uses Proposition 9, which assumes log-consistency, and Lemma 9's proof of log-consistency uses Proposition 2. A formal proof has to break this circle, for example by a direct proof that PF-UCB is log-consistent.

Formalization scope

The probability space is explicit: i.i.d. arrivals with law $p$, one i.i.d. $\mathrm{Normal}(\theta(a),1)$ reward stack per arm, and an i.i.d. uniform draw per step for the policy's randomization. The reward of a pull is the next unused entry of the arm's stack, as on p.6. A policy is one rule for every $\theta$; it sees the past groups, arms and rewards, the arriving group and its draw. Lean step $s$ is paper time $s+1$.

The committed conventions are these.

• Expectations are lower Lebesgue integrals of nonnegative quantities.
• $\mathrm{UtilGain}$, $SW$ and $Y^*$ are extended reals with $\log u=-\infty$ for $u\le0$; $Y^*$ is the supremum of the objective over the feasible set.
• The UCB level is $f(t)=\log t+3\log\log t$ for $t\ge3$ with $f(1)=f(2)=f(3)$; an unpulled arm has UCB $+\infty$ and empirical mean $0$.
• Every arg max is resolved by a tie-breaking rule that is a parameter of the theorems.
• $O(\cdot)$ means $\exists C,T_0,\ \forall T\ge T_0$, with the constant chosen after the instance.
• One correction: every group arrives with positive probability, since with $p=(1,0)$ the printed statement fails.
• Every group has an arm and every arm a group, which excludes only cases where $\mathrm{OPT}(g)$ or $J(a)$ is undefined.

The minimum-norm solution is defined by choice; the first milestone states that it exists and is unique, so the definition is the intended object. An $\mathbb R$-valued welfare (with $\log0=0$) or a Bochner expectation of a non-measurable regret would trivialize the goal; both are ruled out by the choices above.

Selected references

• J. Baek and V. F. Farias, Fair Exploration via Axiomatic Bargaining, arXiv:2106.02553v2, 2022. https://arxiv.org/abs/2106.02553
• J. F. Nash, The Bargaining Problem, Econometrica 18(2), 1950. https://doi.org/10.2307/1907266
• A. Garivier and O. Cappé, The KL-UCB Algorithm for Bounded Stochastic Bandits and Beyond, COLT 2011. https://arxiv.org/abs/1102.2490
• T. L. Lai and H. Robbins, Asymptotically Efficient Adaptive Allocation Rules, Advances in Applied Mathematics 6(1), 1985. https://doi.org/10.1016/0196-8858(85)90002-8
• D. Bertsimas, V. F. Farias and N. Trichakis, The Price of Fairness, Operations Research 59(1), 2011. https://doi.org/10.1287/opre.1100.0865

Motivation

Prizes and patents reward the first innovator to fill a market niche. How generous the reward should be depends on how often useful ideas arrive, and a policy maker rarely knows that rate. Basov, Erkal, Minehart and Scotchmer (SSRN 4628270, 2024; published in Management Science, doi:10.1287/mnsc.2023.03362) model ideas as scarce: they arrive at the times of a Poisson process, each to a different person, and an idea that is not used is lost. A reward then works as a screen. Ideas whose cost is below the reward are developed, and the rest are discarded. The planner trades the cost of the innovation against the delay before it arrives.

The question is how this trade-off changes over time when the arrival rate of ideas is unknown. Each period in which the reward goes unclaimed is evidence that ideas are scarce. The paper shows that the optimal reward rises with the delay and that expected welfare falls. The model belongs to the family of optimal stopping and real-options problems with Bayesian learning (compare Mason and Välimäki, 2011, with two possible arrival rates). Here the planner's belief is a whole density on $\mathbb R_+$, and the paper shows that one scalar state variable still suffices.

Setting

A niche, once filled, has social value $v/r$, where $r>0$ is the discount rate. Each idea has an R&D cost $c$ drawn from a continuous cost density $f>0$ on its support $[\underline c,\overline c]\subset\mathbb R_+$, with distribution function $F(x)=\int_{\underline c}^{x}f$. Throughout, $\underline c<v/r<\overline c$. At time $t$ the planner offers a reward $p(t)\in[\underline c,\overline c]$. An idea that arrives at time $t$ is developed exactly when its cost is at most $p(t)$, which happens with probability $F(p(t))$.

Ideas arrive at an unknown rate $\lambda$. The planner's prior is a density $h_0$ on $[0,\infty)$, and Assumption 1 requires $h_0$ to be continuous and bounded, to have finite moments of every order, and to satisfy $h_0(0)>0$. The cumulative innovation incentive $\phi(t)=\int_0^tF(p(s))\,ds$ is a sufficient statistic: given that no innovation has occurred, the posterior is $h_\phi(\lambda)=h_0(\lambda)e^{-\lambda\phi}/Z(\phi)$ with $Z(\phi)=\int_0^\infty h_0(\lambda)e^{-\lambda\phi}d\lambda$. Its moments are $m_k(\phi)=\int_0^\infty\lambda^kh_\phi(\lambda)\,d\lambda$.

The expected welfare of a reward policy $u$ from state $\phi$ is

$$J(\phi,u)=\int_0^\infty e^{-rt}\,\frac{\int_0^\infty\lambda h_0(\lambda)e^{-\lambda\Phi(t)}d\lambda}{Z(\phi)}\int_{\underline c}^{u(t)}\Bigl(\frac vr-c\Bigr)f(c)\,dc\,dt,\qquad \Phi(t)=\phi+\int_0^tF(u(s))ds .$$

The value function is $V(\phi)=\sup_uJ(\phi,u)$, taken over all admissible policies. It satisfies the Hamilton–Jacobi–Bellman equation

$$0=\max_{p\in[\underline c,\overline c]}\Bigl\{m_1(\phi)\int_{\underline c}^{p}\Bigl(\frac vr-c\Bigr)f(c)dc-\bigl(r+m_1(\phi)F(p)\bigr)V(\phi)+V'(\phi)F(p)\Bigr\}.$$

Formalization targets

Goal: Theorem 3 (p.23)

There is an optimal feedback reward $p(\phi)$. It is the unique solution of

$$V(\phi)=\frac{m_1(\phi)}{r}\int_{\underline c}^{p(\phi)}F(c)\,dc,\qquad(22)$$

it is $C^1$ and strictly increasing, $V$ is strictly decreasing, and

$$p(\phi)=\frac vr-\frac{2}{\phi r}\int_{\underline c}^{v/r}F(c)\,dc+o\Bigl(\frac1\phi\Bigr)\qquad(\phi\to\infty).$$

The statement holds for every cost density and every prior satisfying Assumption 1. It assumes no parametric family.

Milestones, in proof order

1. Lemma 2 (i)–(iii): $m_k$ is positive, $C^1$ and strictly decreasing, with $m_k'=m_km_1-m_{k+1}<0$; $\phi^km_k(\phi)\to k!$; and $m_{k+1}/m_k$ is strictly decreasing with $\phi\,m_{k+1}/m_k\to k+1$.
2. (41)–(42): $V$ is the limit as $\Delta t\to0$ of the fixed points $V^{\Delta t}$ of the Bellman recursion (17)–(18), it is the unique bounded differentiable solution of the HJB equation, and it is decreasing.
3. (20)–(22): the maximiser of the HJB equation is unique, lies above $\underline c$, and satisfies the first-order condition and (22).
4. (24): the reward defined by (22) is $C^1$ and solves $p'=\frac1{F(p)}\bigl(\frac{m_2}{m_1}\int_{\underline c}^{p}F-r(\frac vr-p)\bigr)$.
5. Lemma 3: at a critical point of a solution of (24), $p''<0$.
6. Lemma 4 (single crossing): where $p$ meets the naive reward $p_{na}$, which solves $\frac vr-p_{na}=\frac{m_1}{r}\int_{\underline c}^{p_{na}}F$, we have $p_{na}'<p'$.
7. Theorem 4: $p(\phi)<p_{na}(\phi)$ for every $\phi\ge0$.

Significance

Theorem 3 gives the shape of the optimal reward. It starts low, rises monotonically, and tends to the full social value $v/r$. The rate is governed only by $h_0(0)>0$ and the cost distribution below $v/r$. Theorem 4 says that a planner who learns sets a lower reward than one who treats today's expected rate $m_1(\phi)$ as known. The difference is the option value of the information in an unclaimed reward. These results underlie the paper's legal interpretations, such as rewards that grow with delay and the comparative statics in the cost distribution (Theorem 6).

Formalization adds three things on top of the paper. First, the moment calculus of Lemma 2 is a reusable result about exponential tilting of densities on $\mathbb R_+$. Second, the identification of the value function with the HJB solution and the derivation of (22) and (24) are carried out with a fixed policy class and solution concept. Third, the statements fix the welfare functional precisely: as printed, (16) multiplies $e^{-\lambda\phi(t)}$ by $h_{\phi(t)}(\lambda)$, which already contains that factor. The mission uses the functional that is the limit of the Bellman recursion (17), which the paper's own derivation uses, and the HJB milestone states that limit. None of these results has been machine-checked. The paper's proofs are informal at the limit $\Delta t\to0$.

Difficulty

The obvious route is to write down the HJB equation and read off the policy, and it skips the hard part. The paper passes from discrete time to the HJB equation in one sentence. In continuous time one needs a verification argument: every bounded differentiable solution of the HJB equation bounds the welfare of every admissible policy, and it is attained along closed-loop paths. The value function must also be shown to be differentiable before (21) can be written. A second difficulty is monotonicity. Equation (24) alone does not rule out a reward that first falls. The argument combines Lemma 3, which needs the strict Cauchy–Schwarz inequality behind Lemma 2 (iii), with a limit argument at infinity. The rate constant $2/r$ (not $1/r$, the naive rate) comes from l'Hôpital's rule applied to (24) together with $m_2/m_1=2/\phi+o(1/\phi)$. The latter is a Laplace-type asymptotic that depends on $h_0$ being continuous and positive at $0$.

Formalization scope

The Lean development lives in the namespace ScarceIdeas. States are $\phi\in[0,\infty)$, and every derivative is taken within $[0,\infty)$. Policies are open-loop functions $u$ of time with values in $[\underline c,\overline c]$, measurable on $(0,\infty)$. The value is the real supremum of the welfare over all of them. An optimal reward is a feedback rule $p(\phi)$ whose closed-loop paths $\dot\varphi=F(p(\varphi))$ exist from every state, and every such path attains $V$. The moments are defined by the quotient (31). The naive reward is the root of (56). $o(1/\phi)$ is stated as a limit of $\phi(v/r-p(\phi))$. "Increases" and "decreases" are strict.

The value function is a supremum, not a solution of the HJB equation or of (22). Defining it by either would make the goal circular. Optimality is measured against all admissible policies, not a restricted class. Changing a feedback rule at a single state changes no closed-loop welfare. For that reason the goal pins the optimal reward pointwise through (22), and "unique solution to (22)" means uniqueness of the root at each state.

A complete development needs: differentiation under the integral sign for Laplace-type integrals, and their asymptotics at infinity; the strict Cauchy–Schwarz inequality for integrals; a verification theorem for a one-dimensional infinite-horizon discounted control problem with a bounded state-dependent hazard; and comparison arguments for scalar ODEs. The moment lemma and the verification theorem are reusable beyond this mission. Contributions toward either, and toward any milestone, are welcome.

Selected references

• S. Basov, N. Erkal, D. Minehart, S. Scotchmer, Scarcity of Ideas and Optimal R&D Policy, SSRN manuscript, June 5, 2024. https://ssrn.com/abstract=4628270
• S. Basov, N. Erkal, D. Minehart, S. Scotchmer, Scarcity of Ideas and Optimal R&D Policy, Management Science (published version; its numbering is not used here). https://doi.org/10.1287/mnsc.2023.03362
• R. Mason, J. Välimäki, Learning About the Arrival of Sales, Journal of Economic Theory, 2011, pp. 1699–1711 (reference [17] of the paper).
• N. L. Stokey, R. E. Lucas, E. C. Prescott, Recursive Methods in Economic Dynamics, Harvard University Press, 1989 (reference [23] of the paper; Chapter 3 is used in the proof of Theorem 3).

Motivation

Search engines sell the ad slots next to their results in position auctions: advertisers bid, the highest bidder gets the top slot, the second highest the next one, and so on. A slot higher on the page is clicked more often, and the ratio of click rates between slots is described by a vector of relative position values. The textbook truthful mechanism, Vickrey–Clarke–Groves (VCG), computes its prices from this vector. The auctioneer does not know the true vector; it can only estimate it, and the bidding language of a real auction (one number per bidder) cannot express the bidder's own view of it.

Dütting, Fischer and Parkes (arXiv:1602.07593v4) ask which mechanisms still reach an efficient outcome, with slots assigned in order of value, when the mechanism uses a misspecified estimate. Their answer for complete information is that the non-truthful generalized second price (GSP) auction used in practice is at least as robust as the VCG mechanism run on the same estimate.

Timeline. Varian (2007) and Edelman, Ostrovsky and Schwarz (2007) characterized the envy-free ("symmetric", "locally envy-free") equilibria of GSP when the auctioneer uses the true position values, and showed that one of them reproduces the VCG outcome. Dütting, Fischer and Parkes treat the case of an estimate α different from the true vector β: Theorem 1 (complete information) and Theorem 2 (Bayes–Nash equilibrium of the first price variant). The preprint was posted in 2016 and appeared in Mathematics of Operations Research in 2024.

Setting

There are k positions and n ≥ k bidders. Let $\mathbb R^k_\ge$ be the set of vectors with positive, non-increasing entries, extended by $x_j = 0$ for $j > k$. The true relative values are $\beta \in \mathbb R^k_\ge$, and bidder $i$ values position $j$ at $\beta_j v_i$ with $v_i \ge 0$. The auctioneer uses an estimate $\alpha \in \mathbb R^k_\ge$.

A bid profile is $b \in [0,\infty)^n$. An allocation is a ranking $\sigma$ of the bidders in non-increasing order of bids, with ties resolved by $\sigma$. Write $b_{(t)}$ for the $t$-th highest bid, and $b_{(t)} = 0$ for $t > n$. The bidder in position $g$ pays

$$p^V = \sum_{j=g}^{k} (\alpha_j - \alpha_{j+1})\, b_{(j+1)} \quad (\alpha\text{-VCG}), \qquad p^S = \alpha_g\, b_{(g+1)} \quad (\alpha\text{-GSP}),$$

and its utility in position $g$ at price $p$ is $\beta_g v_i - p$. For $\alpha = \beta$ these are the VCG and GSP auctions.

An equilibrium is a profile $(b, \sigma)$ in which no bidder gains by raising or lowering its bid and being assigned a different position (§3.1, p.8). Moving bidder $i$ to position $r$ leaves the other bidders in their order, and the mechanism charges $i$ its price for position $r$ on the new order. The equilibrium is efficient if $\sigma$ also orders the values. A profile is envy-free (22) if no bidder prefers another bidder's position at that bidder's current price.

Formalization targets

Goal: Theorem 1 (p.11)

For every $k \le n$, every $\alpha, \beta \in \mathbb R^k_\ge$ and every $v \in [0,\infty)^n$:

$$\exists\ \text{efficient } \alpha\text{-VCG equilibrium} \ \Longrightarrow\ \exists\ \text{efficient } \alpha\text{-GSP equilibrium}.$$

The values are not sorted, ties are allowed in $\alpha$, $\beta$ and $v$, and the rankings are existential on both sides.

Milestones

The milestones are stated in the paper's sorted frame ($v_1 \ge \dots \ge v_n$, bidder $i$ in position $i$):

1. conditions (23)–(24) characterize α-VCG equilibria;
2. conditions (24)–(25) characterize envy-freeness;
3. envy-freeness implies equilibrium in both mechanisms;
4. the local form of (24) implies all of (24);
5. the bidder-pessimal profile (26) is an efficient α-VCG equilibrium satisfying (27);
6. (27) implies (25);
7. Lemma 1: an efficient α-VCG equilibrium can be chosen envy-free;
8. inequality (28);
9. Lemma 2: the map $b \mapsto b^S$, $b^S_i = p^V_{i-1}(b)/\alpha_{i-1}$, turns α-VCG payments into α-GSP payments with the same allocation.

Significance

The theorem compares the two mechanisms over all misspecifications at once. For every pair $(\alpha, \beta)$ where the α-VCG mechanism can support an efficient outcome, so can the α-GSP mechanism. §3.1 of the paper shows that the converse fails. Running the "truthful" mechanism therefore buys no robustness, which is one argument for the non-truthful auctions used in practice. The proof also goes through an envy-free α-VCG profile and a map to α-GSP bids that keeps the payments, which describes the α-GSP equilibrium explicitly.

The result is proved on paper. As far as the platform's catalog shows, no part of it, and no position auction model, has a machine-checked proof. The mission produces the model (rankings, both payment rules, deviations, envy-freeness), which other work on sponsored search auctions can reuse, and a checked version of an argument whose statement needed correcting (next section).

Difficulty

The obvious approach compares the equilibrium conditions of the two mechanisms inequality by inequality, as the paper does for three positions in §3.1. In general the α-GSP conditions are not implied term by term: a bidder moving up in the α-GSP auction pays the bid of the occupant it displaces, not a sum of externalities. The paper instead passes through envy-freeness, which depends only on allocation and payments. The work is index-heavy: telescoping sums over positions, a recursively defined profile (26), and boundary positions beyond $k$ and beyond $n$, where $\alpha$, $\beta$ and the order statistics are $0$. The goal is stated for arbitrary rankings and unsorted values, so a relabelling to the sorted frame is also needed.

The equilibrium notion. On p.6 the paper defines a Nash equilibrium with deviations to every real bid under a fixed tie-breaking rule, and efficiency as "$b_i > b_j$ whenever $v_i > v_j$". With that definition Theorem 1 is false. Take $k = 2$, $n = 3$, $\alpha = (0.6, 0.3)$, $\beta = (0.7, 0.4)$, $v = (8, 7, 6)$. The α-VCG profile $b = (9, 8, 0)$ has no ties and is an efficient Nash equilibrium. An efficient α-GSP equilibrium would need $b_1 > b_2 > b_3 \ge 0$. Bidder 3 must not take position 2, which gives $0.3\, b_2 \ge 0.4 \cdot 6$, so $b_2 \ge 8$. Bidder 1 must not drop to position 2, which gives $0.7 \cdot 8 - 0.6\, b_2 \ge 0.4 \cdot 8 - 0.3\, b_3$. With $b_3 < b_2$ this forces $b_2 < 8$, a contradiction. The paper's proof uses the position-deviation conditions (23)–(24) of p.11. Under that notion, with ties resolved by the ranking (Lemma 2 produces the tie $b^S_1 = b^S_2$), the argument is sound. Here the α-GSP profile $(10, 8, 8)$ is an efficient equilibrium.

Formalization scope

Bidders are Fin n, and positions are 0-based ranks Fin n (rank $r$ is position $r+1$). Ranks $r \ge k$ are unassigned positions, worth $0$ and priced at $0$. Rankings are Equiv.Perm (Fin n). $\alpha$ and $\beta$ are functions on $\mathbb N$ that are positive and non-increasing below $k$ and $0$ from $k$ on. Bids in rank order are padded with $0$. Bids and values are non-negative. The equilibrium is the position-deviation equilibrium in both the hypothesis and the conclusion of Theorem 1; it is the mission's one declared correction. In Lemmas 1 and 2, positive vectors in $\mathbb R^n_\ge$ are relaxed to non-negative sorted ones.

Efficiency is part of both sides of the goal. Dropping it, or replacing the deviation price with the current price of the target position (which is envy-freeness), would change the theorem. The sanity file checks that the example above behaves as described. In the model, $(9, 8, 0)$ is an efficient α-VCG equilibrium, $(10, 8, 8)$ is an efficient α-GSP one, and $(10, 8, 7)$ is not an equilibrium.

Everything is finite: sums over ranks, one permutation, real inequalities. No library beyond Mathlib is needed. Proofs of any milestone are welcome, as are a general relabelling lemma that reduces arbitrary rankings to the sorted frame and a proof of the strengthening that keeps the ranking fixed.

Selected references

• P. Dütting, F. Fischer, D. C. Parkes, Non-Truthful Position Auctions Are More Robust to Misspecification, arXiv:1602.07593v4, 2018; Mathematics of Operations Research, 2024. https://arxiv.org/abs/1602.07593
• H. R. Varian, Position auctions, International Journal of Industrial Organization 25(6), 2007. https://doi.org/10.1016/j.ijindorg.2006.10.002
• B. Edelman, M. Ostrovsky, M. Schwarz, Internet Advertising and the Generalized Second-Price Auction: Selling Billions of Dollars Worth of Keywords, American Economic Review 97(1), 2007. https://doi.org/10.1257/aer.97.1.242

Motivation

In Multiway Cut one is given an edge-weighted graph and $k$ terminals, and must delete a minimum-weight set of edges so that no two terminals remain connected. Equivalently, one labels every vertex by a terminal, each terminal by itself, and pays for the edges whose endpoints get different labels. The problem is APX-hard for every fixed $k\ge3$ (Dahlhaus et al., 1994), and it is a standard test case for rounding geometric relaxations.

Timeline of the approximation ratio obtained by rounding the simplex relaxation:

• 1998–2000. Călinescu, Karloff and Rabani introduce the simplex relaxation and the threshold rounding now called CKR, a $3/2-1/k$ approximation (JCSS 2000).
• 1999–2004. Karger, Klein, Stein, Thorup and Young obtain $1.3438$ with computer-optimized rounding and introduce the cut density analysis (Math. Oper. Res. 2004).
• 2013. Buchbinder, Naor and Schwartz mix CKR with exponential clocks and reach $1.32388$ (STOC 2013; SIAM J. Comput. 2018).
• 2014. Sharma and Vondrák reach $\frac14(3+\sqrt5)\approx1.309$ with the same two ingredients, prove that no mixture of these two ingredients alone can do better, and reach $1.2965$ by adding further ingredients, with a partly computer-verified analysis (STOC 2014).
• 2016–2017. Buchbinder, Schwartz and Weizman show that applying a transformation of the simplex before CKR circumvents the $\frac14(3+\sqrt5)$ barrier with the two original ingredients only, and obtain $297/229\approx1.29694$ with a fully analytic proof (SODA 2017; Math. Oper. Res. 2021, doi:10.1287/moor.2020.1073).

Setting

An instance consists of a finite vertex set $V$, a finite edge set $E$ of pairs $(u,v)$, weights $w_e\ge0$, and distinct terminals $t_1,\dots,t_k$. A feasible labeling is $g:V\to\{1,\dots,k\}$ with $g(t_i)=i$; its cost $\mathrm{cut}(g)$ is the total weight of the edges with $g(u)\ne g(v)$.

The simplex relaxation embeds every vertex $u$ as a point $\mathbf u$ of the simplex $\Delta_k=\{x\in\mathbb R^k:x\ge0,\sum_ix_i=1\}$, with $\mathbf t_i=e_i$, and minimizes $\sum_{e=(u,v)}w_e\cdot\frac12\|\mathbf u-\mathbf v\|_1$. A rounding maps the points to labels at random:

• Exponential clocks: draw i.i.d. $Z_i\sim\exp(1)$ and assign $\mathbf u$ to $\arg\min_iZ_i/u_i$.
• CKR: draw $r\sim\mathrm{Unif}[0,1]$ and a uniform order $\sigma$ of the terminals; going through $\sigma$, assign every still unassigned $\mathbf u$ with $u_{\sigma(i)}\ge r$ to $\sigma(i)$, and the rest to the last terminal.
• Algorithm 3: with probability $p$ run exponential clocks on $\{\mathbf u\}$, otherwise run CKR on $\{f(\mathbf u)\}$ for a map $f:\Delta_k\to[0,1]^k$.

The transformation of the paper sorts the coordinates of $\mathbf u$ as $u_1\ge\dots\ge u_k$, forms the vectors $\mathbf u^\ell=(u_\ell,\dots,u_\ell,u_{\ell+1},\dots,u_k)$, sets

$$f_\ell(\mathbf u)=(\mathbf u^\ell)^TA\,\mathbf u^\ell$$

for an explicit symmetric matrix $A$ (display (5.3) of the paper, nonzero only in its first three rows and columns and in $a_{44}$), and puts the values back in the original coordinate order. The cut density of a rounding at an edge that moves mass $\varepsilon$ between the $i$-th and $j$-th largest coordinates (an $(i,j)$-edge) is the limiting separation probability per unit $\varepsilon$.

Formalization targets

Goal: Theorem 1.2

With $p=121/229$ and $A$ the matrix (5.3), for every $k\ge1$, every instance and every feasible embedding $x$: both branches label the terminals correctly almost surely, and

$$\sum_{e=(u,v)\in E}w_e\Pr[g(x_u)\ne g(x_v)]\le\frac{297}{229}\sum_{e=(u,v)\in E}w_e\,\tfrac12\|x_u-x_v\|_1 ,$$

hence $\mathbb E[\mathrm{cut}]\le\frac{297}{229}\,\mathrm{cut}(g)$ for every feasible $g$ when $x$ is an optimal embedding.

Milestones

• the exponential-clocks bound $\Pr[\text{separate }\mathbf u,\mathbf u+\varepsilon(e_i-e_j)]\le\varepsilon(2-u_i-u_j)$ (Lemma 2.1) and the CKR bound $\sum_\ell|u_\ell-v_\ell|/\ell$ for commonly sorted points (Lemma 2.2);
• the subdivision of any edge into short $(i,j)$-edges (Observation 2.1) and the reduction from a per-edge bound $\gamma\varepsilon+C\varepsilon^2$ to the approximation ratio $\gamma$ (p.4, corrected);
• feasibility of the transformation under three prefix-sum conditions (Lemma 5.1), the CKR density bound (5.2) (Lemma 5.2), the prefix-sum order $\succeq$ (Lemma 5.3);
• the properties of (5.3) (Observation 5.1, display (5.4)), the bound $\alpha_{i,j}\le\frac{44}{27}(u_i+u_j)+\frac{55}{108}\sum_{\ell\ne i,j}u_\ell$ (Lemma 5.4), and the overall per-edge bound $\frac{297}{229}\varepsilon+C\varepsilon^2$.

Significance

The theorem shows that the barrier $\frac14(3+\sqrt5)$ of Sharma and Vondrák concerns only coordinate-wise transformations: a transformation that couples the coordinates through their sorted order reaches $1.29694$ with the two original ingredients and a proof checkable by hand. The approach (choose a feasible transformation, then bound the density by a sum of absolute values of linear forms) is a template for other partitioning relaxations.

The result is proved in the paper; nothing here is open. No part of it has a machine-checked proof. Formalizing it checks a long case analysis (the proof of Lemma 5.4 spans pp.8–11) and the reduction from cut density to the approximation ratio, which the paper calls "easy to show" and which, read with the lim sup of Definition 2.1, needs a correction (see below).

Difficulty

The obvious route, "bound the cut density and conclude by the Karger et al. argument", fails as stated: a bound on a pointwise $\limsup$ does not control the separation probability of a long edge, because a labeling can jump between nearby points in a way invisible to every one-sided limit. The mission therefore states the per-edge bound with a remainder $C\varepsilon^2$ uniform over all edges, and the reduction with that hypothesis. Proving the uniform remainder for Algorithm 3 requires following $f$ along an edge exactly, not only its derivative.

The second obstacle is Lemma 5.4: removing the absolute values in (5.2) needs the chain of prefix-sum dominations of Observation 5.1 and Lemma 5.3, then a case analysis over $i\in\{1,2,3,4,\ge5\}$ and $j$ with exact rational arithmetic. The exponential-clocks bound (Lemma 2.1) needs the competing-exponentials computation and a coupling of two argmins.

Formalization scope

Coordinates and terminals are Fin k, indexed from $0$; $\Delta_k$ is stdSimplex ℝ (Fin k). The clocks' law is Measure.pi of expMeasure 1; the argmin runs over the support of $\mathbf u$ by cross-multiplication (Lean's $x/0=0$ would otherwise let a zero coordinate win). CKR's law is the average over permutations of Lebesgue measure on $[0,1]$. Probabilities are measures of events (outer measures), never integrals of indicators, so non-measurability cannot make a bound vacuous; expected costs are $\sum_ew_e\Pr[\text{cut}]$. "$\limsup\le c$" is the eventual form "for every $\eta>0$, eventually ratio $\le c+\eta$". The transformation uses Mathlib's Tuple.sort; its value does not depend on how ties are sorted. The matrix (5.3) is defined for every $k$ by its entry formula.

A trivializing formalization is excluded: the goal keeps the terminal clause (otherwise labeling everything $1$ costs nothing), and constants $p=121/229$, $297/229$ and the matrix entries are fixed.

A complete development needs: the competing-exponentials law $\Pr[\arg\min=i]=u_i$, the CKR union bound, the subdivision of a segment of $\Delta_k$ into order-preserving steps, and exact rational arithmetic for the case analysis. The first three are reusable for any analysis of simplex-relaxation roundings. Proofs of individual milestones, and of the reduction (p.4) independently of this algorithm, are welcome.

Selected references

• N. Buchbinder, R. Schwartz, B. Weizman, Simplex Transformations and the Multiway Cut Problem, manuscript of Nov. 1, 2016 (SODA 2017); Math. Oper. Res. 46 (2021). https://doi.org/10.1287/moor.2020.1073
• G. Călinescu, H. Karloff, Y. Rabani, An Improved Approximation Algorithm for Multiway Cut, J. Comput. Syst. Sci. 60 (2000). https://doi.org/10.1006/jcss.1999.1687
• D. R. Karger, P. Klein, C. Stein, M. Thorup, N. E. Young, Rounding Algorithms for a Geometric Embedding of Minimum Multiway Cut, Math. Oper. Res. 29 (2004). https://doi.org/10.1287/moor.1030.0086
• N. Buchbinder, J. Naor, R. Schwartz, Simplex Partitioning via Exponential Clocks and the Multiway Cut Problem, SIAM J. Comput. 47 (2018). https://doi.org/10.1137/15M1045521
• A. Sharma, J. Vondrák, Multiway Cut, Pairwise Realizable Distributions, and Descending Thresholds, STOC 2014. https://doi.org/10.1145/2591796.2591866
• E. Dahlhaus, D. S. Johnson, C. H. Papadimitriou, P. D. Seymour, M. Yannakakis, The Complexity of Multiterminal Cuts, SIAM J. Comput. 23 (1994). https://doi.org/10.1137/S0097539792225297

Motivation

Many allocation procedures used in practice — school choice, university admissions, course allocation — are run as one-shot direct mechanisms: every participant submits a full ranking, and an algorithm such as deferred acceptance or top trading cycles computes the assignment. Sequential alternatives, in which participants repeatedly pick one option from a menu, may see their pick rejected, and are then offered a smaller menu, have been proposed and studied for college admissions; the iterative deferred acceptance mechanism is the leading example (Bó and Hakimov, Games and Economic Behavior 135, 2022), and laboratory evidence finds more truthful behaviour under it than under its direct counterpart (Bó and Hakimov, The Economic Journal 130, 2020). Two questions arise: which allocation rules can be run this way at all, and when is it in every participant's interest to pick truthfully?

Bó and Hakimov, Pick-an-Object Mechanisms (arXiv:2012.01025v4) answer both questions for a general class of sequential procedures, and the answer is a pair of characterizations. This mission formalizes them.

Setting

$A$ is a finite set of agents and $O=\{o_1,\dots,o_m\}\cup\{\varnothing\}$ a finite set of object types containing the null object $\varnothing$. Each agent $a$ has a strict preference $P_a$ over all of $O$; objects ranked below $\varnothing$ are unacceptable, and $o\,R_a\,o'$ means $o\,P_a\,o'$ or $o=o'$. A rule $\varphi$ maps every preference profile $P=(P_a)_{a\in A}$ to an allocation $\mu:A\to O$. There is no capacity constraint: feasibility is whatever the rule produces. A rule is individually rational if $\varphi_a(P)\,R_a\,\varnothing$ and strategy-proof if no agent gains by reporting another preference.

A choice history is a sequence $((\Omega_1,\omega_1),\dots,(\Omega_k,\omega_k))$ of menus $\Omega_j\subseteq O$ and choices $\omega_j\in\Omega_j$; a collective history $h^A$ has one per agent, and $h^{A-\varnothing}$ is the one in which no agent has chosen yet. A menu function $S$ assigns every agent a menu at every collective history, subject to two rules:

1. the initial menus $S_a(h^{A-\varnothing})$ are non-empty;
2. a later menu is contained in the agent's previous menu with her previous choice removed.

The pick-an-object (PAO) mechanism of $S$ runs in periods. If every menu $S_a(h^A)$ is empty, it stops and each agent receives her last choice. Otherwise every agent with a non-empty menu picks one element, and the history grows. A straightforward agent always picks her most-preferred element of the menu. $S$ sequentializes $\varphi$ if, for every profile $P$, straightforward play from $h^{A-\varnothing}$ ends at $\varphi(P)$.

The lower contour set $\mathcal L(P,\mu)$ is the set of profiles $P'$ such that, for each agent $a$, $P'_a$ has the same objects strictly above $\mu(a)$ as $P_a$, in the same order. A rule satisfies monotonic discoverability if for every allocation $\mu$ and profile $P$, either $\varphi(P)=\mu$, or some agent $a^*$ has $\varphi_{a^*}(P')\ne\mu(a^*)$ for every $P'\in\mathcal L(P,\mu)$.

A strategy chooses an element of the current menu as a function of the agent's own choice history. Straightforward strategies form a perfect ex-post equilibrium of $S$ if, at every collective history $h^A$ that $S$ can produce (under arbitrary past choices) and for every profile $P$, no agent gains by deviating to any other strategy from $h^A$ on. A rule is pick-an-object implementable in perfect ex-post equilibrium if some $S$ sequentializes it with straightforward strategies forming such an equilibrium.

Formalization targets

Goal: Theorem 2 (p.19)

For every individually rational rule $\varphi$:

$$\varphi\ \text{PAO-implementable in perfect ex-post equilibrium}\iff \varphi\ \text{strategy-proof}\ \wedge\ \varphi\ \text{monotonically discoverable},$$

and, if $\varphi$ is PAO-implementable in perfect ex-post equilibrium, straightforward strategies form a perfect ex-post equilibrium of every menu function that sequentializes $\varphi$.

Milestones

• §3, p.11. Every collective history a PAO mechanism can produce is consistent with some preference profile.
• Corollary 1, p.44 (Haeringer–Hałaburda). Recursive dominance, $\varphi_a(\gamma\oplus P_a|_{O\setminus I},P_{-a})\,R_a\,\varphi_a(P^*,P_{-a})$ for every $P^*$ ranking the tuple $\gamma$ first, is equivalent to strategy-proofness.
• Lemma 1, p.44. After any history of a sequentializing mechanism, the outcomes of a straightforward and a deviating agent $a^*$ are $\varphi_{a^*}(\gamma\oplus P_{a^*}|_{O\setminus I},P'_{-a^*})$ and $\varphi_{a^*}(\gamma\oplus P^*|_{O\setminus I},P'_{-a^*})$ with a common $\gamma$ and $P'_{-a^*}$.
• Proof of Theorem 2, p.45. If $\varphi$ is strategy-proof, straightforward strategies form a perfect ex-post equilibrium of every $S$ that sequentializes $\varphi$.
• Proof of Theorem 2, p.46. If some sequentializing $S$ has straightforward strategies as a perfect ex-post equilibrium, $\varphi$ is strategy-proof.
• Theorem 1, p.14. An individually rational $\varphi$ can be sequentialized if and only if it satisfies monotonic discoverability.

Significance

Theorem 1 says exactly which rules a PAO mechanism can run, and shows that the restriction is real: not every rule can be sequentialized, because a rejected choice can never be offered again. Proposition 1 of the paper (not part of this mission) places deferred acceptance, top trading cycles and the Boston mechanism inside the class. Theorem 2 adds incentives: among sequentializable rules, the strategy-proof ones are exactly those for which truthful picking is a best response after every history, against every deviation, for every preference profile — and this holds in every PAO mechanism for the rule, not in a specially designed one. For a designer this means the choice of menus can be made for simplicity or transparency without affecting incentives.

On the formal side, the mission produces a reusable model of sequential menu mechanisms for ordinal object allocation (histories, menu functions, an executable run, strategies, perfect ex-post equilibrium), which the platform does not have; existing items cover strategy-proofness of fixed algorithms (top trading cycles, deferred acceptance) and obviously strategy-proof mechanisms for scheduling. The paper's results are proved on paper only; none is machine-checked. The printed proof of Theorem 1's "if" direction relies on a canonical mechanism (§3.3) that does not sequentialize every monotonically discoverable rule (a two-agent serial dictatorship already fails), so a complete formal proof must supply a different witness.

Difficulty

The equilibrium part is the hard one. Perfect ex-post equilibrium is required at every history, including histories in which agents have already made arbitrary non-truthful choices. Strategy-proofness of $\varphi$ speaks only about complete reports from $h^{A-\varnothing}$, so it does not directly compare two continuations after such a history. The bridge is Lemma 1: every history of the mechanism must be rationalized by preferences (the tuples $\gamma$), the continuations under truthful and deviating play must be re-expressed as straightforward play from the beginning under modified profiles, and the comparison must be made through recursive dominance. Keeping the same $P'_{-a^*}$ in both representations is essential and is where a careless argument breaks.

For Theorem 1, the natural first idea — elicit the whole preference profile with menus and then assign — is not available: menus must shrink and the agent keeps her last pick, so information about lower-ranked objects can only be obtained by permanently rejecting her current choice. The "only if" direction must turn this informational constraint into monotonic discoverability. The "if" direction needs a menu function that rejects only choices that are no longer attainable.

Formalization scope

Object types are Option Obj for a finite type Obj, with none the null object. A strict preference is a ranking Option Obj ≃ Fin (card (Option Obj)) (rank $0$ is best), so every strict linear order is represented exactly once. Allocations are arbitrary maps $A\to O$. Histories are lists of (menu, choice) pairs, oldest first. The run is the $(|A|\cdot|O|+1)$-fold iterate of one period of the mechanism; with menus that strictly shrink, this is enough for the procedure to stop from any history, and a stopped history is a fixed point. Strategies are functions of the agent's own history and current menu that pick from every non-empty menu. The collective histories of $S$ are an inductive predicate: $h^{A-\varnothing}$ and everything reachable from it under arbitrary choices from the offered menus. The menu-shrinking constraint is not imposed at histories other than $h^{A-\varnothing}$ in which some agent has never faced a menu, which the mechanism never produces.

The lower contour set is corrected. The display on p.12 constrains only pairs of objects strictly above $\mu(a)$; with it, the one-agent rule "$x$ iff $x\,P\,\varnothing$" on $O=\{x,y,\varnothing\}$ is individually rational and sequentialized by the single menu $\{x,\varnothing\}$, but fails Definition 3 at $P=(x,\varnothing,y)$, $\mu=\varnothing$, $P'=(y,\varnothing,x)$, so Theorem 1 would be false. The formalization uses the reading stated in the sentence under the display (same objects above $\mu(a)$, in the same order). Likewise, the canonical mechanism of §3.3 is not used as the witness for Theorem 1 and is not part of the formalization.

Restricting perfect ex-post equilibrium to histories generated by straightforward play, or allowing a deviation to "choose" an object outside the menu, would change the equilibrium notion; neither is done.

Needed infrastructure: finite permutations and rankings, list and finset manipulation, induction over reachable histories, and a determinism and termination analysis of the run. The model definitions and the representation of outcomes after arbitrary histories (Lemma 1) are reusable for other sequential mechanisms. Proofs of any milestone, a formal proof that the run's period bound suffices, and alternative witnesses for Theorem 1 are welcome.

Selected references

• I. Bó, R. Hakimov, Pick-an-Object Mechanisms, arXiv:2012.01025v4, 2023 (published in Management Science, 2024). https://arxiv.org/abs/2012.01025
• G. Haeringer, H. Hałaburda, Monotone strategyproofness, Games and Economic Behavior 98, 68–77, 2016 (source of Corollary 1).
• I. Bó, R. Hakimov, The iterative deferred acceptance mechanism, Games and Economic Behavior 135, 411–433, 2022.
• I. Bó, R. Hakimov, Iterative versus standard deferred acceptance: experimental evidence, The Economic Journal 130(626), 356–392, 2020.
• A. Mackenzie, Y. Zhou, Menu mechanisms, Journal of Economic Theory 204, 105511, 2022 (an independent generalization of the equilibrium result).
• D. Bergemann, S. Morris, Robust mechanism design, Econometrica 73(6), 1771–1813, 2005 (perfect ex-post equilibrium). https://doi.org/10.1111/j.1468-0262.2005.00638.x

Why risk-averse bargaining needs its own axioms

When independent firms pool resources, they can share not only a deterministic profit but a random one, chosen through a joint decision. Cooperative models for operations management usually value such payoffs in expectation or by a concave utility, and then bargain over the expected values. Gutjahr, Kovacevic and Wozabal (author manuscript) replace this with coherent acceptability functionals in the sense of Artzner et al. (1999), the class that contains expectation and the Average Value-at-Risk, and ask which sharing rule follows from axioms alone. The classical axioms of Nash (1950) are stated for deterministic utility pairs. The relevant comparison for this mission is the splitting axiom of Hougaard (2009), which the paper carries from deterministic allocation to random payoffs.

Setting

Fix a probability space, an exponent $p\ge 1$, and a compact topological space $\mathcal X$ of decisions. An instance $(R,M,\mathcal A)$ for a finite nonempty player set $N$ consists of endowments $R_i\in L^p$, a profit $M_x\in L^p$ for each decision $x$, with $x\mapsto M_x$ continuous into $L^p$ with the weak topology, and coherent acceptability functionals $\mathcal A_i:L^p\to\mathbb R$, that is, monotone, positively homogeneous, super-additive and translation invariant. Write $v_i=\mathcal A_i(R_i)$. The set of feasible acceptability allocations is

$$\mathcal U(R,M,\mathcal A)=\Big\{u\in\mathbb R^n \;\Big|\; \exists x\ \exists L:\ \sum_{i} L_i=M_x,\ v_i\le u_i\le\mathcal A_i(L_i)\ \forall i\Big\},$$

and $z(R,M,\mathcal A)$ is the maximum of $\sum_i u_i$ over the same constraints, which is problem (8). A bargaining solution $F$ selects a point of $\mathcal U$ for each instance. It is asked to satisfy PAR (Pareto optimality), SYM (equal treatment when all values agree and $\mathcal U$ is permutation invariant) and STR (a player who splits into $\ell$ copies, each with endowment $R_i/\ell$, receives the same total).

Formalization targets

Goal: the corrected Theorem 1

On the class of admissible instances, those with all $v_i>0$ for which the maximum in (8) exists, put

$$u_i=\frac{v_i}{\sum_{j} v_j}\cdot z(R,M,\mathcal A). \tag{9}$$

The goal has four clauses: (a) rule (9) is a bargaining solution; (b) a bargaining solution agreeing with (9) satisfies PAR, SYM, STR and CONT; (c) a bargaining solution with PAR, SYM, STR agrees with (9) wherever the $v_i$ are natural multiples of one positive real; (d) a bargaining solution with PAR, SYM, STR, CONT agrees with (9) everywhere. CONT requires $F$ to be continuous along scalings $R\mapsto(c_iR_i)_i$ with $c\to 1$.

Milestones

The milestones are: Proposition 2 (the polytope (7)), Proposition 1 (compactness, as an equivalence with attainment), Lemma 5 ($z$ does not depend on the endowments), invariance of $z$ and of the class under splitting, the identity $\sum_i u_i=z$ under PAR, the commensurable case (clause (c)), the converse (clauses (a), (b)), and two counterexamples.

Significance

The result gives a sharing rule for risk-averse partners with a closed form: the shares depend only on the values $v_i$, and the decision $x$ enters only through $z$. So a joint decision can be separated from the division of the surplus, which is what makes the rule usable in stochastic optimization models.

The theorem has been published, but the formalization adds more than a check, because the printed statement is false in two ways, and the mission records both as machine-readable counterexamples. Nothing in this mission has a previous machine-checked proof on the platform. The two-player Nash theorem there uses different axioms and yields a different solution.

Difficulty

The obvious route from rational to real values fails. The printed proof treats $v_i\in\mathbb Q$ by splitting and symmetry and then appeals to the continuity of the right-hand side of (9). That continuity says nothing about $F$, and SYM only compares equal values while STR only divides a value by an integer, so two players with $v_i/v_j\notin\mathbb Q$ are never connected. The second obstacle is structural: Axiom STR splits one player at a time, the player type changes at every step, and no relabelling invariance of $F$ is assumed.

Formalization scope

Corrections. Two corrections to the printed Theorem 1 are part of the statement. First, CONT is added to the characterization, and clause (c) keeps what the printed axioms give; the witness is a rule that differs from (9) at $v=(1,\sqrt2)$, $z=10$ and meets PAR, SYM, STR at every admissible instance. Second, the class requires the maximum in (8) to exist: on $\Omega=\{1,2,3\}$ with the uniform probability there is a feasible instance, with $\mathcal A_i\le\mathbb E$, where it does not exist, $\mathcal U$ is not compact, and no rule can satisfy PAR. Proposition 1 and Proposition 2 are restated accordingly. Lemma 4 of the paper is false and is not used.

Representation. $L^p$ is Lp ℝ p μ with p : ℝ≥0∞, 1 ≤ p (so $p=\infty$ is admitted), and $M$ is a map X → Lp ℝ p μ. Functionals are real-valued. No continuity of $\mathcal A_i$, no bound $\mathcal A_i\le\mathbb E$ and no dual representation is assumed. Player sets are finite nonempty types and a rule is a family over all of them, because Axiom 3 changes the player set. A split player set is {j // j ≠ i} ⊕ Fin ℓ with ℓ : ℕ+. The real $z$ is a sSup and equals the maximum exactly on attained instances; every item mentioning $z$ assumes attainment.

Non-triviality. Clause (a) shows that the hypotheses of (c) and (d) can be met, so neither is vacuous, and the class is not empty: it contains every instance with constant endowments and expectations whose total does not exceed a constant profit. Defining $F$ through $z$, or adding an axiom that $F$ depends only on $(v,z)$, would assume part of the conclusion; neither happens here.

Infrastructure. The development needs coherent functionals on Lp, the polytope description of $\mathcal U$, and the split and scaling operations on instances. Coherent acceptability on $L^p$ is reusable for other risk-averse models. Contributions that connect these definitions to Average Value-at-Risk are welcome.

Selected references

• W. J. Gutjahr, R. M. Kovacevic, D. Wozabal, Risk-Averse Bargaining in a Stochastic Optimization Context, Manufacturing & Service Operations Management; this mission cites the author manuscript. https://doi.org/10.1287/msom.2021.1076
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3), 1999. https://doi.org/10.1111/1467-9965.00068
• J. F. Nash, The bargaining problem, Econometrica 18(2), 1950. https://doi.org/10.2307/1907266
• J. L. Hougaard, An Introduction to Allocation Rules, Springer, 2009. https://doi.org/10.1007/978-3-642-01828-2

Motivation

Many developing countries reserve college seats for disadvantaged students, and how large the reservation should be is a live policy question: in 1993 the Supreme Court of India capped reservations at 50% of seats. Bao, Ni and Singh (SSRN 3772113, version of May 30, 2023; published in Management Science, doi:10.1287/mnsc.2021.00249) build an equilibrium model in which higher-income students can buy private tutoring, the job market pays each group the mean ability of its admitted students, and a policymaker moves seats from one group to the other. Their closing finding answers a policy question: the transfer that eliminates the admission gap is larger than the transfer that maximizes overall student welfare, so a welfare-maximizing policymaker leaves inequality in place. The paper asserts this comparison in one line of its appendix.

The admission game

A unit mass of students competes for capacity $z$. A share $\alpha$ is type $x$ and can pay $\kappa$ for proprietary resources; the remaining $1-\alpha$ are type $y$ and cannot. A student who exerts effort $e\ge 0$ pays $ke^2$, and her ability is $e+\varepsilon$ if she invests and $\phi e+\varepsilon$ otherwise, with $\varepsilon\sim U[-1,1]$ and $\phi\in(0,1)$.

The college admits every student whose ability exceeds a cutoff $d$. Write $\rho(m,d)=\Pr(m+\varepsilon>d)$ for the admission probability of a student of mean ability $m$. An admitted student receives a reward $r$ equal to the expected ability of the admitted students of her type. Each student takes $d$ and $r$ as given and maximizes $\rho\,r-ke^2$, net of $\kappa$ if she invested. Seats clear: $z=\alpha\rho_x+(1-\alpha)\rho_y$.

A seat transfer $s$ gives each type its own cutoff $d_x,d_y$ and fixes admissions: type $x$ loses exactly $s$ seats relative to the no-policy benchmark and type $y$ gains exactly $s$. Educational inequality is $EI=\rho_x-\rho_y$, and overall welfare is $U=\alpha u_x+(1-\alpha)u_y$.

The parameters satisfy $k>\tfrac14$, $\phi,\alpha\in(0,1)$, $\kappa>0$ and $\frac{4k\alpha(1-\phi^2)}{(8k-1)(4k-\phi^2)}<z<\tfrac12$. The threshold $\kappa^*$ of equation (32) is the largest cost at which type $x$ does not deviate from investing.

Formalization targets

Goal: Proposition 6

For $\kappa<\kappa^*$, the investing benchmark equilibrium exists and is unique; every feasible transfer $s$ has a unique equilibrium $\sigma(s)$; and

$$s_0=\frac{4k\alpha(1-z)(1-\alpha)(1-\phi^2)}{32k^2+\phi^2-4k\bigl(1+2\phi^2+\alpha(1-\phi^2)\bigr)}$$

is feasible, with $EI(\sigma(s_0))=0$ and $|EI(\sigma(s))|>0$ for every other feasible $s$. Moreover overall welfare has a unique maximizer $s^*$ over feasible transfers, and

$$s_0>s^*.$$

Milestones

The admission probability (4) and reward (10) under uniform noise; effort at a given cutoff (11); the equilibrium cutoff (26)–(27); the investment thresholds (32) and (45); Proposition 1; the equilibrium probabilities (28) and the closed form of inequality (47); the policy cutoffs (51)–(52); Lemma 1 on effort; welfare as a concave quadratic in $s$ (55); its vertex (56); and Proposition 5, the inverted-U shape of welfare.

Significance

The result gives a closed form for the transfer that closes the admission gap and states that closing it costs welfare. The paper draws its policy advice from this: other instruments, such as better basic education and lower wage discrimination, should accompany reservation. Without the strict inequality, the conflict between the two policy goals would not be established.

The results are proved on paper, with first-order conditions and a one-line comparison. They have no machine-checked proof, and this mission adds three things. It derives (4) and (10) from the uniform measure instead of assuming them. It establishes existence and uniqueness of the equilibria the paper takes for granted. It gives a proof of $s_0>s^*$ on the whole parameter domain, a comparison in four real parameters that the paper does not derive. It also corrects errors in the printed statements: the effort range, the claimed equivalence of the cutoff restriction with the capacity interval, the denominator of $z'$ in (57), and a misplaced bracket in $\mu_2$. Exact-rational sampling supports the comparison, with $s^*/s_0$ never above about $0.498$; that is evidence, not a proof.

Difficulty

The closed forms follow from linear algebra once the model is reduced to first-order conditions. The work lies in the reduction: passing from the true clipped probability and a conditional expectation to the linear system, showing that a boundary effort is not a maximizer, and ruling out every other outcome. The naive route of comparing (24) with (56) symbolically fails to be routine, because (56) is the first-order solution only when positive, so $s^*=\max\{0,(56)\}$, and both cases must be handled; the remaining inequality is a polynomial inequality in $(k,\phi,\alpha,z)$ on a non-box domain.

Formalization scope

Parameters are a structure of five reals with the predicate Params.Valid. The noise is the uniform law on $[-1,1]$: Lebesgue measure on $[-1,1]$ scaled by $\tfrac12$. admitProb and admittedMean are the true probability and conditional mean from that measure; (4) and (10) are theorems. Equilibria are pure and symmetric within a type.

Three conventions depart from the printed text and are declared on every theorem. Effort ranges over $[0,\infty)$, because equilibrium effort can exceed the page's bound of $1$. The domain is the capacity interval above with no restriction on $d$. Best responses range over the efforts at which the admission probability lies strictly in $(0,1)$, the set on which (4) holds. Under this convention equilibria are exactly the solutions of the paper's first-order conditions. Against all efforts with the clipped probability they can fail: effort $0$ can pay more than the interior effort when admission chances are small, at $s_0$ itself for small $z$.

The policy game is the investing branch, equation (17), and the feasible transfers are the set of p.41. The transfer $s^*$ in the goal is characterized as the maximizer of $U$, never defined by (56); $s_0$ is characterized by what it achieves; so the goal is not algebra about named formulas. The definitions are local to this model and reusable only through the uniform law. Proofs of the milestones, in any order, are welcome.

Selected references

• W. Bao, J. Ni, S. Singh, Educational Inequality and Reservation Policy in Developing Markets, SSRN 3772113, version of May 30, 2023. https://ssrn.com/abstract=3772113
• W. Bao, J. Ni, S. Singh, Educational Inequality and Reservation Policy in Developing Markets, Management Science, 2023. https://doi.org/10.1287/mnsc.2021.00249