All missions

Motivation

Large games on networks arise whenever many agents interact only with their neighbors: firms in a supply network, banks linked by exposures, users of a congested service, or individuals in an epidemic. A Nash equilibrium of an $n$-player stochastic differential game with heterogeneous interactions is a fixed point over $n$ coupled control problems, and computing one is out of reach for large $n$. Mean field game theory resolves this when interactions are symmetric, by passing to a single representative player facing a population distribution. It does not apply when each player sees a different weighted, directed neighborhood.

Graphon games replace the population by a continuum of players indexed by a label $u\in[0,1]$, with interaction strengths given by a kernel $W(u,v)$. D. Lacker and A. Soret (arXiv:2204.09642) formulate stochastic graphon games in label-state form: one typical player carries a uniform random label $U$ together with its state $X$, and an equilibrium is a flow of joint laws $\mu_t=\mathcal L(U,X_t)$. This mission formalizes their approximation theorem, which says that such an equilibrium yields approximate Nash equilibria for every large network whose interaction matrices converge to $W$.

Timeline. Graphons, the limits of dense graph sequences, are surveyed by Lovász (2012). Caines and Huang (arXiv:1810.11234, 2018) introduced graphon mean field games in which each node carries a subpopulation. Carmona, Cooney, Graves and Laurière (arXiv:1910.03983) studied static graphon games, and Aurell, Carmona and Laurière (arXiv:2003.11896) the linear-quadratic stochastic case, handling a continuum of independent Brownian motions through Fubini extensions. Lacker and Soret (2022) replaced the continuum of players by one random label, which removes that measurability problem and admits unbounded, non-symmetric kernels and sparse networks.

Setting

Fix dimensions $d,d_0\ge1$, a horizon $T>0$, a compact metric action space $A$, and bounded continuous coefficients $b(t,x,a)\in\mathbb R^d$, $\sigma(t,x)\in\mathbb R^{d\times d_0}$, running reward $f(t,x,m,a)$ and terminal reward $g(x,m)$, where $m$ ranges over the finite nonnegative measures $\mathcal M_+(\mathbb R^d)$ with the weak topology. $\sigma$ is Lipschitz, $\sigma\sigma^\top\ge c\,I$ with $c>0$, and $\{(b(t,x,a),z):a\in A,\ z\le f(t,x,m,a)\}$ is convex.

$n$-player game. Player $i$ chooses a measurable feedback $\alpha_i(t,x_1,\dots,x_n)\in A$, and $dX^i_t=b(t,X^i_t,\alpha_i(t,X_t))\,dt+\sigma(t,X^i_t)\,dB^i_t$ with independent Brownian motions. A nonnegative interaction matrix $\xi^n$ with zero diagonal defines the neighborhood empirical measure $M^{n,i}_t=\frac1n\sum_j\xi^n_{ij}\delta_{X^j_t}$, and player $i$ maximizes $J_i=\mathbb E[\int_0^Tf(t,X^i_t,M^{n,i}_t,\alpha_i)\,dt+g(X^i_T,M^{n,i}_T)]$.

Kernels. A kernel is a nonnegative integrable $W$ on $[0,1]^2$, neither bounded nor symmetric in general. With $I^n_i=[(i-1)/n,i/n)$ and $I^n_n=[(n-1)/n,1]$, the step kernel of $\xi^n$ is $W_{\xi^n}=\xi^n_{ij}$ on $I^n_i\times I^n_j$. $W_{\xi^n}\to W$ in the strong operator topology if $\int_0^1|\int_0^1(W_{\xi^n}-W)(u,v)\varphi(v)\,dv|\,du\to0$ for every bounded $\varphi$. A measure $m$ on $[0,1]\times\mathbb R^d$ is mapped to $\mathsf Wm(u)=\int W(u,v)\delta_x\,m(dv,dx)$.

Graphon game. A typical player has $(U,X_0)\sim\lambda$ with $U\sim\mathrm{Unif}[0,1]$, uses $\alpha(t,U,X_t)$, and faces the measure $\mathsf W\mu_t(U)$. A flow $\mu_\cdot$ is a $W$-equilibrium with control $\alpha^*$ if $\alpha^*$ maximizes $J_W(\mu_\cdot,\alpha)=\mathbb E[\int_0^Tf(t,X_t,\mathsf W\mu_t(U),\alpha)\,dt+g(X_T,\mathsf W\mu_T(U))]$ and $\mu_t=\mathcal L(U,X^{\alpha^*}_t)$.

Errors. Player $i$ receives a label $u_i$, uses $\alpha^*(t,u_i,x_i)$ and starts from $X^i_0\sim\lambda_{u_i}$. Its error $\epsilon^n_i(u^n)$ is the largest gain from a unilateral deviation $\beta(t,x_1,\dots,x_n)$.

Formalization targets

Goal: Theorem 3.6

If $\{\lambda_u\}$ has a tight version, $W_{\xi^n}\to W$ in the strong operator topology, $\frac1{n^3}\sum_{ij}(\xi^n_{ij})^2\to0$, and $U^n_i\sim\mathrm{Unif}(I^n_i)$ are independent, then

$$\lim_{n\to\infty}\frac1n\sum_{i=1}^n\mathbb E\big[\epsilon^n_i(U^n_1,\dots,U^n_n)\big]=0.$$

Milestones

1. Lemma 4.1: continuity of $\mu\mapsto\langle\mu,h\rangle$ on measures with uniform first marginal.
2. (6.1) and (6.4): averaging over labels, and a uniform bound on $\frac1{n^2}\sum\xi^n_{ij}$.
3. Theorem 6.1: a law of large numbers for neighborhood empirical measures.
4. Remark 4.6 (4.10) and (5.1): Markovian controls achieve the relaxed value.
5. Lemma 5.1 and Lemma 7.1: optimality survives freezing the label, so deviations gain nothing against the graphon limit.
6. The tightness claim of p.34 and the decomposition (7.4).

Significance

The theorem lets one solve a single label-state equilibrium problem and use its feedback on any large network close to $W$, including sparse Erdős–Rényi graphs rescaled by $1/p_n$ and random-walk Laplacians, both covered because kernels may be unbounded. The approximation holds in an averaged sense over players and random labels, which the paper shows is the natural mode under strong operator convergence alone. Stronger modes (Theorems 3.9 and 3.13) need continuity assumptions.

The result is proved on paper. To our knowledge none of it is formalized. A formal proof requires a law of large numbers for weighted empirical measures, the equality of Markovian and relaxed values for controlled diffusions, and a tightness estimate for SDE laws. The relaxed-control layer is reusable for any mean field game formalization.

Difficulty

The obvious argument decomposes $\epsilon^n_i$ into an optimality term and two empirical-measure errors. The optimality term fails naively: the deviation $\beta$ may depend on all $n$ states, so it is not a control of the graphon game, and $\alpha^*$ is optimal only for the random label, not for each fixed label. Both gaps are closed through the relaxed formulation, (4.10) and (5.1), which is a Markovian projection theorem. The empirical-measure terms require a law of large numbers under strong operator convergence with unbounded weights, where only $\frac1{n^3}\sum(\xi^n_{ij})^2\to0$ controls the variance.

Formalization scope

States live in $\mathbb R^d$ as Fin d → ℝ, paths in $C([0,T];\mathbb R^d)$, time is $\mathbb R_{\ge0}$ read on $[0,T]$, and $\mathcal M_+$ is FiniteMeasure. Solutions of the state equations are relations: a filtered probability space, independent $\mathbb F$-Brownian motions, continuous adapted states and Itô integrals (Peng1990_SMP_Stochastic). Statements quantify over all solutions, which are unique in law under the standing assumptions. $\epsilon^n_i$ is valued in $[0,\infty]$, and $\mathbb E[\epsilon^n_i]$ is the outer integral, so that a non-measurable error cannot be read as zero. $\mathsf Wm(u)$ is set to zero on the null set of labels where its mass is infinite. The initial disintegration is a fixed Markov kernel $\kappa$ with $\lambda=\mathrm{Unif}[0,1]\otimes\kappa$.

The equilibrium hypothesis is Definition 3.1 exactly. Weakening it, for instance by requiring optimality only against deterministic initial states, would make the goal vacuous, and the formalization does not do so. Contributions are welcome on the Markovian projection, on tightness of controlled diffusions, and on weak convergence in $\mathcal P_{\mathrm{Unif}}$.

Selected references

• D. Lacker, A. Soret, A Label-State Formulation of Stochastic Graphon Games and Approximate Equilibria on Large Networks, arXiv:2204.09642v1, 2022; Mathematics of Operations Research, 2023. https://arxiv.org/abs/2204.09642
• P. E. Caines, M. Huang, Graphon Mean Field Games and the GMFG Equations, arXiv:1810.11234, 2018. https://arxiv.org/abs/1810.11234
• R. Carmona, D. Cooney, C. Graves, M. Laurière, Stochastic Graphon Games: I. The Static Case, Mathematics of Operations Research, 2022. https://arxiv.org/abs/1910.03983
• A. Aurell, R. Carmona, M. Laurière, Stochastic Graphon Games: II. The Linear-Quadratic Case, Applied Mathematics & Optimization, 2022. https://arxiv.org/abs/2003.11896
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60, 2012. https://doi.org/10.1090/coll/060

Motivation

Mean field games describe Nash equilibria of stochastic differential games with very many symmetric players, each of whom interacts with the others only through the empirical distribution of their states. The limiting model, introduced by Lasry and Lions and by Huang, Malhamé and Caines, replaces the population by a measure flow and the $N$-player equilibrium by a fixed point. Its use in economics, finance and engineering rests on one question: how close are the equilibria of the $N$-player game to the mean field equilibrium? A quantitative answer gives an error bar for every application that solves the limit instead of the finite game.

This mission formalizes the statements of J. Jackson and L. Tangpi, Quantitative Convergence for Displacement Monotone Mean Field Games with Controlled Volatility (arXiv:2304.04543v2, 2023; later in Mathematics of Operations Research, 2024). The paper proves an $O(1/N)$ rate for open-loop Nash equilibria when the volatility of the idiosyncratic and of the common noise is controlled.

Timeline.

• 2016: Lacker proves convergence of open-loop equilibria without a rate, by compactness (arXiv:1410.1324).
• 2018: Carmona and Delarue's monograph gives rates for open-loop equilibria without common noise and with uncontrolled volatility, through the stochastic maximum principle and propagation of chaos.
• 2019: Cardaliaguet, Delarue, Lasry and Lions obtain rates for closed-loop equilibria from smooth solutions of the master equation, under the Lasry–Lions monotonicity condition (arXiv:1509.02505).
• 2022: Gangbo, Mészáros, Mou and Zhang establish well-posedness of the master equation under displacement monotonicity (arXiv:2101.12362).
• 2023: Jackson and Tangpi treat open-loop equilibria under displacement monotonicity with controlled volatility and controlled common noise.

Setting

Fix a horizon $T>0$, dimensions $n,k,d$, and $m_0\in\mathcal P_2(\mathbb R^n)$, the probability measures with finite second moment $M_2(m)=\int|x|^2m(dx)$, with the Wasserstein distance $\mathcal W_2$. A probability space carries i.i.d. initial states $\xi^1,\xi^2,\dots$ with law $m_0$, a common noise $W^0$ and idiosyncratic noises $W^1,W^2,\dots$, independent $d$-dimensional Brownian motions. The data are $b:\mathbb R^n\times\mathbb R^k\times\mathcal P_2(\mathbb R^n)\to\mathbb R^n$, $\sigma,\sigma^0:\mathbb R^n\times\mathbb R^k\times\mathcal P_2(\mathbb R^n)\to\mathbb R^{n\times d}$, $L:\mathbb R^n\times\mathbb R^k\times\mathcal P_2(\mathbb R^n)\to\mathbb R$ and $G:\mathbb R^n\times\mathcal P_2(\mathbb R^n)\to\mathbb R$.

In the $N$-player game player $i$ chooses a progressive square-integrable control $\alpha^i$ with

$$dX^i_t=b(X^i_t,\alpha^i_t,m^N_{\mathbf X_t})dt+\sigma(X^i_t,\alpha^i_t,m^N_{\mathbf X_t})dW^i_t+\sigma^0(X^i_t,\alpha^i_t,m^N_{\mathbf X_t})dW^0_t,\quad X^i_0=\xi^i,$$

where $m^N_{\mathbf x}=\frac1N\sum_i\delta_{x^i}$, and minimizes $\mathbb E[\int_0^TL(X^i_t,\alpha^i_t,m^N_{\mathbf X_t})dt+G(X^i_T,m^N_{\mathbf X_T})]$. A Nash equilibrium $\boldsymbol\alpha^N$ is a tuple from which no player gains by a unilateral deviation.

In the mean field game a single player with noises $(W^1,W^0)$ faces a flow $m_t$ adapted to the common noise. A mean field equilibrium (MFE) is a pair $(m,\alpha)$ in which $\alpha$ is optimal against $m$ and $m_t=\mathcal L(X_t\mid\mathcal F^0_t)$ is the conditional law of the optimal state given the common noise. The conditionally independent copies $X^i_t=\widetilde X_t(\xi^i,W^0_{[0,t]},W^i_{[0,t]})$ of the equilibrium state run the same functional on player $i$'s own noise.

The Hamiltonian is $H(x,y,z,z^0,m)=\inf_a\{b\cdot y+\sigma\cdot z+\sigma^0\cdot z^0+L\}(x,a,m)$ with minimizer $\hat\alpha$. The central structural condition is displacement monotonicity (2.19) of $H$: for square-integrable random variables,

$$\mathbb E\big[-\Delta D_xH\cdot\Delta X+\Delta D_yH\cdot\Delta Y+\Delta D_zH\cdot\Delta Z+\Delta D_{z^0}H\cdot\Delta Z^0\big]\le-C_H\mathbb E|\Delta X|^2,$$

together with strict displacement monotonicity of $G$.

Formalization targets

Goal: Theorem 2.23

Under Assumptions 2.17, 2.19 and 2.20, for every MFE and every family of $N$-player Nash equilibria there is $C$ independent of $N$ and $i$ with

$$\mathbb E\Big[\sup_{0\le t\le T}|X^{N,i}_t-X^i_t|^2\Big]\le\frac CN,$$

and, if $\hat\alpha$ is Lipschitz with bounded Lipschitz first and second Lions derivatives, $\mathbb E\int_0^T|\alpha^i_t-\alpha^{N,i}_t|^2dt\le C/N$.

Milestones

Lemma 2.1 (the copies), Lemma 3.2 (the $N$-player maximum principle, corrected), Lemma 3.5 (the MFE maximum principle), Lemmas 3.8 and 3.10 (monotonicity projected to empirical measures), Lemma 3.11 (uniqueness for large $N$), Proposition 3.16 (the key error bound), Lemma 3.13 (a weak error estimate) and Lemma 3.12 (symmetry).

Significance

The rate $1/N$ is the rate of the law of large numbers in mean square, so the bound is of optimal order. It is a conditional propagation of chaos: given the common noise, finitely many players of the equilibrium are approximately independent, with conditional law the equilibrium flow. Controlled volatility covers models in which agents choose their exposure to risk, such as portfolio and production problems, which earlier rates excluded. The paper's results are proved on paper; none of them has a machine-checked proof. This mission produces the full statement layer: the games, the equilibrium notions, the assumptions, the two forward–backward systems and the error terms, ready for proofs of the milestones and of the goal.

Difficulty

The obvious route bounds the distance between the $N$-player and the limiting forward–backward systems by a Grönwall argument on the forward equation. It fails: the systems are fully coupled, the backward components are not controlled by the forward ones, and with controlled volatility the difference of the diffusion coefficients enters the Itô expansion. The paper instead expands $\sum_i\Delta X^i\cdot\Delta Y^i$ and uses displacement monotonicity, projected onto empirical measures, to absorb every coupled term. The remainder then consists of the errors from replacing the conditional law by the empirical measure of the copies, which need a second-order weak error estimate. Passing from a sum over players to each player needs uniqueness of the equilibrium for large $N$. In addition, Lemma 3.2 as printed omits the cross terms that appear when $b$, $\sigma$ or $\sigma^0$ depends on the measure; the milestone states the corrected system, and a proof of the goal must carry those terms, which are of order $1/N$.

Formalization scope

All games live on one probability space carrying every player; the paper's canonical spaces are an instance. Filtrations are generated by the noises and initial states (not augmented). States are progressive Itô processes with almost surely continuous paths, through the published Peng1990.SMP stochastic calculus; $\mathcal P_2$, $\mathcal W_2$ and the Lions derivative are the published DisplMonoMFG.WellPosed definitions. Matrices carry the Frobenius norm. The conditional law is encoded as a version of $\mathbb P[X_t\in\cdot\mid\mathcal F^0_t]$, and the copies are built from any measurable functional representation. Expectations of nonnegative quantities are lower Lebesgue integrals. Displacement monotonicity quantifies over couplings with finite second moments. The cost functionals are finite under the assumptions; the equilibrium definitions compare only finite costs.

The goal cannot be trivialized: the constant is chosen before $N$ and $i$, the copies share the common noise and are only conditionally independent, and (2.19) fails for $H\equiv0$ (a sanity check proves this).

A complete development needs Itô's formula for products of semimartingales, stochastic maximum principles for games, conditional laws on path space, and a weak propagation-of-chaos estimate via Lions derivatives. These pieces are reusable well beyond this paper. Contributions are welcome on any milestone, on the definition-level lemmas, and on alternative proofs.

Selected references

• J. Jackson, L. Tangpi, Quantitative Convergence for Displacement Monotone Mean Field Games with Controlled Volatility, arXiv preprint, 2023. https://arxiv.org/abs/2304.04543v2
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications I–II, Springer, 2018. https://doi.org/10.1007/978-3-319-58920-6
• D. Lacker, A general characterization of the mean field limit for stochastic differential games, Probab. Theory Relat. Fields, 2016. https://arxiv.org/abs/1410.1324
• P. Cardaliaguet, F. Delarue, J.-M. Lasry, P.-L. Lions, The Master Equation and the Convergence Problem in Mean Field Games, Annals of Mathematics Studies, 2019. https://arxiv.org/abs/1509.02505
• W. Gangbo, A. R. Mészáros, C. Mou, J. Zhang, Mean field games master equations with nonseparable Hamiltonians and displacement monotonicity, Ann. Probab., 2022. https://arxiv.org/abs/2101.12362
• J.-F. Chassagneux, L. Szpruch, A. Tse, Weak quantitative propagation of chaos via differential calculus on the space of measures, Ann. Appl. Probab., 2022. https://arxiv.org/abs/1901.02556

Motivation

Semidefinite programming (SDP) minimizes a linear function of a symmetric matrix subject to linear equations and positive semidefiniteness. It is a standard modelling tool in control, combinatorial optimization, statistics and quantum information. Interior point methods solve SDPs accurately but each iteration factorizes a dense $m\times m$ Schur complement, which limits them on large instances. Smoothing Newton methods take another route: they write the optimality conditions as a nonsmooth equation, replace the nonsmooth part by a smooth approximation controlled by a parameter $\epsilon$, and drive $\epsilon$ to zero inside a Newton iteration.

L. Liang, D. Sun and K.-C. Toh (arXiv:2303.05825v4, published in Mathematics of Operations Research, 2025) propose such a method built on the Huber function and prove that it converges globally and, under nondegeneracy conditions, superlinearly. Earlier smoothing Newton analyses for SDP were developed mainly for the Chen–Harker–Kanzow–Smale (CHKS) smoothing and mainly for the case $\tau=1$ (paper, pp.9 and 12); the regularity theory they rest on is that of Chan and Sun (doi:10.1137/060666999). The Huber smoothing coincides with the projection outside a band of width $|\epsilon|$, and the paper's algorithm allows inexact Newton solves with accuracy exponent $\tau\in(0,1]$. The convergence result is stated without strict complementarity.

Setting

Let $\mathbb S^n$ be the real symmetric $n\times n$ matrices with the trace inner product, $\mathbb S^n_+$ the positive semidefinite cone, $C\in\mathbb S^n$, $b\in\mathbb R^m$ and $\mathcal AX=(\langle A_1,X\rangle,\dots,\langle A_m,X\rangle)$ with adjoint $\mathcal A^*y=\sum_iy_iA_i$. The primal problem is $\min\{\langle C,X\rangle:\mathcal AX=b,\ X\in\mathbb S^n_+\}$. It is assumed throughout that it has an optimal solution and a Slater point $\tilde X\succ0$ with $\mathcal A\tilde X=b$. A KKT point $(X,y,Z)$ satisfies $\mathcal AX=b$, $\mathcal A^*y+Z=C$, $X,Z\succeq0$, $\langle X,Z\rangle=0$.

The Huber function is $h(\epsilon,t)=t-|\epsilon|/2$ for $t>|\epsilon|$, $t^2/(2|\epsilon|)$ for $0\le t\le|\epsilon|$, $0$ for $t<0$, and $h(0,t)=\max\{t,0\}$. For $W=P\,\mathrm{diag}(d)P^T$ it defines $\Phi(\epsilon,W)=P\,\mathrm{diag}(h(\epsilon,d_i))P^T$, so $\Phi(0,\cdot)$ is the projection onto $\mathbb S^n_+$. With constants $\kappa_p,\kappa_c>0$ the smoothed KKT map is

$$\mathcal E(\epsilon,X,y,Z)=\big(\mathcal AX+\kappa_p|\epsilon|y-b;\ -\mathcal A^*y-Z+C;\ (1+\kappa_c|\epsilon|)X-\Phi(\epsilon,X-Z)\big),\qquad\hat{\mathcal E}=(\epsilon;\mathcal E),$$

with merit function $\psi=\|\hat{\mathcal E}\|^2$, $\zeta=r\min\{1,\|\hat{\mathcal E}\|^{1+\tau}\}$ and $\eta=\min\{1,\hat r\|\hat{\mathcal E}\|^\tau\}$.

Algorithm 1 starts at $\epsilon^0=\hat\epsilon$. At an iterate with $\hat{\mathcal E}\neq0$ it takes any direction $\Delta$ with $\Delta\epsilon=-\epsilon+\zeta\hat\epsilon$ whose residual satisfies $\|\mathcal E+\mathcal E'\Delta\|\le\min\{\eta\|\mathcal E+\mathcal E'_\epsilon\Delta\epsilon\|,\hat\eta\|\hat{\mathcal E}\|\}$. It then backtracks to the smallest $\ell$ with $\psi(w+\rho^\ell\Delta)\le[1-2\sigma(1-\delta)\rho^\ell]\psi(w)$, where $\delta=\sqrt2\max\{r\hat\epsilon,\hat\eta\}<1$.

Primal constraint nondegeneracy at $\bar X$ means $\mathcal A\,\mathrm{lin}(\mathcal T_{\mathbb S^n_+}(\bar X))=\mathbb R^m$ in the coupled form (9). Dual constraint nondegeneracy at $(\bar y,\bar Z)$ means $\mathcal A^*\mathbb R^m+\mathrm{lin}(\mathcal T_{\mathbb S^n_+}(\bar Z))=\mathbb S^n$ in the form (10). Here $\mathrm{lin}(T)$ is the largest subspace contained in the tangent cone $T$.

Formalization targets

Goal: Theorem 3

For every run $\{w^k\}$ of Algorithm 1, every accumulation point $\bar w=(\bar\epsilon,\bar X,\bar y,\bar Z)$ at which primal and dual constraint nondegeneracy hold, and every admissible parameter choice:

$$w^k\to\bar w\qquad\text{and}\qquad\|w^{k+1}-\bar w\|=O\big(\|w^k-\bar w\|^{1+\tau}\big).$$

Milestones

• Proposition 1: $\Phi$ is $C^1$ for $\epsilon\neq0$ with the derivative formula (14), locally Lipschitz, and strongly semismooth.
• Lemmas 6–8 and Theorem 2: nonsingularity of $\hat{\mathcal E}'$ for $\epsilon>0$, finite line search, invariance of $\mathcal N=\{\epsilon\ge\zeta\hat\epsilon\}$, and the global convergence theorem (accumulation points solve $\hat{\mathcal E}=0$ and exist when the KKT set is nonempty and bounded).
• Lemma 4 (corrected), (17), Lemma 5 and Lemma 9: the generalized Jacobians of $\Phi$ at $\epsilon=0$.
• Theorem 1 and Lemma 2 (cited from Chan–Sun) and the uniqueness of multipliers under primal nondegeneracy (cited from Alizadeh–Haeberly–Overton).
• Proposition 2: at a zero of $\hat{\mathcal E}$, nondegeneracy is equivalent to nonsingularity of all elements of $\partial_B\hat{\mathcal E}$ and of $\partial\hat{\mathcal E}$; and the bound (42) on $\hat{\mathcal E}'^{-1}$.

Significance

The theorem gives local superlinear convergence of a smoothing Newton method for linear SDP under the two nondegeneracy conditions alone, with an inexact Newton step whose accuracy exponent $\tau$ is also the convergence order. Together with Theorem 2 it covers the whole run of the algorithm: well-definedness from any starting point, global convergence to KKT points, and the local rate. Proposition 2 characterizes nondegeneracy through the generalized Jacobian of the smoothed system, which can be used for other smoothings with the same structure.

None of these results has a machine-checked proof. The results the paper cites (Theorem 1 and Lemma 2 from Chan–Sun 2008, multiplier uniqueness from Alizadeh–Haeberly–Overton 1997) are also unformalized. The Π-analogues of Lemma 5, Lemma 9 and Lemma 1 are open goals of a separate mission on Sun's 2006 equivalence theorems for nonlinear SDP. A formal development produces reusable infrastructure: Löwner operators via the continuous functional calculus, their derivatives and semismoothness, and B-subdifferentials of spectral maps.

Difficulty

The algorithmic part (Lemmas 7–8, Theorem 2 clauses 1–3) is real analysis on a finite-dimensional space, but it needs the derivative of $\Phi$, i.e. the Daleckii–Krein formula for Löwner operators. Mathlib has the continuous functional calculus, but not its Fréchet derivative or strong semismoothness. The existence of accumulation points (clause 4) rests on a boundedness argument for perturbed projection equations from the literature on weakly univalent functions.

The local theory is harder. Proposition 2 needs an explicit description of $\partial_B\Phi(0,W)$ (Lemma 4). That description fails as printed: the sign of the $\tau$-part on $\alpha$ is coupled to the sign of the $\tau$-part of the $\beta$-block. The formal statement carries the corrected version. The cited Theorem 1 and Lemma 2 involve tangent cones of $\mathbb S^n_+$ and the curvature term $\Gamma_{\bar X}$, with no existing formal counterpart. The obvious route of quoting a general semismooth Newton convergence theorem does not apply directly: the iteration is inexact, has a line search and a moving smoothing parameter, and the unit step must be shown to be accepted eventually.

Formalization scope

$\mathbb S^n$ is the published SymMat (Fin n) (Frobenius = trace inner product). $\mathbb R^m$ is EuclideanSpace ℝ (Fin m), and all products are WithLp 2, so every norm is the Euclidean norm of the paper. $\Phi$ is cfc (huber ε) on symmetric matrices, viewed as one map on $\mathbb R\times\mathbb S^n$. $\partial_B$ and $\partial$ are the published bJac and clarkeJac, and strong semismoothness is the published uniform Definition-1 form StronglySemismoothAt11. The tangent cone is the contingent cone and $\mathrm{lin}$ is $\mathrm{span}(T\cap-T)$. $\Pi_{\mathbb S^n_+}$ in $\mathcal F$ is the metric projector.

A run of Algorithm 1 is a sequence in which every step uses some direction satisfying the inexactness test and the smallest Armijo exponent, and never meets the stopping test. Theorem 3 holds for every such run, which rules out a vacuous goal only together with Theorem 2's clause asserting that runs exist from every starting point. Convergence is Tendsto and accumulation points are MapClusterPt. The rate is $\exists C,\ \forall^{\mathrm f}k$ with a real power. The standing assumption (optimal solution plus Slater point) is an explicit hypothesis; no strict complementarity, surjectivity of $\mathcal A$ or exact Newton step is assumed.

Welcome contributions: the Fréchet derivative of $W\mapsto\mathrm{cfc}(f)(W)$ for $C^1$ functions $f$, strong semismoothness of Löwner operators of piecewise-quadratic functions, the Chan–Sun characterization (Theorem 1), and a general inexact smoothing Newton convergence lemma.

Selected references

• L. Liang, D. Sun, K.-C. Toh, A Squared Smoothing Newton Method for Semidefinite Programming, arXiv:2303.05825v4, 2024; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2303.05825
• Z. X. Chan, D. Sun, Constraint nondegeneracy, strong regularity, and nonsingularity in semidefinite programming, SIAM Journal on Optimization 19(1), 2008. https://doi.org/10.1137/060666999
• F. Alizadeh, J.-P. A. Haeberly, M. L. Overton, Complementarity and nondegeneracy in semidefinite programming, Mathematical Programming 77, 1997. https://doi.org/10.1007/BF02614438
• L. Qi, J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58, 1993. https://doi.org/10.1007/BF01581275
• D. Sun, J. Sun, Semismooth matrix-valued functions, Mathematics of Operations Research 27(1), 2002. https://doi.org/10.1287/moor.27.1.150.342

Why sequence patients by variance

In outpatient clinics, surgery blocks and other appointment systems, a provider sees $n$ clients one after another, each with a random service time. Two decisions determine how long clients wait and how long the provider sits idle: the sequence (who goes in which slot) and the schedule (how long each slot is). Finding the optimal sequence is hard even with independent service times, since it means comparing $n!$ candidates under a cost that has no closed form. The practical rule of thumb is smallest-variance-first (svf): put the least variable clients first. Numerical studies support it, and Gupta (2007) proved it optimal for two patients under a convex-order condition, but without performance guarantees for general $n$.

de Kemp, Mandjes and Olver (arXiv:1812.01467v4, Operations Research 2021) bound the approximation ratio of svf, the factor by which its cost can exceed the optimal sequence's cost. This mission formalizes their general bound: under a dilation ordering of the service times, svf with mean-based slot lengths costs at most four times the optimal sequence.

Setting

There are $n$ patients with independent real service times $B_1,\dots,B_n$ on a probability space, with finite means $\mu_j=\mathbb E B_j$ (mu). Service times may be negative (Remark 2.1 of the paper); finite variances are not needed.

A sequence is a permutation $\tau$ of the patients: $\tau(i)$ is the patient in slot $i$. A schedule $x$ reserves a slot of length $x_j$ for patient $j$. The mean-based schedule is $x=\mu$.

The waiting time $W_i$ of the patient in slot $i$ and the provider's idle time $I_i$ before slot $i$ follow the Lindley recursions (1) (lindley, wait, idle):

$$W_{i+1}=(W_i+B_{\tau(i)}-x_{\tau(i)})^+,\qquad I_{i+1}=(W_i+B_{\tau(i)}-x_{\tau(i)})^-,$$

with $W=I=0$ in the first slot. For a weight $\omega\in[0,1]$ the cost (2) (cost) is

$$C_\omega(B,\tau,x)=\omega\sum_{i=1}^n\mathbb E I_i+(1-\omega)\sum_{i=1}^n\mathbb E W_i .$$

A random variable $A$ is smaller than $B$ in the convex order, $A\le_{\rm cx}B$, if $\mathbb E\varphi(A)\le\mathbb E\varphi(B)$ for every convex $\varphi$, and in the dilation order, $A\le_{\rm dil}B$ (DilationOrder), if $A-\mathbb EA\le_{\rm cx}B-\mathbb EB$. The dilation ordering assumption (Assumption 2.4, DilationChain) is

$$B_1\le_{\rm dil}B_2\le_{\rm dil}\cdots\le_{\rm dil}B_n .$$

It implies nondecreasing variances, so svf is the identity sequence $\mathrm{id}$ under this numbering. The approximation ratio is $\varrho_\omega(B)=C_\omega(B,\mathrm{id},\mu)/\min_\tau C_\omega(B,\tau,\mu)$.

Formalization targets

Goal: Theorem 3.4

Under the dilation ordering, for every $0\le\omega\le1$ and every sequence $\tau$,

$$C_\omega(B,\mathrm{id},\mu)\ \le\ 4\,C_\omega(B,\tau,\mu),$$

that is, $\varrho_\omega\le4$.

Milestones, in the order the proof uses them

1. Eq. (3): $W_{k+1}$ is the maximum $\max\{0,S_1,\dots,S_k\}$ of the walk whose steps are the slot steps $B_{\tau(i)}-x_{\tau(i)}$ taken backwards from slot $k$.
2. Eq. (5): the session-end identity $\sum_i I_i+\sum_i B_i=\sum_{i<n}x_{\tau(i)}+W_n+B_{\tau(n)}$.
3. Convexity claim (proof of Theorem 3.4): for independent steps, $Y_i\le_{\rm cx}Z_i$ for all $i$ implies $\mathbb E\max\{0,S_1(Y),\dots\}\le\mathbb E\max\{0,S_1(Z),\dots\}$.
4. Lemma 3.5: if $\mathbb EW^{\rm svf}_{k+1}\le\varrho'\,\mathbb EW^{\rm opt'}_{k+1}$ for every slot $k$, against the best sequence keeping patients $1,\dots,k$ in the first $k$ slots, then $\varrho_\omega\le\varrho'$.
5. Eq. (9): $\mathbb EW^{\rm opt'}_{k+1}\ge\mathbb E(X_1+\cdots+X_k)^+$ with $X_j=B_j-\mu_j$.
6. Symmetrization: $X\le_{\rm cx}X-X'$ for an independent mean-zero $X'$.
7. Lemma 3.6: for independent symmetric steps, $\max\{0,S_1,\dots,S_k\}$ is stochastically dominated by $|S_k|$, so $\mathbb E\max\{0,S_1,\dots,S_k\}\le\mathbb E|S_k|$.

Milestones 3, 6 and 7 are stated for a general finite walk, which is how the proof applies them (to $X_i-X_i'$ and to $X_j$ in place of $X_i$).

Significance

The bound is a worst-case guarantee for a heuristic used in practice. It holds for every instance satisfying the ordering assumption, including exponential service times and lognormal ones with ordered log-parameters. The paper also shows that some assumption is necessary: Example 2.2 has independent symmetric service times and an unbounded ratio. Example 3.1 gives ratios above $1.52$ under the dilation ordering, so the constant cannot be pushed below that. Theorem 3.3 sharpens the constant to $2$ for symmetric service times, and Theorem 3.8 to $4(\sqrt2-1)$ for normal ones.

The result is proved in the paper; to our knowledge none of it has been machine-checked. A formal proof needs reusable infrastructure: the pathwise algebra of Lindley recursions (milestones 1, 2, 5), the comparison of expected walk maxima under the convex order (milestone 3), and a reflection inequality for symmetric random walks (milestone 7, a Lévy-type maximal inequality). Each of these is useful beyond appointment scheduling, in queueing and in stochastic comparison.

Difficulty

The cost has no closed form, and the optimal sequence is unknown. The proof avoids both: it compares svf slot by slot with the best sequence that keeps the $k$ least variable patients in the first $k$ slots (Lemma 3.5). The obvious slot-wise comparison fails for non-symmetric service times: the walk maximum of svf's centred steps is not directly comparable to $\mathbb E(X_1+\cdots+X_k)^+$. The proof first symmetrizes the steps ($X_i\le_{\rm cx}X_i-X_i'$), which costs a factor $2$, and then bounds the maximum of a symmetric walk by $\mathbb E|S_k|=2\,\mathbb E S_k^+$, another factor $2$.

The real work is Lemma 3.6. It needs a reflection argument at the first passage time of a finite walk with independent symmetric (not identically distributed) steps, for which no platform substrate exists. Milestone 3 needs a coordinatewise conditioning argument on independent families, and the transitivity of the convex order among integrable variables.

Formalization scope

• The service times are B : Fin n → Ω → ℝ on a probability space (Ω, P), measurable, integrable and independent (iIndepFun). The cost is computed from the Lindley recursion pathwise and integrated against P. It is never defined through the closed forms (3)–(5).
• Slots and patients are 0-based. Lean slot $i$ is the paper's slot $i+1$, and the initial values are $W_0=I_0=0$ (the paper's $W_1=I_1=0$, the convention under which (5) holds). The schedule is indexed by patient: slot $i$ has length x (τ i).
• The convex order is the published StochasticOrders.Convex.ConvexOrder, with test functions $\varphi$ for which $\varphi(A)$ and $\varphi(B)$ are integrable. For integrable variables this is the paper's Definition 2.3. Stochastic domination is the published StochasticOrders.Usual.UsualOrder.
• The ratio $\varrho_\omega\le4$ is stated multiplicatively for every sequence $\tau$, with no division: the minimum over $S_n$ is attained, and the case of zero minimum cost is covered. Lemma 3.5 is stated in the same way and needs $\varrho'\ge0$.
• The weight is $\omega\in[0,1]$ (the paper's $(0,1)$ with its endpoints), and the service times are only assumed integrable. Both are generalizations that specialize to the paper's setting.
• The goal is not trivial: the identity does not cost zero in general (a two-point instance gives cost $1/2$ for the swapped sequence), and both independence and the dilation chain are needed (Example 2.2).

Contributions welcome: proofs of the pathwise milestones, of the walk-maximum comparison, and of the reflection inequality, each reusable on its own.

Selected references

• M. A. de Kemp, M. Mandjes, N. Olver, Performance of the Smallest-Variance-First Rule in Appointment Sequencing, Operations Research, 2021; arXiv:1812.01467v4. https://arxiv.org/abs/1812.01467
• D. Gupta, Surgical suites' operations management, Production and Operations Management 16(6):689–700, 2007 (reference [14] of the paper).
• M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

Motivation

Firms increasingly let customers take part in designing the product they will buy: configurators, prototypes, trial versions and co-design platforms. Two features of these settings interact. The firm controls what the customer learns about the product's basic value (it can tune a trial, a simulation or a test), and the customer can invest costly engagement that raises the value of the final product. Once the customer has engaged, the firm sets the price, so the customer's investment can be held up: the firm raises the price and captures the gain.

Guo, Designing Information to Engage Customers (Management Science, 2025, doi:10.1287/mnsc.2022.03503) asks how a seller who can commit to an information structure should design it in this situation. Without engagement, the classical answer of Bayesian persuasion (Kamenica and Gentzkow 2011) for a seller who only needs to price is to reveal everything. The paper shows that engagement changes this: the seller's optimal signal can deliberately exaggerate a low prior or downplay a high one.

Setting

The state is $\omega\in\{H,L\}$ with prior $\Pr(H)=\alpha^0\in(0,1)$. The product's basic value is $\theta_H$ or $\theta_L$, the seller's cost is $c$, and

$$\theta_H>\theta_L>c\ge 0,\qquad \Theta=\theta_H-\theta_L .$$

The customer can engage, $e\in\{0,\bar e\}$, at cost $k$ when $e=\bar e$, with $\bar e>k>0$; engagement raises the value of purchase to $\theta_\omega+e-p$.

The game has four stages. (1.1) The seller commits to a binary signal $\pi=(\pi_h,\pi_l)$ with $\pi_h=\Pr(h\mid H)$, $\pi_l=\Pr(l\mid L)$, $\pi_h\ge 1-\pi_l$. (1.2) The signal is realized and both players form the posterior $\alpha_h$ or $\alpha_l$ by Bayes' rule. (2) The customer chooses $e$. (3) The seller observes $e$ and sets a price $p$. (4) The customer learns $\omega$ and buys if $\theta_\omega+e-p\ge0$.

At a common belief $\alpha$ the seller's profit is $S(\alpha,e,p)=(p-c)(\alpha\mathbf 1[p\le\theta_H+e]+(1-\alpha)\mathbf 1[p\le\theta_L+e])$. The price-cut threshold is $\alpha_e=(\theta_L+e-c)/(\theta_H+e-c)$, with $\alpha_0$ and $\alpha_{\bar e}$ at $e=0,\bar e$; further $\alpha_1=k/\Theta$ and $m=\max\{\alpha_0,\alpha_1\}$. The seller's equilibrium payoff $v^*(\alpha)$ is its payoff in the seller-preferred subgame-perfect equilibrium of stages 2–4. A design's value is $W(\pi)=\Pr(h)v^*(\alpha_h)+\Pr(l)v^*(\alpha_l)$, and the optimal value function $V^*$ is the concave closure of $v^*$: the supremum over the convex hull of its graph on $[0,1]$. The paper assumes $\alpha_1<\alpha_{\bar e}$ throughout §3.2.

Formalization targets

Goal: Proposition 1

The seller-optimal posteriors depend on $\bar e$ relative to $\alpha_0\Theta$ and $\Theta$:

$$(\alpha_l^*,\alpha_h^*)=\begin{cases} (0,1) & \bar e<\alpha_0\Theta,\\ (0,m)\ \text{if}\ \alpha^0<m;\quad (m,1)\ \text{if}\ \alpha^0>m & \alpha_0\Theta\le\bar e\le\Theta,\\ (0,m)\ \text{if}\ \alpha^0<m;\quad (\alpha^0,\alpha^0)\ \text{if}\ m<\alpha^0<\alpha_{\bar e};\quad (\alpha_{\bar e},1)\ \text{if}\ \alpha^0>\alpha_{\bar e} & \bar e>\Theta . \end{cases}$$

The goal states three parts: (a) these posteriors are optimal on the full printed ranges; (b) except at $\bar e=\alpha_0\Theta$, and at $\bar e=\Theta$ with $\alpha^0>m$, every optimal design induces them (in the middle range of the third case, every optimal design keeps both posteriors in $[m,\alpha_{\bar e}]$); (c) at $\bar e=\Theta$ the uninformative design is optimal for $m<\alpha^0\le\alpha_{\bar e}$.

Milestones

1. (5), the seller's price response: cut to $\theta_L+e$ iff $\alpha<\alpha_e$.
2. Lemma 1: the customer engages exactly for $m\le\alpha\le\alpha_{\bar e}$.
3. (6): $v^*(\alpha)=\theta_L+\bar e-c$ on $[m,\alpha_{\bar e}]$ and $\max\{\theta_L-c,\alpha(\theta_H-c)\}$ elsewhere.
4. (2)–(3): posteriors average to the prior, and every pair $a<\alpha^0<b$ is induced by the design (3).
5. (8): the optimal value is $V^*(\alpha^0)$, the least concave majorant of $v^*$, and it is attained.
6. §3.2: $V^*$ is the segment AD, the segments ABD, or the segments ABCD.

Significance

The proposition explains two kinds of deliberate misinformation by one mechanism. When the prior is low, the optimal signal reports state $H$ truthfully but sometimes sends $h$ in state $L$ ($\pi_h=1$, $\pi_l<1$): it exaggerates. When the prior is high it sometimes sends $l$ in state $H$ ($\pi_h<1$, $\pi_l=1$): it downplays. Both move the posterior into the intermediate region where the seller's price responds to engagement by less than $\bar e$, so the customer is willing to engage. The result separates this setting from the benchmark without engagement, where full information is optimal, and it identifies exactly when the benchmark answer survives ($\bar e<\alpha_0\Theta$).

The paper argues graphically and gives no appendix proof, so a formal proof makes every step explicit: the equilibrium of the subgame (including which equilibrium is meant at the boundary beliefs), the reduction from signals to posterior pairs, the concavification, and the strict comparisons behind uniqueness. The formalization also records two boundary cases, $\bar e=\alpha_0\Theta$ and $\bar e=\Theta$, where the optimal design is not unique, so the paper's tie-break selects a different design from the printed one at $\bar e=\Theta$. No part of this result has a machine-checked proof yet.

Difficulty

The equilibrium layer is a finite case analysis, but the boundary beliefs $\alpha_0$, $\alpha_1$ and $\alpha_{\bar e}$ admit several equilibria, and only the seller-preferred one reproduces Lemma 1's closed interval and (6). The concavification step needs the convex hull of the graph of a discontinuous function in $\mathbb R^2$ to be described by two-point splittings, with the supremum attained; this uses the upper semicontinuity of $v^*$. The naive argument "read the optimum off the picture" gives existence but not uniqueness. Uniqueness needs strict dominance of every other splitting, which fails exactly when $B$ lies on $AD$ ($\bar e=\alpha_0\Theta$) or $BD$ is flat ($\bar e=\Theta$).

Formalization scope

Parameters are a structure with $\theta_H>\theta_L>c\ge0$ and $\bar e>k>0$; $\alpha_1<\alpha_{\bar e}$ is a separate hypothesis. Engagement is a Boolean and strategies are pure. The subgame is an instance of the published two-stage SequentialGame with its subgame-perfect equilibrium IsSPNE, in which the seller best-responds after each engagement level, including the one not chosen. The customer buys at indifference. $v^*$ is the supremum of the seller's equilibrium payoffs, not the closed form (6), which is a milestone. Designs are pairs $(\pi_h,\pi_l)\in[0,1]^2$ with $\pi_h+\pi_l\ge1$, and the posterior after a probability-zero signal is the prior. $V^*$ uses Mathlib's convexHull and the real supremum.

Defining $v^*$ by (6), or taking the posteriors as the design variables directly, would make the statement a pure exercise about a given function and skip the game; the definitions rule this out.

A complete development needs the subgame analysis (Milestones 1–3), the Bayes-plausibility algebra (Milestone 4), a one-dimensional concavification theorem for bounded upper semicontinuous functions on $[0,1]$ (Milestone 5, reusable for any binary-state persuasion problem), and the piecewise-linear closed forms (Milestone 6). Contributions to any of these are welcome.

Selected references

• L. Guo, Designing Information to Engage Customers, Management Science, 2025. https://doi.org/10.1287/mnsc.2022.03503
• E. Kamenica and M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
• R. J. Aumann and M. Maschler, Repeated Games with Incomplete Information, MIT Press, 1995. https://mitpress.mit.edu/9780262011471/repeated-games-with-incomplete-information/

Counting Nash equilibria of bimatrix games

A bimatrix game is a two-player game in strategic form, given by two payoff matrices. Its central solution concept is Nash equilibrium, a pair of randomized strategies that are optimal against each other (Nash 1951). How many Nash equilibria a game can have matters for algorithms that find one or all of them, and for the combinatorics of the polytopes that encode the game.

Quint and Shubik conjectured that a non-degenerate $n\times n$ game has at most $2^n-1$ Nash equilibria. The bound is attained by the coordination game, in which both payoff matrices are the identity.

• 1997. Quint and Shubik state the conjecture. It is immediate for $n\le3$ from a count of polytope vertices.
• 1997–1999. The case $n=4$ is proved by Keiding and by McLennan and Park.
• 1999. von Stengel refutes the conjecture for $n\ge6$ with a $6\times6$ game with 75 equilibria, and constructs games with about $2.4^n/\sqrt n$ equilibria. The case $n=5$ stays open.
• 2025. Ickstadt, Theobald and von Stengel prove the case $n=5$.

Best-response polytopes, labels and the index

Let $(A,B)$ be a pair of real $m\times n$ matrices. A mixed strategy is a probability vector over a player's pure strategies. The game is non-degenerate if, for any mixed strategy $z$ of a player, at most $|\mathrm{supp}(z)|$ pure strategies are best responses to $z$. Up to adding a constant to the payoffs, which changes no best response, the polyhedra

$$P=\{x\in\mathbb R^m\mid x\ge0,\ B^\top x\le\mathbf 1\},\qquad Q=\{y\in\mathbb R^n\mid Ay\le\mathbf 1,\ y\ge0\}$$

are bounded, and these best-response polytopes carry the $m+n$ labels of their inequalities. A pair $(x,y)\in P\times Q$ is an equilibrium if every label is binding at $x$ or at $y$. This includes the artificial pair $(0,0)$, and every other equilibrium is a Nash equilibrium after rescaling.

A face arises by turning inequalities into equalities. A $d$-polytope is simple if every vertex lies in exactly $d$ facets, and dual-neighborly if any $\lfloor d/2\rfloor$ of its facets meet. The index of a completely labeled vertex is the sign of a determinant of facet normals, normalized so that $0$ has index $-1$. For a graph $G$, the stable-set bound $b(G)$ is twice the largest size of a pair of disjoint stable sets of equal size. $\mathcal P^d_k$ denotes the set of combinatorial types of simple $d$-polytopes with $k$ facets.

Formalization targets

Goal

The goal is Theorem 5 of the paper: for all $A,B\in\mathbb R^{5\times5}$ with $(A,B)$ non-degenerate,

$$\#\{(x,y)\mid (x,y)\text{ is a Nash equilibrium of }(A,B)\}\le 31.$$

The statement refers to no polytope. No positivity or finiteness is assumed.

Milestones

The milestones follow the paper. The polytope layer: Lemma 2 (maximal vertex numbers), Lemma 3 (non-degeneracy in polyhedral form) and Lemma 4 (from polytopes back to games). The index layer: Theorems 1 and 2 (parity and index on labeled polytopes) and Lemma 5 (adjacent equilibrium vertices have opposite index). The stable-set bounds:

$$\#\{\text{equilibria}\}\le 2|S_1|$$

for a maximal stable pair of the graph of $P$ (Theorem 3), with a version for facets (Theorem 4). The case analysis: Theorem 6 (dual-neighborly case), the tables (8) and (9) of pairs $(V,b)$ for $\mathcal P^4_8,\dots,\mathcal P^4_5$, Theorem 7 (facts on $\mathcal P^4_9$) and Lemmas 7, 8, 9.

What the result gives

Theorem 5 completes the answer to the Quint–Shubik question: the bound $2^n-1$ holds exactly for $n\le5$. The stable-set bound of Theorem 3 is a new obstruction, usable for other game sizes, that strengthens the parity argument of Lemke and Howson through the index of Shapley (1974).

The paper's proof is mathematically complete but rests on computer calculations over published lists of polytopes: the 159,375 dual-neighborly types of Firsching (2017) for Theorem 6, the 1,142 types of $\mathcal P^4_9$ for Theorem 7, and tables (8) and (9). No machine-checked proof of these results has been located. The mission records these inputs as precise statements and asks for proofs. A complete formal proof would also certify the computational classification on which the paper depends, and the polytope layer is usable well beyond this result.

The central difficulty

The obvious approach counts vertices. It is not enough: a simple 5-polytope with 10 facets can have 42 vertices, and a non-neighborly one up to 40, while the target is 32 equilibria. The two disjoint facets of a non-neighborly polytope are 4-polytopes, each carrying at most 16 equilibria, but equilibria may also have vertices on neither facet. So each equilibrium has to be traced through both polytopes at once.

For Lean, the main obstacle is that the classification statements have no short human proof. Displays (8) and (9) and Theorems 6 and 7 are finite facts about all combinatorial types, and no list of the types is in Mathlib. A proof needs either a verified enumeration or a new argument.

Formalization scope

Polyhedra are finite systems $Cz\le q$ in $\mathbb R^N$, and every notion is defined for a face of a system, so a facet of $P$ is a polytope without a change of coordinates. Faces are nonempty, dimension is that of the affine hull, and facets satisfy $\dim G+1=\dim F$. Combinatorial type is an order isomorphism of face posets. Labels of $[m+n]$ are Fin m ⊕ Fin n, and the label of a row is the row index. "Equilibria" counts $(0,0)$; "Nash equilibria", the published IsNE, does not. Counts use Set.encard, so finiteness is part of each claim. "At least $t$ obstruction vertices" is $t+b\le V$, as on p.16 of the paper.

Non-degeneracy ranges over all mixed strategies of both players, and it fails for the zero game, so the goal cannot hold vacuously. The stable-set bound is pinned down by proved checks on the triangle and the 4-cycle, and the face encoding by the unit square.

Theorems 1, 2 and 3 add $d\ge1$, $d\ge1$ and $m\ge1$, because the printed statements fail for the zero-dimensional polytope and the $0\times0$ game.

A complete development needs Lemke–Howson paths on simple polytopes, the sign of a determinant along an edge, the face lattice of a simple polytope, the upper bound theorem, and the enumerations. All of these are reusable. Contributions to any layer are welcome, including independent proofs of the tables and of the classification.

Selected references

• C. Ickstadt, T. Theobald, B. von Stengel, A stable-set bound and maximal numbers of Nash equilibria in bimatrix games, arXiv:2411.12385v3, 2025. https://arxiv.org/abs/2411.12385v3
• T. Quint, M. Shubik, A theorem on the number of Nash equilibria in a bimatrix game, Int. J. Game Theory 26, 1997. https://doi.org/10.1007/BF01263276
• H. Keiding, On the maximal number of Nash equilibria in an $n\times n$ bimatrix game, Games Econ. Behav. 21, 1997. https://doi.org/10.1006/game.1997.0531
• A. McLennan, I.-U. Park, Generic $4\times4$ two person games have at most 15 Nash equilibria, Games Econ. Behav. 26, 1999. https://doi.org/10.1006/game.1998.0640
• B. von Stengel, New maximal numbers of equilibria in bimatrix games, Discrete Comput. Geom. 21, 1999. https://doi.org/10.1007/PL00009438
• L. Shapley, A note on the Lemke–Howson algorithm, Math. Programming Study 1, 1974. https://doi.org/10.1007/BFb0121248
• M. Firsching, Realizability and inscribability for simplicial polytopes via nonlinear optimization, Math. Program. 166, 2017. https://doi.org/10.1007/s10107-017-1120-0

Motivation

A sweeping process is the evolution of a point that is pushed by a moving set: given a set-valued map $S:\mathbb R\rightrightarrows\mathbb R^n$, an orbit $\gamma$ stays in $S(t)$ and moves only along inner normals of $S(t)$. J.-J. Moreau introduced the model in the 1970s for elastoplasticity and unilateral mechanics, and it is now a standard object of nonsmooth dynamics, with applications to crowd motion, hysteresis and electrical circuits. A natural question is when every orbit started near a given time has finite length, uniformly.

For gradient flows the answer is the Kurdyka–Łojasiewicz (KL) inequality. Bolte, Daniilidis, Ley and Mazet (Trans. AMS 2010) proved that, for a $C^2$ convex coercive function with an upper-isolated critical value, the KL inequality holds if and only if the lengths of subgradient curves are uniformly controlled, if and only if the "talweg" $r\mapsto\sup_{f(x)=r}1/\|\nabla f(x)\|$ is integrable. Daniilidis and Drusvyatskiy (Sweeping by a tame process, Ann. Inst. Fourier 67 (2017), 2201–2223) showed that a sweeping process with a definable (o-minimal) bounded graph can always be desingularized by a change of time.

Daniilidis and Tapia-García (arXiv:2110.08686v1, published as Oriented Calmness and Sweeping Process Dynamics, Math. Oper. Res. 2024) drop o-minimality and prove a characterization in the spirit of the KL theory for sweeping processes with a smooth graph. The key new object is an oriented modulus of the coderivative, which sees only the direction in which the sets recede.

Setting

Write $\mathcal S=\operatorname{gph}S=\{(t,x)\in\mathbb R\times\mathbb R^n:x\in S(t)\}$ and $\operatorname{dom}(S)=\{t:S(t)\neq\emptyset\}$. For a set $C$, $N_C(x)$ is the limiting normal cone: the limits of Fréchet normals $v_i\in\hat N_C(x_i)$ with $x_i\to x$ in $C$, where $\hat N_C(x)$ consists of the $v$ with $\limsup_{y\to x,\,y\in C}\langle v,y-x\rangle/\|y-x\|\le0$.

• An orbit on an interval $I$ is an absolutely continuous $\gamma$ with $\gamma(t)\in S(t)$ for all $t\in I$ and $-\dot\gamma(t)\in N_{S(t)}(\gamma(t))$ for almost every $t$; $\mathcal{AC}(S,I)$ is the set of orbits, and $\mathcal{PAC}(S,I)$ the set of piecewise absolutely continuous orbits, whose jumps lie in a closed countable set. The length is $\ell(\gamma)=\int_I\|\dot\gamma\|$.
• The coderivative is $D^*S(t,x)(u)=\{a\in\mathbb R:(a,-u)\in N_{\mathcal S}(t,x)\}$, and the oriented modulus is

$$\|D^*S(t,x)|^+=\sup\{a^+:a\in D^*S(t,x)(u),\ \|u\|\le1\},\qquad \sup\emptyset=0.$$

• The oriented talweg is $\varphi^\uparrow(t)=\sup_{x\in S(t)}\|D^*S(t,x)|^+$.
• $S$ is a smooth sweeping process if $\mathcal S$ is closed and connected and either a $C^1$ submanifold of $\mathbb R^{n+1}$ of dimension at most $n$, or a full-dimensional region whose boundary $\partial\mathcal S$ is a $C^1$ hypersurface.
• With $T=\sup\operatorname{dom}(S)$ and $H_S(t)=\partial\mathcal S\cap(\{t\}\times\mathbb R^n)$: (A1) from every $(t,x)\in\mathcal S$ with finite oriented modulus some orbit starts; (A2) at $\bar t<T$, $\varphi^\uparrow<\infty$ on some $(\bar t,\bar t+\delta)$; (A3) at $\bar t<T$, $H_S$ is Pompeiu–Hausdorff continuous on some $(\bar t,\bar t+\delta)$. $\mathcal T$ is the set of $t\in\operatorname{dom}(S)$ where (A2) and (A3) hold.

Formalization targets

Goal: Theorem A (pp.9–10)

For a smooth sweeping process with bounded values satisfying (A1), and $a\in\mathcal T$, the following are equivalent:

• a) there are $b>a$, $\rho>0$ and an increasing homeomorphism $\Psi:[0,\rho]\to[a,b]$, $C^1$ with $\Psi'>0$ on $(0,\rho)$, such that $\|D^*(S\circ\Psi)(r,x)|^+\le1$ for all $r\in(0,\rho)$, $x\in S(\Psi(r))$;
• b) there are $b>a$ and an increasing continuous $\sigma$ with $\sigma(a)=0$ and $\ell(\gamma)\le\sigma(t_2)-\sigma(t_1)$ for all $a\le t_1<t_2\le b$, $\gamma\in\mathcal{AC}(S,[t_1,t_2])$;
• c) there are $b>a$ and $M>0$ with $\ell(\gamma)\le M$ for every $b'\in(a,b]$ and $\gamma\in\mathcal{PAC}(S,[a,b'])$;
• d) there is $b>a$ with

$$\int_a^b\varphi^\uparrow(t)\,dt<\infty.$$

Clause c) is stated in a corrected form. The paper quantifies only over $\mathcal{PAC}(S,[a,b])$ for one $b$, and that class can be empty for large $b$ while d) fails; the goal's item lists a counterexample. The corrected clause is what the paper's proof uses.

Milestones

Lemma 15 (continuity of both moduli on $\partial\mathcal S$), Lemma 16 (continuity of the talwegs), Proposition 17 (time rescaling of orbits), Proposition 18 a)–c) (geometric facts at boundary points), Lemma 19 ($\|\dot\gamma(t)\|=\|D^*S(t,\gamma(t))|^+$), Proposition 20 (concatenation into piecewise orbits), and the exact chain rule $\|D^*(S\circ\Psi)(r,x)|^+=\Psi'(r)\|D^*S(\Psi(r),x)|^+$ behind the last display of the proof (p.15).

Significance

Theorem A reduces a dynamic property (all orbits near $a$ have controlled length) to a static one (integrability of a function computed from normal cones of the graph), and both to the existence of a desingularizing change of time. It extends the Bolte–Daniilidis–Ley–Mazet characterization from gradient curves to sweeping processes, and the o-minimal desingularization of Daniilidis–Drusvyatskiy to non-definable maps with smooth graph. The companion Theorem B adds discrete versions (catching-up algorithms) and is not part of this mission.

The result is proved on paper. As far as is known, no part of it, and no sweeping-process theory at all, has been formalized. The mission produces Lean statements of the paper's definitions (oriented modulus, talweg, smooth sweeping process, orbits and piecewise orbits) and of each step of the proof, so the whole argument can be checked.

Difficulty

The equivalence chains through four different arguments. a) ⇒ b) needs that the speed of an orbit equals the oriented modulus (Lemma 19), which rests on a normal-cone calculus rule for $\{t\}\times S(t)=\mathcal S\cap(\{t\}\times\mathbb R^n)$ and on the tangent geometry of $\partial\mathcal S$; the qualification condition in that rule fails exactly where the modulus is infinite. c) ⇒ d) builds orbits whose speed nearly attains $\varphi^\uparrow$, which needs continuity of $\varphi^\uparrow$ (from the Hausdorff continuity of the boundary slices) and a transfinite gluing of local orbits into one piecewise orbit (Proposition 20). d) ⇒ a) needs the chain rule for the coderivative under a $C^1$ change of time.

The obvious attempt, bounding lengths by $\int\varphi^\uparrow$ directly through Lemma 19, does not give c) ⇒ d): the bound goes the wrong way, and one must exhibit long orbits, not bound short ones.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\mathbb R^{n+1}$ is $\mathbb R\times\mathbb R^n$ with time first (max norm; normal cones and Hausdorff continuity do not depend on the choice of equivalent norm).
• Normal cones and the coderivative are the published platform definitions GenNewtonSubgrad.ProxReg.{gph, limNormal, coderiv} and StrictCQ.CAKKT.limNormal.
• Moduli, talwegs, lengths and the integral of d) take values in $[0,+\infty]$; $a^+$ is ENNReal.ofReal a, empty suprema are $0$, so a real-valued supremum never returns a junk value.
• Absolute continuity on a non-compact interval is absolute continuity on its compact subintervals; length is $\int\|\gamma'\|$, never the variation (jumps of a piecewise orbit do not count).
• Definition 10 is encoded by local $C^1$ defining functions (a submersion for a submanifold, a function with nonvanishing derivative and $\mathcal S=\{g\le0\}$ near the boundary).

A trivializing formalization is excluded: verification files check that the smoothness predicate is satisfiable, that constant curves are orbits of length $0$, that every orbit is a piecewise orbit, and that the oriented modulus vanishes at interior points of the graph.

Reusable beyond this mission: the oriented modulus and talweg, the orbit classes and the length functional, and the chain rule for a $C^1$ change of time. Proofs of any milestone are welcome; the normal-cone facts for $C^1$ manifolds with boundary are the main missing infrastructure.

Selected references

• A. Daniilidis, S. Tapia-García, Desingularization of the Sweeping Process Mapping, arXiv:2110.08686v1, 2021; published as Oriented Calmness and Sweeping Process Dynamics, Math. Oper. Res., 2024. https://arxiv.org/abs/2110.08686, https://doi.org/10.1287/moor.2021.0269
• J. Bolte, A. Daniilidis, O. Ley, L. Mazet, Characterizations of Łojasiewicz inequalities: subgradient flows, talweg, convexity, Trans. Amer. Math. Soc. 362 (2010), 3319–3363. https://doi.org/10.1090/S0002-9947-09-05048-X
• A. Daniilidis, D. Drusvyatskiy, Sweeping by a tame process, Ann. Inst. Fourier 67 (2017), 2201–2223 (reference [9] of the paper).
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3