Motivation

Mission III of this series ends at an impossibility: without money, incentive compatibility over three or more alternatives means dictatorship. This mission formalizes the classical escape route — quasilinear utilities and payments — and the exact price of it. Vickrey (1961) discovered that a second-price auction makes truth-telling dominant; Clarke (1971) and Groves (1973) generalized the idea to arbitrary social choice: welfare-maximizing rules can always be made truthful by the right payments. The converse program — which choice rules are implementable at all — runs through Rochet (1987) and Myerson (1981) to Saks–Yu (2005): weak monotonicity characterizes implementability on convex domains, and on single-parameter domains the characterization is complete and elementary — monotone rules with critical-value payments. Chapter 9, §§9.3 and 9.5 of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007), written by Nisan, is the source text.

Setting

A set $A$ of alternatives and a finite set $\iota$ of players. Player $i$ holds a private valuation $v_i : A \to \mathbb{R}$ from a publicly known domain $V_i \subseteq \mathbb{R}^A$; utilities are quasilinear: choosing $a$ and charging $p_i$ gives $i$ utility $v_i(a) - p_i$. A (direct revelation) mechanism is a social choice function $f$ from valuation profiles to $A$ together with payment functions $p_i$ (Definition 9.14). The mechanism is incentive compatible if no unilateral misreport from the domain ever beats the truth (Definition 9.15).

A VCG mechanism (Definition 9.16) has $f$ maximizing social welfare $\sum_i v_i(a)$ and payments of the Groves form $p_i = h_i(v_{-i}) - \sum_{j\ne i} v_j(f(v))$; the Clarke pivot rule takes $h_i(v_{-i}) = \max_b \sum_{j \ne i} v_j(b)$. A rule is weakly monotone (Definition 9.28) if a unilateral change of valuation that moves the outcome from $a$ to $b$ satisfies $v_i'(b) - v_i'(a) \ge v_i(b) - v_i(a)$. A single-parameter domain (Definition 9.33) is given by a win set $W_i \subseteq A$ per player and bids $t \in [t_0, t_1]$: the valuation is $t$ on $W_i$ and $0$ elsewhere.

Formalization targets

Goal (capstone) — Theorem 9.36

A normalized mechanism (losers pay 0) on a single-parameter domain is incentive compatible iff the rule is monotone and every winning bid pays the critical value — the threshold below which the bid loses.

Theorem 9.17 — VCG is truthful

Every VCG mechanism is incentive compatible.

Lemma 9.20 — Clarke pivot

With Clarke pivot payments, a welfare-maximizing rule makes no positive transfers, and is individually rational when valuations are nonnegative.

Theorem 9.29 — weak monotonicity

Necessity: incentive compatibility forces WMON, on any domain. Sufficiency: on convex domains, WMON rules admit implementing payments (Saks–Yu).

Significance

These are the working theorems of every later mechanism-design mission: the approximation mechanisms of Chapter 12, the profit-maximization results of Chapter 13, and the sponsored-search analysis of Chapter 28 all argue through Theorem 9.36's monotonicity-plus-critical-value normal form, and VCG is the benchmark they approximate. Formalizing the cluster produces the platform's quasilinear-mechanism vocabulary — domains, truthfulness, Groves payments, weak monotonicity, single-parameter settings — on top of the social-choice layer of Mission III.

The capstone and Theorem 9.17 are textbook results with complete proofs in the source; the Saks–Yu half of Theorem 9.29 is stated but not proved in the book ("quite involved"), so that milestone carries a genuinely hard formalization with a published paper proof. None have prior Lean formalizations.

Difficulty

Theorem 9.17 is a three-line inequality chase once the Groves form is unfolded — a deliberate warm-up. Lemma 9.20 adds the attained maximum over a finite alternative set. The necessity half of 9.29 is a two-application argument; the sufficiency half is the hard point of the mission: the known proofs walk two-cycle inequalities into a path-integral construction of payments on a convex domain, and nothing of the kind exists in Mathlib. For the capstone, the delicate part is the critical value: the book defines it as a supremum that "is undefined" when the player always wins, and the honest formal rendering — a constant payment c that is a least upper bound of the losing bids whenever losing bids exist — makes the case split explicit; the equivalence proof must thread monotonicity, the threshold structure of the winning set, and normalization through both directions.

Formalization scope

Valuations are functions A → ℝ; domains are sets V i : Set (A → ℝ); mechanisms are total functions with every property quantified only over profiles from the domain, so behavior on invalid inputs carries no content. The Groves term hᵢ is a function of the full profile constrained to be invariant under changes of coordinate i — the standard rendering of "depends only on $v_{-i}$". The Clarke payment uses a Finset.sup' over a finite nonempty A, so no junk supremum arises. In the single-parameter setting the valuation induced by a bid is Set.indicator, bids live in Set.Icc t0 t1 with t0 ≤ t1, and the critical value is characterized by IsLUB guarded by nonemptiness of the losing set — the book's "undefined" caveat made precise without a junk sSup. Weak monotonicity's sufficiency half carries Convex ℝ (V i) and finite A (the Saks–Yu setting); the necessity half deliberately carries no hypotheses beyond incentive compatibility itself.

Selected references

• W. Vickrey, Counterspeculation, auctions, and competitive sealed tenders, J. Finance 16 (1961), 8–37. DOI
• E. H. Clarke, Multipart pricing of public goods, Public Choice 11 (1971), 17–33. DOI
• T. Groves, Incentives in teams, Econometrica 41 (1973), 617–631. DOI
• M. Saks, L. Yu, Weak monotonicity suffices for truthfulness on convex domains, Proc. 6th ACM EC (2005), 286–293. DOI
• N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 9, §§9.3, 9.5. DOI

Motivation

Infinite-horizon dynamic programming is the mathematical core of Markov decision processes and reinforcement learning: Bellman equations, value iteration, policy iteration, and their guarantees. Chapter 7 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) develops the finite-state theory in its cleanest generality — stochastic shortest path (SSP) problems first (Prop. 7.2.1–7.2.2), with discounted problems (Prop. 7.3.1) and average-cost problems (Prop. 7.4.1–7.4.2) derived from the SSP analysis. These propositions are cited throughout the MDP/RL literature as the base case of the theory; none of them exists in Mathlib.

Setting

States $1, \dots, n$ plus an implicit cost-free absorbing termination state $t$; finite nonempty control sets $U(i)$; costs $g(i,u)$; sub-stochastic transitions $p_{ij}(u) \ge 0$, $\sum_j p_{ij}(u) \le 1$, the deficit being the termination probability (BertsekasSSPModel). Operators

(BertsekasSSPPolicyOp, BertsekasSSPBellmanOp), $N$-stage costs by backward recursion with policy shift (BertsekasSSPNCost), and the survival mass $P\{x_m \ne t\}$ (BertsekasSSPSurvival). Assumption 7.2.1: for some $m > 0$, every admissible policy has survival mass $< 1$ from every state after $m$ stages. The discounted setting reuses the same model with stochastic rows and $0 < \alpha < 1$ (BertsekasDiscounted*); the average-cost setting adds a designated state $s$ with the avoidance probability of Assumption 7.4.1 (BertsekasSSPAvoidProb).

Target

Under Assumption 7.2.1, there is a vector $J^*$ with

and a stationary policy attaining $J^*$ — BertsekasDP.ssp_main_theorem (goal, Prop. 7.2.1(a),(b)). Milestones: 7.2.1(c) policy evaluation, 7.2.1(d) optimality iff greediness, 7.2.2 policy iteration, 7.3.1 the full discounted counterpart, 7.4.1 the average-cost Bellman equation, 7.4.2 average-cost policy iteration.

Significance

These are the convergence guarantees behind value iteration and policy iteration — the two algorithms at the root of dynamic programming practice and of RL analyses (Q-learning's target operator is exactly $T$). The SSP form is the strongest of the three: the discounted theory is its special case (termination with probability $1 - \alpha$ per stage) and the average-cost theory reduces to it through cycles at the recurrent state. Formalized, the chapter yields a reusable finite-MDP theory: monotone operators, $m$-stage contractions, and the machinery for later Vol. II material. All results are proved in the book; the formalization is new.

Difficulty

$T$ is not a one-stage contraction in the sup-norm under Assumption 7.2.1 — only an $m$-stage contraction, uniformly over the finitely many $m$-stage policy prefixes; extracting the uniform contraction factor $\rho < 1$ (via finiteness of the policy space) is the crux of the whole chapter. The limit of $N$-stage costs for nonstationary policies must be established, not assumed (tail-sum estimate $\rho^{\lfloor N/m \rfloor}$). For the average-cost results the associated-SSP construction (stop on reaching $s$) must be built inside the proof. The liminf phrasing of average-cost optimality is deliberate: for arbitrary nonstationary policies the Cesàro limit need not exist.

Formalization scope

Finite states Fin n, finite control type, constraint sets as Finsets with attained minima; no termination state in the carrier — termination is the sub-stochastic deficit, exactly as the book treats it computationally. Policies are sequences of stage policies (Markov); costs of nonstationary policies via the shift recursion. Convergence is Tendsto in the product topology (equivalently sup-norm, $n$ finite). Average cost uses real liminf and division with the $N = 0$ term junk-valued at 0 (irrelevant at infinity). The discounted theorem packages parts (a)–(e) in one statement mirroring Prop. 7.3.1.

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (§7.1–7.4.) http://www.athenasc.com/dpbook.html
• D. P. Bertsekas, J. N. Tsitsiklis, An analysis of stochastic shortest path problems, Math. Oper. Res. 16 (1991), 580–595. https://doi.org/10.1287/moor.16.3.580
• M. L. Puterman, Markov Decision Processes, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Invertible modules over a commutative semiring are Zariski-locally free, so local semirings have trivial Picard group. The source asks whether the ring-theoretic semilocal conclusion survives without subtraction: must every invertible module over a semiring with finitely many maximal ideals be free? If not, is the conclusion at least true for finite semirings?

This mission turns CUHK-Shenzhen AI Math Problem 19, Picard groups of semi-local or finite semirings, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.

Setting

The main theorem asserts freeness for every invertible module over a commutative semiring with finite maximal spectrum. A separate milestone states the finite-semiring fallback. Both are positive formulations; a concrete counterexample to either resolves that target negatively and should motivate a corrected classification.

Significance

Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in semirings, Picard groups, invertible modules, finite semirings. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.

Difficulty

Ring proofs use subtraction-sensitive k-ideal properties and decompositions into local factors that can fail for semirings. Finite indecomposable semirings need not be local and may have positive Krull dimension. Invertible modules are projective with strong duality, but familiar rank and determinant arguments may not survive additive noncancellation.

Suggested attack route

Formalize the known local-freeness proof from the evaluation isomorphism and study patching over finitely many principal opens. Identify exactly where partitions of unity require k-ideals. For finite semirings, enumerate idempotent matrices representing projective modules, impose the invertibility constraints, and seek either a reduction to principal rank-one modules or a minimal counterexample. Product decompositions and faithful-action lemmas should be reusable.

Formalization scope

The Lean targets use Mathlib's commutative semiring, maximal spectrum, module, invertible-module, and free-module notions. 'Semilocal' is encoded only as finiteness of MaximalSpectrum; no unproved decomposition theorem is assumed. The finite fallback assumes the underlying semiring type is finite but does not assume the module itself finite separately. Cardinality-only variants from the source are not the capstone.

The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.

Milestones

Resolve the finite-semiring statement, computationally or structurally, while developing the local-to-semilocal patching lemmas needed by the main theorem.

The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.

Timeline and literature status

The CUHK-Shenzhen AI Math Problems page added this problem on June 24, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.

Acceptance criteria

A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no sorry, and expose a top-level theorem solution when submitted to Prove2Me.

The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.

Formal verification policy

The files were built locally with Lean 4.30.0 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.

Selected references

• Original problem
• Facets of Module Theory over Semirings
• MathOverflow discussion

Motivation

Linear approximation is only one instance of distance minimization. Feasible sets in optimization are typically convex rather than subspaces, so a useful certificate must compare a target point with an entire convex set and must allow an affine offset. Chapter 5 of Luenberger's Optimization by Vector Space Methods builds this certificate through geometric forms of the Hahn--Banach theorem, supporting hyperplanes, and separation of convex sets. The resulting minimum-distance theorem expresses the distance from a point to a convex set as an optimal gap measured by a norm-bounded continuous linear functional (Luenberger, §§5.12--5.13, pp. 130--137).

This mission advances the series from subspace annihilators to affine separation. It formalizes the Minkowski gauge used by the chapter, three progressively stronger separation statements, and a capstone distance-duality certificate. These results are standard infrastructure for constrained optimization: they turn a geometric exclusion or distance into a scalar inequality that can later become a multiplier or a dual bound.

Setting

Let $X$ be a real normed space and $K\subseteq X$ a nonempty convex set. Convexity is represented by Convex ℝ K, and topological interior, closure, and infimum distance use Mathlib's interior, closure, and Metric.infDist. A continuous affine separator is described by a continuous linear functional $f:X\toL[\mathbb R]\mathbb R$ and a scalar level $c$. The inequality $f(k)\le c$ for all $k\in K$ places $K$ in one closed half-space.

When a convex set contains zero in its interior, its Minkowski gauge is the functional gauge K. The source characterizes it by nonnegativity, positive homogeneity, subadditivity, continuity, and the level sets

These properties are bundled into the first milestone, following Lemma 1 of §5.12 (pp. 131--132).

For two convex sets $K_1,K_2$, Eidelheit separation means finding nonzero $f$ and $c$ with $f(x)\le c\le f(y)$ for $x\in K_1$ and $y\in K_2$. The source assumes that $K_1$ has nonempty interior and that its interior does not meet $K_2$. The Lean statement records the nonemptiness of $K_2$ explicitly, since otherwise nonzero separation is not forced.

Formalization targets

Gauge and geometric Hahn--Banach milestones

Formalize the six gauge properties above. Then, for a convex $K$ with nonempty interior and an affine subspace $V$ disjoint from that interior, produce $f\ne0$ and $c$ such that

This is Mazur's geometric Hahn--Banach theorem as stated in §5.12, Theorem 1 (p. 133).

Supporting hyperplanes and convex-set separation

For $x\notin\operatorname{int}K$, formalize a nonzero functional satisfying $f(k)\le f(x)$ for all $k\in K$. Next formalize Eidelheit separation:

These are Theorems 2 and 3 of §5.12 (pp. 133--134).

Convex minimum-distance duality

Let $x_1$ have positive distance $d$ from $K$. Produce $f$ and a real upper-bound level $c$ with $\|f\|\le1$, $f(k)\le c$ on $K$, and

Every other feasible pair $(g,b)$ must satisfy $g(x_1)-b\le d$. If $x_0\in K$ realizes the distance, require $-f$ to align with $x_0-x_1$. This is the finite real certificate form of §5.13, Theorem 1 (pp. 136--137).

Significance

The capstone is an exact strong-duality statement for distance to a convex set. A feasible pair $(g,b)$ yields a certified lower bound on the distance, and the distinguished pair reaches the primal value. Unlike a nearest-point characterization, it remains meaningful when $K$ is not closed and no minimizing point exists. The conditional alignment clause identifies the equality case when attainment is available.

Formalizing the chapter's progression creates more than one isolated equality. The gauge package links convex geometry to sublinear analysis; Mazur separation handles affine constraints; the supporting-hyperplane and Eidelheit statements provide reusable interfaces for later multiplier rules. The results are known and proved in the 1969 text; the mission's contribution is a coherent machine-checked Lean layer that preserves the source hypotheses and can support later chapters on duality and optimization.

Difficulty

A direct reuse of subspace distance duality is insufficient because a general convex set is neither closed under subtraction nor described by an annihilator. An affine level $c$ is unavoidable. The common shorthand $\sup_{k\in K} f(k)$ introduces a second problem: $K$ need not be bounded, so a real-valued supremum is not available for an arbitrary functional. The capstone therefore quantifies over a real upper bound $c$ and asserts its optimality through a universal inequality; this records the same finite support value without imposing boundedness absent from the source.

Topological hypotheses also differ across the milestones. Separation uses nonempty interior, whereas the final distance theorem only assumes convexity, nonemptiness, and positive distance. Replacing positive distance by mere exclusion $x_1\notin K$ would be invalid for a nonclosed set. Similarly, requiring closure or compactness would make formalization easier but would lose the theorem's intended infinite-dimensional scope.

Formalization scope

The mission is restricted to real normed spaces. Sets use Set X; affine varieties use AffineSubspace ℝ X; separators use ContinuousLinearMap. The gauge is Mathlib's existing gauge, so no competing definition is introduced. The bundled gauge milestone deliberately includes both level-set identities as well as continuity, positive homogeneity for positive real scalars, subadditivity, and nonnegativity.

The Eidelheit theorem includes K₂.Nonempty, an assumption used implicitly by the source's separating conclusion. The capstone includes K.Nonempty and 0 < Metric.infDist x₁ K; it does not assume closedness, boundedness, compactness, or attainment. Its pair $(f,c)$ represents a finite support level, and the universal comparison over all feasible $(g,b)$ rules out a weakened statement in which an arbitrarily loose upper bound could trivialize existence. The optional nearest-point clause uses the exact equality $\|x_0-x_1\|=d$ and fixes the sign of alignment. Contributions may add reusable lemmas on gauges, interiors, affine subspaces, or support bounds, but the public results should remain independent of finite-dimensionality and completeness.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, Chapter 5, §§5.11--5.13, pp. 127--137. Public scan.

Motivation

Many convex programs impose inequalities valued in a vector space: componentwise inequalities, positive-semidefinite constraints, and families of ordered resource constraints are all instances of one cone order. Chapter 8 of David G. Luenberger's Optimization by Vector Space Methods develops a global theory for this setting. A perturbation of the constraint produces a convex value function, continuous linear functionals positive on the ordering cone become Lagrange multipliers, and a strict-feasibility condition yields an attained dual optimum. This mission formalizes the progression in §§8.2–8.6, culminating in the book's Lagrange Duality Theorem.

Setting

Let $X$ and $Z$ be real normed spaces, let $\Omega\subseteq X$ be a nonempty convex set, and let $P\subseteq Z$ be a convex cone. The cone induces the relation

A continuous linear functional $z^*\in Z^*$ is dual-positive when $z^*(p)\ge0$ for every $p\in P$. A map $G:X\to Z$ is cone-convex on $\Omega$ when its value at a convex combination is below the corresponding convex combination of its values in this cone order. The primal program is

where $f$ is real-valued and convex on $\Omega$.

For a multiplier $z^*$, the Lagrangian and its possibly infinite dual value are

The perturbed primal value $\omega(z)$ replaces the zero right-hand side by $G(x)\le_P z$. Lean represents $\omega$ and $\phi$ in EReal, so infeasible perturbations have value $+\infty$ and objectives unbounded below can have value $-\infty$ without arbitrary defaults.

Formalization targets

Main goal: Lagrange duality

Assume $P$ has nonempty interior, the primal value $\mu$ is finite, and there is a strictly feasible point $x_s\in\Omega$ with

Prove that a dual-positive $z_0^*$ exists and attains

If $x_0$ attains the primal infimum, also prove complementarity $z_0^*(G(x_0))=0$ and that $x_0$ minimizes $L(\,·\,,z_0^*)$ over $\Omega$.

Milestones

Five source milestones delimit the reusable theory. A closed convex cone is recovered from all dual-positive inequalities (§8.2, Proposition 1). The finite-height epigraph of the extended perturbation value is convex, and that value is antitone in the cone order (§8.3, Propositions 1–2). A Lagrangian saddle point is sufficient for primal feasibility and optimality when the cone is closed (§8.4, Theorem 2). Finally, multipliers for two perturbed right-hand sides bound the change in optimal objective value from both sides (§8.5, Theorem 1). The root then states §8.6, Theorem 1 rather than duplicating the equivalent multiplier theorem from §8.3.

Significance

The capstone provides both equality of optimal values and an attained multiplier. It applies to a single vector inequality, so finite systems of scalar inequalities and matrix-cone constraints fit the same statement once their ordering cones are supplied. Complementarity and Lagrangian minimization turn a primal optimizer and multiplier into a certificate. The sensitivity milestone additionally gives quantitative information about how the optimum changes when the constraint right-hand side moves.

Formalization produces a reusable cone-order layer independent of coordinate choices. coneLE, dualPositive, and ConeConvexOn can support later Kuhn–Tucker, vector optimization, and conic programming developments. The EReal value functions preserve infeasibility and unboundedness, two cases that a real-valued sInf encoding would collapse. This is a formalization mission for a classical theorem, not a claim that the underlying duality result is open.

Difficulty

The theorem's strict-feasibility condition is load-bearing. Feasibility $-G(x)\in P$ cannot replace interior feasibility, and nonempty interior of $P$ alone does not supply a Slater point. Equality constraints also cannot be converted into pairs of inequalities while retaining strict feasibility; Luenberger explicitly warns about this after the theorem.

The cone assumptions differ across milestones. The main strong-duality theorem does not require $P$ to be closed or pointed, whereas the bipolar and saddle-sufficiency statements require closedness. Using Mathlib's stronger ProperCone everywhere would silently add both topological and order hypotheses and shrink the theorem. Another tempting simplification is to make both value functions real. That loses the empty feasible set and unbounded dual subproblem, precisely the boundary cases used when comparing perturbations. The saddle inequalities must also have the correct orientation: the multiplier coordinate is maximized and the primal coordinate is minimized.

Formalization scope

The mission uses ConvexCone ℝ Z with a custom induced relation; it deliberately does not assume a lattice order on $Z$. Multipliers are continuous linear maps $Z\to\mathbb R$. The root assumes a real finite optimum through IsGLB and a real witness $\mu$, while lagrangeDualValue and perturbationValue retain EReal codomains. The strict condition is written as membership of $-G(x_s)$ in interior P, exactly matching $G(x_s)<_P0$.

No finite-dimensionality, reflexivity, completeness, closedness, or pointedness is added to the root. Closedness appears only where the source uses cone separation to recover primal feasibility. The sensitivity item assumes the two candidate points are feasible, their multipliers are dual-positive and complementary, and each point minimizes its shifted Lagrangian; these hypotheses spell out “solutions and corresponding multipliers” without relying on informal terminology.

Contributions may formalize cone separation, perturbation-value geometry, saddle certificates, or strong duality. Finite-dimensional orthant and positive-semidefinite specializations are useful corollaries but do not replace the general goal. Local multiplier rules, equality constraints, differentiable Kuhn–Tucker conditions, and Chapter 9's local theory remain outside this mission.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, Chapter 8, §§8.2–8.6, pp. 214–225. Open Library record
• Stephen Boyd and Lieven Vandenberghe, Convex Optimization, Cambridge University Press, 2004, Chapter 5. Official book page

AI generated, I think it's correct

Motivation

The matrix-multiplication exponent measures the asymptotic arithmetic cost of multiplying square matrices. A bound $\omega<c$ means that, over the field under consideration, $n\times n$ matrices can be multiplied in $O(n^{c+\varepsilon})$ field operations for every $\varepsilon>0$. Matrix multiplication is a central benchmark in algebraic complexity and a basic subroutine in linear algebra, graph algorithms, and symbolic computation.

The Coppersmith--Winograd tensor and the laser method produced the strongest bounds on $\omega$ for several decades. The 1990 tensor-square analysis gave $\omega<2.375477$. Later analyses of larger powers improved the numerical bound, but they organized their recursion through values assigned independently to constituent tensors. Duan, Wu, and Zhou identified a loss in that organization: several fine constituents that can coexist inside one coarse block may be counted as though they had to be selected independently. Their asymmetric-hashing framework partially compensates for this combination loss. The paper's full second-power specialization improves the best bound obtainable from the square of the Coppersmith--Winograd tensor to $\omega<2.374631$; see Section 6.3 and its parameter Table 2 in Duan--Wu--Zhou.

This mission isolates that second-power result. It is smaller than the paper's record-setting eighth-power calculation, but it contains the genuinely new asymmetric-hashing and hole-repair mechanisms in their first complete form. It therefore provides a focused bridge from the existing formalization of the classical $2.375477$ square analysis to later combination-loss methods.

Setting

For a field $K$, the matrix-multiplication tensor

encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix. A restriction applies one linear map to each tensor leg, while a degeneration permits polynomial families of such maps and takes their first nonzero coefficient. A degeneration from the diagonal tensor $I_r$ gives a border-rank upper bound of $r$.

The Coppersmith--Winograd tensor with parameter $q$ is

It has border rank at most $q+2$. Its coordinate partition has six supported types, and the square $CW_q^{\otimes2}$ has fifteen coarse constituent types $(i,j,k)$ with $i+j+k=4$. A large tensor power contains many blocks with prescribed joint and marginal type distributions. The laser method retains blocks whose variables are disjoint and interprets their direct sum through Schönhage's asymptotic sum inequality.

Duan--Wu--Zhou refine this organization by also retaining a split distribution for the fine indices inside each coarse constituent. Coarse $X$- and $Y$-blocks are made unique, while compatible coarse triples may initially share a $Z$-block. The resulting partially damaged constituent tensors are described as broken copies of a standard-form tensor. The formal target uses $q=6$, the full Section 6 construction, and the paper's released second-power parameters.

Formalization targets

Goal: the full second-power asymmetric-hashing bound

For every field $K$,

The source reports the stronger numerical endpoint $2.374631$, so the displayed rational inequality has strict slack. The Lean declaration has exactly the same field quantification and uses exactly the same matMulExp definition as the existing Coppersmith--Winograd $2.376$ mission; only the theorem name and rational endpoint change.

Source-level milestones

The mission first isolates the available-block shuffling interface extracted from Definitions 5.3--5.5 and Claims 5.8--5.10, then formalizes the finite covering core of the Hole Lemma 5.6. The subsequent tensor realization by zeroing and identification, the multiple-copy Corollary 5.11, the compatibility-rate identity of Lemma 6.7, the probabilistic part of Claim 6.8, and the global restricted-splitting value inequality in Equation (25) remain visible structural leaves rather than being hidden inside scalar assumptions. The numerical milestone instantiates Equation (25) with the exact $q=6$ data of Section 6.3 and Table 2 and checks a strict value surplus at $\tau=23747/30000$. The structural proof must also make explicit the conversion from the paper's six-symmetrized value to a direct HasTauValueAtLeast witness for the mode-symmetric CW square. The final bridge applies the existing tau-value/rank machinery and transfers the Strassen-preorder exponent bound to matMulExp.

Significance

The mathematical result gives the first improvement over the classical Coppersmith--Winograd number while continuing to use only the tensor square. It separates improvement of the tensor analysis from improvement obtained merely by moving to a much higher tensor power. The same standard-form and restricted-splitting language is then reused by the paper's higher-power algorithm, which reports $\omega<2.371866$.

For formalization, the mission adds reusable infrastructure for nested tensor partitions. Existing CW-square work records coarse support types and actual matrix-multiplication restrictions. This mission extends that layer with fine split distributions, compatibility between levels, broken-block bookkeeping, and repair of holes without replacing tensor statements by unverified scalar values. Those definitions are prerequisites for later asymmetric-hashing, complete-split, and more-asymmetry analyses.

The bound is known mathematically and was published at FOCS 2023. The open work is a machine-checked reconstruction. The underlying CW tensor, border-rank certificate, canonical tensor-square grading, Salem--Spencer sets, direct-sum tau-value notion, asymptotic sum inequality, and exponent equivalence already exist on Prove2Me. The new frontier is the cross-level combination-loss analysis and its exact numerical specialization.

Difficulty

The central difficulty is that coarse and fine decompositions cannot be optimized independently. Two coarse triples may share a $Z$-block, and a fine $Z$-block can be useful for one triple, compatible with several, or removed by a collision. Counting all locally valuable fine constituents therefore does not certify a direct sum. Conversely, requiring every coarse $Z$-block to be unique discards precisely the combinations that produce the improvement.

The Hole Lemma must also preserve the actual tensor. A broken copy lacks some fine variable blocks; combining several such copies is useful only when a degeneration covers every required block with controlled loss and does not duplicate monomials. On the numerical side, the same-marginal maximum-entropy term and restricted-splitting values must be bounded with certified real inequalities. Floating-point output from MATLAB is evidence for a witness, not a Lean proof.

Formalization scope

The mission uses the existing TensorObj, MMObj, restriction, degeneration, asymptotic-rank, HasTauValueAtLeast, matMulExp_strassen, and matMulExp declarations in environment 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e. Top-level results quantify over an arbitrary field. Finite supports and block indices are represented by finite types; probability and split distributions are nonnegative real functions of total mass one; entropy and numerical optimization live in the reals.

The formalization is restricted to $CW_6^{\otimes2}$ for the capstone, although generic definitions and source lemmas may quantify over levels and finite index types. A valid proof must connect scalar rate inequalities to witnessed restrictions or degenerations yielding direct sums of concrete matrix-multiplication tensors. A constant-valued surrogate for the restricted-splitting value, a hypothesis that already assumes the desired exponent bound, or a certificate definition containing its own conclusion is outside scope.

Contributions are welcome for standard-form tensor encodings, finite permutation arguments, hole repair, type and split counting, entropy maximization certificates, certified logarithm and power inequalities, and the final tau-value/rank assembly. Statements should identify the corresponding definition, lemma, claim, equation, or table in the source.

Selected references

• Ran Duan, Hongxun Wu, and Renfei Zhou, Faster Matrix Multiplication via Asymmetric Hashing, 64th IEEE Symposium on Foundations of Computer Science (FOCS), 2023. arXiv:2210.10173 and released verification code.
• Don Cop persmith and Shmuel Winograd, Matrix Multiplication via Arithmetic Progressions, Journal of Symbolic Computation 9, 1990, pp. 251--280. DOI 10.1016/S0747-7171(08)80013-2.
• Arnold Schönhage, Partial and Total Matrix Multiplication, SIAM Journal on Computing 10(3), 1981, pp. 434--455. DOI 10.1137/0210032.

Motivation

Convex duality converts an optimization problem over points into one over linear functionals. It supplies lower bounds, certificates of optimality, and alternative formulations whose geometry can be simpler than the primal problem. In §§7.8–7.12 of David G. Luenberger's Optimization by Vector Space Methods, this theory is developed for finite-valued convex and concave functions on convex subsets of a real normed space. The capstone is Fenchel duality with restricted domains and an attained continuous-linear-functional dual optimum. This mission preserves that functional-analytic setting rather than reducing the theorem to Euclidean space or silently extending the functions to the whole space.

Setting

Let $X$ be a real normed space, let $C,D\subseteq X$ be nonempty convex sets, let $f:X\to\mathbb R$ be convex on $C$, and let $g:X\to\mathbb R$ be concave on $D$. For a continuous linear functional $\ell\in X^*$, the restricted convex conjugate and restricted concave conjugate are

The convex conjugate is admitted into $C^*$ only when its defining set is bounded above; the concave conjugate is admitted into $D^*$ only when its defining set is bounded below. Because $C$ and $D$ are nonempty and the functions are real-valued, these predicates exactly exclude the unwanted infinite endpoint. The Lean definitions use real sSup and sInf, with boundedness carried explicitly by theorem hypotheses.

The restricted epigraph of $(f,C)$ is the set of $(x,r)$ satisfying $x\in C$ and $f(x)\le r$; the restricted hypograph of $(g,D)$ reverses the scalar inequality. Luenberger's qualification requires a common point of the relative interiors of $C$ and $D$, represented by Mathlib's intrinsicInterior, and also requires ordinary nonempty interior of at least one of these two graph sets.

Formalization targets

Main goal: Fenchel duality

Assume the finite primal value $\mu$ is the greatest lower bound of

Prove that some $\ell_0\in C^*\cap D^*$ attains

If $x_0$ attains the primal infimum, also prove that $x_0$ attains both conjugate extrema at $\ell_0$: $f_C^*(\ell_0)=\ell_0(x_0)-f(x_0)$ and $g_D^*(\ell_0)=\ell_0(x_0)-g(x_0)$.

Milestones

The mission records four source milestones. A local minimum of a convex function on its convex domain is global (§7.8, Proposition 1). Convexity of a restricted function is equivalent to convexity of its restricted epigraph (§7.8, Proposition 2). The finite-conjugate domain and the convex conjugate are convex (§7.10, Proposition 1). Finally, a closed restricted epigraph agrees pointwise on $C$ with the continuous-linear biconjugate (§7.10, Proposition 2). Together these statements expose the geometric and conjugacy interfaces on which the capstone depends without turning every paragraph of the chapter into a separate item.

Significance

The theorem gives an attained dual certificate in an arbitrary real normed space. Equality of primal and dual values eliminates a duality gap, while attainment produces a specific functional that can certify an optimal primal point through simultaneous conjugate equality. The biconjugate milestone is independently useful: it expresses a closed convex function as a supremum of continuous affine minorants on its domain.

Formalizing this material adds a restricted-domain conjugacy API that is not supplied by the existing project artifact named fenchelConjugate. That artifact accepts finite-valued functions on a Euclidean space and has no independent convex domain or concave conjugate. Reusing it here would erase hypotheses that are central to Luenberger's theorem. The new definitions remain small, but their exact boundedness contracts make them reusable for later separation, minimax, and Lagrange-duality missions. The theorem is classical; the mission asks for a checked development faithful to the 1969 source and the current Mathlib representation of continuous dual spaces.

Difficulty

The qualification is not the usual finite-dimensional slogan that relative interiors merely intersect. The source additionally demands that either the restricted epigraph or restricted hypograph have nonempty ordinary interior. Dropping that condition changes the theorem in infinite-dimensional spaces. Replacing intrinsicInterior by topological interior would also make valid lower-dimensional domains appear empty.

Extended values create another boundary. Real sSup and sInf are meaningful here only together with nonempty domains and the respective boundedness hypotheses. Treating their default values outside those hypotheses as genuine conjugates would admit false dual candidates. A finite-dimensional conjugate definition avoids neither issue and would prove only a special case. The biconjugate target must quantify over continuous linear functionals, not all algebraic linear maps, because closed epigraph separation is topological. Finally, the dual statement must include actual attainment; proving only equality with a supremum would omit a principal assertion of §7.12.

Formalization scope

All primal functions are finite-valued real functions. Infinite conjugate values are represented by domain predicates—BddAbove for $f_C^*$ and BddBelow for $g_D^*$—rather than by changing the public conjugate codomain. The primal finiteness assumption is encoded by a real number $\mu$ together with IsGLB, which simultaneously rules out an empty feasible intersection and an infimum of $-\infty$. Epigraph pairs are ordered as $(x,r)$ to match Mathlib conventions, although Luenberger prints the scalar coordinate first.

The ambient space is normed but is not assumed finite-dimensional, reflexive, or complete. Both $C$ and $D$ are explicitly nonempty. The main theorem keeps the common intrinsic-interior condition and the disjunctive ordinary-interior condition verbatim. Contributions may develop separation lemmas, boundedness facts for restricted conjugates, or direct proofs of the milestone statements. A whole-space Euclidean specialization is welcome only as a corollary, not as a replacement for the root. The minimax theorem of §7.13 and extended-real lower-semicontinuous variants are outside this mission.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, Chapter 7, §§7.8–7.12, pp. 191–202. Open Library record
• R. Tyrrell Rockafellar, Convex Analysis, Princeton University Press, 1970. DOI: 10.1515/9781400873173

Every full-dimensional convex body is sandwiched between an ellipsoid and its $n$-fold dilation: shrinking the minimum-volume covering (Löwner–John) ellipsoid $\mathcal{E}$ about its centre $x_0$ by the factor $1/n$ lands inside the body,

and the factor $n$ is tight on simplices. This rounding theorem underlies the ellipsoid method, John's theorem on the Banach–Mazur distance to the Euclidean ball, and much of modern convex geometry. The mission formalizes §8.4 of Boyd & Vandenberghe for polytopes $C = \operatorname{conv}\{x_1,\dots,x_m\}$, exactly as the book proves it: existence and uniqueness of the extremal ellipsoid, the KKT identities at the normalized optimum ($\sum_i \lambda_i x_i x_i^{T} = I$, $\sum_i \lambda_i x_i = 0$, $\sum_i \lambda_i = n$), the convex-combination step that produces the $1/n$ ball, and affine invariance.

Parallel repetition for quantum games

Nonlocal games

A nonlocal game is played between a classical referee and two or more cooperating players who are not allowed to communicate during the game. In the two-player, one-round setting, the referee samples a pair of questions $(x,y)$ from a distribution $\mu$, sends $x$ to Alice and $y$ to Bob, and receives answers $a$ and $b$. The players win when a predicate $V(x,y,a,b)$ accepts. Before the game begins they may agree on a strategy and share a resource, but after receiving their questions they are isolated from one another.

Nonlocal games occupy a useful interface between complexity theory and quantum information. From the perspective of complexity theory, they are the basic objects underlying multiprover interactive proofs: a verifier delegates a computation to separated provers and uses the consistency of their answers to distinguish valid from invalid claims. Classical two-prover games play a central role in the PCP theorem, hardness of approximation, and soundness amplification. Allowing the provers to share entanglement leads to the class $\mathrm{MIP}^*$ and to a substantially richer theory. The theorem $\mathrm{MIP}^*=\mathrm{RE}$ shows how dramatically entanglement changes this landscape: even estimating the entangled value of a nonlocal game can encode undecidable computation Ji--Natarajan--Vidick--Wright--Yuen 2020.

From the perspective of quantum information, nonlocal games are operational formulations of Bell experiments. A separation between classical and entangled values witnesses correlations that cannot be explained by a local hidden-variable model. The same framework supports self-testing, in which near-optimal behavior certifies the underlying state and measurements up to local equivalence, and device-independent cryptography, in which security or randomness is certified from observed input-output statistics rather than a trusted description of the devices. Representative references include Cleve--Høyer--Toner--Watrous 2004, Reichardt--Unger--Vazirani 2013, and Pironio et al. 2010. The survey of Palazuelos--Vidick 2016 describes further connections among nonlocal games, Bell inequalities, operator spaces, and quantum information.

Thus the value of a nonlocal game is simultaneously a complexity-theoretic soundness parameter and a quantitative measure of the power of nonclassical correlations. Understanding how this value changes under natural operations on games is important in both subjects.

Entangled strategies and value

We take the finite answer alphabets to be nonempty. In a classical strategy, Alice's answer depends only on $x$, Bob's answer depends only on $y$, and the players may coordinate using shared randomness. In a finite-dimensional entangled strategy, the players share a bipartite state $\rho$ and use POVM measurement operators

for their respective questions. The probability of producing answers $(a,b)$ on questions $(x,y)$ is

The supremum of the winning probability over all such finite-dimensional strategies is the entangled value $\omega^*(G)$. This optimization ranges over arbitrary local dimensions, shared states, and local measurements, which is one reason even apparently elementary questions about nonlocal games can be difficult.

Parallel repetition

For a positive integer $n$, the repeated game $G^n$ consists of $n$ independently sampled copies of $G$ played simultaneously. Alice receives $(x_1,\ldots,x_n)$, Bob receives $(y_1,\ldots,y_n)$, and they answer with tuples $(a_1,\ldots,a_n)$ and $(b_1,\ldots,b_n)$. They win only if

for every coordinate $i$.

Parallel repetition is a basic method of soundness amplification. Starting from a game that dishonest players cannot win with certainty, the verifier repeats the test in the hope of driving the optimal success probability rapidly toward zero. The difficulty is that independence in the verifier's sampling does not force independence in the players' strategy. Alice may choose her entire answer tuple as a function of all her questions, Bob may do the same, and an entangled strategy may use a single state and joint measurements spanning all coordinates. In particular, one cannot obtain an upper bound on $\omega^*(G^n)$ merely by analyzing the strategy that plays each coordinate independently.

For classical games, Raz's parallel repetition theorem gives exponential decay whenever the one-shot value is below one Raz 1998. Establishing the corresponding behavior for entangled games has been a long-running problem. A general polynomial bound was proved in Yuen 2016, implying for the first time that $\omega^*(G^n)$ tends to zero for every finite two-player entangled game with $\omega^*(G)<1$.

The full exponential-decay theorem was recently settled by OpenAI. In Chapter 6 of Ten Advances in Mathematics and Theoretical Computer Science, OpenAI proves that for every finite two-player entangled game $G$ with $\omega^*(G)<1$, there is a constant $c_G>0$ such that

for every positive $n$. OpenAI also released a Lean certificate for the result. This resolves the general quantum parallel-repetition conjecture, but it does not end the study of the problem. The proof introduces quantitative losses and a substantial technical apparatus, and there remains considerable value in finding alternative arguments, isolating the essential mechanism, improving the dependence on the one-shot gap and answer size, and producing shorter or more conceptual formal proofs.

A hierarchy of formalization targets

This mission develops a reusable Lean framework for parallel repetition rather than formalizing only one paper. Its targets are organized by the strength of the asserted decay.

Qualitative decay

The main mission theorem is the fundamental asymptotic statement:

Equivalently, for every $\delta>0$, all sufficiently large $n$ satisfy $\omega^*(G^n)<\delta$. This statement deliberately specifies no rate. It is a stable top-level theorem that can be recovered from any sufficiently strong quantitative bound.

Polynomial decay

A stronger target asks for game-dependent constants $C>0$ and $\alpha>0$ such that

The abstract formulation avoids fixing a particular exponent or logarithmic correction. More refined formalizations can record explicit dependence on the gap $1-\omega^*(G)$, the answer alphabet, or other game parameters. Yuen's 2016 theorem is one important result at this level.

Exponential decay

The exponential target asks for game-dependent constants $C,c>0$ such that

Following OpenAI's recent resolution, this target is now a theorem rather than an open conjecture. Within this mission it remains a central milestone: contributors may formalize the released argument in the mission's common interface, construct an independent proof, seek a more elegant or modular proof, or establish sharper quantitative variants.

These levels do not exhaust the project. The same framework can accommodate explicit finite-$n$ inequalities, stretched-exponential estimates, bounds for structured classes of games, improved parameter dependence, and reductions showing that one decay statement implies another.

Formalization scope

The foundational Lean development represents a game by finite question sets $X,Y$, finite answer sets $A,B$, a nonnegative normalized question distribution $\mu(x,y)$, and a Boolean verification predicate $V(x,y,a,b)$. The parallel-repetition theorems explicitly assume that $A$ and $B$ are nonempty. The development defines finite-dimensional entangled strategies using density matrices and POVM measurement operators, defines the repeated game on tuples, and takes the entangled value as a supremum over all finite-dimensional strategies. Repeated strategies are indexed by complete question tuples and are not required to factor coordinatewise.

A complete development will draw on formal libraries for finite probability, tensor products, positive semidefinite matrices, density matrices, POVMs, trace norms, fidelity, entropy, mutual information, and correlated sampling. These components should be formulated for reuse and should expose the dependence of each bound on the relevant game parameters.

The goal is both to verify parallel-repetition theorems and to build a dependable language for nonlocal games in Lean. Formalization forces distinctions that are easy to suppress on paper: whether constants depend on the game, whether a bound holds for all $n$ or only asymptotically, which strategy model is optimized over, and which hypotheses are needed for a particular rate. The mission welcomes reconstructions of known proofs as well as new, shorter, or conceptually different proofs.

Selected references

• R. Cleve, P. Høyer, B. Toner, and J. Watrous, Consequences and limits of nonlocal strategies, CCC 2004.
• R. Raz, A parallel repetition theorem, SIAM Journal on Computing 27(3), 1998.
• H. Yuen, A parallel repetition theorem for all entangled games, ICALP 2016.
• Z. Ji, A. Natarajan, T. Vidick, J. Wright, and H. Yuen, $\mathrm{MIP}^*=\mathrm{RE}$, Communications of the ACM 64(11), 2021.
• OpenAI, Ten Advances in Mathematics and Theoretical Computer Science, Chapter 6, 2026; accompanying Lean formalization.

Interior point methods solve linear programs by moving through the interior of the feasible set instead of along its edges — the approach that turned Karmarkar's 1984 breakthrough into today's practical large-scale solvers. This mission formalizes the primal path following algorithm of Chapter 9 of Bertsimas–Tsitsiklis. For $\mu > 0$ the logarithmic barrier

replaces the constraint $\mathbf{x} \ge \mathbf{0}$; the minimizers $\mathbf{x}(\mu)$ of $B_\mu$ over $\{A\mathbf{x} = \mathbf{b}\}$ trace the central path, characterized by the KKT conditions (9.17): $A\mathbf{x} = \mathbf{b}$, $\mathbf{x} \ge \mathbf{0}$, $A'\mathbf{p} + \mathbf{s} = \mathbf{c}$, $\mathbf{s} \ge \mathbf{0}$, $XS\mathbf{e} = \mu\mathbf{e}$ (Lemma 9.5). The algorithm follows the path with one Newton step of the barrier problem per shrink $\mu^{k+1} = \alpha\mu^k$, maintaining the proximity invariant

. The goal theorem is Theorem 9.7: with $\alpha = 1 - \frac{\sqrt{\beta}-\beta}{\sqrt{\beta}+\sqrt{n}}$ and a $\beta$-close start, after $K = \Big\lceil \frac{\sqrt{\beta}+\sqrt{n}}{\sqrt{\beta}-\beta}\,\log\frac{(\mathbf{s}^0)'\mathbf{x}^0(1+\beta)}{\varepsilon(1-\beta)} \Big\rceil$ iterations the algorithm reaches primal and dual feasible solutions with duality gap $(\mathbf{s}^K)'\mathbf{x}^K \le \varepsilon$ — the explicit form of the celebrated $O(\sqrt{n}\log(1/\varepsilon))$ iteration bound. Alongside it we formalize the generic potential-reduction scheme (Theorem 9.4): any algorithm cutting $G(\mathbf{x},\mathbf{s}) = q\log\mathbf{s}'\mathbf{x} - \sum_j \log x_j - \sum_j \log s_j$ by $\delta$ per step reaches gap $\varepsilon$ within an explicit $K$.

Can the feasibility of a system of linear inequalities be decided in a provably small number of iterations? The ellipsoid method — the algorithm with which Khachiyan showed in 1979 that linear programming is polynomially solvable — answers this with pure convex geometry. This mission formalizes Chapter 8 of Bertsimas–Tsitsiklis. An ellipsoid is

with $D$ symmetric positive definite. The geometric engine is Theorem 8.1: the half-ellipsoid $E \cap \{\mathbf{x} \mid \mathbf{a}'\mathbf{x} \ge \mathbf{a}'\mathbf{z}\}$ is contained in the explicitly constructed ellipsoid $E' = E(\bar{\mathbf{z}}, \bar{D})$,

and the volume contracts:

. Two integer-data estimates make the contraction decisive: every extreme point of $P = \{\mathbf{x} \mid A\mathbf{x} \ge \mathbf{b}\}$ with entries bounded by $U$ has coordinates in $[-(nU)^n, (nU)^n]$ (Lemma 8.2), and a full-dimensional bounded such polyhedron has $\mathrm{Vol}(P) > n^{-n}(nU)^{-n^2(n+1)}$ (Lemma 8.4). The goal theorem is Theorem 8.2: started on a ball $E(\mathbf{x}_0, r^2 I)$ of volume at most $V$ containing $P$, with $v$ a lower bound on $\mathrm{Vol}(P)$ when $P$ is nonempty, the ellipsoid method correctly decides whether $P$ is empty within $t^* = \lceil 2(n+1)\log(V/v) \rceil$ iterations — the explicit iteration count behind the polynomial-time headline.

Why do network linear programs return integer answers for free? This mission formalizes the structural theory of the minimum cost network flow problem of Chapter 7 of Bertsimas & Tsitsiklis: a directed graph $G=(\mathcal{N},\mathcal{A})$ with external supplies $b_i$, arc costs $c_{ij}$, and the node-arc incidence matrix $\mathbf{A}$ — an $n\times m$ matrix in which every column has exactly one $+1$ (start node) and one $-1$ (end node) — so that flow conservation reads $\mathbf{A}\mathbf{f}=\mathbf{b}$, forcing the standing assumption $\sum_{i\in\mathcal{N}} b_i=0$. Because the rows of $\mathbf{A}$ sum to zero, the book works with the truncated matrix $\tilde{\mathbf{A}}$ of the first $n-1$ rows. The combinatorial heart is the correspondence between algebra and graph structure: a set $T$ of $n-1$ arcs forming a tree determines a unique tree solution of $\tilde{\mathbf{A}}\mathbf{f}=\tilde{\mathbf{b}}$, $f_{ij}=0$ off $T$ (Theorem 7.3); connectedness makes $\tilde{\mathbf{A}}$ full-rank (Corollary 7.1); and a flow vector is a basic solution if and only if it is a tree solution (Theorem 7.4). The goal theorem is the integrality theorem (Theorem 7.5): for the uncapacitated problem on a connected graph, every basis matrix $\mathbf{B}$ has an integer inverse $\mathbf{B}^{-1}$ (its determinant is $\pm 1$ by the tree/lower-triangular argument), integer supplies make every basic solution integer, and integer costs make every dual basic solution integer — whence integer optimal primal and dual solutions exist whenever the optimal cost is finite (Corollary 7.2). This is the fountainhead of combinatorial integrality in linear optimization, feeding the max-flow min-cut mission that follows.

How does the optimal cost of a linear program respond when the problem data change? Chapter 5 of Bertsimas-Tsitsiklis studies the standard form problem $\min\{c'x \mid Ax = b,\ x \ge 0\}$ (rows of $A$ linearly independent) as the requirement vector $b$ and the cost vector $c$ vary. On the convex set $S = \{b \mid P(b) \neq \emptyset\}$ of feasible right-hand sides, and under the standing assumption that the dual feasible set is nonempty, the optimal cost $F(b)$ is finite and convex (Theorem 5.1) — indeed $F(b) = \max_{i} (p^i)'b$ over the extreme points $p^1, \dots, p^N$ of the dual feasible set, a piecewise linear convex function whose breakpoints are exactly where the dual optimum is non-unique. The capstone (Theorem 5.2) identifies the generalized gradients of $F$: if the primal at $b^*$ is feasible with finite optimal cost, then $p$ is an optimal solution of the dual if and only if $p$ is a subgradient of $F$ at $b^*$ (Definition 5.1: $F(b^*) + p'(b - b^*) \le F(b)$ for all $b \in S$) — the precise sense in which dual variables are marginal costs. Dually (Theorem 5.3), the set $T$ of cost vectors with finite optimal cost is convex, the optimal cost $G(c)$ is concave on $T$, and near any $c$ with a unique primal optimum $x^*$, $G$ is linear with gradient $x^*$. Local ranging (Section 5.1) and parametric programming (Section 5.5) are the procedural companions, folded into the design notes.

Every linear programming problem has a shadow. To the primal $\min c'x$ we associate the dual $\max p'b$, whose variables price the primal constraints: one dual variable per primal constraint and one dual constraint per primal variable, with signs governed by the correspondence of Table 4.1. This mission formalizes §4.1–4.5 of Bertsimas–Tsitsiklis: the dual of a general-form linear program, the involution "the dual of the dual is the primal" (Theorem 4.1), and weak duality $p'b \le c'x$ for any primal-feasible $x$ and dual-feasible $p$ (Theorem 4.3) with its two corollaries — an unbounded primal forces an infeasible dual (Corollary 4.1), and feasible $x, p$ with $p'b = c'x$ are automatically both optimal (Corollary 4.2). The goal theorem is strong duality (Theorem 4.4): if a linear programming problem has an optimal solution, so does its dual, and the respective optimal costs are equal — proved in the book by running the simplex method with the lexicographic pivoting rule of Mission IV on a standard-form transform. The statement is deliberately the book's attainment form: by Table 4.2 the primal and the dual can be simultaneously infeasible (Example 4.5), so an unguarded equality of optimal values is false. The mission closes with complementary slackness (Theorem 4.5): feasible $x$ and $p$ are simultaneously optimal if and only if $p_i(a_i'x - b_i) = 0$ for all $i$ and $(c_j - p'A_j)x_j = 0$ for all $j$ — the certificate structure behind the dual simplex method and every LP optimality check.

How does one actually solve a linear program? Chapter 2 showed that if a standard-form problem $\min c'x$ subject to $Ax = b$, $x \ge 0$ has an optimal solution, it has an optimal basic feasible solution; the simplex method searches among basic feasible solutions, moving along edges of the feasible set in cost-reducing directions. This mission formalizes the mathematics of Chapter 3 of Bertsimas–Tsitsiklis: feasible directions, the reduced costs

measuring the cost rate along the basic directions, the optimality conditions of Theorem 3.1 ($\bar{c} \ge 0$ implies optimality, and conversely at nondegenerate optima), the basis change of Theorem 3.2, and the pivot iteration itself — encoded as a predicate relating a basis/BFS pair to its successor, so that every theorem covers every pivoting rule. The goal theorem is Theorem 3.3: if the feasible set is nonempty and every basic feasible solution is nondegenerate, the simplex method terminates after a finite number of iterations, ending either with an optimal basis and an associated optimal basic feasible solution, or with a direction $d$ satisfying $Ad = 0$, $d \ge 0$, $c'd < 0$ certifying optimal cost $-\infty$. The secondary capstone, Theorem 3.4, removes the nondegeneracy assumption: under the lexicographic pivoting rule every tableau row other than the zeroth stays lexicographically positive, the zeroth row strictly increases lexicographically, and the simplex method terminates on every problem — the anticycling guarantee that also supplies the optimal-basis existence used by the strong duality theorem of Mission V.

Every linear programming problem asks to minimize a linear cost $c'x$ over a polyhedron — a set of the form $P = \{x \in \mathbb{R}^n \mid Ax \ge b\}$, or in standard form $\{x \mid Ax = b,\ x \ge 0\}$. Chapter 2 of Bertsimas–Tsitsiklis develops the geometry of these feasible sets, and its central achievement is making the intuitive notion of a "corner point" rigorous. There are three natural candidates: the extreme point — a point of $P$ that cannot be written as a convex combination of two other points of $P$ (purely geometric, representation-independent); the vertex — the unique minimizer of some linear cost $c'y$ over $P$ (geometric, via supporting hyperplanes); and the basic feasible solution — a feasible point at which $n$ linearly independent constraints are active (algebraic, the object the simplex method actually computes with). This mission formalizes polyhedra, active constraints, vertices and basic (feasible) solutions, and proves the fundamental Theorem 2.3: for a nonempty polyhedron all three notions coincide. Around the capstone sit the supporting pillars: polyhedra are convex (Theorem 2.1), the characterization of points pinned down by $n$ linearly independent active constraints (Theorem 2.2), finiteness of the set of basic solutions (Corollary 2.1), and the basis-column characterization of basic solutions in standard form (Theorem 2.4) — the combinatorial engine behind the simplex method of Chapter 3 and the root of the entire series.

A continuous piecewise linear (CPWL) function is one assembled from finitely many flat pieces glued along flat seams. Every ReLU network computes such a function, and every such function is computed by some ReLU network. Questions about how deep a network must be are therefore questions about the internal structure of CPWL functions.

In 1993 Breiman built such functions from hinges: maxima of two affine maps. Sums of hinges approximate anything, but from two dimensions up they fail to represent most CPWL functions exactly. Wang and Sun (2005) widened the maxima, proving that every CPWL function on ℝⁿ is a signed sum of maxima of at most n+1 affine maps. Twenty years on it remains the workhorse structural fact, reducing any question about a network to a question about a single max gate and underpinning every known upper bound on the depth of exact representation.

That includes the newest one: at STOC 2026, Bakaev et al disproved the short standing conjecture that ⌈log₂(n+1)⌉ hidden layers are necessary, showing ⌈log₃(n−1)⌉+1 suffice. In this mission we deliver a machine-checked proof of the Wang and Sun theorem so future formalizations of network expressivity can invoke it rather than reprove it. Note that we take as given the lattice representation of Tarela and Martínez, independently proved by Ovchinnikov, which writes any CPWL function as a max of mins of its affine pieces. That is the one external ingredient the argument consumes, and our definition of CPWL builds it in.

How quickly does the empirical mean of independent random variables concentrate around the true mean? This question is the analytic engine of the entire theory of stochastic bandits: every optimistic algorithm (Explore-Then-Commit, UCB and its relatives) is calibrated by a tail bound on the sample mean. This mission formalizes the subgaussian framework of Chapter 5 of Lattimore–Szepesvári's Bandit Algorithms: a random variable $X$ is $\sigma$-subgaussian when $\mathbb{E}[e^{\lambda X}] \le e^{\lambda^2\sigma^2/2}$ for all $\lambda$, and the Cramér–Chernoff method converts this moment-generating-function control into the exponential tail $\mathbb{P}(X \ge \varepsilon) \le e^{-\varepsilon^2/(2\sigma^2)}$. The goal theorem is the Hoeffding-type bound: the sample mean of $n$ independent $\sigma$-subgaussian deviations exceeds the true mean by $\varepsilon$ with probability at most $\exp(-n\varepsilon^2/(2\sigma^2))$, together with its confidence form $\mathbb{P}\big(\hat\mu + \sqrt{2\sigma^2\log(1/\delta)/n} \le \mu\big) \le \delta$ — the exact bound every UCB index is built from. These few lines of analysis are cited by every regret bound in the series.

Multi-agent reinforcement learning approximates a global value function by summing per-agent local value functions learned independently — a trick that works surprisingly well in practice (ride-hailing dispatch, restless bandits) but had no general theoretical justification. Chen and Peng (arXiv:2506.02385) explain why: they define a Markov entanglement measure for the joint transition dynamics of a multi-agent MDP, directly analogous to quantum entanglement of a two-party state, and show it controls exactly how much error this value-decomposition trick incurs. This mission formalizes their sharpest quantitative bound (Theorem 4): the error of decomposing the global Q-function into per-agent local Q-functions is controlled, entrywise, by the agent-wise total-variation measure of Markov entanglement.

A platform sourcing items from monopolistic sellers with private quality cannot tractably maximize its true profit: the bundle revenue $Rev(v_S)$ is neither monotone, submodular, supermodular, subadditive, nor superadditive. Theorem 4.6 of Buying to Bundle: Optimal Sourcing from Monopolistic Sellers shows that the simple surrogate threshold mechanism — maximize the linearized objective $\varpi(x)=N\,E[x(\mu)(\mu-\varphi(\mu))]$ — is profit-optimal up to a $1+O(N^{-1/3})$ factor in large markets. Prove it: Bernoulli concentration for the bundle quality plus sub-exponential control of the dispersion gap $|Rev(v)-E[v]|$ (Lemma 4.5).