Probability

Motivation

Algorithmic mechanism design, introduced by Nisan and Ronen (Games Econ. Behav. 35, 2001), studies optimization problems whose input is held by self-interested agents. Each agent reports its private data to a protocol, and the protocol must choose an output and payments so that reporting the truth is in every agent's interest while the chosen output is close to optimal.

The paper's test case is task scheduling on unrelated machines: $k$ tasks must be assigned to $n$ agents, agent $i$ needs time $t^i_j$ for task $j$, and the goal is to minimize the make-span. For deterministic mechanisms the paper shows that truthfulness is costly: the MinWork mechanism achieves ratio $n$, and no mechanism achieves a ratio below $2$ (Theorem 4.6). Section 4.4 asks whether randomization helps and answers yes for two agents: a randomized mechanism, truthful for every outcome of its coins, achieves expected ratio $7/4 < 2$.

Timeline.

• 1979: Roberts characterizes weighted (affine) maximizers; the weighted Vickrey–Groves–Clarke (VGC) mechanisms are truthful.
• 1999: Lehmann supplies the case analysis that improves the authors' original bound of $1.823$ to $7/4$ (acknowledged on p. 182).
• 2001: Nisan and Ronen publish the randomly biased min work mechanism and Theorem 4.16.

Setting

There are two agents, $1$ and $2$, and $k$ tasks. A type vector $t = (t^1, t^2)$ gives, for each agent $i$ and task $j$, the positive time $t^i_j$ agent $i$ needs for task $j$. An allocation $x$ assigns each task to one agent; $x^i$ is the set of tasks of agent $i$. The make-span of $x$ is

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

A direct mechanism receives declared types $d$ and returns an allocation $x(d)$ and payments $p^i(d)$ handed to the agents. Agent $i$ with true type $t^i$ gets utility $p^i(d) - \sum_{j \in x^i(d)} t^i_j$. The mechanism is truthful if declaring the true type maximizes an agent's utility whatever the other agent declares, and strongly truthful if in addition every false declaration is strictly worse for some declaration of the other agent.

A randomized mechanism is a probability distribution over deterministic mechanisms; its objective is the expected make-span. It is universally truthful if every mechanism in its support is truthful, and universally strongly truthful if moreover truth-telling is the only strategy dominant in every mechanism of the support.

The biased min work mechanism with parameters $\beta \ge 1$ and $s \in \{1,2\}^k$ treats each task $j$ separately. With $i = s_j$ the favoured agent and $i' = 3 - i$ the other: if $t^i_j \le \beta \cdot t^{i'}_j$, task $j$ goes to $i$, who is paid $\beta \cdot t^{i'}_j$; otherwise it goes to $i'$, who is paid $\beta^{-1} \cdot t^i_j$. The randomly biased min work mechanism draws $s$ uniformly from $\{1,2\}^k$ and uses $\beta = 4/3$. Its expected make-span is

$$\mathbb{E}_s\, g(x_s(t), t) = \frac{1}{2^k} \sum_{s \in \{1,2\}^k} g(x_s(t), t).$$

Formalization targets

Goal: Theorem 4.16

For every $k$: the randomly biased min work mechanism is universally strongly truthful, and for every positive type vector $t$ and every allocation $y$,

$$\frac{1}{2^k} \sum_{s \in \{1,2\}^k} g(x_s(t), t) \le \frac74\, g(y, t).$$

Milestones

• Theorem 3.2 (Roberts): for positive weights $\beta^i$, a mechanism whose output maximizes $\sum_i \beta^i v^i(t^i, o)$ and whose payments are $p^i = \frac{1}{\beta^i}\sum_{j \ne i}\beta^j v^j(t^j, o) + h^i(t^{-i})$ is truthful.
• Lemma 4.15: for every $\beta \ge 1$ and every $s$, the biased min work mechanism is strongly truthful.
• Lemma 4.17: the randomly biased min work mechanism is universally strongly truthful.
• Claim 4.19, part 5: allocating two tasks independently at random gives an expected make-span no larger than allocating their merge at random.
• Reduced case (Fig. 2, Cases 1–3): for $a, b, c, d \ge 0$ with $a + c = \frac43 b + d$,

$$\tfrac14\Big(\max(a+b+c+\tfrac43 d, 0) + \max(a+b+c, d) + \max(a+b+\tfrac43 d, \tfrac43 c) + \max(a+b, \tfrac43 c + d)\Big) \le \tfrac74 (a+c).$$

• Lemma 4.18: the $7/4$ bound on the expected make-span.

Significance

The result. Theorem 4.16 separates randomized from deterministic truthful mechanisms for scheduling two unrelated machines: $7/4$ against the deterministic lower bound of $2$. The notion of truthfulness it uses is the strong one, dominance for every coin outcome, so the separation does not rest on agents being risk-neutral or knowing the distribution. Later work on truthful randomized scheduling, and on the gap between deterministic and randomized truthful mechanisms, starts from this construction.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it is known. A formalization produces a checked definition of universal truthfulness for randomized mechanisms, a checked weighted VGC theorem usable for any affine-maximizer mechanism, and a checked version of the reduction argument (Claim 4.19), which the paper states in five informal instance transformations, one of them a limiting argument.

Difficulty

Truthfulness reduces to one task at a time, where the mechanism is a weighted VGC mechanism; the difficulty lies in the approximation bound. A naive task-by-task comparison with the optimum fails: the bound is on a maximum of two loads averaged over $2^k$ coin vectors, and the maximum does not decompose over tasks. The paper reduces an arbitrary instance to four tasks through transformations that each move the ratio in one direction, and the reduced instance still needs a three-way case analysis. Making the reduction rigorous is the main work: part 1 of Claim 4.19 replaces a ratio "arbitrarily close to $\beta$" by $\beta$, and under the mechanism's tie rule a task with ratio exactly $\beta$ is allocated by the coin rather than to the efficient agent.

Formalization scope

• Agents are Fin 2 (agent $1$ is 0, agent $2$ is 1); the other agent is other i = 1 - i. Tasks are Fin k; allocations are functions Fin k → Fin 2. The statements hold for every $k$, including $k = 0$.
• Types are positive: every truthfulness quantifier ranges over positive declarations, true types and misreports, and the approximation bound is stated on positive type vectors. The reduced-case and merging milestones are pure real inequalities with nonnegative times, since the paper represents missing tasks by zero times.
• Payments are handed to the agent; utility is quasi-linear.
• The make-span is a finite maximum (Finset.sup') over the two agents. The expected make-span is the average over all $2^k$ vectors $s$, which is exactly the expectation of Definition 15 for the uniform distribution; no measure theory is used.
• Universal (strong) truthfulness quantifies over all $s \in \{1,2\}^k$, the support of the uniform distribution. Truthfulness in expectation over $s$ is weaker and is not the notion stated.
• The tie rule of Fig. 1 ($\le$: ties go to the favoured agent) is kept.
• The goal fixes $\beta = 4/3$; only Lemma 4.15 is stated for every $\beta \ge 1$. The ratio is compared with every allocation $y$, not with one fixed allocation, and the average is over all $s$, not the best $s$.
• Roberts' theorem is stated for arbitrary output sets, type sets and valuations, with positive weights.
• "Polynomial time computable" in Theorem 4.16 is not formalized; running time is out of scope.
• Claim 4.19 (the reduction to the four-task case) is not a separate item beyond its part 5, because its parts are instance transformations with a limiting step, not a single statement; a solver may formalize the reduction in any form that proves Lemma 4.18.

Contributions welcome: proofs of the milestones, and reusable lemmas on averages of maxima over product coin spaces.

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
• K. Roberts, The characterization of implementable choice rules, in J.-J. Laffont (ed.), Aggregation and Revelation of Preferences, North-Holland, 1979, pp. 321–349.
• T. Groves, Incentives in teams, Econometrica 41 (1973) 617–631. https://doi.org/10.2307/1914085

Motivation

Fictitious play is the oldest model of learning in games: players repeatedly play a fixed normal form game, and each round every player best-responds to the empirical frequencies of the opponents' past play. Brown (1951) proposed it as an algorithm for computing the value of a zero-sum game, and Robinson (1951) proved that the empirical frequencies converge to the set of equilibria in that case. In stochastic fictitious play (Fudenberg and Kreps 1993) each player's payoffs are perturbed by fresh random shocks before every choice. The shocks make best responses single-valued and smooth in beliefs, which puts the process within reach of stochastic approximation theory: its long-run behaviour is governed by a deterministic perturbed best response dynamic.

Before Hofbauer and Sandholm (2002), convergence of stochastic fictitious play was known only for 2×2 games (Fudenberg and Kreps 1993; Kaniovski and Young 1995) and for certain games with two strategies per player (Benaïm and Hirsch 1999). The difficulty was the perturbed dynamic itself, whose vector field involves choice probabilities with no closed form for general noise distributions. Hofbauer and Sandholm showed that every such dynamic can be rewritten with a deterministic payoff perturbation (their Theorem 2.1), and used that to carry Lyapunov functions over to arbitrary noise distributions. This mission covers the first two classes of games in their main convergence theorem: symmetric games with an interior evolutionarily stable strategy, and two player zero-sum games.

Setting

A two player normal form game has strategy sets $S^1 = \{1,\dots,n^1\}$ and $S^2 = \{1,\dots,n^2\}$ and utilities $u^\alpha : S^1 \times S^2 \to \mathbb R$. Player $\alpha$'s mixed strategies form the simplex $\Delta S^\alpha$, and $\Sigma = \Delta S^1 \times \Delta S^2$. The payoff vector $U^\alpha(x^{-\alpha}) \in \mathbb R^{n^\alpha}$ lists the expected payoff of each pure strategy of $\alpha$ against the opponent's mixed strategy. The game is zero-sum if $u^1(s) = -u^2(s)$ for every profile $s$.

Each player $\alpha$ has a shock density $f^\alpha$ on $\mathbb R^{n^\alpha}$. The choice function $C^\alpha(\pi)_i = P(\operatorname{argmax}_j \pi_j + \varepsilon_j = i)$, for $\varepsilon$ with density $f^\alpha$, gives the perturbed best response $\tilde B^\alpha(x^{-\alpha}) = C^\alpha(U^\alpha(x^{-\alpha}))$. The densities are required to be strictly positive with continuously differentiable choice functions ("the conditions of Theorem 2.1").

Standard stochastic fictitious play. Pure strategies are identified with basis vectors $e_i$. Choices $\zeta_1$ are arbitrary. At every time $t \ge 1$ each player $\alpha$ draws a shock $\varepsilon^\alpha_t$ with density $f^\alpha$ and plays at time $t+1$ the pure strategy maximizing $U^\alpha_k(Z^{-\alpha}_t) + (\varepsilon^\alpha_t)_k$, where the beliefs are the time averages

$$Z_t = \frac1t \sum_{u=1}^t \zeta_u \in \Sigma .$$

The shocks are independent over time and across players. The expected motion of $Z_t$ is the perturbed best response dynamic

$$\text{(P)}\qquad \dot x^\alpha = \tilde B^\alpha(x^{-\alpha}) - x^\alpha \quad\text{on } \Sigma .$$

Symmetric games. A two player game is symmetric if $S^1 = S^2 = \{1,\dots,m\}$ and $u^1(i,j) = u^2(j,i)$; it is described by the matrix $A_{ij} = u^1(i,j)$, and $U^1(z) = Az$. In symmetric stochastic fictitious play two players in roles 1 and 2 play at every time, their shocks are independent and identically distributed with one density $f$, and the state is the average of all past plays in both roles,

$$\hat Z_t = \frac1{2t}\sum_{u=1}^t \big(\hat\zeta^1_u + \hat\zeta^2_u\big) \in \Delta S^1 .$$

Its mean dynamic is $\text{(SP)}\ \dot x = C(Ax) - x$ on $\Delta S^1$. A mixed strategy $x^*$ in the interior of $\Delta S^1$ is an interior evolutionarily stable strategy (ESS) if $x^*\cdot Ax > x\cdot Ax$ for all mixed $x \ne x^*$ near $x^*$.

Rest points and chain recurrence. For a dynamic $\dot x = F(x)$ on a compact set $X$, the rest points are the zeros of $F$ in $X$. A point $x$ is chain recurrent if for every $\varepsilon > 0$ one can return from $x$ to $x$ by following solution segments of length at least $1$, with jumps of size less than $\varepsilon$ between segments.

Formalization targets

Goal: Theorem 6.1 (i) and (ii)

(i) If $A$ has an interior ESS, then (SP) has a unique rest point $\hat x$ and

$$P\Big(\lim_{t\to\infty} \hat Z_t = \hat x\Big) = 1 .$$

(ii) If the two player game is zero-sum, then (P) has a unique rest point $x^*$ and

$$P\Big(\lim_{t\to\infty} Z_t = x^*\Big) = 1 .$$

Both hold for all shock densities meeting the conditions of Theorem 2.1, all probability spaces carrying the shocks, and all initial choices.

Milestones

1. Theorem 2.1: for such a density, the choice function $C$ is the unique maximizer $C(\pi) = \operatorname{argmax}_{y \in \operatorname{int}\Delta}(y\cdot\pi - V(y))$ for one admissible deterministic perturbation $V$.
2. With an interior ESS, $\hat\Lambda(x) = x\cdot Ax - V(x) - W(Ax)$, where $W(\pi) = \max_y (y\cdot\pi - V(y))$, is strictly concave and a strict Lyapunov function for the deterministically perturbed dynamic (SPV).
3. Its maximizer is the unique chain recurrent point of (SPV).
4. In zero-sum games, $\Lambda(x^1,x^2) = -V^1(x^1) - W^1(U^1(x^2)) - V^2(x^2) - W^2(U^2(x^1))$ is strictly concave and a strict Lyapunov function for (PV).
5. Its maximizer is the unique chain recurrent point of (P).
6. The maximizer of $\hat\Lambda$ is the unique chain recurrent point of (SP).

Significance

The theorem gives global, almost sure convergence of a learning process for arbitrary noise distributions, not only for the logit (Gumbel) noise under which the perturbed dynamic has a closed form. For zero-sum games it is the stochastic counterpart of Robinson's theorem. For symmetric games with an interior ESS it shows that a population learning by stochastic fictitious play settles at a single mixed state. Since the choice functions are continuous, the players' choice probabilities converge as well. The limit is the rest point of the perturbed dynamic, which approximates a Nash equilibrium (in case (i), the ESS) as the noise vanishes.

On the formal side, the paper's results are proved, but no part of them is machine-checked, and the platform has no model of learning in games, of chain recurrence, or of stochastic approximation. The mission produces a formal model of stochastic fictitious play as a random process, formal statements of the Hofbauer and Hofbauer–Hopkins Lyapunov functions, and the chain recurrence characterizations that connect them to the process.

Difficulty

The obvious route replaces the process $Z_t$ by the ODE (P) and argues that (P) converges. That step is where the argument is incomplete: convergence of every solution of (P) does not give convergence of the stochastic process, because a stochastic approximation can in principle circulate near a set of orbits the ODE never follows. The right invariant is the chain recurrent set, and the limit sets of the process lie in a connected component of it (Benaïm and Hirsch 1999; Benaïm 1999). The characterization therefore has to be of chain recurrence, which is strictly weaker than asymptotic stability of individual orbits.

The second obstacle is that (P) itself is defined through the noise distribution and admits no useful Lyapunov function in general. The Lyapunov functions exist for the deterministic form (PV)/(SPV), and moving between the two forms requires the representation of Theorem 2.1, whose perturbation $V$ has no closed form either.

Formalization scope

Players and strategies are indexed from $0$. Mixed profiles live in $\prod_\alpha \mathbb R^{n^\alpha}$ and every vector field is defined on that ambient space. The processes are defined pathwise from a family of shock vectors on an arbitrary probability space. Ties in the argmax are broken by the smallest index, an event of probability zero because the shocks have densities. The shock drawn at time $t$ produces the choice at time $t+1$. Shock densities are arbitrary strictly positive densities with continuously differentiable choice functions; no noise law is fixed, and the two players' densities in (ii) may differ. Independence is joint over times and players (and roles in (i)). The symmetric process has its own state in one simplex and is not the standard process applied to a symmetric game.

Deterministic perturbations are functions defined on the whole space whose values off the open simplex are ignored; derivatives are taken of their composition with the projection onto the affine plane $\{\sum_i y_i = 1\}$. Perturbed best responses in (PV) and (SPV) are supplied as maps together with the hypothesis that they are the unique maximizers. A strict Lyapunov function must increase strictly along every non-constant solution on $(0,\infty)$. The ESS definition includes $x \ne x^*$, which the source omits.

The conclusions assert existence and uniqueness of the rest point; they are not hypotheses. A statement for the ODE (P) in place of the process $Z_t$, for one fixed noise law, or with the ESS as the limit point would be a different theorem.

A complete development needs Theorem 2.1 (convex duality and the Legendre transform on the simplex), existence and uniqueness of solutions of (P), basic chain recurrence theory, and the stochastic approximation results of Benaïm and Hirsch, which are not restated here and are welcome as independent contributions. The model layer (games, payoff vectors, choice functions, stochastic fictitious play) is shared with the other missions of this series.

Selected references

• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70(6), 2265–2294, 2002. https://doi.org/10.1111/1468-0262.00376 (theorem numbers and pages here follow the authors' manuscript of February 21, 2002).
• D. Fudenberg and D. M. Kreps, Learning Mixed Equilibria, Games and Economic Behavior 5, 320–367, 1993. https://doi.org/10.1006/game.1993.1021
• Y. M. Kaniovski and H. P. Young, Learning Dynamics in Games with Stochastic Perturbations, Games and Economic Behavior 11, 330–363, 1995. https://doi.org/10.1006/game.1995.1054
• M. Benaïm and M. W. Hirsch, Mixed Equilibria and Dynamical Systems Arising from Fictitious Play in Perturbed Games, Games and Economic Behavior 29, 36–72, 1999. https://doi.org/10.1006/game.1999.0717
• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, 1–68, 1999. https://doi.org/10.1007/BFb0096509
• J. Robinson, An Iterative Method of Solving a Game, Annals of Mathematics 54, 296–301, 1951. https://doi.org/10.2307/1969530
• J. Hofbauer and E. Hopkins, Learning in Perturbed Asymmetric Games, Games and Economic Behavior 52, 133–152, 2005. https://doi.org/10.1016/j.geb.2004.06.006

Motivation

In the capacitated vehicle routing problem (CVRP) a fleet of $m$ vehicles of capacity $Q$ leaves a depot and serves $n$ customers; every customer is visited once, and the load of each route must not exceed $Q$. In practice customer demands are uncertain at planning time. The chance-constrained CVRP asks that each route respect the capacity with probability at least $1-\epsilon$, but this presupposes a known demand distribution, which is rarely available. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) require the chance constraints to hold for every distribution in an ambiguity set $\mathcal P$ built from the information that can actually be estimated: support, means and dispersion bounds.

Their branch-and-cut method separates rounded capacity inequalities whose right-hand side is the worst-case value-at-risk of the total demand of a customer set $S$. This quantity is evaluated thousands of times during the search, so it matters whether it has a closed form or a small convex reformulation. This mission concerns the paper's covariance ambiguity sets (§5.2), which bound the whole covariance matrix of the demands and can therefore express that demands of nearby customers are correlated, as happens with geographically clustered demand. The covariance bound can be derived from data, for example analytically through McDiarmid's inequality (Delage and Ye, 2010) or by bootstrapping.

Setting

Customers are indexed by $i\in\{1,\dots,n\}$ and their random demand vector is $\tilde{\boldsymbol q}\in\mathbb R^n$. Fix a box $\mathcal Q=[\underline{\boldsymbol q},\overline{\boldsymbol q}]$ with $\underline{\boldsymbol q}\ge\mathbf 0$, a mean vector $\boldsymbol\mu$ in the interior of $\mathcal Q$, and a symmetric positive definite matrix $\Sigma\succ0$. The covariance ambiguity set is

$$\mathcal P=\Big\{\mathbb P\in\mathcal P_0(\mathbb R^n):\ \mathbb P[\tilde{\boldsymbol q}\in\mathcal Q]=1,\ \mathbb E_{\mathbb P}[\tilde{\boldsymbol q}]=\boldsymbol\mu,\ \mathbb E_{\mathbb P}\big[(\tilde{\boldsymbol q}-\boldsymbol\mu)(\tilde{\boldsymbol q}-\boldsymbol\mu)^\top\big]\preceq\Sigma\Big\},\tag{16}$$

where $\mathcal P_0(\mathbb R^n)$ is the set of all probability distributions on $\mathbb R^n$ and $A\preceq\Sigma$ means that $\Sigma-A$ is positive semidefinite.

For a distribution $\mathbb P$ and a real random variable $\tilde X$, the value-at-risk at level $1-\epsilon$, $\epsilon\in(0,1)$, is $\mathbb P\text{-VaR}_{1-\epsilon}[\tilde X]=\inf\{x\in\mathbb R:\mathbb P[\tilde X\le x]\ge1-\epsilon\}$. For a customer set $S$, the worst-case value-at-risk is $\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}[\sum_{i\in S}\tilde q_i]$. A route serving $S$ satisfies the chance constraint for every $\mathbb P\in\mathcal P$ exactly when this number is at most $Q$.

Two componentwise bounds appear in the answer:

$$\boldsymbol q^\ell=\max\Big\{-\tfrac{1-\epsilon}{\epsilon}(\overline{\boldsymbol q}-\boldsymbol\mu),\ \underline{\boldsymbol q}-\boldsymbol\mu\Big\},\qquad\boldsymbol q^u=\min\Big\{\tfrac{1-\epsilon}{\epsilon}(\boldsymbol\mu-\underline{\boldsymbol q}),\ \overline{\boldsymbol q}-\boldsymbol\mu\Big\}.$$

A route set is an ordered partition of the customers into $m$ nonempty ordered routes. It is feasible in the distributionally robust problem RVRP($\mathcal P$) if every route satisfies the chance constraint for every $\mathbb P\in\mathcal P$, and feasible in a deterministic instance with capacity $Q'$ and demands $\boldsymbol q$ if every route's total demand is at most $Q'$.

Formalization targets

Goal: Theorem 7

For every customer set $S$,

$$\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]=\max\Big\{\mathbf 1_S^\top\boldsymbol\mu+\mathbf 1_S^\top\boldsymbol q:\ \boldsymbol q^\top\Sigma^{-1}\boldsymbol q\le\tfrac{1-\epsilon}{\epsilon},\ \boldsymbol q\in[\boldsymbol q^\ell,\boldsymbol q^u]\Big\}.\tag{17}$$

The right-hand side maximizes an affine function over the intersection of an ellipsoid and a box.

Milestone: Corollary 4 (corrected)

For a diagonal bound $\Sigma=\operatorname{diag}(\sigma_1^2,\dots,\sigma_n^2)$, program (17) collapses to a search over one parameter $\theta\ge0$ with $S(\theta)=\{i\in S:\sigma_i^2>\theta q^u_i\}$:

$$\sup_{\theta}\ \mathbf 1_S^\top\boldsymbol\mu+\sum_{i\in S(\theta)}q^u_i+\sqrt{\Big[\tfrac{1-\epsilon}{\epsilon}-\sum_{i\in S(\theta)}\big(\tfrac{q^u_i}{\sigma_i}\big)^2\Big]\Big[\sum_{i\in S\setminus S(\theta)}\sigma_i^2\Big]},\tag{18}$$

over the $\theta$ for which the first bracket is nonnegative and the point of (17) that $\theta$ induces respects $\boldsymbol q^u$ (see Formalization scope).

Milestone: Theorem 6

For some instance with the ambiguity set (16), no deterministic CVRP instance on the same customers and fleet has the same set of feasible route sets.

Significance

Theorem 7 makes the worst-case value-at-risk over (16) computable in polynomial time as a convex quadratically constrained program. With it, the rounded capacity inequalities of the two-index vehicle flow formulation can be separated for covariance information. Theorem 2 of the same paper shows that the resulting demand estimator is subadditive, so this formulation is exact. Corollary 4 gives a closed form for the diagonal case, which the paper uses to evaluate the estimator in time linear in $|S|$ after sorting. Theorem 6 explains why the paper needs this machinery: the robust feasible region cannot be reproduced by any deterministic demand vector and capacity.

The results are proved in the paper's online supplement. No part of them is formalized anywhere to our knowledge; the platform has no worst-case value-at-risk and no moment-based ambiguity set. A complete development would give machine-checked worst-case VaR bounds over moment sets with second-order information. These are used well beyond routing, in distributionally robust portfolio and inventory models.

Difficulty

The supremum ranges over an infinite-dimensional set of distributions, while (17) ranges over vectors. The inequality "$\ge$" requires, for every feasible $\boldsymbol q$ of (17), a sequence of distributions in (16) whose value-at-risk approaches $\mathbf 1_S^\top(\boldsymbol\mu+\boldsymbol q)$. The value-at-risk is a lower quantile, so a distribution placing mass exactly $\epsilon$ on a high point does not attain the value: the construction has to be a limit. The inequality "$\le$" is harder. It must rule out every distribution, not only two-point ones, and a bound through the one-dimensional Chebyshev–Cantelli inequality for $\sum_{i\in S}\tilde q_i$ alone ignores the box: it yields $\sqrt{\frac{1-\epsilon}{\epsilon}\mathbf 1_S^\top\Sigma\mathbf 1_S}$, which is too large whenever the support bounds bind. The interaction between the Loewner constraint and the componentwise support bounds, which produces the unusual bound $\boldsymbol q^\ell$, is where the work lies. For Theorem 6 the difficulty is to exhibit the instance and to evaluate enough chance constraints exactly.

Formalization scope

Customers are Fin n (0-based) and demand vectors are Fin n → ℝ. Distributions are measures on Fin n → ℝ. The set (16) is covarianceSet qlo qhi μ Sig: a probability measure with P (Set.Icc qlo qhi) = 1, coordinate means μ, and Sig - M positive semidefinite, where M is the matrix of integrals $\int(q_i-\mu_i)(q_j-\mu_j)\,d\mathbb P$. The covariance bound is called Sig because Σ is Lean syntax. The side conditions $\underline{\boldsymbol q}\ge\mathbf 0$, $\boldsymbol\mu\in\operatorname{int}\mathcal Q$, $\Sigma\succ0$ (Sig.PosDef) and $0<\epsilon<1$ are hypotheses of every theorem. The value-at-risk is the published MultistageStochastic.valueAtRisk P Y (1 - ε). The worst-case value-at-risk is a real sSup over the image of the set. That image is nonempty (the Dirac measure at $\boldsymbol\mu$ lies in (16)) and bounded (the box), so the supremum is genuine. "The optimal objective value" of a maximization is stated as a supremum; attainment is not part of any claim. $\Sigma^{-1}$ is Mathlib's matrix inverse.

The paper states Theorem 7 and Corollary 4 with "$\mathbb P$-VaR" without a level; the level $1-\epsilon$, used in the sentence introducing Theorem 7 and everywhere else, is read in. Corollary 4 as printed is false. It maximizes over every $\theta\ge0$ with a nonnegative bracket. For $n=1$, every large $\theta$ then gives the value $\mu_1+\sigma_1\sqrt{(1-\epsilon)/\epsilon}$, which can exceed $\overline q_1$ and hence every value-at-risk. The formal statement adds the condition that makes each $\theta$ a feasible point of (17): $\sigma_i^2\sqrt{s(\theta)}\le q^u_i\sqrt{\sum_{k\in S\setminus S(\theta)}\sigma_k^2}$ for $i\in S\setminus S(\theta)$, where $s(\theta)$ is the first bracket. With this condition the statement is the diagonal case of Theorem 7.

A theorem about the Lean set is trivial if the set is empty or the supremum is a junk value. Neither happens here, and replacing the Loewner constraint by a scalar variance bound on $\sum_{i\in S}\tilde q_i$ would state a different theorem. The dual second-order cone program printed after Theorem 7 is not a target: as printed it has the all-ones vector where Lagrangian duality gives $\mathbf 1_S$, and it has no multiplier for $\boldsymbol q\ge\boldsymbol q^\ell$.

Needed infrastructure: quantiles of pushforward measures, the Loewner order on moment matrices, and finite-support (two-point) distributions. The value-at-risk lemmas and the moment-matrix lemmas are reusable beyond this mission, and contributions of either kind are welcome. Theorem 6 needs only the route-set layer defined here and one explicit instance.

Selected references

• S. Ghosal and W. Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Operations Research 68(3):716–732, 2020. https://doi.org/10.1287/opre.2019.1924
• E. Delage and Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511804441
• G. Laporte, Y. Nobert and M. Desrochers, Optimal Routing under Capacity and Distance Restrictions, Operations Research 33(5):1050–1073, 1985. https://doi.org/10.1287/opre.33.5.1050

Motivation

In the capacitated vehicle routing problem (CVRP) a depot serves customers $V_C=\{1,\dots,n\}$ with $m$ vehicles of capacity $Q$, and every route must respect the capacity. When customer demands are uncertain, the distributionally robust chance-constrained CVRP of Ghosal and Wiesemann (Oper. Res. 68(3), 2020) requires every route to meet its capacity with probability at least $1-\epsilon$ under every distribution in an ambiguity set $\mathcal P$, a family of distributions consistent with what is known about the demands. Such constraints are handled in a branch-and-cut scheme through rounded capacity inequalities, whose right-hand sides require one quantity for each customer subset $S$: the worst-case value-at-risk of the cumulative demand of $S$.

For ambiguity sets that describe each customer separately (marginal moment sets), this quantity is additive over customers and the problem reduces to a deterministic CVRP. Such sets cannot express that the demands of customers in the same municipality, county or state vary jointly within limits. The first-order generic moment ambiguity set does express this: it bounds the mean absolute deviation of the cumulative demand of prescribed customer groups. The mean absolute deviation is a standard robust dispersion measure, less sensitive to outliers than the standard deviation (see Casella and Berger, Statistical Inference, 2002). This mission formalizes the paper's description of the worst-case value-at-risk over such sets.

Setting

Demands form a random vector $\tilde{\boldsymbol q}$ on $\mathbb R^n$. The data are a support box $\mathcal Q=[\underline{\boldsymbol q},\overline{\boldsymbol q}]$ with $\underline{\boldsymbol q}\ge\mathbf 0$, a mean vector $\boldsymbol\mu$ in the interior of $\mathcal Q$, customer subsets $S_1,\dots,S_p\subseteq V_C$ and bounds $\boldsymbol\nu>\mathbf 0$. For $A\subseteq V_C$, $\mathbf 1_A\in\{0,1\}^n$ is its indicator vector. The first-order generic moment ambiguity set, Eq. (12) of the paper, is

$$\mathcal P=\Bigl\{\mathbb P\in\mathcal P_0(\mathbb R^n):\ \mathbb P[\tilde{\boldsymbol q}\in\mathcal Q]=1,\ \mathbb E_{\mathbb P}[\tilde{\boldsymbol q}]=\boldsymbol\mu,\ \mathbb E_{\mathbb P}\bigl[\mathbf 1_{S_i}^\top|\tilde{\boldsymbol q}-\boldsymbol\mu|\bigr]\le\nu_i\ \ \forall i=1,\dots,p\Bigr\},$$

where $\mathcal P_0(\mathbb R^n)$ is the set of probability distributions on $\mathbb R^n$ and $|\cdot|$ acts componentwise. The subsets are arbitrary: they may overlap and need not cover $V_C$.

For a risk level $\epsilon\in(0,1)$ and a random variable $\tilde X$, the value-at-risk is $\mathbb P\text{-VaR}_{1-\epsilon}[\tilde X]=\inf\{x\in\mathbb R:\mathbb P[\tilde X\le x]\ge1-\epsilon\}$. For a customer subset $S$ the quantity of interest is

$$\sup_{\mathbb P\in\mathcal P}\ \mathbb P\text{-VaR}_{1-\epsilon}\Bigl[\sum_{i\in S}\tilde q_i\Bigr].$$

Write $\hat{\boldsymbol q}=\min\{\overline{\boldsymbol q}-\boldsymbol\mu,\ \frac{1-\epsilon}{\epsilon}(\boldsymbol\mu-\underline{\boldsymbol q})\}$ (componentwise) and $[\cdot]_+$ for the componentwise positive part. A route set $\mathbf R=(\mathbf R_1,\dots,\mathbf R_m)$ partitions $V_C$ into $m$ nonempty ordered routes. It is feasible in the deterministic CVRP with demands $\boldsymbol q$ if $\sum_{i\in\mathbf R_k}q_i\le Q$ for all $k$, and feasible in the distributionally robust CVRP if $\mathbb P[\sum_{i\in\mathbf R_k}\tilde q_i\le Q]\ge1-\epsilon$ for all $\mathbb P\in\mathcal P$ and all $k$.

Formalization targets

Goal: Theorem 5 (p. 726)

For every customer subset $S$,

$$\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Bigl[\sum_{i\in S}\tilde q_i\Bigr]=\inf_{\boldsymbol\gamma\in\mathbb R^p_+}\ \mathbf 1_S^\top\boldsymbol\mu+\hat{\boldsymbol q}^\top\Bigl[\mathbf 1_S-2\sum_{i=1}^p\gamma_i\mathbf 1_{S_i}\Bigr]_+ +\frac1\epsilon\boldsymbol\nu^\top\boldsymbol\gamma .$$

The right-hand side is the optimal value of the paper's problem (13). The statement holds for every family of subsets and all data satisfying the standing assumptions, so it is the general form of which the milestones are special cases.

Corollary 2 (p. 726, Eq. (14))

If $S_1,\dots,S_{p-1}$ are pairwise disjoint and cover $V_C$ and $S_p=V_C$, then

$$\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Bigl[\sum_{i\in S}\tilde q_i\Bigr]=\mathbf 1_S^\top\boldsymbol\mu+\min\Bigl\{\frac{\nu_p}{2\epsilon},\ \sum_{i=1}^{p-1}\min\Bigl\{\mathbf 1_{S\cap S_i}^\top\hat{\boldsymbol q},\ \frac{\nu_i}{2\epsilon}\Bigr\}\Bigr\}.$$

Corollary 3 (pp. 726–727, Eq. (15))

If $p=n+1$, $S_i=\{i\}$ for $i\le n$ and $S_{n+1}=V_C$, then

$$\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Bigl[\sum_{i\in S}\tilde q_i\Bigr]=\mathbf 1_S^\top\boldsymbol\mu+\min\Bigl\{\frac{\nu_{n+1}}{2\epsilon},\ \sum_{i\in S}\min\Bigl\{\hat q_i,\ \frac{\nu_i}{2\epsilon}\Bigr\}\Bigr\}.$$

Theorem 4 (p. 726)

For some instance with an ambiguity set of the form (12), no deterministic CVRP instance on the same customers and vehicles (capacity $Q'\ge0$, demands $\boldsymbol q'\ge\mathbf 0$) has the same set of feasible route sets.

Significance

Theorem 5 makes the worst-case value-at-risk over (12) computable in polynomial time as the value of a nonsmooth convex problem over the nonnegative orthant, which the paper notes can be written as a linear program. This gives the right-hand sides of the rounded capacity inequalities in a branch-and-cut scheme for the distributionally robust CVRP. Corollaries 2 and 3 give closed forms for two structured families of groups, evaluable in time linear in $|S|$. Theorem 4 shows the gain in modelling power has a cost: unlike the marginal case, the problem cannot in general be replaced by a deterministic CVRP with altered demands. With a single customer and $S_1=\{1\}$, Theorem 5 reduces to the closed form $\mu+\min\{\hat q,\nu/(2\epsilon)\}$ for marginalized first-order sets, so it extends that single-customer formula to joint dispersion constraints.

All four results are proved in the paper's online supplement. As far as a platform search shows, none has been machine-checked. The mission produces checked proofs of the equality in Theorem 5, the two closed forms, and an explicit instance for Theorem 4.

Difficulty

The supremum ranges over an infinite-dimensional set of joint distributions, and the value-at-risk is neither convex nor concave in the distribution. Bounding the value-at-risk of each group separately and adding the bounds does not work when groups overlap, and it ignores the total-dispersion constraint. It gives only an upper bound, and in the setting of Corollary 2 that bound is strict whenever the total bound $\nu_p/(2\epsilon)$ is the binding term. Showing that the infimum in (13) is attained in the limit needs distributions that saturate several overlapping dispersion constraints at once while keeping the mean fixed and the support inside the box. For Theorem 4, the witness must separate the feasible-route-set family of the robust instance from every family defined by a single linear capacity inequality with nonnegative weights.

Formalization scope

Customers are Fin n (0-based), subsets are Sfam : Fin p → Finset (Fin n), and a distribution is a Measure (Fin n → ℝ) that is required to be a probability measure. Support is P (Set.Icc qlo qhi) = 1, the mean condition is ∫ q, q j ∂P = μ j, and the dispersion condition is ∫ q, ∑ j ∈ Sfam l, |q j - μ j| ∂P ≤ ν l. The integrability clauses stated alongside are automatic for measures carried by the box. The value-at-risk is the published MultistageStochastic.valueAtRisk P Y (1 - ε). The worst-case value-at-risk is the real sSup of its image over the set; under the standing assumptions this image is nonempty (the Dirac at $\boldsymbol\mu$ lies in the set) and bounded (bounded support), so the real supremum is the paper's. The optimal value of (13) is the real sInf of the objective over $\{\boldsymbol\gamma\ge\mathbf 0\}$, a nonempty set on which the objective is bounded below by $\mathbf 1_S^\top\boldsymbol\mu$. Attainment is not claimed. All statements carry the standing assumptions $\underline{\boldsymbol q}\ge\mathbf 0$, $\underline{\boldsymbol q}<\boldsymbol\mu<\overline{\boldsymbol q}$, $\boldsymbol\nu>\mathbf 0$ and $0<\epsilon<1$. Corollary 2 writes $p=r+1$ with the last subset Sfam (Fin.last r). Corollary 3 indexes the singleton of customer $i$ by Fin.castSucc i. In Theorem 4 route sets are Fin m → List (Fin n) and only feasibility is modelled; costs play no role.

The theorems are not trivialized by an empty ambiguity set or a junk supremum: membership of the Dirac distribution at $\boldsymbol\mu$ is checked locally with a sorry-free proof. Theorem 4 needs a genuinely separating instance: an instance in which no route set is robustly feasible, for example, is matched by a deterministic instance in which none is feasible either.

Needed infrastructure: two-point and finitely supported distributions on $\mathbb R^n$ and their value-at-risk; weak duality for moment problems over the box; the positive-part calculus of (13). The value-at-risk lemmas for finitely supported measures are reusable in the sibling missions on this paper. Contributions of any of the milestones, of lemmas for these building blocks, or of either inequality of Theorem 5 on its own are welcome.

Selected references

• S. Ghosal and W. Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Operations Research 68(3):716–732, 2020. https://doi.org/10.1287/opre.2019.1924
• G. Casella and R. L. Berger, Statistical Inference, 2nd ed., Duxbury, 2002.
• S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511804441
• G. Laporte, Y. Nobert and M. Desrochers, Optimal routing under capacity and distance restrictions, Operations Research 33(5):1050–1073, 1985. https://doi.org/10.1287/opre.33.5.1050

Motivation

The capacitated vehicle routing problem (CVRP) assigns customers to a fleet of $m$ identical vehicles of capacity $Q$ and orders each vehicle's visits so as to minimize transportation cost, subject to each vehicle's total load not exceeding $Q$. In practice the customers' demands are not known when the routes are planned. Two classical responses are the robust CVRP, which requires feasibility for every demand vector in an uncertainty set, and the chance-constrained CVRP, which requires each capacity constraint to hold with probability at least $1-\epsilon$ under a known demand distribution. The first ignores all distributional information; the second assumes a distribution that is rarely known and usually requires independent demands.

Ghosal and Wiesemann (Oper. Res. 68(3), 2020) study the distributionally robust chance-constrained CVRP, RVRP($\mathcal P$), in which each capacity constraint must hold with probability at least $1-\epsilon$ under every distribution of an ambiguity set $\mathcal P$. Whether this problem can be solved with existing CVRP technology depends on how the worst-case value-at-risk of a customer set's total demand behaves as a set function. This mission formalizes §4 of the paper, which treats ambiguity sets that only constrain each customer's demand separately.

Setting

There are $n$ customers $V_C=\{1,\dots,n\}$ with random demand vector $\tilde{\boldsymbol q}\in\mathbb R^n$ and a risk level $\epsilon\in(0,1)$. For a probability distribution $\mathbb P$ and a real random variable $\tilde X$, the value-at-risk is

$$\mathbb P\text{-VaR}_{1-\epsilon}[\tilde X]=\inf\{x\in\mathbb R:\ \mathbb P[\tilde X\le x]\ge1-\epsilon\}.$$

For an ambiguity set $\mathcal P$ and a customer subset $S$, the worst-case value-at-risk of $S$ is $\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}[\sum_{i\in S}\tilde q_i]$.

Fix a support box $\mathcal Q=[\underline{\boldsymbol q},\overline{\boldsymbol q}]$ with $\underline{\boldsymbol q}\ge\mathbf 0$, a mean vector $\boldsymbol\mu$ in the interior of $\mathcal Q$, and for each customer $i$ a componentwise convex dispersion measure $\boldsymbol\varphi_i:\mathbb R\to\mathbb R^{p_i}$ with bound $\boldsymbol\sigma_i>\boldsymbol\varphi_i(\mu_i)$. The marginalized moment ambiguity set (5) is

$$\mathcal P=\Big\{\mathbb P\in\mathcal P_0(\mathbb R^n):\ \mathbb P(\tilde{\boldsymbol q}\in\mathcal Q)=1,\ \mathbb E_{\mathbb P}[\tilde{\boldsymbol q}]=\boldsymbol\mu,\ \mathbb E_{\mathbb P}[\boldsymbol\varphi_i(\tilde q_i)]\le\boldsymbol\sigma_i\ \forall i\in V_C\Big\}.$$

It constrains marginal moments only, and so contains joint distributions of every dependence structure, from independent to perfectly correlated demands. Three special cases have their own closed forms: the first-order set (6), where $\sigma_i>0$ bounds the mean absolute deviation $\mathbb E|\tilde q_i-\mu_i|$; the variance set (8), where $\sigma_i>0$ bounds $\mathbb E(\tilde q_i-\mu_i)^2$; and the semivariance set (10), where $\sigma_i^+,\sigma_i^->0$ bound $\mathbb E[\tilde q_i-\mu_i]_+^2$ and $\mathbb E[\mu_i-\tilde q_i]_+^2$.

A route set $\mathbf R=(R_1,\dots,R_m)\in\mathfrak P(V_C,m)$ partitions the customers into $m$ nonempty ordered routes. It is feasible in RVRP($\mathcal P$) if $\mathbb P[\sum_{i\in R_k}\tilde q_i\le Q]\ge1-\epsilon$ for all $\mathbb P\in\mathcal P$ and all $k$, and feasible in the deterministic CVRP with demands $\boldsymbol q$ if $\sum_{i\in R_k}q_i\le Q$ for all $k$.

Formalization targets

Goal: Theorem 3 (p. 723)

For every marginalized moment ambiguity set (5) and every nonempty $S\subseteq V_C$,

$$\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]=\sum_{i\in S}\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}[\tilde q_i].$$

The dispersion measures are left arbitrary (convex, componentwise, any number of components), so the goal covers every set of the form (5).

Milestones

• Proposition 2 (p. 724, Eq. (7)), first-order sets: $\sup_{\mathbb P}\mathbb P\text{-VaR}_{1-\epsilon}[\tilde q_i]=\mu_i+\min\{\overline q_i-\mu_i,\frac{1-\epsilon}{\epsilon}(\mu_i-\underline q_i),\frac1{2\epsilon}\sigma_i\}$.
• Proposition 3 (p. 725, Eq. (9)), variance sets: the same with last term $\sqrt{\frac{1-\epsilon}{\epsilon}\sigma_i}$.
• Proposition 4 (p. 725, Eq. (11)), semivariance sets: the four-term minimum with $\sqrt{\sigma_i^+/\epsilon}$ and $\sqrt{(1-\epsilon)\sigma_i^-}/\epsilon$.
• Corollary 1 (p. 723): a route set is feasible in RVRP($\mathcal P$) over (5) if and only if it is feasible in the deterministic CVRP with demands $q_i=\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}[\tilde q_i]$.

Significance

Theorem 3 says that over (5) the worst case of a sum is the sum of the worst cases. Because the value-at-risk is not additive for a fixed distribution, and the online supplement exhibits distributions in such a set for which the individual values-at-risk are not additive, the statement is about the ambiguity set, not about any of its members. Its consequence, Corollary 1, is that RVRP($\mathcal P$) over (5) is a deterministic CVRP with inflated demands, so existing branch-and-cut and branch-and-cut-and-price codes solve it unchanged. Propositions 2–4 make those inflated demands explicit for three standard dispersion measures, so that the whole reduction is in closed form. The corollary also exposes a limitation: under (5) the worst-case distribution does not depend on the route set, and the model cannot represent known dependencies between customers.

The results are proved in the paper's online supplement; none has a machine-checked proof. A formalization produces a checked worst-case value-at-risk calculus over moment sets with support constraints, including sharp one-sided Chebyshev-type bounds under mean-absolute-deviation, variance and semivariance constraints, which are reusable in distributionally robust optimization beyond vehicle routing.

Difficulty

The value-at-risk is neither subadditive nor superadditive in general, so neither inequality of Theorem 3 follows from properties of a single distribution. The inequality "$\ge$" requires combining near-worst-case distributions of the individual customers into one joint distribution in $\mathcal P$ that is simultaneously near-worst for the sum; the inequality "$\le$" requires bounding the value-at-risk of the sum for an arbitrary joint law using only marginal information. In Propositions 2–4 the supremum is typically not attained: the distribution concentrating mass at the claimed worst-case value violates the mean constraint, and the value is reached only as a limit of distributions in $\mathcal P$. An argument that exhibits a single maximizer therefore fails, and the statements must be proved as equalities of suprema.

Formalization scope

Customers are Fin n (0-based) and demand vectors are Fin n → ℝ. An ambiguity set is a set of measures on Fin n → ℝ, each required to be a probability measure; the support condition is P (Set.Icc qlo qhi) = 1 and expectations are Bochner integrals. The sets are sets of joint laws on $\mathbb R^n$, never products of marginals. In (5) each expectation $\mathbb E_{\mathbb P}[\varphi_{i,l}(\tilde q_i)]$ is required to exist; this is automatic for convex $\varphi_{i,l}$ on the bounded support. The value-at-risk is the published definition MultistageStochastic.valueAtRisk P Y (1 - ε), and the worst-case value-at-risk is the real supremum of its values over the ambiguity set; under the standing assumptions that set of values is nonempty (the Dirac law at $\boldsymbol\mu$ belongs to $\mathcal P$) and bounded (by the support), so the supremum is not a default value. The single-customer quantity is the case $S=\{i\}$. The standing assumptions ($\underline{\boldsymbol q}\ge\mathbf 0$, $\underline{\boldsymbol q}<\boldsymbol\mu<\overline{\boldsymbol q}$, convexity of $\varphi_{i,l}$, $\varphi_{i,l}(\mu_i)<\sigma_{i,l}$, $\boldsymbol\sigma,\boldsymbol\sigma^\pm>\mathbf 0$, $0<\epsilon<1$) are explicit hypotheses. Routes are lists of customers; a route set has nonempty routes whose concatenation is a permutation of all customers. Costs are not formalized, since both routing problems minimize the same cost over their feasible route sets.

All targets are equalities or equivalences; a one-sided inequality, a statement asserting that some distribution attains the value, or a formulation over product measures is a different theorem and does not count.

Contributions welcome: the reduction of the chance constraint to a value-at-risk bound, the right-continuity lemmas for the value-at-risk of a measure on $\mathbb R^n$, two-point constructions in the ambiguity sets, and one-sided Chebyshev-type bounds with support constraints.

Selected references

• S. Ghosal and W. Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Operations Research 68(3):716–732, 2020. https://doi.org/10.1287/opre.2019.1924
• G. Laporte, Y. Nobert and M. Desrochers, Optimal routing under capacity and distance restrictions, Operations Research 33(5):1050–1073, 1985. https://doi.org/10.1287/opre.33.5.1050
• G. Casella and R. L. Berger, Statistical Inference, 2nd ed., Duxbury, 2002.

Motivation

The capacitated vehicle routing problem (CVRP) asks for a set of minimum-cost routes by which a fleet of identical vehicles of capacity $Q$, based at a depot, serves every customer exactly once without any vehicle carrying more than its capacity. In practice customer demands are not known when routes are planned. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) study the distributionally robust CVRP: the demand vector $\tilde{\boldsymbol q}$ is random, its distribution is known only to lie in an ambiguity set $\mathcal P$, and every route must respect its capacity with probability at least $1-\epsilon$ under every distribution in $\mathcal P$.

Exact CVRP solvers rely on compact two-index vehicle flow formulations strengthened by rounded capacity inequalities, which bound from below the number of vehicles entering any customer subset $S$ by a demand estimator $d(S)$. The paper shows (its Theorem 1) that the robust two-index formulation is exact whenever the demand estimator is subadditive and demands are nonnegative, and that this fails for some natural ambiguity sets: sets that fix the marginal distribution of each customer's demand violate it (Example 1). This mission formalizes the paper's positive result for the most widely used class of ambiguity sets, the moment ambiguity sets of distributionally robust optimization (see El Ghaoui et al. 2003, Delage and Ye 2010, Wiesemann et al. 2014).

Setting

There are $n$ customers, indexed $i=1,\dots,n$; the demand vector is $\tilde{\boldsymbol q}\in\mathbb R^n$. Fix

• a rectangular support $\mathcal Q=[\underline{\boldsymbol q},\overline{\boldsymbol q}]$ with $\underline{\boldsymbol q}\ge\mathbf 0$;
• a mean vector $\boldsymbol\mu\in\mathbb R^n$;
• a dispersion measure $\boldsymbol\varphi=(\varphi_1,\dots,\varphi_p):\mathbb R^n\to\mathbb R^p$ (for example mean absolute deviations $|q_i-\mu_i|$, variances $(q_i-\mu_i)^2$ or Huber losses) and bounds $\boldsymbol\sigma\in\mathbb R^p$.

The moment ambiguity set is

$$\mathcal P=\Big\{\mathbb P\in\mathcal P_0(\mathbb R^n):\ \mathbb P(\tilde{\boldsymbol q}\in\mathcal Q)=1,\ \ \mathbb E_{\mathbb P}[\tilde{\boldsymbol q}]=\boldsymbol\mu,\ \ \mathbb E_{\mathbb P}[\boldsymbol\varphi(\tilde{\boldsymbol q})]\le\boldsymbol\sigma\Big\},$$

where $\mathcal P_0(\mathbb R^n)$ denotes all probability distributions on $\mathbb R^n$. The paper's standing assumptions are $\boldsymbol\mu\in\operatorname{int}\mathcal Q$, each $\varphi_l$ closed and convex, and $\boldsymbol\varphi(\boldsymbol\mu)<\boldsymbol\sigma$.

For a distribution $\mathbb P$ the value-at-risk of a random variable is $\mathbb P\text{-VaR}_{1-\epsilon}[\tilde X]=\inf\{x\in\mathbb R:\mathbb P[\tilde X\le x]\ge1-\epsilon\}$, with risk level $\epsilon\in(0,1)$. The worst-case value-at-risk of a customer subset $S$ is $\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}[\sum_{i\in S}\tilde q_i]$, and the demand estimator (2) is

$$d_{\mathcal P}(S)=\max\left\{\left\lceil\frac1Q\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]\right\rceil,1\right\}\quad(S\neq\emptyset),\qquad d_{\mathcal P}(\emptyset)=0 .$$

The Lean development names these momentAmbiguitySet qlo qhi μ φ σ, worstCaseVaR, demandEstimator and twoPointMeasure in the namespace DRCVRP.Moment.

Formalization targets

Goal: Theorem 2 (p. 723)

For every moment ambiguity set satisfying the standing assumptions, every $\epsilon\in(0,1)$ and every $Q>0$,

$$d_{\mathcal P}(S\cup T)\le d_{\mathcal P}(S)+d_{\mathcal P}(T)\qquad\text{for all customer subsets } S,T .$$

This is condition (S) of the paper, stated for the rounded estimator (2) and for all pairs of subsets, overlapping or empty ones included.

Milestone: Proposition 1 (p. 723)

For every customer subset $S$ there are two-point distributions $\mathbb P^t=p_1^t\delta_{\boldsymbol q_1^t}+p_2^t\delta_{\boldsymbol q_2^t}\in\mathcal P$ with $p_1^t,p_2^t\ge0$ and $\boldsymbol q_1^t,\boldsymbol q_2^t\in\mathcal Q$ such that

$$\mathbb P^t\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]\longrightarrow\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]\qquad(t\to\infty).$$

Significance

Combined with the paper's Theorem 1, Theorem 2 says that for every moment ambiguity set with nonnegative demands the robust CVRP can be solved through the compact two-index formulation with robust rounded capacity inequalities, i.e. by the branch-and-cut machinery of the deterministic CVRP. It also separates moment ambiguity sets from ambiguity sets built from marginal histograms, hypothesis tests, $\phi$-divergences or Wasserstein balls, whose estimators can violate subadditivity. Proposition 1 describes the worst case: however many moment constraints the set contains, two demand scenarios suffice to approach the worst-case value-at-risk, strengthening the Richter–Rogosinski theorem for this functional.

Both results are proved in the paper's online supplement. They have not, to the best of current knowledge, been machine checked. This mission produces a checked statement and proof of both, together with a reusable encoding of moment ambiguity sets and of the worst-case value-at-risk over them. The companion missions of the series formalize the equivalence theorem (I) and the explicit worst-case VaR formulas for marginalized (III), first-order (IV) and covariance (V) ambiguity sets.

Difficulty

Value-at-risk is not subadditive for a single distribution, so the obvious route, subadditivity of the worst-case VaR followed by $\lceil a+b\rceil\le\lceil a\rceil+\lceil b\rceil$, needs an argument specific to the moment set; for the marginal-histogram set of Example 1 the worst-case VaR itself fails to be subadditive. The supremum over $\mathcal P$ ranges over an infinite-dimensional set of distributions and is in general not attained, so an argument that picks a maximizer does not apply, and the classical finite-support reduction (Richter–Rogosinski) yields a number of support points that grows with the number of moment constraints, not two. The integer rounding and the $\max\{\cdot,1\}$ must also be handled for all pairs of subsets, including overlapping ones.

Formalization scope

Customers are Fin n (0-based) and customer subsets are Finset (Fin n). Distributions are measures on Fin n → ℝ; membership in the moment set requires a probability measure giving mass one to the closed box Set.Icc qlo qhi, integrable coordinates with ∫ q, q i ∂P = μ i (an equality), and integrable φ l with ∫ q, φ l q ∂P ≤ σ l. The integrability clauses hold automatically under the standing assumptions and do not shrink the set. The dispersion measure is an arbitrary real-valued function whose components are convex (convex real functions on $\mathbb R^n$ are continuous, which covers "closed"); $p=0$ is allowed. The value-at-risk is the published platform definition MultistageStochastic.valueAtRisk at level $1-\epsilon$. The worst-case VaR is a real sSup; over a moment set satisfying the standing assumptions the set of VaRs is nonempty (the Dirac measure at $\boldsymbol\mu$ belongs to $\mathcal P$) and bounded by the box, so this is the true supremum. The estimator is integer valued. Every standing assumption is a hypothesis of both theorems.

Neither statement can be satisfied trivially: the goal is about the rounded estimator of the true supremum over a nonempty set, not about subadditivity of an arbitrary set function, and the milestone requires the two-point laws to lie in $\mathcal P$ and their VaRs to converge to the supremum, not to be attained. Extended-valued dispersion measures, such as the one expressing the covariance set of §5.2 as an instance of (4), are outside the scope of the real-valued encoding.

A complete development needs basic facts about quantiles of finitely supported measures, the structure of the moment set, and a duality or construction argument for the worst-case VaR. Lemmas about value-at-risk of two-point laws and about moment sets are reusable across the series. Proofs of the milestone, of the goal, and of intermediate lemmas are welcome.

Selected references

• S. Ghosal, W. Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Operations Research 68(3):716–732, 2020. https://doi.org/10.1287/opre.2019.1924
• L. El Ghaoui, M. Oks, F. Oustry, Worst-case value-at-risk and robust portfolio optimization: A conic programming approach, Operations Research 51(4):543–556, 2003. https://doi.org/10.1287/opre.51.4.543.16101
• E. Delage, Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• W. Wiesemann, D. Kuhn, M. Sim, Distributionally robust convex optimization, Operations Research 62(6):1358–1376, 2014. https://doi.org/10.1287/opre.2014.1314
• A. Shapiro, D. Dentcheva, A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, 2nd ed., SIAM, 2014. https://doi.org/10.1137/1.9781611973433

Motivation

Chapter 16 of Keller and Trotter's Applied Combinatorics (2017 Edition, CC BY-SA 4.0) is a survey of seven topics. Two of them are self-contained results with complete proofs on the page, and this mission formalizes both.

The first is the Lovász Local Lemma. It was introduced by Erdős and Lovász in 1975 to show that certain hypergraphs are 3-colourable (Erdős–Lovász 1975), and it has become a standard tool of the probabilistic method. The classical probabilistic argument shows that a random object has a property with probability close to one. The local lemma is different: it shows that a good object exists even when it is exceedingly rare, provided that each "bad" event depends on only a few of the others. It underlies lower bounds for Ramsey numbers such as $R(3,n) \ge c\,n^2/\ln^2 n$, the subject of Section 16.8. It also underlies results on colouring, satisfiability and Latin transversals, and the algorithmic version of Moser–Tardos (2010).

The second is the Gale–Ryser Theorem, proved independently by Gale (1957) and Ryser (1957). It decides when a zero–one matrix with prescribed row and column sums exists. Equivalently, it decides when a pair of sequences is the degree sequence of a bipartite graph. Its condition is a comparison in the dominance order on integer partitions.

Setting

A finite probability space is a finite set $\Omega$ with a function $P$ defined on all subsets, finitely additive, with $P(\emptyset) = 0$ and $P(\Omega) = 1$. Let $\mathcal F = (A_i)_{i \in \iota}$ be a finite family of events. For a subfamily $G \subseteq \iota$ write

$$\prod_{j \in G} \overline{A_j} = \bigcap_{j \in G} (\Omega \setminus A_j),$$

the event that every event of $G$ fails; for $G = \emptyset$ it is $\Omega$. Fix, for each $i$, a subfamily $N(i) \subseteq \iota \setminus \{i\}$. The event $A_i$ is independent of any event not in $N(i)$ if $P(A_i \mid \prod_{j\in G}\overline{A_j}) = P(A_i)$ for every $G$ with $i \notin G$ and $G \cap N(i) = \emptyset$. In the formalization this condition is IndepOutside μ A N i, written as

$$P\Big(A_i \cap \prod_{j\in G}\overline{A_j}\Big) = P(A_i)\,P\Big(\prod_{j\in G}\overline{A_j}\Big).$$

A partition of a positive integer $t$ is a non-increasing string $V = (v_1, \dots, v_m)$ of positive integers with sum $t$; $\mathcal P(t)$ is the set of partitions of $t$. It is partially ordered by $V \ge W$ iff $V$ is no longer than $W$ and every partial sum $v_1 + \dots + v_j$ is at least $w_1 + \dots + w_j$ (Dominates). $V$ covers $W$ when $V > W$ with nothing in between (Covers). The dual partition $V^d$ has $v_1$ entries, the $j$-th being the number of $i$ with $v_i \ge j$ (dual). A zero–one matrix with row sum string $R$ and column sum string $C$ is an $m \times n$ matrix with entries in $\{0,1\}$ whose row $i$ sums to $r_i$ and column $j$ to $c_j$ (IsZeroOneMatrixWithSums).

Formalization targets

Goal: the asymmetric local lemma (Lemma 16.14)

If $0 < x(i) < 1$ and $P(A_i) \le x(i)\prod_{j \in N(i)}(1 - x(j))$ for every $i$, then for every non-empty $G \subseteq \iota$

$$P\Big(\prod_{i \in G}\overline{A_i}\Big) \ge \prod_{i\in G}\big(1 - x(i)\big), \qquad\text{and}\qquad P\Big(\prod_{i\in\iota}\overline{A_i}\Big) > 0 .$$

Milestone: the symmetric local lemma (Lemma 16.15)

If $0 < p < 1$, $d \ge 1$, $P(A_i) \le p$, $|N(i)| \le d$ and $e\,p\,(d+1) < 1$, then

$$P\Big(\prod_{i\in\iota}\overline{A_i}\Big) \ge \Big(1 - \frac1{d+1}\Big)^{|\mathcal F|} > 0 .$$

Milestones: covers in $\mathcal P(t)$ and Gale–Ryser (Proposition 16.11, Theorem 16.12)

If $V$ covers $W$ in $\mathcal P(t)$, then $W$ arises from $V$ by moving one unit from a part $v_i$ to a later part $v_j$ (possibly a new part of size one), and all parts strictly between equal $v_i - 1$. For partitions $R, C$ of $t > 0$,

$$\exists\, M \in \{0,1\}^{m\times n} \text{ with row sums } R \text{ and column sums } C \iff R^d \ge C \text{ in } \mathcal P(t).$$

The Erdős–Ko–Rado bound of Theorem 16.8 enters as the published reference FamousTheorems.erdos_ko_rado.

Significance

The local lemma is the entry point to the probabilistic method's rare-event side. A formal statement in the book's form — finite spaces and the book's conditional notion of independence — is a reusable interface for formalizing its applications: Ramsey lower bounds, hypergraph colouring and $k$-SAT with bounded occurrences. The symmetric form is the version most applications call. Mathlib has no local lemma. The platform has a conditional-probability bound from an unrelated paper mission (Erdos390.WholePaper.finiteAsymmetricLocalLemma_conditionalBound), which bounds $P(A_i \cap \prod_{j\in s}\overline{A_j})$ with $0 \le x < 1$ and does not state the product lower bound for the joint failure.

Gale–Ryser is the prototype of margin problems for $\{0,1\}$-matrices and of degree-sequence characterizations (compare Erdős–Gallai for graphs). Formalizing it produces the dominance order, conjugate partitions and covering relations on sorted lists of positive integers. Mathlib has Nat.Partition but no dominance order or conjugate. None of these results is formalized on the platform. The results themselves are classical and proved; the work is formalizing the proofs.

Difficulty

For the local lemma, the naive induction on $|G|$ fails. Conditioning on the joint failure of a subfamily requires that failure to have positive probability, and that is only known after the inductive bound has been proved for smaller subfamilies. The induction must therefore carry the lower bound and the positivity of every smaller joint failure at once. It must also split each conditioning family into the part inside $N(i)$ and the part outside. The independence hypothesis controls only the part outside, and only through intersections of complements, not through arbitrary events.

For Gale–Ryser, necessity is an exchange argument, but sufficiency needs the fine structure of covers in the dominance order (Proposition 16.11): the case analysis of where the moved unit lands, including a new last part, and the fact that a maximal chain from $R^d$ down to $C$ exists. Converting the list-level statements into matrix constructions over Fin m × Fin n is the other main cost.

Formalization scope

• Probability space. Fintype Ω with DiscreteMeasurableSpace Ω and a measure μ with IsProbabilityMeasure μ; every subset is an event and probabilities are μ.real, as in the book's finite probability spaces.
• Family and neighbourhoods. The family is A : ι → Set Ω over a Fintype ι, so repeated events are allowed. Neighbourhoods are N : ι → Finset ι with i ∉ N i.
• Weights. 0 < x i < 1 is strict on both sides, as on the page.
• Independence. The conditional-probability equation is stated multiplicatively. This agrees with the book whenever the conditioning event has positive probability, and it is automatic otherwise.
• Excluded trivialization. The independence hypothesis is not full mutual independence of the family, which would make the product formula immediate. It is not pairwise independence either, under which the lemma is false. It is exactly the book's condition on intersections of complements.
• Explicit constant (Lemma 16.15). The book's displayed conclusion is misprinted: it mentions $\mathcal G$ and $x$, which are never introduced. The statement uses the bound the book's proof yields with $x(E) = 1/(d+1)$, namely $(1 - 1/(d+1))^{|\mathcal F|}$, with $|\mathcal F|$ = Fintype.card ι, together with positivity. Here $p$ and $d$ are real and $e$ is Real.exp 1.
• Partitions. Partitions are List ℕ, non-increasing with positive entries. Entries are 1-based through entry, and partial sums are (V.take j).sum.
• Dual partition. The page's rule "at least $n+1-j$" lists the conjugate in increasing order, and its example is misprinted (it sums to 40, not 42). The definition is the conjugate partition in non-increasing order, the only reading under which Theorem 16.12 holds.
• Matrices. Matrices are Matrix (Fin m) (Fin n) ℕ with entries in $\{0,1\}$.

Not included.

• The on-line colouring and antichain-partitioning results of Section 16.1 (Theorems 16.2, 16.4, 16.5) need a formal model of adaptive Builder/Assigner games.
• Theorem 16.9 (regular Markov chains) is stated without proof.
• Theorem 16.13 (van der Waerden) is stated without proof and followed by "Material will be added here".

Welcome contributions. Reusable infrastructure: a finite-space conditional-probability API, and the dominance order as a PartialOrder on sorted partitions linked to Nat.Partition.

Selected references

• M. T. Keller, W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 16, pp. 315–330. https://www.appliedcombinatorics.org/
• P. Erdős, L. Lovász, Problems and results on 3-chromatic hypergraphs and some related questions, Infinite and Finite Sets, 1975. https://www.renyi.hu/~p_erdos/1975-34.pdf
• D. Gale, A theorem on flows in networks, Pacific J. Math. 7 (1957). https://doi.org/10.2140/pjm.1957.7.1073
• H. J. Ryser, Combinatorial properties of matrices of zeros and ones, Canad. J. Math. 9 (1957). https://doi.org/10.4153/CJM-1957-044-3
• R. A. Moser, G. Tardos, A constructive proof of the general Lovász Local Lemma, J. ACM 57 (2010). https://doi.org/10.1145/1667053.1667060
• P. Erdős, C. Ko, R. Rado, Intersection theorems for systems of finite sets, Quart. J. Math. 12 (1961). https://doi.org/10.1093/qmath/12.1.313

Motivation

Ramsey theory studies the principle that complete disorder is impossible: every sufficiently large structure contains a large, perfectly uniform substructure. Its most familiar instance concerns graphs. In any graph on six vertices there are three vertices that are pairwise adjacent or three that are pairwise non-adjacent, and the same phenomenon persists at every scale. The quantity that measures it, the Ramsey number $R(m, n)$, is one of the most studied and least understood functions in combinatorics. Only a handful of values are known exactly ($R(3,3) = 6$, $R(4,4) = 18$), while $R(5,5)$ is only known to lie between 43 and 49 (Radziszowski, Small Ramsey Numbers).

The subject has a short, well-documented history. F. P. Ramsey proved the general theorem in 1930 as a lemma in decidability (Ramsey 1930). Erdős and Szekeres (1935) gave the upper bound $R(m, n) \le \binom{m+n-2}{m-1}$ (Erdős–Szekeres 1935). In 1947 Erdős proved an exponential lower bound for the diagonal numbers $R(n, n)$ by counting graphs (Erdős 1947); this argument is now regarded as the origin of the probabilistic method. In 1959 Erdős used the same method to show that graphs of large girth and large chromatic number exist (Erdős 1959). For decades the exponential bases $\sqrt 2$ and $4$ stood essentially unchanged; the upper base was lowered below $4$ only in 2023 (Campos–Griffiths–Morris–Sahasrabudhe).

This mission formalizes these results as presented in Chapter 11 of Keller and Trotter, Applied Combinatorics (2017 Edition).

Setting

A graph $G$ is a finite simple graph: a finite vertex set with a symmetric, irreflexive adjacency relation (no loops, no multiple edges). A complete subgraph on $m$ vertices is a set of $m$ pairwise adjacent vertices; an independent set of size $n$ is a set of $n$ pairwise non-adjacent vertices.

A non-negative integer $N$ is a Ramsey bound for $(m, n)$ if every graph with at least $N$ vertices contains a complete subgraph on $m$ vertices or an independent set of size $n$. The Ramsey number $R(m, n)$ is the least positive Ramsey bound. In Lean these are AppliedComb.Ramsey.IsRamseyBound m n N and AppliedComb.Ramsey.ramseyNumber m n.

More generally, write $[n] = \{1, \dots, n\}$ and $C(X, s)$ for the family of $s$-element subsets of $X$. For a string $h = (h_1, \dots, h_r)$, the number $R(s : h_1, \dots, h_r)$ is the least positive $N$ such that for every $n \ge N$ and every colouring $\phi : C([n], s) \to [r]$ some colour $\alpha$ has a set $H_\alpha \subseteq [n]$ of size $h_\alpha$ all of whose $s$-subsets receive colour $\alpha$ (hypergraphRamseyNumber s r h).

The girth of a graph is the smallest number of vertices on a cycle, and infinite for a forest; the chromatic number $\chi(G)$ is the least number of colours in a proper vertex colouring.

Formalization targets

Goal: Erdős's lower bound (Theorem 11.4)

For every positive integer $n$,

$$R(n, n) \;\ge\; \frac{n}{e\sqrt 2}\, 2^{n/2}.$$

Equivalently, below this threshold there is a graph on each number of vertices with neither a complete subgraph on $n$ vertices nor an independent set of size $n$. The statement is for every $n \ge 1$, with no asymptotic slack.

Milestones

• Lemma 11.1. Every graph with at least six vertices has a complete subgraph on 3 vertices or an independent set of size 3.
• Theorem 11.2 (Ramsey's Theorem for Graphs). For positive integers $m, n$ the least positive integer $R(m, n)$ exists.
• Theorem 11.6. For positive integers $r, s$ and $h_1, \dots, h_r \ge s$, the least positive integer $R(s : h_1, \dots, h_r)$ exists.
• Theorem 11.7 (Erdős). For all integers $g \ge 3$ and $t$ there is a graph with $\chi(G) > t$ and girth greater than $g$.

A further item, not a milestone because the book does not number it, records the bound that the proof of Theorem 11.2 establishes: every graph with at least $\binom{m+n-2}{m-1}$ vertices has a complete subgraph on $m$ vertices or an independent set of size $n$.

Significance

The goal is the diagonal lower bound that every later improvement is measured against. With the upper bound from the proof of Theorem 11.2 it shows that $R(n,n)$ grows exponentially, with base between $\sqrt 2$ and $4$. No explicit construction is known to give $R(n, n) > c^n$ for any constant $c > 1$. Theorem 11.7 is the standard example of a statement whose only known proofs for decades were probabilistic, and it shows that chromatic number is not a local property.

On the formal side, Mathlib has cliques, independent sets, girth and chromatic number, but no Ramsey numbers, no Erdős lower bound and no high-girth theorem. The platform already has weaker or differently shaped relatives, all checked for this mission. Erdos1947.ramsey_lower_bound gives a graph on $2^{\lfloor k/2 \rfloor}$ vertices without monochromatic $k$-sets, a weaker bound than the goal's. BookSixth.high_girth_chromatic is a single-parameter form of Theorem 11.7 in another Lean environment. ramsey_theory_upper_bound is a diagonal $4^k$ bound. The goal statement carries the constant $1/(e\sqrt2)$ exactly, which requires an explicit, non-asymptotic lower bound for $n!$ where the book writes "Stirling's approximation".

Difficulty

The obvious route to the goal is to count graphs with a large clique or independent set and compare the result with the total number of graphs. Two steps of that route do not go through as written in the text. First, the book replaces $n!$ by its Stirling approximation, which is only asymptotic; a statement for every $n \ge 1$ needs an inequality valid for all $n$, and the constant $1/(e\sqrt2)$ leaves no room for a cruder estimate such as $n! \ge (n/e)^n$ alone. Second, the counting argument yields a graph on each $t$ below the threshold, whereas $R(n,n)$ is defined as a least threshold over all graphs with at least that many vertices; the two have to be connected.

Theorem 11.7 needs random graphs with edge probability depending on $n$, a first-moment bound on short cycles and on independent sets, and a deletion step. The book states Theorem 11.6 without proof.

Formalization scope

• Graphs are Mathlib SimpleGraph V on a finite type V : Type (Theorems 11.1, 11.2, 11.4) or on Fin N (Theorem 11.7). Cliques and independent sets are SimpleGraph.IsNClique and SimpleGraph.IsNIndepSet on a Finset.
• IsRamseyBound m n N quantifies over every graph with at least $N$ vertices, as the book does; ramseyNumber m n is the sInf of the positive Ramsey bounds. Theorem 11.2 is stated as IsLeast {N | 0 < N ∧ IsRamseyBound m n N} (ramseyNumber m n), so its content is the nonemptiness of that set. The same pattern is used for Theorem 11.6.
• The goal compares real numbers: (n : ℝ) / (Real.exp 1 * Real.sqrt 2) * (2 : ℝ) ^ ((n : ℝ) / 2) ≤ (ramseyNumber n n : ℝ), with a real power. Explicit constant: the book says "use the Stirling approximation … after some algebra"; the statement keeps the book's constant $1/(e\sqrt 2)$ and holds for every $n \ge 1$ with no threshold.
• The bound of the proof of Theorem 11.2 is stated as the Ramsey property at $\binom{m+n-2}{m-1}$, not as an inequality on ramseyNumber, so it cannot hold through an empty defining set.
• Girth is Mathlib's SimpleGraph.egirth (valued in $\mathbb N \cup \{\infty\}$, $\infty$ for forests), not SimpleGraph.girth, which is $0$ on forests. Chromatic number is SimpleGraph.chromaticNumber in $\mathbb N \cup \{\infty\}$. The parameter $t$ of Theorem 11.7 is a natural number; negative $t$ is trivial.
• Theorem 11.6 is printed with typos: $h_i \ge s$ is read for all $i = 1, \dots, r$, the undefined $n_0$ is read as $R(s : h_1, \dots, h_r)$, and $C([n], s]$ as $C([n], s)$. Colourings are functions on the subtype of $s$-element subsets of Fin n, with colours in Fin r.
• Trivializing formalizations ruled out. A Ramsey number defined as an arbitrary upper bound, or as a supremum with junk value $0$, would make the goal vacuous or false. Here the goal's right-hand side is positive, so it forces the defining set to be nonempty, and every graph is simple on exactly its vertex type, with no loops or multiple edges.
• Reusable infrastructure: IsRamseyBound/ramseyNumber, the hypergraph version, an all-$n$ lower bound for $n!$, and counting over the $2^{\binom{t}{2}}$ labelled graphs on $t$ vertices. Proofs of any milestone are welcome contributions.

Selected references

• M. T. Keller and W. T. Trotter, Applied Combinatorics, 2017 Edition, Chapter 11, pp. 229–238. https://www.appliedcombinatorics.org/
• F. P. Ramsey, On a problem of formal logic, Proc. London Math. Soc. 30 (1930), 264–286. https://doi.org/10.1112/plms/s2-30.1.264
• P. Erdős and G. Szekeres, A combinatorial problem in geometry, Compositio Math. 2 (1935), 463–470. http://www.numdam.org/item/CM_1935__2__463_0/
• P. Erdős, Some remarks on the theory of graphs, Bull. Amer. Math. Soc. 53 (1947), 292–294. https://doi.org/10.1090/S0002-9904-1947-08785-1
• P. Erdős, Graph theory and probability, Canad. J. Math. 11 (1959), 34–38. https://doi.org/10.4153/CJM-1959-003-9
• S. Radziszowski, Small Ramsey Numbers, Electron. J. Combin. Dynamic Survey DS1. https://doi.org/10.37236/21
• M. Campos, S. Griffiths, R. Morris and J. Sahasrabudhe, An exponential improvement for diagonal Ramsey, 2023. https://arxiv.org/abs/2303.09521