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?
Two-stage decision problems split decisions into a here-and-now decision , taken before an uncertain parameter is observed, and a wait-and-see (recourse) decision , taken after. Stochastic programming minimizes the expected total cost under a known distribution of ; robust optimization minimizes the worst-case cost over a support set. Distributionally robust optimization sits between the two: it minimizes the worst-case expected cost over an ambiguity set of distributions consistent with the available data. When the data are samples , a natural ambiguity set is the ball of radius around the empirical distribution in the Wasserstein distance, which contains the two-stage stochastic program with a discrete distribution () and, for a bounded support, the two-stage robust program (large ) as special cases.
Single-stage Wasserstein problems with piecewise-linear losses admit finite convex reformulations (Mohajerin Esfahani and Kuhn; Gao and Kleywegt). Two-stage problems are generically NP-hard, and the existing approaches were exponential-size reformulations or decision-rule restrictions. Hanasusanto and Kuhn (arXiv:1609.07505v3) show that two-stage distributionally robust linear programs over a 2-Wasserstein ball are equivalent to, or approximated arbitrarily well by, copositive programs of polynomial size: all the difficulty is moved into the cone. This mission formalizes that result, Theorem 5 of the paper, and the chain of lemmas behind it (§3, pp. 7–19).
The first-stage decision ranges over a set with cost . The recourse function is the optimal value of a linear program,
where and are affine in and ; its value lies in . The uncertain parameter takes values in the polyhedron , assumed non-empty. The problem has complete recourse if for some , and sufficiently expensive recourse if for every there is with (the dual recourse problem is feasible); the latter is a standing assumption.
The worst-case expectation is
with the 2-Wasserstein distance for the Euclidean cost. Problem (1) is: minimize over .
A symmetric matrix is copositive () if for all , strictly copositive () if for all nonzero , and completely positive () if for an entrywise nonnegative . The extended data stack the support constraints under the recourse data: , , , , (in the paper, and are script letters).
For , is the value of the copositive program (24): minimize over , , , , subject to a block matrix built from , , , , and the extended data being copositive for every ; enters only as in the middle diagonal block. is the value of the completely positive program (25), with objective . At these are (10) and (14), with values and . Problem (28) replaces in (1) by .
Under the standing assumptions,
The result. Theorem 5 turns an infinite-dimensional min–sup–min problem into a single finite conic program whose size is polynomial in . Replacing the copositive cone by any of the known inner approximation hierarchies then yields a sequence of tractable conservative approximations, which is how the paper obtains its numerical method. Item 4 states that without complete recourse nothing is lost asymptotically: the perturbed programs approximate (1) from below to arbitrary accuracy. The same statements cover classical two-stage robust optimization with bounded polyhedral uncertainty (Corollary 1).
Formalizing it. The result is proved in the paper; no machine-checked proof of it is known. A complete development would give the first formal treatment of copositive and completely positive duality, of the moment/dual reformulation of Wasserstein balls around an empirical distribution for extended-real losses, and of an epi-convergence argument for parametrized optimal values. The paper omits the proof of Proposition 1 ("Details are omitted for brevity"), so a formal proof also fills a gap in the written argument.
Lagrangian duality between (10) and (14) gives only , and Example 1 of the paper (p. 15) shows that this gap can be infinite: the obvious "dualize and invoke strong duality" argument fails without a constraint qualification, and the copositive cone has no tractable description from which one could be read off. The equality is not a duality statement at all: it compares a supremum over probability measures with a supremum over completely positive moment matrices, and feasible moment matrices need not come from any distribution on when is unbounded. Theorem 1 already requires the moment and duality theory of Wasserstein balls for an extended-real, possibly discontinuous loss. Item 4 of the goal is an exchange of a limit in with an infimum over , which fails without compactness and without lower semicontinuity of in , a property not visible from the definition of as an infimum.
The Lean development uses the namespace WassTwoStage.Copositive. Uncertain parameters live in EuclideanSpace ℝ (Fin K); matrices act on coordinate vectors, and stacked blocks are indexed by sum types (Fin N₂ ⊕ Fin J, Fin M ⊕ Fin J, and Fin K ⊕ ((Fin M ⊕ Fin J) ⊕ Unit) for the block matrices). and are affine maps. Every optimal value, including , , , and the values of (1) and (28), is an infimum or supremum in EReal, so an infeasible copositive program has value . Limits are taken in the order topology of , from the right. The expectation of the extended-real recourse value is when its positive part has infinite integral. The Wasserstein ball, empirical distribution, expectation and copositivity are reused from published platform definitions.
The following hypotheses, implicit in the paper, are explicit binders: ; for every ; ; sufficiently expensive recourse; (and only for the dual (6)). "For any fixed " is stated for every . A minimizer for (28) is the first-stage part of a solution, minimizing ; the inner infimum need not be attained. The completely positive cone allows any finite number of columns. Item 2 of the goal drops the paper's assumption "(1) fails to have complete recourse", which the bound does not use.
The statement cannot be trivialized: is defined as the supremum over the Wasserstein ball, not by (5) or (6); no Bochner integral (which returns for non-integrable integrands) and no real-valued sSup/sInf occur; copositivity quantifies over the whole nonnegative orthant, not over all of ; and item 1 asserts equality of values and of minimizer sets, not an inequality.
A complete proof needs conic duality for the copositive/completely positive pair, the Wasserstein moment duality of Theorem 1, measurable selections, and lower semicontinuity and epi-convergence arguments. The cone and Schur-complement lemmas (Lemmas 1, 3, 4) and Theorem 1 are reusable beyond this mission. Proofs of individual milestones, alternative arguments, and supporting lemmas are welcome.
Many problems in optimization, game theory and mechanics come down to a variational inequality: find a point of a convex set at which a given vector field points "inward" against every feasible direction. Constrained convex minimization (where the field is a gradient), saddle-point problems (where it is the gradient of a convex–concave function with one sign flipped), Nash equilibria of convex games and complementarity problems are all of this form. In large-scale and infinite-dimensional settings the methods of choice are projection methods, which use only evaluations of the field and projections onto the feasible set.
The plain projected gradient iteration does not converge for merely monotone fields: on a rotation field in the plane it spirals outward for every step size. Korpelevich's extragradient method (1976) repairs this with two field evaluations and two projections per iteration. Later methods (Tseng's forward–backward–forward method, 2000; the subgradient extragradient method of Censor, Gibali and Reich, 2011) reduce the number of projections to one, but still need two evaluations of the field.
Yu. Malitsky's paper (arXiv:1502.04968, SIAM J. Optim. 25(1), 2015, doi:10.1137/14097238X) introduces the projected reflected gradient method, which uses one projection and one field evaluation per iteration, evaluated at a "reflected" point, and proves that it converges weakly under the same assumptions as the extragradient method. This mission formalizes that convergence theorem, Theorem 3.2 of the paper.
Let be a real Hilbert space with inner product and norm . Let be closed and convex, and let be a mapping. For , the metric projection is the unique point of nearest to (it exists when is nonempty). The variational inequality (1.1) asks for with
and denotes its solution set. The standing assumptions are:
Algorithm 3.1 (projected reflected gradient method). Fix a step size and a starting point , and iterate
The point is the reflection of through . A sequence converges weakly to , written , if for every .
Under (C1)–(C3), for and every run of Algorithm 3.1 there is with
In the order the proof uses them:
Companion items, not milestones: the defined projection is the metric projection (so runs of Algorithm 3.1 exist from every starting point), Remark 2.1 ( is closed and convex), and the characterization of as the zeros of the projected residual (§3, p. 4).
The result. Theorem 3.2 shows that a monotone Lipschitz variational inequality in Hilbert space can be solved by an iteration costing one projection and one evaluation of per step, the minimum for a projection method, with no knowledge beyond the Lipschitz constant. This halves the cost of each iteration relative to the extragradient method when evaluating is expensive, and keeps the cost of projections at one when projecting onto is expensive. The method and its analysis became the basis for several later algorithms, including the adaptive variant in §4 of the same paper and the golden ratio algorithm of Malitsky (2020).
Formalizing it. The theorem is proved in the paper; no machine-checked proof is known to exist. The formal development needs, beyond the main argument, a usable library of facts about projections onto closed convex sets in Hilbert space, weak convergence of sequences (boundedness of weakly convergent sequences, weak sequential compactness of bounded sets) and Opial's property. These are reused by every weak-convergence proof for splitting and projection methods, and several companion missions of this series and of related papers rely on the same facts.
The naive Lyapunov function is not monotone along the iteration: because is evaluated at the reflected point rather than at , the cross terms do not cancel as they do for the extragradient method. The quantity that does decrease (milestones 3–4) carries extra terms, and the step bound is what the decrease requires. As a consequence, itself is not known to converge, so the standard Opial lemma ("if converges for every and all weak cluster points lie in , then converges weakly") does not apply directly; the uniqueness of the weak cluster point has to be argued with the perturbed quantity and Opial's inequality. In infinite dimension, the weak cluster point step also needs weak sequential compactness of bounded sets, which is not norm compactness.
[CompleteSpace H] in every statement that needs completeness; it is never specialised to , where weak and norm convergence coincide.Contributions welcome: proofs of the milestones in any order; general Hilbert-space lemmas (boundedness of weakly convergent sequences via the uniform boundedness principle, weak sequential compactness of bounded sets, Opial's inequality) are useful well beyond this mission.
Many engineered and natural systems are networks of identical dynamical units coupled through a directed interaction graph: arrays of oscillators, power grids, sensor and multi-agent networks, gene regulatory circuits. A basic control question for such a network is how to force every unit onto a prescribed reference trajectory (an equilibrium, a periodic orbit or a chaotic solution of a single unit) by acting on only a few of them. Applying a feedback controller to a small fraction of the vertices and letting the coupling spread its effect is called pinning control. It was introduced for scale-free networks by Wang and Chen (2002), shown to work with a single controller on undirected networks by Chen, Liu and Lu (2007), and turned into checkable criteria for undirected networks by Yu, Chen and Lü (2009).
Directed networks are harder. Earlier criteria for directed networks (Zhou, Lu and Lü 2008; Song and Cao 2010) were stated through the symmetric part of the coupling matrix, which may have eigenvalues with positive real part even when the network synchronizes, so they lose the structural information of the graph. Yu, Chen, Lü and Kurths (SIAM J. Control Optim., 2013) replaced the standard quadratic Lyapunov function by one weighted with the positive left null vector of the coupling matrix. This mission formalizes their main criterion for strongly connected networks (§3 of the paper) together with the matrix-theoretic lemmas it rests on (§2).
The network has vertices with states . A coupling matrix has for ( means a connection from vertex to vertex ) and zero row sums, . The network is strongly connected if any vertex can be reached from any other by a directed path; is irreducible if no simultaneous permutation of rows and columns brings it to block lower-triangular form with square diagonal blocks of sizes and , . The in-degree of vertex is .
Each vertex runs the dynamics for a continuously differentiable . A reference trajectory solves . With coupling strength , inner coupling matrix and control gains (vertex is pinned when ), the controlled network is
It is globally synchronized if for every , every reference trajectory and every solution. The vector field satisfies Assumption 1 if, for a constant matrix ,
For positive weights put , and .
Let satisfy Assumption 1 with symmetric, let be a strongly connected coupling matrix, and let be positive with having zero row sums (the weights of Lemma 2.12). If
then the controlled network is globally synchronized.
The path to the goal follows the paper: Lemma 2.5 (irreducible strongly connected), Lemma 2.9 ( for nonnegative with constant row sums), Lemma 2.8 (Perron–Frobenius, already on the platform), Lemma 2.11 (a positive vector with ), Lemma 2.12 (the weights ), and the derivative estimate (3.4) for , :
Lemma 2.7, Lemma 2.10, and, under the paper's standing assumptions (, ) with positive definite: Corollary 3.2 (the condition suffices), Corollary 3.3 (i) (an explicit coupling threshold ), and Corollary 3.4 (the necessary conditions at pinned and at unpinned vertices).
The criterion reduces global synchronization of an -dimensional nonlinear system to one linear matrix inequality in the data , and the corollaries reduce it further to an inequality and to explicit bounds. Corollary 3.4 turns this into a pinning rule: vertices whose in-degree is below must be controlled. Weighting by the left null vector of is the device that later work on directed consensus and pinning reuses; Lemmas 2.11 and 2.12 isolate it as a statement about Metzler matrices.
The paper's results are proved on paper; none of them has a machine-checked proof that this mission is aware of. A formalization adds three things: a corrected statement of Theorem 3.1 (see the scope section), a Lean library of directed-network matrix facts (irreducibility in the permutation form, its equivalence with strong connectivity, positive left null vectors, the weighted symmetrization ), and a reusable Lyapunov argument for linearly coupled networks with Kronecker-structured quadratic forms.
The obvious first idea, the unweighted Lyapunov function , produces the symmetric part of , which for a directed network need not be negative semidefinite; this is exactly the defect of earlier criteria. The weights must come from a positive left null vector of , whose existence is a Perron–Frobenius statement that needs irreducibility, hence the graph–matrix equivalence of Lemma 2.5. The analytic part needs a derivative of along solutions on , the conversion of a sum over vertices into a Kronecker quadratic form, and the passage from a negative definite form to convergence of every error component. On the Mathlib side, irreducibility in the paper's permutation sense, spectral radius through characteristic roots, and largest eigenvalues of symmetric matrices all have to be connected to existing API.
States are Fin n → ℝ and matrices are indexed by Fin N, Fin n and, for Kronecker products, by pairs (i, a) with ; the stacked error uses the same order. Convergence (2.7) is stated with the neighbourhood filter of in , which does not depend on the norm. Derivatives are taken within . Pinning is encoded by instead of the paper's reordering of the first vertices. "" is positive definiteness of (Mathlib PosDef, which includes symmetry); every matrix compared with is symmetric by construction. of a symmetric matrix is the least with for all ; is the largest modulus of a complex characteristic root. Global synchronization quantifies over every reference solution and every network solution; existence of solutions is not asserted.
Added hypotheses, each disclosed in the item: in Theorem 3.1 and (3.4), because the printed theorem allows any and is then false (a directed 3-cycle with satisfies (3.2) but its error grows); in Corollary 3.4; at least one pinned vertex in Corollary 3.3 (i); in Lemma 2.10. The weights are not arbitrary: Theorem 3.1 and the corollaries require to have zero row sums, which for a coupling matrix is equivalent to . Assuming the derivative bound (3.4), negative definiteness of or decay of in the goal would trivialize it and is excluded.
The mission needs: graph reachability for matrices with nonnegative off-diagonal entries; Perron–Frobenius for irreducible nonnegative matrices (referenced from the platform); Gershgorin-type bounds; Kronecker products and positive definiteness; and calculus of quadratic forms along solutions. The matrix lemmas (2.5, 2.7, 2.9–2.12) are reusable beyond this mission. Proofs of any item, and alternative proofs of the milestones, are welcome. Corollary 3.3 (ii) is not posed.
A chance constraint asks that an uncertain constraint hold with high probability: a decision is acceptable if the loss it incurs is nonpositive with probability at least . Chance constraints appear in portfolio selection, power-system dispatch, inventory control and engineering design, wherever an occasional violation is tolerable but a frequent one is not. Two obstacles stand in the way of using them. The distribution of is rarely known exactly, and even when it is, the feasible set of a chance constraint is in general nonconvex and hard to compute.
Distributionally robust chance constraints address the first obstacle by requiring the constraint to hold for every distribution consistent with the available information. Zymler, Kuhn and Rustem (Math. Program. 137, 2013) take that information to be the mean and the covariance of . The standard way around the second obstacle is to replace the probability by the Conditional Value-at-Risk (CVaR) of Rockafellar and Uryasev (J. Risk 2, 2000): a nonpositive CVaR implies the chance constraint, and the worst-case CVaR over a moment set can be computed by semidefinite programming. The approximation is conservative, and the question this mission formalizes is when it loses nothing.
Timeline. Isii (Ann. Inst. Statist. Math. 12, 1960) established strong duality for moment problems, the basis of generalized Chebyshev bounds; Calafiore, Topcu and El Ghaoui (Systems & Control Letters 58, 2009) gave the semidefinite form of the worst-case probability of a set under mean and covariance information that the paper uses as Lemma A.2. El Ghaoui, Oks and Oustry (Oper. Res. 51, 2003) computed the worst-case Value-at-Risk of a portfolio under mean and covariance information. Calafiore and El Ghaoui (J. Optim. Theory Appl. 130, 2006) showed that a distributionally robust individual chance constraint with a loss affine in is a second-order cone constraint. Zymler, Kuhn and Rustem (2013) showed that the worst-case CVaR approximation is exact for every continuous loss that is concave or quadratic in (Theorem 2.2), which is the goal of this mission, and extended the approach to joint chance constraints (the companion mission II).
Let be a random vector in . Fix a mean vector and a covariance matrix with (positive definite). The moment set is the set of all probability distributions on with finite second moments, and . The second-order moment matrix is
and is the trace scalar product.
Fix a tolerance and a loss . Write . The CVaR of under is
and the worst-case CVaR is its supremum over . The distributionally robust individual chance constraint is . The worst-case Value-at-Risk is
A loss is quadratic if , with no sign condition on .
For a continuous loss that is either concave or (possibly nonconcave) quadratic in ,
The implication from left to right holds for every loss; the content of the theorem is the converse.
The theorem says that for concave and for quadratic losses the worst-case CVaR constraint, which is a linear matrix inequality in the decision through (20), describes exactly the feasible set of the distributionally robust chance constraint. Its affine special case (Corollary 2.1 of the paper) gives an exact semidefinite representation of robust individual chance constraints with affine dependence on the uncertainty, the case most used in robust portfolio and engineering models. The same equality between worst-case CVaR and worst-case VaR is the starting point of the paper's treatment of joint chance constraints, where an exact representation is obtained by optimizing over scaling parameters (mission II). The quadratic case covers losses such as portfolio variance terms or quadratic constraint functions, which are neither convex nor concave in general.
The results are proved in the paper, but parts of the argument are sketches. Lemmas A.1 and A.2 are strong duality theorems for moment problems that the paper cites from Isii and from Calafiore et al. rather than proves, and the interchange of supremum and infimum in the worst-case CVaR is justified by a citation to a stochastic saddle-point theorem. To our knowledge none of these results has a machine-checked proof. A formalization produces a checked moment-duality theorem with given mean and covariance, a nonlinear Farkas lemma, and a complete proof of the exactness theorem.
The direction from the worst-case CVaR constraint to the chance constraint is elementary. The converse cannot be obtained distribution by distribution: for a single distribution the CVaR is strictly larger than the VaR in general, and for a convex piecewise-linear loss the worst-case equivalence fails (Example 2.1 of the paper). The identity therefore depends on the specific moment set and the specific loss classes, and passes through two infinite-dimensional dualities. The moment set is not compact in the weak topology, since mass can escape to infinity while the first two moments stay fixed, so the minimax interchange in the worst-case CVaR does not follow from a standard compact minimax theorem. Lemmas A.1 and A.2 are stated for an arbitrary measurable function and an arbitrary Borel set; their strong duality uses in an essential way. Finally, the semi-infinite constraint "for all with " involves a strict inequality on a nonconvex set, and turning it into a matrix inequality is where concavity or quadraticity of enters.
Fin k → ℝ; matrices in are indexed by Fin k ⊕ Unit with the extra coordinate last, so that is liftQuad M ξ. is built from the published ConvexOptimization.symQuadBlock.MomentDRO.Conf.HasSecondMoments, meanVec, covMat). It is not restricted to discrete laws, densities or a support set.A complete development needs moment-problem duality on , a convex Farkas lemma, and the S-procedure (already proved on the platform). The first two are reusable beyond this mission, in particular by mission II, which uses Lemmas A.1 and A.2 verbatim. Proofs of any milestone are welcome independently.
An online classifier must predict a label before learning the correct answer. Its errors matter directly: a low numerical loss is useful only if it controls the number of wrong predictions. Chapter 8 of Orabona's textbook examines this connection for linear classification, where a vector of weights produces a score by taking an inner product with the incoming example. The Perceptron is a particularly spare example: it changes its weights only after a mistake, and it needs no learning rate or chosen comparator. This makes its guarantee a useful point of contact between classification mistakes and the convex losses used elsewhere in online optimization.
Theorem 8.2 compares the Perceptron's mistake count with a whole family of comparator losses, indexed by a real exponent . The theorem is a known result in the book, not an unsolved conjecture. The mission concerns a faithful Lean statement and, subsequently, its machine-checked proof. The distinction matters because other Perceptron bounds on the platform address batch separability, multiclass prediction, or a hinge loss only on update rounds; those results do not state this theorem with its constants and quantifiers.
Fix a dimension and a sequence of feature vectors with binary labels , for rounds . The Perceptron begins at . At round it predicts , where . It records a mistake when and, on exactly those rounds, adds to its weights. Write and . A zero score is a mistake even though it is not a strict sign disagreement.
For a score , a label , and a real power , the hinge-power loss is . A fixed competitor has cumulative loss . The loss is zero when gives every example the correct sign with margin at least one. The book assumes the input vectors obey ; is a nonnegative radius. The sequence is arbitrary, so the result includes examples chosen with knowledge of earlier predictions.
The goal is Theorem 8.2, p. 144 of Orabona. For every and every real ,
All constants and the full family of powers are part of the target. For a competitor with , choosing yields the finite mistake bound , as the book explains on p. 144. For a nonseparable sequence, the same statement measures mistakes relative to the competitor's nonzero loss.
The milestone list follows the book's named ingredients: Lemma 4.29 converts an implicit square-root inequality into an explicit one; the constant-step clause of Theorem 2.13 gives the linear-loss gradient bound; and displays (8.4) and (8.5) relate the Perceptron updates to the comparator and to the hinge loss. Theorem 2.13 is stated in the linear, whole-space case used on p. 145. The printed (8.4) has an invalid extra term on its left; the milestone retains the printed text for provenance, while the Lean statement gives the valid comparator inequality used by (8.5). The correction is described in the item and moderation notes.
The guarantee answers a practical question about a simple online rule: how many classification errors can it make when a fixed linear predictor has small convex loss? The answer has explicit dependence on the feature radius, comparator norm, loss exponent, and comparator loss. It contains the separable margin case and also applies when no comparator classifies every example with margin one. The quantifier over all permits a later analyst to choose a competitor after seeing the sequence without changing the algorithm or the theorem.
A complete formalization would provide a reusable account of a deterministic online classifier, its exact zero-score convention, and the passage from update counts to a family of hinge losses. The local Lean declarations currently compile as statements with proof placeholders; compilation does not establish the mathematical inequalities. A proof of the goal and milestones remains to be supplied and checked. In particular, the correction to (8.4) should be made explicit in any downstream development so that later results never depend on the false printed left side.
The mistake count is discontinuous in the prediction score, while the competitor is measured by a smooth family of convex surrogates. A direct comparison of their per-round losses does not give the theorem's constants. The update rule also depends on its own current score, so its condition must be tied to the weight sequence generated by earlier rounds. Treating the update indicators as free variables, or counting only rounds with a strictly negative score, changes the statement.
The book's proof passes through an implicit inequality involving . That relation alone is weaker than the displayed goal until its constants and nonnegative domains are handled precisely. Real powers require special attention at a zero hinge value. The printed (8.4) introduces an additional difficulty: with and two one-dimensional examples , carrying positive labels, its left side is positive while its right side is zero. The valid comparator inequality has to be distinguished from that printed display.
Lean uses EuclideanSpace ℝ (Fin d) for , its Euclidean inner product and norm, and sequences indexed by natural numbers with active rounds . Index zero carries no data requirement. A total recursive definition fixes and every later Perceptron update. Mathlib's Real.sign supplies ; an indicator records both a wrong sign and a zero score. The comparator loss uses a maximum with zero before taking a real power. No probability space is needed because Algorithm 8.2 is deterministic.
The Lean theorems explicitly require binary labels on the active rounds, for the goal, , and . They allow , , and ; the formulas remain meaningful in these cases. The set in the book's theorem is omitted because the assertion uses only the given feature sequence and its norm bound. The constant-step milestone requires because its formula divides by . The definitions include a mistake count, hinge-power loss, cumulative comparator loss, and the fixed algorithm; the theorem layer can reuse Mathlib's inner-product and real-analysis results. Contributions toward these statements, the algebraic milestone, or the full theorem proof are in scope. A run that can skip a zero-score update or whose iterates are chosen independently of the recursion is outside this mission.
Phase recovery asks to reconstruct a complex signal from the moduli of linear measurements, , where is known. The problem arises in X-ray crystallography, diffraction imaging and microscopy, where detectors record intensities but not phases (Shechtman et al., 2015). Since the map is not linear, the problem is non-convex, and a line of work since 2011 replaces it by semidefinite programs over Hermitian matrices.
Two such relaxations are compared in this mission. PhaseLift (Candès, Strohmer and Voroninski, 2013) lifts to and asks for a positive semidefinite with ; its trace-free version is called Weak PhaseLift. PhaseCut (Waldspurger, d'Aspremont and Mallat, 2015) separates amplitude and phase, with , and relaxes the resulting complex MaxCut-type problem to a semidefinite program in a Hermitian matrix with unit diagonal. In the noiseless case the two relaxations are equivalent (Corollary 4.3 of that paper). This mission formalizes the paper's comparison of the two in the presence of noise: Theorem 4.7 and the two lemmas of Appendix A behind it.
Write for the Hermitian complex matrices and for the positive semidefinite ones. Let be the orthogonal projector onto the range , with the Moore–Penrose pseudoinverse. Define the face
the affine section , and the trace-norm distance , where .
After rescaling, PhaseCut minimizes over with . By Lemma 4.1 this objective equals for , so PhaseCut is the projection problem
Weak PhaseLift, as solved by first-order methods with an distance (), is the projection problem in the other direction,
Both aim at a point of ; PhaseCut starts from , Weak PhaseLift from .
Noise enters through with . With the Frobenius norm of a matrix and the Euclidean norm of a vector, an algorithm is -stable at (Definition 4.5) if, for every close enough to zero, every minimizer of its problem satisfies
For , , and :
The constant is the paper's. The paper remarks that any would do, but that variant is printed without proof and is not a target.
The theorem says that PhaseCut is "almost as stable as" Weak PhaseLift: any stability guarantee proved for the lifted relaxation, such as the noisy recovery bounds of Candès and Li for Gaussian measurements (Candès and Li, 2014), carries over to PhaseCut with a constant of the same order. This justifies using PhaseCut, whose block-coordinate algorithms are cheap, with the stability theory developed for PhaseLift. The paper notes that the converse transfer does not seem to hold.
The result is proved in the paper. No part of it has a machine-checked proof that we know of. Formalizing it means proving the trace-norm identity of Lemma 4.1, which needs a Hölder-type bound for an orthogonal projector , the matrix Cauchy–Schwarz estimates of Appendix A, and the contradiction argument of Theorem 4.7, all for complex Hermitian matrices and an arbitrary, possibly non-injective, .
The obvious argument transports a PhaseCut minimizer to a Weak PhaseLift minimizer, but is in general not in , and its compression is not in for the same noise. Two estimates are needed at once: the distance between and , and the size of the new noise vector . Both rest on bounding by the squared noise, which uses the optimality of in (13) against a specific competitor, and on Lemma 4.1, whose printed proof is incomplete: the matrix it calls the projection of onto is not the trace-norm projection in general, so the identity requires a separate lower bound.
Matrices are Matrix (Fin n) (Fin p) ℂ, and signals are vectors Fin p → ℂ. is the matrix of Mathlib's orthogonal projection onto LinearMap.range (toEuclideanLin A); no pseudoinverse is built. The trace norm is the published definition WildeQIT.traceNorm (), and is a real infimum over a nonempty set bounded below by . Frobenius and Euclidean norms are written out as square roots of sums of squares. Diagonal entries and traces of Hermitian matrices are read through their real parts. Lemma 4.1 is stated in , so it also asserts that the trace is real. "Close enough to zero" is , and stability quantifies every minimizer for every small noise.
The formal statements depart from the print in three places:
The case is not excluded; there the hypothesis on Weak PhaseLift fails, as the paper notes. The milestones keep only the hypotheses their proofs use, listed in each statement.
A trivializing formalization would define the minimizer predicates so that no matrix satisfies them, or quantify the noise before . Here (13) and (14) both have minimizers (checked for ), and precedes the noise.
Needed infrastructure: the trace norm and its duality with the operator norm on Hermitian matrices, compressions by orthogonal projectors, and Cauchy–Schwarz for positive semidefinite forms. These are reusable for other trace-norm and semidefinite-relaxation missions. Proofs of the milestones in any order are welcome, as are proofs of the general facts as separate lemmas.
In online convex optimization, a learner selects a point before seeing the current loss. A useful guarantee compares the learner's accumulated loss with that of a single fixed point chosen in hindsight. A step size chosen from a preannounced bound on all future gradients can be wasteful when the realized gradients are small. Chapter 4 of Orabona's online learning text studies step sizes determined from the gradients observed so far. Its adaptive online subgradient descent bound uses the actual sum of squared subgradient norms, without requiring that sum in advance (Theorem 4.14, p. 40).
The chapter then asks for a more informative guarantee when the losses have small values at a good competitor. For self-bounded losses, a small loss at a point limits the size of its subgradients. Theorem 4.30 on p. 45 turns that relation into a bound in terms of the competitor's cumulative loss. This is useful for problems such as the squared hinge loss discussed immediately after the theorem: if one feasible comparator has zero loss on every round, the regret bound becomes independent of the number of rounds. These are known textbook results. The goal here is a machine-checked formulation and, eventually, a proof of the stated constants.
Fix a finite horizon and a nonempty, closed, convex decision set . Its Euclidean diameter is at most : every satisfy . In round , the learner plays and receives a convex loss . The loss sequence is arbitrary. A subgradient of at satisfies for every . The regret against a fixed competitor is
The learner uses projected online subgradient descent. After observing , it sets
when . If , the algorithm leaves . Here is a Euclidean nearest point in . The current gradient appears in the sum defining because the update is made after that gradient is observed. The initial point is any member of , and every admissible choice of subgradient is allowed.
A loss is -self-bounded on when it is bounded below, has a subgradient at each point of , and every subgradient at every satisfies
The infimum is over the whole ambient space. The target theorem additionally assumes that each loss is nonnegative everywhere. The in these formulas is nonnegative. These conventions follow Definition 4.26 and Theorem 4.30 of the pinned preprint.
The first milestone is Theorem 4.14. Under the setting above, for every ,
This bound depends on the gradient sequence encountered by the algorithm. The printed theorem also equates this expression with a minimum over constant positive step sizes. At zero accumulated gradient energy that minimum is an unattained infimum, so the formal milestone states the regret inequality in every case and the identity with the minimum only when the accumulated squared gradient norm is positive.
The goal is Theorem 4.30. If every loss is nonnegative, convex, and -self-bounded on , then for every fixed ,
The target includes the intermediate displayed bound on p. 45 and Lemma 4.29 as milestones. Their statements capture the passage from a regret bound involving the learner's cumulative loss to one involving the competitor's cumulative loss. The constants and are those printed in the theorem; the goal does not replace them with asymptotic notation.
Theorem 4.14 provides a guarantee without supplying a gradient bound or the horizon-dependent sum of squared gradients to the learner. Theorem 4.30 sharpens the interpretation when the losses are self-bounded: for a comparator with , the regret is at most . For larger comparator losses, the bound changes continuously with their accumulated value. The guarantee holds against each competitor, not merely one selected by an infimum over .
A formal development would make the algorithm's timing, its zero-gradient branch, the ambient-space infimum, and the exact numerical constants explicit. These details are reusable in later analyses of adaptive step sizes and small-loss bounds. The proposal contains open Lean theorem statements and a compiled definitions file; it does not claim that these results already have machine-checked proofs in this mission. The metric projection relation is reused from an existing published definition, and the intended work is proving the open statements and developing their supporting inequalities.
A fixed step size can be selected after looking at all gradients, but that selection does not define an online update. The adaptive step size must use only gradients observed through the current round. The zero-gradient case needs an explicit update rule because its displayed quotient has a zero denominator on an all-zero prefix. These issues already appear in the first milestone.
For the goal, the self-bounded inequality controls subgradient norms using loss at the learner's own points. Substituting that control into the gradient bound yields a right-hand side containing , although the desired statement is expressed using . The intermediate estimate on p. 45 is therefore implicit. The square-root inequality of Lemma 4.29 supplies the separate arithmetic statement needed to express the final result with the printed constants. A direct substitution that treats the learner's loss as the competitor's loss would not justify the theorem.
The Lean carrier is EuclideanSpace ℝ (Fin d), including dimension zero; the theorem remains valid there. Rounds are indexed from one, with index zero unused, and sums range over Finset.Icc 1 T. The loss functions are real-valued on the whole Euclidean space. The book permits extended-real losses that take outside their domain; this formalization addresses the real-valued case. Full-space subgradients retain the source's definition. Convexity and nonnegativity hold on the whole Euclidean space, and self-boundedness holds at every feasible point, for each round through .
The adaptive run is a relation covering every legal selection of subgradients and projections. It requires the update after every nonzero gradient and the unchanged point after a zero gradient. The closed, convex, nonempty set assumptions ensure that Euclidean projection is meaningful. The diameter condition is written as for all feasible , so it also covers any valid upper bound on the diameter. Self-boundedness uses the real infimum of the full range of each loss, together with boundedness below; global nonnegativity in the goal guarantees that condition. The explicit and conditions prevent boundary values from silently changing the meaning of a quotient or a square root.
The goal must hold for every comparator and every admissible run. A definition that checks self-boundedness only at , or permits arbitrary next decisions, would lose the algorithmic guarantee. The reusable components are the regret and gradient-energy definitions, the adaptive run relation, the self-boundedness predicate, and the scalar inequality in Lemma 4.29. Contributions that establish the projection analysis and the three listed milestones directly support the goal.
In online learning, a decision is made before the loss for that round is revealed. The learner cannot optimize a known objective once and use its minimizer forever: the sequence of objectives may be arbitrary. A basic performance measure is regret, the learner's total loss minus the loss of one fixed decision chosen with hindsight. A regret bound that grows more slowly than the number of rounds shows that the learner's average excess loss vanishes. Orabona's introduction develops this measure and derives a bound for projected online gradient descent without requiring advance knowledge of the loss sequence (Orabona, Chapter 1 and Theorem 2.13).
The result is useful because it separates the geometry of the feasible set from the size of the gradients seen during play. It also supports step sizes that change with time, which matters when a learner adjusts its updates as more rounds pass. The exact endpoint term in the theorem records information that would be discarded by a coarser regret estimate (Orabona, Theorem 2.13 and the discussion on p. 14).
Let be a nonempty closed convex set in a real inner-product space. At round , the learner chooses , receives a differentiable convex loss function , and incurs . For a fixed competitor , the book's regret is
The competitor stays fixed through all rounds; it is not the best separate decision for each round. The losses may differ on every round, and their sequence is arbitrary (Orabona, p. 2).
A metric projection is a point of nearest to in Euclidean distance. Convexity makes the projection single valued when is nonempty and closed. Projected online gradient descent, Algorithm 2.1, starts from an arbitrary , chooses positive step sizes , forms , and sets
The projection keeps the next decision feasible even when the unconstrained gradient step leaves (Orabona, Algorithm 2.1, p. 12). The first-order optimality condition of Theorem 2.8, the projection inequality of Proposition 2.11, and the one-round inequality of Lemma 2.12 are the numbered milestones leading to the main statement. Lemma 2.31 records the parallel one-round statement for subgradients (Orabona, pp. 11–13, 19).
For of finite diameter , positive nonincreasing step sizes, and any , the main target is the complete first inequality of Theorem 2.13:
The negative terminal term is part of the target. The constant-step clause of the same theorem is a separate companion item. If on every round, it states
This clause has no finite-diameter hypothesis, so it applies on unbounded feasible sets as well (Orabona, Theorem 2.13, p. 13).
The theorem gives a deterministic guarantee against every fixed feasible competitor, for every loss sequence and every valid run of the algorithm. It exposes the cumulative effect of the gradient magnitudes and the step sizes. Its constant-step form uses the distance from the initial decision to the comparator rather than the diameter of the whole set. The bound is therefore informative on some unbounded sets where the diameter term has no finite value (Orabona, Theorem 2.13 and p. 14).
This is a known textbook theorem, not an open conjecture. The mission asks for machine-checked proofs of the source statements in a reusable Lean interface: a fixed-comparator regret definition, a finite-horizon run predicate, and the projection and one-step results. The published metric-projection predicate is reused, while the one-based regret and run definitions are specific to this book's convention.
An immediate attempt to sum the one-round estimate leaves squared-distance terms with different coefficients when the step size varies. They do not cancel as they would with a fixed coefficient. The theorem's monotonicity condition on the step sizes and the finite diameter of are what make a uniform bound possible; omitting either changes the first displayed claim. Keeping the final negative squared-distance term also requires more care than proving only the weaker bound obtained by dropping it. On the nonsmooth side, an arbitrary vector cannot replace a subgradient: its defining inequality supplies the link between a loss difference and the linearized direction (Orabona, Lemmas 2.12 and 2.31, Theorem 2.13).
Lean uses a complete real inner-product space, covering the book's and using only the geometry needed by this chapter. Time remains one based: round zero is unused, sums run from through , and the output after the last round is . The horizon satisfies , so the last step size and the terminal iterate are part of an actual run. The run predicate requires a gradient and a metric projection at every round through ; it does not select a favorable projection after seeing the comparator. The theorem requires each loss to be convex and differentiable on an open neighborhood containing , as in Algorithm 2.1.
The diameter in the main target is Mathlib's real Metric.diam V, with boundedness imposed so that it is the finite supremum in the book. The constant-step clause has no boundedness requirement. The projection relation is the published OnlineConvexOpt.FirstOrder.IsMetricProjection: it includes membership in and minimal distance to the point being projected. Thus, the update cannot be satisfied by an arbitrary point of . Every regret claim quantifies over a comparator ; extending the quantifier outside would assert a different result.
For Lemma 2.31, losses are real valued on , and the stated subgradient inequality is relative to . The book defines a full-space subgradient for an extended-real-valued function; every such subgradient gives the relative inequality used here. This is the precise convention for that milestone and is disclosed in its item description. Contributions that establish the projection inequality, the single-round inequalities, and either complete form of Theorem 2.13 fit the mission. The regret and run definitions can be reused in later deterministic online optimization results, while the projection predicate is already shared with another textbook development.
When the players of a game repeatedly adjust their strategies with no-regret learning algorithms, the empirical distribution of play converges to a coarse correlated equilibrium, and in smooth games the average social welfare approaches the price-of-anarchy guarantee of the game (Roughgarden 2009). For generic no-regret algorithms such as Hedge the convergence rate is , because each player's regret after rounds is of order in the worst case, against an adversary.
Other players are not adversaries: they are also learning, and their strategies change slowly. Syrgkanis, Agarwal, Luo and Schapire (NIPS 2015, arXiv:1507.00407v5) identify a property of learning algorithms, regret bounded by variation in utilities (RVU), under which this predictability can be exploited in general multi-player games, and show that a natural class of algorithms has it. This mission formalizes their first main consequence: if every player uses optimistic follow the regularized leader (OFTRL), the sum of all players' regrets stays bounded by a constant independent of , so the average welfare converges at rate .
Timeline. Rakhlin and Sridharan (COLT 2013; NIPS 2013) introduced optimistic mirror descent and showed convergence to the minimax value in two-player zero-sum games when both players use it. Syrgkanis et al. (2015) extend the fast-rate phenomenon to general -player games and arbitrary no-regret algorithms with the RVU property (Theorem 4), and establish RVU for OFTRL (Proposition 7), giving Corollary 8.
A game has players. Each player has a finite strategy set with , and a utility for each pure profile . A mixed strategy is a point of the probability simplex , and a mixed profile induces the product distribution on pure profiles.
The game is played for rounds. At round each player picks and then observes the utility vector with entries
so that is the expected utility of player at round . The regret of player is
The primal norm is and its dual is . A regularizer is 1-strongly convex if for all , and denotes a bound on its range, on . Optimistic FTRL with step size and predictors plays and, for ,
With one-step recency bias, : the algorithm bets that the next utility vector equals the last one.
An algorithm has the RVU property with constants , if for every utility sequence
If every player runs OFTRL with and , , then for every
A companion statement, Proposition 2 (p. 3), turns a regret bound into a welfare bound in a -smooth game: .
Corollary 8 says that uncoupled learning dynamics, in which each player sees only its own utility vectors, can keep the total regret of all players bounded by a constant in an arbitrary finite game. By Proposition 2 this gives convergence of the average welfare to the price-of-anarchy bound in smooth games, against for generic no-regret algorithms. The RVU framework has since become a standard tool in the analysis of optimistic learning in games, and Theorem 4 decouples the game-level argument from the choice of algorithm.
The paper's proofs are in its supplementary material (App. A and C). None of the results here has a machine-checked proof to our knowledge. A complete formalization produces a reusable layer: utility vectors of mixed profiles, total-variation subadditivity for finite product distributions, and the regret analysis of optimistic FTRL under an -strongly convex regularizer.
The game-level step (Theorem 4) is short once display (2) is available, but (2) itself, subadditivity of total variation over products of finite distributions, is not available in Mathlib in this form.
The core is the single-player analysis. Theorem 19 and Lemma 20 compare the iterates with the leader sequence, an object the algorithm never computes, and both rest on the quadratic-growth fact that a maximizer of a -strongly concave function satisfies . Footnote 3's midpoint inequality does not give the constant in a single application; it has to be upgraded to the standard form of strong convexity first.
Players are Fin n, strategies Fin d; time keeps the paper's indices with and . is the utility vector against , the formula of p. 2 at , which the paper uses but never writes. Mixed profiles and expectations come from the published definition agt_games. is defined explicitly and is Mathlib's sup norm. Regret and are never written as suprema: a bound on is stated for every profile of comparators in , and is any upper bound on the range of every regularizer.
Added hypotheses, each disclosed in its statement:
Theorem 19, Lemma 20 and Proposition 7 are stated for ; the paper allows any norm.
OFTRL is an argmax predicate, so the goal holds for every trajectory the dynamics can produce, not for a chosen one. It is not the entropic closed form (Optimistic Hedge). The utility bound is kept, since the game-level statements are false without it. A sanity file shows that satisfies the strong-convexity hypothesis and that OFTRL runs exist, so the hypotheses are satisfiable.
Contributions are welcome for each milestone. The quadratic-growth lemma for midpoint strongly convex continuous functions on the simplex and the total-variation bound for products are reusable beyond this mission.
Training a model by stochastic gradients on a constrained or regularized loss is a stochastic composite problem: a smooth expected loss, observed only through noisy gradients, plus a simple non-smooth term such as a constraint set or an penalty. For convex losses, accelerated stochastic approximation methods attain the optimal rates (Lan 2012; Ghadimi & Lan 2012). For nonconvex losses, the available guarantees came from randomized stochastic gradient methods (Ghadimi & Lan 2013) and their mini-batch proximal versions (Ghadimi, Lan & Zhang 2016), which are not optimal when the problem happens to be convex.
Ghadimi and Lan (arXiv:1310.3787v1, 2013; Math. Program. 156, 2016) gave one accelerated scheme covering both cases. This mission formalizes its most general result, Theorem 4 (§3.2): the randomized stochastic accelerated gradient (RSAG) method with mini-batches, on a composite objective whose smooth part may be nonconvex and whose gradients are noisy.
Work in with the Euclidean norm. The problem (1.3) is
where is differentiable with -Lipschitz gradient and may be nonconvex, is convex and differentiable with -Lipschitz gradient, , and is a convex, possibly non-smooth function with bounded domain (for instance the indicator of a convex compact set, or that indicator plus ).
The prox map (2.37) is for , and the gradient mapping (2.38) is . With , a small certifies approximate stationarity. Assumption 2 asks for with for all and .
Gradients come from a stochastic oracle: queried at , it returns for a random sample . Assumption 1 asks that the output be unbiased, , with variance at most .
Algorithm 4 takes , for , , batch sizes , starts from , and for sets
With and (2.6), the output is , where is drawn independently of the oracle with
Fix , assume for
let be an optimal solution and . Then
and, if ,
The expectations are over and all samples. The goal keeps general step sizes and batch sizes; Corollaries 4 and 5 (explicit policies) are left for follow-up work.
In the order of the proof: Lemma 4 ( is 1-Lipschitz); the mini-batch variance bound (3.28) and its consequence (3.29) for the gradient mapping; Lemma 1, (2.16) and Lemma 5, the two-sided bound ; the three-point inequalities (3.32)–(3.33) and their combination (3.34); the descent bound (2.46) (already proved on the platform) and (2.47); the one-step and summed inequalities of p. 22; the iterate bound (2.52); the summed inequality at ; and the expected bound (3.35).
The result. Theorem 4 covers stochastic composite problems whether or not is convex, with one step-size policy. Under Corollary 4's policy and batch sizes it gives a sample complexity for that improves the dependence on over mini-batch proximal stochastic gradient [Ghadimi, Lan & Zhang 2016], and when it recovers the optimal rate for convex stochastic composite optimization. Its proof is a template for later variance-controlled accelerated methods: a weighted Lyapunov argument in which nonconvexity enters only through and noise only through the martingale and variance terms.
Formalizing it. The result has been proved and refereed since 2016. As far as is known, no proof assistant has a formalization of it, and the platform has no accelerated stochastic method with a nonconvex guarantee. A complete development gives machine-checked versions of the mini-batch variance bound for martingale-difference noise, the Lipschitz property of the gradient mapping, the proximal three-point inequality on a convex domain, and the composite accelerated analysis with noise. Each of these can be reused in other stochastic proximal methods.
Copying the deterministic composite proof (Theorem 2) fails in two places. First, the deterministic step bounds through the decrease , but here is computed from , so this decrease measures the stochastic gradient mapping. Passing back to the exact one costs an extra variance term, which is why the constant is 8 rather than 2. Second, the noise appears in two ways. The linear term vanishes only in expectation, and only because is fixed before the batch is drawn. The quadratic terms need the variance of an average of dependent samples, which is only when the samples within a batch are conditionally unbiased given the earlier ones. A pathwise argument cannot remove either term, and an unconditional reading of Assumption 1 does not give the second.
EuclideanSpace ℝ (Fin n) (the published GhadimiLan.RSG.E). Smoothness of and is the platform's ConvexOptAlg.SmoothGD.IsBetaSmooth. , and are given with the identities , , .K with finite values X and ConvexOn ℝ K X; the prox map is a function P with the minimizer hypothesis IsProxMap K X P. A real-valued on all of is excluded: it makes Assumption 2 unsatisfiable and the goal vacuous. So is a free P with no minimizer property.GhadimiLan.RSG.AssumptionA1 along these query points: conditional unbiasedness given a filtration of the earlier calls, and conditional variance bound . This conditional form is what the paper's proof uses, and the i.i.d. setting satisfies it. The oracle is jointly measurable. The variance bound (3.28) is a milestone and is never assumed.Contributions welcome: proofs of any milestone. Lemma 4, (3.28) and the three-point inequality are self-contained and reusable. Also welcome: the measurability of the iterates, and Corollaries 4–5 as follow-up statements.
Reinforcement learning with large or continuous state spaces relies on function approximation: value functions are represented as functions of a -dimensional feature map instead of tables indexed by states. Before 2019, regret guarantees for exploration with function approximation either needed strong assumptions (deterministic dynamics, a generative model) or applied only to tabular problems. Jin, Yang, Wang and Jordan (arXiv:1907.05388, COLT 2020) showed that in a linear MDP, where transitions and rewards are linear in known features, an optimistic version of least-squares value iteration, LSVI-UCB, has regret , with no dependence on the number of states or actions (Theorem 3.1).
Exact linearity is rarely satisfied by features chosen in practice. A guarantee that collapses under a small modelling error would say little about real use, and a naive adaptation of linear-bandit methods can break down entirely when the model is wrong. Theorem 3.2 of the same paper addresses this: if the MDP is only -approximately linear, LSVI-UCB with an episode-dependent bonus still has sublinear regret plus an additive term linear in . This mission formalizes that result. A companion mission formalizes Theorem 3.1.
An episodic MDP has a measurable state space , a finite action set , a horizon , and for each step a transition kernel and a reward . A policy chooses an action at state and step . Its value functions satisfy the Bellman equation
and is the optimal value, with defined by the same recursion.
A feature map with makes the MDP -approximately linear (Assumption B) if for every step there are signed measures on and a vector with
for all , together with the normalization and a bound on the masses of . At this is a linear MDP.
LSVI-UCB (Algorithm 1) plays episodes. In episode , with data from earlier episodes, it computes backwards from
and then acts greedily, . An adversary may choose each initial state . The regret after episodes is
where is the greedy policy of episode . Throughout, and .
There are absolute constants such that for every -approximately linear MDP, every and every run of LSVI-UCB with and , with probability at least ,
The constants are not fixed numerically, so improvements of the constants in the proof do not invalidate the target.
The milestones follow Appendix C: the approximate linearity of (Lemma C.1) and the bound on its weights (Lemma C.2); the trace inequality D.1 and the adversarial-noise bound C.4; the self-normalized concentration bound D.3 (published) and the concentration event of Lemma C.3; the key estimate C.5; approximate optimism C.6; the recursive formula C.7; and the elliptical potential lemma D.2 (published) with the bonus-sum bound (21)–(24).
Theorem 3.2 shows that the regret of LSVI-UCB degrades gracefully under misspecification: the extra cost is of order , linear in because of the bias of linear approximation and negligible when . The paper also converts it into a PAC guarantee with an additive error. It is a reference point for later work on misspecified linear bandits and RL, which asks how far the linear term can be improved.
The result is proved on paper; no machine-checked proof is known. The formalization supplies an episodic MDP on a general measurable state space, LSVI-UCB as a function of the observed data, and its interaction with an adaptive adversary on a filtered probability space. These are shared with the companion mission on Theorem 3.1 and are reusable for other optimistic algorithms with linear function approximation. At the goal specializes to Theorem 3.1 under the same normalization; this is a consistency check, not a dependency.
The central difficulty is that the regression targets depend on the data through , which is computed from all earlier episodes. A martingale concentration bound for a fixed function does not apply. Lemma C.3 needs a bound that holds uniformly over the class of functions LSVI-UCB can produce, which requires a covering-number argument whose size depends on ; that is why the constant must be independent of and is chosen afterwards. Under misspecification a second error appears: the deviations and are not mean-zero and can be adversarial, so they cannot be concentrated away. Lemma C.4 absorbs them into the bonus at the price of the term in . Optimism then holds only up to an error that accumulates over the horizon (Lemma C.6).
Lemmas C.3 and C.5 are formalized as printed. Their proofs use , which Algorithm 1 does not enforce from below; a solver may find that one of them needs an additional argument.
A formalization in which the goal assumes the event , the optimism of Lemma C.6 or the recursion of Lemma C.7, or in which the run does not fix the actions to Algorithm 1's, would be trivial or false; the goal assumes none of these. Contributions are welcome on the linear-algebra lemmas (D.1, C.4, (21)–(24)), on measurability of the LSVI-UCB estimates, and on the covering argument behind Lemma C.3.
Reinforcement learning with large or continuous state spaces is done in practice with function approximation: the agent represents value functions in a low-dimensional parametric family instead of a table indexed by states. For tabular Markov decision processes, regret bounds of order have been known since the work on UCRL and UCBVI, but they scale with the number of states and actions and say nothing when is infinite. Before 2019, provable guarantees for function approximation either needed a simulator, assumed deterministic transitions, or had regret exponential in the horizon.
Jin, Yang, Wang and Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation (arXiv:1907.05388, COLT 2020), identified a model, the linear MDP, in which an optimistic version of least-squares value iteration has regret polynomial in the feature dimension and the horizon and independent of and . The model and the algorithm, LSVI-UCB, became a standard reference point for the theory of RL with function approximation.
Timeline:
An episodic MDP has a measurable state space , a finite action set , a horizon , transition kernels and deterministic rewards for steps . A policy chooses an action at each state and step. Its value functions satisfy the Bellman equation , , , where ; the optimal values , satisfy the same recursion with a maximum over actions.
The MDP is linear (Assumption A) with feature map if and for each step there are signed measures and a vector with
and , .
In each episode an adversary chooses the initial state ; the agent then plays steps, the next state being drawn from . LSVI-UCB (Algorithm 1) computes, backwards over , the Gram matrix of the past features , the ridge-regression weight for the targets , and the optimistic estimate
and then plays greedily with respect to . Its policy in episode is , and the regret is
There are absolute constants such that for every linear MDP, every and every run of LSVI-UCB with and , ,
The milestones follow Appendix B of the paper: linearity of (Proposition 2.3) and the weight bounds (Lemmas B.1, B.2, with Lemma D.1); the covering bound for the value class (Lemma D.6, with the Euclidean-ball covering of Lemma D.5); the uniform self-normalized concentration (Lemma D.4, with Theorem D.3) and the good event (Lemma B.3); the error propagation (Lemma B.4), optimism (Lemma B.5) and the recursion (Lemma B.6); and the bonus-sum bound (17)–(18), with Lemma D.2. Lemma D.2, Theorem D.3 and Lemma D.5 are already on the platform and are referenced.
A companion statement, not a milestone, formalizes Proposition 5.1 (§5): on a finite state space with non-degenerate features, if the Bellman operators of (8) map linear action-value functions to linear ones for every policy, then is linear in .
The theorem shows that exploration with function approximation can be sample-efficient without a simulator: the regret depends on the intrinsic dimension of the features and polynomially on , not on the size of the state space. Its analysis, a uniform concentration bound over a data-dependent class of value functions combined with optimism, is the template for a large later literature: misspecified and low-rank MDPs, kernel and neural function approximation, and reward-free exploration.
The result has a published proof, but no machine-checked one. A formalization supplies the measure-theoretic episodic MDP on a general state space, an interaction protocol with adaptive initial states, the LSVI-UCB algorithm, and a checked chain from self-normalized martingale bounds to the regret theorem. The formal statements also record two points where the printed paper is imprecise: the normalization of the measures (see Formalization scope) and the existential reading of the weights in Lemma B.1.
The regression targets depend on all past data through . The self-normalized bound for vector-valued martingales (Theorem D.3) therefore cannot be applied to them directly: the natural first idea, conditioning on the past and treating as fixed, fails because is not measurable with respect to the past at the time is drawn. The concentration must hold uniformly over a function class, which requires a covering-number bound for a class parametrized by vectors and matrices (Lemma D.6) and a union bound in the right scale.
A second difficulty is formal: the probabilistic protocol mixes an adversary, a learning algorithm reading its own past outputs, and transition kernels on a general measurable space, and the martingale argument (Azuma–Hoeffding over the steps) needs every object to be measurable with respect to the right σ-algebra.
Retailers that carry a limited range of products often know something about a customer before choosing which of those products to display. The customized assortment problem asks which products to carry when the displayed assortment may be tailored to the arriving customer's type. This separates the first-stage capacity decision from the later offer decision. El Housni and Topaloglu study the problem under a mixture of multinomial logit choice models and develop an approximation framework for it in their SSRN paper. This mission isolates their structural guarantee for Augmented Greedy, Theorem 4.2 of the PDF version dated 7 December 2021. The theorem identifies the revenue recovered from customer types whose optimal personalized offers agree with a chosen product subset.
The paper contrasts this setting with ordinary assortment optimization, where every type sees the same products. Its later approximation results use the structural guarantee here as a component. The classical comparison is the cardinality-constrained greedy bound for monotone submodular functions, associated with Nemhauser, Wolsey and Fisher (1978). The paper's Appendix B gives an instance in which the customized revenue function lacks global submodularity, so that classical result does not apply directly. El Housni and Topaloglu, §§4 and App. B.
Let be a finite product set. Product has positive revenue , and products are indexed with . Let be customer types. A type- customer arrives with probability , with , and assigns each product a nonnegative preference weight . The no-purchase option has weight one. Offering an assortment to that customer gives MNL expected revenue
If the retailer initially carries only , it can still choose the best offer to each customer type. Thus . For , write , and abbreviate . The first-stage capacity is ; an optimal solution of CAP maximizes among sets with at most products. These definitions and the standing data assumptions are stated in §2 and §4 of the paper.
For each product , the prefix contains products at least as early in the revenue ordering. Greedy starts at the empty set, repeatedly adds an available product that maximizes the new objective value, and stops at cardinality or when the prefix is exhausted. Augmented Greedy runs Greedy on for each , using , and returns whichever candidate has the greatest value. Both stages may break ties arbitrarily. El Housni and Topaloglu, §4.1.
For type , use the optimal personalized assortment , characterized by Lemma E.1. A type is complete with respect to when ; let collect these types. The threshold choice matters because zero-weight products can be present in other optimal offers without helping a customer. El Housni and Topaloglu, Definition 4.1 and App. E.
For every , , with , and every output of Augmented Greedy on ,
This is the mission goal, the structural performance statement of Theorem 4.2, p. 11. It does not assert a constant-factor approximation to all of CAP: it identifies the contribution from complete customer types.
The milestone list follows the results used with this bound: monotonicity of from Appendix C; the MNL threshold assortment of Lemma E.1; submodularity of on from Lemma 4.3; and the cited Greedy guarantee for a nonnegative monotone submodular objective. The greedy milestone compares its output against every feasible set of cardinality at most .
The theorem says that one algorithmic output captures a fixed fraction of the benchmark supplied by complete types, despite the absence of global submodularity of . It connects the local behavior of truncated type revenues to the full customized assortment objective. The paper uses this result in the development of later algorithms; without it, the standard submodular greedy theorem gives no immediate conclusion for CAP. El Housni and Topaloglu, §§4–5.
The mathematical results are proved in the 2021 paper. The formalization work here is to give machine-checkable statements for the objective, the algorithm with all its legal tie choices, and the four supporting targets, then supply proofs. The MNL revenue formula is already available as a published platform definition; the local CAP and algorithm definitions specify the extra model needed by this theorem. A completed development could also support later CAP missions that use the same threshold and submodularity properties.
The tempting argument applies the classical greedy guarantee directly to , since increases when more products are carried. Appendix B of the paper shows that this fails: even for one customer type, need not be submodular. Restricting the ground set to a revenue prefix and truncating each at that prefix's revenue level changes the submodularity question, but the final guarantee must still concern the untruncated objective. The threshold condition in the definition of is what makes that comparison meaningful. El Housni and Topaloglu, App. B, Lemma 4.3 and Theorem 4.2.
Products and types are Fin n and Fin m; their zero-based Lean indices correspond to the paper's indices plus one. Assortments and type groups are finite sets. The model assumes , , , , and decreasing revenue order. The no-purchase weight is exactly one. CAP and personalized revenue use maxima over nonempty finite powersets, so empty input sets have their intended value rather than an arbitrary real supremum. The theorem keeps the source's optimality assumption on , even though its particular inequality uses less.
The Greedy predicate describes each successive maximizer and the exact stopping rule. Augmented Greedy requires a Greedy output at every prefix and an -maximizing choice among them. Thus the output is constrained by the printed algorithm, and the statement covers every tie-break. The type- assortment is defined from by the Lemma E.1 threshold, rather than supplied as a free set. These choices rule out a size-only output condition, an arbitrarily chosen , a vacuous run predicate, and real supremum defaults. The target includes the corner cases , , and , where its right side is zero. Arrival probabilities summing to one force ; Augmented Greedy has an output only when at least one product exists.
The reusable parts are the MNL threshold characterization, finite-set submodularity and the general Greedy bound. Contributions toward those lemmas, the paper's case analysis for Lemma 4.3, and the final structural theorem are in scope. Runtime claims, the paper's later logarithmic approximation theorems and its computational experiments are outside this mission.
Computing an approximate Nash equilibrium of a two-player game is one of the central questions of algorithmic game theory. For a constant approximation , the algorithm of Lipton, Markakis and Mehta runs in quasi-polynomial time , and for a long time it was unknown whether polynomial time is possible. A. Rubinstein, Settling the Complexity of Computing Approximate Two-Player Nash Equilibria (FOCS 2016, arXiv:1606.04550), proved that, assuming an exponential-time hypothesis for PPAD, quasi-polynomial time is also necessary.
The proof is a chain of reductions. Its middle links produce multiplayer games in which only most players are approximately best-responding (the WeakNash notions of Babichenko, Papadimitriou and Rubinstein, Can Almost Everybody be Almost Happy?, ITCS 2016). Its last link turns a bipartite multiplayer game into a two-player game. Section 8.1 of the paper sits between the two: it shows that the weaker mixed-response notion of WeakNash can be converted into the stronger support-based notion, with a loss of only a square root in the approximation. This mission formalizes that step, Lemma 8.1, together with the intermediate claims of its proof.
Timeline. Daskalakis, Goldberg and Papadimitriou (SIAM J. Comput. 2009, doi:10.1137/070699652) introduced the trimming argument (their Lemma 4.28 and Claim 6) for exact-all-players -approximate equilibria of general games. Babichenko–Papadimitriou–Rubinstein (2016) introduced -WeakNash. Rubinstein (2016) adapted the trimming argument to WeakNash of bipartite polymatrix games, where the constant no longer grows with the number of players.
A finite game has a finite set of players , a finite action set for each player , and utilities on action profiles. A mixed strategy is a probability vector on ; a mixed profile is one mixed strategy per player, drawn independently. For an action , is the expected utility of when plays and the others play , and .
A polymatrix game is one in which each pair of players plays a two-player subgame, each player uses one action in all of its subgames, and its utility is the sum of its subgame payoffs. In a complete bipartite polymatrix game the players form two sides , with , ; every plays a bimatrix subgame against every , and same-side pairs play nothing. Lemma 8.1 assumes the payoffs of -vertices lie in and those of -vertices in , so every utility lies in .
The trimmed profile with parameter : every player that plays -optimally in drops the actions with , whose total mass is , and renormalises, on the kept actions; every other player keeps .
For a complete bipartite polymatrix game with the payoff ranges above, , and an -WeakNash , the trimmed profile with satisfies
The result. Lemma 8.1 is the link that allows the hardness of WeakNash, the notion the PPAD-hardness argument naturally produces, to be transferred to the support-based notion used by the two-player reduction of Section 8.2 (Lemma 8.3, via Althöfer's games). The polynomial loss and the unchanged are what keep the final constant approximation constant. The same trimming technique, with constants that do not depend on the number of players, applies to any polymatrix game with normalised payoffs.
Formalizing it. The result is proved on paper; it is not formalized anywhere. The published platform items DGPNash.WellSupported.* formalize the Daskalakis–Goldberg–Papadimitriou version, which assumes every player is -optimal and has a constant growing with the number of players; this mission produces the WeakNash and polymatrix version and a reusable vocabulary of WeakNash notions (Definitions 2.5–2.9) for the rest of the paper.
The obvious argument applies the trimming of Daskalakis–Goldberg–Papadimitriou to every player, and it fails in two places. First, only a -fraction of players are -optimal; for the others the trimmed mass can equal , so the renormalisation is undefined and those players cannot be trimmed, while their neighbours' payoffs still depend on them. Second, the general bound on how much a payoff moves when the other players' strategies move grows with the number of players, which would make the final constant depend on and ; Lemma 8.1 has no such dependence, and the payoff normalisation , is what must absorb it. The constant of milestone 4 is tight enough that the page's own displayed chain, which ends at , does not reach it directly.
VA ⊕ VB; action sets are finite types S i; subgame payoffs are PA v w (for against ) and PB w v. The general polymatrix payoff (Definition 2.9) sums over ; the bipartite instance sets same-side subgames to zero.agt_games bundle. is DGPNash.NashMap.purePayoff; , and the trim formula are maxPurePayoff, trimMass, trim of DGPNash_WellSupported_Equilibria.The bare existence of some -Well-Supported WeakNash is a consequence of Nash's theorem and does not use ; the goal therefore names the specific trimmed profile computed from .
Contributions welcome: proofs of the milestones; general lemmas expressing of a polymatrix game as a bilinear sum and the multilinearity of expected payoffs, which are reusable for the rest of the paper.
Many problems in statistics, signal processing and machine learning have the form "smooth loss plus simple non-smooth term": a differentiable data-fit term together with a constraint set or a sparsity-inducing penalty such as the norm. When the loss is convex, Nesterov's accelerated gradient (AG) method and its proximal variants are known to be optimal among first-order methods: after iterations the optimality gap is , against for plain proximal gradient (Nesterov 1983, reference [24] of the paper; Beck & Teboulle 2009). When the loss is nonconvex, the classical accelerated schemes come with no convergence guarantee at all, and practitioners must choose between a method that is fast on convex problems and one that is guaranteed to make progress on nonconvex ones.
Ghadimi and Lan (arXiv:1310.3787v1, 2013; Math. Program. 156, 2016) proposed a single AG scheme that does both. This mission formalizes their result for composite problems (§2.2, Theorem 2), where the smooth part is split into a possibly nonconvex piece with Lipschitz constant and a convex piece, and a non-smooth convex term is handled through a proximal step. The theorem shows that one aggressive step-size policy, the one that is optimal in the convex case, still drives a stationarity measure to zero when the smooth part is nonconvex.
Work in with the Euclidean norm. The problem (1.3) is
where:
The prox map (2.37) is
and the gradient mapping (2.38) is . With it reduces to when , and a small certifies approximate stationarity of (1.3). Assumption 2 asks for a constant with for all and ; it holds whenever is proper, closed, convex with bounded domain (Lemma 2).
Algorithm 2 takes step sizes with , for , , , starts from , and for sets
The weights are , (2.6).
Fix and assume, for ,
Let be an optimal solution of (1.3). Then
and, if ,
The goal is stated for general step sizes, so it does not hard-code the constants of a particular policy; Corollary 2 (the policy , , ) is a specialization left for follow-up work.
In the order of the proof: Lemma 1 (unrolling a -weighted recursion) and (2.16); the identity (2.42) linking to ; Lemma 5, the two-sided bound ; the descent bound (2.46) (already proved on the platform); the one-step inequalities (2.47)–(2.51); the summed inequality after (2.51); and the bounds (2.52)–(2.53).
The result. Theorem 2 gives a uniform treatment of convex and nonconvex composite problems. The same step sizes yield the optimal optimality gap when is affine, and a bound on the gradient mapping when is nonconvex. Under Corollary 2's policy that bound gives an iteration count of for , which depends on the Lipschitz constant of the convex part more mildly than projected gradient does. The proof template (a weighted Lyapunov argument in which the nonconvexity appears only through ) recurs in later stochastic and variance-reduced accelerated methods, including the paper's own Theorem 4.
Formalizing it. The result has been proved and refereed since 2016. As far as is known it has not been formalized in any proof assistant, and the platform holds no accelerated method with a nonconvex guarantee. A complete development would give a machine-checked proximal three-point inequality for convex functions on a convex domain, a checked composite AG analysis, and a checked version of Lemma 5. These are reusable pieces for any accelerated proximal method.
The obvious route is to copy the convex analysis of accelerated methods. It breaks at the convexity step: the bound needs convexity of , which is now available only up to -quadratic errors. Those errors involve and , which do not telescope and are not controlled by the usual potential; without some a priori bound on the iterates they can grow with . A formal proof also has to track the extended-valued carefully, since its convexity is used only at points of its domain, and the first iteration, where is not a prox output.
EuclideanSpace ℝ (Fin n). Smoothness of and is the platform's ConvexOptAlg.SmoothGD.IsBetaSmooth (differentiable with an explicit gradient map, Lipschitz gradient, nonnegative constant). and are written as and .K and its finite values X : E n → ℝ on K, with ConvexOn ℝ K X. Points outside K never enter: is compared only on K, is optimal over K, and (2.48)–(2.51) quantify over . A real-valued on all of is ruled out, because Assumption 2 is then unsatisfiable ( as ) and the goal would hold vacuously.P x y c with the hypothesis IsProxMap K X P: for every , P x y c ∈ K and it minimizes the prox objective over K. Without this minimizer hypothesis the three-point inequalities and the goal are false, so it cannot be dropped.Finset.inf' over . Conditions (2.9)–(2.10) are imposed for , and is written .Contributions welcome: proofs of any milestone. The three-point inequality (2.48)–(2.49) and Lemma 5 are self-contained and reusable. Also welcome: a proof of Lemma 2 (bounded domain implies Assumption 2), and Corollary 2 as a follow-up statement.
Many problems in machine learning and signal processing minimize a smooth loss plus a simple non-smooth regularizer: -regularized least squares, group-sparse regression, and constrained problems written with an indicator function. The standard algorithm for this composite form is the proximal-gradient method, a gradient step on the smooth part followed by a proximal step on the regularizer. Its classical linear convergence guarantee needs the smooth part to be strongly convex, a hypothesis that fails for -regularized least squares with fewer observations than variables and for most problems of interest without explicit regularization.
For smooth problems the Polyak–Łojasiewicz (PL) inequality gives a linear rate for gradient descent without convexity (Polyak 1963). Karimi, Nutini and Schmidt (arXiv:1608.04636, ECML PKDD 2016) propose a generalization to the composite setting, the proximal-PL inequality, under which the proximal-gradient method converges linearly with a one-paragraph proof. They show that it contains the PL case, the strongly convex case, and convex objectives with quadratic growth, and that it is equivalent to the Kurdyka–Łojasiewicz inequality (Bolte, Nguyen, Peypouquet, Suter 2017) and to the proximal error bound used earlier by Luo, Tseng and Drusvyatskiy–Lewis.
Timeline:
Let and consider problem (11),
The function is differentiable with an -Lipschitz gradient, with . The function is convex. has a minimizer , and .
For a base point and a parameter , the proximal model is
and the paper's measure of non-stationarity is
satisfies the proximal-PL inequality with modulus if
When is constant, and (12) is the PL inequality.
The proximal-gradient method with step size starts at an arbitrary and sets
The proximal residual function of Appendix E is .
Under the hypotheses above,
Theorem 5 gives a global linear rate for the proximal-gradient method under a hypothesis that does not require strong convexity, or convexity of . Through the classes of Section 4.1 it covers -regularized least squares, the composite strongly convex case, and convex composite problems with quadratic growth. The quantity also drives the analysis of proximal coordinate descent (Theorem 6, mission VI of this series), and Lemma 1 is what lets the sufficient conditions of Appendix F, which hold with for , be used in (12).
The results are proved in the paper; none of them has a machine-checked proof that this mission knows of. The work here is to formalize the known proofs, including the properties of and that the paper uses without stating: the minimum in (13) exists, and the value is finite.
The proof of Theorem 5 is short; the difficulty sits in the objects. is defined through a minimum over of a function involving a non-smooth convex , so every step that replaces the minimum by its value at a particular point needs the minimum to be finite and attained. The paper never states these facts, and they fail for an arbitrary : for and the model is unbounded below and the minimum in (13) does not exist. The monotonicity of in its second argument (Lemma 1) rests on the convexity inequality of , and Appendix F item 4 relies on the projection onto the solution set, whose existence depends on that set being closed, convex and non-empty.
EuclideanSpace ℝ (Fin d), is Mathlib's gradient f, and the Lipschitz hypothesis is written literally, ‖gradient f x - gradient f y‖ ≤ L * ‖x - y‖, with 0 < L.xstar with F xstar ≤ F y for all y; is f xstar + g xstar, never a free real.ConvexOn ℝ Set.univ g). Indicator functions of convex sets, which the paper lists among its examples, take the value and are outside this formalization; the formulas (13)–(15) subtract values of , which is undefined at .ShiOptRates.PolyakLojasiewicz (the paper's (3) multiplied by 2), and (2) is the published ShiOptRates.QuadUpper.Quadratic growth is stated with the distance to the solution set, , which equals for the projection the paper uses. Appendix F item 3 (Hoffman's bound with an unspecified constant ) and the equivalences of Appendix G are not included.
Contributions of every kind are welcome: proofs of the milestones, of the companion lemmas, and reusable facts about (finiteness, attainment, continuity in ) that other proximal-method missions can import.
Accelerated gradient (AG) methods go back to Nesterov (1983), who showed that a first-order method with a momentum-like extrapolation reaches an -optimal value of a smooth convex function in iterations, against for gradient descent, and that this rate is optimal among first-order methods. Many objectives met in practice (training losses, nonconvex penalties, problems with unknown convexity) are smooth but not convex. For those, gradient descent is known to drive the gradient norm to zero, with , while the classical AG method has no convergence guarantee at all.
Saeed Ghadimi and Guanghui Lan (arXiv:1310.3787v1, 2013; Mathematical Programming 156, 2016) modified the AG method with a third step size and proved that one algorithm handles both cases: on a smooth nonconvex problem it has the gradient-descent rate for , and when the problem turns out to be convex it keeps Nesterov's optimal rate for the optimality gap. This mission formalizes that result, Theorem 1 of the paper, and its proof path in §2.1.
Let be differentiable with Lipschitz gradient: there is with
and bounded from below, with (problem (1.1)). need not be convex.
Algorithm 1 (AG). The inputs are a starting point and step sizes , , with , for , and . Set and, for ,
One gradient is evaluated per iteration, at the middle point ; takes a long step and the aggregated point a short step . With the method reduces to gradient descent, with to a variant of Nesterov's method.
The weights are , (), and for a horizon and
Fix .
a) If for , then
b) If is convex with a minimizer , and for one has and , then
The theorem leaves the step-size policy open: any sequences meeting the conditions are covered, and the rates of Corollary 1 ( in part a, for the gap in part b) follow by substitution.
The milestones follow the proof in §2.1: the quadratic bound (2.1); Lemma 1, which unrolls the recursion ; the nonconvex chain (2.13), (2.15), the identity for , (2.16), (2.17), (2.18) and (2.19); and the convex chain (2.20)–(2.25).
The result. Theorem 1 is the first convergence guarantee for an accelerated gradient method on nonconvex smooth problems. It shows that acceleration costs nothing in the nonconvex case (the same rate for the squared gradient norm as gradient descent) while keeping the optimal gap when the function is convex, so a user need not know in advance which case holds. The same analysis is the template for the composite and stochastic results of the paper (Theorems 2–4) and for the later literature on accelerated methods for nonconvex optimization.
Formalizing it. The theorem is proved on paper; it is not known to have a machine-checked proof. The mission produces a Lean definition of the AG run with its three step sizes, a formal Lemma 1 (a reusable tool for any Nesterov-type analysis), and the two chains of estimates with all constants explicit. These pieces are reused by the composite and stochastic missions of the same paper.
The standard analysis of Nesterov's method is an estimate-sequence or potential argument that relies on convexity at every step: it bounds below by a linearization. Without convexity that lower bound fails, and the potential need not decrease. Part a) instead tracks the decrease of along the sequence, where gradients are evaluated at a different point ; the error this creates is governed by the gap , which accumulates all past gradients with weights . Controlling that accumulated term, and showing it is absorbed by the condition with depending on the horizon , is the delicate step. Part b) needs the monotonicity (2.10) to turn a weighted telescoping sum into a single initial-distance term.
EuclideanSpace ℝ (Fin n). The gradient is an explicit map g, tied to by the published predicate ConvexOptAlg.SmoothGD.IsBetaSmooth Ψ g LΨ (differentiable with gradient , and (1.2)); as in (1.2). The quadratic bound (2.1) is the published, proved ConvexOptAlg.SmoothGD.lemma_3_4.agRun, with xSeq, xagSeq, xmdSeq), computed by (2.2)–(2.4) from ; indices are 1-based as in the paper. , so . is C LΨ α β lam N k and depends on .BddBelow (Set.range Ψ) and is ⨅ x, Ψ x. The minimum over is Finset.inf' over Finset.Icc 1 N with . Convexity is ConvexOn ℝ Set.univ Ψ; is any global minimizer.Welcome contributions: proofs of Lemma 1 and of the algebraic milestones (the identity before (2.16), (2.16), (2.17), (2.22), (2.25)), which are independent of ; then the descent chains; then Theorem 1.
Social networks exhibit triadic closure: two people with many friends in common tend to be friends themselves. Fox, Roughgarden, Seshadhri, Wei and Wein (arXiv:1804.07431, SIAM J. Comput. 2020, doi:10.1137/18m1210459) turn this empirical regularity into a distribution-free graph class and ask which algorithmic problems that are hard on worst-case graphs become tractable on it. Their test case is the enumeration of maximal cliques, a standard primitive of community detection. On a general -vertex graph the number of maximal cliques can be (Moon and Moser, 1965), so no enumeration algorithm can be polynomial. The question is how far triadic closure alone pushes this count down.
Timeline:
All graphs are finite, simple and undirected; is the set of neighbours of a vertex , and for , is the subgraph induced by .
For a positive integer , is -closed if any two distinct vertices with are adjacent. A 1-closed graph is a disjoint union of cliques, and every graph on vertices is -closed, so interpolates between the two. Being -closed passes to induced subgraphs, with common neighbours counted inside the subgraph.
A clique is a set of pairwise adjacent vertices; it is maximal if no further vertex can be added. Write for the number of maximal cliques of , and
The proof uses four further objects, computed in the current induced subgraph: the maximum degree ; for a non-empty set of vertices, ; the set of vertices at distance exactly from ; and the function
For all positive integers and every -closed graph on vertices,
For fixed the exponent is , strictly below , which is what the improvement over Theorem 2.1 consists of. The constant is the one printed in the theorem.
The milestones follow the proof on pp. 9–11:
Together with Theorem 2.1, Theorem 3.1 gives Theorem 1.4 of the paper: a -closed graph on vertices has at most maximal cliques. For constant the count is polynomial with exponent below , so all maximal cliques can be listed in polynomial time, and the problem is fixed-parameter tractable in . Theorem 4.1 shows the exponent cannot drop below for , so the bound is polynomially tight for .
The result is proved in the paper; it has not been formalized. This mission produces a machine-checked proof of Theorem 3.1 together with the steps of the paper's argument. The printed argument has gaps that a formal proof must close: the base of the exponential factor changes from to in the middle of the proof, Claim 3.3 is applied with that may exceed , the induction meets the empty graph (one maximal clique, while ), and the recursion deletes vertices where the recurrence writes . A proof that also closes the stronger base- bound, which the arithmetic suggests, would be a welcome addition.
The count of maximal cliques through a vertex reduces to , which is -closed, so a naive induction on gives . When the maximum degree is large this is no better than . The high-degree case needs a separate count of the cliques that meet without containing , grouped by their trace on ; bounding the sum over these traces requires the convexity of in its first argument and the constraint coming from -closedness. The resulting recurrence then has to be solved with explicit real exponents of the form , for all simultaneously, with the induction on and arranged so that the empty graph never enters the inductive hypothesis.
SimpleGraph (Fin n). The general statements are over a finite vertex type with decidable equality.Set.ncard and reads "at least " as c ≤ ncard, not c < ncard. The relative notion IsCClosedOn c G W counts common neighbours inside and is equivalent to -closedness of G.induce W.Finset that is maximal under inclusion among cliques contained in ; the empty graph has exactly one maximal clique. Neither all cliques nor maximal cliques of a different graph are counted.Everything is built from Mathlib's SimpleGraph, commonNeighbors, IsClique, Maximal and Real.rpow. The definitions of -closedness and of the maximal-clique count come from the reviewed shared module CClosedGraphs.Peeling.Setting. Contributions welcome: proofs of the milestones, a proof of the goal by a different route, and the base- strengthening.
Stochastic optimization methods often see only noisy gradients. For a nonconvex objective, a useful guarantee is that an output point has a small gradient: this is a first-order stationarity certificate, even when there is no claim that the point is globally optimal. A guarantee on the expected squared gradient leaves open how often one particular run succeeds. The two-phase randomized stochastic gradient method of Ghadimi and Lan (2013) addresses that question by generating several candidates and using further oracle calls to select one. The paper gives an explicit bound on the probability of failure and on the number of oracle calls needed for a prescribed accuracy and confidence.
The work sits within stochastic approximation, where the objective may be a population expectation or another function accessible through noisy observations. The 2013 paper develops first- and zeroth-order methods for smooth nonconvex problems. This mission concerns its two-phase first-order result, Theorem 2.4, rather than the Gaussian smoothing results in its later section. The source for every index here is the arXiv v1 preprint; the printed page and PDF page coincide.
The objective is a differentiable function bounded below, with true optimal value . Its gradient map is -Lipschitz: for all . The mission uses . No convexity is assumed.
A stochastic first-order oracle returns a vector when called at the current iterate . Assumption A1 says that the oracle is unbiased at that iterate and has squared error of expectation at most . The noise may depend on earlier calls. In the formal model, the mean is conditional on the past, and the oracle and squared-error random variables are integrable. This makes explicit the probabilistic assumptions used when the paper takes expectations. The model takes because the paper's displayed stepsize and post-optimization sample size otherwise degenerate under Lean's total division convention.
A randomized stochastic gradient run starts at and uses . It chooses an output index with the probability mass function in equation (2.3), independently of that run's oracle noise, and outputs . For a parameter , the constant stepsize in equation (2.13) is . The paper writes and
The two-phase method makes independent RSG runs, yielding . For each candidate it averages fresh oracle outputs into an estimated gradient . It selects a candidate whose estimated-gradient norm is minimal. The post-optimization samples for different candidates may be recycled; the paper explicitly permits this. The candidate itself is known when its post-optimization samples are taken, so the conditional oracle assumption is stated relative to a filtration that contains it at time zero.
The first target is the one-run mean bound of Corollary 2.2, , followed by the one-run tail bound (2.19). Lemma 2.3(a) controls the squared norm of a sum of vector martingale differences. Equation (2.28) relates a selected candidate's true gradient to the best candidate and the estimation errors. Equation (2.29) factors the probability of simultaneous failure across independent runs and bounds it, while (2.30) bounds the other source of failure: every optimization run performing poorly, and at least one estimated gradient being inaccurate.
For arbitrary positive , Theorem 2.4(a) states the stronger quantitative tail bound
The goal, Theorem 2.4(b), specializes those parameters to an accuracy and failure probability . It sets
An -solution is a point satisfying . With those parameter values, the method computes such a point using at most stochastic first-order oracle calls. The formulas and constants above are those of equations (2.24)–(2.27) of the preprint.
The result turns a mean stationarity bound into a confidence guarantee for one returned point, with an explicit accounting of both candidate generation and candidate assessment. It identifies how the number of independent runs, iterations per run, and gradient estimates scale with the requested accuracy and failure probability. Without the post-optimization phase, the paper's direct Markov estimate (2.19) gives a less favorable dependence on the failure probability for a single run.
The mathematical theorem is proved in the 2013 paper; the Lean declarations in this proposal are statements awaiting machine-checked proofs. A completed formalization would give reusable definitions for a dependent-noise gradient oracle, a random-output stochastic-gradient run, and a post-optimization selection procedure. The vector martingale estimate and finite-candidate inequality could also serve later stochastic-optimization developments. Contributions to the probability and measurability infrastructure, as well as the final rate proof, are within scope.
Selecting the candidate with the smallest estimated gradient need not select the one with the smallest true gradient. The estimates are random and are evaluated at candidates that are themselves random outputs of earlier oracle runs. A bound for a fixed point does not address this dependence. The argument needs a conditional oracle contract at each candidate and a separate guarantee that the optimization runs supply a sufficiently good candidate. The paper's intermediate display (2.31) applies a fixed-candidate tail estimate to the selected candidate even though the selection examines the same estimates; that step is not justified by the stated assumptions. The final bound can be phrased without treating (2.31) as a separate target.
The space is EuclideanSpace ℝ (Fin n). Iterations and oracle samples retain the paper's one-based indexing; candidate runs use Fin S, which reindexes the paper's . The objective's true infimum is carried by IsGLB (Set.range f) fstar, so cannot be weakened by substituting an arbitrary lower bound. Each candidate is generated by the RSG recursion and the mass function (2.3); the one-run performance bound is a theorem, not a hypothesis of the two-phase model. Independent candidate outputs are required for (2.29). The selected candidate may be any minimizer of the estimated-gradient norm, with any tie rule; no measurability of the selection is assumed.
All expectations are Bochner integrals, with integrability included in the oracle assumptions and in the one-run conclusion. Probabilities are ℝ≥0∞ values. The noise carrier is generalized from the paper's Borel subsets of Euclidean space to a measurable type. The general vector martingale lemma omits the paper's Polish-space and trivial-time-zero conditions; neither is needed for its squared-norm bound, and the latter would conflict with a candidate known at time zero. Its non-strict tail statement is restricted to a positive sum of variance bounds, because the printed version is false when every bound is zero. The goal reads the logarithm in (2.24) as base two, matching the paper's final comparison. Positive and avoid zero steps and an empty post-optimization average.
The formal goal states the probability guarantee. The oracle-call bound follows directly from the algorithm's two loops and is recorded in the theorem's prose rather than in a separate operational semantics for calls. A complete proof may use Mathlib's conditional expectations, independent random variables, finite sums, and real logarithm and ceiling libraries. No assumption may simply postulate the one-run gradient bound or the final success probability.
Many optimization problems in simulation-based design, reinforcement learning and machine learning can be evaluated but not differentiated. Their objective is an expectation that can only be sampled through noisy function values . Gradients may be unavailable because the model is a black box, a simulator, or a legacy code. Methods for this setting are called zeroth-order or derivative-free stochastic methods. The objective is often nonconvex, so the realistic target is an approximately stationary point, , not a global minimizer.
Ghadimi and Lan (arXiv:1309.5549; SIAM J. Optim. 23(4), 2013) gave the first complexity bounds for stochastic zeroth-order methods on nonconvex problems. Their randomized stochastic gradient free (RSGF) method combines two ingredients. The first is the Gaussian smoothing and random finite-difference estimator of Nesterov and Spokoiny (Found. Comput. Math. 17, 2017; preprint 2011). The second is a randomized stopping rule that outputs an iterate chosen at random along the trajectory. The resulting bound has become the standard reference point for derivative-free nonconvex stochastic optimization.
Timeline:
Let be Euclidean space and let be a random vector with distribution on a measurable space . The problem is
The sample functions lie in almost surely: they are differentiable, and their gradients are -Lipschitz. Two assumptions describe the noise. Assumption A1 concerns the first-order oracle : it is unbiased, , and has variance at most . Assumption A3 says the zeroth-order oracle is unbiased, .
For a smoothing parameter and an -dimensional standard Gaussian vector , the Gaussian smoothing of is (3.3). The RSGF method starts from and uses stepsizes . At step it draws a fresh sample and a fresh Gaussian direction , forms the zeroth-order estimator
and sets (3.13). The output is , where the random iteration count has the probability mass function
In the Lean development, is objective P F, is szoGrad (the published RandomGradFree.Shared.oracle applied to ), and is the published RandomGradFree.Shared.smoothing. The smoothing parameter is μs, because μ names the probability measure.
Let for , with , and let . Then
The stepsizes are left free, so every stepsize policy specializes the goal.
The milestones follow the paper's proof.
The theorem shows that function values alone suffice to find approximately stationary points of nonconvex stochastic programs. The price is a factor of the dimension : with constant stepsizes the RSGF method needs iterations, against for the first-order RSG method. The randomized output rule and the analysis through are reused in later zeroth-order methods, including two-phase variants, mirror-descent variants and variance-reduced schemes.
The result is proved in the paper. It is not formalized anywhere known to this mission. The platform already holds parts of the Gaussian-smoothing theory from the Nesterov–Spokoiny series, but only for convex problems with exact function values. This mission adds:
The first idea is to treat the RSGF method as the first-order RSG method run on with the unbiased estimator , and to quote the RSG bound. This fails, because the variance has no uniform bound: by (3.7) it grows with at the random iterate. The analysis has to carry that term along and absorb it into the left side, which is where the weights come from. It must also move between and through (3.6) at a cost polynomial in .
On the formal side, three obstacles stand out.
EuclideanSpace ℝ (Fin n). The constants , , use the same natural number . The Gaussian is Mathlib's stdGaussian.IsGLB), with bounded below. The paper's (3.10) is read as an infimum, since the minimum need not be attained.The following are explicit additions; the paper leaves them implicit.
Every conclusion about an expectation also asserts the integrability of its integrand. A non-integrable function has Lean integral , so a bound without this conjunct could hold for the wrong reason.
The goal is stated about the objects of the method only: , , , the run (3.12)–(3.13), and the constants. It does not mention , or the filtration, so it cannot be discharged by choosing an auxiliary object.
A complete development needs:
The Gaussian-smoothing lemmas (3.6), (3.7) and (3.9) are reusable by any zeroth-order mission. Contributions of proofs of individual milestones are welcome, as are alternative proofs of (3.7) without Nesterov's bound.
Mobile devices run applications whose computational demand often exceeds what a battery-powered processor can serve with acceptable delay. Computation offloading sends part of the work elsewhere: to a cloudlet, a small cluster of servers one wireless hop away, or to a distant cloud reached through the wide-area network. When many users share one cloudlet, each user's response time depends on how much the others offload, and selfish users interact strategically. Cardellini, De Nitto Personé, Di Valerio, Facchinei, Grassi, Lo Presti and Piccialli (Math. Program., 2016) model this interaction as a generalized Nash equilibrium problem (GNEP): every user minimises its own expected cost, and all users share a coupling constraint that caps the cloudlet's utilisation.
The paper computes equilibria through a variational inequality (VI) reformulation and, for distributed computation, through an extended game with a price player. The convergence of the methods it relies on (proximal-point and best-response schemes for monotone VIs, see Facchinei and Pang, 2003) requires the VI map to be monotone. This mission formalizes the paper's Theorem 1, which gives an explicit, checkable condition on the model's parameters under which that map is monotone.
There are users . Each user splits its task stream over three tiers (own device, cloudlet, cloud) and chooses fractions ; a strategy profile is . The data are positive rates combined into (the traffic intensities a user generates on its device, the wireless link, the cloud path and the cloudlet), power parameters , the number of cloudlet servers, the offloadable fraction and the utilisation cap .
The cloudlet load is and . User 's private feasible set consists of the with , and the power budget . The shared constraint is , and the joint feasible set is . User minimises
Assumption A requires and all to lie in .
The VI map stacks each user's gradient in its own variables:
is monotone on if for all . Finally .
Under Assumption A, if
then is monotone on . The condition involves only the data of the game, so the goal is the paper's statement with no constant changed.
The milestones follow the paper's argument in order.
Theorem 1 is the hypothesis under which the rest of the paper operates. The extended game of §5.2 inherits the monotonicity properties of (p. 14), and the distributed solution methods of §6 are designed for that monotone setting. Condition (18) translates monotonicity into a statement about the system: the largest per-user cloudlet traffic intensity must stay below a threshold that grows with the number of servers and shrinks with , and . Remark 1 (p. 14) stresses that (18) is only sufficient.
The result is proved in the paper; this mission produces a machine-checked proof. On the way it yields statements reusable outside this model: the Jacobian criterion for monotonicity of a differentiable map on a convex set, and the spectrum of the symmetric rank-two matrix . None of these statements is on the platform; the Schur product theorem, which the proof also uses, is referenced as a published platform theorem.
The Jacobian is not symmetric: carries the row user's own term , so in general, and the eigenvalues of say nothing directly about its quadratic form. The quadratic form must be controlled uniformly over the whole feasible set , whose shape (simplices cut by the cap , the power budgets and the shared constraint) enters the final bound, and the condition must come out in the paper's exact constants. In Lean, the main costs are the coordinatewise Fréchet derivative of on , the characteristic polynomial of a rank-two matrix of arbitrary size, and the passage from a characteristic polynomial to positive semidefiniteness.
Users are Fin N (0-based); tiers are a three-element type Tier; a profile is Fin N → Tier → ℝ. The inner product on is written out as , and the norm on in (21)–(23) is the Euclidean norm written as , because Mathlib's norm on function types is the sup norm. is defined by the closed form of p. 11, not as a derivative, so milestone 2 has content. is the real supremum of the , which is the maximum for .
Standing hypotheses carried by every statement: Assumption A, and . Disclosed choices relative to the page:
The formulas for , , and divide by and , and Lean sets . Every statement is therefore restricted to or to a region where these denominators are nonzero; monotonicity on the larger set , where can vanish, is a different and false-by-junk claim and is not posed. is nonempty for admissible data (e.g. all users computing locally), so the goal is not vacuous.
Contributions welcome: proofs of any milestone, especially the generic ones (1 and 6), which belong in a general library.
Twin-width was introduced by Bonnet, Kim, Thomassé and Watrigant (J. ACM 69(1), Article 3, 2021) as a graph parameter under which first-order model checking is fixed-parameter tractable when a contraction sequence is given. Its interest lies in the classes it covers at once: planar and, more generally, -minor-free graphs, bounded-degree grids, unit ball graphs of bounded clique number, and the classes of bounded rank-width or clique-width. These are the classical dense-graph width measures, for which FO (indeed MSO) model checking was already known to be tractable through Courcelle–Makowsky–Rotics.
This mission formalizes the link to the dense width measures, stated in the paper through boolean-width (Bui-Xuan, Telle and Vatshelle, Theor. Comput. Sci. 412(39), 2011). It is known that (Vatshelle's PhD thesis, Chapter 4), so a bound on twin-width in terms of boolean-width shows that bounded twin-width captures bounded rank-width, clique-width, module-width and boolean-width simultaneously.
Let be a finite simple graph on a vertex set .
Two vertex sets are homogeneous if either all pairs are edges or none is. For a partition of , a part has red degree equal to the number of other parts that are not homogeneous to ; is a -partition if every part has red degree at most . The graph has twin-width at most , written , if there are partitions of with the partition into singletons, having at most one part, each obtained from by merging two parts, and every a -partition. This is the paper's partition form (p. 3:32) of its definition through trigraphs and red edges (pp. 3:11–3:12).
A decomposition tree of is a rooted binary tree , every internal node having exactly two children, whose leaves are in one-to-one correspondence with . Each edge of lies above exactly one rooted subtree and induces a cut of : is the set of leaf labels of that subtree and . For disjoint write
the number of different neighbourhoods in of subsets of , the empty subset included. The boolean-width of the cut is , the boolean-width of is its maximum over the edges of , and is the minimum over all decomposition trees. In Lean, nbhdCount G A B is , and BoolWidthLE G N states that some decomposition tree has on every edge, so is BoolWidthLE G (2^k).
Every graph with boolean-width has twin-width at most . With , the integer neighbourhood count,
The theorem places the classes of bounded boolean-width, and therefore of bounded clique-width and rank-width, inside the classes of bounded twin-width, with a single-exponential bound. Combined with the paper's model-checking algorithm, it recovers tractability of FO model checking on these classes once a contraction sequence is computed, and it situates twin-width as a common generalization of the dense width measures and of sparse classes such as -minor-free graphs.
No machine-checked version of twin-width or boolean-width is known to exist; neither notion is in Mathlib. The mission produces Lean definitions of twin-width in partition form, of decomposition trees and of the neighbourhood count behind boolean-width, together with the four combinatorial steps the paper's proof states explicitly. The definitions are shared, in identical form, with the other missions of this series on the same paper.
The first three milestones are elementary: a counting bound on contraction sequences, a walk down a binary tree, and a pigeonhole argument. The fourth is a direct count of non-homogeneous parts.
The difficulty is the iteration. After the first contraction the leaves of the updated tree are contracted vertices, so "the same neighbourhood in " must be read as homogeneity to all of for a set of vertices, and the boolean-width bound of the cuts must be re-established for sets rather than single vertices. The paper asserts the invariant that the contractions never create a red component of more than vertices without proving it. A complete proof of the goal therefore has to supply an invariant, carried through all contractions, that keeps every part's red degree below . The naive repetition of the first step does not by itself control red edges between previously contracted parts.
Twin-width is the predicate TwinWidthLE G d, never a numerical infimum, so a junk value of an empty or unbounded infimum cannot make the goal trivial. A contraction sequence must merge exactly two parts at each step and start from singletons; it cannot jump to one part. Homogeneity counts all pairs between two parts, in both of its alternatives. Boolean-width is bounded on every edge of the decomposition tree, not only at the root, and the count runs over neighbourhoods of all subsets of , not only of single vertices. The bound depends only on , not on the graph.
Boolean-width is kept as the integer count ; since means that the least admissible count is , the Lean goal for this is exactly the printed theorem. Subtractions are in and exact where used. Graphs live on a Fintype vertex type with decidable equality and decidable adjacency. A graph on the empty vertex set has no decomposition tree; the goal is silent about it, and it has twin-width . No hypothesis is added to any statement relative to the page except in milestone 2, which the page has implicitly () and without which the conclusion is impossible.
The definitions needed are the setting module TwinWidthI.BoolWidth.Setting: merge steps, homogeneity, -partitions, twin-width, decomposition trees (DTree), the count and BoolWidthLE. Proofs of the milestones, a proof of the goal, and lemmas towards the iteration invariant are welcome.
The Yukawa potential (or screened Coulomb potential)
was introduced by Hideki Yukawa in 1935 to model the short-range nuclear force as the exchange of a massive particle, later identified with the pion. The same profile reappears as the Debye–Hückel screened interaction in plasmas and electrolytes, as the static Green's function of the massive Klein–Gordon (screened Poisson) operator, and as the Newtonian correction in massive-graviton models. The mathematical facts behind these uses are classical, short, and stated in every textbook treatment — which makes them a natural, self-contained target for formalization: each one is an explicit identity of real analysis in three dimensions.
Timeline. Heisenberg (1932–33) proposed a short-range exchange interaction between nucleons; Fermi (1934) introduced exchange of light particles in beta decay; Yukawa (1935, Proc. Phys.-Math. Soc. Japan 17, 48) combined the two ideas, derived the potential above, and predicted a mediating particle of mass about 200 electron masses; the pion was observed in 1947.
Throughout, is the coupling (amplitude) constant, a scaling constant, the mass of the exchanged particle and the radial distance; is the range. The potential is the function
Points of space are with Euclidean norm , and the potential of a point source at the origin is . The Laplacian is the usual sum of unmixed second partial derivatives on . For a uniform, infinitesimally thin spherical shell of radius with total scaling constant , the potential felt by a point of scaling constant located at is
the average over the unit sphere (uniform surface measure ) of the pair interaction.
For and every ,
This is the identity the article's sections Fourier transform and Feynman amplitude rest on: the momentum-space Yukawa potential is the massive propagator times .
The results. The Fourier identity is what makes the Yukawa potential the non-relativistic limit of single-meson exchange; milestone 3 identifies it as the Green's function of the screened Poisson operator ; milestones 5–7 give the Born-approximation scattering amplitude and the closed-form total cross section quoted in quantum mechanics textbooks (e.g. Griffiths); milestones 8–9 are the Yukawa analogue of Newton's shell theorem, whose failure to reduce to a point source of the same strength is the reason massive-graviton models violate the weak equivalence principle.
Formalizing them. All statements are classical and proved on paper. The mission produces machine-checked versions together with reusable infrastructure: three-dimensional Fourier integrals of radial functions, Laplacians of radial functions, spherical averages with respect to the surface measure, and conditionally convergent oscillatory integrals.
The individual computations are short on paper but each crosses a gap in the library. The goal requires reducing a three-dimensional Lebesgue integral of a radial function to a one-dimensional integral (polar coordinates in ), then evaluating . The inverse transform is not absolutely convergent — is not integrable on — so the naive Lebesgue statement is false (it would assign the value ); only the ball-truncated limit is meaningful, and its evaluation needs the improper integral . The shell theorem needs the surface measure on and the Archimedes-type change of variables .
All quantities are real numbers; space is EuclideanSpace ℝ (Fin 3) with Lebesgue measure. The potential is a single definition YukawaPotential.yukawaPotential g α m r; at Lean's division convention gives the junk value , so every statement either restricts to / or integrates (where a single point is null). The physical conventions , (and where the article divides by ) are explicit hypotheses. The Fourier transform uses the convention , ; the inverse is stated as a limit over balls. The shell potential averages over the unit sphere with Mathlib's Measure.toSphere (uniform surface measure); since it is an average, its normalisation is irrelevant. The Laplacian is Mathlib's Laplacian.laplacian on inner-product spaces. Physical constants in milestones 5 and 7 are arbitrary reals: the identities hold without sign assumptions on them.
Out of scope: the historical mass estimate of the pion, the heuristic wave-equation derivation of the photon/pion dispersion relations, the perturbative asymptotic expansions of Schrödinger eigenvalues and Regge trajectories (stated in the source only up to unspecified and "" terms), and the limits of the shell formulas.
Contributions welcome: polar-coordinate integration for radial functions on , spherical-average lemmas, and the improper integrals above as standalone lemmas.
In the usual textbook presentation, quantum theory starts from postulates that have no obvious operational meaning: states are density operators on a complex Hilbert space, measurements are positive operators, and probabilities are given by the trace formula . In Quantum Theory From Five Reasonable Axioms (Hardy 2001), Lucien Hardy asks whether this structure can instead be derived from simple statements about preparations, transformations and measurements, in the same way that classical probability theory can be set up by pure thought. He proposes five axioms (probabilities, simplicity, subspaces, composite systems, continuity) and argues that they single out finite- and countably-infinite-dimensional quantum theory. Dropping a single word, "continuous" in Axiom 5, leaves classical probability theory instead.
The paper is one of the starting points of the operational or generalized probabilistic theory (GPT) approach to the foundations of quantum mechanics. It was followed by reconstructions that replace the simplicity axiom, e.g. Dakić–Brukner 2009, Masanes–Müller 2011 and Chiribella–D'Ariano–Perinotti 2011.
A system is described by two integers. The dimension is the maximum number of states that can be distinguished in a single-shot measurement. The number of degrees of freedom is the minimum number of probability measurements needed to determine the state. The state is the vector of the probabilities of fiducial measurements. States are not assumed normalized: the null state (no system present) is allowed. The set of allowed states is convex, and its pure states are its extremal points other than .
The five axioms are:
A probability theory can be summarized by its signature , defined through
Classical probability theory has and . Complex quantum theory has and . Real and quaternionic quantum theory have and .
Section 8.1 shows that Axiom 3 forces , and Axiom 4 forces . The goal theorem is the purely arithmetic consequence (Eq. (57)):
The milestones follow the paper's own steps, in the paper's numbering:
The goal is the step at which the two structural axioms (subspaces and composites) cut the space of possible theories down to a single integer parameter . Combined with Section 8.5, which rules out by continuity, and with the simplicity axiom, it gives . Everything after that in the paper (the Bloch sphere, general , the trace formula, complete positivity) is carried out inside the case. The milestones on signatures make precise in which sense real and quaternionic quantum theory are excluded: their degree-of-freedom counts are not multiplicative under composition.
The paper's argument is informal physics. This mission isolates the mathematically precise statements that the argument relies on, so that they can be proved independently of the physical interpretation. It does not formalize the axioms themselves as a single Lean structure.
The arithmetic goal is an instance of a classical question about monotone completely multiplicative functions. Complete multiplicativity alone fixes only through its values at the primes, which are a priori unrelated to one another, and monotonicity is the only link between different primes. The step from a real exponent to an integer exponent is a separate integrality argument that the paper does not spell out. The linearity milestones need care because the hypotheses hold only on a convex set containing , not on all of . The milestones are explicit but delicate algebra with square roots and boundary cases .
HardyFiveAxioms. State vectors are functions Fin K → ℝ. Indices are -based, so the paper's fiducial vector is index .ℕ → ℕ (goal) or ℕ → ℝ (Appendix 2), constrained only at arguments . The value at is irrelevant.[x₁, …, x_L], and is written as the binomial coefficient .Set.extremePoints ℝ S \ {0}. The classical state space is .vecMulVec v (star v) over ℂ, and the qubit matrices , , and the roots are explicit definitions.unitInterval → ℝᴺ that stays inside the pure states.Contributions are welcome on any milestone. The linearity, extreme-point and positive-definiteness lemmas are reusable beyond this mission.
Whether the gravitational field must be quantized is a long-standing foundational question. One family of arguments, due to DeWitt (1962) and Eppley and Hannah (1977), claims that consistency alone forces quantization: a classical field coupled to a quantum system would supposedly violate momentum conservation, the uncertainty relations, or the impossibility of superluminal signalling. Albers, Kiefer and Reginatto (Phys. Rev. D 78, 064051 (2008)) dispute this claim. In their Sec. IV they give an explicit counterexample: a hybrid model in which a classical gravitational wave interacts with a quantized massive scalar field. The model is the two-dimensional scalar theory of gravity of Nordström, written in the formalism of ensembles in configuration space.
This mission is the second one on this paper. The first, Albers–Kiefer–Reginatto 2008: Measurement Analysis and Quantum Gravity, formalizes Sec. II (the reduced state of photon 2), Sec. III B and Sec. V, and lists Sec. IV and the appendices as out of scope. This mission covers the explicit non-interacting solution of Sec. IV A and the harmonic-oscillator analogy of Appendix A, which the authors use to interpret it.
Timeline.
Ensembles in configuration space. The state of the gravitational field together with the scalar field is a probability functional and a conjugate functional . They obey a modified Hamilton–Jacobi equation (37) and a continuity equation (38). The coupling constant is . For the authors use the ansatz and , with Gaussian functionals
and a one-particle Gaussian with kernel . Substituting the ansatz yields the kernel equations (43)–(48).
Mode representation. Every kernel is expanded in real orthonormal eigenfunctions of with eigenvalue . A kernel is then represented by its mode coefficient . Under this expansion , , and . The paper's solution is
Eqs. (49)–(51), (54), (55), where and are arbitrary constants.
Oscillator ensemble (Appendix A). For a unit-mass oscillator of frequency , a state is a pair . It satisfies and . The paper takes , and the Gaussian
For every finite family of modes and every time with , the coefficients (49)–(51), (54), (55) satisfy the mode forms of Eqs. (44), (45), (46), (47) and (48).
The goal is the precise content of the paper's explicit solution. It is the base point of the first-order hybrid solution in Sec. IV B, and it underlies the paper's counterexample to DeWitt's claim that "the quantization of a given system implies also the quantization of any other system to which it can be coupled". Appendix A provides the interpretation of that solution: the classical sector behaves like an oscillator ensemble prepared with zero momentum and no momentum uncertainty but localized in space.
Formalization adds exact hypotheses: where the cosines must be non-zero, the regularity under which the paper's "most general solution" claim holds, and a correction to the printed energy formula. The paper prints , which is correct only for ; Milestone 11 targets the corrected value. None of these statements has a machine-checked proof on the platform.
The Sec. IV A identities are trigonometric computations once they are reduced to modes, so their difficulty lies mainly in the side conditions. Milestone 7 is a uniqueness statement for a first-order linear PDE on a strip. It requires an argument along characteristics: exhibiting a solution is not enough. Milestones 9–11 are Gaussian integrals, and Milestone 10 is a weak limit of Gaussians whose variance tends to while the centre tends to .
tan, division, and deriv at degenerate points, so every statement assumes where it is needed.