Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 19.8899945Formalized record≤ 14.797074Open frontier

6 provers on it3 of 7 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 90Formalized record

2 provers on it2 of 2 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 85Formalized record≤ 5Open frontier

35 provers on it10 of 12 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.37134Formalized record≤ 2.371177Open frontier

16 provers on it7 of 8 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 19.8899945Formalized record≤ 14.797074Open frontier

6 provers on it3 of 7 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 90Formalized record

2 provers on it2 of 2 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 85Formalized record≤ 5Open frontier

35 provers on it10 of 12 missions formalized

Matrix multiplication exponent

≤ 2.37134Formalized record≤ 2.371177Open frontier

16 provers on it7 of 8 missions formalized

All missions

Completed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Convex Optimization: Algorithms and Complexity III: Projected Subgradient Descent with η = R/(L√t) Satisfies f(average) − f(x*) ≤ RL/√tTextbook

Motivation

Many convex optimization problems in machine learning and statistics have objectives that are convex but not differentiable: hinge losses, $\ell_1$ penalties, maxima of finitely many affine functions, and the dual functions of Lagrangian relaxations. Methods that rely on gradients do not apply to them directly, while cutting-plane methods such as the ellipsoid method pay a price that grows with the dimension. The projected subgradient method replaces the gradient by an arbitrary subgradient and restores feasibility by a Euclidean projection. Its guarantee depends on the dimension only through two constants, a radius $R$ and a Lipschitz constant $L$ . This is the reason it, and its descendants (mirror descent, stochastic gradient descent, online gradient descent), are the standard tools for large-scale nonsmooth problems.

The rate analysed here goes back to the subgradient methods of Shor and Polyak in the 1960s and 1970s and to the lower bounds of Nemirovski and Yudin (1983). The book follows the presentation of Nesterov, Introductory Lectures on Convex Optimization (2004). The strongly convex variant with weights proportional to $s$ is from Lacoste-Julien, Schmidt and Bach (2012).

This mission is the third of a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015), and covers the preamble of Chapter 3, Section 3.1 and Section 3.4.1.

Setting

Let $\mathbb R^n$ carry the Euclidean inner product $x^\top y$ and norm $\|\cdot\|$ . Let $\mathcal X\subseteq\mathbb R^n$ be compact and convex, and let $f$ be a convex function on $\mathcal X$ with a minimizer $x^*\in\mathcal X$ .

A vector $g$ is a subgradient of $f$ at $x\in\mathcal X$ if $f(x)-f(y)\le g^\top(x-y)$ for every $y\in\mathcal X$ . The set of subgradients at $x$ is written $\partial f(x)$ . The projection $\Pi_{\mathcal X}(y)$ of a point $y\in\mathbb R^n$ is the point of $\mathcal X$ nearest to $y$ .

Fix step sizes $\eta_s>0$ . Projected subgradient descent starts at some $x_1\in\mathcal X$ and iterates, for $s\ge1$ ,

y_{s+1}=x_s-\eta_s g_s,\quad g_s\in\partial f(x_s),\qquad x_{s+1}=\Pi_{\mathcal X}(y_{s+1}).

Any subgradient may be chosen at each step. In Section 3.1 the step is constant, $\eta_s=\eta$ . The set $\mathcal X$ lies in the Euclidean ball of radius $R$ centred at $x_1$ , and the subgradients have norm at most $L$ .

A function $f$ is $\alpha$ -strongly convex on $\mathcal X$ if $f(x)-f(y)\le g^\top(x-y)-\frac{\alpha}{2}\|x-y\|^2$ for all $x,y\in\mathcal X$ and $g\in\partial f(x)$ .

Formalization targets

Goal: Theorem 3.2

For every horizon $t\ge1$ , projected subgradient descent with the constant step $\eta=R/(L\sqrt t)$ satisfies

f\Big(\frac1t\sum_{s=1}^{t}x_s\Big)-f(x^*)\le\frac{RL}{\sqrt t}.

Milestones

Lemma 3.1. For $x\in\mathcal X$ and $y\in\mathbb R^n$ : $(\Pi_{\mathcal X}(y)-x)^\top(\Pi_{\mathcal X}(y)-y)\le0$ , already on the platform as a published theorem. The mission also states its consequence

\|\Pi_{\mathcal X}(y)-x\|^2+\|y-\Pi_{\mathcal X}(y)\|^2\le\|y-x\|^2 .

The per-step inequality in the proof of Theorem 3.2:

f(x_s)-f(x^*)\le\frac1{2\eta}\big(\|x_s-x^*\|^2-\|y_{s+1}-x^*\|^2\big)+\frac\eta2\|g_s\|^2 .

The summed inequality for any constant step $\eta>0$ :

\sum_{s=1}^{t}\big(f(x_s)-f(x^*)\big)\le\frac{R^2}{2\eta}+\frac{\eta L^2t}{2}.

Companion: Theorem 3.9

If $f$ is $\alpha$ -strongly convex and its subgradients are bounded by $L$ , then with $\eta_s=2/(\alpha(s+1))$ ,

f\Big(\sum_{s=1}^{t}\frac{2s}{t(t+1)}x_s\Big)-f(x^*)\le\frac{2L^2}{\alpha(t+1)}.

Significance

Theorem 3.2 gives an oracle complexity of $O(R^2L^2/\varepsilon^2)$ for reaching an $\varepsilon$ -optimal point, independent of the ambient dimension. Section 3.5 of the book shows this rate is unimprovable for black-box first-order methods once the dimension is large. Theorem 3.9 shows how strong convexity improves the rate to $O(1/t)$ , with the averaging weights changed from uniform to linear. These two bounds are the reference points against which the rest of Chapter 3 and Chapters 4 to 6 (smooth, accelerated, mirror, stochastic methods) are measured.

The results are classical and their proofs are short. Formalizing them produces a reusable, machine-checked account of the basic projected first-order step: the projection inequality, the one-step distance recursion, and the telescoping argument with Jensen's inequality for averaged iterates. To our knowledge, no machine-checked proof of the averaged-iterate bound for the projected subgradient method exists in Mathlib. Related platform items cover other algorithms or other averaging schemes.

Difficulty

The arithmetic is elementary, and the obvious argument works. The care is in the bookkeeping. The projection must be shown not to increase the distance to $x^*$ , which needs convexity of $\mathcal X$ and the variational characterization of the nearest point. The sum must telescope with a horizon-dependent constant step. Jensen's inequality must be applied to a finite convex combination of points of $\mathcal X$ , which requires showing that the average lies in $\mathcal X$ . In Theorem 3.9 the step sizes and the averaging weights are coupled, so neither can be changed independently. In Lean, the iterates are indexed from $1$ with natural-number horizons, and the bounds involve $\sqrt t$ , so these casts need care.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The iterates are sequences ℕ → EuclideanSpace ℝ (Fin n) with the first iterate at index $1$ . The projection is the published relation OnlineConvexOpt.FirstOrder.IsMetricProjection ( $x_{s+1}\in\mathcal X$ is a nearest point to $y_{s+1}$ ). Subgradients are taken relative to $\mathcal X$ (Definition 1.2). A run is a predicate on the steps $s=1,\dots,t$ , and every theorem holds for all runs, that is, for every choice of subgradients. Compactness and convexity of $\mathcal X$ , convexity of $f$ on $\mathcal X$ and the existence of the minimizer $x^*$ are the book's standing assumptions and appear as hypotheses. $R>0$ , $L>0$ and $\alpha>0$ are explicit, because Lean's division by zero would otherwise turn the step size into a junk value.

The book assumes $\|g\|\le L$ for every subgradient at every point of $\mathcal X$ . With subgradients relative to a compact $\mathcal X$ , that assumption can never hold at a boundary point, since every outward normal can be added to a subgradient. Stated that way the theorems would be vacuous. The mission therefore assumes the bound only for the subgradients $g_1,\dots,g_t$ that the run uses. This is a weaker hypothesis and gives a stronger, non-vacuous statement. Bounding only these subgradients is a deliberate choice, not a trivialization: the bound still constrains every quantity the conclusion depends on.

Contributions welcome: proofs of the four inequalities and of the two rates, and a reusable lemma that the convex combination of finitely many points of a convex set lies in the set, together with Jensen's inequality in the form used here.

Selected references

S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. https://arxiv.org/abs/1405.4980
Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.
S. Lacoste-Julien, M. Schmidt and F. Bach, A simpler approach to obtaining an O(1/t) convergence rate for the projected stochastic subgradient method, 2012. https://arxiv.org/abs/1212.2002
N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer, 1985. https://doi.org/10.1007/978-3-642-82118-9

7 thms4 active usersReviewed

Combinatorics Discrete Geometry Linear Optimization·Captain: mikedeng1

A Counterexample to the Hirsch Conjecture I: A 43-Dimensional Polytope with 86 Facets Whose Diameter Exceeds 43Research Paper

Motivation

The Hirsch conjecture, stated by Warren M. Hirsch in a 1957 letter to George Dantzig, asserts that the combinatorial diameter of a $d$ -dimensional polytope with $n$ facets is at most $n-d$ . The diameter is the largest number of edge steps needed to walk between two vertices of the polytope. The question matters to linear optimization: every edge-following pivot rule of the simplex method, starting at a vertex of the feasible region, needs at least as many pivots as the graph distance to an optimal vertex. A polynomial bound on polytope diameters is a necessary condition for a strongly polynomial simplex method, which is still unknown.

Timeline of the conjecture before the counterexample:

1967, Klee and Walkup: the conjecture fails for unbounded polyhedra, and for bounded polytopes it is equivalent to the $d$ -step conjecture (the case $n=2d$ ). They also proved it for $n-d\le 5$ .
1992, Kalai and Kleitman: a quasi-polynomial upper bound $n^{\log_2 d+2}$ on the diameter.
2010, Santos: a counterexample in dimension 43 with 86 facets (arXiv:1006.2814, published in Ann. of Math. 176 (2012) 383–412). It is the subject of this mission.
2012, Matschke, Santos and Weibel: smaller 5-dimensional spindles, giving counterexamples in dimension 20 (arXiv:1202.4701).

The polynomial Hirsch conjecture, which asks only for a bound polynomial in $n$ and $d$ , remains open.

Setting

A polytope in $\mathbb R^d$ is written as $\mathrm{Hpoly}(a,b)=\{x:\langle a_i,x\rangle\le b_i,\ i=1,\dots,n\}$ . A facet presentation is one in which $\mathrm{Hpoly}(a,b)$ has nonempty interior and no inequality is redundant. For a bounded polytope it then has dimension $d$ , and its $n$ inequalities correspond one to one to its facets. A step between two vertices crosses an edge (a one-dimensional face). The polytope is non-Hirsch when its diameter exceeds $n-d$ .

A spindle (Santos, Definition 1.4) is a polytope with two distinguished vertices $u,v$ such that every facet contains exactly one of them. Its length is the graph distance from $u$ to $v$ . The polar objects are prismatoids: polytopes with two parallel facets $Q^+,Q^-$ containing all vertices, whose width is the dual-graph distance between $Q^+$ and $Q^-$ .

Santos's explicit object is the 5-prismatoid $Q$ whose vertices are the 48 rows of Table 1 of the paper: $1^+,\dots,24^+$ with $x_5=1$ and $1^-,\dots,24^-$ with $x_5=-1$ . Its polar $Q^\Delta=\{x\in\mathbb R^5:\langle r,x\rangle\le1\ \text{for each row } r\}$ is a spindle with apices $e_5$ and $-e_5$ . Table 2 of the paper lists the 322 facets of $Q$ , which are the 322 vertices of $Q^\Delta$ : $\pm e_5$ and the points $\frac1{c_0}(\pm c_1,\pm c_2,\pm c_3,\pm c_4,c_5)$ of twenty types $B,B',\dots,K,K'$ with sixteen sign patterns each. The symmetry group $\Sigma$ of $Q$ has order 64; its index-two subgroup $\Sigma^+$ preserves $Q^+$ and $Q^-$ .

Formalization targets

Goal: Corollary 1.7

\exists\, a:\mathrm{Fin}\,86\to\mathbb R^{43},\ b\in\mathbb R^{86}:\quad \mathrm{Hpoly}(a,b)\ \text{nonempty, bounded, a facet presentation, and}\ \operatorname{diam}\mathrm{Hpoly}(a,b)>43.

The goal fixes the dimension (43) and the number of facets (86), as the paper does. It does not assert the exact diameter (44, remarked on p. 24).

Milestones

§3, first bullet (polar form): $Q^\Delta$ is a bounded 48-facet spindle with apices $\pm e_5$ , the rows tight at $e_5$ being $1^+,\dots,24^+$ .
Theorem 4.1(1) (polar form): the 322 points of Table 2 are distinct vertices of $Q^\Delta$ ; the letter classes are $\Sigma^+$ -orbits and the six $\Sigma$ -orbits are A ∪ L, B ∪ K, C ∪ J, D ∪ I, E ∪ H, F ∪ G.
Theorem 4.1(2) (polar form): $Q^\Delta$ has no other vertices.
Theorem 3.1 (polar form): the distance from $e_5$ to $-e_5$ in the graph of $Q^\Delta$ is exactly 6.
Theorem 1.6: a 5-spindle with 48 facets, 322 vertices and length exactly six exists.
Inductive step of Theorem 2.6 (polar form): a $d$ -spindle with $n>2d$ facets and length at least $l$ yields a $(d+1)$ -spindle with $n+1$ facets and length at least $l+1$ .
Theorem 1.5 (strong $d$ -step theorem): a $d$ -spindle with $n$ facets and length at least $l$ yields an $(n-d)$ -spindle with $2n-2d$ facets and length at least $l+n-2d$ , non-Hirsch when $l>d$ .

Significance

Corollary 1.7 settles the Hirsch conjecture in the negative. Theorem 1.5 is the reusable part: it turns any spindle whose length exceeds its dimension into a counterexample. That made the later search for small spindles (Matschke–Santos–Weibel) a finite, low-dimensional problem. Theorem 1.6 is the concrete certificate. Its claims about Tables 1 and 2 are finite statements about explicit rational data.

The result is proved, and several pieces are already formalized on Prove2Me. Hirsch.santos_counterexample (Proved) states that some polytope violates the bound $n-d$ , with no dimension or facet count. Hirsch.strong_dstep_spindle (Proved) is the "in particular" clause of Theorem 1.5, counting inequalities rather than facets. Lemmas 2.2 and 2.4 of the paper are Proved in polar form (Hirsch.spindle_inward_row_push_graph, Hirsch.spindle_wedge_vertex_graph_projection), as is the bound $n\ge2d$ for spindles (Hirsch.spindle_n_ge_two_d). This mission adds the dimension-43, 86-facet statement with facets counted exactly, the general length bound $l+n-2d$ with the spindle structure preserved, and a machine-checkable account of Santos's specific spindle.

Difficulty

The obvious first idea for the 5-dimensional milestones is brute computation. This is feasible in principle but heavy in Lean. Showing that 322 given points are extreme requires exhibiting, for each, five linearly independent tight rows among 48. Showing that no other vertex exists requires a complete enumeration argument rather than a membership check. Exact distance 6 requires the full adjacency structure between the 322 vertices, not only a path.

For the general theorems, the difficulty is that the construction is a one-point suspension followed by a perturbation. Edges and facets of the new polytope must be controlled, with the face lattice changing only in a prescribed way. Diameter is not monotone under arbitrary perturbations, and in particular a walk can become shorter. Keeping the facet count exact (not merely the inequality count) adds an irredundancy argument at each step.

Formalization scope

Polytopes are H-presentations Hirsch.Hpoly a b with a : Fin n → EuclideanSpace ℝ (Fin d), from the platform definition Hirsch_model. "A $d$ -polytope with $n$ facets" is boundedness plus IsFacetPresentation: nonempty interior and every row irredundant. Without this predicate, padding with redundant rows would change the bound $n-d$ , and the statement would collapse to the platform's dimension-free Hirsch.santos_counterexample. Diameter and length use the platform's padded walks (Hirsch.DiamLE, Hirsch.Reach). "Length at least $L$ " means no walk of fewer than $L$ steps, and "length exactly $L$ " adds a walk of $L$ steps. The junk-valued Hirsch.gdist is never used.

All prismatoid statements of the paper (§3, Theorems 2.6, 3.1, 4.1) are stated for the polar spindle, which the paper licenses (pp. 6, 8, 9). Vertices of $Q$ become rows, facets of $Q$ become vertices, the width becomes the apex distance, and $Q^\pm$ become $\pm e_5$ . Natural-number expressions $n-d$ , $2n-2d$ , $l+(n-2d)$ are faithful because spindles have $n\ge2d$ . Theorem 1.5's "length $l$ " is read as "length at least $l$ ", which is equivalent by monotonicity. Tables 1 and 2 are written entry by entry in Lean in the page's order.

Useful contributions include proofs of the finite Table 1/Table 2 facts by certified computation, reusable lemmas on one-point suspensions and on facet presentations under perturbation, and a proof of Corollary 1.7 from milestones 5 and 7.

Selected references

F. Santos, A counterexample to the Hirsch conjecture, Ann. of Math. 176 (2012) 383–412; cited version arXiv:1006.2814v3. https://arxiv.org/abs/1006.2814 , https://doi.org/10.4007/annals.2012.176.1.7
V. Klee and D. W. Walkup, The d-step conjecture for polyhedra of dimension d < 6, Acta Math. 117 (1967) 53–78. https://doi.org/10.1007/BF02395040
G. Kalai and D. J. Kleitman, A quasi-polynomial bound for the diameter of graphs of polyhedra, Bull. Amer. Math. Soc. 26 (1992) 315–316. https://arxiv.org/abs/math/9204233
B. Matschke, F. Santos and C. Weibel, The width of five-dimensional prismatoids, Proc. London Math. Soc. 110 (2015) 647–672. https://arxiv.org/abs/1202.4701

15 thms4 active usersReviewed

Control Theory Dynamic Programming Operations Research+1·Captain: mikedeng1

Stochastic Optimal Control: The Discrete-Time Case III: Monotone Increase Models — Accumulation Points of DP-Optimal Controls Give an Optimal Stationary PolicyTextbook

Motivation

Infinite-horizon dynamic programming with positive (nonnegative) costs and no discounting, or with discount factors that do not make the Bellman operator a contraction, is the setting of Blackwell's and Strauch's positive and negative programming models and of many deterministic control and reachability problems. In this regime the classical contraction argument is unavailable: the optimal cost may be infinite at some states, value iteration may fail to converge to it, and an optimal policy may fail to exist. Chapter 5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), treats these problems in an abstract framework, a single monotone mapping $H$ , so that one set of theorems covers stochastic control with additive or multiplicative costs and minimax control. The chapter is the book version of Bertsekas, "Monotone mappings with application in dynamic programming", SIAM J. Control Optim. 15 (1977).

The chapter's last structural result answers a practical question: when value iteration is run from the terminal cost, do the minimizing controls it computes at each stage lead to an optimal stationary policy?

Setting

The abstract monotone model consists of a state space $S$ , a control space $C$ , nonempty constraint sets $U(x)\subseteq C$ , a terminal function $J_0 : S\to(-\infty,\infty]$ , and a mapping $H(x,u,J)\in[-\infty,\infty]$ defined for $x\in S$ , $u\in C$ and $J : S\to[-\infty,\infty]$ , which is monotone: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$ .

A selector is a function $\mu : S\to C$ with $\mu(x)\in U(x)$ ; a policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ of selectors, and it is stationary if all $\mu_k$ are equal. The operators are

T_\mu(J)(x)=H(x,\mu(x),J),\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J),

the cost of a policy is $J_\pi(x)=\lim_{N\to\infty}(T_{\mu_0}T_{\mu_1}\cdots T_{\mu_{N-1}})(J_0)(x)$ , $J_\mu$ is the cost of the stationary policy $(\mu,\mu,\dots)$ , and the optimal cost is $J^*(x)=\inf_\pi J_\pi(x)$ . A policy is optimal if $J_\pi=J^*$ .

Assumption I (uniform increase) is $J_0(x)\le H(x,u,J_0)$ for all $x$ , $u\in U(x)$ ; under it the sequence defining $J_\pi$ is nondecreasing, so the limit exists in $[-\infty,\infty]$ . Assumption I.1 says $H(x,u,\cdot)$ commutes with limits of nondecreasing sequences above $J_0$ , and I.2 says that for some $\alpha>0$ , $H(x,u,J)\le H(x,u,J+r)\le H(x,u,J)+\alpha r$ for all $r>0$ and $J\ge J_0$ . Assumptions D, D.1, D.2 are the mirror images (uniform decrease, continuity along nonincreasing sequences below $J_0$ , and a lower shift bound).

The DP algorithm (value iteration) generates $T(J_0), T^2(J_0),\dots$ ; for $k\ge0$ and $\lambda\in\mathbb R$ the level sets

U_k(x,\lambda)=\{u\in U(x)\mid H[x,u,T^k(J_0)]\le\lambda\}

collect the controls that keep the stage- $k$ cost below $\lambda$ .

Formalization targets

Goal: Proposition 5.11

Let I, I.1 and I.2 hold, let $C$ be a Hausdorff space, and let $U_k(x,\lambda)$ be compact for all $x\in S$ , $\lambda\in\mathbb R$ and $k\ge\bar k$ . Then (a) some policy $\pi^*=(\mu_0^*,\mu_1^*,\dots)$ satisfies

(T_{\mu_k^*}T^k)(J_0)=T^{k+1}(J_0)\qquad\forall k\ge\bar k;

(b) for every such policy, $\{\mu_k^*(x)\}$ has an accumulation point whenever $J^*(x)<\infty$ ; and (c) any $\mu^*$ that picks such an accumulation point at those states, and any admissible control where $J^*(x)=\infty$ , defines an optimal stationary policy:

J_{\mu^*}=J^*.

Milestones

In the order of the mission's milestone list: Lemma 3.1 (compact sublevel sets give a minimum), Proposition 5.2 (Bellman's equation $J^*=T(J^*)$ under I, I.1, I.2), Proposition 5.4 (a stationary policy is optimal iff $T_{\mu^*}(J^*)=T(J^*)$ ), Proposition 5.10 (under the compactness hypothesis, $J_\infty=T(J_\infty)=T(J^*)=J^*$ and a stationary optimal policy exists), Proposition 5.6 ( $\varepsilon$ -optimal policies from approximate attainment, with explicit constants $\sum_k\alpha^k\varepsilon_k=\varepsilon$ and $\varepsilon(1-\alpha)$ ), Corollaries 5.3.1 and 5.7.1 (Bellman's equation and $\varepsilon$ -optimal policies under D, D.2 with finite $S$ and $J^*>-\infty$ ), and Propositions 5.14 and 5.15 (the multiplicative-cost and minimax models satisfy I, I.1, I.2 or D, D.1/D.2 with explicitly named scalars).

Significance

Proposition 5.10 alone gives existence of an optimal stationary policy; Proposition 5.11 identifies one. It says that the minimizers computed by value iteration, which any implementation produces anyway, converge (along subsequences, state by state) to optimal controls. This is the abstract form of the classical results for deterministic and stochastic positive-cost problems with compact control sets, and through Propositions 5.14 and 5.15 it applies to multiplicative (risk-sensitive) costs and to minimax control without new arguments.

Lemma 3.1, Propositions 5.1–5.5, 5.7–5.10, Lemmas 5.1–5.2 and Corollaries 5.2.1, 5.3.2 are already formalized and proved on the platform, in the MonotoneDP.Increase and MonotoneDP.Decrease developments built from the 1977 paper; this mission reuses their model and assumption definitions and links Lemma 3.1, Proposition 5.2 and Proposition 5.10 as milestones. Propositions 5.4 (in the book's stronger form, with policies optimal state by state), 5.6, 5.11, 5.14, 5.15 and Corollaries 5.3.1, 5.7.1 are new here. All are proved in the book; none has a machine-checked proof yet.

Difficulty

The obvious route to (c) is to pass to the limit in $H[x,\mu_k^*(x),T^k(J_0)]=T^{k+1}(J_0)(x)$ . That fails twice. First, $\{\mu_k^*(x)\}$ need not converge, and different subsequences may have different limits; the statement is about an arbitrary accumulation point, and in a general Hausdorff space accumulation points are not limits of subsequences. Second, $H$ is not assumed continuous in $u$ at all: the only regularity in $u$ is compactness of the level sets $U_k(x,\lambda)$ , and the only regularity in $J$ is I.1 along monotone sequences. States with $J^*(x)=\infty$ need separate treatment, because there the level sets give no control on $\mu_k^*(x)$ .

For Corollaries 5.3.1 and 5.7.1 the difficulty is that D.1 is not assumed; the replacement uses finiteness of $S$ and $J^*>-\infty$ essentially, and both hypotheses are needed.

Formalization scope

Functions $J$ are S → EReal. The model, Assumptions I, I.1, I.2, D, D.1, D.2 and the epigraph sets used by Proposition 5.10 are the published definitions MonotoneDP_Increase_Model, MonotoneDP_Increase_Assumptions, MonotoneDP_Increase_Epigraph, MonotoneDP_Decrease_Model and MonotoneDP_Decrease_Assumptions. In them $J_\pi$ is the limit (limUnder) of the policy compositions, which exists under I or D; $T^k$ is the iterate T^[k]; the composition $(T_{\mu_0}\cdots T_{\mu_{N-1}})(J)$ applies $T_{\mu_{N-1}}$ first; the model requires $S$ nonempty and $J_0>-\infty$ ; "I.2 holds" is the existence of a scalar $\alpha$ , and results that name the scalar take it as a parameter. An accumulation point of a sequence in $C$ is a cluster point (MapClusterPt), not a limit; in Proposition 5.11(c) the conclusion includes that $\mu^*$ is admissible. $J^*+\varepsilon$ is computed pointwise in $[-\infty,\infty]$ and equals $+\infty$ where $J^*$ does.

The book computes in $[-\infty,\infty]$ with $\infty-\infty=\infty$ . Mathlib's EReal gives $\top+\bot=\bot$ , so the two mappings of Section 2.3 use the series' shared definitions, which follow the book's convention: the expected value on a countable $W$ (expect, positive and negative parts summed in $[0,\infty]$ , $+\infty$ when the positive part diverges) and the sum inside the minimax supremum (badd, $+\infty$ when either summand is $+\infty$ ), both from BertsekasShreve.FiniteHorizon.SpecificModels. Propositions 5.14 and 5.15 quantify over every model whose $H$ and $J_0$ are these mappings; such models exist because the mappings are monotone.

A formalization in which $J_\pi$ or $J^*$ is introduced as an arbitrary fixed point of $T$ , or in which (c) assumes that $\mu^*$ is a limit of $\mu_k^*$ , would make the goal trivial or different; both are ruled out by the definitions above.

Contributions welcome: proofs of the milestones, and reusable EReal infrastructure (limits of monotone sequences, series of nonnegative extended reals) that the Part I chapters of the book share.

Selected references

D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; reprinted Athena Scientific, 1996. Chapter 5, pp. 70–90. https://web.mit.edu/dimitrib/www/soc.html
D. P. Bertsekas, "Monotone mappings with application in dynamic programming", SIAM J. Control Optim. 15 (1977) 438–464. https://doi.org/10.1137/0315031
D. Blackwell, "Positive dynamic programming", Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1 (1967) 415–418. https://projecteuclid.org/euclid.bsmsp/1200512999
R. E. Strauch, "Negative dynamic programming", Ann. Math. Statist. 37 (1966) 871–890. https://doi.org/10.1214/aoms/1177699369

16 thms4 active usersReviewed

Machine Learning Optimization Probability+1·Captain: mikedeng1

Variance-based Regularization with Convex Objectives III: Localized-Rademacher Risk Bounds for the Robust MinimizerResearch Paper

Why variance-regularized risk bounds

In statistical learning, one picks a function $f$ from a class $\mathcal F$ to make the population risk $\mathbb E[f]$ small, with access only to an i.i.d. sample $x_1,\dots,x_n$ from an unknown distribution $P$ . Empirical risk minimization replaces $\mathbb E[f]$ by the empirical mean $\mathbb E_{\widehat P_n}[f]$ , and its classical guarantees decay like $1/\sqrt n$ regardless of how concentrated $f$ is. Bernstein-type inequalities show that the deviation of $\mathbb E_{\widehat P_n}[f]$ from $\mathbb E[f]$ scales with the standard deviation of $f$ , so a procedure that minimizes "empirical risk plus a standard-deviation penalty" can, in principle, achieve faster rates when the variance at the optimum is small (Maurer and Pontil, 2009). The penalized objective is non-convex even when every $f$ is convex in its parameters, which makes it hard to optimize.

J. C. Duchi and H. Namkoong (arXiv:1610.02581v3, 2017) replace the penalty by a distributionally robust objective: the worst-case risk over all reweightings of the sample within a $\chi^2$ -divergence ball. This objective is convex whenever the losses are, and (Theorem 1 of the paper) it equals the empirical mean plus a standard-deviation penalty up to an error of order $1/n$ . This mission formalizes the paper's guarantee for the minimizer of that robust objective in terms of localized Rademacher complexities (Section 3.2, Theorem 4), the sharpest of the paper's three generalization analyses. It is the third of four missions on the paper.

Setting

Let $P$ be a probability measure on a measurable space $\mathcal X$ and $x_1,\dots,x_n$ , $n\ge1$ , an i.i.d. sample from $P$ with empirical distribution $\widehat P_n$ . Let $M\ge1$ and let $\mathcal F$ be a collection of measurable functions $f:\mathcal X\to[0,M]$ (losses).

The $\chi^2$ ball of radius $\rho\ge0$ is the set $\mathcal P_n$ of weight vectors $p\in\mathbb R^n$ with $p_i\ge0$ , $\sum_ip_i=1$ and $\frac12\sum_i(np_i-1)^2\le\rho$ ; equivalently, the distributions $P$ on the sample with $D_\phi(P\|\widehat P_n)\le\rho/n$ for $\phi(t)=\frac12(t-1)^2$ .
The robust risk of $f$ is $\sup_{P:\,D_\phi(P\|\widehat P_n)\le\rho/n}\mathbb E_P[f]=\sup_{p\in\mathcal P_n}\sum_ip_if(x_i)$ , and a robust minimizer $\widehat f$ minimizes it over $\mathcal F$ .
The empirical Rademacher complexity is $\mathfrak R_n(\mathcal F)=\mathbb E_\varepsilon\big[\sup_{f\in\mathcal F}\frac1n\sum_i\varepsilon_if(x_i)\big]$ with i.i.d. uniform signs $\varepsilon_i\in\{-1,1\}$ , and $\mathbb E[\mathfrak R_n(\mathcal F)]$ averages it over the sample.
A function $\psi:\mathbb R_+\to\mathbb R_+$ is sub-root if it is nonnegative, nondecreasing, and $r\mapsto\psi(r)/\sqrt r$ is nonincreasing on $r>0$ .
The localization inequality (20) asks that, for all $r\ge0$ ,

\psi_n(r)\ \ge\ \mathbb E\big[\mathfrak R_n(\{cf : f\in\mathcal F,\ c\in[0,1],\ \mathbb E[c^2f^2]\le r\})\big],

with $\psi_n$ sub-root, and $r_n^\star>0$ is a point with $r_n^\star\ge\psi_n(r_n^\star)$ .

Formalization targets

Goal: Theorem 4, inequality (23), as its proof establishes it

Let $0<t<n$ and let $\rho$ satisfy (21): $\frac\rho n\ge8\big(\frac{45M}n\big(t+\log\lceil\log\frac nt\rceil\big)+18r_n^\star\big)$ . With probability at least $1-4e^{-t}$ , every robust minimizer $\widehat f$ satisfies

\mathbb E[\widehat f]\ \le\ \Big(1+2\sqrt{\tfrac{2\rho}n}\Big)\inf_{f\in\mathcal F}\Big(\mathbb E[f]+\sqrt{\tfrac{182\rho}{45n}\mathrm{Var}(f)}\Big)+\Big(14+6\sqrt{\tfrac{2\rho}n}\Big)\frac{M(3\rho+t)}n .

Milestones

In attack order: Bousquet's form of Talagrand's inequality (Lemma B.2); the elementary root bound (Lemma D.4); the contraction principle (Lemma D.5, a published theorem); the uniform Bernstein inequality with Rademacher complexity (Lemma D.1); its localized version in terms of $r_n^\star$ (Lemma D.2); localized second-moment bounds (Lemma D.3); the deterministic expansion (10) of Theorem 1,

\Big(\sqrt{\tfrac{2\rho}n s_n^2}-\tfrac{2M\rho}n\Big)_+\le\sup_{P}\mathbb E_P[Z]-\mathbb E_{\widehat P_n}[Z]\le\sqrt{\tfrac{2\rho}ns_n^2};

and the uniform bound (22): with probability at least $1-2e^{-t}$ , for all $f\in\mathcal F$ ,

\mathbb E[f]\le\Big(1+2\sqrt{\tfrac{2\rho}n}\Big)\sup_{P:\,D_\phi(P\|\widehat P_n)\le\rho/n}\mathbb E_P[f]+\Big(13+4\sqrt{\tfrac{2\rho}n}\Big)\frac{M\rho}n .

Significance

The bound (23) says that the robust minimizer competes with the best trade-off between risk and standard deviation in the class, and that the complexity of the class enters only through the fixed point $r_n^\star$ of a localized complexity bound. For bounded VC classes $r_n^\star$ is of order $\frac{d\log(n/d)}n$ (Bartlett, Bousquet and Mendelson, 2005, Corollary 3.7), so when the optimal function has small variance the excess risk is of order $\rho/n$ , faster than the $1/\sqrt n$ of uniform covering arguments; and localized complexities apply to classes, such as balls of reproducing kernel Hilbert spaces, whose covering numbers are too large for the covering-number analysis of the paper's Theorem 3 (mission II of this series).

The paper's result is proved, not open. No part of it, and none of the localized-complexity machinery of Bartlett, Bousquet and Mendelson, is formalized in Lean or Mathlib to our knowledge. The mission produces a checked version of the theorem with every constant explicit and, along the way, the localization lemmas D.1–D.3, which are reusable for any localized-complexity analysis. Reading the proof also exposed three arithmetic slips in the printed statements; the mission states what the proof establishes (see Formalization scope).

Difficulty

The obvious route applies a uniform concentration inequality to $\mathcal F$ and then a Bernstein bound to each $f$ . Talagrand's inequality applied to the whole class gives a deviation governed by the largest variance in the class and by the global complexity $\mathbb E[\mathfrak R_n(\mathcal F)]$ , which yields only $1/\sqrt n$ rates. Obtaining a deviation that scales with each function's own second moment requires peeling the class into shells of comparable second moment and a fixed-point argument on the sub-root bound, with a union bound whose cost appears as $\log\lceil\log\frac nt\rceil$ . The two directions of the localized inequalities (population to sample, and sample to population for second moments) must then be combined with the deterministic expansion (10) while keeping the constants explicit. A further subtlety is the self-normalized rescaling $f\mapsto\sqrt{r/(\mathbb E[f^2]\vee r)}\,f$ , which differs from the variance normalization of Bartlett et al. and is what makes the bound compatible with the robust objective.

Formalization scope

Lean conventions. The sample is the coordinate map of the product measure $P^n$ on Fin n → X. Distributions on the sample are weight vectors in the $\chi^2$ ball; the robust risk is the real supremum over that ball (attained, since the ball is nonempty and compact for $n\ge1$ , $\rho\ge0$ ). Population means and variances are ∫ x, f x ∂P and ProbabilityTheory.variance f P for measurable bounded $f$ ; empirical means and variances are normalized by $1/n$ . The empirical Rademacher complexity is the published UnderstandingML_Rademacher definition evaluated on $\{(f(x_1),\dots,f(x_n))\}$ . Its expectation is a Bochner integral, and every hypothesis that bounds it also asserts that the integrand is integrable: otherwise the integral is $0$ , (20) would hold for free, and the theorem would be false. Probability bounds are stated for the failure event under $P^n$ (an outer measure when the event is not measurable). The goal speaks about every minimizer of the robust risk, so it is not vacuous when the set of minimizers is empty. The condition $r_n^\star>0$ is part of the page's "root" (and the proof divides by $\sqrt{r_n^\star}$ ); with $r_n^\star=0$ allowed, $\psi(r)=\sqrt r$ would remove the complexity term from (21). The condition $t<n$ makes $\log\lceil\log\frac nt\rceil$ defined.

Corrections of printed statements, each recorded in the item's docstring and Formalization Note (the milestone texts stay verbatim):

(22) is stated with probability $1-2e^{-t}$ ; the paper prints $1-e^{-t}$ , and its proof (p. 41) concludes $1-2e^{-t}$ .
(23) is stated with probability $1-4e^{-t}$ (printed $1-3e^{-t}$ ; the proof adds two fixed- $f$ events to the two of (22)) and with $\frac{182\rho}{45n}$ (printed $\frac{91\rho}{45n}$ ; the proof's step $\sqrt\rho+\sqrt t\le\sqrt{91\rho/45}$ multiplies $\sqrt{2\mathrm{Var}(f)/n}$ ).
Lemma D.3 is stated with the additive term $72M^2(1+\eta)r_n^\star+(4(1+\eta)+\frac{14}3)\frac{M^2t}n$ and, in the reversed direction, the coefficient $1+\frac1{1+\eta}$ , as its proof yields (printed: $\frac{Mt}n(4+\frac73M)$ and $1+\frac\eta{1+\eta}$ ), under Theorem 4's standing hypothesis $M\ge1$ .
Lemma D.5 is linked to the published contraction lemma UnderstandingML.contraction_lemma, which states it at a fixed sample for nonempty bounded classes and allows a different Lipschitz map per coordinate.

Contributions welcome: proofs of the milestones in any order; Lemma B.2 (Bousquet's inequality) is the deepest single ingredient and is reusable well beyond this mission, as are the peeling Lemma D.1 and the sub-root fixed-point Lemma D.2.

Selected references

J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv:1610.02581v3, 2017. https://arxiv.org/abs/1610.02581
P. L. Bartlett, O. Bousquet and S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 2005. https://doi.org/10.1214/009053605000000282
O. Bousquet, A Bennett concentration inequality and its application to suprema of empirical processes, Comptes Rendus Mathématique 334(6), 2002. https://doi.org/10.1016/S1631-073X(02)02292-6
A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT 2009. https://arxiv.org/abs/0907.3740
M. Ledoux and M. Talagrand, Probability in Banach Spaces, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4

14 thms4 active usersReviewed

Number Theory·Captain: xuanji

The irrationality measure of π is at most 14.797074 (Rhin–Viola 1993)Research Paper

Motivation

The irrationality measure $\mu(\pi)$ is the supremum of the $\mu$ for which $|\pi - p/q| < q^{-\mu}$ has infinitely many rational solutions $p/q$ . Every irrational number has $\mu \ge 2$ (Dirichlet), almost every real number has $\mu = 2$ , and it is conjectured that $\mu(\pi) = 2$ . Known upper bounds:

Mahler (1953): $42$ , the first proof that $\pi$ is not a Liouville number.
Mignotte (1974): $20.6$ .
Chudnovsky (1982): $19.8899944\ldots$
Rhin–Viola (1993): $14.797074$ .
Hata (1993): $8.016045\ldots$
Salikhov (2008): $7.606308\ldots$
Zeilberger–Zudilin (2020): $7.103205334137\ldots$ , the current record.

The campaign's first proved value is Mahler's $42$ . This entry records Rhin–Viola's bound.

Formalization target

The campaign template with the value $14.797074$ filled in: PiIrrationality.UpperBound (14.797074 : ℝ), i.e. $\mu(\pi) \le 14.797074$ .

Value. The paper's Theorem states exactly that $7.398537$ is an effective irrationality measure of $\zeta(2)$ , "whence $14.797074$ is an effective irrationality measure of $\pi$ ". The value is used as stated, with no rounding.

How the bound arises

Rhin and Viola prove that $7.398537$ is an effective irrationality measure of $\zeta(2) = \pi^2/6$ , using a birational transformation acting on Beukers' double integrals and semi-infinite linear programming to optimise the arithmetic. A measure $\mu$ for $\pi^2$ gives $2\mu$ for $\pi$ (if $|\pi - p/q|$ is small then $|\pi^2 - p^2/q^2|$ is small with denominator $q^2$ ), hence their $2 \times 7.398537 = 14.797074$ .

Significance

Each step down the list replaces Mahler's approximations with a sharper family. Formalizing $14.797074$ would build reusable explicit machinery: integral constructions of rational approximations to $\pi$ , bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.

Selected references

G. Rhin, C. Viola, On the irrationality measure of $\zeta(2)$ , Ann. Inst. Fourier (Grenoble) 43 (1993), no. 1, 85–109. https://doi.org/10.5802/aif.1322
K. Mahler, On the approximation of $\pi$ , Indag. Math. 15 (1953), 30–42.
F. Beukers, A rational approach to $\pi$ , Nieuw Arch. Wiskd. (5) 1 (2000), 372–379.
Source table: https://teorth.github.io/optimizationproblems/constants/7a.html

13 thms4 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Air Travel Demand and Airline Seat Inventory Management II: The EMSR Protection Level for Two Nested Fare ClassesTextbook

Why airlines protect seats

An airline sells the seats of one flight in several fare classes at different prices, all drawn from one shared cabin. Discount fares are bought early, under advance-purchase restrictions, while most high-fare requests arrive close to departure. Accepting every early low-fare request fills the aircraft with cheap passengers and turns away late high-fare passengers; refusing too many leaves seats empty. Seat inventory control decides how many seats to keep away from the low fare. Peter Belobaba's 1987 MIT thesis (Flight Transportation Laboratory Report R87-7) introduced the expected marginal seat revenue (EMSR) model for this decision, and EMSR-type rules remain the basis of the booking-limit logic in airline revenue management systems.

Timeline. Littlewood (1972, AGIFORS Symposium Proceedings; reprinted 2005) proposed accepting a low-fare request as long as its fare is at least the high fare times the probability of selling all remaining seats to high-fare passengers. Analysts at Trans World Airlines (1973) and Richter at Lufthansa (1982) gave equivalent formulations for the dynamic case. Belobaba (1987, Ch. 5) restated the two-class rule as a static protection level for nested inventories and extended it heuristically to many classes. Brumelle and McGill (Operations Research 41, 1993) and Curry (Transportation Science 24, 1990) later proved optimality of nested protection levels for any number of classes under low-to-high arrivals, and showed that Belobaba's multi-class EMSR levels are not optimal for three or more classes. This mission concerns only the two-class result, which is correct.

Setting

A single flight leg has capacity $C \in \mathbb N$ . Class 1 has fare $f_1$ , class 2 has fare $f_2$ , with $0 \le f_2 \le f_1$ . The numbers of requests for the two classes are random variables $r_1, r_2$ with values in $\mathbb N$ , defined on a probability space $(\Omega, \mu)$ and independent. There are no cancellations, no no-shows, and a refused request is lost.

The inventory is nested: a class-1 request is accepted as long as any seat is unsold. A protection level $S \in \{0, \dots, C\}$ is the number of seats reserved for class 1; it sets the class-2 booking limit $BL_2 = C - S$ . All class-2 requests arrive before any class-1 request. Class 2 therefore books $\min(r_2, C - S)$ seats and class 1 books $\min(r_1, C - \min(r_2, C-S))$ , and the realised revenue is

R_S = f_2 \min(r_2, C - S) + f_1 \min\bigl(r_1,\, C - \min(r_2, C - S)\bigr).

The expected revenue is $\bar R(S) = \mathbb E[R_S]$ .

The tail probability of class 1 is $\bar P_1(S) = P[r_1 \ge S]$ , the probability of receiving $S$ or more class-1 requests, and the expected marginal seat revenue of the $S$ -th class-1 seat is

\mathrm{EMSR}_1(S) = f_1 \cdot \bar P_1(S).

For a single class with $S$ seats the expected revenue is $f_1\,\mathbb E[\min(r_1, S)]$ , and $\mathrm{EMSR}_1(S)$ is its increment from $S-1$ to $S$ seats. The EMSR protection level $S_2^1$ is the largest integer $S \in \{0, \dots, C\}$ with

\mathrm{EMSR}_1(S) \ge f_2 .

In Lean these objects are nestedRevenue, expectedNestedRevenue, tailProb, classRevenue, emsr and emsrProtectionLevel in SeatInventory.Nested.

Formalization targets

Goal: Eqs. (5.15)–(5.16), optimality of the EMSR protection level

\bar R(S) \le \bar R(S_2^1) \qquad \text{for all } S \in \{0, \dots, C\}.

The goal fixes no distribution: it holds for every pair of independent $\mathbb N$ -valued demands, and $S_2^1$ depends only on $f_2/f_1$ and the law of $r_1$ .

Milestones

Eq. (5.11). $f_1\mathbb E[\min(r_1,S)] - f_1\mathbb E[\min(r_1,S-1)] = f_1 P[r_1 \ge S]$ for $S \ge 1$ .
Eqs. (6.1)–(6.2). $\bar P_1$ and, for $f_1 \ge 0$ , $\mathrm{EMSR}_1$ are non-increasing in $S$ .
Eq. (4.8), Littlewood's rule, already on the platform as RevenueManagement.littlewood_marginal_value (Talluri and van Ryzin's Eq. (2.1), proved).
Sect. 5.2, p. 112. $\bar R(S) \le \bar R(S_2^1)$ for $S_2^1 \le S \le C$ : a smaller booking limit for class 2 cannot raise expected revenue.
Sect. 5.2, p. 114. With the same class-2 limit $C - S$ , the expected nested revenue is at least the expected revenue of two distinct inventories with $S$ and $C - S$ seats, strictly if $f_1 > 0$ and $P[r_2 < C - S,\ r_1 > S] > 0$ .

Significance

The two-class result says that, for a static booking limit set once before sales open and low-fare demand arriving first, the airline needs only the high-fare demand distribution and the fare ratio to set the optimal limit; the low-fare forecast is irrelevant. This is the rule that the thesis then applies class by class in multi-class nested systems, and it is the base case against which the later exact multi-class theory (Brumelle–McGill, Curry) is checked. Milestone 5 makes precise why nested inventories dominate the distinct-inventory allocation of the thesis's Sect. 5.1 with the same class-2 limit.

The result is classical and proved, in the sense that the optimality of a two-class threshold policy follows from Littlewood's argument and from the dynamic-programming treatment in Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004, Ch. 2). On Prove2Me, Littlewood's marginal rule and the dynamic-programming optimality of nested protection levels (RevenueManagement.static_optimal_controls) are formalized, but in Bellman form: there the protection level is defined through the value function of a dynamic program. What is not formalized is the statement in Belobaba's form, where the protection level is the explicit threshold of $f_1 P[r_1 \ge S]$ against $f_2$ and the objective is the explicit expected revenue of a booking limit. Connecting the two forms, and the comparison with distinct inventories, is the work of this mission.

Difficulty

The expected revenue couples the two demands through the capacity left by class 2, so $\bar R$ is not a sum of single-class revenues and is not separately concave in an obvious way. The step that requires care is the increment $\bar R(S) - \bar R(S-1)$ : it is not $\mathrm{EMSR}_1(S) - f_2$ , as the thesis's sentence after the milestone on p. 112 suggests, because the extra protected seat matters only on the event that class 2 would have reached its limit. Independence of $r_1$ and $r_2$ is what makes that event's probability factor out; without independence the threshold rule is not optimal. The discrete reading matters too: with $P[r_1 > S]$ in place of $P[r_1 \ge S]$ the rule is off by one seat and the claim fails.

Formalization scope

Conventions the Lean statements commit to:

Demands are $\mathbb N$ -valued measurable random variables r₁ r₂ : Ω → ℕ on a probability space μ; the goal and milestone 4 assume IndepFun r₁ r₂ μ. The thesis writes continuous densities (Eqs. (5.1)–(5.5)) but requires integer seat counts; the discrete model is used throughout.
$\bar P_1(S) = P[r_1 \ge S]$ , as in Eq. (6.2) and the prose of Eq. (5.11), not $P[r_1 > S]$ as in Eq. (5.2).
The EMSR protection level is the largest $S \in \{0,\dots,C\}$ with $f_1 P[r_1 \ge S] \ge f_2$ (Eq. (5.15)); Eq. (5.16)'s equality is the continuous idealisation and is not stated.
Booking order: all class-2 requests precede all class-1 requests (pp. 108, 112). This order is built into the revenue formula, not assumed separately.
Fares satisfy $0 \le f_2 \le f_1$ ; the thesis has $f_1 > f_2$ , and the statements also cover equality.
Expectations are Bochner integrals of bounded revenues, probabilities are μ.real; seat counts use truncated subtraction only where $S \le C$ .

A trivializing formalization is ruled out: $S_2^1$ is defined by the threshold of (5.15), never as an argmax of expected revenue, and the expected revenue is computed from the realised revenue of the booking process, not postulated as a sum of marginal terms.

The multi-class EMSR levels of Eqs. (5.19)–(5.29) and the dynamic revision of Eqs. (5.31)–(5.32) are out of scope. Proofs need the discrete expectation identity $\mathbb E[\min(r,S)] - \mathbb E[\min(r,S-1)] = P[r \ge S]$ and expectation of products of independent bounded functions, both in Mathlib's reach and reusable for other single-leg revenue models. Proofs of any milestone, and a proof of the goal from milestones 1, 2 and 4 plus the matching lower-half argument, are welcome.

Selected references

P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT, Flight Transportation Laboratory Report R87-7, 1987 (no DOI).
K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4, 2005. https://doi.org/10.1057/palgrave.rpm.5170134
S. L. Brumelle and J. I. McGill, Airline seat allocation with multiple nested fare classes, Operations Research 41, 1993. https://doi.org/10.1287/opre.41.1.127
R. E. Curry, Optimal airline seat allocation with fare classes nested by origins and destinations, Transportation Science 24, 1990. https://doi.org/10.1287/trsc.24.3.193
K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000

8 thms4 active usersReviewed

Completed

Mathematical Physics Partial Differential Equations·Captain: Lucas

Tegmark 1997: On the Dimensionality of SpacetimeResearch Paper

Motivation

In a short 1997 letter, Max Tegmark argued that, given the other laws of physics, a spacetime with $n$ space and $m$ time dimensions can host observers who understand and predict their world only when $(n,m)=(3,1)$ (Tegmark 1997). The argument is physical and anthropic, but each step rests on a precise mathematical fact: the classification of second-order linear PDEs into elliptic, hyperbolic and ultrahyperbolic type, the well-posedness (or ill-posedness) of the corresponding initial-value problems, the potential theory of $\mathbb R^n$ , the stability of Kepler orbits, and the algebra of curvature tensors in low dimension. This mission collects those mathematical facts as formal targets.

Timeline of the ingredients cited by the letter:

1917 — Ehrenfest observes that planetary orbits and classical atoms are unstable when $n>3$ .
1936 — Ásgeirsson proves his mean value theorem for the ultrahyperbolic equation.
1962 — Courant and Hilbert (vol. II) give the textbook treatment of PDE type and causal structure.
1963 — Tangherlini shows that the hydrogen atom has no bound states for $n>3$ .
1973/1984 — Misner–Thorne–Wheeler and Deser–Jackiw–'t Hooft emphasize that general relativity has no gravitational force when $n<3$ .

Setting

A second-order linear PDE on $\mathbb R^d$ has the form

\sum_{i,j=1}^d A_{ij}\,\partial_i\partial_j u+\sum_{i=1}^d b_i\,\partial_i u+c\,u=0,

with $A$ symmetric. Following the paper, at a point it is elliptic if all eigenvalues of $A$ are positive or all are negative, hyperbolic if one eigenvalue is positive and the rest negative (or vice versa), and ultrahyperbolic if at least two are positive and at least two negative. Eigenvalues are counted with multiplicity; the Lean development counts them as the positive/negative real roots of the characteristic polynomial (numPosEigenvalues, numNegEigenvalues, IsElliptic, IsHyperbolic, IsUltrahyperbolic).

A spacetime of dimensionality $(n,m)$ carries a metric $g$ with $m$ positive (time-like) and $n$ negative (space-like) eigenvalues, so that $(n,m)=(3,1)$ has signature $(+---)$ . The covariant field equations $u_{;\mu}{}^{\mu}=0$ (wave) and $u_{;\mu}{}^{\mu}+\mu^2u=0$ (Klein–Gordon) have coefficient matrix $A=g^{-1}$ . The Laplacian on $\mathbb R^n$ is $\nabla^2 f=\sum_i\partial_i^2 f$ (laplacian).

Formalization targets

Goal: type of the field equations as a function of $(n,m)$

For a symmetric $g$ with $m$ positive and $n$ negative eigenvalues,

\text{elliptic}\iff n=0\ \text{or}\ m=0,\qquad \text{hyperbolic}\iff n=1\ \text{or}\ m=1,\qquad \text{ultrahyperbolic}\iff n\ge2\ \text{and}\ m\ge2.

Milestones (in the order of the paper)

(p. L70) For $n>2$ , $r^{2-n}$ is harmonic on $\mathbb R^n\setminus\{0\}$ .
(p. L70) For $n>3$ the effective potential $U(r)=\frac{L^2}{2\mu r^2}-k\,r^{2-n}$ has no strict local minimum: no stable orbits.
(p. L70) For $n=3$ and $L\neq0$ it has one: stable circular orbits exist.
(p. L71) For $n>3$ the hydrogen energy functional is unbounded below.
(p. L71) For $n<3$ , Ricci-flat algebraic curvature tensors in dimension $n+1$ vanish.
(p. L73) $g^{-1}$ has the same numbers of positive and negative eigenvalues as $g$ .
(p. L73) The signatures $(+---)$ , $(+++++)$ , $(++--)$ give hyperbolic, elliptic, ultrahyperbolic equations.
(p. L73) The Cauchy problem for the Laplace equation with data on a line is ill-posed.
(p. L73) The Klein–Gordon initial-value problem is well-posed in the cones of dependence (energy estimate).
(p. L73) Ásgeirsson's mean value theorem for $\nabla_x^2u=\nabla_y^2u$ .

Significance

The goal makes precise the paper's central new observation: the hyperbolicity needed for a well-posed initial-value problem singles out exactly one time dimension (or, in the tachyonic mirror case, one space dimension). The milestones supply the mathematical content behind each of the paper's other claims, namely instability for $n>3$ and the absence of gravity for $n<3$ , as well as the well-posedness and ill-posedness facts behind the "predictability" argument. All of these are classical results; none of them is new mathematics. The value of the mission is a machine-checked record of exactly which mathematical statements the argument uses, under which hypotheses, and with which caveats (for instance the critical coupling in four dimensions).

Difficulty

The goal is linear algebra. The difficulty lies in the milestones: Ásgeirsson's theorem and the Klein–Gordon energy estimate need integration over spheres and balls, a divergence theorem or spherical-mean calculus, and differentiation under the integral sign, and Mathlib supports these only partially. The four-dimensional hydrogen case sits exactly at the Hardy-inequality threshold, where the outcome depends on the coupling constant.

Formalization scope

Matrices are real and indexed by Fin d; eigenvalue counts are root counts of the characteristic polynomial with multiplicity. Classification is pointwise: one constant coefficient matrix.
Functions on $\mathbb R^n$ live on EuclideanSpace ℝ (Fin n); derivatives are Fréchet derivatives, and the Laplacian is the sum of pure second derivatives along the standard basis.
"Stable orbit" means a strict local minimum of the radial effective potential at some radius $r_0>0$ .
"No bound states" means that the energy $\int|\nabla\psi|^2-\kappa\int|x|^{2-n}\psi^2$ is unbounded below on smooth, compactly supported, $L^2$ -normalized real $\psi$ (units $\hbar^2/2m=1$ ). For $n=4$ the claim is only asserted for $\kappa>1$ , the Hardy threshold.
"No gravity" is formalized pointwise: a tensor with the Riemann symmetries and zero Ricci contraction vanishes.
Ill-posedness of the elliptic Cauchy problem is formalized by one explicit instance (the Laplace equation in the plane with data on $y=0$ ). Well-posedness of the hyperbolic one is formalized by the local energy inequality for $C^2$ Klein–Gordon solutions.

Reusable infrastructure: PDE type via eigenvalue signs, spherical means, and local energy estimates for wave-type equations.

Selected references

M. Tegmark, On the dimensionality of spacetime, Class. Quantum Grav. 14 (1997) L69–L75. https://doi.org/10.1088/0264-9381/14/4/002
R. Courant and D. Hilbert, Methods of Mathematical Physics, vol. II, Interscience, 1962.
L. Ásgeirsson, Über eine Mittelwertseigenschaft von Lösungen homogener linearer partieller Differentialgleichungen 2. Ordnung mit konstanten Koeffizienten, Math. Ann. 113 (1936) 321–346.
F. R. Tangherlini, Schwarzschild field in n dimensions and the dimensionality of space problem, Nuovo Cimento 27 (1963) 636–651.
P. Ehrenfest, Proc. Amsterdam Acad. 20 (1917) 200.

19 thms4 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Linear Programming: Foundations and Extensions I: Degeneracy and Termination of the Simplex Method under Bland's RuleTextbook

Motivation

The simplex method is the standard algorithm for linear programming, and its correctness rests on one question: does it stop? Each pivot of the method moves from one dictionary to another without decreasing the objective value, but a pivot can leave the objective unchanged. When that happens repeatedly, the method can return to a dictionary it has already visited and loop forever. This behaviour, cycling, is not hypothetical: Vanderbei's Chapter 3 exhibits a problem with four decision variables and three constraints on which the "largest coefficient" entering rule with a natural tie-breaking rule cycles through six dictionaries (Vanderbei 2014, pp. 26–27).

The chapter answers the question with two pivoting rules under which the simplex method provably terminates, and then draws the consequence that makes linear programming a finite theory: the fundamental theorem of linear programming. This mission formalizes the chapter's four numbered theorems in Vanderbei's own setting of standard-form problems with slack variables.

Timeline. Hoffman (1953) and Beale (1955) gave the first examples of cycling. The perturbation and lexicographic methods go back to Charnes (1952) and to Dantzig, Orden and Wolfe (1955). Bland (1977) introduced the smallest-index rule and proved that the simplex method terminates under it (Bland 1977).

Setting

A linear program in standard form has $m$ constraints and $n$ decision variables:

\text{maximize } \sum_{j=1}^n c_j x_j \quad\text{subject to}\quad \sum_{j=1}^n a_{ij}x_j \le b_i\ (i=1,\dots,m),\qquad x_j \ge 0\ (j=1,\dots,n).

A solution $x$ is feasible if it satisfies every constraint, and optimal if in addition it maximizes the objective among feasible solutions. The problem is infeasible if no feasible solution exists, and unbounded if it has feasible solutions with arbitrarily large objective values.

The slack variables $w_i = b_i - \sum_j a_{ij}x_j$ are appended to the list of variables as $x_{n+i} = w_i$ , so that the constraints become the linear system $[A\ I]\,x = b$ with $x \ge 0$ in $\mathbb{R}^{n+m}$ . A dictionary is given by a set $\mathcal B$ of $m$ basic indices whose columns of $[A\ I]$ are linearly independent; the remaining indices $\mathcal N$ are nonbasic. Solving for the basic variables gives

\zeta = \bar\zeta + \sum_{j\in\mathcal N}\bar c_j x_j,\qquad x_i = \bar b_i - \sum_{j\in\mathcal N}\bar a_{ij}x_j\quad (i\in\mathcal B).

The basic solution of the dictionary sets the nonbasic variables to zero. The dictionary is feasible if $\bar b_i \ge 0$ for every $i\in\mathcal B$ , and degenerate if $\bar b_i = 0$ for some $i\in\mathcal B$ .

The simplex method (Phase II) starts at a feasible dictionary and repeats a pivot: an entering variable $x_k$ is chosen among the nonbasic variables with $\bar c_k > 0$ , and a leaving variable $x_l$ among the basic variables with $\bar a_{lk} > 0$ that minimize the ratio $\bar b_l/\bar a_{lk}$ ; then $x_k$ becomes basic and $x_l$ nonbasic. The method stops when no $\bar c_j$ is positive (the dictionary is optimal) or when the entering column has no positive $\bar a_{ik}$ (the problem is unbounded). A pivoting rule resolves the remaining choices. Bland's rule chooses both the entering and the leaving variable as the candidate with the smallest index. The lexicographic rule perturbs the right-hand sides by symbols $0<\epsilon_m\ll\dots\ll\epsilon_1\ll$ all data and chooses the leaving variable by the perturbed ratio test.

Formalization targets

Goal: Theorem 3.3 (termination under Bland's rule, p. 31)

From every feasible dictionary $D_0$ , there is no infinite sequence of pivots

D_0\to D_1\to D_2\to\cdots

in which both the entering and the leaving variable follow Bland's rule; and a finite sequence of such pivots reaches a dictionary $D_T$ at which the method stops, optimal or exhibiting unboundedness.

Milestones

Theorem 3.1 (p. 27): if the simplex method fails to terminate, it must cycle, i.e. an infinite run visits some dictionary twice.
Theorem 3.2 (p. 30): the simplex method always terminates when the leaving variable is selected by the lexicographic rule.
Theorem 3.4 (p. 33), the fundamental theorem: (1) with no optimal solution the problem is infeasible or unbounded; (2) if a feasible solution exists, a basic feasible solution exists; (3) if an optimal solution exists, a basic optimal solution exists.

Significance

The result. Termination under Bland's rule is what turns the simplex method from a heuristic into an algorithm. Combined with Phase I, it yields the fundamental theorem of linear programming, which reduces the search for an optimum to finitely many basic solutions and underlies the duality theory of the following chapters. Bland's rule also needs no perturbation or extra bookkeeping, and it is the anticycling rule used in many correctness proofs of simplex-type and combinatorial pivoting algorithms, including oriented-matroid programming.

Formalizing it. All four theorems are classical and proved. The Prove2Me library has the lexicographic rule and a nondegenerate termination theorem in the tableau setting of Bertsimas and Tsitsiklis (equality form $Ax=b$ , $x\ge 0$ , full row rank), and the existence of basic feasible and optimal solutions in that form. It has no statement of Bland's theorem, and none of Vanderbei's dictionary formulation over $[A\ I]$ . This mission produces a machine-checkable model of dictionaries and pivoting rules in that formulation, and targets Bland's theorem, whose proof is a genuine combinatorial argument rather than a monotonicity argument.

Difficulty

The natural argument for termination is monotonicity: each pivot increases the objective, so no dictionary repeats. It fails exactly at degenerate pivots, where the step length $\bar b_l/\bar a_{lk}$ is zero and the objective and the basic solution do not change. Bland's rule gives no potential function that strictly increases along degenerate pivots, so the proof has to reason about a hypothetical cycle as a whole: which variables enter and leave the basis within it, and how two dictionaries of the cycle, in which the same variable leaves and later enters, constrain each other's coefficients. Relating the coefficients of two different dictionaries of the same problem is the step that has no counterpart in the model's definitions and has to be developed.

For Theorem 3.2, the symbols $\epsilon_i$ cannot be replaced by a fixed small real number: the method treats them as formal quantities on separate scales, and the statement is about that symbolic rule.

Formalization scope

Vectors are Fin n → ℝ, Fin m → ℝ, and the constraint matrix is Matrix (Fin m) (Fin n) ℝ. The $n+m$ variables are indexed by Fin (n + m) with the decision variables first and the slacks after them, which is the order $x_1,\dots,x_n,x_{n+1}=w_1,\dots,x_{n+m}=w_m$ that Bland's rule compares. A dictionary is a structure holding its basic set, a proof that it has $m$ elements and a proof that its columns of $[A\ I]$ are linearly independent; the coefficients $\bar b,\bar a,\bar c,\bar\zeta$ are computed as coordinates in the basis of basic columns. A dictionary is therefore determined by its basic set, as the proof of Theorem 3.1 uses. "Basic solution" is defined through such a dictionary, not as a support condition.

Termination is stated as the nonexistence of an infinite run from a feasible dictionary, for Theorems 3.2 and 3.3. The goal adds that a finite Bland run reaches a stopping dictionary, so that it cannot hold because pivots fail to exist. The lexicographic rule is encoded by lexicographic comparison of the coefficient vectors $(\bar b_i, r_{i1},\dots,r_{im})/\bar a_{ik}$ of the perturbed ratios; the symbol $\epsilon_p$ is attached in the starting dictionary to its $p$ -th basic variable in increasing index order, which for the initial dictionary is the $p$ -th constraint. Unboundedness in Theorem 3.4 is "for every $M$ a feasible solution with objective $>M$ ", as defined on p. 7. The statements carry no explicit constants.

A formalization that stated Theorem 3.3 for arbitrary pivot sequences with pairwise distinct bases would be Theorem 3.1's counting argument, not Bland's theorem; the goal is stated for pivots that follow Bland's rule and only those.

A complete development needs: the pivot update of a dictionary and the invariance of the solution set under it, feasibility preservation by the ratio test, the relation between the objective rows of two dictionaries, and finiteness of the set of bases. These are reusable for any later formalization of simplex-type algorithms. Proofs of the milestones, alternative proofs of Theorem 3.3, and Phase I (to connect Theorem 3.4 with the algorithm) are welcome.

Selected references

R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 3. https://doi.org/10.1007/978-1-4614-7630-6
R. G. Bland, New finite pivoting rules for the simplex method, Mathematics of Operations Research 2(2):103–107, 1977. https://doi.org/10.1287/moor.2.2.103
G. B. Dantzig, A. Orden, P. Wolfe, The generalized simplex method for minimizing a linear form under linear inequality restraints, Pacific Journal of Mathematics 5(2):183–195, 1955. https://doi.org/10.2140/pjm.1955.5.183
E. M. L. Beale, Cycling in the dual simplex algorithm, Naval Research Logistics Quarterly 2(4):269–275, 1955. https://doi.org/10.1002/nav.3800020406
D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §3.4 (lexicographic rule and Bland's rule in tableau form).

10 thms4 active usersReviewed

Completed

Analysis Convex Optimization Optimization·Captain: mikedeng1

Minimization Methods for Non-Differentiable Functions I: The Subdifferential of a Nonnegative Combination of Convex FunctionsTextbook

Motivation

Many optimization problems in operations research have objectives that are convex but not differentiable: the maximum of finitely many linear or smooth functions, the value function of a Lagrangian dual, the cost of a two-stage linear program as a function of the first-stage decision. Gradient methods do not apply to these directly. N. Z. Shor's Minimization Methods for Non-Differentiable Functions (Springer Series in Computational Mathematics 3, 1985; translated by K. C. Kiwiel and A. Ruszczyński from the 1979 Russian edition) develops the algorithms that replace the gradient by a subgradient, and its first chapter sets up the calculus of subgradients these algorithms rely on.

This mission is the first of a series formalizing the book. It covers §1.2 (convex functions and the concept of subgradient) and §1.3 (rules for computing subgradients), printed pages 7–16. Every later mission in the series (the subgradient method, space dilation, the ellipsoid method, decomposition) assumes that a subgradient of the objective can be computed, and §1.3 is where the book explains how: by combining subgradients of simpler pieces.

Setting

Write $E_n$ for $n$ -dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$ . A function $f$ with domain a convex set $M \subseteq E_n$ is convex if its epigraph $\{(u, x) : u \ge f(x),\ x \in M\}$ is convex, equivalently $(1-\alpha) f(x_1) + \alpha f(x_2) \ge f((1-\alpha)x_1 + \alpha x_2)$ for $x_1, x_2 \in M$ and $\alpha \in [0,1]$ .

Let $x_0$ be an interior point of $M$ . A vector $g$ is a subgradient (or generalized gradient) of $f$ at $x_0$ if

f(x) - f(x_0) \ge (g, x - x_0) \qquad \text{for all } x \in M. \tag{1.3}

The set of all subgradients is the subdifferential, written $G(x_0)$ or $G_f(x_0)$ . For $f$ differentiable at $x_0$ it is the single gradient; for $f(x) = |x|$ on $E_1$ it is $[-1, 1]$ at $x_0 = 0$ .

The one-sided directional derivative of $f$ at $x_0$ in direction $\eta$ is

f'_\eta(x_0) = \lim_{t \to 0+} \frac{f(x_0 + t\eta) - f(x_0)}{t}.

A direction $\eta \ne 0$ is a direction of steepest descent at $x_0$ if $\min_{\|\xi\| = 1} f'_\xi(x_0) = f'_\eta(x_0)/\|\eta\|$ .

Formalization targets

Goal: Theorem 1.12 (p. 13), the subdifferential of a nonnegative combination

For convex $f_1, \dots, f_k$ on $E_n$ and $a_1, \dots, a_k \ge 0$ , the function $f = \sum_{i=1}^k a_i f_i$ is convex and, at every $x_0$ ,

G_f(x_0) = \Big\{ \sum_{i=1}^k a_i g_i \;:\; g_i \in G_{f_i}(x_0),\ i = 1, \dots, k \Big\}.

Both inclusions are part of the goal.

Milestones

Theorem 1.7 (p. 9): at an interior point $x_0$ of the domain, $G(x_0)$ is nonempty, bounded, convex and closed.
Theorem 1.8 (p. 9): at an interior point, $f'_\eta(x_0)$ exists for every $\eta$ and $f'_\eta(x_0) = \max_{g \in G(x_0)} (g, \eta)$ , with the maximum attained.
Corollary (p. 12): an interior point $x_0$ minimizes $f$ on $M$ if and only if $0 \in G(x_0)$ .
Theorem 1.11 (p. 12): if $0 \notin G(x_0)$ and $g_0$ is the element of $G(x_0)$ nearest the origin, then $-g_0$ is a direction of steepest descent.
Theorem 1.9 (p. 11): $f$ is convex on $E_n$ if and only if $f'_\eta(x)$ exists everywhere and $t \mapsto f'_\eta(x + t\eta)$ is nondecreasing for all $x, \eta$ .
Theorem 1.10 (p. 11): a twice continuously differentiable $f$ is convex if and only if its Hessian is positive semidefinite everywhere.
Theorem 1.13 (p. 14): for convex $f_1, \dots, f_m$ , the function $\varphi = \max_i f_i$ is convex and $G_{f_i}(x_0) \subseteq G_\varphi(x_0)$ for every index $i$ active at $x_0$ .

Significance

The result. Theorem 1.12 is the finite-dimensional, finite-valued case of the Moreau–Rockafellar sum rule. With Theorem 1.13 it is the book's recipe for computing subgradients of functions assembled from simple pieces by nonnegative combinations and pointwise maxima, the two operations that produce most nonsmooth convex objectives in practice (Lagrangian duals, penalty functions, piecewise-linear costs). Theorem 1.8 identifies the directional derivative with the support function of the subdifferential; the Corollary and Theorem 1.11 give the optimality condition and the steepest-descent direction that every descent method for nonsmooth convex functions starts from.

Formalizing it. These results are classical and have been proved many times in textbooks (Rockafellar, Convex Analysis, 1970, §23). Mathlib at the pinned revision has convexity, separation theorems and Carathéodory's theorem, but no subdifferential of a convex function on $E_n$ and no max formula. The mission builds that layer: a subdifferential with the book's inequality (1.3), a one-sided directional derivative defined as a right-hand limit, and the calculus rules above. The platform has a Clarke-gradient analogue of Theorem 1.8 for locally Lipschitz functions and a Banach-space sum rule for $f + \tfrac12\|\cdot\|^2$ ; neither states the convex, finite-dimensional results here.

Difficulty

The inclusion " $\supseteq$ " in Theorem 1.12 is immediate from (1.3). The inclusion " $\subseteq$ " is the content: a subgradient of the sum is a global object, and nothing in (1.3) splits it into subgradients of the pieces. Adding the inequalities of the pieces only produces vectors of the right form; it does not show every subgradient of $f$ arises this way. Any argument has to use the finite dimension and the interior-point setting, which is where Theorems 1.7 and 1.8 (existence of subgradients, compactness of $G(x_0)$ , existence of one-sided derivatives) come in.

Theorem 1.8 in turn needs the existence of a finite right-hand limit of the difference quotient, which requires both monotonicity of the quotient and a lower bound, and the existence of a subgradient attaining the maximum, which is a separation statement. Theorem 1.9's "if" direction must rebuild convexity from one-sided derivative information alone, with no differentiability assumption.

Formalization scope

$E_n$ is EuclideanSpace ℝ (Fin n) and $(x, y)$ is inner ℝ x y. A function is f : EuclideanSpace ℝ (Fin n) → ℝ; the domain $M$ is a set, convexity on it is ConvexOn ℝ M f (which includes convexity of $M$ ), and interior points are x₀ ∈ interior M. Theorems 1.9, 1.10, 1.12 and 1.13 are stated on all of $E_n$ (Set.univ), as the book proves them.
The subdifferential subdifferential M f x₀ is the set of $g$ with $f(x) - f(x_0) \ge (g, x - x_0)$ for all $x \in M$ . It is defined for any $x_0$ ; the interior-point assumption is a hypothesis of each theorem that needs it.
HasOneSidedDirDeriv f x₀ η d is the right-hand limit Tendsto … (𝓝[>] 0) (𝓝 d), not Mathlib's two-sided lineDeriv. Maxima and minima are stated with IsGreatest/IsLeast (attained), never with sSup/sInf.
Theorem 1.12 is an equality of sets over indices Fin k; $k = 0$ and zero coefficients are allowed, as in the book. Theorem 1.13's maximum is Finset.sup' over Fin m with $m \ge 1$ , and it asserts only the inclusion the book states.
Theorem 1.11 is stated as the book's proof establishes it: the steepest-descent direction is minus the minimal-norm subgradient. The printed statement names the minimal-norm subgradient itself, along which the directional derivative is positive.
A formalization that states only " $\supseteq$ " in Theorem 1.12, or only that each $\sum a_i g_i$ is a subgradient, is the easy half and does not count as the goal.
Theorems 1.1–1.6 (supporting hyperplane, separation, representation by extremal points, the convexity inequality, continuity on the interior) are Mathlib-level (geometric_hahn_banach_*, Carathéodory and Krein–Milman, ConvexOn.continuousOn_interior) and are not restated.

Contributions welcome: proofs of any milestone, a reusable lemma that the difference quotient of a convex function is monotone in $t$ , and a general max formula; these are reusable in the later missions of the series, which define subgradients the same way.

Selected references

N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, §§1.2–1.3, pp. 7–16. https://doi.org/10.1007/978-3-642-82118-9
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §23 (subgradients) and Theorem 23.8 (sum rule). https://doi.org/10.1515/9781400873173
J.-J. Moreau, "Fonctionnelles sous-différentiables", Comptes Rendus de l'Académie des Sciences 257 (1963), 4117–4119.

10 thms4 active usersReviewed

Completed

Dynamic Programming Operations Research Probability+1·Captain: mikedeng1

Stochastic Dynamic Programming and the Control of Queueing Systems III: Approximating Sequences for the Discounted Cost CriterionTextbook

Motivation

Optimal control of queueing systems leads to Markov decision problems whose state space is countably infinite (buffer contents, numbers of customers) and whose costs are unbounded (holding costs grow with the queue). Such a problem cannot be solved on a computer as it stands. The standard remedy is to truncate: solve a finite problem on the states $\{0,1,\dots,N\}$ and hope that its value and its optimal policy approximate those of the original problem as $N$ grows. Linn Sennott's approximating sequence method (ASM) makes this hope precise. For the expected discounted cost criterion, Sections 4.6–4.7 of Sennott's book (Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999) identify a single condition, Assumption DC( $\alpha$ ), that is necessary and sufficient for convergence of the truncated values, and give checkable sufficient conditions for it.

The method matters because naive truncation can fail. The book's Example 4.6.1 has a chain whose value at state $0$ is finite, yet a natural truncation produces values $V^N_\alpha(0)\ge \alpha N^2/((1-\alpha)[N(1-\alpha)+\alpha])\to\infty$ . How the probability that would leave the truncated set is redistributed decides whether the computation is meaningful.

Earlier truncation schemes (Fox 1971; White 1980, 1982; Hernández-Lerma 1986; Cavazos-Cadena 1986; Whitt 1978–79; see the bibliographic notes on p. 81 of the book and Puterman 1994) require bounded rewards or pass directly to an algorithm. The ASM instead produces a sequence of finite Markov decision chains that can be studied in their own right; the material of Sections 4.6–4.7 is presented in the book as new.

Setting

A Markov decision chain (MDC) $\Delta$ has a countable state space $S$ ; for each state $i$ a finite nonempty action set $A_i$ ; nonnegative finite costs $C(i,a)$ ; and transition probabilities $P_{ij}(a)$ with $\sum_j P_{ij}(a)=1$ . A policy $\theta$ chooses the action at time $t$ at random from a distribution $\theta(\cdot\mid h_t)$ on $A_{i_t}$ that may depend on the entire history $h_t=(i_0,a_0,\dots,i_{t-1},a_{t-1},i_t)$ . A stationary policy $f$ always chooses $f(i)\in A_i$ in state $i$ . Fix a discount factor $\alpha\in(0,1)$ . The discounted cost of $\theta$ and the discounted value function are

V_{\theta,\alpha}(i)=\sum_{t\ge0}\alpha^tE_\theta[C(X_t,A_t)\mid X_0=i],\qquad V_\alpha(i)=\inf_\theta V_{\theta,\alpha}(i),

both in $[0,\infty]$ , the infimum over all policies. A policy is discount optimal if $V_{\theta,\alpha}=V_\alpha$ .

An approximating sequence $(\Delta_N)_{N\ge N_0}$ consists of finite nonempty sets $S_N$ increasing to $S$ and, for $i\in S_N$ and $a\in A_i$ , probability distributions $P_{ij}(a;N)$ on $S_N$ with $P_{ij}(a;N)\to P_{ij}(a)$ as $N\to\infty$ . The finite MDC $\Delta_N$ has state space $S_N$ and the same actions and costs; $V^N_\alpha$ is its value function and $f^N_\alpha$ a stationary policy attaining the minimum in its discount optimality equation

V^N_\alpha(i)=\min_{a\in A_i}\Big\{C(i,a)+\alpha\sum_{j\in S_N}P_{ij}(a;N)V^N_\alpha(j)\Big\},\qquad i\in S_N.

An augmentation type approximating sequence (ATAS) keeps the original probabilities inside $S_N$ and redistributes the excess probability $P_{ir}(a)$ , $r\notin S_N$ , according to augmentation distributions $q_j(i,a,r,N)$ on $S_N$ : $P_{ij}(a;N)=P_{ij}(a)+\sum_{r\notin S_N}P_{ir}(a)q_j(i,a,r,N)$ .

Assumption DC( $\alpha$ ): for every $i\in S$ , $W_\alpha(i):=\limsup_{N}V^N_\alpha(i)<\infty$ and $W_\alpha(i)\le V_\alpha(i)$ .

Formalization targets

Goal: Theorem 4.6.3

The following are equivalent:

\text{(i)}\ \lim_{N\to\infty}V^N_\alpha(i)=V_\alpha(i)<\infty\ \ (i\in S);\qquad \text{(ii)}\ \text{Assumption DC}(\alpha).

Under either, every limit point of $(f^N_\alpha)_{N\ge N_0}$ (a stationary $f$ with $f^{N_r}(i)=f(i)$ eventually along a subsequence, for each $i$ ) is discount optimal for $\Delta$ .

Milestones

Lemma 4.6.2: $\liminf_N V^N_\alpha\ge V_\alpha$ for every approximating sequence.
Proposition 4.7.1: bounded costs imply DC( $\alpha$ ).
Lemma 4.7.2: taboo probabilities of avoiding $S-S_N$ converge to the $t$ -step transition probabilities.
Lemma 4.7.3: for the first passage time $T_i(N)$ out of $S_N$ under a stationary policy, $E[\alpha^{T_i(N)}]\to0$ .
Proposition 4.7.4: if $V_\alpha<\infty$ and the ATAS sends excess probability to a finite set, DC( $\alpha$ ) holds.
Corollary 4.7.5: the case of a single distinguished state $z$ , with the relative form of the optimality equation for $\Delta_N$ .
Proposition 4.7.6: if $V_\alpha<\infty$ and the augmentation distributions satisfy $\sum_{j\in S_N}q_j(i,a,r,N)v_{\alpha,n}(j)\le v_{\alpha,n}(r)$ for all $n\ge0$ , then $V^N_\alpha\le V_\alpha$ on $S_N$ .

Significance

Theorem 4.6.3 turns the question "does truncation work?" into the verification of one inequality between a lim sup and the true value, and it delivers both the value and an optimal stationary policy from finite computations. Propositions 4.7.4–4.7.6 give conditions that hold in the queueing models of the book with unbounded holding costs, and Corollary 4.7.5 supplies the computational form used for the inventory model of Chapter 5. The discounted theory is also the stepping stone to the average cost ASM of Chapter 8, which is built on discounted approximations.

All results are proved in the book. None of them is formalized: the platform has no statement about approximating sequences or state truncation of countable-state MDPs, and Mathlib has no Markov decision processes. The mission produces machine-checked versions of the convergence theorem and its sufficient conditions, for general history-dependent randomized policies and $[0,\infty]$ -valued costs.

Difficulty

The value functions are infima over uncountably many history-dependent policies and may be infinite, so no contraction argument applies: costs are unbounded and $V_\alpha$ is only the minimal nonnegative solution of its optimality equation. Passing to the limit in $N$ inside $\sum_{j\in S_N}P_{ij}(a;N)V^N_\alpha(j)$ is an interchange of limit and infinite sum under a moving probability measure, with no dominating function in general; Example 4.6.1 shows that the interchange genuinely fails. The upper bound of Proposition 4.7.4 requires comparing $\Delta_N$ with $\Delta$ along a coupled first passage out of $S_N$ , which needs the taboo-probability estimates of Lemmas 4.7.2–4.7.3. The obvious idea of bounding $V^N_\alpha$ by $\sup C/(1-\alpha)$ works only for bounded costs (Proposition 4.7.1).

Formalization scope

The state type S is countable ([Countable S]); actions live in a type Act, with a finite nonempty Finset of admissible actions per state. Costs are ℝ≥0, transition probabilities and all value functions are ℝ≥0∞, so infima over policies are lattice infima and $+\infty$ is a legitimate value. A general policy is a function of the history, encoded as the list of past state–action pairs (most recent first) and the current state; the expected cost at time $t$ is the $[0,\infty]$ -valued sum over histories. $V_\alpha$ is the infimum over all such policies; a stationary policy enters as the policy putting mass one on $f(i)$ . The discount factor is α : ℝ≥0 with $0<\alpha<1$ (the chapter's standing assumption). $\Delta_N$ is an MDC on the subtype $S_N$ ; $V^N_\alpha(i)$ is extended by $0$ when $N<N_0$ or $i\notin S_N$ , a convention that affects finitely many $N$ for each fixed $i$ and hence no limit in $N$ . Limits, lim sups and lim infs are along Filter.atTop in ℝ≥0∞. Taboo probabilities and the first passage quantity $E[\alpha^{T}]=\sum_{n\ge1}\alpha^nP(T=n)$ (so $\alpha^\infty=0$ ) are defined combinatorially from the transition probabilities.

A trivializing formalization is ruled out: $V_\alpha$ is not an infimum over stationary policies only (which would make optimality of limit points close to definitional), DC( $\alpha$ ) keeps both of its conditions, and statement (i) of the goal includes finiteness of $V_\alpha$ .

A complete development needs the minimality of $V_\alpha$ among nonnegative solutions of the discount optimality equation (Theorem 4.1.4, chunk II of this series), Fatou-type lemmas for sums against converging distributions (Appendix A, chunk XI), and compactness of stationary policies (Proposition B.5). Contributions of these as reusable lemmas about countable-state MDCs are welcome.

Selected references

L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley, 1999, Sections 4.6–4.7, pp. 73–81. https://doi.org/10.1002/9780470317037
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

11 thms4 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Operations Research·Captain: mikedeng1

Theory of Games and Economic Behavior IX: Solutions for Acyclic RelationsTextbook

Motivation

The solution concept of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944) is defined from two ingredients: a set of imputations and a domination relation between them. A solution is a set of imputations that is internally stable (no member dominates another) and externally stable (every non-member is dominated by some member). In §65 of the book the authors observe that this definition never uses what imputations and domination actually are. They abstract it to an arbitrary set $D$ and an arbitrary relation $\mathcal S$ on $D$ , and ask which properties of $\mathcal S$ guarantee that exactly one solution exists.

The abstract notion is what graph theory now calls a kernel of a directed graph: draw an arc $x \to y$ whenever $x\mathcal S y$ ; a solution is a set of vertices that is independent and absorbs every vertex outside it. Kernels appear in combinatorial game theory (the losing positions of a finite impartial game form a kernel of its move graph) and in the theory of preference and choice.

Timeline.

1944 (1st ed.; 3rd ed. 1953, reprinted 2007): von Neumann and Morgenstern define solutions for an arbitrary relation (§65), show that a finite set with an acyclic relation has exactly one solution (65:X), and that acyclicity is necessary for every subset to have a unique solution (65:Z).
1953: M. Richardson, Solutions of irreflexive relations, extends existence (not uniqueness) to finite relations without cycles of odd length.

Setting

Let $D$ be an arbitrary set and $\mathcal S$ an arbitrary relation on $D$ ; $x\mathcal S y$ is read " $x$ dominates $y$ ". A solution (in $D$ for $\mathcal S$ ) is a set $V \subseteq D$ with

\text{(65:1)}\qquad V = \{\, y \in D : x\mathcal S y \text{ holds for no } x \in V \,\}.

For $E \subseteq D$ , an element $x$ is a maximum of $E$ if $x \in E$ and no $y \in E$ has $y\mathcal S x$ ; the set of maxima is $E^m$ .

For $m \ge 1$ , condition $(A_m)$ says: never $x_1\mathcal S x_0, x_2\mathcal S x_1, \dots, x_m\mathcal S x_{m-1}$ with $x_0 = x_m$ and all $x_i \in D$ . The relation is acyclic if it satisfies every $(A_m)$ , $m = 1, 2, \dots$ ; in particular never $x\mathcal S x$ . It is strictly acyclic if there is no infinite sequence $x_0, x_1, x_2, \dots$ in $D$ with $x_{i+1}\mathcal S x_i$ for every $i$ . Property (65:K) says that every non-empty $E \subseteq D$ has $E^m \ne \ominus$ . A partial ordering (65:B) is a transitive relation for which at most one of $x = y$ , $x\mathcal S y$ , $y\mathcal S x$ holds.

For the main theorem the book constructs a candidate solution by induction (65.7.1): $A_1 = D$ ; $B_i = A_i^m$ ; $C_i$ is the set of elements of $A_i$ dominated by some element of $B_i$ ; $A_{i+1} = A_i - B_i - C_i$ . With $i_0$ the first index for which $A_{i_0} = \ominus$ ,

\text{(65:2)}\qquad V_0 = B_1 \cup \cdots \cup B_{i_0 - 1}.

In Lean the elements live in a type α, D V : Set α, and S : α → α → Prop with S x y meaning $x\mathcal S y$ ; the predicates are IsSolution D S V, maxima E S, IsAcyclic, IsStrictlyAcyclic, HasMaximaProperty, IsPartialOrdering, ConditionG, and the construction stageA, stageB, stageC, V0.

Formalization targets

Goal: (65:X)

If $D$ is finite and $\mathcal S$ is acyclic on $D$ , then

\exists!\, V:\ V \text{ is a solution in } D \text{ for } \mathcal S, \qquad\text{and}\qquad V \text{ is a solution} \iff V = V_0 .

Milestones, in attack order

(65:I) For a partial ordering, a finite $D$ satisfies (65:G): every non-maximal $y$ is dominated by some maximum.
(65:H) For a partial ordering of an arbitrary $D$ : $V$ is a solution $\iff$ (65:G) holds and $V = D^m$ .
(65:O:c) Strict acyclicity implies acyclicity; for finite $D$ the two are equivalent.
(65:P) (65:K) $\iff$ strict acyclicity, for arbitrary $D$ .
(65:S) For finite $D$ and acyclic $\mathcal S$ , some $A_i$ is empty.
(65:V) For finite $D$ and acyclic $\mathcal S$ , every solution equals $V_0$ .
(65:W) For finite $D$ and acyclic $\mathcal S$ , $V_0$ is a solution.
(65:Z) If every $E \subseteq D$ has a unique solution in $E$ for $\mathcal S$ , then $\mathcal S$ is acyclic on $D$ .

Significance

The result itself. (65:X) is the most general of the book's three existence-and-uniqueness theorems for solutions (complete ordering, partial ordering, acyclic relation; 65.8.1). For games proper it has no direct application: the set of imputations of an essential game has no maxima, so (65:K) fails (65.9.1). Its role is to isolate a sufficient condition for a unique solution. With (65:Z), and applied to every subset of $D$ , it characterizes the finite relations for which every subset has exactly one solution: exactly the acyclic ones (65.8.2). In graph language it is the statement that a finite directed acyclic graph has exactly one kernel. In combinatorial game theory this is the partition of the positions of a finite impartial game into P- and N-positions. The complete- and partial-ordering results (65:E)–(65:I) are the special cases the book treats first.

Formalizing it. The results are classical and fully proved in the book; to the best of our knowledge none of them is on the Prove2Me platform, and Mathlib has well-foundedness (WellFounded, RelEmbedding of ℕ) but no kernel or von Neumann–Morgenstern solution notion for an abstract relation. The mission produces machine-checked proofs of the book's §65 chain: the equivalence of (65:K) with strict acyclicity for arbitrary sets, the finite equivalence of acyclicity and strict acyclicity, the explicit construction of $V_0$ , and the characterization of 65.8.2.

Difficulty

Most of the individual steps are short. The work is in making the book's finite induction precise. The sets $A_i$ are defined recursively and $V_0$ refers to the first empty stage $i_0$ . The uniqueness proof (65:V) is a minimal-counterexample argument over the stage index, which moves between "smallest $k$ with $y \notin A_k$ " and the disjoint decomposition (65:U) of $D$ into the $B_i$ and $C_i$ . A tempting shortcut, taking an arbitrary well-founded rank function instead of the book's construction, proves existence and uniqueness but not that the solution is the $V_0$ of (65:2), which is part of the goal. For (65:P) and (65:O:c) the difficulty is the passage between finite cycles and infinite chains. Going from a chain in a finite set to a repetition needs a pigeonhole argument, and going from a set without maxima to a chain needs dependent choice.

Formalization scope

Representation. An ambient type α; D, E, V are Set α; the relation is S : α → α → Prop and is only ever consulted on elements of the set under consideration, so it is the book's relation on $D$ (or its restriction to $E$ ). Finite and infinite sequences are functions ℕ → α.
Solutions. IsSolution D S V is the set equation (65:1) literally; it forces $V \subseteq D$ . Uniqueness in the goal is ∃! over all V : Set α, not over a subtype; there is no degenerate reading in which the solution is fixed by construction.
Acyclicity. IsAcyclic D S requires $(A_m)$ for every $m \ge 1$ , all cycle elements in $D$ . The case $m = 0$ is excluded, as in the book (it would be unsatisfiable). This is equivalent to the absence of a Relation.TransGen loop inside $D$ , but the book's form is stated.
Construction. Stages are indexed from $0$ : stageA D S k is the book's $A_{k+1}$ . V0 D S is the union of all $B_i$ , which equals $B_1 \cup \cdots \cup B_{i_0 - 1}$ because every later $B_i$ is empty.
Standing hypotheses instantiated. (65:S), (65:V), (65:W) and the goal (65:X) carry the hypotheses of 65.7.1, " $D$ finite and $\mathcal S$ acyclic" (for finite $D$ equivalently strictly acyclic, i.e. (65:K)), as D.Finite and IsAcyclic D S. (65:H) and (65:I) carry the partial-ordering hypothesis (65:B:a), (65:B:b) of 65.5.1, and (65:I) also finiteness of $D$ . (65:O:c), (65:P) and (65:Z) are for arbitrary $D$ and $\mathcal S$ , as 65.6.2 and 65.8.2 state. The empty $D$ is allowed everywhere; there the unique solution is $\ominus$ .
Not stated. The infinite case of (65:X) and of (65:Y), which the book leaves open (65.7.1, 65.8.3, question (65:9)); the complete-ordering results (65:E), (65:F), which silently assume $D \neq \ominus$ ; the counting statement (65:8).
Needed infrastructure. Finite-set induction and pigeonhole on Set.Finite, dependent choice for (65:P). The definitions are reusable for any later work on kernels of digraphs and on abstract stable sets. Proofs of any milestone, and alternative proofs of the goal, are welcome.

Selected references

J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd ed., 1953), §65, pp. 587–602. https://doi.org/10.1515/9781400829460
M. Richardson, Solutions of irreflexive relations, Annals of Mathematics 58 (1953), 573–590. https://doi.org/10.2307/1969755

13 thms4 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Theory of Games and Economic Behavior VIII: Characteristic Functions of General n-Person GamesTextbook

Motivation

The theory of Theory of Games and Economic Behavior (von Neumann and Morgenstern, 1944; 3rd ed. 1953) rests on one object: the characteristic function $v(S)$ , the amount a coalition $S$ of players can secure for itself whatever the other players do. For zero-sum $n$ -person games, Chapter VI defines $v(S)$ and proves (25.3.1 and 26.1.1) that the set functions arising this way are exactly those with $v(\emptyset)=0$ , $v(-S)=-v(S)$ and superadditivity. Economic applications, however, are rarely zero-sum: exchange and production create value. Chapter XI extends the theory to general (non-zero-sum) games by adding a fictitious player who absorbs the total gain, and §57 answers the question that decides the scope of this extension: which set functions are characteristic functions of general games?

The answer, that these are exactly the superadditive set functions vanishing on the empty set, is the reason why the cooperative game theory that followed could take "a superadditive $v$ with $v(\emptyset)=0$ " as its primitive object, usually without any underlying strategic game.

Setting

A general $n$ -person game $\Gamma$ in normalized form has players $I=\{1,\dots,n\}$ . Player $k$ chooses $\tau_k\in\{1,\dots,\beta_k\}$ with $\beta_k\ge 1$ , without knowing the choices of the others, and receives the real amount $\mathcal H_k(\tau_1,\dots,\tau_n)$ . No condition is imposed on $\sum_k\mathcal H_k$ . The game is zero-sum if $\sum_{k=1}^n\mathcal H_k\equiv 0$ .

The zero-sum extension $\overline\Gamma$ (56.2.2) adds a fictitious player $n+1$ , who has no move and receives

\mathcal H_{n+1}(\tau_1,\dots,\tau_n)=-\sum_{k=1}^n\mathcal H_k(\tau_1,\dots,\tau_n).

Write $\overline I=\{1,\dots,n,n+1\}$ . For $S\subseteq\overline I$ , the coalition $S$ and its complement $\bot S=\overline I-S$ play a zero-sum two-person game. The pure strategies of $S$ are the tuples of choices of its real members. A mixed strategy $\xi$ of $S$ is a single probability distribution over these tuples, so the members of a coalition randomize jointly, and likewise $\eta$ for $\bot S$ . The payoff to $S$ is $\sum_{k\in S}\mathcal H_k$ . Then

v(S)=\max_\xi\min_\eta K(\xi,\eta),

where $K$ is the expected payoff to $S$ . The function $v$ on all $S\subseteq\overline I$ is the extended characteristic function; its restriction to $S\subseteq I$ is the restricted characteristic function (57.1). For a zero-sum game the restricted function is the characteristic function of Chapter VI.

Formalization targets

Goal: 57.3.4

For every $n$ and every set function $v$ on the subsets of $I$ ,

v \text{ is the restricted characteristic function of some general game} \iff v(\emptyset)=0 \text{ and } v(S\cup T)\ge v(S)+v(T) \text{ for } S\cap T=\emptyset,

and for every set function $v$ on the subsets of $\overline I$ ,

v \text{ is the extended characteristic function of some general game} \iff v(\emptyset)=0,\ v(\bot S)=-v(S),\ v \text{ superadditive}.

In each direction a single game realizes $v$ on every set simultaneously; $v(I)$ is not constrained.

Milestones

(57:1:a)–(57:1:c): necessity of the extended conditions.
(57:2:a), (57:2:c), (57:2:b): necessity of the restricted conditions, including $v(-S)\le v(I)-v(S)$ .
57.3.1: sufficiency of (57:2:a), (57:2:c).
57.3.3: sufficiency of (57:1:a)–(57:1:c).
(57:G): for such $v$ , $v(-S)=-v(S)$ for all $S$ holds iff $v(S)+v(-S)=v(I)$ for all $S$ and $v(I)=0$ .
(57:B): in a zero-sum game every one-element set of players is removable, meaning that some zero-sum game with the same characteristic function has payoffs that do not depend on that player's choice.
(57:C): the set of all players is removable iff the game is inessential, i.e. $v(S)=\sum_{k\in S}\alpha_k$ .

Significance

The characterization fixes the domain of Chapter XI: every statement about solutions of general games is, by 57.3.4, a statement about superadditive set functions with $v(\emptyset)=0$ , and conversely every such function is attained by a strategic game. That converse justifies studying cooperative games abstractly. (57:G) separates the zero-sum and constant-sum subclasses inside this domain. (57:B) and (57:C) quantify how much of a player's strategic role survives when his moves are removed, which is the book's justification for the fictitious player.

Status: all results are proved in the book (1944). To our knowledge none of them is machine-checked; the Prove2Me catalog has superadditive and convex cooperative games, but none tied to a strategic game, and no characteristic function built from a minimax value. The work here is formalizing the known proofs.

Difficulty

Necessity reduces to the zero-sum theory applied to $\overline\Gamma$ , but still requires the minimax theorem for the coalition's two-person game and a careful treatment of joint mixing when two disjoint coalitions merge. Sufficiency requires building one finite game whose coalition values equal an arbitrary superadditive $v$ exactly, for all $2^n$ coalitions at once. The obvious attempt, choosing payoffs coalition by coalition, fails because the payoffs are shared: a construction that gives $S$ the right value can change the value of every set that overlaps $S$ . The difficulty is to obtain the upper bound $v(S)\le v_0(S)$ for every $S$ simultaneously. For the extended function there is a further difficulty. The fictitious player has no move, so the values on sets containing $n+1$ are forced by the others, and they must be reconciled with (57:1:b).

For (57:B), the target game must reproduce an arbitrary zero-sum characteristic function while one prescribed player's choice has no effect on any payoff.

Formalization scope

Players are Fin n (book indices $1,\dots,n$ become $0,\dots,n-1$ ); sets of players are Finset (Fin n). The extended domain $\overline I$ is Fin (n + 1) with the fictitious player Fin.last n, and $\bot S$ is the complement in Fin (n + 1). A game (GeneralGame n) has $\beta_k\ge1$ strategies Fin (β k) per player and real payoffs; zero-sum is the predicate IsZeroSum. The fictitious player's single strategy is left out of the coalition's strategy tuples, which does not change the two-person game. Max and Min are ⨆/⨅ over Mathlib's stdSimplex on the coalition's strategy tuples (one joint distribution per coalition). Both simplices are nonempty and the payoff is bounded, so these are attained values and no junk value from an empty or unbounded supremum occurs.

Standing hypotheses and their instantiation:

finite strategy sets with $\beta_k\ge1$ (11.2.3, 56.2.2): a field of GeneralGame;
"always assuming (57:2:a), (57:2:c)" for (57:G) (p. 537): an explicit hypothesis;
"zero-sum $n$ -person game" in (57:A)–(57:C) (p. 533): the hypothesis Γ.IsZeroSum and the requirement that the replacement game $\Gamma'$ is zero-sum;
"no influence upon the course of the game" (57:A): all payoffs are independent of that player's variable, as in the proof of (57:C) on p. 534;
"inessential" (57:C): the additive form (57:13), which p. 534 calls "precisely the definition of inessentiality".

No normalization is imposed: $v(I)$ is arbitrary and nothing is reduced. Every statement is made for all $n\ge0$ ; the book's $n\ge1$ is not needed, so this is a strengthening.

A trivializing formalization is ruled out: the characteristic function is defined from the game through the coalition's minimax value, so it is never a free parameter, and the existence claims must produce one game for all coalitions at once.

Needed infrastructure: finite zero-sum two-person games with joint mixed strategies over dependent product types; the minimax theorem ((17:6), on the platform as AGT.zero_sum_minimax for matrices); and product decompositions of coalition strategy tuples. The coalition-value API is reusable for any mission built on characteristic functions (Chapters VI, IX–XI). Contributions of this API as separate lemmas are welcome.

Not stated: (57:E*), (57:F*) (given without proof on p. 535), the open question (57:D), and (57:H), because the notion of a "dummy" it uses (from 46.9 and 56.3) is not defined on these pages.

Selected references

J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd ed., 1953), §§56–57, pp. 504–537. https://doi.org/10.1515/9781400829460
J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320. https://doi.org/10.1007/BF01448847

12 thms4 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Operations Research·Captain: mikedeng1

Theory of Games and Economic Behavior VII: Simple Games, Weighted Majorities and the Main Simple SolutionTextbook

Motivation

Many collective decisions are taken by coalitions that either carry the vote or do not: committees, legislatures, shareholder meetings, councils with weighted votes. In such a situation the only aim of a participant is to be part of a coalition that wins, and nothing is left to bargain about except the division of the prize inside the winning coalition. Chapter X of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; 3rd ed. 1953) isolates exactly this class of zero-sum $n$ -person games, the simple games, and studies their numerical description by weighted majorities and their finite main simple solutions.

The chapter is the origin of a large later literature: simple games and weighted voting games are the standard model of voting bodies in political science and social choice (for instance the Shapley–Shubik power index, 1954). The characterization of which simple games admit homogeneous weights, and the solutions they carry, starts here.

Setting

A zero-sum $n$ -person game with players $I = \{1, \dots, n\}$ is represented by its characteristic function $v$ , a real function on the subsets of $I$ with $v(\ominus) = 0$ , $v(-S) = -v(S)$ ( $-S$ the complement) and $v(S \cup T) \geqq v(S) + v(T)$ for disjoint $S, T$ . An imputation is a vector $\vec\alpha$ with $\alpha_i \geqq v((i))$ and $\sum_i \alpha_i = 0$ ; $\vec\alpha$ dominates $\vec\beta$ if some nonempty $S$ has $\sum_{i\in S}\alpha_i \leqq v(S)$ and $\alpha_i > \beta_i$ for $i \in S$ ; a solution is a set $V$ of imputations none of which dominates another and which dominates every imputation outside it (30.1.1). The game is inessential when its reduced form vanishes identically, essential otherwise.

A coalition $S$ is flat if $v(S) = \sum_{k\in S} v((k))$ . The losing coalitions $L_\Gamma$ are the flat sets, and the winning coalitions $W_\Gamma$ are the sets whose complement is flat. The game is simple if it is essential and every coalition is winning or losing. $W^m$ denotes the minimal winning coalitions, those of which no proper subset wins.

Weights $w_1, \dots, w_n$ define the winning system $W = \{S : \sum_{i\in S} w_i > \tfrac12 \sum_i w_i\}$ , and under the conditions (50:B) (non-negative weights, no player with half the total weight, no ties) this is the weighted majority game $[w_1,\dots,w_n]$ . The weights are homogeneous if the advantage $a_S = \sum_{i\in S} w_i - \sum_{i\in -S} w_i$ is the same for all $S$ in $W^m$ .

In §50 the game is taken in reduced form with $\gamma = 1$ , so $v((i)) = -1$ . For numbers $x_i \geqq 0$ and a coalition $S$ let $\vec\alpha^S$ give $-1$ to the players outside $S$ and $-1 + x_i$ to player $i$ in $S$ . When the $x_i$ satisfy $\sum_{i \in S} x_i = n$ for every $S \in W^m$ , the set $V$ of all $\vec\alpha^S$ , $S \in W^m$ , is a main simple solution.

Formalization targets

Goal: (50:K), p. 444

\text{Every homogeneous weighted majority game possesses a main simple solution,}

namely the set of $\vec\alpha^S$ , $S \in W^m$ , with $x_i = \frac{n}{b} w_i$ , $b = \frac12(\sum_i w_i + a)$ , $a$ the common advantage. Conversely, if $x_i \geqq 0$ solve $\sum_{i\in S} x_i = n$ on $W^m$ , then $w_i = x_i$ are homogeneous weights for the game if and only if

\sum_{i=1}^n x_i < 2n .

Milestones

(49:C) $L_\Gamma$ contains the empty set and all one-element sets.
(49:A) $W_\Gamma, L_\Gamma$ are mapped onto each other by complementation, $W_\Gamma$ is closed under supersets, and $L_\Gamma$ is closed under subsets.
(49:B) $W_\Gamma \cap L_\Gamma = \ominus$ if and only if the game is essential. If the game is inessential, every set is both winning and losing.
(49:F) The pairs $W, L$ of simple games are exactly those satisfying (48:A:a)–(48:A:d) and (49:C).
(50:A) The essential three-person game is simple: it is the direct majority game.
(50:B) Non-negative weights define a winning system with (49:W*) if and only if (50:B:a), (50:B:b) hold.
(50:D) $a_S > 0$ on $W$ , $a_S < 0$ on $L$ , and $a_S = 0$ never occurs.
(50:G) An imputation $\vec\beta$ is undominated by $V = \{\vec\alpha^S : S \in U\}$ if and only if $R(\vec\beta) \in U^+$ .
(50:J) The exact criterion (50:8*), (50:9*) for $V$ to be a solution.

Significance

The result links two descriptions of a simple game. One is numerical: a vector of weights, normalized by homogeneity. The other is game-theoretic: a finite solution in which each minimal winning coalition forms and divides a fixed total among its members. When the weights are homogeneous they are, up to scale, the shares in the main simple solution. When a main simple solution exists, its shares are homogeneous weights exactly under the inequality (50:20). The criterion (50:J) behind it is the chapter's general tool for deciding which systems of "profitable" minimal winning coalitions yield a finite solution. It is used again in the enumeration of simple games in §§51–55.

All of the results are proved in the book. As far as a search of the Prove2Me library shows (queries on simple game, weighted majority, winning coalition and stable set, 2026-09-28), none of them has been machine-checked. The only stable-set statements on the platform concern feasible payoff vectors of convex games, which is a different domain. The mission therefore asks for a formal proof of the known results, including the case analysis of §50.5–50.6, and in doing so it produces a reusable Lean theory of simple games and their winning systems.

Difficulty

The characterizations of §49 are set-theoretic, but they depend on superadditivity to show that subsets of flat sets are flat, and on the strategic-equivalence description of essentiality. The substantial part is (50:J). Deciding whether $V$ is a solution means classifying every imputation $\vec\beta$ by the set $R(\vec\beta)$ where it meets the shares $-1 + x_i$ .

The natural first attempt is to check only the minimal winning coalitions. It fails, because domination can be exercised through any winning coalition. The book's argument has to exclude sets of $U^+$ with $\sum_{i\in T} x_i < n$ by producing infinitely many undominated imputations against a finite $V$ . It also has to handle indifferent players with $x_i = 0$ , whose presence makes $R(\vec\beta)$ larger than the coalition that generated $\vec\beta$ . For the converse half of the goal, the obstacle is the strict inequality $a > 0$ : the equations (50:17) are linear and say nothing about it.

Formalization scope

Players are Fin n (the book's player $i$ is index $i - 1$ ), coalitions are Finset (Fin n), and characteristic functions are Finset (Fin n) → ℝ. Imputations are vectors Fin n → ℝ, and systems of coalitions are Set (Finset (Fin n)). A game is identified with its characteristic function (by 26.1 every $v$ satisfying (25:3:a)–(25:3:c) arises from a game). The theory is the "old" one of 30.1.1 (49.1.1), with no excess. The definitions of imputation, domination and solution are the same as in mission V of this series and are restated here, because a draft cannot import another draft.

The standing hypotheses, stated in each theorem where the book has them in force:

(25:3:a)–(25:3:c) on $v$ in every theorem;
simplicity (essential + (49:1:b)) in (50:G), (50:J), (50:K);
the reduced form with $\gamma = 1$ , as $v((i)) = -1$ for all $i$ (50.4.1), in (50:G), (50:J), (50:K);
$U \subseteq W^m$ , (50:7) $x_i \geqq 0$ and (50:8) $\sum_{i\in S} x_i = n$ for $S \in U$ (50.5.1) in (50:G), (50:J);
(50:B) on the weights in (50:D) and in the first half of (50:K);
non-negative weights in (50:B). The book states (50:B) for arbitrary real weights, but its "only if" direction is false without $w_i \geqq 0$ : $[10, 10, 10, -\tfrac1{10}]$ is a counterexample. The corrected statement is recorded in the item.

The numbers $x_i$ are given for every player. Players in no minimal winning coalition, for whom the book defines no $x_i$ , do not affect any $\vec\alpha^S$ . In the converse of (50:K) the derived weights are $w_i = x_i$ for every player.

The goal is not the bare solvability of (50:17). A statement that only asserted " $x$ exists with (50:7), (50:17)" would reduce to linear algebra. The goal asserts that the set of $\vec\alpha^S$ is a solution in the sense of 30.1.1, with domination requiring a nonempty effective set, and it adds the converse equivalence with (50:20). The set $V$ is built from $W^m$ only, never from all of $W$ .

Welcome contributions: proofs of the §49 milestones, which form a small reusable library on winning and losing systems; a proof of (50:G) and (50:J); and lemmas connecting $W_\Gamma$ of a simple reduced game with the explicit formula (49:2), $v(S) = n - |S|$ on $W$ and $-|S|$ on $L$ .

Selected references

J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary ed., Princeton University Press, 2007 (reprint of the 3rd ed., 1953), Chapter X, §§48–50, pp. 420–444. https://doi.org/10.1515/9781400829460
L. S. Shapley, M. Shubik, "A method for evaluating the distribution of power in a committee system", American Political Science Review 48 (1954) 787–792. https://doi.org/10.2307/1951053

13 thms4 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Theory of Games and Economic Behavior IV: The Characteristic Function of a Zero-Sum n-Person GameTextbook

Motivation

Chapter VI of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; 3rd ed. 1953) opens the general theory of zero-sum games with more than two players. The authors propose to describe everything that can be said about coalitions, compensations between partners and fights between coalitions through one numerical object, the characteristic function $v(S)$ : the amount a group of players $S$ can secure for itself against all the others (25.2.1). The whole later theory of the book (imputations, domination, solutions, simple games, decomposition) is built on this set function, and the same object, under the name "coalitional game" or "TU game", is the starting point of cooperative game theory as a field (cores, Shapley value, nucleolus).

§§25–27 settle two foundational questions about it. First, which set functions arise as characteristic functions of actual games? Second, which characteristic functions describe the same strategic situation, and how is a canonical representative chosen? The answers (a complete characterization by three conditions, and the reduced form under strategic equivalence) are what later chapters, and much of the cooperative literature, use when they take "a characteristic function" as a primitive without reference to any game.

Setting

A zero-sum $n$ -person game in normalized form $\Gamma$ (11.2.3, 25.1.3) has players $k = 1, \dots, n$ . Player $k$ chooses a pure strategy $\tau_k \in \{1, \dots, \beta_k\}$ , $\beta_k \geqq 1$ , uninformed about the others' choices, and then receives the real amount $\mathcal H_k(\tau_1, \dots, \tau_n)$ , subject to (25:1)

\sum_{k=1}^n \mathcal H_k(\tau_1, \dots, \tau_n) \equiv 0 .

Let $I = \{1, \dots, n\}$ and, for $S \subseteq I$ , $-S = I \setminus S$ . The book defines $v(S)$ in 25.1.3 through a fictitious two-person game: all players of $S$ form one composite player $1'$ , all players of $-S$ another, $2'$ . The pure strategies of $1'$ are the aggregates $\tau^S$ (one choice $\tau_k$ for each $k \in S$ ), those of $2'$ are the aggregates $\tau^{-S}$ , and $1'$ receives (25:2)

\overline{\mathcal H}(\tau^S, \tau^{-S}) = \sum_{k \in S} \mathcal H_k(\tau_1, \dots, \tau_n).

A mixed strategy of $1'$ is a probability vector $\xi$ on the set of all aggregates $\tau^S$ , and one of $2'$ is a probability vector $\eta$ on the aggregates $\tau^{-S}$ . With $K(\xi, \eta) = \sum_{\tau^S, \tau^{-S}} \overline{\mathcal H}(\tau^S, \tau^{-S})\, \xi_{\tau^S} \eta_{\tau^{-S}}$ ,

v(S) = \operatorname{Max}_\xi \operatorname{Min}_\eta K(\xi, \eta) = \operatorname{Min}_\eta \operatorname{Max}_\xi K(\xi, \eta).

The coalition therefore randomizes jointly: $\xi$ is one distribution over its members' strategy tuples, not a product of independent mixtures. The empty set and $I$ are coalitions too (footnote 2, p. 241).

The three conditions of 25.3.1 on a set function $v$ are

\text{(25:3:a)}\ v(\ominus) = 0, \qquad \text{(25:3:b)}\ v(-S) = -v(S), \qquad \text{(25:3:c)}\ v(S \cup T) \geqq v(S) + v(T) \ \text{ if } S \cap T = \ominus .

From 26.2 on, every set function satisfying them is called a characteristic function.

Two such functions are strategically equivalent (27.1) if $v'(S) = v(S) + \sum_{k \in S} \alpha^0_k$ for numbers $\alpha^0_k$ with $\sum_k \alpha^0_k = 0$ ((27:1), (27:2)). A function is reduced if all one-element coalitions have the same value, (27:3); with that common value written $-\gamma$ , (27:5). A game is inessential if the reduced form of its characteristic function is $\equiv 0$ , and essential otherwise (27.3).

Formalization targets

Goal: the characterization of characteristic functions (26.2)

v \text{ satisfies (25:3:a)–(25:3:c)} \iff \exists\, \Gamma \text{ zero-sum } n\text{-person game with } v_\Gamma = v .

The "only if" half is 25.3.1; the "if" half is 26.1.1, which requires a single game $\Gamma$ realizing $v$ on every coalition simultaneously.

Milestones

25.3.1: every $v_\Gamma$ satisfies (25:3:a)–(25:3:c).
(25:A): the three conditions are equivalent to $v(S_1) + \dots + v(S_p) \leqq 0$ on decompositions of $I$ for $p = 1, 2, 3$ , with equality for $p = 1, 2$ .
26.1.1: every $v$ satisfying (25:3:a)–(25:3:c) is $v_\Gamma$ for some game $\Gamma$ .
(27:A): every characteristic function is strategically equivalent to exactly one reduced characteristic function, given by (27:2), (27:4).
(27:7): for reduced $\bar v$ and every $p$ -element $S$ , $-p\gamma \leqq \bar v(S) \leqq (n-p)\gamma$ , with equality in the stated boundary cases.
(27:B): inessential iff $\sum_j v((j)) = 0$ ; essential iff $\sum_j v((j)) < 0$ .
(27:C) and (27:D): inessential iff $v$ is additive, $v(S) \equiv \sum_{k \in S} \alpha^0_k$ , equivalently iff (25:3:c) always holds with equality.

Significance

The characterization makes the three conditions (25:3:a)–(25:3:c) the complete axiomatics of zero-sum characteristic functions. Every later result in the book that is stated "for a characteristic function" (the solutions of the three-person game in §32, the simple games of Chapter X, the decomposition theory of Chapter IX) is thereby a result about zero-sum games, and conversely no further constraint on $v$ is hidden in the game model. The reduced form of §27 cuts the parameter space of characteristic functions by $n$ and turns essentiality into a sign condition, which is used throughout the rest of the book.

These results are proved in the book. As far as a search of the Prove2Me catalog shows (queries on characteristic function, coalition, strategic equivalence, inessential, superadditive), none of them is formalized there; the existing cooperative-game definitions on the platform use other normalizations ( $v(\emptyset) = 0$ only, no complementarity condition) and are not this object. The mission produces a machine-checked link between the non-cooperative model of an $n$ -person game and the cooperative set function, including the book's explicit game construction behind 26.1.1.

Difficulty

The "only if" direction requires comparing values of different two-person games: (25:3:c) asks that the coalition $S \cup T$ can guarantee as much as $S$ and $T$ separately, which rests on the coalition mixing jointly, and (25:3:b) needs the minimax theorem, since $v(-S)$ is a Max-Min for the opposite side. The "if" direction is an existence claim: from an abstract $v$ one must produce one finite game whose characteristic function matches $v$ on all $2^n$ coalitions at once. Producing, for each $S$ separately, a game with the right value $v_\Gamma(S)$ is easy and proves nothing. The §27 results are finite linear algebra over set functions, but the uniqueness in (27:A) and the boundary equalities in (27:7) depend on using all three conditions.

Formalization scope

Players are Fin n (the book's $1, \dots, n$ are $0, \dots, n-1$ ), coalitions are Finset (Fin n), $-S$ is the complement Sᶜ, and set functions are Finset (Fin n) → ℝ. A game is a structure ZeroSumGame n with strategy sets Fin (β k), a field β k > 0 (finitely many and at least one pure strategy per player), real payoffs H τ k, and the zero-sum condition (25:1) as a field. An aggregate $\tau^S$ is a dependent function on the members of $S$ ; mixed strategies are elements of Mathlib's stdSimplex, and the coalition's $\xi$ is a single distribution on aggregates, as in 25.1.3. The Max and Min in $v(S)$ are written as ⨆/⨅ over the simplices; these are nonempty and the bilinear form is bounded on them, so no junk value arises. No lower bound on $n$ is imposed: the book's statements remain true for $n = 0$ and $n = 1$ , so dropping the implicit $n \geqq 1$ is a harmless strengthening.

Standing hypotheses instantiated in the statements: finiteness of the strategy sets and (25:1) (25.1.3) are part of ZeroSumGame; the §27 results carry (25:3:a)–(25:3:c) as a hypothesis, the book's standing assumption from 26.2 on ("characteristic function"); (27:7) carries reducedness (27:3) and the definition (27:5) of $\gamma$ ; strategic equivalence includes (27:1). The reduced form is the explicit function of (27:2), (27:4), with $\frac1n$ as a real division that only matters for $n \geqq 1$ .

A trivializing reading of the goal, "for every $S$ there is a game with $v_\Gamma(S) = v(S)$ ", is excluded: the statement asks for one game $\Gamma$ with $v_\Gamma = v$ as functions. The coalition value is not the value under independent mixtures of the members, which is smaller in general and for which (25:3:c) can fail.

A complete development needs the minimax theorem for finite matrix games (the platform's AGT.zero_sum_minimax covers it for matrices indexed by Fin (m+1), and can be transported to the aggregate types), bookkeeping for splitting and joining strategy profiles along $S$ and $-S$ , and the construction of 26.1 with its zero-sum check. The profile-splitting lemmas and the value facts for coalition games are reusable for the book's Chapter XI (general games) and for any work on coalitional values of strategic games. Contributions welcome: the §27 milestones, which are self-contained, and the two directions of the goal.

Selected references

J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd edition, 1953), §§25–27, pp. 238–254. https://doi.org/10.1515/9781400829460
J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320 (the minimax theorem used for $v(S)$ ). https://doi.org/10.1007/BF01448847
M. Maschler, E. Solan and S. Zamir, Game Theory, Cambridge University Press, 2013, Ch. 16 (coalitional games with transferable utility). https://doi.org/10.1017/CBO9780511794216

13 thms4 active usersReviewed

Completed

Algorithmic Game Theory Convex Optimization Linear Optimization+1·Captain: mikedeng1

Theory of Games and Economic Behavior III: Mixed Strategies, the Minimax Theorem and Good StrategiesTextbook

Motivation

A zero-sum two-person game in normalized form is a real matrix $\mathcal H(\tau_1, \tau_2)$ : player 1 chooses a row $\tau_1$ , player 2 simultaneously chooses a column $\tau_2$ , and player 2 pays player 1 the amount $\mathcal H(\tau_1, \tau_2)$ . Matrix games are the base case of non-cooperative game theory, the prototype of every minimax statement in optimization, statistics (Wald's decision theory) and online learning, and, through their equivalence with linear programming, a standard tool of operations research.

Chapter III of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; third edition 1953) gives the book's complete solution of these games. Timeline:

1928. J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Math. Annalen 100, proves that every matrix game has a value in mixed strategies (the minimax theorem), by a topological argument. https://doi.org/10.1007/BF01448847
1937. von Neumann's growth-model paper gives a second proof via a fixed-point argument, later generalized by Kakutani (1941).
1938. J. Ville gives the first elementary proof, based on convexity.
1944. The Theory of Games presents Ville's route: a theorem of the alternative for matrices (§16) yields the minimax theorem (17:6), from which §17 derives the structure of the sets of good strategies.
1951. Gale, Kuhn and Tucker, and Dantzig, relate matrix games to linear-programming duality.

Setting

Player 1 has $\beta_1 \ge 1$ pure strategies $\tau_1$ , player 2 has $\beta_2 \ge 1$ pure strategies $\tau_2$ , and $\mathcal H$ is an arbitrary real $\beta_1 \times \beta_2$ matrix (14.1.1). A mixed strategy of player 1 is a probability vector $\xi$ in the simplex

S_{\beta_1} = \Big\{ \xi \in \mathbb R^{\beta_1} : \xi_{\tau_1} \ge 0,\ \sum_{\tau_1} \xi_{\tau_1} = 1 \Big\},

and similarly $\eta \in S_{\beta_2}$ for player 2. The pure strategy $\tau$ is the coordinate vector $\delta^{\tau}$ . The expected payoff is the bilinear form (17:2)

K(\xi, \eta) = \sum_{\tau_1=1}^{\beta_1} \sum_{\tau_2=1}^{\beta_2} \mathcal H(\tau_1, \tau_2)\, \xi_{\tau_1} \eta_{\tau_2}.

The good strategies of player 1 form the set $\bar A$ of those $\xi \in S_{\beta_1}$ at which $\operatorname{Min}_\eta K(\xi, \eta)$ assumes its maximum; those of player 2 form the set $\bar B$ of those $\eta \in S_{\beta_2}$ at which $\operatorname{Max}_\xi K(\xi, \eta)$ assumes its minimum ((17:B:a), (17:B:b)). A saddle point of $K$ is a pair with $K(\xi', \eta) \le K(\xi, \eta) \le K(\xi, \eta')$ for all $\xi', \eta'$ . With pure strategies alone one has $v_1 = \operatorname{Max}_{\tau_1}\operatorname{Min}_{\tau_2}\mathcal H$ and $v_2 = \operatorname{Min}_{\tau_2}\operatorname{Max}_{\tau_1}\mathcal H$ ; the game is specially strictly determined when $v_1 = v_2$ .

For a general real function $\phi(x, y)$ (§13) the same notions are $\operatorname{Max}_x \operatorname{Min}_y \phi$ , $\operatorname{Min}_y \operatorname{Max}_x \phi$ , saddle points, and the sets $A^\phi$ (maximizers of $\operatorname{Min}_y \phi$ ) and $B^\phi$ (minimizers of $\operatorname{Max}_x \phi$ ), always under the book's standing hypothesis that these maxima and minima exist.

Formalization targets

Goal: (17:D), good strategies characterized by their supports

For all $\xi \in S_{\beta_1}$ and $\eta \in S_{\beta_2}$ : $\xi \in \bar A$ and $\eta \in \bar B$ if and only if

\xi_{\tau_1} = 0 \text{ whenever } \sum_{\tau_2} \mathcal H(\tau_1, \tau_2)\eta_{\tau_2} < \max_{\tau_1'} \sum_{\tau_2} \mathcal H(\tau_1', \tau_2)\eta_{\tau_2},

\eta_{\tau_2} = 0 \text{ whenever } \sum_{\tau_1} \mathcal H(\tau_1, \tau_2)\xi_{\tau_1} > \min_{\tau_2'} \sum_{\tau_1} \mathcal H(\tau_1, \tau_2')\xi_{\tau_1}.

The statement fixes no value and no constant; it says which pairs of mixed strategies are optimal.

Milestones, in attack order

(13:A*) $\operatorname{Max}_x \operatorname{Min}_y \phi \le \operatorname{Min}_y \operatorname{Max}_x \phi$ .
(13:D*) If $\operatorname{Max}\operatorname{Min} = \operatorname{Min}\operatorname{Max}$ , the saddle points of $\phi$ are exactly $A^\phi \times B^\phi$ .
(17:A) $\operatorname{Min}_\eta K(\xi, \eta) = \operatorname{Min}_{\tau_2} \sum_{\tau_1} \mathcal H(\tau_1, \tau_2)\xi_{\tau_1}$ , and dually for $\operatorname{Max}_\xi$ .
(16:C) For every matrix $a(i, j)$ exactly one of: some $x \in S_m$ with $\sum_j a(i,j)x_j \le 0$ for all $i$ ; some $w \in S_n$ with $\sum_i a(i,j)w_i > 0$ for all $j$ .
(16:F) The weak form with $\ge 0$ in place of $> 0$ .
(17:6) The minimax theorem: a saddle point of $K$ exists (already on the platform as AGT.zero_sum_minimax, proved).
(17:C:f) $\xi \in \bar A$ and $\eta \in \bar B$ iff $\xi, \eta$ is a saddle point of $K$ .

After the goal: (17:E) the game is specially strictly determined iff each player has a pure good strategy.

Significance

(17:D) is the complementary-slackness description of the optimal strategy pairs of a matrix game: a good strategy puts weight only on pure strategies that are best replies to the opponent's good strategy, and conversely any pair of mutually supported best replies is optimal. It is the basis of support-enumeration methods for matrix games, of the equalizing arguments used to solve small games by hand (the book's Chapter IV applies it to Matching Pennies, Stone–Paper–Scissors and Poker), and of the rectangular structure $\bar A \times \bar B$ of the set of optimal pairs. (17:E) connects the mixed-strategy solution to the pure-strategy theory of §14 and to the perfect-information games of §15.

The results are classical and proved in the book. The minimax theorem itself is already machine-checked on the platform (AGT.zero_sum_minimax), and Mathlib contains Sion's minimax theorem and the basic saddle-point lemmas for extended-real functions on sets. This mission adds the book's own chain: the §13 saddle-point calculus under its standing attainment hypothesis, the theorems of the alternative (16:C) and (16:F) in the simplex-normalized form the book uses, the reduction (17:A) to pure strategies, and the characterizations (17:C:f), (17:D), (17:E) of good strategies, which are not on the platform in any form.

Difficulty

The "if" direction of (17:D) cannot be proved from the support conditions alone by local reasoning: that a pair of mutual best replies consists of good strategies uses that the value $\operatorname{Max}_\xi \operatorname{Min}_\eta K$ equals $\operatorname{Min}_\eta \operatorname{Max}_\xi K$ , i.e. the minimax theorem. Without that equality the "if" direction of (13:D*) fails (points of $A^\phi \times B^\phi$ exist but are not saddle points), so the calculus of §13 alone does not suffice. Likewise (16:C) is not a direct instance of the Farkas lemma forms on the platform: its alternatives are normalized to the simplex and the second one is strict, and both the existence and the mutual exclusion must be shown.

Formalization scope

Lean conventions, fixed throughout:

Pure strategies are Fin β₁, Fin β₂ (numbered from $0$ ), the matrix is H : Fin β₁ → Fin β₂ → ℝ, and $S_\beta$ is Mathlib's stdSimplex ℝ (Fin β).
Nonempty strategy sets ( $\beta \ge 1$ , from "τ = 1, …, β" in 14.1.1): every theorem assumes 0 < β₁, 0 < β₂, or mixed strategies $\xi \in S_{\beta_1}$ , $\eta \in S_{\beta_2}$ , which force it. The theorems of the alternative assume $n, m \ge 1$ (a matrix with rows and columns).
Standing hypothesis of 13.2.1 ("we are restricting our considerations to such functions, for which Max and Min exist"): the §13 results (13:A*), (13:D*) are stated for an arbitrary $\phi : X \times Y \to \mathbb R$ under the predicate MaxMinAttained φ, which says that $\operatorname{Min}_y \phi(x, y)$ , $\operatorname{Max}_x \phi(x, y)$ , $\operatorname{Max}_x \operatorname{Min}_y \phi$ and $\operatorname{Min}_y \operatorname{Max}_x \phi$ are attained. (13:D*) also carries the hypothesis of 13.5.2 that saddle points exist, stated as $\operatorname{Max}_x \operatorname{Min}_y \phi = \operatorname{Min}_y \operatorname{Max}_x \phi$ .
$\operatorname{Max}$ and $\operatorname{Min}$ are the real ⨆, ⨅; they are the book's attained values under the hypotheses above (compactness of the simplex and continuity of $K$ for the mixed game). (17:A) asserts attainment explicitly (IsLeast, IsGreatest). "Does not assume its maximum at $\tau_1$ " in the goal is written without any Max operator.
$\bar A$ , $\bar B$ are defined as maximizers and minimizers directly from $K$ , not through an assumed value $v'$ .

A trivializing formalization is ruled out: $\bar A$ and $\bar B$ are not taken as hypotheses or defined through the support conditions, strategy sets cannot be empty, and no Max over an empty or unbounded set occurs.

Contributions welcome: proofs of the milestones, especially (16:C) (from Mathlib's convex separation or from a platform Farkas lemma) and the bridge from AGT.zero_sum_minimax to (17:C:f). The §13 lemmas and the (17:A) reduction are reusable by any mission about matrix games or bilinear saddle points.

Selected references

J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd edition, 1953), §§13, 16, 17. https://doi.org/10.1515/9781400829460
J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320. https://doi.org/10.1007/BF01448847
J. Ville, "Sur la théorie générale des jeux où intervient l'habileté des joueurs", in É. Borel, Traité du calcul des probabilités et de ses applications, IV.2, Gauthier-Villars, 1938, 105–113.
S. Kakutani, "A generalization of Brouwer's fixed point theorem", Duke Mathematical Journal 8 (1941), 457–459. https://doi.org/10.1215/S0012-7094-41-00838-4
D. Gale, H. W. Kuhn and A. W. Tucker, "Linear programming and the theory of games", in Activity Analysis of Production and Allocation, Wiley, 1951, 317–329.

11 thms4 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Theory of Games and Economic Behavior I: Numerical Utility from the Axioms of Preference and MixtureTextbook

Motivation

Game theory as von Neumann and Morgenstern built it measures every outcome by a single number, the utility a player attaches to it, and combines those numbers linearly when an outcome is uncertain: a lottery that yields $u$ with probability $\alpha$ and $v$ with probability $1-\alpha$ is worth $\alpha\,\mathrm v(u) + (1-\alpha)\,\mathrm v(v)$ . Every later chapter of Theory of Games and Economic Behavior uses this without comment, from the value of a zero-sum game to the characteristic function of a coalition. Section 3 of the book justifies it: it states axioms on preferences and on the combination of alternatives with probabilities, and claims that they force utility to be a number, unique up to the choice of a zero and a unit. The proof, announced in 3.6.1 as "somewhat lengthy", was added as the Appendix The Axiomatic Treatment of Utility in the second edition (1947).

The result, the expected utility theorem, is the foundation of decision theory under risk and of expected-payoff reasoning in game theory, statistics and operations research. The axiomatics were later recast by Marschak (1950), Herstein and Milnor (1953) in the language of mixture spaces (Herstein–Milnor). This mission formalizes the original statement and its original proof structure.

Setting

A system of utilities (3.6.1) is an abstract set $U$ of entities $u, v, w, \dots$ , together with

a relation $u > v$ (" $u$ is preferable to $v$ "); write $u < v$ for $v > u$ ;
for every number $\alpha$ with $0 < \alpha < 1$ , an operation producing an element written $\alpha u + (1-\alpha) v$ of $U$ from $u, v \in U$ .

The axioms are:

(3:A) $>$ is a complete ordering: (3:A:a) for any $u, v$ exactly one of $u = v$ , $u > v$ , $u < v$ holds; (3:A:b) $u > v$ , $v > w$ imply $u > w$ .
(3:B) Ordering and combining: (3:B:a) $u < v$ implies $u < \alpha u + (1-\alpha)v$ ; (3:B:b) $u > v$ implies $u > \alpha u + (1-\alpha)v$ ; (3:B:c) $u < w < v$ implies $\alpha u + (1-\alpha)v < w$ for some $\alpha$ ; (3:B:d) $u > w > v$ implies $\alpha u + (1-\alpha)v > w$ for some $\alpha$ .
(3:C) Algebra of combining: (3:C:a) $\alpha u + (1-\alpha)v = (1-\alpha)v + \alpha u$ ; (3:C:b) $\alpha(\beta u + (1-\beta)v) + (1-\alpha)v = \gamma u + (1-\gamma)v$ with $\gamma = \alpha\beta$ .

All weights lie strictly between $0$ and $1$ , and $=$ is identity. The expression $\alpha u + (1-\alpha)v$ is notation for an abstract operation: $U$ carries no linear structure. The Appendix mostly writes the operation as $(1-\gamma)u + \gamma v$ , and writes $u \leqq v$ for " $u = v$ or $u < v$ ". In the Lean development the system is the structure UtilitySystem U with fields gt and mix; S.cmb γ u v is $(1-\gamma)u + \gamma v$ .

A numerical utility (3.5.1) is a map $\mathrm v : U \to \mathbb R$ with

\text{(i)}\quad u > v \implies \mathrm v(u) > \mathrm v(v), \qquad \text{(ii)}\quad \mathrm v\big((1-\gamma)u + \gamma v\big) = (1-\gamma)\mathrm v(u) + \gamma\,\mathrm v(v) \quad (0<\gamma<1).

Formalization targets

Goal: (A:V) and (A:W), p. 627

For every system of utilities satisfying (3:A)–(3:C):

\exists\, \mathrm v : U \to \mathbb R \ \text{with (i), (ii)}, \qquad\text{and}\qquad \forall\, \mathrm v, \mathrm v' \text{ with (i), (ii)}:\ \exists\, \omega_0 > 0,\ \omega_1,\ \forall w,\ \ \mathrm v'(w) = \omega_0\,\mathrm v(w) + \omega_1 .

The constants $\omega_0, \omega_1$ are chosen before $w$ . No assumption on the size of $U$ is made.

Milestones

The milestones follow the Appendix's own chain:

(A:A) if $u < v$ and $\alpha < \beta$ then $(1-\alpha)u + \alpha v < (1-\beta)u + \beta v$ ;
(A:B), (A:C) for $u_0 < v_0$ , the map $\alpha \mapsto (1-\alpha)u_0 + \alpha v_0$ is a one-to-one, monotone map of $(0,1)$ onto the utility interval $u_0 < w < v_0$ ;
(A:E), (A:F) the interval function $f_{u_0,v_0}$ of (A:D) (value $0$ at $u_0$ , $1$ at $v_0$ , and the weight $\alpha$ in between) is monotone and linear toward each endpoint, and is characterized by these properties;
(A:R), (A:S) for fixed $u^* < v^*$ , the normalized mapping $h$ with $h(u^*) = 0$ , $h(v^*) = 1$ , monotone, and linear on combinations of $u < v$ , exists and is unique;
(A:T) $(1-\gamma)u + \gamma u = u$ always;
(A:U) $h$ is linear on all combinations, without the restriction $u < v$ .

Significance

The theorem turns an ordinal preference over uncertain prospects into a cardinal scale on which expectation is meaningful. It is what licenses replacing a player's preferences by numerical payoffs whose mixtures are averaged, which the rest of the book, and most of game theory and stochastic optimization after it, assumes. The uniqueness part (A:W) states exactly how much freedom the scale has: a positive linear transformation, i.e. zero and unit may be fixed at will and nothing else.

The theorem has been proved many times since 1947, in textbooks and in the mixture-space literature, but the book's axiom system differs from the later ones (it uses a strict order with identity, strict monotony, and the two algebraic axioms (3:C) only). As far as the curators know, neither this axiom system nor the Appendix's derivation has a machine-checked proof, and Mathlib has no mixture-space or expected-utility module. The mission produces a checked proof of the original theorem under its original hypotheses and a reusable abstract mixture-space layer.

Difficulty

The obvious argument treats $U$ as a convex set and $\alpha u + (1-\alpha)v$ as a convex combination, then reads the utility off the segment between two reference points. None of that is available. The operation is formal, so identities that hold in a vector space, idempotence $(1-\gamma)u + \gamma u = u$ included, must be derived from (3:B) and (3:C) alone; only one associativity rule (3:C:b), for a repeated right argument, is given. The correspondence between a utility interval and a numerical interval requires the continuity axioms (3:B:c), (3:B:d) and the completeness of the reals. The local scales on different intervals have to be fitted into one global function, and the linearity for pairs $u > v$ and $u = v$ has to be recovered from the case $u < v$ .

Formalization scope

$U$ is an arbitrary type (Type*); the relation is gt : U → U → Prop and the operation mix : OpenUnit → U → U → U, where OpenUnit is the subtype $(0,1)$ of $\mathbb R$ . mix α u v stands for $\alpha u + (1-\alpha)v$ . The operation is not defined at $\alpha = 0, 1$ (3.6.1, footnote 4) and is not extended there.
Axiom (3:A:a) is stated literally ("exactly one of the three relations"), so the order is a strict total order and indifference is identity (A.1.2). The weak-order generalization of §66 is not this theorem.
Numbers are real numbers. Monotony is strict, as in (3:1:a).
Standing hypotheses: every item assumes (3:A)–(3:C), bundled in UtilitySystem. The items from (A:E) on assume fixed $u_0 < v_0$ or $u^* < v^*$ as explicit hypotheses, as the book does "from now on until we get to (A:V) and (A:W)"; the goal does not, since (A:V), (A:W) hold for every $U$ .
The interval function $f_{u_0,v_0}$ is a total Lean function; its value outside $u_0 \leqq w \leqq v_0$ is a placeholder that no statement uses.
A formalization in which $U$ is a convex subset of a vector space, or a space of probability measures, assumes more than the book and makes (A:T) free; it does not count. Neither does a weak monotony, under which constant maps satisfy (A:V) and (A:W) fails.

A complete development needs only order theory and the completeness of the reals from Mathlib. The mixture-space layer (the structure, (A:A)–(A:C), (A:T)) is reusable for any later work on expected utility, including the generalization in §66 and 67 of the book. Proofs of any milestone, alternative routes to the goal (for instance through the Herstein–Milnor axioms, once shown to follow from (3:A)–(3:C)), and statements of the omitted intermediate results (A:G)–(A:Q) are all welcome.

Selected references

J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd edition, 1953), §3 and Appendix. https://doi.org/10.1515/9781400829460
I. N. Herstein, J. Milnor, An axiomatic approach to measurable utility, Econometrica 21 (1953), 291–297. https://doi.org/10.2307/1905540
J. Marschak, Rational behavior, uncertain prospects, and measurable utility, Econometrica 18 (1950), 111–141. https://doi.org/10.2307/1907264

12 thms4 active usersReviewed

Dynamical Systems Group Theory·Captain: Lucas

Gottschalk's Surjunctivity ConjectureOpen Problem

Motivation

A cellular automaton over a group $G$ with a finite alphabet $A$ is a map on configurations $x : G \to A$ that updates every cell by the same finite local rule, read off from a finite neighbourhood of that cell. Cellular automata over $\mathbb{Z}^d$ go back to von Neumann and Ulam and are a standard model in symbolic dynamics; replacing $\mathbb{Z}^d$ by an arbitrary group links the theory to geometric group theory.

In 1973 Gottschalk asked which groups $G$ have the property that every injective cellular automaton over $G$ is automatically surjective, and called such groups surjunctive. For a finite group this is the pigeonhole principle, since $A^G$ is then a finite set. For infinite groups the configuration space is an uncountable compact space and the pigeonhole principle is no longer available. Gottschalk's surjunctivity conjecture states that every group is surjunctive. It is open.

Timeline

1962–1963 — Moore and Myhill prove the Garden of Eden theorem for $\mathbb{Z}^2$ (and, in the same way, $\mathbb{Z}^d$ ): a cellular automaton is surjective if and only if it is pre-injective. In particular $\mathbb{Z}^d$ is surjunctive.
1969 — Hedlund (crediting Curtis and Lyndon) characterises cellular automata over $\mathbb{Z}$ as the continuous shift-commuting self-maps of $A^{\mathbb{Z}}$ (the Curtis–Hedlund–Lyndon theorem); the characterisation extends to every group.
1973 — Gottschalk introduces surjunctivity and states the conjecture; he records Lawton's result that residually finite groups are surjunctive.
1999 — Ceccherini-Silberstein, Machì and Scarabotti prove the Garden of Eden theorem for amenable groups, which implies that amenable groups are surjunctive.
1999–2000 — Gromov introduces what Weiss names sofic groups, and both show that sofic groups are surjunctive. Sofic groups include all residually finite groups and all amenable groups.
Today — no group is known to be non-sofic, and no group is known to be non-surjunctive.

Setting

Fix a group $G$ and a finite nonempty set $A$ (the alphabet). A configuration is a function $x : G \to A$ ; the set of configurations is $A^G$ . It carries the product topology, where $A$ has the discrete topology; this makes $A^G$ compact.

The left shift of $x$ by $g \in G$ is the configuration

(g \cdot x)(h) = x(g^{-1}h), \qquad h \in G,

written shift G g x in the Lean development. A map $\tau : A^G \to A^G$ is shift-equivariant (IsShiftEquivariant) if $\tau(g\cdot x) = g\cdot\tau(x)$ for all $g$ and $x$ .

The group $G$ is surjunctive (IsSurjunctive) if, for every finite nonempty alphabet $A$ , every map $\tau : A^G \to A^G$ that is continuous, shift-equivariant and injective is also surjective.

A map $\tau$ is a cellular automaton (IsCellularAutomaton) if there are a finite memory set $S \subseteq G$ and a local rule $\mu : A^S \to A$ with

\tau(x)(g) = \mu\big(s \mapsto x(gs)\big) \qquad \text{for all } x \in A^G,\ g \in G.

Three classes of groups appear in the milestones:

$G$ is residually finite (IsResiduallyFinite) if every $g \neq 1$ lies outside some normal subgroup of finite index.
$G$ is amenable if there is a finitely additive, left-invariant probability measure defined on all subsets of $G$ (the existing platform definition Garrido.IsAmenable).
$G$ is sofic (IsSofic) if for every finite $K \subseteq G$ and every $\varepsilon > 0$ there are a finite nonempty set $X$ and a map $\sigma : G \to \mathrm{Sym}(X)$ such that $\sigma_{gh}(x) = \sigma_g(\sigma_h(x))$ for at least a $(1-\varepsilon)$ fraction of the points $x \in X$ whenever $g, h \in K$ , and $\sigma_g(x) \neq x$ for at least a $(1-\varepsilon)$ fraction of the points whenever $g \in K \setminus \{1\}$ .

Formalization targets

Goal: Gottschalk's conjecture

\forall\, G \text{ group}: \quad G \text{ is surjunctive.}

Milestones

Curtis–Hedlund–Lyndon: for finite $A$ , a map $\tau : A^G \to A^G$ is continuous and shift-equivariant if and only if it is a cellular automaton.
Subgroups: every subgroup of a surjunctive group is surjunctive.
Local character: if every finitely generated subgroup of $G$ is surjunctive, then $G$ is surjunctive.
Finite groups are surjunctive.
Residually finite groups are surjunctive (Lawton).
Amenable groups are surjunctive (Ceccherini-Silberstein–Machì–Scarabotti).
Sofic groups are surjunctive (Gromov; Weiss).

Significance

The result itself. A positive answer would make the implication "injective $\Rightarrow$ surjective" for cellular automata hold unconditionally, extending the pigeonhole principle from finite sets to all shift spaces $A^G$ . Surjunctivity is also tied to Kaplansky's direct finiteness conjecture: for a surjunctive group $G$ and any finite field $K$ , the group ring $K[G]$ is directly finite ( $ab = 1 \Rightarrow ba = 1$ ). A counterexample would be the first known non-sofic group, since sofic groups are surjunctive.

Formalizing it. Milestones 4–7 are proved results in the literature; milestones 1–3 are standard facts of the theory. At the time of writing, none of milestones 1–3 and 5–7 is known to exist as a machine-checked proof on this platform. Formalizing them requires building the basic theory of cellular automata over groups (memory sets, local rules, induced automata on subgroups), which can be reused by other work in symbolic dynamics. The goal theorem itself is open.

Difficulty

For infinite $G$ the space $A^G$ is infinite, so no counting argument applies directly. All known proofs approximate $G$ by finite objects: finite quotients (residually finite case), Følner sets with an entropy count (amenable case), or approximate finite permutation models (sofic case). No such approximation is known to exist for every group, and it is not known whether every group is sofic. A proof of the full conjecture therefore needs either a proof that every group is sofic or an argument that does not go through finite approximations.

Formalization scope

Groups $G$ and alphabets $A$ live in Type (universe $0$ ). Alphabets are finite (Fintype) and nonempty; their topology is an arbitrary topology assumed to be discrete, and $A^G$ carries Lean's product topology.
The shift is a plain function shift, not a MulAction instance, to avoid a clash with Mathlib's pointwise action on function types.
Amenability is taken from the existing platform definition Garrido.IsAmenable (finitely additive invariant probability measure on all subsets). Residual finiteness and soficity are defined in GottschalkSurjunctivity_Defs.
Soficity is stated with a normalised count of points; the conditions are required for every $\varepsilon > 0$ , so small $\varepsilon$ is where the content lies.
Surjunctivity is not trivialised by the nonemptiness assumption: for a nonempty group and a nonempty alphabet, $A^G$ is nonempty and, when $G$ is infinite, uncountable.

Contributions welcome: the Curtis–Hedlund–Lyndon theorem, restriction and induction of cellular automata along subgroups, and the residually finite case are natural first steps.

Selected references

W. H. Gottschalk, Some general dynamical notions, Recent Advances in Topological Dynamics, Lecture Notes in Math. 318, Springer, 1973, pp. 120–125. https://doi.org/10.1007/BFb0061728
G. A. Hedlund, Endomorphisms and automorphisms of the shift dynamical system, Math. Systems Theory 3 (1969), 320–375. https://doi.org/10.1007/BF01691062
T. Ceccherini-Silberstein, A. Machì, F. Scarabotti, Amenable groups and cellular automata, Ann. Inst. Fourier 49 (1999), 673–685. https://doi.org/10.5802/aif.1686
M. Gromov, Endomorphisms of symbolic algebraic varieties, J. Eur. Math. Soc. 1 (1999), 109–197. https://doi.org/10.1007/PL00011162
B. Weiss, Sofic groups and dynamical systems, Sankhyā Ser. A 62 (2000), 350–359.
T. Ceccherini-Silberstein, M. Coornaert, Cellular Automata and Groups, Springer Monographs in Mathematics, 2010. https://doi.org/10.1007/978-3-642-14034-1
Wikipedia, Surjunctive group. https://en.wikipedia.org/wiki/Surjunctive_group

10 thms4 active usersReviewed

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Convex Optimization I: Prékopa's TheoremTextbook

Markov Entanglement: Value Decomposition Error in Multi-agent MDPsResearch Paper

Excursion Coupling for the Monge Problem on the Line (Juillet 2019)Research Paper

Introduction to Linear Optimization X: Max-Flow Min-CutTextbook

Bandit Algorithms XIII: Pure Exploration and Best-Arm IdentificationTextbook

Bandit Algorithms IV: Bernoulli Bandits and KL-UCBTextbook

Bandit Algorithms VI: Information-Theoretic FoundationsTextbook

The Riemann HypothesisOpen Problem

Convex Optimization: Algorithms and Complexity III: Projected Subgradient Descent with η = R/(L√t) Satisfies f(average) − f(x*) ≤ RL/√tTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 3.2

Milestones

Companion: Theorem 3.9

Significance

Difficulty

Formalization scope

Selected references

A Counterexample to the Hirsch Conjecture I: A 43-Dimensional Polytope with 86 Facets Whose Diameter Exceeds 43Research Paper

Motivation

Setting

Formalization targets

Goal: Corollary 1.7

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stochastic Optimal Control: The Discrete-Time Case III: Monotone Increase Models — Accumulation Points of DP-Optimal Controls Give an Optimal Stationary PolicyTextbook

Motivation

Setting

Formalization targets

Goal: Proposition 5.11

Milestones

Significance

Difficulty

Formalization scope

Selected references

Variance-based Regularization with Convex Objectives III: Localized-Rademacher Risk Bounds for the Robust MinimizerResearch Paper

Why variance-regularized risk bounds

Setting

Formalization targets

Goal: Theorem 4, inequality (23), as its proof establishes it

Milestones

Significance

Difficulty

Formalization scope

Selected references

The irrationality measure of π is at most 14.797074 (Rhin–Viola 1993)Research Paper

Motivation

Formalization target

How the bound arises

Significance

Selected references

Air Travel Demand and Airline Seat Inventory Management II: The EMSR Protection Level for Two Nested Fare ClassesTextbook

Why airlines protect seats

Setting

Formalization targets

Goal: Eqs. (5.15)–(5.16), optimality of the EMSR protection level

Milestones

Significance

Difficulty

Formalization scope

Selected references

Tegmark 1997: On the Dimensionality of SpacetimeResearch Paper

Motivation

Setting

Formalization targets

Goal: type of the field equations as a function of (n,m)(n,m)(n,m)

Milestones (in the order of the paper)

Significance

Difficulty

Formalization scope

Goal: type of the field equations as a function of $(n,m)$