Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Stochastic gradient methods are the standard tool for minimizing an objective that can only be accessed through noisy gradient samples. Training a machine-learning model on sampled data, simulation-based optimization, and stochastic programs with endogenous uncertainty are all of this kind. In many of these applications the objective is nonconvex: the loss or the regularizer of a learning problem may be nonconvex, as may the expected cost of a simulation model.
Before 2013 the complexity theory of stochastic approximation (SA) was essentially a convex theory. Robbins and Monro (1951) introduced the method. Polyak and Juditsky (1992) and Nemirovski, Juditsky, Lan and Shapiro (2009) established optimal rates for convex problems, and Lan (2012) unified the smooth, nonsmooth and stochastic convex cases. None of these results covered nonconvex objectives. Ghadimi and Lan (2013) gave the first non-asymptotic complexity bound for a stochastic gradient method on a smooth nonconvex problem. The bound is stated for the expected squared gradient norm at a randomly chosen iterate, and it is the result this mission formalizes.
The problem is
where is differentiable and bounded below, and its gradient is -Lipschitz: for all . This class is written . The function need not be convex.
The gradient is accessible only through a stochastic first-order oracle: at the -th query point it returns , where are random variables and is a Borel function. Assumption A1 asks that for every , conditionally on the past, is an unbiased estimate of , and that its error has second moment . The noise variables need not be independent of each other or of the iterates.
The randomized stochastic gradient (RSG) method takes an initial point , an iteration limit , stepsizes and a probability mass function on . It draws a random index , runs
and outputs . The mass function used in the main theorem is
The constants are and, in the convex case with minimizer , .
If for , , and has the mass function above, then under Assumption A1
where the expectation is over and the noise. Any stepsize sequence below is allowed, so the goal does not fix a step rule, and the step rules of the paper's corollaries follow from it.
Theorem 2.1 b) bounds by when is convex with a minimizer. Corollary 2.2 specializes both bounds to the stepsizes :
and the analogous bound with for in the convex case.
Theorem 2.1 a) is the basic guarantee for stochastic gradient descent on smooth nonconvex objectives. With the stepsizes of Corollary 2.2 it shows that oracle calls suffice to reach . The paper builds two further methods on it: a two-phase variant with large-deviation guarantees, and a zeroth-order variant (RSGF) that uses Gaussian smoothing when only function values are available. Later analyses of variance-reduced and adaptive stochastic methods for nonconvex problems measure their improvements against this bound.
The result is proved on paper; no machine-checked proof of it is known. A formalized fixed-step bound of the form "some iterate among the first has small expected squared gradient" exists, but it is a different statement: it has no randomized output and no general stepsizes. A complete formalization would check the measure-theoretic content that the paper treats informally: integrability of the iterates' gradients, the conditional-expectation step under dependent noise, and the role of the independence of .
The algebra of (2.8)–(2.9) is routine. The difficulty is in the probability. The noise may depend on the past, so the cross term vanishes only in conditional expectation, and only once is known to be measurable with respect to the past. Its integrability is not assumed anywhere: must be shown to have a finite second moment from the recursion, the Lipschitz gradient and Assumption A1. The randomized output adds a second step, where is rewritten as a weighted average. This needs independent of the noise, and has to be exhibited as a measurable function of the noise sequence. A proof that replaces by the deterministic weighted average skips exactly this step.
EuclideanSpace ℝ (Fin n). is the published predicate ConvexOptAlg.SmoothGD.IsBetaSmooth f g L, with the gradient given as a map . is the greatest lower bound of the range of , not an arbitrary lower bound.Stochastic programs and chance-constrained models in operations research contain expectations of the form
where is a random input under an unknown distribution , is a decision and is a known loss. In practice is seen only through i.i.d. data . Distributionally robust optimization (DRO) replaces the unknown expectation by the worst case over a set of plausible distributions, and a recurring question is how large that set should be so that the robust value is a statistically valid bound, without being needlessly conservative.
The usual answer, for divergence-based sets on a finite support of size , sets the radius from a quantile (Ben-Tal et al. 2013). This guarantee holds simultaneously for every function of the distribution, and so it is loose for a single expectation, and it degrades as grows. H. Lam (arXiv:1605.09349, Operations Research 2019) observed that if the ball is placed around the empirical distribution and measured with the Burg entropy, the right radius uses one degree of freedom, whatever the support. The DRO bounds then form an asymptotically exact confidence interval for . The mechanism is the empirical likelihood method of Owen (Owen 1988; Owen 2001).
Timeline:
Data: are i.i.d. random elements of a measurable space under . A decision is fixed, and is measurable with .
The empirical Burg-entropy divergence ball of radius is the set of weight vectors on the data points
with . It is the -divergence ball around the uniform weights for the Burg generator . Let be the -quantile of the law, i.e. for . The empirical DRO bounds are
For a sample and a value , the profile empirical likelihood statistic is
equal to when no weight vector is feasible.
The event is two-sided and joint. No rate is claimed.
Theorem 2 says that a robust optimization formulation with a data-driven Burg ball of radius yields an asymptotically exact confidence interval for an expected loss, independently of the support size of . Proposition 2 is the bridge: it identifies the DRO interval with the empirical likelihood confidence region, so any distributional result on transfers to the DRO bounds. This is the pointwise basis of the paper's later results on feasibility of chance and expectation constraints.
The result is proved in the paper, and Theorem 1 is classical. To our knowledge none of these statements has a machine-checked proof. Formalizing them requires the empirical likelihood theorem in Lean, which is reusable well beyond DRO (empirical likelihood tests and intervals for means). The Open platform theorem GenEmpLik.Coverage.theorem_3 (Duchi, Glynn and Namkoong) implies the goal when its decision set is the single point and its generator is with radius ; it is a different, more general statement and is not proved. Likewise the Open GenEmpLik.Expansion.lemma_7 implies Lemma 3, and the Proved NumStochOpt.ListScheduling.lemma_8_1_i_max_over_sqrt_ae gives Lemma 3 after passing to .
Proposition 2 is a finite-dimensional convexity statement, but it needs attainment of the minimum defining , which holds only because the objective blows up at the boundary of the simplex. The central difficulty is Theorem 1. The optimal weights are explicit only through a Lagrange multiplier that solves a nonlinear equation; to expand one must first show , which requires controlling the largest observation by Lemma 3 together with the law of large numbers for , and then bound the cubic Taylor remainder of uniformly in . A direct appeal to the central limit theorem for the sample mean does not suffice, since is an implicitly defined optimal value, not a smooth function of the mean.
ξ : ℕ → Ω → Ξ, measurable, mutually independent and identically distributed, indexed from ; the size- sample is fun i : Fin n => h x (ξ i ω).MemLp (h x ∘ ξ 0) 2 together with 0 < variance. Positive variance cannot be dropped: for a constant loss the coverage is .gaussianReal 0 1 {y | y^2 ≤ q} = ofReal (1 - α) with ; it is not a free parameter, and it is not the normal quantile.GenEmpLik.Expansion.robustMean burg (q/2) (its ball has radius , so ); the lower bound is its infimum twin robustLower. The ball uses the published probUncertaintySet and phiDiv.elStat minimizes over strictly positive weights with the empty infimum equal to . Lean's junk value therefore never enters: a formalization with and real logarithms would admit boundary weights with spurious finite divergence and is ruled out. For the value sets of the DRO bounds are nonempty and bounded, so the real infimum and supremum are not junk values.Contributions welcome: proofs of Proposition 2 and Lemma 3 (from the Proved reference), the KKT analysis (49)–(52), and a Lean empirical likelihood theorem.
A set of agents must share a set of indivisible goods, each agent valuing bundles of goods by her own valuation. Two fairness notions dominate the literature. Envy-freeness up to any good (EFX), introduced by Caragiannis, Kurokawa, Moulin, Procaccia, Shah and Wang (EC 2016), asks that no agent prefer another's bundle once any single good is removed from it. The maximin share (MMS), proposed by Budish (JPE 2011), asks that every agent receive at least what she could secure by splitting the goods into bundles herself and taking the worst one.
Neither notion is known to be achievable in full. Whether complete EFX allocations always exist is open in general. Complete MMS allocations need not exist: Procaccia and Wang (EC 2014) gave a counterexample with three agents, and the best known approximation factors for additive valuations are (Ghodsi et al., EC 2018) and (Garg and Taki, arXiv:1903.00029). Amanatidis, Birmpas and Markakis (IJCAI 2018) showed that every complete EFX allocation is a -MMS allocation.
Caragiannis, Gravin and Huang (EC 2019) showed that EFX can be achieved if some goods are left unallocated, with no bound on how many. Chaudhury, Kavitha, Mehlhorn and Sgouritsa (arXiv:1907.04596, SODA 2020, SIAM J. Comput. 2021) relax completeness instead: some goods may be "donated to charity". Their Theorem 8 produces an EFX partial allocation in which nobody envies the donated set and the donated set has fewer goods than there are unenvied agents. This mission formalizes their Theorem 14: such an allocation also gives every agent a maximin-share guarantee that improves as more goods are donated.
Agents are and goods are , . Agent has a valuation , assumed additive: for every .
A (partial) allocation gives agent the bundle , the bundles being pairwise disjoint. The pool of unallocated goods is , and .
the maximum over partitions of into possibly empty bundles. Agent 's maximin share in the instance is .
The three conditions of Theorem 8 on are:
For every allocation with pool satisfying conditions 1–3, and every agent ,
The factor ranges from when to when .
Theorem 14 shows that leaving goods unallocated is not merely a cost: under conditions 1–3, each donated good buys a quantitative improvement of every agent's maximin-share guarantee, interpolating between the factor the bound gives when the pool is empty and a factor tending to when nearly goods are donated. Together with Theorem 8 it shows that a single allocation can be simultaneously EFX, envy-free towards the charity, small in its charity, and approximately MMS. The same reduction (Proposition 13 applied to a carefully chosen sub-instance) is the template for the paper's -groupwise-maximin-share result, Theorem 16, formalized in mission III of this series.
The result is proved in the paper; no machine-checked proof of it, of Proposition 13, or of the existence of EFX allocations with bounded charity is known to exist. The mission produces a formal maximin-share definition on arbitrary subsets of goods with an arbitrary number of bundles, a formal proof of the monotonicity of the maximin share under removal of agents and goods (Proposition 13, which the paper quotes without proof), and the guarantee itself. Combined with mission I of this series (Theorem 8), it yields the printed existence statement.
The guarantee compares an agent's own bundle with a benchmark defined over all partitions of all goods, while EFX and the source condition speak only about the allocation at hand. The obvious attempt, summing over all agents and adding the pool, gives only a factor near and ignores the pool's size. Agents holding a single good are the obstruction: EFX gives no bound on the value of their bundles relative to , and the benchmark is defined on the full instance, which contains them. Proposition 13, the comparison of maximin shares across instances, is a combinatorial statement about all partitions of the original instance and requires nonnegativity of the valuations: with a good of negative value it fails.
Agents are Fin n (0-based) and goods Fin m; the set is the whole of Fin m. Valuations are functions Fin n → Finset (Fin m) → ℝ; additivity is the sum formula together with nonnegativity, which is the paper's codomain . An allocation is a family of pairwise disjoint finsets and the pool is always computed as the complement of their union, never taken as a free parameter. Sources are agents of indegree zero in the envy graph (nobody envies them), not agents who envy nobody. The maximin share is a supremum over labellings Fin m → Fin k' restricted to of the minimum bundle value; it is used only with , which every statement has in its hypotheses or derives from them (in the goal, condition 3 forces ). Every cardinality is cast to before division or subtraction, and under condition 3, so no division by zero occurs.
The goal is posed as an implication for every allocation satisfying conditions 1–3, rather than as the paper's "there exists an allocation"; the paper's proof of the MMS bullet uses only those three conditions, and existence is Theorem 8. The Nash-social-welfare bullet of Theorem 14 is not posed: it depends on Lemma 12, which takes the allocation of an earlier paper as a black box. The goal cannot be trivialized by a free pool, by overlapping bundles, by zero agents (condition 3 excludes them), by a junk maximin share over zero bundles, or by natural-number division; the statement keeps all three conditions, each of which is needed.
Contributions welcome: a library-quality maximin-share API for additive valuations (attainment of the maximum, monotonicity, the proportional bound), which is reusable for other MMS results; proofs of the milestones; and the final assembly.
The quantum linear systems problem asks, given a sparse Hermitian matrix with condition number and a procedure preparing a state , to prepare a state close to . Harrow, Hassidim and Lloyd (2009) gave a quantum algorithm whose running time is polynomial in and but grows like in the target precision , because it estimates eigenvalues by phase estimation. Childs, Kothari and Somma (arXiv:1511.02306, SIAM J. Comput. 46(6), 2017) reduced the precision dependence to , an exponential improvement.
The reduction has two parts. A quantum part implements a linear combination of unitaries applied to , and turns any function that is -close to on the spectrum of into an approximate preparation of the solution state (Corollary 10 and Proposition 9 of the paper). An analytic part supplies such a function with small degree and small coefficient weight. The paper gives two analytic constructions: a Fourier expansion (Section 3) and an expansion in Chebyshev polynomials (Section 4). This mission formalizes the analytic core of the Chebyshev construction, the input to the paper's Theorem 4. The quantum algorithms and their query and gate counts are not formalized here.
For a real number (a condition number: the ratio of the largest to the smallest singular value), the domain is
A function is -close to on a set if for all .
The Chebyshev polynomials of the first kind are , and ; those of the second kind satisfy the same recursion with , .
For natural numbers let
the probability of more than heads in fair coin flips. The tamed inverse (74) is , and the odd Chebyshev series is
In Lean these are Dκ, coeff b j, fTamed b, and chebSum b n in the namespace QuantumLinSys.Chebyshev; bOf κ ε and j0Of b ε are the parameters and below.
With and , the truncated series
is -close to on , for every and .
Two further statements of the same approach are included as companion theorems: Lemma 16 (p. 17), the closed form of the -th power of the rotation block in terms of and , and Proposition 9 (p. 9), the perturbation bound for normalized states.
Lemma 14 provides a polynomial of degree whose Chebyshev coefficients have total weight , approximating uniformly on the region where a well-conditioned matrix has its eigenvalues. Applied to a Hermitian matrix through a quantum walk, whose powers implement (Lemma 16), it gives the query complexity of Theorem 4. The same polynomial approximation of reappears in later work on quantum singular value transformation and matrix inversion.
All results of this mission are proved in the paper. None of them is machine-checked in Mathlib or on the platform, as far as a search found: Mathlib has the Chebyshev polynomials and the identity , but no Chebyshev expansion of a rational function, no binomial tail bound in this form, and no approximation theorem for . The formalization produces a checked uniform approximation of with explicit, non-asymptotic parameters.
The exact identity (Lemma 18) has no slack: every coefficient, sign and summation bound of (77) must be right for all , and an off-by-one in the inner sum or in the Chebyshev index makes it false. Mathlib's Chebyshev library offers evaluation facts but no expansion of a given polynomial in the Chebyshev basis. The bound (89) is a Chernoff–Hoeffding tail bound for a symmetric binomial distribution, which must be stated for sums of binomial coefficients rather than for random variables. The goal then needs both approximation errors at the page's specific parameters, including the corner cases in which or is negative.
All functions are real functions of one real variable. Chebyshev polynomials are Mathlib's Polynomial.Chebyshev.T ℝ and Polynomial.Chebyshev.U ℝ, indexed by integers. The sum is over Finset.range n, so the series of (55)/(88) truncated at is chebSum b (j₀ + 1) and the full series (77) is chebSum b b.
The formalization commits to the following conventions, each disclosed in the item it affects.
A trivializing reading is ruled out: the goal fixes the page's , and constant , so neither an arbitrarily large truncation nor a weaker constant satisfies it, and the domain excludes the origin, where Lean's would make closeness to meaningless.
Useful infrastructure, reusable beyond this mission: Chebyshev expansions of polynomials on , binomial tail bounds, and uniform approximation of . Contributions of general lemmas of this kind are welcome.
Allocating indivisible goods fairly is difficult because a single good can change how an agent compares two bundles. Exact envy-freeness can be impossible (one good, two agents), so the field works with relaxations. Envy-freeness up to any good (EFX) requires each agent to prefer her own bundle to every other agent's bundle after any one good of that other bundle is removed. Whether EFX allocations of all goods always exist is open; the question motivates weakening the requirement that every good be assigned, and asking how little must be left over. Chaudhury, Kavitha, Mehlhorn and Sgouritsa show that leaving a small, unenvied set of goods unallocated (donated to "charity") suffices for every normalized monotone valuation profile (arXiv:1907.04596v3, Theorem 8, pp. 11–12).
Timeline (as recounted on pp. 2–3 of the source):
The two bounds matter separately. The empty allocation is EFX and donates everything; a cardinality bound alone still lets the donated goods carry most of an agent's value; the value bound alone allows almost all goods to be donated. The paper's later maximin-share and groupwise-maximin-share guarantees (Theorems 14 and 16, treated in the next missions of this series) are derived from exactly the allocation produced here.
There are agents, indexed by in the paper, and a finite set of indivisible goods. Agent has a valuation . It is normalized if and monotone if implies . No additivity, submodularity or substitutes condition is assumed. These are the general valuations of §1.1.1, p. 3, and §2 of the source.
A partial allocation consists of pairwise disjoint bundles . Its pool is the goods not assigned to anyone,
The allocation is EFX when
The paper calls allocations partial by default (p. 3, footnote 5). The envy graph has the agents as vertices and an edge when . A source is a vertex with no incoming edge. Its reachability component includes itself. The social welfare of is . These notions are introduced on pp. 8–9 of the source.
For a set of goods, an envied set is one some agent values more than her own bundle. An inclusion-wise minimal envied subset is envied, but no strict subset of is envied by anyone. An agent who envies such a is a most envious agent of ; the paper allows ties. The three update rules U0, U1 and U2 use these sets to change an allocation while maintaining EFX (Definition 3 and Algorithm 2, p. 9).
The goal is the allocation guarantee of Theorem 8:
Both the stronger source-count bound and its consequence are stated. The theorem asserts existence for every normalized, monotone valuation profile, including nonadditive profiles. It does not require the returned envy graph to be acyclic; acyclicity is an invariant used during construction, rather than an additional advertised property of the final allocation.
The attack path consists of the paper's numbered Lemmas 2, 4, 5, 6 and 7. Lemma 2 concerns removal of envy cycles; its Lean form keeps the page's conditional "if is EFX then is EFX" and the unconditional strict welfare increase. Lemma 4 records what U0 does and what its failure implies. Lemma 5 records U1's welfare and EFX guarantees. Lemma 6 supplies the finite source, good and agent data required for U2. Lemma 7 states U2's welfare and EFX guarantees. Their source wording and page locations appear in the milestone list; the Lean statements include the exact allocation updates where those lemmas rely on them.
The theorem guarantees a partial EFX allocation even for general monotone valuations, while limiting the unallocated pool more tightly than the number of agents: its size is below the number of unenvied agents. Every agent also values that entire pool no more than her own bundle. These two bounds distinguish the allocation from a merely EFX partial allocation. They provide the starting point for the paper's later statements on approximate maximin shares under additive valuations (Theorems 14 and 16).
The mathematical result is proved in the paper. The mission asks for a machine-checked proof of its allocation guarantee and of the supporting lemmas, with a reusable Lean account of finite partial allocations, the unallocated pool, envy graphs, minimal envied subsets and the update rules. Such definitions are useful for other fair-division questions involving unallocated indivisible goods.
EFX must hold after the allocation is changed, for every agent pair and for removal of every good from the other agent's new bundle. Simply giving a pool good to an agent may violate that condition, even though it makes the pool smaller. Conversely, replacing a bundle with an envied subset can improve welfare while returning goods to the pool. The source-count bound depends on controlling both kinds of progress. Rule U2 adds a further complication: its bundle moves follow envy paths, so an overlap between selected paths would make the new allocation ambiguous. These are the points at which the straightforward approach of distributing the remaining goods one at a time stops working.
Lean represents agents by Fin n, goods by Fin m, bundles by finite sets of goods, and valuations by real-valued functions on bundles. The paper's one-based subscripts become zero-based Lean indices. Nonnegative values need no separate hypothesis: normalization and monotonicity imply them. The hypothesis is explicit because the paper presumes agents and the strict bound is false when . The pool is computed as the complement of the union of pairwise disjoint assigned bundles. It is never a free set. EFX ranges over every pair , including , and every good of .
The minimal-envied-subset definition checks every strict subset against every agent. The most envious agent is a relation, allowing the paper's arbitrary tie choice. Reachability includes a path of length zero. U2's new allocation is calculated from its paths and chosen subsets. Lemma 6 includes Algorithm 1's acyclic-graph invariant and the ordering property established in its proof. It replaces the printed threshold with , the exact number of fresh goods its construction needs and the threshold used by the goal. Lemma 7 takes that ordering property to make path assignments unambiguous.
The printed U2 pool expression in Algorithm 2, line 13, is malformed; the formal statement uses the pool of the constructed allocation and the corrected union of leftover goods. Theorem 8's final sentence also asserts an iteration bound. This mission poses the allocation conclusions, while a future run-level formalization would be needed to state and check the iteration count. The paper's preceding count of U1/U2 steps and successive U0 steps does not by itself imply the printed number. Definitions and the numbered lemma statements are welcome contributions; a purported proof that uses a free empty pool, overlapping bundles, zero agents or an arbitrary replacement allocation would not establish this target.
Mobile devices run applications whose computational load can exceed what the device itself can serve in reasonable time and with reasonable battery drain. Computation offloading sends part of that load elsewhere: to a cloudlet, a small cluster of servers one wireless hop away, or to a distant cloud reached through the wide-area network. The cloudlet is shared, so its response time depends on how much load all users send to it, and each user's best offloading decision depends on everybody else's. Cardellini, De Nitto Personé, Di Valerio, Facchinei, Grassi, Lo Presti and Piccialli (Math. Program., 2016, DOI 10.1007/s10107-015-0881-6) model this as a non-cooperative game between users and study it with the tools of variational inequalities.
The game is a generalized Nash equilibrium problem (GNEP): not only the costs but also the feasible sets of the players depend on the other players' choices, because all users share one capacity constraint on the cloudlet. GNEPs with a shared convex constraint (jointly convex games) can be reduced to a single variational inequality, a reduction the paper takes from Facchinei, Fischer and Piccialli (Oper. Res. Lett. 2007, DOI 10.1016/j.orl.2006.03.004); Facchinei and Kanzow survey the area (Ann. Oper. Res. 2010, DOI 10.1007/s10479-009-0653-x). This mission formalizes the first step of the paper's analysis: the game has an equilibrium.
There are users and three tiers (mobile device, cloudlet, cloud). User chooses the fractions of its tasks run on each tier. A profile is .
The data are reals (arrival rates divided by service or transfer rates), powers , the number of cloudlet servers, the offloadable fraction and a utilisation cap . Assumption A requires and every to lie in .
User 's private feasible set is
the shared constraint is , and the joint feasible set is . User minimises the mean response cost
over . A solution of the GNEP is a profile at which no user can lower its cost by a deviation that keeps the shared constraint satisfied.
The map stacks the users' partial gradients,
and solves the variational inequality if and for all . Such solutions are the variational (or normalized) solutions of the game.
Under Assumption A, and provided every is nonempty,
Milestones 3 and 5 give the goal; milestones 1 and 2 are what milestone 3 rests on, and milestone 4 is what milestone 5 rests on. The platform's Proved statement of Brouwer's fixed-point theorem (AGT.brouwer_fixed_point) is included as a reference item for milestone 5.
The result. Existence of an equilibrium is the precondition for everything else in the paper: the monotonicity of (Theorem 1), the reformulation with a cloudlet price as an extended game (Theorem 2), and the distributed algorithm whose convergence is Theorem 3. Proposition 1 also shows that variational solutions exist, which is the specific equilibrium the paper's algorithm computes.
Formalizing it. The result is proved in the paper, in three lines that cite two textbook theorems. The work here is to make those citations machine-checked for this concrete model: that the closed-form is indeed the stacked partial gradient, that each user's problem is convex despite the rational cost terms, that the VI-to-GNEP reduction holds, and that a VI on a compact convex set with continuous map has a solution. None of these steps is formalized in Mathlib for GNEPs; the last is a finite-dimensional Hartman–Stampacchia theorem, which Mathlib does not contain. No part of this paper has a machine-checked proof.
The obvious argument is to apply Kakutani's theorem to the best-response correspondence. With a shared constraint this needs lower semicontinuity of the feasible-set map , which is a separate argument, and Kakutani is not in Mathlib either. The VI route avoids it but has its own points. The cost has the rational terms and , and convexity and differentiability must be checked on the region where the denominators are positive; on a user's feasible set this needs Assumption A and the shared constraint, not the private constraints alone. The existence of a VI solution needs a fixed-point theorem on a compact convex set, and Mathlib has no Brouwer theorem. That is why the platform's statement of it is attached to this mission.
Users are Fin N (0-based) and tiers an inductive type Tier with three constructors; a profile is Fin N → Tier → ℝ. The inner product is the coordinatewise double sum (not Mathlib's sup norm on Pi types). The cost and are the paper's closed forms; is not defined as a derivative, so milestone 1 has content. Lean's makes both formulas junk where a denominator vanishes. Under Assumption A both denominators are positive on and at every point the GNEP definition compares, and milestone 1 assumes the two positivity conditions explicitly.
Standing hypotheses in every statement: Assumption A, , . Nothing is assumed of or the powers, as in the paper. Added hypothesis: every is nonempty, in the goal and in milestone 5. The printed proposition is false without it: if then , so . The condition is equivalent to . Milestone 4 adds convexity of to the paper's "continuous and compact".
Trivializing formalizations are ruled out: cannot be empty under the added hypothesis, is not a derivative by definition, no statement evaluates the cost at a point with a vanishing denominator, and the GNEP keeps the shared constraint in each player's feasible set (dropping it gives a different game, a NEP).
Contributions welcome: a finite-dimensional Hartman–Stampacchia theorem (reusable well beyond this mission), the general VI-implies-GNEP reduction for jointly convex games, and proofs of the model-specific milestones.
Steepest descent is the oldest method for unconstrained minimization: to minimize a smooth function , it moves from the current point along the negative gradient . It is the prototype of every first-order method, and its worst-case evaluation complexity — how many iterations it may need before the gradient norm drops below a tolerance — is the reference point against which faster methods are measured.
For a function that is bounded below and has a Lipschitz continuous gradient, steepest descent with a suitable step-length rule reaches within iterations (Nesterov, Introductory Lectures on Convex Optimization, 2004, p. 29). Whether this bound is tight on nonconvex problems remained open until Cartis, Gould and Toint (preprint 15 October 2009; SIAM J. Optim. 20(6), 2010) built explicit one-dimensional examples showing that it is essentially sharp. The same paper shows that Newton's method can be as slow, and that the bound of cubically regularized Newton methods is also tight; those results are the other missions of this series.
Timeline:
Let be twice continuously differentiable, bounded below, with a derivative that is bounded and Lipschitz continuous. The paper calls these standing assumptions AS.0. Write for the gradient.
Steepest descent with step lengths starts at and sets
The step lengths are only required to lie in a fixed interval (condition (2.6))
Such step lengths can be produced by a Goldstein–Armijo linesearch, which accepts a step when the decrease lies between and for fixed constants .
Fix and put . The mission's definitions (namespace SlowConvergence.SteepestDescent) record the paper's prescribed data: iterates xk, steps sk, values fk, gradients (gk), and the quintic pieces p with the quantities , , of (2.11)–(2.15).
For every , every and every step-length sequence with , there is satisfying AS.0 on all of on which the steepest descent run from has
No constant (Lipschitz constant, gradient bound, lower bound) is fixed in the goal; only its existence is asserted.
The result. Since is arbitrary, the example shows that the upper bound for steepest descent cannot be improved to for any under AS.0, even with a standard Goldstein–Armijo linesearch. It separates steepest descent from second-order methods with better worst-case bounds, and it is the template for the Newton and regularized-Newton examples of the same paper. A matching upper bound for gradient descent with step is formalized elsewhere on the platform (ShiOptRates.gd_exact_rate); together the two describe the complexity of the method up to the exponent .
Formalizing it. The result is proved on paper; to our knowledge no machine-checked version exists. The mission adds a statement in which the method, the function class and the iteration count are fixed precisely. It also corrects three printed slips that a formal check exposes: the iteration count is off by one, the Goldstein–Armijo interval is printed reversed, and an intermediate step of (2.17) is false while its end bounds hold.
Matching prescribed values and gradients at the iterates is easy one point at a time. The difficulty is doing it with uniform control. The interval lengths shrink like , so a naive interpolant has second derivatives growing with , and the gradient is then not globally Lipschitz. The prescribed values must also decrease at a rate whose sum stays finite, or the function is unbounded below. Both constraints pin the exponent: the construction works only because makes the iterates escape to infinity while keeps finite. A further step remains: the paper's function lives on and must be extended to all of without losing any property of AS.0.
The problem is one-dimensional: f : ℝ → ℝ, the gradient is deriv f, and the second derivative is iteratedDeriv 2. AS.0 is ContDiff ℝ 2 f, BddBelow (Set.range f), a global bound on |deriv f|, and LipschitzWith L (deriv f). Every property holds on all of ; the paper constructs on and says it extends smoothly to the negative reals, and that extension is part of the goal.
Conventions:
Real.rpow with base .Infrastructure needed: quintic Hermite interpolation on intervals, gluing piecewise polynomials into a function on along an unbounded increasing knot sequence, a extension to the negative reals, and bounds for real -series. The gluing lemma and the extension are reusable for the Newton and regularized-Newton missions of the series. Contributions of any milestone, of a construction of the glued function of (2.16), or of a direct proof of the goal are welcome.
Quasi-Newton methods replace a costly exact Hessian with an operator updated from successive changes in position and gradient. A secant update must map the observed step to the observed gradient difference . Many operators satisfy that one equation, so the choice of update needs another criterion. Gilbert and Lemaréchal's working paper studies variable-storage quasi-Newton algorithms and, in its Annex, characterizes familiar update formulas by how little they change the previous operator. The Annex treats real Hilbert spaces, rather than only matrices on Euclidean space, and allows the underlying scalar product and the weighting operator to vary. Its least-change characterization is the subject of this mission.
The source is the August 1988 IIASA Working Paper WP-88-121. A revised journal article appeared in 1989, but the theorem numbers and printed page references here belong to the working paper. The work is a formalization of a result proved in that paper; the mathematical question is not open.
Let be a complete real inner-product space. A continuous linear operator is the current Hessian approximation. A step and a gradient difference determine the quasi-Newton equation for the updated operator . Write , where is the perturbation. The source restricts to the Hilbert–Schmidt class , so its size can be measured by an orthonormal basis :
The index set need not be countable; membership in means the displayed family is summable. The value is independent of the chosen orthonormal basis. For , the paper's bracket operator is . The order of its arguments matters.
The nonsymmetric feasible set is . For a self-adjoint , the symmetric problem uses . A bijective continuous operator weights the symmetric objective . The vector records how this weight changes the update. Both the feasible set and the weighted objective matter: taking a minimum over every bounded operator would change the problem.
The goal is Proposition A.2 on printed p. 28 of the working paper. Suppose , is bijective, and . With and , define
The target asserts that belongs to and is the unique minimizer of over . Its formula depends on only through . No positivity condition on or on is part of this result.
The milestones follow the source's supporting statements in order. They establish that the Hilbert–Schmidt sum is independent of the orthonormal basis and defines a norm on its domain; that the operator norm is bounded by this norm and the Hilbert–Schmidt class is stable under multiplication by bounded operators; the bracket identity ; the two bracket composition identities; Proposition A.1, the unique nonsymmetric least-change update for ; and its instance , Broyden's update (A.5). The goal adds self-adjointness and a single two-sided weight.
The Annex then draws consequences of the goal, which are further milestones: the instance is the psb (Powell symmetric Broyden) update; Proposition A.3 states that for nonzero a self-adjoint positive operator ( for ) with exists if and only if for a bijective , if and only if ; with the weight becomes and (A.7) becomes the dfp (Davidon–Fletcher–Powell) update (A.8); and (A.9) is a product form of the dfp update from which its positivity follows when is self-adjoint positive and .
The theorem gives a precise optimization property to a rank-two symmetric secant formula. It identifies the operator selected by the weighted least-change criterion and guarantees there is no other feasible minimizer with the same value. Taking the weight to be the identity yields the psb update, and taking with yields the dfp update, so two of the classical symmetric secant formulas are least-change updates for different weights. Proposition A.1 similarly characterizes the rank-one update that becomes Broyden's formula when its right weight is the identity. These consequences explain why the familiar formulas arise from a common variational question, as the Annex states.
The paper supplies a mathematical proof. The remaining formalization work is to represent the Hilbert–Schmidt class, its norm and ideal property, the weighted objectives, and the exact minimization claims in Lean, then prove those claims. Mathlib supplies Hilbert spaces, Hilbert bases, bounded linear maps, adjoints, and the rank-one operator corresponding to the paper's bracket. The statements drafted for this mission compile, but they carry sorry and have no machine-checked proof from this mission yet. A completed development would leave reusable Hilbert–Schmidt and rank-one operator results beyond this quasi-Newton application.
The secant equation alone fixes an operator on only one vector. Even in two dimensions, a rank-one perturbation can satisfy that equation while failing to preserve self-adjointness. Requiring self-adjointness leaves many candidates, and minimizing the two-sided weighted Hilbert–Schmidt norm must distinguish exactly one of them. In infinite-dimensional spaces the norm also has a domain: some bounded operators have an infinite square sum. A formulation that silently assigns a finite default value to a nonsummable operator could turn the least-change claim into a different assertion. These are the mathematical and formal obstacles the milestone list exposes.
Lean uses an arbitrary complete real inner-product space, with no finite-dimensional or separability assumption, and an arbitrary HilbertBasis index type. Each theorem takes a basis parameter; the basis-independence milestone states why this represents the paper's basis-free norm. The reusable definitions for the bracket and the Hilbert–Schmidt square sum are separate from the paper-specific feasible sets. bracket u v abbreviates Mathlib's rankOne ℝ u v, with paired with the input. A bijective bounded operator is represented by a continuous linear equivalence ; the bounded inverse theorem makes this equivalent to the paper's bijective member of . The definition of applies the adjoint of to .
Lean's real tsum has a default value when the family is not summable, so the Hilbert–Schmidt norm is used as a norm only for operators satisfying the explicit summability predicate. Both and include that predicate. The ideal-property milestone covers the weighted operators in the two objectives. The hypothesis is exactly the proposition's condition; it entails , so no extra nonzero-denominator hypothesis is imposed. The statement spells out “unique solution” as feasibility, minimality over every feasible perturbation, and equality of every feasible minimizer with . The paper prints “problem (A.5)” in Proposition A.2, but (A.5) labels Broyden's displayed formula; its preceding paragraph defines the relevant symmetric minimization as (A.6). This mission formalizes (A.6).
In Proposition A.3 and (A.9), "positive" is the paper's strict notion for , not the non-strict positivity of Mathlib. The identity (A.9) is stated for self-adjoint and , the setting of the Annex's symmetric problem; the paper's sentence before the psb formula repeats the "(A.5)" misprint and is read as (A.6) in the same way.
The definition layer, basis independence, operator-ideal property, bracket results, both least-change propositions, and the Broyden, psb, dfp and positivity statements are welcome proof targets. The scaling results of §4.1 are outside this mission.
Modular composition asks, given univariate polynomials over a ring, for . It is the bottleneck step in the classical algorithms for factoring univariate polynomials over finite fields (Cantor–Zassenhaus, von zur Gathen–Shoup, Kaltofen–Shoup), for irreducibility testing and for computing minimal polynomials. Brent and Kung (1978) gave an algorithm using operations for degree , and for three decades no algorithm with a near-linear operation count was known in general.
Kedlaya and Umans (Dagstuhl Seminar Proceedings 08381, 2008; journal version SIAM J. Comput. 40(6), 2011, doi:10.1137/08073408X) obtained near-linear modular composition over finite fields, and with it asymptotically faster algorithms for factoring polynomials over finite fields. Their route has two halves: a reduction of modular composition to multivariate multipoint evaluation (Section 3), and new fast algorithms for the latter (Sections 4 and 6). This mission formalizes the correctness of the first half, Theorem 3.1. The paper notes that Shoup and Smolensky used essentially the same transformation in an unpublished 1992 manuscript.
Throughout, is an arbitrary commutative ring. Variables are indexed from .
MULTIVARIATE MULTIPOINT EVALUATION (Problem 2.1): given with individual degrees at most and points , output .
MODULAR COMPOSITION (Problem 2.2): given with individual degrees at most , and of degree at most with the leading coefficient of a unit, output , the unique with and .
The inverse Kronecker map (Definition 2.3) is the -linear map that sends the monomial to , where is the base- expansion. It trades individual degree for number of variables: every individual degree of is below .
The algorithm of Theorem 3.1 takes , sets and , receives points whose differences are units, and
for all , , with individual degrees , of degree with a unit, and distinct with unit differences. The right-hand side is stated through the characterization of the remainder (divisibility by and degree below ).
A supporting theorem states that the interpolation formula over a commutative ring (Figure 1) recovers every polynomial of degree from its values at nodes with unit differences.
Theorem 3.1 says that modular composition is no harder than one multivariate multipoint evaluation with variables, individual degrees below , and points, up to quasi-linear univariate work. Combined with the paper's fast multipoint evaluation algorithms this gives modular composition over in bit operations, and from there the paper's improved bounds for polynomial factorization, irreducibility testing, minimal polynomials and modular power projection (Sections 7–8). The converse reduction (Theorem 3.3) shows the two problems are essentially equivalent.
The paper's proof of correctness is a short paragraph; the operation counts are the paper's main concern. This mission makes the correctness exact: the algorithm is defined step for step, and its output is proved equal to the specification. As far as the platform's corpus shows, neither the inverse Kronecker map nor this reduction has a machine-checked statement; the running-time half is not part of this mission.
The obvious argument substitutes for and invokes the inverse Kronecker identity. Two points keep this from being immediate. First, is linear but not multiplicative, and it discards base- digits beyond position ; the identity holds only for individual degrees at most , which here requires . Second, the algorithm never sees itself, only its values at points: interpolation recovers it only if its degree is below , which is why Step 2 reduces modulo before substituting, and interpolation over a ring (not a field) needs the unit-difference hypothesis throughout. Mathlib's Lagrange interpolation is stated over fields, so the ring version must be handled directly.
CommRing R); there is no field or nontriviality assumption.Fin m; the new variables are Fin m × Fin ℓ; points are Fin N'.MvPolynomial.degreeOf; "degree at most " is natDegree ≤ N - 1.Nat.clog d₀ d and ; is not a free parameter.Ring.inverse of the node differences.MvPolynomial.eval, which is exactly the output of Problem 2.1.Step 5 is the interpolation formula applied to the computed values and nodes alone; it is not defined as the polynomial , and the goal is the six-step output, not the congruence alone, so the statement cannot be closed by unfolding definitions.
Useful infrastructure, reusable beyond this mission: base- digit manipulation of exponent vectors, Lagrange interpolation over commutative rings with unit node differences, and remainders modulo polynomials with unit leading coefficient. Proofs of any milestone, and of the supporting interpolation theorem, are welcome independently.
Many objectives in statistics and machine learning are neither smooth nor convex, yet are well behaved in a weaker sense: robust phase retrieval, blind deconvolution, robust PCA and training with piecewise-linear losses all lead to weakly convex functions, functions that become convex after adding a fixed quadratic. For such functions the plain subgradient method remains the method of choice, and the natural question is how fast it reaches approximate stationarity. Davis and Drusvyatskiy (SIAM J. Optim. 2019) gave the first such rate, measured by the gradient of the Moreau envelope, of order .
Das Gupta, Van Parys and Ryu (Math. Program. 204 (2024) 567–639) introduced BnB-PEP, a branch-and-bound method for solving nonconvex performance-estimation problems to global optimality, and used it to construct optimal and efficient first-order methods. Their one fully analytical result (§6.3) is a new potential-function analysis of the subgradient method on weakly convex functions with bounded subgradients. It produces an explicit stepsize and a rate that strictly improves on the Davis–Drusvyatskiy bound for all large enough . The certificate was found numerically; the paper then gives a classical proof that can be checked by hand. This mission formalizes that result.
Work in with the Euclidean norm. A function is -weakly convex if is convex. For such , a vector is a subgradient of at , written , when
The class consists of the -weakly convex whose subgradients all satisfy . Since exactly when , the paper sets and writes ; here the normalized bound is written (Lean: InWeakClass 1 L f, with subgradients IsWeakSubgrad 1 f x g).
For the proximal point is the unique minimizer of , and the Moreau envelope is the minimum value
(Lean: SAGA.Convex.IsProxPoint f (1/ρ̂) x y and moreauEnv ρ̂ f x). The envelope is continuously differentiable, and its gradient is a subgradient of at the prox point . With , the paper's choice, small means that is near a point that is nearly stationary for .
The method is for , where each is arbitrary. One writes , , assumes a global minimizer and the initial condition , and sets .
For the stepsize , provided ,
The bound holds for every choice of subgradients along the run.
For , , and , the potentials satisfy
In proof order: the Moreau-envelope facts of §6.3.1; the one-step inequality (32) for an arbitrary point; the telescoping display after (32); the closed form (44) of with nonnegativity; Theorem 1; the closed form (45) of its bound in ; the majorant (46) with Bernoulli's upper bound; and the minimizer of (46) with its value.
The result. Corollary 1 gives an explicit, non-asymptotic rate for the most basic method of nonsmooth nonconvex optimization, with explicit constants and an explicit stepsize. As the bound is asymptotic to , and the paper shows it is strictly below the earlier bound once . It also bounds . It shows that computer-assisted performance estimation can produce closed-form guarantees beyond the convex, interpolable function classes where PEP is usually applied.
Formalizing it. The result is proved on paper twice (pp. 622–627), but nothing about weakly convex functions, their subdifferential or the Moreau envelope in the nonconvex regime is formalized on the platform, and the convergence analysis has not been machine-checked. A complete development formalizes the potential-function proof and supplies reusable facts about weakly convex functions and the Moreau envelope.
The scalar part of the argument ((44)–(46) and the plug-in) is elementary algebra and one Bernoulli inequality. The analytic weight sits in two places. First, the Moreau envelope of a nonconvex function: showing that the real infimum is attained at the prox point, that the envelope is differentiable with gradient , and that this gradient is a subgradient of at with the weak-convexity modulus (not the modulus that the prox inequality gives directly). Second, inequality (32): it is not a consequence of convexity, since is not convex, and it must hold for an arbitrary current point and an arbitrary subgradient, with parameters fixed in advance. The obvious route through descent of itself fails: need not decrease for nonconvex , which is why the potential uses the envelope at the iterates.
The carrier is EuclideanSpace ℝ (Fin d), and is real-valued and defined everywhere. The weak-convexity modulus is normalized to , and the Lean name L is the paper's ; the general class follows by scaling and is not stated. The subdifferential is the weak-convexity inequality above. For weakly convex it equals the Clarke, Fréchet and limiting subdifferentials, so it is the paper's abstract in every admissible instance. The convex subdifferential of is not used: it can be empty for nonconvex and would make the statements vacuous. The run is given by sequences x g y : ℕ → E, with g k an arbitrary subgradient at x k for , and y k tied to x k by IsProxPoint f (1/2) for . is not free: it is . The Moreau envelope is a real ⨅; it is finite and attained in this regime, and the first milestone proves this. The parameters of Theorem 1 are pinned by hypotheses, not chosen existentially.
Two hypotheses are made explicit. Corollary 1 is stated "in the setup of Theorem 1", which requires ; for the prescribed stepsize this is , and it is carried as the hypothesis . It fails for and whenever is large relative to . Inequality (32) is stated for one arbitrary step, under the nonnegativity of the alternate proof's weights (, , ). The minimizer is assumed, as in the paper; the remark on p. 627 that suffices is not used.
Useful contributions include basic lemmas on weakly convex functions (existence of subgradients, strong convexity of the prox subproblem), differentiability of the Moreau envelope for , the weighted-sum identity behind (32), and Bernoulli's upper bound for .
Nash's existence theorem for finite games is a fixed-point theorem: one writes down a continuous map from the set of mixed strategy profiles to itself whose fixed points are exactly the Nash equilibria, and applies Brouwer's theorem. Nash's own map (Nash 1951) divides by , and the choice of map matters as soon as the question is computational rather than existential.
Etessami and Yannakakis (SIAM J. Comput. 39 (2010)) introduce the class FIXP of fixed-point search problems whose maps are given by algebraic circuits over and rational constants, and show that computing a Nash equilibrium of a 3-player game is FIXP-complete. In Section 4 they ask which gates are really needed. Since the Nash problem is complete, it suffices to find, for every game, a map with the same fixed points and a cheaper circuit. They define a division-free map , prove that its fixed points are precisely the Nash equilibria (Lemma 20), show that it is computed by a circuit with gates (Lemma 21), and conclude that FIXP is unchanged if circuits use only and rational constants (Theorem 22). The same map, defined as a Euclidean projection, appears earlier in Gul, Pearce and Stacchetti (1993).
This mission formalizes the game-theoretic content of that section: the map , its well-definedness, and Lemma 20.
A finite game has a finite set of players ; each player has a finite, nonempty set of pure strategies, and a payoff function assigns a real number to every pure strategy profile. A mixed strategy of player is a vector with and ; a mixed profile is one mixed strategy per player, and denotes the set of mixed profiles (the product of the players' unit simplices). The expected payoff is the expectation of when the players draw their strategies independently according to . For , is player 's expected payoff when plays and the others play according to . A Nash equilibrium is a mixed profile such that no player can raise by switching unilaterally to another mixed strategy.
For a vector indexed by pairs , let and . For each player define the function of a real variable
It is continuous, nonincreasing, strictly decreasing below and zero above it, so there is a unique threshold with . The division-free map is
In the Lean development, is DGPNash.NashMap.purePayoff u x i j, is hVal, is fSum, is threshold and is G, all in the namespace FixpNash.DivFree.
For every finite game with nonempty strategy sets and every ,
This last milestone is off the goal's path; it is the formula behind the division-free circuit.
Lemma 20, with Brouwer's theorem and the continuity of , gives an elementary proof of Nash's theorem. With Lemma 21 it shows that the Nash equilibrium problem, and therefore every FIXP problem, is represented by circuits without division; the paper uses this to obtain Theorem 22. The pure-deviation criterion of milestone 3 is the standard test for equilibria and is used throughout equilibrium computation. The closed form of milestone 6 is the threshold of the Euclidean projection onto the simplex, used widely in optimization.
All of these results are proved in the paper. The mission produces machine-checked versions. No platform item states Lemma 20 or the pure-deviation criterion for AGT.IsMixedNash. Related posed items, with other conventions, are credited below rather than reused: the thresholds of the simplex projection in the Condat 2015 series (SimplexProj.Condat.simplex_projection_threshold, threshold_root_bracket, subsequence_mean_le_threshold, stated for the projection on with a radius), and the best-response fixed-point characterization in supermodular games (Supermodularity.Games.equilibrium_iff_fixed_point_v2, a different map). The paper also remarks, without proof, that is the point of closest to . That remark is not a target here.
The map is defined through an implicitly determined threshold. In the formalization the threshold has to be a definition that does not depend on a proof, and every statement about it rests on the existence and uniqueness of the root of . This is an intermediate-value argument for a piecewise linear function of a finite sum of terms. Its strict monotonicity holds only below , and the argument must use that is nonempty.
The equivalence itself needs the multilinearity of the expected payoff: and, more generally, the payoff of a deviation to a mixed strategy is . In the agt_games representation the expected payoff is a sum over all pure profiles of products of probabilities, so this identity must be extracted from the product structure rather than read off.
The game uses the published agt_games vocabulary: players form a finite type ι with decidable equality, the strategies of player i a finite type S i, payoffs are real (the paper's are rational, so this is a generalization), mixed profiles are real weight functions satisfying AGT.IsMixedProfile, and Nash equilibrium is AGT.IsMixedNash (no profitable deviation to any lottery). The pure-strategy payoff is the published DGPNash.NashMap.purePayoff.
The following readings are explicit in the Lean and implicit on the page:
∀ i, Nonempty (S i)). The paper assumes this tacitly; without it is empty and does not exist;AGT.IsMixedNash and the pure-deviation inequalities for a mixed profile;Contributions welcome: proofs of any milestone. The multilinearity of AGT.expectedPayoff in one player's strategy, and the existence and uniqueness of the threshold of a finite sum of hinge functions, are reusable beyond this mission.
Reductions that prove hardness for Nash equilibrium computation encode a computation (a circuit, a fixed-point problem) into the probabilities that players put on their strategies in every equilibrium. For the encoding to be meaningful, the designer has to control how each player distributes probability across groups of strategies, independently of the incentives that carry the computation. A standard tool for this is a generalized matching pennies game: each "computing" player is paired with an adversary who is penalized for guessing which group the computing player is playing, and who therefore forces that player to spread probability evenly over the groups. Versions of this device appear in the PPAD-hardness reductions of Daskalakis, Goldberg and Papadimitriou and of Chen and Deng, and in Etessami and Yannakakis's Theorem 4, which reduces the SQRT-SUM and PosSLP problems to deciding, with a promised gap, whether the unique Nash equilibrium of a 4-player (or 3-player) game plays a given pure strategy (Etessami–Yannakakis, SIAM J. Comput. 2010).
This mission formalizes the version of the device that Etessami and Yannakakis isolate as Lemma 6 (p. 24 of the authors' manuscript), with the explicit constants of their construction.
A finite game has a finite set of players; each player has a finite set of pure strategies, and receives payoff at each pure profile . A mixed profile assigns to each player a probability vector on ; players randomize independently, and is 's expected payoff. Write for the expected payoff of when plays the pure strategy and everyone else plays according to . A Nash equilibrium is a mixed profile such that no player can raise their expected payoff by switching unilaterally to another mixed strategy.
Fix two players . The pure strategies of are partitioned into blocks, in one-to-one correspondence with the pure strategies of . This is recorded by a surjective map : the block of a strategy of corresponds to the strategy of . The total probability of block under is
The payoffs of have the block matching-pennies form with first term , constant and parameter when
does not depend on , , and has at most strategies. Player is rewarded for "matching" the strategy of with the block it plays; player loses when matched. The term is arbitrary otherwise: in the paper it carries the gate gadgets of the circuit.
For every Nash equilibrium of a game in which have the block matching-pennies form,
Part 1 says divides its probability evenly among its blocks (each block gets ); part 2 says the matching player uses every strategy.
In the paper, Lemma 6 is what makes every unprimed player of the 10-player game of Section 3 spread probability (or ) on each block, so that the split of probability inside a block can carry the value of a circuit gate, and the gate gadgets of Lemma 7 act on correctly normalized quantities. Without it, the gadgets' analysis does not apply. The lemma is stated for an arbitrary game containing such a pair, so it is reusable for any reduction that pairs computing players with matching-pennies adversaries.
The result is proved in the paper; nothing in it is open. As far as the platform and its index show, no machine-checked version exists: the platform has the 2×2 matching pennies game (PotentialGames.matchingPennies_no_pureNash, which shows it has no pure equilibrium) and our CalibratedCE.Convergence.MatchingPennies (Foster–Vohra's example), neither of which is the block game. This mission produces a checked version of the lemma with the paper's constants, together with the support property of mixed Nash equilibria for the agt_games vocabulary, a basic fact other game-theory missions can import.
The argument is short; the difficulty is in the accounting. The expected payoff of a pure strategy of mixes the arbitrary term , evaluated under the product distribution of all other players, with the matching term, which depends only on . Separating the two requires that depends only on and that the expected-payoff sum factors over independent players. The constants also interact: the lower bound uses that has at most strategies, so that some strategy of has probability at least , and the comparison of the two bounds needs , which is exactly . A tempting shortcut, comparing only with the average block probability, does not identify which strategies of vanish; the argument goes through the set of maximum-probability blocks.
The game uses the published agt_games vocabulary: players and strategies are arbitrary finite types ι, S : ι → Type*, payoffs are real (u : ι → (∀ k, S k) → ℝ), mixed profiles are families of probability vectors, and AGT.IsMixedNash allows deviations to arbitrary mixed strategies. The pure-strategy payoff is the published DGPNash.NashMap.purePayoff. The block structure is a surjective map ; surjectivity is the "1-1 correspondence" of blocks with strategies of (an empty block would make the lemma vacuous). The definition item packages the form "given above" as FixpNash.Blocks.IsBlockPair.
Explicit readings of the page:
The degenerate case is allowed and reads . A formalization in which has no strategies, or a block is empty, would make the lemma vacuous; the surjectivity of and the definition of a mixed profile exclude this. Contributions welcome: proofs of the support property (reusable well beyond this mission), of the two payoff bounds (a factorization of the expected payoff over independent players), and of the lemma.
For games with three or more players, Nash equilibria can be irrational, so they cannot in general be computed exactly. Bubelis made this precise: any real root of any univariate polynomial arises as the probability of a particular strategy, or the payoff of a particular player, in a Nash equilibrium of a three-player game whose payoffs depend on the coefficients of the polynomial (Bubelis 1979).
Etessami and Yannakakis (SIAM J. Comput. 39 (2010)) restate Bubelis's construction as Lemma 7, in a form that controls the equilibrium probabilities rather than a payoff, and that guarantees the equilibrium is unique. They use it, for linear polynomials, as the single gadget behind every arithmetic operation in their reduction from PosSLP and SQRT-SUM to deciding properties of the unique Nash equilibrium of a three- or four-player game (their Theorem 4). The uniqueness clause is what makes the composed game itself have a unique equilibrium.
Fix an integer and real coefficients , and let
so is the coefficient of ; the leading coefficient may vanish.
The gadget is a game with three players. The primary player 1 has the strategies ; the auxiliary players 2 and 3 each have the strategies . For a pure profile , and with the indicator of a predicate , the payoffs are
The auxiliary payoffs do not depend on and take values in .
A mixed profile assigns to each player a probability vector on its strategies; the players randomize independently. Player 's expected payoff is the expectation of its payoff under the product distribution, and is its expected payoff when it switches to the pure strategy . A Nash equilibrium is a mixed profile in which no player can raise its expected payoff by switching unilaterally to any other mixed strategy. A profile is fully mixed if every pure strategy of every player has positive probability. Throughout, , and , are the equilibrium payoffs of players 2 and 3.
Assume , , and that has a unique root in . Then every Nash equilibrium of satisfies
and if and , then has exactly one Nash equilibrium, and it is fully mixed.
Milestones 2–4 hold for every coefficient vector; only milestone 5 and the goal use the hypotheses on .
The lemma is the arithmetic engine of the hardness results of Etessami and Yannakakis: a polynomial equation in one unknown is solved, exactly and uniquely, by the equilibrium of a fixed-size game whose auxiliary payoffs do not depend on the equation. With linear, the gadget implements addition, multiplication and division of probabilities in ; with higher degree it implements roots and fractional powers. Without the uniqueness clause, the composed games of Theorem 4 could have spurious equilibria, and the reduction would not apply to games promised to have a unique equilibrium.
The result is proved in the paper (pp. 25–26, following Bubelis). As far as is known, no part of it is machine-checked: there is no formal statement of Bubelis's gadget, and the support property of Nash equilibria is not on the platform in this vocabulary. This mission produces the first formal statement and proof of the gadget's equilibrium characterization, including the existence half of "has a unique Nash equilibrium", which the paper takes from Nash's theorem but which here is a concrete profile to check.
The gadget's equilibria are those of a three-player game, so the payoffs are cubic in the probabilities and no linear-programming argument applies. The obvious first idea, writing down the indifference conditions of players 2 and 3 and solving them, presupposes that every strategy of player 2 is played; nothing guarantees that in advance, and the profiles in which some strategies are unplayed have to be excluded. The boundary cases and are not covered by an indifference argument for the primary player and need the sign conditions and separately. The strategy of player 3 is pinned down only when , which is why the uniqueness part of the lemma excludes the endpoints. Finally, existence of the equilibrium is part of the statement and cannot be delegated to Nash's theorem, which is not available on the platform.
The game uses the published vocabulary agt_games (mixed profiles as weight functions, AGT.expectedPayoff, AGT.IsMixedNash with mixed deviations) and DGPNash.NashMap.purePayoff for . The players are a three-element type primary | aux2 | aux3; strategies are Fin 2 and Fin (m+1), 0-based as on the page. The coefficients are c : Fin (m+1) → ℝ and is the explicit sum with natural-number exponent; the congruence is addition in Fin (m+1); for every , including .
Explicit readings committed to:
∃! over mixed profiles);The goal is not trivialized by a pure-strategy notion of equilibrium (deviations are mixed), by dropping uniqueness of the root (without it is false), or by reading "unique equilibrium" as uniqueness alone. For the hypotheses cannot hold, as on the page.
A complete development needs the support property (reusable for any finite game), the linearity of expected payoff in one player's strategy, and finite-sum manipulations for the geometric weights . Contributions of general lemmas about AGT.IsMixedNash and purePayoff are welcome and reusable well beyond this mission.
Methods for smooth unconstrained minimization, , are compared by how many evaluations of and of its gradient they need, in the worst case, to reach an approximately first-order critical point, an iterate with . For steepest descent with a Lipschitz gradient the answer is (Nesterov, Introductory Lectures on Convex Optimization, 2004, p. 29). Nesterov and Polyak (2006) showed that globally minimizing a cubic regularisation of the second-order model, with the exact Hessian and a global Lipschitz constant, improves this to .
The adaptive regularisation with cubics (ARC) framework of Cartis, Gould and Toint makes that idea practical: the Hessian is replaced by an approximation , the Lipschitz constant by an adaptive weight , and the global model minimizer by any step that does at least as well as a Cauchy point. Part I (Math. Program. 127, 2011) proved global convergence; Part II (Math. Program. 130, 2011) counts evaluations. This mission covers the first count of Part II (§§2–3): with only the Cauchy condition on the step, ARC needs iterations, the same order as steepest descent and as trust-region methods (Gratton, Sartenaer and Toint, SIAM J. Optim. 19, 2008).
Let be continuously differentiable (AF.1), , and the Euclidean norm. At iterate , with a symmetric matrix and a weight , the cubic model is
Algorithm 2.1 (ARC) takes parameters , , and a starting point . At iteration it
For , and are the successful and unsuccessful iterations among . The complexity results use three assumptions: AM.1, for all ; AF.4, on an open convex set , with ; and a lower bound . Optionally, (2.10): on very successful iterations, for some . The constants are
Let with , and let be the first iteration with . Then
and, if (2.10) holds,
The constants are kept exactly as printed. The first bound counts gradient evaluations and the second counts all iterations, which is the number of function evaluations.
The corollary establishes that the ARC framework, whatever step it takes beyond the Cauchy point and whatever symmetric it uses, is never worse than steepest descent in evaluation count. It is the baseline against which Part II measures its second-order variant ARC(S), whose bound is the subject of a separate mission in this series. Theorems 2.1 and 2.2 are generic: they convert any per-iteration model decrease and any bound on into iteration counts, and are reused verbatim for ARC(S).
The results are proved in the paper. No machine-checked proof of any of them exists on Prove2Me or, to our knowledge, elsewhere. The work here is to formalize the known proofs: the Cauchy-point analysis of Part I (quoted, not reproved, in Part II), the Taylor-remainder estimate of Lemma 3.2, and the counting arguments. Formalizing also checks the printed statements: two of them need a small correction (see Formalization scope).
Each step is elementary, but the statements are about a nondeterministic algorithm: and are choices, so every bound must hold for all admissible choices, not for one convenient run. The constants are explicit, and the ceilings interact: the printed proof of (3.17) adds the ceilings of (3.15) and (3.22), which does not by itself give ; the bound must be derived from the unrounded estimates. Lemma 3.1 i) requires a careful one-dimensional analysis of with an indefinite . The ratio is a quotient, and its denominator must be shown positive before any comparison with , is meaningful.
The space is EuclideanSpace ℝ (Fin n); is Mathlib's gradient f; is a continuous linear operator with IsSelfAdjoint, and is the operator norm. A run is a predicate IsARCRun on the sequences ; the Cauchy condition is stated as for all , which is equivalent to comparing with the Cauchy point and avoids defining an argmin. The run is infinite; a run that the paper would stop at extends trivially, and every statement only concerns iterations with . Lean's x / 0 = 0 gives (unsuccessful) when ; Theorem 2.2 assumes (2.6), , up to its horizon, and §3's results need nothing extra because makes the denominator positive.
"" is stated as: every with for all satisfies (and similarly for ). This asserts that is finite without presupposing it. Statements with are given for every finite .
Two corrections to the printed text are built in. In Theorem 2.1 the bound is assumed for : as printed () the theorem fails for , iteration unsuccessful, . In AF.4 the set must contain the trial points as well as the iterates, because Lemma 3.2 applies the Lipschitz bound on the segment .
A trivializing formalization is ruled out: the goal quantifies over every admissible step and weight update rather than one particular choice, keeps (2.10) out of the first conclusion, and keeps every constant as printed rather than replacing it by an existential.
A complete development needs the one-dimensional cubic analysis behind Lemma 3.1, a mean-value bound for functions along a segment, and finite counting over Finset.range. The generic counting results (Theorems 2.1, 2.2) are reusable for every ARC variant. Proofs of any milestone, and of the goal from the milestones, are welcome.
Nash proved that every finite game has an equilibrium by exhibiting a continuous map of the set of mixed profiles into itself whose fixed points are exactly the equilibria, and applying Brouwer's fixed point theorem (Nash, 1951). Computationally, the same map is the bridge between games and fixed-point problems: complexity classes for total search problems such as PPAD (Papadimitriou, 1994) and FIXP (Etessami and Yannakakis, 2010) are defined through fixed points, and a game problem is placed in such a class by passing through Nash's map.
For three or more players, equilibria can be irrational, so algorithms produce approximations. Two different notions compete. An -Nash equilibrium is a profile at which no player can gain more than by deviating unilaterally; a weak -approximate fixed point of Nash's map is a profile that the map moves by less than in every coordinate. Proposition 3 of Etessami and Yannakakis shows that the two notions are interchangeable up to polynomially related tolerances. Since weak approximate fixed points of polynomially continuous, polynomially computable maps can be found in PPAD (their Proposition 2), this gives the membership of -Nash equilibria in PPAD, first observed by Daskalakis, Goldberg and Papadimitriou (2009) and by Papadimitriou (1994).
A finite game in normal form has a finite set of players; each player has a finite nonempty set of pure strategies and a payoff function on the pure strategy profiles . A mixed profile assigns to each player a probability vector ; is the set of mixed profiles. The expected payoff of player is , and is the expected payoff of when plays the pure strategy and every other player keeps its mixed strategy. The gain of switching to is
Nash's function is
A profile is an -NE if for every player and every mixed strategy of . A weak -approximate fixed point is an with .
The proof uses three constants of the game: , the maximum number of pure strategies of a player; , the maximum over players of ; and .
is an -NE.
The result says that the "almost at equilibrium" notion of approximation and the "almost fixed" notion attached to Nash's map are the same notion up to polynomial changes of tolerance. It is the reason the weak approximation problem for Nash's function inherits PPAD membership from Proposition 2 and conversely why PPAD-hardness of -NE transfers to weak approximation. The paper contrasts it with strong approximation (being close to an actual equilibrium), which it shows to be much harder; the explicit tolerances make precise which of the two notions a fixed-point algorithm for Nash's map actually delivers.
The result is proved in the paper. To our knowledge neither direction is formalized. On Prove2Me, the Daskalakis–Goldberg–Papadimitriou series contains the analogous Lemma 3.8 (DGPNash.NashMap.approx_fixed_point_is_approx_nash, posed) and its inequality (3) (DGPNash.NashMap.eq_3, posed): they concern the same map, but for games with a common strategy set Fin n, nonnegative payoffs and a different error term, so they are credited rather than reused. This mission states both directions for arbitrary finite strategy families with the paper's own constants.
Neither direction needs advanced mathematics; the difficulty is in the second direction. The obvious reading, that a profile moved little by has small gains, fails as stated: the approximate fixed-point condition controls , the gain of a strategy relative to the player's total positive gain weighted by , not the gain itself. A strategy that carries most of the probability and most of the positive gain can be almost fixed while its gain is large, so the bound on each has to come from information that the coordinatewise condition alone does not contain, with the exact constants and of the paper tracked throughout; the paper's argument is compact and leaves several of these estimates implicit. In Lean, the multilinearity of the expected payoff in a single player's mixed strategy, which underlies both the reduction to pure deviations and the zero-average identity, has to be derived from the product-form definition of the expected payoff.
Games, mixed profiles and expected payoffs are those of the published agt_games bundle: players form a finite type ι, player i has a finite strategy type S i, payoffs are real (u : ι → (∀ i, S i) → ℝ; the paper's payoffs are rational for computational reasons only). is the published DGPNash.NashMap.purePayoff, and the -NE is the published DGPNash.WellSupported.IsEpsApproxNash, which includes that is a mixed profile. New definitions: gain, nashFunction (by the printed formula, the sum over all of ), IsWeakApproxFixedPoint (a mixed profile with every coordinate of of absolute value ), and the constants maxNumStrategies (), payoffSpread () and cConst (), all computed from the game.
Explicit readings of the paper's text:
The constants , , are definitions computed from the game, not free parameters: a formalization that lets them be chosen (for instance a large in the second direction, or so that becomes ) would trivialize the statement and is ruled out. Contributions of reusable lemmas are welcome, in particular the linearity of AGT.expectedPayoff in one player's mixed strategy and the bound , which are useful to every game-theoretic mission built on agt_games.
Quasi-Newton methods minimize a smooth function using gradients only, while building up an approximation to the inverse of the Hessian matrix from the changes of gradient they observe. They are the default algorithms of unconstrained nonlinear optimization: BFGS and its limited-memory variant L-BFGS sit inside most numerical optimization libraries and most large-scale fitting codes in statistics and machine learning.
The family starts with William C. Davidon's Argonne report ANL-5990 of 1959, Variable Metric Method for Minimization, rejected by a journal in 1957 and published only in 1991 as the first article of the SIAM Journal on Optimization, with a preface by the author (DOI 10.1137/0801001). The report's body describes a flowchart algorithm; its Appendix describes "a simplified method embodying some of the ideas" of that algorithm, in one and a half pages. That simplified method is what is now called the symmetric rank-one (SR1) update, and the Appendix contains its quadratic-termination property: on a quadratic, after at most steps the trial matrix equals the inverse Hessian, and the next step lands at the minimum.
Timeline.
Vectors are elements of and matrices are real . Fix a symmetric positive definite matrix and a point , and let
a quadratic with constant Hessian and minimum point . Its gradient is , display (6) of the Appendix.
The method keeps a point and a symmetric trial matrix , which plays the role of . Write . One iteration is
a full step with no line search followed by a symmetric rank-one update. With the two scalars
footnote 2 of the Appendix fixes the coefficient on a quadratic to , which makes the paper's quality measure of (4) vanish. Write for the step and for the change of gradient. The paper writes , , for the current quantities and , , for the updated ones, and uses the letter both for the number of variables and for the scalar ; here the number of variables is .
If is symmetric and for every , then
This is the sentence after (8) on p. 17: "After no more than steps (for which ), will equal and the following step will be to the exact minimum."
The termination theorem says that on a quadratic the rank-one update recovers the exact inverse Hessian from gradient differences, without line searches and without positive definiteness of the trial matrix, and then takes the Newton step. This is the property that justifies the name "variable metric": the metric converges to the one that makes the problem trivial. The secant equation (8) and the persistence of earlier secant equations (7) are the template for the analysis of every later quasi-Newton update, and the SR1 update remains in use in trust-region methods because it does not force positive definiteness.
The result is classical and its proof is short; what this mission adds is a machine-checked version stated in the paper's own form. In particular the hypothesis is the paper's: only that each of the first coefficients is defined. Textbook statements of SR1 termination often assume in addition that the steps are linearly independent; the paper does not, and the formal goal does not either. No Lean formalization of SR1, DFP or BFGS termination was found in Mathlib or on Prove2Me. On Prove2Me, the related open targets are L-BFGS termination (Nocedal 1980) and conjugate-gradient termination (Hestenes–Stiefel 1952); the definitions here are independent of theirs.
Each update changes by a rank-one term, and nothing in a single step forces to be : the coefficient depends on the current iterate and the update could, a priori, destroy what earlier steps achieved, as general rank-one updates do. The obvious count — steps, conditions — does not by itself give independent conditions on ; the steps produced by the method are not chosen to be independent, and the only hypothesis available is that the denominators are nonzero. The difficulty is to get the full conclusion from that hypothesis alone, without assuming independence, positive definiteness of , or a line search.
Vectors are Fin n → ℝ with 0-based indices, matrices Matrix (Fin n) (Fin n) ℝ; is u ⬝ᵥ (H *ᵥ v) and is vecMulVec (H *ᵥ g) (H *ᵥ g). The definition file DavidonVM.Termination.Method provides quad, grad, Nval, Mval, the run predicate IsRunWith for an arbitrary gradient field and coefficients, and IsQuadRun for the quadratic with ; DavidonVM.Termination.Delta provides the update and the quantity of (4).
Committed conventions, each a reading of something the paper leaves implicit:
A statement of the goal with the extra hypothesis " are linearly independent", or with assumed, would be a weaker theorem than the paper's and is ruled out. The case is trivial; the hypotheses are jointly satisfiable for (checked locally).
Welcome contributions: proofs of the four milestones and the goal; general facts about rank-one updates (determinant and positive definiteness, Sherman–Morrison form of the inverse) that the further statements need and that are reusable for DFP, BFGS and trust-region analyses.
Many optimization problems in machine learning, signal processing and distributed computation have an objective that is a sum of a large number of component functions: one per data point, per sensor, or per processor. Evaluating the whole sum, or a subgradient of it, at every iteration is expensive when is large. Incremental methods process one component at a time, cycling through the components or sampling them, and update the iterate after each one. Incremental gradient and subgradient methods go back to the training of neural networks and to least squares; incremental proximal methods replace the subgradient step of a component by a proximal step, which is more stable and handles nonsmooth terms exactly.
Bertsekas (LIDS-P-2847, 2010, rev. 2011; Math. Program. 129 (2011)) proposed a unified family that mixes the two: each component is split as , a proximal step is taken on and a subgradient step on , followed by a projection onto the constraint set. This mission formalizes the convergence analysis of that family under the cyclic order of component selection.
Timeline. Incremental subgradient methods were analysed by Nedić and Bertsekas (SIAM J. Optim. 12 (2001)) for cyclic and randomized orders. Incremental proximal methods were studied by Bertsekas (Optimization for Machine Learning, 2011, ch. 4). The 2011 paper combines the two analyses; its cyclic-order results are Propositions 3–6.
Let carry the Euclidean norm and inner product . The data are a nonempty closed convex set and real-valued convex functions , . The problem is
with optimal value , possibly , and optimal set , possibly empty.
A subgradient of a convex at is a vector with for all ; is the point of nearest to . At iteration one component is processed with stepsize . The three iterations are
The -subgradient is taken at the new point, which makes the -part a proximal step (Proposition 1). In the cyclic order ; a block of consecutive iterations is a cycle, and is constant within a cycle.
The analysis assumes that the subgradients the iteration uses are bounded by a constant and that, at each cycle start , the function values at the intermediate points of the cycle differ from those at by at most times the distance (Assumption 1 for (19), (20); Assumption 2 for (21)). Both hold, for example, when all , are polyhedral or Lipschitz.
If and , then
and if moreover and , then for some . Both parts are one item, as in the paper.
Proposition 6 is the exact-convergence guarantee for the cyclic incremental subgradient-proximal methods: with a diminishing, non-summable stepsize they reach the optimal value whatever the starting point, and with square-summable stepsizes the iterates converge to a single optimal solution. It covers the pure incremental subgradient method () and the pure incremental proximal method () as special cases, and it is the template for the randomized-order analysis of the companion mission. Proposition 4 quantifies what a constant stepsize achieves.
These results are proved in the paper. None of them, nor the underlying estimates, is formalized on the platform or, to our knowledge, in Mathlib. The mission produces machine-checked versions of the proximal-step lemma for extended-real-valued functions on a constrained set, of the cycle estimate (27) with its explicit constants, and of the deterministic supermartingale convergence lemma, all reusable for other incremental and proximal methods.
The obvious argument treats one cycle as one step of a subgradient method on . It fails because within a cycle the subgradients are taken at the intermediate points or , not at , and the proximal steps use subgradients at the points they produce. The error between and at those points must be controlled through the drift of the iterates during the cycle, and the bookkeeping differs between (19)/(20) and (21), which is why differs. For the second part of Proposition 6, convergence of the values in the sense does not by itself give convergence of the iterates, and may contain more than one point.
EuclideanSpace ℝ (Fin n). Components are Fin m (0-based), so is k % m, and the paper's with becomes with z (k + j). is assumed (NeZero m).IsProj: a nearest point of ), not a choice function.Step between , , and the two subgradients it uses, with the -subgradient at the point the paper names. A run records these subgradients, so Assumptions 1–2 bound exactly them. The assumptions are not replaced by Lipschitz continuity, which is only a sufficient condition (p. 9).EReal; is allowed and no boundedness is assumed.MoreauProx.Characterization.GammaZero) and its subgradients, with relative interiors as Mathlib's intrinsicInterior.The goal cannot be satisfied vacuously: a sorry-free check confirms that the hypotheses hold together (for , , , , ). Restricting to Lipschitz components, to bounded-below , or to would state a weaker theorem and is ruled out.
Proofs of any item are welcome, as are general lemmas (the projection theorem as a variational inequality, the subdifferential sum rule under the relative-interior condition) that the proofs need.
In many production and service settings a single resource is shared by parties with different goals: two departments sending orders to the same machine, two customers of a contract manufacturer, or two classes of requests on one processor. Multi-agent scheduling models this directly. Each agent owns its own jobs and its own objective, and a schedule is judged by the pair of objective values it gives the two agents rather than by a single combined criterion.
Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004, pp. 229–242) set up the systematic study of the two-agent single-machine problem. For each pair of classical objectives they ask how hard it is to optimise one agent's objective while the other agent's objective stays within a given bound. This mission formalises their §9, the case in which both agents minimise their own total completion time. With a single agent, minimising the total completion time is solved by sorting the jobs by length (the shortest-processing-time rule of Smith, 1956). §9 shows that two agents, each with this easiest of objectives, already give an NP-hard problem (Theorem 9.2), and that the problem is solved in pseudopolynomial time by a dynamic program (Theorem 9.3).
There are two agents, A and B. Agent A owns jobs with processing times ; agent B owns jobs with processing times . All jobs are available at time and are processed on one machine, one at a time, without interruption. Since both objectives are nondecreasing in the completion times, a schedule is a sequence of all jobs processed back to back from time . The completion time of a job is the total processing time of the job and of all jobs before it. Agent A's cost is and agent B's cost is .
The recognition problem asks, for thresholds , whether some schedule has
The source problem is PARTITION (Problem 9.1): given integers with , is there a set with ?
The paper's reduction numbers the integers so that and gives both agents identical job sets, jobs of lengths , with thresholds , where
Writing for the pair , an SPT schedule processes in order, each pair in either internal order; denotes the total length of the pairs in which B goes first.
Here is polynomial-time many-one reducibility between languages of binary codes: a polynomial-time Turing-machine-computable map on strings that sends codes of PARTITION yes-instances, and only those, to codes of yes-instances of the recognition problem. Together with the NP-completeness of PARTITION (Karp 1972) this is the statement " is binary NP-hard".
With each agent's jobs numbered by nondecreasing length and the total length of , the recursion
with for and for yields , and when no schedule meets the bound.
Theorem 9.2 fills one cell of the paper's complexity table: even when both agents use the objective that is trivial for one agent, sharing the machine makes the constrained problem NP-hard. Together with Theorem 9.3 it places exactly: NP-hard under binary encoding, solvable in pseudopolynomial time, hence not strongly NP-hard unless P = NP. The later literature on two-agent and multi-agent scheduling (for example the monograph of Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal, Multiagent Scheduling, Springer 2014) cites this classification.
Neither result has a machine-checked proof that we know of. The mission adds a formal record of the reduction and of the dynamic program, reusable definitions for the two-agent total-completion-time problem, and a correction of the printed proof: the equivalence between PARTITION and the constructed instance, as printed, holds only when the integers are pairwise distinct. For PARTITION has no solution, yet a schedule meets for both agents. Theorem 9.2 itself is not affected, since PARTITION remains NP-hard, but a complete formal proof needs a reduction that is correct on every input.
The equivalence for distinct integers rests on two facts: the overall total is at least for every schedule, with equality only for sequences in nondecreasing order of length; and, with distinct lengths, such a sequence is made of consecutive pairs, whose split is controlled by . The naive formal argument stops at the second fact, which is false with repeated lengths: a block of equal-length jobs can be shared between the agents in ways no sequence of pairs realises. The goal adds the encoding layer: the reduction must be computable in polynomial time on a Turing machine, must handle repeated and zero sizes and odd (where is not an integer and the language's thresholds are), and must send strings that do not code a PARTITION instance outside the target language. For Theorem 9.3, the dynamic program is correct only because some optimal schedule orders each agent's jobs by length, and the constraint makes this exchange argument less direct than for a single agent.
Jobs are Fin nA ⊕ Fin nB (Sum.inl h is , Sum.inr k is , 0-based). Schedules, completion times and the idle-free sequence model are the published MooreLateJobs.Shared.completionTime (Moore 1968 series): a schedule is a duplicate-free list containing every job once, and completion times are real numbers. Processing times and thresholds of the language are natural numbers. Reducibility is the published CookPvsNP.PolyReducible, and PARTITION, the alphabet and the binary codes are the published ProjSchedTW.Complexity.Encoding (partitionLang, whose sizes are natural numbers including ). The target language allows any job counts and any processing times; identical job sets are a property of the construction only.
The following readings are explicit:
The goal cannot be met by a trivial reduction: PolyReducible requires the map to be computed by a polynomial-time Turing machine and to be correct on every string, and the target language contains every two-agent instance, not only those with identical job sets. Contributions welcome: the exchange lemmas for total completion time on the shared sequence model, the SPT formulas, and Turing-machine constructions for list sorting and arithmetic on binary codes, which other reductions of this series reuse.
In many production and logistics settings a single resource is shared by parties with different goals: two departments of a plant that send orders to the same machine, two customers of a contract manufacturer, or two classes of traffic on one processor. Multi-agent scheduling models this directly. Each agent owns its own jobs and its own objective, and a schedule is judged by the pair of objective values it gives the two agents rather than by one combined criterion.
Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004, pp. 229–242) set up the systematic study of the two-agent single-machine problem. For each pair of classical objectives they ask how hard it is to optimise one agent's objective while the other agent's objective stays within a given bound. Their Table 1 lists the outcome for each pair. This mission formalises one entry, Theorem 5.2: when agent A minimises its total weighted completion time and agent B only requires its makespan to stay below a bound, the problem is NP-hard under binary encoding of the numbers. The corresponding single-agent bicriteria problem had been shown NP-hard in the strong sense by Lenstra, Rinnooy Kan and Brucker (1977); the two-agent version differs because only B's jobs are constrained.
There are two agents, A and B. Agent A owns jobs ; job has a processing time and a weight . Agent B owns jobs with processing times . All jobs are available at time and are processed on one machine, one at a time, without interruption.
Because both objectives are nondecreasing in the completion times, there is no reason to leave the machine idle, so a schedule is a sequence of all jobs processed back to back from time . The completion time of a job is the total processing time of and of all jobs sequenced before it. Agent A's cost is ; agent B's cost is its makespan .
The paper's recognition problem asks, for given thresholds , whether some schedule has
The source problem is KNAPSACK (Problem 5.1): given nonnegative integers , and integers , is there with and ?
Here is polynomial-time many-one reducibility between languages of binary codes: a Turing-machine-computable, polynomial-time map on strings sending codes of KNAPSACK yes-instances, and only those, to codes of yes-instances of the recognition problem. Together with the NP-completeness of KNAPSACK (Garey and Johnson 1979) this is the statement " is binary NP-hard".
The paper's reduction builds, from a KNAPSACK instance, the two-agent instance with , , a single B-job of length (where , ), and thresholds , . The milestones are the two directions of the proof and their combination:
Theorem 5.2 fixes the complexity of one cell of the two-agent classification. It shows that the polynomial algorithm for the unweighted case (Theorem 5.5 of the same paper) cannot be extended to arbitrary weights unless P = NP. Through §8 it also settles . The hardness is binary, not strong: the reduction produces numbers of size about , so pseudo-polynomial algorithms are not ruled out, which is consistent with the dynamic programs studied in later two-agent literature.
The result is proved in the paper; no machine-checked proof is known to exist. Formalizing it produces a complete reduction from a two-constraint knapsack problem to a scheduling recognition problem, with the encoding, the degenerate instances and the polynomial running time all made explicit. The model and the KNAPSACK language are reusable by other two-agent reductions (Theorems 9.2, 10.1 and 10.2 of the paper reduce from PARTITION in the same frame).
The two directions of the equivalence are short computations with completion times. The printed argument, however, is not correct as written in two places. The bounds "smaller than " and "smaller than " in the derivation of (1) hold only with equality allowed. The strict inequalities in (2) fail when , and then the reduction itself fails: with all and the KNAPSACK instance is a no-instance while the constructed instance has and every schedule meets both thresholds. A complete reduction must recognise such instances and treat them separately.
The construction also produces integer thresholds that can be negative (, or ), while instances of the target are coded with natural numbers. Finally, the reduction must be a polynomial-time Turing machine computation over binary codes, including the decoding of arbitrary strings and the binary multiplication ; that is where most of the formal work lies.
Fin nA ⊕ Fin nB (0-based: Sum.inl h is , Sum.inr k is ). Schedules and completion times are the published MooreLateJobs.Shared sequence model (IsSchedule, completionTime) of the Moore (1968) series: a duplicate-free list of all jobs, processed without idle time from time . Integer processing times are cast to .CookPvsNP.PolyReducible (Cook's Definition 3, one-tape Turing machines). Codes use the published binary encoding ProjSchedTW.Complexity.Encoding (alphabet BSym, encNat, encInt) of the Neumann–Schwindt–Zimmermann series. A KNAPSACK instance is coded as the integers ; a target instance as the natural numbers , the processing times and weights, and . The target language allows any ; the reduction uses .Contributions welcome: proofs of the two directions, of the equivalence, the treatment of the degenerate instances, and the Turing machine for the reduction, which would also serve the other binary-coded reductions on the platform.
Balanced truncation is the standard method for reducing the state dimension of a linear control system while keeping its input–output behaviour: states that are both hard to reach and hard to observe are discarded. Its justification rests on two Gramians, the solutions and of a pair of Lyapunov equations, whose quadratic forms measure how much input energy a state costs to reach and how much output energy it produces. For linear systems the facts are classical: the image of the controllability Gramian is the reachable subspace, and the kernel of the observability Gramian is the unobservable subspace.
Bilinear systems, in which the input multiplies the state, are the simplest nonlinear extension of linear control systems. Their generalized Lyapunov equations have the same form as the Lyapunov equations of linear stochastic systems with multiplicative noise, which is why Benner and Damm treat the two classes together. Balanced truncation was extended to them using the solutions of generalized Lyapunov equations (Al-Baiyat and Bettayeb, 1993; Gray and Mesko, 1998, both as cited by Benner and Damm). Benner and Damm, in Lyapunov Equations, Energy Functionals, and Model Order Reduction of Bilinear and Stochastic Systems (SIAM J. Control Optim. 49(2), 2011, doi:10.1137/09075041X), examine which of the linear-system energy interpretations survive for bilinear systems. Their Theorem 3.1 is the structural result that does survive: the kernels of the Gramians still identify states that are unreachable from the origin and states that produce no output, so these states can be eliminated without changing the transfer behaviour.
Fix and real matrices , , . The bilinear control system (3.1)–(3.2) is
with state , input and output . The homogeneous system (3.5) drops the term : , . The same indexes the bilinear terms and the columns of . Write for a solution with input and initial state , and .
An admissible input is a function that is integrable on every interval . A solution with is a continuous satisfying
The generalized Lyapunov equations (3.6) are
A solution of the first is a controllability Gramian and a solution of the second an observability Gramian. "" means is symmetric nonnegative definite; and are its image and kernel.
(a) If solves the first equation of (3.6), then for every admissible input
(b) If solves the second equation of (3.6) and , then for the homogeneous system (3.5) and every admissible input
The result. Part (a) says that a state outside cannot be reached from the origin by any input, so its controllability energy is infinite; part (b) says that a state in is indistinguishable from the origin at the output, so its observability energy is zero. Together they justify the first step of balanced truncation for bilinear systems (Remark 3.2 of the paper): the system can be restricted to and projected along without changing its input–output map, after which the Gramians are nonsingular and can be balanced. The theorem needs neither stability of nor uniqueness of the Gramians, so it applies to every nonnegative definite solution of (3.6). The rest of §3 of the paper shows that the finer, quantitative energy estimates of the linear case fail for bilinear systems; this qualitative statement is what remains exact.
Formalizing it. The theorem is proved in the paper; no machine-checked version is known. A formal proof yields a reusable invariance principle: a subspace that is invariant under every vector field is invariant under the flow of the input-driven system, for merely integrable inputs. It also yields the linear-algebra lemmas relating kernels of nonnegative definite solutions of generalized Lyapunov equations to the system matrices, which are used throughout model reduction and stochastic stability theory.
The algebraic part (milestones 1, 2, 4) rests on the fact that for a nonnegative definite matrix , forces , applied to the terms of the Lyapunov equation tested against a kernel vector. The passage from the vector field to trajectories is where care is needed. The paper's sentence " whenever , so is invariant" is not by itself an argument: tangency of a vector field to a subspace implies invariance only together with a uniqueness or Gronwall-type estimate, and here the field depends on time through an input that is only integrable, so is merely absolutely continuous and exists only almost everywhere. A pointwise "the derivative points into the subspace" argument therefore does not apply as stated, and the step needs an estimate on the component of orthogonal to the subspace.
The Lean development uses states Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, the matrix–vector product *ᵥ, and indices as Fin m. and are LinearMap.range and LinearMap.ker of Matrix.toLin' P; "" is Matrix.PosSemidef, which includes symmetry. Admissible inputs are integrable on every (this contains , the input space of the paper's energy functionals). A solution is a function continuous on whose integrand is integrable on every and which satisfies the integral equation for all ; no uniqueness of solutions is presupposed, and the theorem is asserted for every such solution.
Two reading decisions are fixed. First, part (b) is stated for every admissible input , not only for as printed in the theorem: the paper's proof concludes " for all , implying ", and the theorem's clause "i.e., " (with a maximum over inputs) needs this form. The statement contains the printed one. Second, the clauses "i.e., " and "i.e., ", which restate the conclusions through the energy functionals (3.3)–(3.4), are not formalized.
The statements must not be trivialized: assuming positive definite makes (a) empty (), assuming stable or the Gramians unique adds hypotheses the paper does not have, and a solution notion requiring trajectories for integrable inputs would make the solution set empty. None of these is used. A local check confirms the hypotheses have content: for , , , the matrix is a nonnegative definite solution of (3.6) with .
A complete development needs Mathlib's facts on nonnegative definite matrices, interval integrals of vector-valued functions, and a Gronwall inequality with an integrable coefficient. The flow-invariance lemma for input-driven linear-in-state systems is reusable beyond this mission. Contributions welcome: proofs of the five milestones, and the passage from vector-field invariance to trajectory invariance.
That noncooperative play usually wastes something is part of the folklore of game theory, with the Prisoner's Dilemma as its emblem: each player's best reply leads to an outcome that both would trade for another. Pradeep Dubey's paper turns this folklore into a theorem about smooth games. For games whose payoffs are twice continuously differentiable, and for all payoffs outside a negligible (closed, nowhere dense) set, Nash equilibria are finite in number and are Pareto-inefficient unless some player sits at a vertex of his strategy set. The same conclusion applies to Nash's mixed extensions of finite games (Nash 1951), where a vertex is a pure strategy.
The question is basic to welfare analysis of strategic interaction: market games, oligopoly, public goods and trading mechanisms (Shapley and Shubik 1977) all ask whether equilibrium outcomes can be efficient. Dubey's answer is that efficiency of an equilibrium is non-generic, so a model that delivers it is exploiting special structure.
Timeline. Nash (1951) introduced equilibrium points and multi-matrix games. Smale (1973, "Optimizing several functions") gave the first-order condition for Pareto optimality of several smooth functions: at an efficient interior point the gradients are linearly dependent. Harsanyi (1973, IJGT 2:235–250) proved that generic finite games have finitely many, indeed an odd number of, mixed equilibria. Dubey's Cowles Foundation Discussion Paper 508R (1978) stated finiteness and inefficiency; the version formalized here is the rewrite IIASA WP-83-74 (1983), published as Mathematics of Operations Research 11(1):1–8 (1986).
There are players . Player 's strategy set is the unit simplex
whose vertices (extreme points) are the origin and the unit vectors. Profiles range over , .
Fix open neighbourhoods and . The space consists of the functions with finite -norm . A game is . For , replaces by for . A profile is -efficient if no gives for all with strict inequality for some . It is a Nash equilibrium if it is -efficient for each , efficient if it is -efficient, and a strong Nash equilibrium if it is -efficient for every . The three sets are , , .
In the proof, is the matrix with rows ; is the subspace of matrices whose -th row vanishes on player 's block of columns; is the set of matrices with linearly dependent rows.
There is an open dense set such that for :
For interior profiles ( for all ):
; the linear perturbation satisfies (the computation behind (**)); claim (*) for : for an open dense set of games is transverse to on a compact neighbourhood of ; under that transversality is finite; and the Theorem restricted to interior profiles.
The Theorem (Multi-Matrix) (p. 14): for an open dense set of payoff vectors , the mixed Nash equilibria of are finite, an efficient one has a player using a pure strategy, and a strong one is pure. From the example of §3: every game on with payoffs has a unique Nash equilibrium (p. 9); Lemma 1, (p. 9); Lemma 2(a), an interior equilibrium is efficient iff or (p. 10).
The theorem gives the generic structure of equilibrium sets in smooth games: isolated and finitely many equilibria, and a sharp location of the only places where efficient equilibria can survive, namely the vertices. It explains why efficiency results for noncooperative models need boundary solutions or non-generic structure, and in its multi-matrix form it shows that strong equilibria of generic finite games are in pure strategies. It also supplies the finiteness of equilibria used in comparative-statics and index arguments.
On the formalization side, the result is proved on paper but has no machine-checked version. A complete development would give Lean its first generic-finiteness theorem for Nash equilibria of smooth games, a first-order Pareto condition in the form of Smale's lemma, and a parametric transversality argument in finite dimensions. The multi-matrix companion connects to the published vocabulary of finite games (agt_games), and the example of §3 is an elementary, fully explicit check of the general picture.
The interior case reduces, by (i) and (ii), to a dimension count: should be zero-dimensional and empty. Neither holds for every game: they hold only when is transverse to and to the strata of , and the step that requires work is showing that transversality is an open and dense condition in the topology. Density is not obtained by adding linear functions to the payoffs: a linear function has finite -norm on only when is bounded, so perturbations must be localized. The step from interior profiles to the whole of is a second difficulty. It requires repeating the argument on every product of faces of the simplices and on every subgame, and then intersecting finitely many open dense sets. Efficiency at a boundary point is not -efficiency in a subgame, so the reduction has to be made with care.
Players are Fin n with 2 ≤ n; block sizes k : Fin n → ℕ with 1 ≤ k i; profiles are ∀ i, Fin (k i) → ℝ. The simplex is the paper's corner simplex {x ≥ 0, ∑ x ≤ 1}, not the probability simplex; "vertex" is Set.extremePoints. The neighbourhoods are taken open, and the goal is stated for every such choice, not assuming bounded or convex. Payoffs are total functions; a game is ContDiffOn ℝ 2 on with finite -norm, which takes values in , so no junk real supremum enters. "Open dense in " is written in -form for the product of -norm topologies; Lean's sup-type norms are equivalent to the Euclidean ones, so the open dense sets are the same. Deviations range over all strategies in , not only pure or vertex deviations.
Added hypotheses, all disclosed in the items: openness of ; interiority of every on milestones (i), (ii) and the finiteness step (the proof's standing case assumption); in claim (*). The printed "By (i), " is stated for interior equilibria, which is where (i) applies.
A trivializing formalization is ruled out: the open dense set must contain games arbitrarily close to every game (the zero game is a game, so it is never empty), interiority appears only in the milestones and not in the goal, and efficiency is with respect to all deviations in .
Not stated: (*) for a general submanifold , and the decomposition of into submanifolds of codimension , both of which need embedded submanifolds of ; Remarks 1–4 (Remark 4's openness claim for strictly concave payoffs is false as printed); Lemma 2(b); §5, which the author leaves as a conjecture. Contributions welcome: a finite-dimensional parametric transversality theorem, Smale's first-order Pareto condition, and the face-by-face reduction.
Nonlinear model predictive control (NMPC) computes a feedback law by solving, at every sampling time, an optimal control problem that starts from the currently measured state. The control actually applied is the first control of that problem's solution. When the dynamics are fast relative to the time an optimizer needs, solving each problem to convergence is impossible, and the delay between measuring the state and applying the control degrades or destabilises the closed loop.
Diehl, Bock and Schlöder (SIAM J. Control Optim. 43(5), 2005) analysed the real-time iteration: a scheme that performs a single Newton-type iteration per sampling time and then moves on to the next problem. The scheme is the basis of widely used NMPC software (for example the ACADO toolkit and acados) and of much of the later theory on suboptimal and "anytime" MPC. The paper's Theorem 4.1 is the first contraction result for it; Theorem 5.1 bounds the price paid in closed-loop cost for not solving each problem to optimality.
A discrete-time system , , has states and controls . For and a state , the shrinking-horizon problem is
Its primal-dual vector is and its Lagrangian is
The projection drops the block .
A Newton-type method solves by steps , where is the KKT matrix with its Hessian blocks (and the terminal block) replaced by approximations, for instance those of the constrained Gauss–Newton method. The real-time iteration starts from a guess and, for , computes for , applies , lets the system evolve to , and sets .
The analysis uses a neighbourhood and its projections , norms on with and , two constants (the Hessian approximation error) and (a Lipschitz-type constant of ), the rates , and the ball .
Assume is twice continuously differentiable on , is continuous with bounded inverse on , the conditions (4.1a)–(4.1c) hold with , and . Then for
for
and the Newton-type iterates of started at converge to a stationary point with
No constant is chosen by the formalization: all of them are the paper's.
The proof has three parts (contraction, well-definedness, distance to the stationary points). The milestones are its steps: the gradient transition identity between consecutive problems; the block identity ; the one-step contraction; the recursion ; the lifting of a nearby point of to ; the contraction (4.7) of the Newton-type method on a fixed problem; and the convergence of those iterates to .
If moreover on , then , and for the loss is . The intermediate estimate (5.4), , is a separate item.
Theorem 4.1 says that a scheme which never solves any problem to convergence still produces iterates that contract at the rate of the underlying Newton-type method and approach the exact solutions of the problems along the closed loop, geometrically. It justifies the "one iteration per sample" design of real-time NMPC under explicit, checkable conditions on the Hessian approximation, and its constants are those of the classical affine-invariant Newton-type convergence theory, so it extends to Gauss–Newton and other approximations. Theorem 5.1 turns the contraction into a closed-loop performance guarantee: the suboptimality is quadratic in the first step, quartic for exact Newton.
The results are proved in the paper; none is formalized. A formal proof would supply the details the paper leaves implicit (that the segments used by the integral mean value theorem stay in the domains, that the ball around lies in ), would give a reusable Lean model of discrete-time optimal control problems with their KKT structure and shrinking-horizon projections, and would make the classical local contraction argument for Newton-type methods available for general norms.
Each single estimate is a variant of the textbook local convergence proof for Newton-type methods. The difficulty is that the real-time iteration changes the problem at every step: the next step is computed for a different, smaller problem at a different initial state, so the textbook argument does not apply as is. The proof needs two structural facts that tie consecutive problems together, the gradient transition along the undisturbed closed loop and the block identity of the Hessian errors, together with the compatibility of the norms with the projections. A second obstacle is well-definedness: the iterates must be shown to stay in regions where the hypotheses hold, which requires tracking the projections of through all shrinking spaces.
is a Euclidean space whose coordinates are indexed by (multiplier, state or control block, stage, component) for the stages ; is a restriction and its transpose the extension by zero. The gradient and Hessian are Mathlib's gradient and fderiv; the inverse is ContinuousLinearMap.inverse. The approximations of the stage Hessian blocks depend on (the paper's misprinted read as ), the terminal block may be approximated as in §2.2, and symmetry of the approximations is not required. The norms are a structure carrying the norm axioms and the two compatibility conditions. The real-time iterates follow the undisturbed closed loop. The hypotheses (4.1a)–(4.1c) are imposed at the points of where the paper's functions are defined, that is, for with ; no convexity of is assumed. Theorem 5.1 is stated with Euclidean norms on every , because its last step bounds by ; is the objective at the primal part of , not an infimum.
Mathlib's inverse is at a non-invertible operator and its derivative is at non-differentiable points; either junk value would make every step vanish and every bound trivial. The statements therefore require invertibility and twice continuous differentiability at the points of , keep the membership (4.2) as a conclusion, and pin as the limit of the Newton-type scheme started at , so it cannot be chosen after the fact. Degenerate norms are excluded by the norm axioms.
Some milestones add a hypothesis that Theorem 4.1 supplies internally: a segment , the ball around the starting point contained in , or for the abstract δ-recursion. Contributions welcome: proofs of the milestones, a sorry-free instance of the hypotheses for a linear-quadratic problem, and general lemmas on the integral mean value theorem for gradients in arbitrary norms.
Treewidth measures how closely a graph resembles a tree. Many problems that are NP-hard on general graphs can be solved in time linear in the number of vertices once a tree decomposition of bounded width is available, so computing such decompositions quickly is a basic task in algorithmic graph theory. Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (SIAM J. Comput. 45(2), 2016) gave an algorithm that, for a graph on vertices and an integer , either reports that the treewidth of exceeds or returns a tree decomposition of width at most , in time .
The paper's headline is that algorithm, a statement about pseudo-code and running times. This mission does not formalize it. It formalizes one of the paper's combinatorial lemmas, Lemma 6.5 (p. 369), which the algorithm's data structure uses to answer its balanced-separator query: it turns the search for a small balanced separator into two maximization problems that a dynamic program can solve.
Timeline. Robertson and Seymour (Graph Minors II, J. Algorithms 7, 1986) proved that graphs of treewidth have balanced separators of size (Lemma 2.1 of the paper). Robertson and Seymour (Graph Minors XIII, 1995) used it in an approximation algorithm, Reed (1992) improved the dependence on to , and Bodlaender et al. (2016) reached linear time with a single-exponential dependence on .
All graphs are finite and simple. For , is the graph obtained by deleting ; its components are the vertex sets of its connected components.
A separation of is a partition of (parts may be empty) such that no edge of joins to . Its order is . It is -balanced if .
For and sets of terminals , a terminal separation of the induced subgraph of order (Definition 6.4) is a partition of with
It is left-pushed if is maximum, and right-pushed if is maximum, among all terminal separations of of order with the same terminals.
The treewidth is the least width of a tree decomposition of (Definition 1.1), where the width is the largest bag size minus one.
Let and let be a separation of with . Then there are a partition of and integers with such that, for with terminals ,
In the order of the proof, the milestones are: Lemma 2.1 (balanced -separators of size , cited from Graph Minors II); the packing step of the proof sketch of Lemma 2.2 (components holding at most of each split into two sides holding at most each); the folklore -balanced separation of order ; the restriction of that separation to , which gives part (i); four lower bounds on , ; the dichotomy that two opposite "quadrants" have at least vertices each; the comparison of pushed separations with the restricted one; and the gluing step of part (ii).
Lemma 6.5 is what makes the paper's balanced-separator query computable: given a bag that splits a component in a balanced way, a left-pushed and a right-pushed terminal separation are each the solution of a maximization problem, and the lemma guarantees that gluing them gives a separator of order whose sides are bounded away from . The constant feeds into the approximation ratio of the whole algorithm.
The proof is complete in the paper and elementary given Lemma 2.1. No part of it is formalized in Lean's Mathlib or, as far as a search of the Prove2Me catalog shows, on the platform. Lemma 2.1 itself, Robertson and Seymour's balanced-separator theorem for bounded treewidth, is not in Mathlib; a machine-checked proof of it would be reusable wherever treewidth separators are used (divide-and-conquer on tree decompositions, Lipton–Tarjan style arguments, grid-minor theorems).
Everything after Lemma 2.1 is counting with partitions, but the bookkeeping is the obstacle: the two separations and cut into nine pieces, the induced subgraphs overlap on , and pushedness is a maximum over a family of partitions of a subset, not of .
Lemma 2.1 is the hard milestone. It is a statement about tree decompositions, and any proof has to relate subtrees of the decomposition tree to components of for a bag , infrastructure that does not yet exist in Mathlib.
V : Type with decidable equality; vertex sets are Finset V, is Finset.univ, is Fintype.card V. Universe 0 matches the published definition of treewidth.RobertsonSeymour1986.GM5.TreewidthLE G k: a decomposition tree on a finite type whose bags have at most vertices. Definition 1.1 roots the tree; rooting does not change the width.avoidComp G X u: the vertices reachable from by a walk of none of whose vertices, endpoints included, lies in .Part (i) is part of the goal: without it, left- and right-pushed separations of the chosen orders might not exist and part (ii) would hold vacuously. Choosing does not trivialize the goal, because the size bound and the budget must hold simultaneously.
Welcome contributions: a proof of Lemma 2.1 from tree decompositions (reusable on its own), the packing lemma, and the counting milestones of the proof of Lemma 6.5.
In a congestion game, several users choose facilities and each facility becomes more costly as more users choose it. Such games model settings in which each participant chooses a route or collection of resources for personal use while the resulting load is shared. A pure Nash equilibrium is a stable choice of routes: no single participant can lower their own cost by switching. Stability alone gives no assurance that the resulting allocation serves the group well. The price of anarchy compares the social cost of an equilibrium with the best social cost attainable by coordinated choices.
Christodoulou and Koutsoupias studied finite congestion games with linear latency functions and several notions of social cost. For the maximum cost borne by any player, their STOC 2005 paper gives both an upper bound valid for all such games and a family of instances showing that its square-root dependence on the number of players has the right order. This mission formalizes those two claims together. The maximum criterion matters when a single heavily delayed user is significant even if the total cost of the population is moderate.
Let be the number of players and let be a finite set of facilities. Player has a finite collection of available pure strategies, each a subset of . A profile chooses one strategy for every player. For a facility , its load is the number of players whose chosen strategy contains . The latency of at load is . Player pays the sum of the latencies on the facilities they chose:
A profile is a pure Nash equilibrium if no player can decrease this cost by replacing their own strategy while the others keep theirs. The paper calls latencies linear when with ; these are affine functions in standard terminology. The paper displays many calculations for the special case and states the general nonnegative affine convention in its model section. The maximum social cost is ; the total cost is . The paper's average social cost is .
For a game with at least one pure Nash equilibrium and a positive optimal maximum cost, the maximum-cost pure price of anarchy is the largest equilibrium value of divided by the smallest feasible value. The Lean targets use inequalities against every feasible comparison profile rather than dividing by an optimum. This form continues to say something when an optimum has cost zero, and finite strategy sets ensure an optimum exists whenever the profile space is nonempty.
For every , every finite game with nonnegative affine latencies, every pure Nash equilibrium , and every feasible profile , Theorem 5's proof yields
This states a numerical version of the paper's theorem without an unspecified constant. Taking to minimize gives the corresponding price-of-anarchy bound. The bound is about asymmetric games: players may have different strategy sets, and no symmetry assumption is present.
For every integer , let . Theorem 6 provides an identity-latency congestion game with players and facilities, a pure Nash profile , and an optimal profile for which
Every feasible profile in the instance has maximum cost at least . Thus the ratio is , and . The proof's explicit instance has positive comparison cost, so the lower bound cannot be satisfied by a zero-cost game. The source also says such behavior occurs in network congestion games and sketches a network realization in Figure 2; this mission's formal lower target is the finite congestion-game construction.
Together these results identify the order of growth of the worst pure equilibrium maximum cost relative to an optimum: it can grow with the population, yet for linear latencies it grows no faster than a constant times . The upper statement applies to any feasible comparison profile, so it can also be used when a convenient benchmark is known without solving the entire optimization problem. The lower family prevents replacing the square-root dependence by a bound independent of for this class of games.
The results are proved in the 2005 paper; the mission is to give them machine-checked Lean proofs in a common finite-game representation. The development also supplies reusable definitions of congestion games, loads, pure cost equilibria, and maximum social cost, together with the total-cost estimate of Theorem 1 and the intermediate bounds appearing in Theorem 5. The current draft contains statements with sorry placeholders, not completed proofs.
A bound on total player cost does not directly control the cost of the most expensive player sharply enough. An individual player can use several facilities whose loads interact, and bounding each load separately loses the dependence required for the square-root result. Affine coefficients add another issue: the proof printed for identity latencies writes a cardinality where the general statement needs a coefficient-weighted quantity. The lower example has an indexing discrepancy in the printed alternative strategies, so the intended Nash profile must be checked against the costs on every permitted deviation.
Players are represented by Fin N; facilities by an arbitrary finite type in upper bounds and by a type with elements in the lower family. A profile is a function from players to finite facility sets, with feasibility stated separately. Latencies are real-valued on natural-number loads. The IsLinear predicate requires explicit nonnegative affine coefficients. Pure Nash uses a cost inequality; it is the negative-payoff version of a standard finite game's payoff equilibrium. MAX requires at least one player, and all upper-bound targets therefore require . The lower family begins at , where is positive.
The source's number is written as in Lean to keep natural-number subtraction inside its valid range. The two expressions agree for . In the source's one-based indexing, the proposed alternative strategy uses a ceiling index. The printed denominator makes some alternative facilities carry users and breaks the Nash assertion; denominator agrees with Figure 2's short-route users per layer and gives the stated costs. This correction is recorded with the lower theorem. No normalization of coefficients or artificially restricted strategy class is assumed. Contributions to the finite-game definitions, Theorem 1, the player-cost bounds, and the explicit lower instance are all in scope.
How should a set of indivisible items (courses, shifts, inherited objects) be divided among people who have different entitlements but no money to transfer? A classical answer for divisible goods is the competitive equilibrium from equal incomes (CEEI): give every agent a budget of artificial currency, find prices at which every agent can afford her favourite bundle and the market clears. The resulting allocation is Pareto optimal and fair. With indivisible items a CEEI can fail to exist already for one item and two agents with equal budgets: at any price, either both agents can afford the item or neither can.
Babaioff, Nisan and Talgam-Cohen (arXiv:1703.08150; Math. Oper. Res. 2021, doi:10.1287/moor.2020.1062) study this Fisher market with indivisible goods when budgets are generic: unequal budgets, with a measure-zero set of exceptional budget pairs excluded. Their main result is for two agents with almost equal budgets. This mission formalizes the companion result for two agents with identical additive preferences and arbitrary unequal budgets (Theorem 8.1 of the paper, its informal Theorem 1.4). With identical preferences the division problem is a discrete claims (bankruptcy) problem: one cake of fixed value is split between claimants with different entitlements .
Timeline of the relevant results:
There are indivisible items and two agents. Agent has a valuation that is additive, normalized (), non-negative, monotone and strict (different bundles have different values), and a budget , with . An allocation gives every item to exactly one agent. Item prices price a bundle at .
A bundle is demanded by agent at prices if and for every bundle with . A competitive equilibrium (CE) is a pair in which each is demanded by agent . An allocation is Pareto optimal (PO) if every other allocation is strictly worse for some agent. It is budget-proportional if for both agents, and anti-proportional if for both, strictly for one.
The truncated share of agent is
the best she can get in a PO allocation that gives her at most her budget share; an allocation gives her the truncated share if . The exceptional set (Definition 6.2) consists of the budget pairs for which two PO allocations , consecutive in agent 's order of preference, satisfy . It is finite. The rectangle (Definition 6.1) is a set of allocations between the truncated-share maximizers of the two agents.
In Lean all objects live in GenericBudgets.IdenticalPrefs: bundle, price, IsDemanded, IsCE, IsPO, IsStandardValuation, IsBudgetProportional, IsAntiProportional, GetsTruncatedShare, IsTruncMaximizer, InRectT, InR.
If , , and for some agent , then
Theorem 8.1 shows that the non-existence of CEEI for identical preferences is a knife-edge phenomenon: for every market with identical strict additive preferences, every unequal budget pair outside a finite set admits a CE, and the CE allocation is as close to budget-proportional as indivisibility allows. It gives a market-based solution to the indivisible claims problem with unequal entitlements, and its CE inherits Pareto optimality from the first welfare theorem (Theorem 2.4 of the paper).
The formalization targets three things on top of the paper. First, a machine-checked proof of the paper's main technical tool, Lemma 6.3, which also drives the paper's main Theorem 7.1 (mission 1 of this series), where it is applied to almost equal budgets instead of identical preferences. Second, precise definitions of the truncated share, the rectangle and the exceptional set , whose informal versions leave conventions implicit (the maximization runs over PO allocations only; is indexed by consecutive PO allocations). Third, verification of the proof chain Proposition 5.1 → Lemma 6.3 → Lemma 8.2 → Theorem 8.1. The statements compile, but none of these results has a machine-checked proof yet.
The reduction of Theorem 8.1 to Lemma 8.2 and the proof of Lemma 8.2 from Proposition 5.1 and Lemma 6.3 are short. The substance is in Lemma 6.3, which must exhibit prices supporting a PO allocation when no allocation gives both agents their budget shares. Demand is a condition over all bundles, so a candidate price vector has to be checked against every bundle each agent prefers, and the paper's construction breaks down on the exceptional budget pairs , which is why they are excluded; the argument is a case analysis over the finite Pareto frontier. The easy case, Proposition 5.1, covers only markets with a budget-proportional or anti-proportional PO allocation; with identical preferences and unequal budgets neither typically exists (no allocation is ever anti-proportional), so Lemma 6.3 cannot be avoided.
Items are Fin m; agents are Fin 2, with indices for the paper's agents , so is b 1 < b 0. Valuations are functions Finset (Fin m) → ℝ bundled with the standing assumptions in IsStandardValuation; identical preferences are the hypothesis v 0 = v 1. An allocation is a map Fin m → Fin 2, so every item is allocated exactly once. Budgets are positive reals summing to . All quantities are real.
Committed conventions and disclosed restrictions:
max: for every PO with .Trivializing formalizations are ruled out: the demand condition quantifies over every bundle with strict inequality, allocations must assign every item, prices are non-negative, the truncated share is maximized over PO allocations only (not over all allocations), and the budget hypothesis excludes only the finite set for one agent, never all unequal budgets.
Proposition 5.1 and Lemma 6.3 are posed with the same statement as in mission 1 of this series; a proof of either transfers verbatim. Contributions welcome: the finite-frontier infrastructure (existence and uniqueness of the truncated-share maximizer), Proposition 5.1 through budget-exhausting combination pricing, and Lemma 6.3.