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?
Many online selection problems ask an algorithm to accept or reject items one at a time, irrevocably, while keeping the accepted set feasible: independent in a matroid, a matching in a graph, or within a knapsack budget. In Bayesian versions, such as prophet inequalities and posted-price mechanisms, a fractional point of a relaxation of the feasible sets is available in advance, and each item is active independently with probability . An online contention resolution scheme (OCRS), introduced by Feldman, Svensson and Zenklusen, turns this random active set into a feasible selection as items arrive.
The quality of an OCRS is measured by its selectability: the probability that every element is accepted when it is active, whatever the arrival order. Applications, however, care about the value of the selected set, often a submodular function such as a coverage or a utility with diminishing returns. Theorem 1.10 of the paper is the bridge between the two: a selectability guarantee yields an approximation guarantee for every monotone submodular objective, and for non-monotone ones, even against an adversary who sees every random outcome before fixing the order. The other four missions of this series construct selectable OCRSs for matroids, matchings and knapsacks and combine them; this mission formalizes what such a guarantee is worth.
The offline counterpart is the theory of contention resolution schemes (CRSs) of Chekuri, Vondrák and Zenklusen (SIAM J. Comput. 2014), whose Theorem 1.3 shows that a monotone balanced CRS rounds the multilinear extension of a submodular function with the balancedness factor. The proof of Theorem 1.10 reduces the online statement to that offline result.
Let be a finite ground set and a down-closed family of feasible sets. A polytope is a relaxation of if it contains exactly the characteristic vectors with among the -points. For , the random set contains every independently with probability .
A greedy OCRS fixes, for each input , a down-closed family containing (deterministically, or drawn from a distribution independent of ). The elements then arrive one by one; an arriving active element is selected if, together with the elements already selected, it forms a set in . An element is selectable for the active set if for every with . For the OCRS is -selectable if for every and every
The arrival order is chosen by the almighty adversary, which knows , the realized family and every random bit of the algorithm before choosing it.
For , the multilinear extension is . The function is submodular if for all , and monotone if implies . For a set , keeps every element of independently with probability .
An (offline) CRS for maps each , possibly at random, to a subset with . It is -balanced if for and , and monotone if whenever . The characteristic CRS of a greedy OCRS is .
Let be a relaxation of , let be a -selectable greedy OCRS for , let , and let be submodular. Against every almighty adversary, the selected set satisfies
where in the second case the coins defining are known to the adversary. The constants are the paper's and are not parameters to be improved here.
Theorem 1.10 is what makes selectability useful. Combined with the paper's OCRSs for matroids, matchings and knapsacks (Theorem 1.8) and the combination rule (Theorem 1.9), it gives constant-factor online algorithms for submodular objectives under intersections of these constraints, and through them the paper's applications to prophet inequalities, posted-price mechanisms and stochastic probing. The guarantee holds against the strongest adversary considered, so it applies whatever arrival order the application imposes.
The theorem and its proof are published; none of the statements of this mission has a machine-checked proof. Formalizing it produces a reusable interface between online and offline contention resolution, and machine-checked versions of two standard lemmas on correlated random subsets of submodular functions (Lemmas 3.6 and 3.7) used throughout submodular maximization. Lemma 3.5 is the substantial imported ingredient: its formal proof amounts to formalizing the rounding theorem of Chekuri, Vondrák and Zenklusen for non-monotone objectives.
The first idea is to compare the online selection directly with element by element: each element is selected with probability at least . For a linear objective this suffices. For a submodular objective it does not, because the marginal value of an element depends on which other elements are selected, and the adversary controls this through the order. The reduction to the characteristic CRS removes the order, but the offline rounding result (Lemma 3.5) then needs the full CRS machinery, including a pruning step that depends on alone.
For non-monotone , selecting extra elements can lose value, and the adversary decides which elements beyond are selected, after seeing the coins. Controlling this requires the correlated-sampling bounds of Lemmas 3.6 and 3.7 rather than independence.
The ground set is a finite type α : Type with decidable equality; sets are Finset α; vectors are α → ℝ. All probabilities and expectations are exact finite sums of product weights, without measure theory. is the pointwise scaling b • P, which handles . The multilinear extension and submodularity are the published definitions NonmonotoneSubmod.Shared.F and NonmonotoneSubmod.Shared.Submodular.
A randomized greedy OCRS is a weight function on families Finset (Finset α), a CRS a weight function on maps Finset α → Finset α; a deterministic OCRS is a point mass. The almighty adversary is any function from the realized family and active set (and, in part 2, the coin set , with and uniform and independent of everything else) to an order listing every element once. The standing assumptions of Definition 1.3 are explicit hypotheses: down-closed, a polytope contained in and a relaxation of , and . A polytope is encoded as the convex hull of finitely many vectors. Every greedy family contains , so the empty family cannot make every element vacuously selectable, and the inputs lie in , so the product weights are probabilities.
Definition 3.1 is printed with ""; the formalization uses "", as the proof of Lemma 3.4 and Definition 4.5 do. Lemma 3.5 keeps the paper's quantifier order: is fixed before , , , and .
Welcome contributions: proofs of the milestones in any order; Lemmas 3.6 and 3.7 are self-contained and reusable; Lemma 3.5 may be split further along the proof of Chekuri–Vondrák–Zenklusen.
Social networks exhibit triadic closure: two people with a common friend are more likely to be friends themselves than two people chosen at random, and the more common friends they have, the more likely they are to be connected. The principle goes back to sociology (Granovetter 1973) and is documented on large network data sets (see the Enron e-mail graph in Figure 1 of Fox, Roughgarden, Seshadhri, Wei and Wein).
A common computational task on such networks is to list all maximal cliques, the groups of mutually connected vertices that cannot be enlarged. On an arbitrary graph this is hopeless in the worst case: Moon and Moser showed in 1965 that an -vertex graph can have maximal cliques, and that no graph has more (Moon and Moser 1965). Yet clique enumeration on real social networks runs quickly. Fox, Roughgarden, Seshadhri, Wei and Wein proposed a distribution-free graph class, defined by a coarse form of triadic closure, on which the worst case is provably polynomial. This mission formalizes their first bound, for the class of weakly -closed graphs (Theorem 2.2 of the paper, also stated as Theorem 1.5), together with the peeling argument that proves it.
All graphs are finite, simple and undirected. For a graph with vertex set and a vertex , is the set of neighbours of ; for , is the subgraph induced by . The common neighbours of two vertices are the vertices of .
Every -closed graph is weakly -closed, but not conversely. The paper's example: a clique on vertices with one edge removed is not -closed for any , but it is weakly 1-closed (order and last).
In the Lean development these objects are IsCClosed, IsBadPairIn, IsWeaklyCClosed, maxCliquesIn, numMaxCliquesIn and numMaxCliques, in the namespace CClosedGraphs.Peeling.
For all positive integers and , every weakly -closed graph on vertices satisfies
The milestones follow the proof of Theorem 2.1 in §2.1 and the remark that extends it to Theorem 2.2. Fix a graph, an induced subgraph and a vertex . A maximal clique of is of type 1 if , of type 2 if and is maximal in , and of type 3 otherwise.
For fixed , the theorem makes the number of maximal cliques of a weakly -closed graph polynomial in , against for general graphs. Since all maximal cliques can be listed in polynomial time per clique, this makes maximal-clique enumeration fixed-parameter tractable in on the class. The paper's Theorem 2.3 turns the proof into an enumeration algorithm. Weak -closure is the version that matters in practice: Table 1 of the paper reports social networks with thousands of vertices that are weakly -closed for modest while being -closed only for much larger . The bound is the starting point of the paper's sharper Theorem 3.1 () and its lower bound Theorem 4.1, which are separate missions of this series.
The result is proved in the paper, and the proof is short. No machine-checked proof of it or of the Moon–Moser bound exists in Mathlib at the pinned revision or on Prove2Me. This mission produces both, together with a reusable vocabulary for counting maximal cliques of induced subgraphs. Proofs of the sharp Moon–Moser values, or of the sharper in the recursion, are welcome as further contributions but are not milestones.
The counting argument is elementary. The work lies in two places. First, the Moon–Moser bound is not in Mathlib and needs its own proof, and its exponential bound must be handled with real powers. Second, the type decomposition must be handled exactly: a type-3 clique is charged to a pair , and the charge has to be injective while ranges over all vertices outside . The degenerate cases are real. When is isolated in and , the clique is of type 3 and . The peeling for weakly -closed graphs must also follow the given vertex ordering, with closure checked in the shrinking induced subgraphs rather than in .
SimpleGraph (Fin n). Auxiliary statements are generic over a finite type with decidable equality.Fin n with . The set is .Set.ncard, which is exact on a finite type. "At least " is , not .Three trivializing readings are ruled out. The count is of maximal cliques, not of all cliques or of cliques of a given size. A bad pair needs at least common neighbours, not more than . In the weakly closed definition, common neighbours are counted inside , not in ; counting them in would make the hypothesis stronger and the theorem weaker.
A complete development needs a Moon–Moser lemma for induced subgraphs, the injections behind milestones 2 and 4, and a peeling induction over a vertex ordering. The first two are reusable for any maximal-clique counting argument. The induced-subgraph counts numMaxCliquesIn are also used by the later missions of this series, which repeat the definitions in their own namespaces.
Generalized Turán problems ask for the maximum number of copies of a fixed graph in an -vertex graph that avoids a family of forbidden subgraphs. The ordinary Turán number counts edges (); Alon and Shikhelman (arXiv:1506.03397) started the systematic study of the general function , building on earlier results of Erdős on cliques, Bollobás and Győri on pentagons in triangle-free graphs, and Győri and Li on triangles in graphs without a long odd or even cycle. Counting cycles in graphs with forbidden cycles is closely tied to extremal problems for Berge hypergraphs, and the constructions used are sparse hypergraphs of large girth.
Gerbner, Győri, Methuku and Vizer, Generalized Turán problems for even cycles (arXiv:1712.07079, J. Combin. Theory Ser. B, 2020), determine or bound for many cycle families. This mission covers one of their results in §6.2: the number of odd cycles in a graph in which every shorter cycle is forbidden and, in addition, one longer odd cycle is forbidden. Its companion (Theorem 17, a separate mission of this series) forbids a longer even cycle instead, and there the paper obtains a sub-quadratic upper bound; with an odd extra cycle only a quadratic upper bound is proved.
All graphs are finite and simple. For an integer , is the cycle of length . For a set of integers , write ; a graph is -free if it contains no with as a (not necessarily induced) subgraph. The family consists of all cycles .
For graphs and , is the number of copies of in : subgraphs of isomorphic to , counted without labelling. The generalized Turán number is
For a vertex of , is the set of vertices at distance exactly from .
A hypergraph is a finite set of hyperedges (vertex sets); it is -uniform if each hyperedge has vertices. A Berge cycle of length is a sequence of distinct vertices and distinct hyperedges with and . The girth of a hypergraph is the length of its shortest Berge cycle; "girth at least " means there is no Berge cycle of length .
For all integers , as ,
Both the lower and the upper bound are part of the goal; the implied constants may depend on and only.
The supporting published theorem erdos_gallai_path_conjecture (the Erdős–Gallai path theorem: a graph on vertices with no path of edges has at most edges) is included as a reference item; the paper's proof of Claim 19 invokes it.
Theorem 18 shows that forbidding all cycles up to length together with one odd cycle still permits polynomially more than copies of , at least , and at most . Compared with Theorem 17, where an even cycle is forbidden and the count is , it isolates the role of the parity of the extra forbidden cycle. The authors conjecture that the true order is sub-quadratic (Conjecture 34, §8 of the paper), so the gap between the two exponents in Theorem 18 is a stated open question; a formal development of the known bounds is the base on which any improvement would be checked.
The result is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it produces: a reusable encoding of generalized Turán numbers for cycle families on top of Mathlib's copyCount; Berge cycles and the girth of uniform hypergraphs; distance layers ; and a formal statement of the Nešetřil–Rödl existence theorem, which is used as a black box by many extremal constructions.
The upper bound requires careful bookkeeping of distance layers around a vertex in a graph without short cycles. The obvious estimate, bounding the copies of through by the number of pairs of vertices of , gives only per vertex and hence nothing better than the trivial bound overall; the content of Claim 19 is that forbidding the single cycle makes the edge count inside linear, and the parity of is used essentially.
The lower bound rests on Theorem 29, a cited result that is not proved in the paper, and for which Mathlib has no supporting theory of uniform hypergraphs or Berge cycles. For the construction itself, the paper only asserts that the cycle-replacement graph has no short cycle other than the inserted 's; a cycle of the graph may wander through many hyperedges, and relating it to the girth of the hypergraph is the step a formal proof has to supply.
Fin n; graphs are SimpleGraph (Fin n). Cycles are Mathlib's SimpleGraph.cycleGraph, and is Mathlib's unlabelled copyCount.Set.Icc 3 (2 * l) ∪ {2 * k + 1}: every length , not only .edist, so vertices of other components lie in no layer.Finset (Finset V); "girth at least " is a predicate (no Berge cycle of length ), not an infimum, so a hypergraph without Berge cycles has every girth.Asymptotics.IsBigO along atTop, with real exponents; both directions of the goal are stated.A formalization that states only the upper bound, uses labelled copies, lets a constant depend on the graph, omits the short cycles from the forbidden family, or defines by a supremum that can take a junk value, does not prove this theorem.
Contributions welcome: proofs of the milestones, a proof of Theorem 29, and general lemmas on breadth-first layers in graphs of large girth, which are reusable by the companion missions of this series.
Minimum-cost flow is a standard model for routing a quantity through a network while paying a cost on each arc. Unit capacities arise when each input arc can carry at most one unit; they include flow formulations of several matching and assignment problems. Goldberg, Kaplan, Hed and Tarjan analyze a cost-scaling algorithm for this setting. Their second-phase argument depends on a bound on the excess left in a pseudoflow when every excess vertex has undergone enough potential increases. This mission formalizes that bound, Lemma 5 of their STACS 2015 paper. The published paper gives an running-time bound for its unit-capacity algorithm; the running-time statement itself is outside this mission.
A network has a finite vertex set and an arc set that contains both orientations of each input arc. Write . Every input arc has capacity one; its reverse has capacity zero and opposite cost. Write for the number of input arcs, so . The paper assumes no parallel or antiparallel input arcs, allowing an arc to be identified by its ordered endpoints. Costs are antisymmetric between orientations.
A pseudoflow assigns an antisymmetric quantity to each arc and respects its capacity. Its excess at is the sum of incoming flow. Positive excess means that has flow to discharge; negative excess is a deficit. A circulation is a pseudoflow with zero excess at every vertex. An arc is residual for when its residual capacity is positive. For vertex prices , its reduced cost is . A pseudoflow is -optimal at when every residual arc has reduced cost at least . These are the paper's conventions on p. 408.
At the start of a cost scale, let be a circulation that is -optimal at prices . During the scale, is a pseudoflow that is -optimal at prices . The potential increase in scale units is . Put . The second phase begins when every excess vertex has ; the paper also states that every deficit then has and that the levels are integral. The remaining excess is .
The comparison graph has arcs and vertices . An excess–deficit cut meets every path in this graph from an excess vertex to a deficit vertex. Thus a cut is measured among comparison arcs, not among arbitrary arcs of the original network. Lemmas 3 and 4 of the paper establish the level and cut bounds on which the excess estimate rests.
The goal is Lemma 5 on p. 410, stated with both constants obtained in its proof. Under the cost-scale conditions above, and the divisibility conventions in footnotes 5–6, its two cases are
The second case also assumes that six divides the integer ; the first uses divisibility by three. The goal keeps the two conclusions separate so that the stronger bound is retained when determines the scale. Its milestone list follows the paper: Lemma 3 bounds by three on an arc of ; Lemma 4 bounds total excess by a cut; and the proof of Lemma 5 supplies the cut bands and the two size estimates. The bands use the exact three-level and six-level ranges printed on p. 410.
The result connects a condition on price increases to a numerical bound on the amount of flow still needing discharge. Combined with the paper's time per unit of remaining excess, this is the bound needed for its second-phase running-time estimate. The two regimes show how the same cost-scale state can be controlled by either the number of input arcs or the number of vertices. Without the excess bound, the paper's argument gives no comparable limit on the remaining work at the phase transition.
The paper proves Lemma 5, but this particular unit-capacity excess argument has no matching theorem in the platform catalog checked for this mission. The network, circulation and pseudoflow interfaces are already published as reusable definitions from earlier cost-scaling work. A completed machine-checked development would add the cut argument and band counts to those interfaces. Those facts can also support other analyses that compare an entry circulation with an intermediate pseudoflow; this mission does not claim to formalize the algorithm's entire execution or its running-time model.
The main obstacle is linking local price inequalities to a global bound on excess. A reduced-cost inequality controls a single residual arc, while excess may move through a path and is measured over many vertices. The comparison graph is essential: on a residual arc outside , the level difference used by Lemma 3 is not available. Counting all residual arcs as if they were comparison arcs would therefore not justify the cut bound. There is a separate counting issue: the represented network has both directions of each input arc, so using for changes the constant in the square-root case.
Lean represents the network by a finite symmetric arc set with real capacities and antisymmetric real costs. A local unit-capacity predicate marks each reverse pair as capacities or ; counts the capacity-one orientations. Flows are real valued as on p. 408. Integer costs on that page are generalized to real costs because Lemmas 3–5 use only antisymmetry and reduced-cost inequalities. No result here depends on cost integrality.
The formalization takes the cost-scale state as hypotheses: , entry circulation and -optimality, current -optimality, integral levels, level at least at excess vertices, and zero level at deficits. It takes as a natural number equal to and records the paper's divisibility simplifications. The indexed pigeonhole milestones also require so their index ranges are nonempty; the goal includes the zero-arc boundary without requiring an index. Cuts use reachability after deleting a subset of , equivalent to meeting every excess-to-deficit path. The proof of Lemma 5 prints “cut in ”; the formalized claim uses , the graph for which Lemma 3 gives the required level control and Lemma 4 states its bound.
The definition layer, path-cut lemma and finite counting arguments are the reusable infrastructure. Contributions that establish these exact statements, their necessary elementary flow identities, or a machine-checked goal proof are in scope. Counting with reverse arcs, allowing cuts outside , using arbitrary real levels in place of integral ones, or replacing both cases by the weaker bound does not express this target.
Lower bounds for interactive decision making (bandits, reinforcement learning, and the general decision making with structured observations framework of Foster, Kakade, Qian and Rakhlin, arXiv:2112.13487) compare what a learner observes under two different environments. A learner's whole interaction history is generated one step at a time: each observation is drawn from a conditional law that depends on everything seen before. Statistical estimation guarantees, by contrast, are stated one step at a time, as bounds on the divergence between the conditional laws at each round. Passing from the per-step guarantees to a statement about the laws of entire histories requires a chain rule for the divergence in use.
For the Kullback–Leibler divergence the chain rule is an identity. The paper's guarantees, however, are stated in the squared Hellinger distance, which is bounded, symmetric, and the natural loss for density estimation with the logarithmic loss. Hellinger distance has no exact chain rule. Lemma A.13 of the paper (App. A.2, p. 73) supplies an approximate one, losing a factor logarithmic in the number of steps, and the paper uses it in the proof of its main regret lower bound (Theorem 3.2, via App. C.1.3).
Fix and finite sets . A sequence is with , and denotes its prefix; .
For probability distributions on a finite set, the squared Hellinger distance, the Hellinger distance and the Kullback–Leibler divergence are
the last one set to when charges a point that does not. Note that the paper's carries no factor , so .
A family of sequential kernels assigns to each and each prefix a probability distribution on . Its sequential law is the law of under :
For a second family with law , the quantity controlled by per-step estimation is
In Lean these are IsSeqKernel, seqLaw and condHellingerSum, with hellingerSq and klDivDiscrete the published discrete divergences.
The constant is the paper's; the shape that matters downstream is the logarithmic dependence on with no assumption on the kernels beyond their being probability kernels.
If and for every , prefix and event , then .
The result. Inequality (97) converts per-round Hellinger estimation error into a bound on the Hellinger distance between the laws of complete interaction histories, under no boundedness assumption on likelihood ratios. In the paper this is the step that lets the lower bound of Theorem 3.2 relate any algorithm's behaviour under a reference model to its behaviour under alternatives, and hence express the minimax regret through the decision-estimation coefficient. Without it, only the KL chain rule is available, which requires bounded likelihood ratios (the situation of (98)) or loses more than a logarithmic factor. Lemma A.11, a milestone here, is used independently in the same lower bound and in the paper's tabular reinforcement learning analysis.
Formalizing it. The lemma is proved in the paper; no machine-checked proof exists. The published layer on the platform has the discrete divergences and the comparisons of Lemmas A.5 and A.10; the sequential-law objects, the triangle inequality, the convexity of , the discrete chain rule and Lemma A.11 are new. A completed development gives a reusable chain-rule toolkit for any later formalization of lower bounds over adaptive interaction histories.
The squared Hellinger distance does not tensorize along adaptive sequences: the natural attempt to write as a product of conditional affinities fails because the conditional affinities are random, depending on the prefix, and their expectation does not factor. Bounding by and applying the KL chain rule fails in the other direction: the conditional KL divergences are not controlled by the conditional Hellinger distances unless the likelihood ratios are bounded, and in (97) they are not. The difficulty is to obtain a bound that pays only for an unbounded ratio, with explicit constants that survive the final numerical comparison.
Fintype, distributions are probability vectors, expectations are finite sums. Coordinates are indexed by Fin n (0-based) and the alphabets may differ from coordinate to coordinate.P i x of the whole sequence that is a probability vector and depends only on the coordinates j < i; this is what makes seqLaw P the law the paper describes.Contributions welcome: proofs of any milestone and of the fact that seqLaw is a probability vector.
Neural networks trained by empirical risk minimization are sensitive to small adversarial perturbations of their inputs. Distributionally robust optimization addresses this by training against the worst distribution in a neighbourhood of the data distribution. Sinha, Namkoong, Volpi and Duchi (arXiv:1710.10571v5, ICLR 2018) take the neighbourhood to be a Wasserstein ball and relax the hard constraint to a Lagrangian penalty with multiplier . For large the inner maximization becomes strongly concave and is solved per data point by a transportation map , which turns each training example into its worst-case perturbation.
The average transport cost is the amount of robustness the trained model actually certifies on the sample: by the paper's duality result, the empirical worst-case loss at level is computable, and it is the certificate of robustness that the paper advertises. A certificate measured on the training sample is only useful if it transfers to the population. This mission formalizes the result that it does: concentrates around its population counterpart, uniformly over the parameter set.
Parameters range over a set and data over a set , both with the Euclidean norm. A transportation cost satisfies and Assumption A: is continuous and is -strongly convex for each . A loss satisfies Assumption B: its partial gradients , are Lipschitz in each variable, with constants .
For the problem is -strongly concave on , and the transportation map is its maximizer,
Given i.i.d. samples with and empirical distribution , the empirical robustness level and its population counterpart are
The complexity of enters through its covering number , the least number of points such that every is within of some ( if there is no finite such family).
Two alternative regularity conditions close the setting, with a constant : (i) is -Lipschitz on in each argument; or (ii) and is -Lipschitz. Put in case (i) and in case (ii).
For every ,
In case (i), and this is exactly the last display of the proof of Theorem 4 (p. 44); case (ii) is the "identical reasoning" the paper invokes with . is an arbitrary subset of : no compactness is assumed, and an infinite covering number makes the bound vacuous rather than false.
In the order the proof uses them:
The tail bound gives a -type generalization rate for the gap between the robustness certified on the sample and the robustness achieved on the population: with for bounded , the deviation is of order . It also implies, as the paper notes, that the certified level stays positive for large whenever the loss is not invariant to the data.
The paper states the result as Theorem 4, display (17), in "with probability " form with the constant . That form does not follow from the proved tail bound as printed: inverting the tail bound gives a deviation with a covering radius that depends on the deviation rather than on , whereas (17) uses in both places and drops and . The mission therefore poses what the proof establishes, the tail bound above, and does not claim (17). None of this paper's results has a machine-checked proof; Hoeffding's inequality and covering numbers are in Mathlib, the argmax stability and the cover argument are not.
Concentration at a single fixed is Hoeffding's inequality and carries no information about the trained model, whose parameter depends on the sample. The supremum over an arbitrary, possibly uncountable is the content. A union bound needs a finite family, and transferring control from a finite family to all of needs the deviation to be Lipschitz in . The deviation is built from the transportation map, which is an argmax and has no closed form; its regularity in comes only from strong concavity, which holds only for . In case (ii) the cost itself has no Lipschitz assumption, and the Lipschitz property of has to be extracted from the optimality of at two different parameters. Finally, the supremum event is not obviously measurable.
Spaces are EuclideanSpace ℝ (Fin d) and EuclideanSpace ℝ (Fin m); the paper's general norm is specialised to , in Assumptions A and B, in cases (i) and (ii), and in the covering number. The cost is real valued and constrained on only; the loss is typed on , but Assumption B and the argmax property of the transportation map are required only for and , matching the paper's . The transportation map is a function together with its argmax property. Samples are the coordinates of the product measure ; of the supremum event is its outer measure, so no measurability of the event is assumed. The supremum is a real supremum of quantities bounded by . The covering number is Mathlib's Metric.coveringNumber (closed balls, centres in , values in ). The definition on p. 9 does not say where the centres lie; the proof applies Hoeffding's inequality "for any fixed " at the centres, and the loss is only defined on , so the centres are taken in .
Hypotheses made explicit that the page leaves implicit:
Case (ii) is assumed for only, as printed in Theorem 4.
A bound for one fixed , a supremum taken outside the probability, a covering radius not tied to , or a covering number of a set other than would be a different and much weaker statement; the goal has the supremum over inside the event and the radius .
A complete development needs the stability of maximizers of strongly concave functions under Lipschitz perturbation of the gradient, a finite-cover union bound for outer measures, and Hoeffding's inequality for bounded i.i.d. coordinates of a product measure. The first two are reusable well beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for the goal.
Neural networks trained by empirical risk minimization are sensitive to small, deliberately chosen perturbations of their inputs ("adversarial examples"). A standard defence is adversarial training: at each step, perturb the training example to increase the loss, then take a gradient step at the perturbed point. Sinha, Namkoong, Volpi and Duchi (arXiv:1710.10571, ICLR 2018) recast adversarial training as distributionally robust optimization over a Wasserstein ball around the data distribution, and replaced the hard ball constraint by a Lagrangian penalty. The resulting procedure perturbs each example by solving a penalized inner maximization, and the paper shows that, when the penalty is large enough relative to the smoothness of the loss, this inner problem is strongly concave and therefore tractable.
This mission formalizes the paper's computational guarantee, Theorem 2: stochastic gradient descent on the penalized robust objective, with an inexact adversary, reaches an approximate stationary point at the rate of smooth nonconvex stochastic optimization. The analysis follows Ghadimi and Lan's argument for nonconvex SGD (arXiv:1309.5549), adapted to a gradient oracle that is biased by the inexact inner maximization.
Parameters live in and data in a set ; both spaces carry the Euclidean norm . Data are drawn from a probability distribution on .
A transportation cost measures how expensive it is to move a data point to . Assumption A: is continuous, , and for each the map is -strongly convex. The canonical example is .
A loss has partial gradients and . Assumption B: these gradients are Lipschitz in each argument,
For a penalty , the robust surrogate and the robust objective are
By Wasserstein duality, equals the worst-case expected loss over all distributions , penalized by times the transport distance from to .
Algorithm 1 (with and constant stepsize ): from , for , draw independently, find an -approximate maximizer , meaning , and set .
Let , , , and assume for all . With and ,
for every constant stepsize . The goal is this bound at the balancing stepsize.
The result. Theorem 2 certifies that the robust training procedure is no harder, in iteration count, than ordinary nonconvex SGD: the stationarity measure decays as , and the inexactness of the adversary enters only as an additive term proportional to , independent of . This is what licenses running a few steps of gradient ascent for the inner problem rather than solving it exactly. It also explains the role of the penalty: the guarantee requires , so smoothness of the loss in the data (smooth activations rather than ReLUs) is what makes the robust problem tractable.
Formalizing it. The result and its proof are published; nothing here is open. To our knowledge none of it is machine-checked. A formal proof would add a verified Danskin-type theorem for strongly concave suprema with explicit Lipschitz constants (Lemma 1), which is reusable well beyond this paper, and a verified nonconvex SGD analysis with a biased oracle, including the measure-theoretic bookkeeping (independence of the fresh sample from the current iterate, differentiation under the integral) that the paper's proof compresses into one line.
The deterministic inequalities (31), (32) and the bias bound are short. The weight sits elsewhere. First, Lemma 1 requires differentiability of a supremum over a possibly unbounded set, with the maximizer depending on ; the paper invokes a Danskin-type theorem that is not in Mathlib, and the cost is not assumed differentiable, so the first-order optimality conditions for the inner problem must be derived from strong convexity alone. Second, the expectation step uses , which needs both differentiation under the integral sign for and the independence of from along the run. Third, finiteness of every expectation along the run is not assumed and must be propagated from step to step.
Lean representation: and are EuclideanSpace ℝ (Fin d) and EuclideanSpace ℝ (Fin m); is a set in the latter. The loss is a function on all of ; its partial gradients are required at points of and the Lipschitz conditions on only. Strong convexity is Mathlib's StrongConvexOn, whose modulus convention matches the paper. Suprema are sSup over the image of . is a Bochner integral, and is assumed -integrable for every . The run is driven by (Measure.pi). The expectations in the conclusion and in the variance hypothesis are lower Lebesgue integrals in ; the -term of Theorem 2 is moved to the right-hand side.
Hypotheses made explicit that the paper leaves implicit: (the paper writes but divides by ); nonempty, convex and closed; Lipschitz constants nonnegative; , , , ; bounded below (so is a real number); integrability of ; ; joint measurability of the oracle ; and, in (32) and the later milestones, , which the paper assumes "in the rest of the proof". Lemma 1 is specialized to the Euclidean norm, the case Theorem 2 uses. The cost is not assumed differentiable.
A trivializing formalization is ruled out: the run uses an oracle tied to by the -gap and to by membership, is the supremum of the penalized loss over , is its -integral, and the hypotheses are satisfiable (for instance , , , a point mass, ). Expectations as lower integrals prevent a non-integrable from being read as .
Infrastructure a complete development needs: the descent lemma for functions with Lipschitz gradient; first-order characterizations of strong concavity on a convex set; a Danskin/envelope theorem for strongly concave suprema; differentiation under the integral for ; and conditional-expectation bookkeeping for Markov-type recursions driven by i.i.d. samples on a finite product space. The first three are reusable in any minimax or bilevel analysis. Contributions to any milestone, or to these supporting facts as separate lemmas, are welcome.
A prophet inequality compares an online decision maker, who sees random inputs one at a time and must commit irrevocably, with a "prophet" who sees all inputs in advance. The classic single-item version (Krengel–Sucheston, Samuel-Cahn) says that a well-chosen fixed threshold earns at least half of the expected maximum. In mechanism design the same statement reads: a posted-price mechanism, which offers each arriving buyer a take-it-or-leave-it menu of prices, extracts a constant fraction of the optimal expected welfare, and does so in a way that is truthful, simple and order oblivious.
Dütting, Feldman, Kesselheim and Lucier (SIAM J. Comput. 49 (2020)) reduce the construction of such prices to a deterministic question. If, for every fixed valuation profile , one can find prices that are balanced — high enough to pay for the welfare an early allocation destroys, low enough that whatever is still feasible stays affordable — then the expected prices , suitably scaled, give a prophet inequality. This is their Theorem 3.2 for -balanced prices. For combinatorial auctions with bundles of size at most , MPH- valuations and related settings, the natural prices only satisfy a weaker condition, in which the affordability bound may also spend a multiple of the benchmark welfare. Theorem 3.5, the subject of this mission, is the extension theorem for that weak balancedness; it is what turns the paper's Theorem 4.1 (bundle size ) and Theorem 1.6 (MPH-) into - and -approximate posted-price mechanisms.
There are agents . Agent has an outcome space containing a null outcome ; outcome profiles are . For , gives to the agents in and to the others, and keeps only the agents before . The feasible profiles form a set that is downward closed ().
Agent has a valuation , drawn independently from a known distribution ; . The welfare of is , and (zero on ). An allocation rule maps every valuation profile to a feasible outcome.
A pricing rule assigns prices to outcome offered to agent given the partial allocation , with when . In the posted-price mechanism the agents are approached in index order; agent sees the prices and buys a utility-maximizing outcome, utility being .
A family of sets of profiles is exchange compatible if for every , and . Given and , a pricing rule is weakly -balanced (Definition 3.4) with respect to and if for every
A collection is weakly balanced if one exchange-compatible family works for every .
If is weakly -balanced with , then with
the posted-price mechanism with prices , approaching agents in index order, satisfies
The result. Theorem 3.5 is the second of the paper's two extension theorems. Its hypothesis is a deterministic, full-information property of prices, which is often checkable by a direct combinatorial argument; its conclusion is a Bayesian guarantee for an online, truthful mechanism. The paper instantiates it with weakly -balanced fractional prices for combinatorial auctions with bundle size at most (Theorem 4.1) and for MPH- valuations (Theorem 1.6), obtaining approximation ratios linear in and , where -balancedness alone would not apply.
Formalizing it. The theorem is proved on paper; no machine-checked version exists. The mission produces a formal account of the sequential posted-price mechanism with history-dependent prices (an online run defined by recursion over the agents), of the ghost-sample argument, and of the case analysis in . The definitions are general enough that the paper's applications — and other balanced-price arguments — can be stated on top of them. The printed proof has a slip: (A.1) is printed as an equality but only the inequality "" holds; the formalization states the inequality.
Two steps carry the content. First, the utility bound (A.1): agent could have bought its part of the deviation , but that deviation is defined from the run on a different profile. The argument needs that the partial allocation does not depend on — the mechanism is online — and that exchanging with an independent copy preserves the joint law. Making this exchange rigorous on a product measure, and handling an empty (where no deviation exists and the bound must come from ), is where the work lies. Second, is a supremum that need not be attained, so "buy your part of OPT" must be replaced by near-optimal selections and a limit.
The tempting shortcut of treating weak balancedness as -balancedness and applying Theorem 3.2 does not work: property (b) of Definition 3.1 bounds prices by a multiple of alone, which can be zero while is not.
Agents are Fin n, 0-based: the paper's agent is index , and "the order they are indexed" is the order of Fin n. Prices take values in ENNReal with ; price sums are never converted to reals, and property (a) passes its right side through ENNReal.ofReal (a negative bound becomes , which is the page's meaning). is the real supremum sSup, zero on the empty set, meaningful because values lie in .
Valuations are given by type spaces and an evaluation . The type spaces are countable with discrete σ-algebras — a disclosed restriction of the paper's general distributions, which makes every function measurable and every bounded one integrable. The null outcome is assumed free at feasible partial allocations ( for ): every pricing rule in the paper has this property, and the proof needs its consequence . Exchange compatibility is required for all , as printed. The agents' behaviour is a choice rule that sees only the agent's own type and the earlier agents' outcomes and maximizes utility at every feasible partial allocation; at infeasible ones no requirement is made. The constant is written literally inside the posted prices, never as a free parameter.
The milestones (A.1)–(A.4) are stated for an arbitrary , and (A.1)–(A.2) for an arbitrary selector into in place of the maximizer, with an explicit zero when ; both are generalizations of the printed steps. A statement in which the agents' optimality hypothesis can never be met, or in which an infinite price sum is read as , would make the goal vacuous; the encoding above excludes both, and a sorry-free one-agent instance in the workspace confirms that all hypotheses of the goal can hold together.
Needed infrastructure: product measures and the swap of one coordinate with an independent copy, lower integrals of ENNReal-valued prices, the recursion defining the run, and near-maximizers of bounded suprema. The model and mechanism definitions are reusable for the paper's other extension theorem (Theorem 3.2) and its applications. Contributions are welcome on any milestone; the pure inequality of Case 2 is self-contained.
A two-stage stochastic programme chooses a decision before an uncertain parameter is revealed and pays a cost . When is known only through data points, or through a law with many atoms, the expected cost is expensive to optimize, and practitioners replace the law by a small set of reduced scenarios. Classical scenario reduction chooses these scenarios to be close to the data in a Wasserstein distance, without looking at the cost (Dupačová, Gröwe-Kuska and Römisch, 2003; Rujeerapaiboon, Schindler, Kuhn and Wiesemann, 2022). Bertsimas and Mundru (Operations Research, 2023) propose problem-dependent scenario reduction: the distance between two scenarios measures how much the optimal decision for one costs when evaluated on the other. Their method needs, for each cluster of data, the scenario that minimizes a cost-dependent dissimilarity, which they replace by a convex upper bound, problem (16).
Theorem 3 of the paper is the sanity check for that upper bound. For the simplest cost to which it applies and a single reduced scenario (), under a symmetry assumption on the law, the minimizer of the upper bound is the mean of , which is also what Wasserstein scenario reduction returns for . This mission formalizes that statement.
Decisions and parameters both live in , with the Euclidean inner product . The feasible set is a polytope
for a matrix and a vector , assumed nonempty and bounded. The cost is , a special case of the piecewise bilinear costs of (15) (take , , ).
An optimal-decision map is any function with for every ; for a vector , is the whole set of minimizers. The set of cost-reducing parameters is
For a candidate reduced scenario , the per-scenario upper-bound loss is
For this cost it is the optimal value, in the auxiliary variables , of the per-point linear programme in (16). With a random parameter of law , the upper-bound objective for is . The squared cost for Wasserstein reduction to one atom is ; (4) takes its square root, which preserves minimizers.
Assumption 5 (p. 24) asks:
Under Assumption 5, for every measurable optimal-decision map ,
The page's "the solution … is simply the mean" is read as "the mean is a minimizer", which is what the proof concludes; uniqueness is not claimed.
The upper bound (16) is the computational core of the paper's Algorithm 1: each alternating-minimization step solves one instance of it per cluster. Theorem 3 is the only result in the paper that identifies its minimizer in closed form, and it shows that, in a symmetric case, the cost-aware reduction agrees with the classical one at . It is the paper's justification that the upper bound is a sensible surrogate and not an arbitrary convex relaxation.
The argument is a variant of the mean-minimizes-the-surrogate result of Elmachtoub and Grigas for the SPO+ loss (Management Science, 2022, Proposition 6(a)), with both terms clipped at zero and with a law living only on instead of all of . Theorem 3 is proved on paper; it has not been formalized, and on Prove2Me the Elmachtoub–Grigas statement is posed but open. The work here is to formalize the known proof, including the measure-theoretic steps the paper treats in one sentence each: integrability of the loss, exchange of the subdifferential and the expectation, and the almost-sure uniqueness of linear minimizers over a polytope.
Convexity of the objective and a vanishing subgradient at would settle the theorem, but two steps of that argument are not routine. First, the objective is not differentiable everywhere, and the subdifferential of is not in general the expectation of the pointwise subdifferentials: the exchange needs the integrable bound of milestone 2 and the almost-sure uniqueness of milestone 3. Second, that uniqueness is a statement about the geometry of polytopes and about the law of the reflected parameter together: neither convexity nor absolute continuity alone gives it. The clipping at zero adds a third point: one has to check that it is inactive at almost surely, which is where Assumption 5a's support condition on and Assumption 5b enter. Dropping either half of Assumption 5a breaks the argument: a two-atom symmetric law can put both atoms where is a whole edge, and a law charging the complement of can make the first clipping active at .
EuclideanSpace ℝ (Fin d) and is ⟪z, ξ⟫_ℝ. Decision and parameter spaces coincide (), as the cost requires.polytope P qv, with the hypotheses that it is nonempty and bounded (§1 of the paper assumes nonempty and compact; the polytope is closed).SmartPTO.Fisher.xi, SmartPTO.Fisher.zstar and SmartPTO.Fisher.Wstar; "symmetric about its mean" is the published SmartPTO.Fisher.CentrallySymmetric.zsel with the hypothesis that zsel ξ is a minimizer for every , and it is assumed measurable (needed for ; not on the page). The theorem holds for every such selection; uniqueness of minimizers is not assumed.Useful infrastructure, reusable beyond this mission: support functions of polytopes and their directional derivatives; the fact that a linear function has a unique minimizer over a polytope for Lebesgue-almost every cost vector; differentiation of convex integral functionals under the integral sign. Contributions of any of these as stand-alone lemmas are welcome.
The source is the authors' accepted manuscript (MIT DSpace, "Submitted to Operations Research"), not the published article; all page and theorem numbers refer to the manuscript, whose printed page numbers equal its PDF page numbers.
Online combinatorial optimization is a repeated game in which a learner selects, round after round, a structured object (a subset of fixed size, a path, a matching, a spanning tree) encoded as a 0/1 vector, and an adversary assigns a cost to every coordinate. It models routing, ranking, scheduling and many other sequential decision problems in operations research and machine learning, and it contains prediction with expert advice as the special case of one-hot vectors.
The most widely used algorithm for this game is the exponentially weighted forecaster, which keeps a weight on every action and multiplies it by after each round. Applied to a combinatorial action set it is called EXP2 (Audibert, Bubeck and Lugosi), or Expanded Hedge in the full-information case (Koolen, Warmuth and Kivinen, COLT 2010). Its standard analysis gives regret of order , while online mirror descent with the negative entropy (Component Hedge) achieves , which is optimal. Koolen, Warmuth and Kivinen left open whether a better tuning or a better analysis of EXP2 could close this gap.
Timeline.
Fix integers (the dimension) and (the number of rounds). An action set is a nonempty finite set whose elements all have the same number of ones: for every . At each round :
The regret after rounds is
EXP2 with learning rate starts from the uniform distribution on and updates, for every ,
In the Lean development IsBinaryActionSet A m is the action-set condition, exp2Weights A η z t is , and exp2Regret A η z n is against a fixed loss sequence . thmOneSet d, adv1 d and adv2 d ε are the action set and the two adversaries of the paper's proof.
For with a multiple of , there is an action set with constant such that for every some adversary with losses in makes EXP2 pay
The action set is chosen before the learning rate, and the adversary after it.
The result. Theorem 1 shows that the gap between EXP2 and mirror descent with the negative entropy is not an artefact of the analysis: on an action set with , where the optimal rate is of order , no learning rate brings EXP2 below . Exponential weights over the actions are therefore provably suboptimal in online combinatorial optimization, which motivates working with the convex hull of (mirror descent) rather than with the actions themselves. The construction is also a template for algorithm-specific lower bounds: two adversaries, one punishing large and one punishing small learning rates.
Formalizing it. The result is proved in the paper (App. A, with Lemma 3 in App. C); to our knowledge none of it is machine-checked. A formalization yields a checked algorithm-specific lower bound for exponential weights, an exact closed-form regret computation for EXP2 on a structured action set, and a rigorous proof of Lemma 3, whose printed proof checks numerically before an asymptotic argument with Stirling's formula.
The statements are elementary, but each step hides a real computation. The first adversary requires the exact distribution of EXP2 on a set of actions over alternating rounds, and a regret identity rather than a bound. The second requires controlling EXP2's expected loss over all rounds against a constant adversary on the same exponentially large set. Lemma 3 is the hardest piece: at it is tight at , while the ratio tends to as ; the printed proof verifies numerically, so a formal proof needs an argument valid for every . A naive attempt to prove the goal with a single adversary fails: one adversary only defeats either large or small learning rates.
Fin d → ℝ with entries in , so is the dot product. Coordinates and rounds are 0-based: the paper's odd rounds are the even indices.Finset.inf'; every statement requires nonempty, so no junk value enters.Contributions welcome: proofs of the milestones, a proof of Lemma 3 by any method, and reusable lemmas on exponential weights (normalization, closed form, monotonicity of weights along a constant adversary). The paper's proofs are in its App. A and App. C.
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.
In a prophet inequality, a gambler sees prizes one at a time and must decide when to stop, while a prophet knows every realization and takes the largest. A stopping guarantee compares the gambler’s expected prize with the prophet’s. The order of arrival changes the problem: here the prizes are independent but can have different distributions, and every permutation of their arrival is equally likely. Before seeing any prize, the gambler chooses a threshold for each distribution and accepts the first prize above its threshold. Such a rule has no need to update thresholds after observing rejections. Correa, Foncea, Hoeksma, Oosterwijk, and Vredeveld prove that this restricted rule still earns at least a fraction of the prophet’s expected maximum (Theorem 1, pp. 1455, 1459).
The random-arrival stopping model also supplies guarantees for posted-price mechanisms. A posted price gives a buyer a take-it-or-leave-it offer; the first buyer who accepts ends the sale. The paper explains the connection between its stopping rules and expected revenue under random buyer arrival (§1.1 and §5). This mission formalizes the stopping theorem itself, which is the mathematical guarantee used before that economic translation.
Let , and let be independent, nonnegative real random variables with known, possibly different distributions. Their realizations arrive in a uniformly random order. A nonadaptive threshold rule chooses constants before any realization is observed. It accepts the first arriving index with and receives . If no prize crosses its threshold, its reward is zero. An infinite threshold deliberately excludes an index. The strict comparison matches Theorem 1, even though an earlier description in §1.2 uses a weak comparison (pp. 1454–1455).
For fixed realized prizes, write . Conditional on the set of indices with , each accepted index is equally likely to arrive first. The conditional expected reward is therefore
The prophet benchmark is . The theorem compares with , including distributions for which either expectation may be infinite. The variables need no common distribution and no atomlessness assumption.
The paper’s main supporting result is the Bernoulli Selection Lemma. It starts with independent Bernoulli indicators of success probabilities , fixed real prizes , and a chosen subset . Its payoff is the average , again zero when the denominator vanishes. The lemma compares the best subset with a finite linear optimization problem over and (Lemma 1, p. 1455).
The goal is the exact constant of Theorem 1:
The quantifiers range over every finite nonempty family of independent nonnegative variables. The thresholds are deterministic and indexed by the distributions, and the assertion covers atoms as well as continuous laws. This is the paper’s headline nonadaptive result (Theorem 1, p. 1459).
The milestone list includes the paper’s multilinear formulation (4), its substitution (5), Proposition A.1, Lemmas 2 and 3, and the Bernoulli Selection Lemma. The latter states, in particular, that the maximum expected selected average dominates times the optimum over feasible . Two further milestones express the decomposition of the expected maximum and the upper-tail comparison used for continuous distributions (§2–3 and Appendix A). These targets fix the finite selection problem and the probabilistic quantities that the goal must connect.
The guarantee identifies what fixed, distribution-specific thresholds can achieve under random arrival: the expected accepted prize reaches a constant fraction of the prophet’s benchmark for every collection of independent nonnegative distributions. The paper also gives examples showing why a rule that keeps every positive prize is inadequate and studies where the factor is tight (§2.1 and §3.1). These are claims about the performance of a restricted class of stopping rules, not about an optimal adaptive strategy.
The paper proves Theorem 1; a machine-checked proof of this mission’s goal remains to be supplied. The finite Bernoulli model, its subset optimum, and the nonnegative expectation conventions would be reusable for other random-order stopping and allocation results. This mission makes the paper’s claimed constants, event comparisons, and boundary cases explicit in the theorem statements so a later proof has a fixed target.
Taking the first value above a single low threshold can accept a modest prize before a rare large one arrives. Raising every threshold can instead reject too many prizes. The paper’s example with a constant prize and a rare large prize shows that accepting all available values does not meet the claimed factor (p. 1460). The difficulty is obtaining one set of fixed thresholds that balances those risks across different distributions, while the benchmark selects the largest realization after seeing them all. The Bernoulli selection inequality carries the sharp constant; connecting it to general distributions must also account for ties and atoms.
Lean represents the index set by Fin n with , so its index zero is the paper’s index one. The existing published definition SamuelCahnProphet.Median.Setting.maxX supplies the sample maximum; this mission defines the strict accepted set and its real-valued reward ratio. Thresholds live in because the paper explicitly uses to exclude a variable. Expectations are nonnegative extended integrals of ENNReal.ofReal, preserving infinite values and avoiding a default zero for nonintegrable real integrals. The source’s nonnegativity assumption is represented almost surely, which is enough for these expectations and does not restrict the distributions further.
The Bernoulli law is a finite product formula. Its probabilities lie in , while prizes are arbitrary real numbers as in the printed lemma. The feasibility condition includes : these variables are probabilities, and allowing negative values would change the optimization problem. The finite subset optimum is an attained maximum. Proposition A.1 is stated for ; an empty contradicts the budget conclusion for . It also includes the printed case. Lemma 2 includes as printed: the removable division by zero in (6) is assigned its continuous value . The comparison milestones for continuous distributions assume atomlessness explicitly; the goal does not.
The accepted set depends only on fixed thresholds and the realized values. It cannot depend on the sampled arrival order or on prior observations. A constant choice such as accepting every positive prize does not prove the target guarantee. Contributions that establish the finite Bernoulli selection result, its analytic bounds, the random-order reward identity, or the passage from continuous to arbitrary distributions all serve the stated goal. The random-order identity and the discontinuous case are further work beyond the current milestone list.
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.
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.