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?
A design constraint may require a symmetric matrix to remain positive semidefinite even when some of its coefficients are uncertain. Such constraints arise in the structural design problems discussed in Chapter 8 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization. A design that satisfies a constraint at the nominal data can fail after a perturbation. The mathematical question is therefore whether the same design satisfies the matrix inequality throughout a specified uncertainty set.
A robust counterpart imposes the original constraint for every admissible perturbation. Even when each individual constraint is simple, the resulting family is generally infinite. This mission concerns one specific family for which the book gives an exact finite representation: a full rectangular matrix perturbation bounded in its Euclidean operator norm. The goal is Theorem 8.2.3, including its nonzero fixed-factor hypothesis and its semidefinite boundary cases.
A real symmetric matrix is positive semidefinite, written , when for every real vector . A linear matrix inequality requires a symmetric matrix whose entries depend affinely on the decision variables to be positive semidefinite. Affine dependence permits both a constant term and a linear term.
Let denote the design variables. The nominal matrix is a symmetric matrix, and is a matrix. Both depend affinely on . The matrix is fixed and nonzero. A perturbation is any real matrix satisfying , where and the Euclidean operator norm measures the greatest expansion of a Euclidean unit vector. Full uncertainty means that no sparsity, diagonal, or block structure is imposed on .
The perturbed matrix is
The two perturbation terms are transposes of one another. Thus this expression is symmetric. This is the fixed- orientation of Definition 8.2.1; the source permits interchanging the two factors when the other factor is constant. All these conventions come from §8.2.1, printed pp. 205–206.
The supporting milestone is the homogeneous S-lemma, Lemma 6.3.5(i). For real symmetric matrices of equal size, assuming for some , it states
The published proved item ModernConvex.SLemma.s_lemma supplies this result. Only part (i) is a milestone: the source's proof of the selected capstone uses the homogeneous version.
The goal is the following equivalence for each design :
This is Theorem 8.2.3, equations (8.2.6)–(8.2.7), printed pp. 206–207. The existential multiplier is chosen for the design, independently of the perturbation. Equivalently, projecting the feasible set in onto gives exactly the robust feasible set.
The block inequality is affine in the joint variables because is fixed. The theorem therefore replaces an infinite family of matrix constraints by one finite matrix inequality with one additional scalar variable. Both directions matter: a feasible certificate guarantees robustness, and every robustly feasible design admits a certificate. The result is stronger than a sufficient relaxation because it loses no feasible designs.
The mathematical theorem is already established in the textbook. The local draft states its exact affine form for a Lean proof. The S-lemma is already proved on Prove2Me, as is the related full linear-fractional perturbation lemma RobustSDP.FullPert.lemma_3_1. That reference includes feedback data and a unit-radius formulation; its relationship to the present statement requires a change of orientation and block coordinates. It is included as prior art rather than labeled as another numbered result from this chapter.
The constraint allows singular matrices. Replacing semidefiniteness by positive definiteness would discard designs permitted by the theorem. Likewise, a reformulation requiring a strictly positive multiplier would change the allowed boundary behavior. The difficult content is the existence of a single scalar certificate for all perturbations, with exactly the displayed block matrix, while retaining those boundaries. A check on a finite sample of perturbations does not establish this universal statement.
All data are real and finite dimensional. Mathlib supplies matrices, transposes, multiplication, affine maps, identity matrices, block matrices, positive semidefiniteness, and the Euclidean operator norm. These existing definitions are used directly; no new definition layer is needed. Matrix indices use Fin, and the block matrix uses the disjoint sum of its two index sets. The row dimension is positive. The nonzero condition on already forces and to be positive. A zero design dimension represents constant affine data.
The nominal matrix is symmetric at every design. It need not be invertible, and may vanish. The multiplier is a real existential variable, with its sign constrained by the block inequality itself. Robust feasibility is an explicit universal statement over the norm ball; no certificate equivalence is assumed in a definition. Theorems 6.3.2 and Proposition 6.4.1 are precursor results, not additional targets of this capstone mission.
Beyond the paper. One sharpness probe removes only from the faithful goal. Constant scalar data , , , satisfy every perturbed original inequality, but the certificate is , whose determinant is . Finding F1 records this evidence. The probe seeks a disproof and is neither the goal nor a milestone.
An engineering decision often has to satisfy a bound even when some coefficients are known only within an uncertainty set. A robust counterpart requires the bound to hold for every allowed realization. For a norm constraint, this replaces a single inequality by an infinite family. The practical question is when that family has an exact finite representation that preserves the feasible decisions. Chapter 6 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization identifies such representations for several uncertainty models. This mission concerns its unstructured norm-bounded model and Theorem 6.3.2.
The result is relevant when an uncertain matrix acts on a residual vector and the model specifies a bound on its largest singular value. It allows the robust constraint to be expressed through positive-semidefinite matrices and a conic certificate. The uncertainty model is consequential: independent uncertainty on the two sides is an explicit assumption, and the theorem does not claim the same formula for coupled perturbations.
The decision is a vector . The nominal residual is , where and are fixed. The uncertain left side has one of two forms:
The dimensions and are positive. The matrix ranges over all real matrices whose induced Euclidean operator norm is at most one. Equivalently, for every vector . In the first form is affine and is fixed and nonzero. In the second, is fixed and nonzero and is affine. The dimensions of and are and , respectively.
The right side is , with affine functions and . Its perturbation set is
Here are fixed data. The set is closed under the standing convention in Section 5.1.2 (printed p. 151). The literal polyhedral branch does not explicitly require it to be nonempty; this omission is retained in the faithful goal and corrected in a separate companion. Either is a closed convex pointed cone and this representation is strictly feasible, or has an explicit finite homogeneous inequality representation. The source denotes the vector by ; the new letter avoids confusing it with the row dimension of . The perturbations and are chosen independently.
The goal is the full equivalence in both parts of Theorem 6.3.2, at every decision . Write
where the dual cone is . In the first case, the target is
with
In the second case the analogous equivalence uses
These are the matrices on printed page 162, equations (6.3.4) and (6.3.5). Positive semidefiniteness, written , means that the symmetric matrix has nonnegative quadratic form on every vector.
The supporting targets retain the book's numbering: the conic representation in Theorem 1.3.4, the Lorentz-cone arrow representation in Lemma 6.3.3, and the Schur-complement and S-lemma results in Lemmas 6.3.4–6.3.5. The Schur-complement reference covers the positive-definite branch; Mathlib supplies the semidefinite branch. Both forms of the S-lemma have published proved references. The homogeneous S-lemma and inhomogeneous S-procedure are reused rather than posed again.
The result identifies exactly the original decisions that satisfy every uncertain inequality. The auxiliary variables describe a projection: their existence is equivalent to robust feasibility at that decision. It is therefore stronger than a sufficient conservative certificate. The nominal residual, the affine factor and the right-side coefficients remain arbitrary within the stated dimensions and assumptions.
The book states the equivalence. This mission preserves its literal hypotheses, including the empty-uncertainty omission recorded in finding F6. Consequently the faithful goal admits a disproof; a corrected companion adds nonempty right uncertainty and retains both equivalences. A successful statement build establishes type correctness; it is not a proof. The remaining theorem items are open formalization tasks, while the referenced S-lemma and positive-definite Schur-complement results already have machine-checked proofs. The finite block constructions can also serve later work on robust quadratic constraints with other uncertainty models.
Exactness must include feasible points on the boundary of the semidefinite cone. In particular, cannot be discarded or treated by assuming an inverse of . An argument restricted to positive would leave part of the theorem unproved. The nonzero fixed factors and the right-side regularity assumptions also have distinct roles and must survive every reformulation.
The source proof contains two local typographical discrepancies recorded in the mission's findings: the sign of a displayed Schur-complement minimizer and a missing additive in equation (6.3.6.a). Neither discrepancy changes the theorem statements. A third proof gap is the use of a right-side minimum where only an infimum is guaranteed: the closed, strictly feasible set has infimum zero for the objective , without a minimizer (F7). Certificate attainment also matters: replacing an existential certificate with a limiting family would change the target.
Coordinates use real function spaces indexed by finite sets, with explicit Euclidean norms . Matrix uncertainty is defined by the contraction property, so the default supremum norm on function spaces never substitutes for the intended operator norm. The two LMI matrices are concrete block matrices, and robust feasibility is independently defined by universal quantification over the two adversaries. Certificate existence is not part of the definition of robustness. Affine maps encode dependence on the decision; there is no full-column-rank restriction on the conic data.
The perturbation dimensions are positive, so the multiplier identity blocks retain their sign implications. Other coordinate spaces can have dimension zero. The nonzero hypotheses exclude impossible fixed-factor cases automatically. All scalar bounds and multipliers are real. There are no real infima, suprema, divisions or integrals whose default values could conceal infeasibility. The cone and dual-cone definitions are reused from the published ModernConvex conic-problem module. The new setup supplies the lifted set, regularity predicate, operator ball and the explicit matrices. Its regularity predicate includes closedness from Section 5.1.2; convexity follows from the lifted cone representation. Nonemptiness is an additional premise only of the corrected companions.
Beyond the paper. A corrected companion to Theorem 1.3.4 adds nonemptiness of the perturbation set. The literal polyhedral statement allows , , , giving an empty set, while a nonzero uncertain right coefficient makes its certificate impossible. The faithful theorem remains the milestone; the correction is a separate item and is not the goal. This finding concerns the literal absence of a nonemptiness clause, rather than the common convention that an uncertainty set has realizations. The same issue affects Theorem 6.3.2 (F6): with the same empty right set and , both robust conditions are vacuous, but requires . A second corrected companion adds exactly nonempty right uncertainty to both cases. The literal theorem remains the goal, and neither companion is a milestone.
The path of a light beam changes when the transparent material through which it travels moves. This matters when interpreting light bending and phase shifts around a flowing liquid, and when asking whether a dielectric can imitate some effects of curved spacetime. Leonhardt and Piwnicki gave a geometrical-optics treatment of a moving, nondispersive dielectric and related its ray dynamics to a spacetime metric in their 1999 paper. This mission isolates their statement that light rays are null geodesics of that metric. Their treatment also connects this geometric picture to a Hamiltonian, a Lagrangian with an artificial mass, and a raised wave vector tangent to the ray. The physical model assumes that the refractive index and flow change gradually over an optical wavelength and cycle; the mission starts with the resulting local optical data rather than claiming an error estimate for that approximation.
A nondispersive dielectric has a refractive index that is independent of optical frequency. Let denote the vacuum speed of light, and let be the velocity of the material at an event, with . The paper uses . The four-flow is , where ; spacetime coordinates are with . The flat metric is .
Gordon's optical metric has contravariant and covariant matrices
The second matrix is the inverse of the first in the physical regime §III.B–C, equations (31), (42)–(43). A wave has laboratory frequency and spatial wave vector ; its covariant wave vector is . The eikonal null equation becomes the dispersion relation . The paper solves it for its positive comoving-frequency branch and defines the laboratory ray velocity . A ray parametrized by laboratory time has tangent , since §III.B, equations (28)–(36).
The goal is the existing Open platform theorem QAlgorithms.Papers.Independent.Renew46.P42.rays_nullGeodesic, posed from §III.D, equations (50)–(51). For a twice continuously differentiable optical patch with and subluminal flow, and a ray satisfying both Hamilton equations with , it asserts at every point of the ray
The scalar allows laboratory time to be a nonaffine parameter. The goal also includes the local-rest-frame identity
where takes a displacement from the medium's rest frame to the laboratory frame. The milestones follow the paper's path: the polarization-independent wave symbol, the dispersion polynomial, the Hamiltonian and its comoving light speed, the inverse metric, the massive action, the rest-frame line element, the zero proper time of the ray tangent, and the tangent relation for the raised wave vector. Three of these are new draft statements; the remaining five are published platform references. The rest-frame milestone is the pointwise form of the goal's second conjunct.
The result identifies the same rays through two descriptions: Hamiltonian trajectories in a moving dielectric and null curves of a Lorentzian optical metric. It fixes which metric acts on covectors and which acts on tangent vectors, and it makes the rest-frame speed visible in the line element. These identifications support the paper's later discussion of phase shifts and vortex flows §IV. Without the null-geodesic link, those later geometric analogies have no stated connection to the ray Hamiltonian.
The formalization work is still open even though the paper's result is known. The platform already has the shared definitions and six relevant theorem statements: three milestones are Proved, while the Hamiltonian characterization, the massive-action result, and the null-geodesic goal are Open. This proposal adds three local statements around equations (33) and (51) and the vanishing proper time. It does not duplicate the existing Open goal. A complete checked development would connect the local identities to the differential-geometric conclusion for rays in varying media.
The pointwise null identity is shorter than the geodesic conclusion. A ray velocity is a gradient of a Hamiltonian containing square roots, and its coordinates are defined only on the nonzero wave-vector branch used here. The full goal then has to relate Hamilton's time-parametrized equations to the Levi-Civita acceleration of a metric whose coefficients vary with position and time. A pointwise null calculation alone does not establish that the covariant acceleration is parallel to the tangent. The distinction between a covector and its raised vector , together with the spatial minus sign in , is essential: using the wrong variance changes the dispersion relation and the tangent statement.
The Lean model uses real coordinate vectors indexed by Fin 3 and Fin 4, real matrices, and the published module QAlgorithms_Papers_Independent_Renew46_P42. Its functions gUp, gDown, fourFlow, waveCovector, lorentzBoost, rayDispersion, rayHamiltonian, and rayVelocity are shared by the goal and every new draft. quadratic comes from the module's published dependency. The boost is the identity at zero flow. The ray tangent is in coordinates . Positive comoving frequency selects the Hamiltonian branch; laboratory frequency itself need not be positive.
The conditions , , and make the physical regime explicit. The zero-proper-time milestone also requires , where the Hamiltonian gradient represents a ray direction. The optical patch in the goal has an open domain and twice continuously differentiable index and flow. The ray has the stated regularity and satisfies both Hamilton equations on an open time set. The local null milestone has nonempty physical instances, rather than relying on a junk square-root value or zero wave vector. The curve-level goal is a universal implication and is vacuous when its open time set is empty. The paper's phrase about minimizing proper time is treated as a local null and pregeodesic claim, without a global minimizing assertion for Lorentzian length.
Reusable contributions include coordinate lemmas for the two Gordon metrics, Lorentz boosts, differentiation of the ray Hamiltonian, and the relation between Hamiltonian motion and covariant acceleration. The wave equation's slow-variation approximation, polarization transport, curvature formula, and vortex applications lie outside this mission's target.
Semidefinite programs that arise in coding theory, extremal geometry, crossing-number bounds and polynomial optimization are often too large to solve directly, but they are invariant under a large symmetry group. Restricting the matrix variable to the invariant matrices loses nothing, and the invariant matrices form a matrix ∗-algebra. The survey of Bachoc, Gijswijt, Schrijver and Vallentin (arXiv:1007.2905, published in the Handbook on Semidefinite, Conic and Polynomial Optimization, Springer, 2012) organizes this symmetry reduction into steps. Its Step 2 (§1.2, pp. 5–7) replaces an SDP over such an algebra by an SDP over a few small blocks, and the justification of that step is a single structure theorem: every matrix ∗-algebra is ∗-isomorphic to a direct sum of full matrix algebras (Theorem 1.2, restated as Theorem 2.7 on p. 13).
The theorem is classical. It is the finite-dimensional case of the structure theory of C∗-algebras (Davidson, C∗-Algebras by Example, Chapter I.10), and in the unital, non-star form it is the Wedderburn–Artin theorem for semisimple algebras over ℂ. Its use in SDP symmetry reduction goes back to Gatermann and Parrilo (2004) and de Klerk, Pasechnik and Schrijver (2007). Section 2.5 of the survey gives a short, elementary, self-contained proof using only linear algebra; this mission follows that proof.
A matrix ∗-algebra (Definition 2.1, p. 10) is a complex linear subspace that is closed under matrix multiplication and under the conjugate transpose . It need not contain the identity matrix, and it may be .
A map between matrix ∗-algebras is a ∗-homomorphism (Definition 2.6, p. 13) if it is linear, satisfies and ; a bijective ∗-homomorphism is a ∗-isomorphism. The direct sum is the algebra of block-diagonal matrices with diagonal blocks of sizes (p. 10).
The proof uses the following vocabulary (p. 13). The center of is . The unit of is the unique with for all . is simple if it is non-zero and . For a partition , is the zero-one diagonal matrix with ones in the positions of .
For every matrix ∗-algebra there are and and a ∗-isomorphism
The goal fixes no sizes: it asserts only the existence of the block structure, which is the form Step 2 uses.
Milestones 7 and 8 together give the goal.
The result. A ∗-isomorphism preserves positive semidefiniteness, so Theorem 2.7 turns the constraint ", " into independent constraints on blocks of sizes , with . This is what makes the Lovász ϑ-number of symmetric graphs, the Delsarte and Schrijver bounds for codes, and the crossing-number bound of de Klerk et al. computable at scale (§§4–6 of the survey). Without it, an invariant SDP still has a variable of the original size .
Formalizing it. The theorem is proved and textbook material; it is not open. As far as a search of the platform shows, it is not formalized in this form: Mathlib has Wedderburn–Artin for semisimple unital algebras over an algebraically closed field, which yields an algebra isomorphism but neither the star structure nor the non-unital case, and the platform holds a proved matrix-units statement for unital ∗-subalgebras (HarlowTASI.fdStarAlgebra_exists_matrixUnits, attached to this mission as a reference). The mission adds the non-unital ∗-isomorphism, the simultaneous unitary diagonalization of a commutative matrix ∗-algebra, and the intermediate facts of the elementary proof, each stated in a reusable form.
Two points make the obvious routes insufficient. First, a matrix ∗-algebra need not contain the identity: its unit is a projection onto a subspace, and the coordinates in carry no part of the algebra. Statements and arguments that start from a unital subalgebra do not apply without first cutting the algebra down to the range of its unit. Second, an algebra isomorphism onto a product of matrix algebras is not enough: the isomorphism must commute with the conjugate transpose, since positive semidefiniteness is defined through it. Abstract Wedderburn–Artin provides the first kind of isomorphism, and turning it into a ∗-isomorphism requires choosing the matrix units compatibly with the adjoint, which is where the content of the theorem lies. The elementary proof avoids ring theory entirely but has to control every off-diagonal block , which is the role of observations (i)–(iii).
NonUnitalStarSubalgebra ℂ (Matrix (Fin n) (Fin n) ℂ); Mathlib's star on matrices is the conjugate transpose. The index set is Fin n (0-based).StarAlgEquiv ℂ (≃⋆ₐ[ℂ]) on the subtype of : additive, multiplicative, ℂ-linear, star-preserving and bijective, exactly Definition 2.6.(k : Fin d) → Matrix (Fin (m k)) (Fin (m k)) ℂ with pointwise operations and star; it is ∗-isomorphic to the block-diagonal algebra (Matrix.blockDiagonal'). is allowed and is needed for .S : Fin n → Option (Fin k), with none for and some i for ; the paper's block is represented by the full-size product .The goal is not to be read with a unital StarSubalgebra (that adds the hypothesis and is the case already covered by the reference item), with an AlgEquiv that ignores the star, or with a mere linear equivalence (which exists for dimensional reasons and has no content). Each of these would trivialize or weaken the statement.
Useful infrastructure, reusable beyond this mission: simultaneous unitary diagonalization of commuting normal matrices, the unit and the central decomposition of a non-unital finite-dimensional ∗-algebra, and an explicit ∗-isomorphism from a corner algebra onto . Proofs of any milestone, and alternative routes to the goal (for example through Mathlib's Wedderburn–Artin plus a star-compatibility argument), are welcome.
A reverse convex set is the part of a polyhedron that lies outside an open convex set: , where and is open and convex. Such sets arise whenever a model forbids a convex region: integrality (a lattice-free convex set contains no feasible point in its interior), bilevel programs, where the points with for a convex value function are infeasible, and nonconvex quadratic or polynomial constraints. Optimizing over calls for valid inequalities for its closed convex hull.
The classical tool is the intersection cut of Balas (Balas 1971): starting from a basic solution of the linear relaxation that lies inside , one follows the extreme rays of the basis cone until they leave , and the exit points define a valid inequality. Towle and Luedtke study the opposite case, where the basic solution lies outside the closure of . Then the rays of the basis cone may enter , cross it, or never leave it, and no single inequality captures the structure. They replace the cut by a disjunction: a finite union of simpler sets that contains , to which the disjunctive programming machinery of Balas can be applied. The present mission targets their multi-term disjunction (Theorem 5 of the paper), which uses the full recession cone of .
Let have full row rank and . A basis splits the variables into basic variables and nonbasic variables , with a tableau and a basic solution ( for ) such that holds exactly when for all . Dropping the sign constraints on the basic variables gives the basis cone
a translated simplicial cone with apex and extreme rays (): , for , and for the other nonbasic .
The recession cone of is . Along each ray, the halfline , , meets in an interval with endpoints
in the extended reals, with , when the halfline misses . This sorts the nonbasic indices into (the ray misses ), ( finite and positive, : the ray enters and stays) and (: the ray crosses ); write . For extended reals and a vector , the segment is , and , are defined likewise. The paper builds the inner approximation of
and the sets
Throughout, , and (Assumption 2 of the paper) .
With ,
The relaxation of is thus a disjunction of terms.
Theorem 5 turns the nonconvex set into a finite union of sets with explicit generators. By the paper's Theorem 2, has the same closed convex hull as , so valid inequalities for the disjunction are valid for the reverse convex set and lose nothing in the limit. The paper then relaxes each term to a polyhedron (§4.4), and a cut-generating linear program over the union separates candidate points; when is bounded the disjunction collapses to the two-term disjunction of the paper's Theorem 1. The disjunction is therefore the bridge between the geometry of (its recession cone and the exit parameters along the basis rays) and polyhedral cut generation.
The result is proved in the paper (arXiv:1901.02112v5, pp. 17–18; Mathematics of Operations Research, 2022). It has no machine-checked proof. Formalizing it checks the extended-real conventions for , the treatment of empty and unbounded segments, and the role of the recession cone, all of which the paper handles in prose. The definitions of the basis cone, the exit parameters and the recession cone are reusable for other intersection-cut results on the platform.
The inclusion is immediate from the definitions. The reverse inclusion is the substance: a point lying in every term comes with unrelated representations, one per term, each using different segment parameters, a different multiple of and a different recession direction. A point of needs a single representation with all segment parameters inside and no negative multiples of the rays. A naive average of the representations keeps the negative components along the rays , so it does not land in . The rewriting of in Proposition 5 also needs care: it replaces by inside a convex hull, and absorbs the rays of into the recession cone, which holds only because is open.
Vectors are functions on a finite index type (the paper's ). The basis is the published Disjunctive.GeneralDisjunctions.IsTableau (a genuine tableau of , with a partition and ) together with , and the extreme rays are the published Disjunctive.GeneralDisjunctions.extremeRay. is defined, as on the page, by the tableau equations and . The exit parameters are EReal-valued infima and suprema over real parameters, so the empty set gives and and an unbounded set gives ; segments quantify over real compared with extended-real endpoints. are filters of , and . The index of is encoded by stating the term separately from the terms , . The recession cone is the universal-quantifier cone, which is the whole space for ; in that case every set in the goal is empty or and the identity is .
All hypotheses are the paper's: open and convex, of full row rank (§2), (§3), and Assumption 2 (§4). One generalization: the basic solution need not be feasible ( is not imposed); the paper's own Example 2 uses an infeasible basic solution and the proof of Theorem 5 does not use feasibility.
Real-valued (where an empty or unbounded parameter set returns ), segments with endpoints converted to reals, or an encoding in which is always empty would trivialize the statement; the extended-real definitions rule these out, and a sorry-free check confirms that the hypotheses are satisfiable with (one variable, ).
The development needs Minkowski sums and convex hulls of unions in , recession cones of open convex sets, and a Farkas-type alternative (for Lemma 2); the platform's LinearOptimization.farkas_lemma is available. Proofs of the milestones in any order are welcome; Lemma 2 is self-contained.
A creator-side experiment on a short-video platform may assign treatment to individual videos while measuring outcomes over a viewer's whole session. A treated video can alter what the viewer watches next, so its effect may persist beyond the immediate reward. The paper studies this form of interference using a Markov decision process and asks how well data from a per-video experiment estimate the effect of treating every video instead of none. Its motivating application is an experiment at Douyin, where viewer state includes attention and other factors that need not be observed by the estimator. Farias et al., 2023 give an estimator based on reward-to-go and a quantitative bias bound for an absorbing-session model.
The distinction matters for experimental design: the usual inverse-propensity estimate weights only the reward received immediately after an assigned action. In this setting it can omit the effect of that action on later rewards. The paper's Differences-in-Qs (DQ) statistic instead weights the remaining reward in the session after each assignment. The mission focuses on the theorem that quantifies the resulting bias in the finite absorbing model of Sections 3–5.
Let be a finite state set and let the actions be control and treatment . An action has a stochastic transition matrix and conditional mean reward . The initial state has probability law . A stationary policy assigns action probabilities at each state; its induced transition matrix is . Global control always selects , global treatment always selects , and the experiment independently selects each action with probability one half at each step. Thus .
A path consists of successive state-action pairs . Its law begins with , draws each action from , and then draws from . The total expected reward is . The target average treatment effect is .
The session has a common absorbing class : under each policy of interest, transitions from this class stay in it, and its mean rewards vanish. Assumption 1 bounds the expected number of steps spent outside that class, from every initial state, strictly by . These conditions make the infinite total-reward quantities meaningful. The paper writes a stronger absorbing-row equation that does not define a stochastic row when the class contains more than one state; the formalization uses the closed-class interpretation and records the discrepancy for review.
For a path from the half-treatment policy, the DQ estimator assigns weight or to the reward remaining after each treatment or control action, respectively. With the path stopped at , write that statistic as . The infinite-horizon expectation is defined through the limit of its finite-path expectations, not through a value-function identity.
The goal is Theorem 1 of Farias et al., in the absorbing regime. If every row of has total-variation norm at most and , then the estimator expectations converge to and
The milestone targets include the matrix resolvent identities of Lemmas 1–2, Theorem 2's finite-order expansion of the total-reward value functional, and Corollary 1's absorbing-case remainder bound. They also identify trajectory reward with the value functional and connect the trajectory DQ statistic to the first-order expansion. The listed order follows these mathematical dependencies. The mission does not assert Theorem 2's discounted, average-reward, or finite-horizon cases, which the goal does not need.
The bound distinguishes the DQ estimator from an immediate-reward estimate: its bias is at most quadratic in the row distance , with explicit dependence on expected session length and reward magnitude. It gives a criterion for when a per-video experiment can approximate the all-treatment versus all-control effect despite changes to later states. This is a statement about expected estimator bias; it does not by itself give a variance or finite-sample confidence bound.
The formal development separates three objects that are easy to conflate: the statistic computed from a trajectory, its expectation under the experimental policy, and a value-functional expansion used to analyze that expectation. The matrix identity corresponding to Lemma 1 is already machine checked on Prove2Me as MarkovEntanglement.resolvent_identity. The goal and other mission statements are compilation-checked drafts with proof obligations still open. A completed formalization would establish their convergence and equality claims as well as the printed bias constant, and would leave reusable finite-state path and absorbing-value definitions.
The immediate-reward estimate evaluates outcomes under the experimental state distribution, while ATE compares outcomes under two different state distributions. Weighting each current reward cannot generally account for that mismatch. The DQ statistic incorporates reward-to-go, but its infinite double sum must be related to a convergent trajectory expectation before any bias inequality applies. The central quantitative issue is to control how changing a policy perturbs the total-reward functional across repeated transitions, with the exact scale. A direct comparison of one-step rewards alone does not yield that order.
States and actions are finite. Transitions are nonnegative and row-stochastic, the initial law is a probability vector, and policies are stationary probability kernels. The goal's actions are Fin 2, with treatment and control. Path expectations are finite sums; infinite expected rewards and Q-functions use real series. The absorption-time condition asserts convergence with HasSum and a strict bound from every state. Its closed-class, zero-reward conditions apply under , , and . The reward field records conditional means, sufficient for the expectation claims.
Here is the row norm . The paper does not define its normalization; with the alternative half- convention the printed Theorem 1 constant fails. This choice is part of the statement, not a hidden rescaling. The truncated estimator is formed from path rewards exactly as equation (4) prescribes; defining its expectation as the first-order expansion would erase the mission's main identification step. The paper's Section 5.3 display also places the outer value functionals at and , while its claimed identity and Theorem 2 require ; the milestone states that corrected reading and retains the printed display in its provenance.
Useful contributions include convergence of finite-path expectations, the absorbing total-reward resolvent theory, and the exact finite-order remainder estimate. These definitions and lemmas can also support other finite absorbing policy-evaluation problems.
Quadratic hedging chooses a self-financing trading strategy that minimizes the expected squared difference between its terminal value and a payoff ; with constant it becomes mean–variance portfolio selection. The classical theory works in discounted prices: one asset is a risk-free numeraire, and optimal strategies are written in terms of the remaining assets (Černý and Kallsen 2007; the paper refers to Schweizer's 2010 encyclopedia entry Mean–variance hedging for an overview). Černý, Czichowsky and Kallsen drop that assumption. In their market no asset need be risk-free, and they want formulas for the optimal strategy that do not depend on which asset is used as the unit of account (arXiv:2110.09416v4, §1).
In their feedback formula (Theorem 4.1, p. 15) the optimal strategy is built from two processes. One is the adjustment process , which corrects the hedging error accumulated so far. The other is the pure hedge , which offsets the fluctuations of the claim's value process. At each time both are minimizers of a finite-dimensional quadratic problem with one linear budget constraint. The covariance-type matrix in that problem may be singular, for instance whenever a risk-free asset is present. So the minimizers are not unique and ordinary matrix inversion does not describe them. Theorem 4.3 of the paper (p. 16) gives explicit formulas for the whole solution sets, and Appendix A (pp. 24–28) proves the linear algebra behind them. That linear algebra is a general result on affinely constrained quadratic minimization with singular data, built on the oblique-projector analysis of Černý 2009.
Fix a time and a state. The data of the pointwise problem are:
Portfolios are row vectors and price-type quantities are column vectors, as in the paper (§2, p. 6). is the column space and the null space of a matrix. Every matrix exponent in the paper denotes the Moore–Penrose pseudoinverse: the unique with , , , (p. 24, (A.2)). The two problems are
where an is the set of all global minimizers over the whole hyperplane (possibly empty). With and the paper defines
The general problem of Appendix A is to minimize over with , where and .
and , .
In attack order: existence and uniqueness of the pseudoinverse (published, proved); Proposition A.1 (pseudoinverse rules); Proposition A.3 (affinely constrained least squares); (A.8) and ; (A.14)–(A.15); the completed square (A.16); Theorem A.4(1) (bounded below iff ); A.4(2) (all minimizers are with of minimum norm); A.4(3) (value identities); Lemma A.5; A.4(4) (formulas (A.6)–(A.7) through the oblique projector onto along ); and the range fact used in the proof of Theorem 4.3.
Theorem 4.3 gives closed forms for both ingredients of the optimal hedge. It covers markets with and without a risk-free asset in one formula, because and are the only two cases. In the second case is a fully invested portfolio with zero instantaneous variance. The paper uses them in its efficient-frontier analysis (§5) and its examples (§6). Theorem A.4 does not depend on finance. It gives a complete solution of a positive semidefinite quadratic program with linear equality constraints: when it is solvable, the full set of minimizers, and the minimum-norm minimizer. Its proof needs nothing beyond finite-dimensional linear algebra.
The paper proves all of these results. Proposition A.3 is taken from Černý (2009), and v4 (7 July 2025) strengthened Proposition A.3 and Theorem A.4 after the journal version (doi:10.1287/moor.2023.1374). The mission cites only v4. None of the statements has a machine-checked proof. The Penrose predicate and Penrose's existence and uniqueness theorem are already on Prove2Me as proved results. Mathlib at the pinned revision has no Moore–Penrose pseudoinverse, so the pseudoinverse calculus built here can be reused.
With a singular , completing the square with an inverse is not available. On the affine set, the quadratic part can vanish in some directions while the linear part keeps decreasing. The boundedness criterion has to detect exactly these directions. Under that criterion, a formula has to describe every minimizer, not just one stationary point. The constraint brings in the projector , and need not commute with it. As a result, the relevant projector is oblique, not orthogonal, and the obvious guess plus a correction fails. Exhibiting one feasible point with zero gradient does not prove the set equality, the minimum-norm property, or the case formulas (A.7). The case needs its own treatment through .
Fin d → ℝ with ⬝ᵥ, and matrices are Matrix (Fin m) (Fin n) ℝ. A row vector times a matrix is written x ᵥ* M and a matrix times a column vector M *ᵥ x, matching the paper's printed order. Column and null spaces are LinearMap.range/LinearMap.ker of Matrix.toLin'.LocalDistanceNetwork.IsMoorePenroseInverse (the four equations (A.2)). Because the pseudoinverse exists and is unique, this is the same as "the" pseudoinverse. Lean's ⁻¹ is used only on real scalars, never on a singular matrix.Matrix.PosSemidef, which includes symmetry. Argmin sets range over the whole affine set or hyperplane. Minimum norm compares squared Euclidean norms over the whole set.An investor can improve a portfolio by adding a zero-cost combination of long and short positions. Ordinary arbitrage asks whether such a combination pays nonnegatively in every outcome and positively in some outcomes. That test is restrictive when payoffs have both gains and losses. Arvanitis and Post instead ask whether one overlay portfolio raises expected utility for every admissible risk preference and every benchmark portfolio in a specified class. This gives an asset-pricing question that acknowledges uncertainty about investors' preferences and starting positions. The authors use the concept to study factor portfolios and transaction costs in their 2022 working paper Ordering Arbitrage Portfolios and Finding Arbitrage Opportunities (AUEB Department of Economics Working Paper 04-2022), published as Generalized Stochastic Arbitrage Opportunities in Management Science in 2024.
The target is the paper's Theorem 2.3.1, an existence condition for a pricing system. The working-paper statement needs a finite-generation condition on the utility class for its converse. The resulting mission records the corrected theorem and the general direction that does hold for arbitrary admissible utility classes.
There are finitely many base assets, indexed by . Their one-period payoff vector is with probability law , supported on for finite . A benchmark position costs . The benchmark set is closed and bounded; it can contain many portfolios and need not be convex. An overlay is feasible when , where has rows. Thus is the bounded overlay polytope, and is the passive choice.
The utility class contains continuously differentiable, strictly increasing, strictly concave functions . It is convex and uniformly bounded on bounded payoff intervals. For an overlay , the expected utility increment relative to benchmark is
A strict stochastic arbitrage opportunity is a single feasible overlay that improves every benchmark for every admissible utility. The set is
The paper's candidate stochastic discount factors are . A factor assigns the present-value vector to the base assets. The relevant polar cone is written in the paper's constraint coordinates as . This representation encodes the overlay inequalities and their shadow prices.
For the paper's general convex class , the existence of a mixture of marginal-utility discount factors whose present value lies in rules out every strict stochastic arbitrage opportunity:
If is the convex hull of a finite set of admissible utility functions, the converse is also claimed:
This is the mission's goal. The benchmark set remains any closed bounded set satisfying the budget restriction. ### Supporting milestones
The milestones follow the proof of Theorem 2.3.1 (pp. 34–35): the first-order (Karush–Kuhn–Tucker) condition for optimality on the segment , ,
the concavity bound ; the convexification step (9)–(10) in its pointwise form; the minimax reversal (10)–(11) and the linear-programming duality (11)–(13), both available as proved platform theorems; and the general pricing implication above.
The condition translates absence of a portfolio improvement shared by all the specified investors into the existence of a discount factor with constrained asset values. In markets with transaction costs, the cone can permit price intervals rather than one exact price vector. This connects an investor-facing arbitrage test to restrictions that can be checked through the market's linear constraints. The working paper (§2.3, p. 11) discusses that interpretation and its factor-investing application.
The result is a published mathematical claim but, in this representation, still a Lean proof obligation. A formal development would produce reusable definitions of strict utility-based arbitrage and marginal-utility pricing, plus machine-checked proofs of the valid pricing implication and the corrected converse. The two general minimax and linear-duality results referenced here already have proved Prove2Me statements; the paper-specific statements in this mission are draft goals and have no machine-checked proofs yet.
The converse has a quantifier problem: no single overlay can improve every utility and benchmark, even though different utilities may reject different overlays. Treating one failed endpoint comparison as a first-order optimality condition does not resolve that problem. In fact, a concave expected-utility function may end below its starting value at while initially increasing as leaves zero. The paper's proof makes that invalid identification. Its unrestricted utility class also permits limiting behavior that defeats the asserted converse. The finite-generation condition in the goal prevents that particular failure while retaining a nontrivial family of preferences and a general compact benchmark set.
Lean uses Fin N → ℝ for payoffs and portfolio positions, a probability measure for , and Bochner integrals for expectations. The almost-sure box-support condition makes the utility and marginal-utility expressions integrable under the stated continuity assumptions. The matrix inequality defines directly; is the paper's representation, rather than an abstract inequality definition. The set of discount factors allows every positive scale and takes the ordinary finite convex hull. The utility derivative is deriv u, justified by the continuously differentiable assumption. Lean's lo and hi name the support endpoints and aVec names the constraint right-hand side; the paper uses for both roles.
The corrected goal's finite generation of is an explicit addition to the printed Theorem 2.3.1. To see the need, take one riskless payoff , a second payoff with equal probabilities, one benchmark , and overlays for . A convex class generated by increasingly steep, smooth, strictly concave utilities has no strict SAO, yet every candidate marginal-utility discount factor at that benchmark is a positive constant and assigns positive value to the second asset, outside .
The SAO predicate remains the actual difference of two expected utilities. Defining it through the derivative inequality would erase the principal economic question. Supporting work may establish bounded-support integration, finite-dimensional compactness, convex-hull behavior, and the relation between the matrix cone and the overlay inequalities; these are reusable for other one-period pricing models. A result that only assumes the pricing restriction, or changes the benchmark set to a singleton, does not settle this goal.
Empirical risk minimization (ERM) is the inductive principle behind most of statistical learning: a learning machine picks, from a set of functions, the one with the smallest average loss on the training data, in place of the one with the smallest expected loss under the unknown distribution. Whether this substitution is justified is the first question of learning theory, and Chapter 2 of V. N. Vapnik, The Nature of Statistical Learning Theory (2nd ed., Springer 2000, doi:10.1007/978-1-4757-3264-1) answers it.
The history is short. Vapnik and Chervonenkis gave the entropy criterion for uniform convergence of frequencies to probabilities in 1968 and published the proof in 1971 (Theory Probab. Appl. 16, 264–280); in 1981 they extended it to uniformly bounded real functions (Theory Probab. Appl. 26, 532–553); in 1989 they proved the key theorem, which reduces consistency of ERM to uniform one-sided convergence. The book states all of these results without proofs (Preface, p. xi); the proofs are in Vapnik, Statistical Learning Theory (Wiley 1998) and the cited papers.
Let be a probability measure on a measurable space , and let , , be a set of real functions on indexed by an arbitrary parameter set . The risk of is . For an i.i.d. sample drawn from , the empirical risk is . Probabilities are taken under the product measure .
For let . The ERM method is nontrivially consistent (from p. 38 on simply "consistent") if for every with nonempty,
Removing the functions of smallest risk rules out consistency that is caused only by a single function lying below all the others. Uniform one-sided convergence means for all (2.4). Uniform two-sided convergence is the same with (2.6).
For a set of bounded functions , the random VC entropy is the logarithm of the size of a minimal -net, in the metric (maximum over the sample points), of the vectors . The net is internal: its points are themselves vectors of the set. The VC entropy is . For indicator functions, is the number of distinct binary vectors on the sample. From it the book defines the entropy , the annealed VC entropy , and the growth function .
If for all , then
Only the risks are bounded, not the functions. The constants and are arbitrary, and they appear only in the hypothesis.
VapnikChervonenkis.Entropy.theorem4_entropy_criterion and is referenced here.The key theorem says that consistency of ERM is decided by the worst function of the set, in the one-sided sense of (2.4). Every analysis of ERM must therefore control a supremum over the whole set, a worst-case analysis (p. 39). This turns the question of consistency into the question of uniform laws of large numbers. Theorem 2.3 and its corollary answer that question through the VC entropy. The three capacity concepts underlie the "three milestones" of §2.7: consistency, a fast rate of convergence, and distribution-free guarantees. These are also the objects of the later missions of this series.
The platform already has the 1971 indicator-class criterion (Proved) and the related entropy-rate lemmas for event classes. It has no real-valued loss class with a parameter set, no notion of nontrivial consistency, no key theorem, and no VC entropy built from -nets of real functions. This mission supplies those definitions with the book's conventions, and states the key theorem and its neighbours as open targets.
The theorem is an equivalence between a statement about infima over the shrinking families and a statement about one supremum over all of . Neither the functions nor the empirical risks are bounded; only the risks are. The empirical infimum over may therefore be , and no compactness of is available. Single-function laws of large numbers control each separately, but they do not control the supremum: for an infinite they are not enough, and that is the content of the chapter. For Theorem 2.3, the necessity direction is a genuine probabilistic argument about the growth of covering numbers, and the measurability of suprema over an uncountable must be handled explicitly.
All declarations are in the namespace NatureSLT.Consistency. The parameter set is an arbitrary Lean type and . A sample of size is Fin ℓ → Z under Measure.pi (fun _ => F), and a probability is a value of that measure in . The risk is a Bochner integral, and every theorem that uses it assumes each integrable. Logarithms are natural. The minimal -net is internal and uses the metric , as in the book's footnote 3; it is not Mathlib's external covering number. "Monotonically decreases" (p. 50) is read as non-increasing.
Suprema of deviations and the infimum of empirical risks over are taken in the extended reals, so they are genuine values and never a junk default. The infimum of the risks is a real infimum over a nonempty , which is bounded below by . No extended-real subtraction occurs: the event is written as or .
The book's "some (technical) conditions of measurability" are explicit hypotheses. In Theorem 2.1, and are measurable functions of the sample. In Theorem 2.3, , , the half-sample deviation and the random VC entropy are measurable. For indicator classes, is measurable.
A trivializing formalization is ruled out. Consistency is the nontrivial notion (2.3), quantified over every nonempty , not the classical one that a minorizing function satisfies trivially. The probability of a non-measurable event is never read as : Lean evaluates it as an outer measure.
Beyond the paper. One strengthened variant is posed, key_theorem_strong (finding F1). It is Theorem 2.1 with the two measurability hypotheses removed and probabilities read as outer probabilities. The known argument needs only monotonicity and finite subadditivity of the probability of events, together with the weak law of large numbers for a single integrable function, so measurability is never used.
Contributions are welcome on any item. Reusable beyond this mission are the risk and empirical-risk definitions, uniform one- and two-sided convergence, and the VC entropy of a real class. Theorems 2.2 (maximum likelihood), 2.4 (one-sided convergence through minorant classes), 2.5 and 2.6 (nonfalsifiability) are not part of this mission.
Gittins index policies are optimal for a single server choosing among alternative bandit processes, and the achievable region method of Bertsimas and Niño-Mora (Math. Oper. Res. 1996) explains why: when the performance vectors of a scheduling system satisfy generalized conservation laws, the region they fill is a polytope whose optimal vertex is an index priority. Most real systems have several servers working in parallel, and for them the conservation laws fail. Glazebrook and Wilkinson (Ann. Appl. Probab. 2000) observed that parallel machines are close to a single machine working at times the speed, where the laws do hold, and turned that closeness into explicit bounds on how much an index policy can lose. Section 5.7 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., Wiley 2011, doi:10.1002/9780470980033), presents that analysis for the simple family of alternative bandit processes (SFABP). Its first quantitative output is an upper bound on the optimal return, Corollary 5.20. This bound is the reference point against which the index heuristics of the rest of the section are measured.
This mission continues the public series Multi-armed Bandit Allocation Indices I–VI. Mission IV of that series formalized the single-machine achievable region theory of Chapter 5: Lemma 5.1, Theorems 5.5 and 5.10, and the identity of the adaptive greedy indices with Gittins indices.
There are arms. Arm has a finite state space ; the are disjoint, and their union is the set of job types. One transition kernel on moves an arm when it is processed. Each is closed under , and is irreducible on each . Time is discrete, rewards are discounted by with , and processing a job of type earns . There are identical machines, . At each time a policy chooses, on the basis of the history, a set of exactly arms. Each chosen arm makes one transition and the others are frozen. From the initial state-vector , the performance is the expected total discounted number of times a job of type is processed. The return is , and .
The matrix is the single-arm matrix of §5.3, published in the series as conservationCoeff: for , , where is the number of transitions the chain started at needs to return to , and otherwise. Job types are numbered in ascending order of the indices produced by the adaptive greedy algorithm (IsAdaptiveGreedy, greedyIndex), and . Write
Let be the number of arms with no job type in , let , and number the arms so that . For each other arm, is the processing needed to bring it from into for the first time, and is the sum of these over the other arms, which evolve independently.
The goal keeps the book's constants. Eq. (5.27) is a companion bound from the same identity.
The bound is explicit and computable from single-arm quantities: the AG indices and the laws of first-entry times. Subtracting from it the exact return of a concrete policy gives a certified suboptimality gap without solving the parallel-machine dynamic program, which has no index solution. The book uses it in exactly this way. With the exact return (5.30)–(5.31) of the heuristic , it shows that loses , and in the limit that is average-overtaking optimal (Theorem 5.25).
All of these results are proved in the book and in Glazebrook and Wilkinson (2000). None is machine-checked. The series so far covers only the single-machine theory, and there is no parallel-machine bandit model on Prove2Me. This mission supplies that model and states the first link of the chain: from conservation-law algebra to a bound for a system that does not satisfy the conservation laws.
The identity (5.25) is algebra once the policy processes exactly arms in every period. The difficulty is the lower bound on . The obvious idea, which works for one machine, is to minimize by giving priority to job types outside . On machines such a policy cannot keep every machine busy outside , and the minimizing policy is not known, so has no closed form and must be bounded below over all history-dependent policies at once. The bound has to hold uniformly: it must account for each arm's processing both before and after its first visit to , with arms frozen for random lengths of time in between. The printed proof also contains a step whose last inequality goes the wrong way (finding F2). The lemma is true, but the printed chain of inequalities cannot be followed literally.
Job types are Fin (N + 1), so the book's is Lean's N + 1 and the book's type is the Lean index i - 1. Sums over run over i : Fin N, with = ν i.succ, = ν i.castSucc and = Finset.Iic i.castSucc. The arms are Fin n, and arm : Fin (N + 1) → Fin n assigns job types to arms. One kernel on the disjoint union replaces the book's per-arm matrices , and IsArmFamily states closedness and irreducibility. A policy (ParallelPolicy n N M) is a sequence of Markov kernels from histories to Boolean selection vectors with exactly true entries. The law of the history is built by composition, and the performance is a discounted sum of expected per-period occupation counts. and are a real supremum and infimum over all policies. The class is nonempty because , and both families are bounded, so neither takes a junk value. is an integral against the product of the single-arm chain laws, with a real exponent and . The numbering by AG indices is two hypotheses: the identity permutation is an output of , and is monotone. The arm numbering is a function lowest with lowest b and lowest monotone.
Unit conversions: none. Section 5.7 is written in discrete time with discount factor , the convention of the series' published definitions, so every constant is the book's.
Correction of the setup: the book assumes "the number of parallel servers exceeds the number of arms " (p. 139). The rest of the section needs the opposite (finding F1): for instance, the arm index in Corollary 5.20 is not positive when . Every item assumes .
Trivializing formalizations ruled out: is not a hypothesis or an abstract GCL quantity. It is the infimum over an explicitly constructed, nonempty class of parallel-machine policies, so the goal cannot be discharged by assuming the conservation laws for the -machine system (which fail). The theorems do not allow , where the policy class is empty and the supremum would take the junk value .
Out of scope: the branching-bandit bounds of §5.5 (Theorems 5.12 and 5.13). They need a continuous-time branching-bandit model whose GCL property the book only cites. Also out of scope are Theorem 5.11 (priority classes) and the results 5.21–5.23 and Theorem 5.25.
Reusable infrastructure: the parallel-machine SFABP model (Def_AllocationIndices_Branching_Parallel) serves the remaining results of §5.7. Lemmas on the law of a frozen arm's trajectory under an arbitrary policy are welcome contributions.
A multi-armed bandit in the sense of Gittins is a sequential allocation problem: several independent Markov reward processes compete for a single resource, at each decision time exactly one of them is operated, and the goal is to maximize the expected total discounted reward. The Gittins index theorem says that it is optimal to operate, at every decision time, a process of largest index, where the index of a process depends only on that process. Chapter 4 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., Wiley 2011, doi:10.1002/9780470980033), extends it to superprocesses, precedence constraints and arrivals.
In practice an index is rarely computed exactly. It is approximated numerically, or a heuristic policy is shown to be close to an index policy, so one needs to know how much reward is lost when a policy is only approximately an index policy. Section 4.10 of the book answers this for two notions of approximation. For ε-index* policies, which choose whole stages whose reward rate is within ε of the largest index, Corollary 4.16 bounds the loss by ε times the total discounted time. This mission formalizes Corollary 4.16 and the freezing-rule and promotion-rule lemmas of §4.5 on which its proof rests. The bound goes back to Katehakis and Veinott (Math. Oper. Res. 1987).
This mission continues the public series Multi-armed Bandit Allocation Indices I–VI in the same namespace, AllocationIndices, reusing its model and definitions.
A bandit process is a Markov chain on a countable state space with transition kernel . Each time the continuation control is applied it yields the bounded reward and moves one step; under the freeze control it stays put and pays nothing. Decision times are and rewards are discounted by with . For a positive stopping time of , and are the expected discounted reward and time before , , and the Gittins index is (the discrete-time index (2.6), gittinsIndex P r a x).
A freezing rule for is a nondecreasing sequence in , where depends only on . The reward of process time is postponed to time , and means it never accrues. Then
A stopping rule is the special freezing rule for and otherwise.
A simple family of alternative bandit processes is operated by a policy : at each decision time chooses, possibly at random and on the basis of the whole history, one process to continue, and the others are frozen. Its payoff is the expected total discounted reward, and . For a positive stopping time of the family's history, and are the reward and discounted time accrued before , and the index of the family is
An ε-index* policy proceeds in stages. At the start of a stage it chooses a process and a positive stopping time of 's own evolution with , all indices evaluated at the current states. It continues up to and then repeats.
For every ε-index* policy , every and every initial state-vector ,
The book states in continuous-time units; is the same bound in the discrete-time units of the index (2.6) (see Formalization scope).
where and are the reward and discounted time with no freezing.
5. Theorem 2.1 (p. 91, restated in §4.5), referenced: an index policy attains (BanditAlgorithm.gittins_index_theorem, proved on the platform).
Corollary 4.16 makes the index theorem robust. Any procedure that certifies, stage by stage, a reward rate within ε of the largest index is guaranteed a payoff within of optimal. Examples are a numerical index computation with error ε, or a heuristic whose stages are near-optimal stopping problems. At it is the statement that modified forwards induction policies are optimal. Lemmas 4.5–4.7 carry the freezing-and-promotion proof of the index theorem, which the book notes "comes into its own" for families that are not simple (§4.6–4.7, jobs with precedence constraints).
Status: the index theorem itself is formalized and proved on the platform (BanditAlgorithm.gittins_index_theorem). The companion bound for ε-index policies, Theorem 4.18 ( in the same units), is posed and open as AllocationIndices.eps_index_policy_near_optimal. Freezing rules, the family index (4.5) and ε-index* policies have no formal counterpart yet.
The obvious attempt is to repeat the interchange argument of Lemma 2.4 stage by stage. It does not work directly: an arbitrary policy interleaves the first stage of with portions of the other processes in a history-dependent way. Moving that stage to the front postpones the other processes' rewards by a random amount and advances 's rewards by another. Comparing the two needs inequalities that hold for every past-measurable postponement or promotion, not just for stopping rules. These are Lemmas 4.5 and 4.7. Lemma 4.6(i) is also needed, to bound the reward rate of the rest of the family by the largest index. The stage-by-stage losses then have to be summed over infinitely many stages, each started at a random time.
markovChainMeasure P x, trajectory stopping times (ℕ → S) → ℕ∞, gittinsIndex, stoppedReward, stoppedTime, stoppedRatio, IsPositiveStoppingTime, BoundedReward. Families use the published MarkovBanditPolicy k T and markovBanditDiscountedValue P r a π x: all bandits share one kernel P and reward r on a common state space, which by §2.9 is no loss of generality (disjoint unions). State spaces are countable with measurable singletons, and rewards are bounded (§2.4).markovBanditDiscountedValue over all MarkovBanditPolicys, a bounded set because rewards are bounded.Prove a block-sensitivity versus sensitivity separation exponent of 2.15.
Recommendation platforms and online retailers choose which products to show a customer, and customers often buy more than one of them in a single visit. Classical choice models such as the multinomial logit (MNL) assume a customer buys at most one product, and under MNL the revenue-maximizing set of products to display is easy to find: it is one of the revenue-ordered sets, so it can be found in linear time. Tulabandhula, Sinha, Karra and Patidar (arXiv:2006.08055, Manufacturing & Service Operations Management, 2023) introduce the BundleMVL-K model, a multivariate logit model in which a customer buys a bundle of up to products, with pairwise interaction terms that capture complementarity and substitution. They estimate it on retail data and design algorithms for choosing the recommendation set.
The first question for any such model is whether the revenue problem stays tractable once purchases of two products are allowed. Theorem 1 of the paper answers it negatively: already for the unconstrained revenue problem is NP-complete. This mission formalizes that theorem and its proof, a reduction from Max-Cut.
The products are . Product has a revenue . A BundleMVL-2 instance assigns a nonnegative weight to every product and to every unordered pair of products, together with a no-purchase weight . (In the paper , and , so , is allowed.) A customer shown the recommendation set buys the nonempty bundle , , with probability , and buys nothing with probability . The expected revenue of is eq. (4),
With the indicator of , the weights , () and the revenues , (), both numerator and denominator are quadratic forms in .
The revenue problem (5) is ; its decision version asks, for a threshold , whether some has . SIMPLE MAX CUT asks, for a simple graph and an integer , whether the nodes of split into two parts with at least edges between them.
NP-completeness is in the sense of Cook's Definition 4: membership in NP and a polynomial-time many-one reduction from every NP language.
The result. Theorem 1 separates the multi-purchase model from its single-purchase counterpart: the revenue-ordered structure that makes MNL assortment optimization linear-time fails once pairs can be bought, and no polynomial-time exact algorithm exists unless P = NP. This is what justifies the paper's design of exact algorithms without running-time guarantees (a noisy binary search over the Compare-Step) and of polynomial-time heuristics, and it places BundleMVL-2 next to other hard assortment problems such as the mixture of two multinomial logits (Rusmevichientong et al. 2010, as cited by the paper) and the MMC model of Benson, Kumar and Tomkins (2018), whose hardness is the paper's Theorem 2.
Formalizing it. The theorem is proved in the paper; no machine-checked proof exists. The paper's argument constructs the instance and asserts the equivalence; it does not argue NP membership or the polynomial running time of the reduction, and it leaves the revenues and threshold free subject to inequalities. A formal proof must fix concrete rational parameters, show that the instance code has polynomial size, and handle malformed inputs. The Compare-Step identity (milestone 2) is also the correctness lemma for the paper's binary-search algorithm.
The mathematics of the reduction is short; the obstacles are the two halves that the paper treats as evident. First, the reduction must be a polynomial-time computable map on strings, in Cook's one-tape Turing-machine model, that sends codes of Max-Cut instances to codes of BundleMVL-2 instances and every other string to a non-member; the rational entries must be computed and written in reduced form. Second, NP membership needs a polynomial-time verifier that evaluates exactly in rational arithmetic, with a bound on the bit size of the sums. An approach that states the reduction as "for every graph there is an instance with the same answer" proves nothing: a fixed yes- or no-instance does that.
The development is in MultiPurchase.Hardness. Conventions committed to:
Fin n, 0-based; in the reduction the hub is 0 : Fin (m+1) and graph node i : Fin m is product i.succ.ℚ). Weights may be zero (), as the paper's own reduction requires (); revenues are positive and . These well-formedness conditions are part of the yes-predicate.BSym, rationals as reduced numerator and denominator.The complexity layer is the published CookPvsNP_defs (Cook's , , , NP-completeness) and ProjSchedTW_Complexity_Encoding (binary codes, cutSize, maxCutLang), with the proved CookPvsNP.polyReducible_trans. Contributions welcome: Turing-machine programs for rational arithmetic and list manipulation (reusable for every NP-membership proof over rational data), the polynomial-time reduction, and a proof of Karp's theorem for SIMPLE MAX CUT, which would discharge the hypothesis.
The price of anarchy (PoA) measures how much selfish routing costs compared with a coordinated optimum: it is the ratio of the cost of a Wardrop equilibrium to the minimum social cost. Worst-case bounds on this ratio are classical (Roughgarden and Tardos, JACM 2002; Correa, Schulz and Stier-Moses, Math. Oper. Res. 2004), and for polynomial costs of degree they grow with . Empirical studies of road traffic, however, observed that the PoA of real networks is close to 1 both in light and in heavy traffic (Youn, Gastner and Jeong, Phys. Rev. Lett. 2008; O'Hare, Connors and Watling, Transp. Res. B 2016). This mission concerns the theorem that explains the heavy-traffic half of that observation for a large class of cost functions.
Timeline:
A non-atomic congestion game has a finite non-empty set of groups, a finite set of resources, and for each group a finite non-empty set of strategies, each a non-empty subset of ; every resource belongs to some strategy (2.1). Each resource carries a cost function , non-negative, non-decreasing and continuous on .
Given a demand vector , a profile splits each over with . The load of a resource is , a strategy costs , and the social cost is . An NE profile uses only cheapest strategies of each group; an SO profile minimizes . The price of anarchy is
The total demand is ; a demand sequence is unbounded if . A game is asymptotically well designed (Definition 2.1) if for every unbounded demand sequence. A function is regularly varying (§1.2) if for every the limit exists and lies in .
If every is regularly varying, then for every demand sequence with and ,
Each resource may have its own regular variation index, and nothing is assumed about how the groups' demands grow relative to each other.
The paper's own route, in order:
The result shows that for every cost class in common use (polynomials with non-negative coefficients, the BPR functions of traffic engineering, logarithmic factors and their products and sums) selfish routing becomes asymptotically efficient as traffic grows, whatever the demand pattern. It replaces the growth conditions of earlier work by a condition on the cost functions alone, and its limit-game and decomposition framework is reusable for other asymptotic questions about equilibria. For BPR costs the paper further shows that every SO profile is an -approximate NE profile (Theorem 4.1); that refinement is not part of this mission.
The theorem is proved in the paper; none of it is machine-checked. The platform has the Wardrop layer (KellyStochasticNetworks_Wardrop) and fixed-demand PoA results, and KellyStochasticNetworks.wardrop_equilibrium_exists proves existence of Wardrop equilibria for globally continuous monotone delays, but nothing about limits of the PoA in the demand. A formalization would produce the first verified heavy-traffic efficiency theorem for congestion games, and check a proof whose central step (Theorem 3.2, Appendix A.3) is a six-page induction.
The natural first idea is to scale all costs by one common factor and pass to a limit game, as for gaugeable sequences. That fails when groups' demands grow at different rates: a single scaling makes the slower groups' contribution vanish or blow up, and the limit game then says nothing about their equilibrium behaviour. The paper therefore scales each class of comparable groups separately, and must show that interactions between classes through shared resources become negligible in the right order. Two further obstacles are specific: the limit cost functions take the value on resources that grow faster than the scaling, so the limit game lives in with the convention ; and the choice of scaling for a class in Appendix A.5 relies on the uniform behaviour of regularly varying functions (, Karamata's characterization, which Mathlib does not have).
The game is a structure with J resources, R strategies and Sd groups, a 0/1 incidence inc and a group map grp; profiles, loads and the Wardrop condition are those of the published definition KellyStochasticNetworks_Wardrop. Conventions fixed in Lean:
Game.Standing.ℝ≥0∞. Condition (L4) is encoded as: an NE profile of the limit game exists, and every NE profile has cost in and is an SO profile of the limit game.EReal.The goal does not mention limit games or decompositions: these appear only in milestones, so the goal cannot be satisfied by an encoding that builds the conclusion into a definition. Regular variation is not encoded as a power law or with a fixed index.
A complete development needs: existence and equal cost of Wardrop equilibria for costs continuous and non-decreasing on ; compactness of profile sets; uniform convergence of monotone functions to a continuous limit; Karamata's characterization theorem for monotone regularly varying functions. The last two are reusable well beyond this mission and are welcome as separate contributions.
Redundancy (sending several copies of a job to different servers and keeping the first one to finish) is a standard way to cut response times in parallel computing systems whose servers have variable speeds: replicated requests in data centres, speculative execution in MapReduce-type frameworks, duplicated queries in distributed storage (Vulimiri et al., CoNEXT 2013; Gardner et al., 2017). The price is extra work: while a job is present, all its copies occupy servers. The first question about such a system is therefore whether redundancy shrinks the set of arrival rates the system can handle.
For i.i.d. exponential copies and First-Come-First-Served service, Gardner et al. (Queueing Systems 2016) and Bonald and Comte (Performance Evaluation 116, 2017) proved that the stability region is , the same as without redundancy. Anton, Ayesta, Jonckheere and Verloop (arXiv:1903.04414, Operations Research 2021) studied other service disciplines and other correlation structures. Their first result, Proposition 3, extends to Processor Sharing and Random Order of Service. Their Example 1 shows that the extension fails for an arbitrary work-conserving discipline.
There are servers , each of capacity , and a redundancy degree . Jobs arrive in a Poisson process of rate . Each job chooses servers uniformly at random and sends one copy to each. The copies of a job have i.i.d. exponential service requirements of mean . When one copy completes, the other copies of that job are removed (cancel-on-complete).
A job's type is its set of servers . The set of types is , with , and . is the number of type- jobs and the number of copies at server . Two service disciplines are considered:
The system is stable when this Markov process is positive recurrent. The load is .
The statement contains no constant beyond the paper's threshold . That threshold cannot be improved: the total service rate is at most , so is necessary for every (p. 5).
The result. Proposition 3 shows that, with i.i.d. copies, replication costs no capacity under PS or ROS. Redundancy can then be used for its latency benefits at any load the non-redundant system can carry. The comparison with the rest of the paper shows what is at stake. With identical copies under PS the region shrinks to (Proposition 11). A priority discipline with i.i.d. copies can be unstable at (Example 1). The PS/ROS result is therefore not a consequence of work conservation.
Formalizing it. The result is proved on paper, and nothing of it is machine-checked. A complete formalization would check every step: a fluid-limit argument for a queue with simultaneous service at several servers, and the transfer from an empty fluid model to positive recurrence of a countable continuous-time chain (Robert 2003, Corollary 9.8, which the paper cites). The paper's argument also has two weak points that a formal proof must settle. Lemma 1 prints , which is false for (see below). The proof of Lemma 2 uses the PS departure rate (1) for ROS as well, where (1) holds only on average (p. 6).
The obvious argument is a Foster–Lyapunov drift for . It fails at finite states. The departure rate from a most-loaded server is at least only through the ratios , which are not monotone along the chain, and under ROS the instantaneous departure rate depends on which jobs happen to be in service, not on alone. The paper therefore passes to fluid limits. The drift (14) has to be identified for the limit of with (a differential inclusion, via Gast and Gaujal), and the negative drift at the maximum has to be turned into stability through a general fluid-stability theorem. For ROS, the averaging "a fraction of server serves type " must be justified at the fluid scale; the paper does not do this in the proof of Lemma 2.
Fin K; types are {c : Finset (Fin K) // c.card = d}; is lam.ProcessingNetworks.Stability definitions. Stability is their PositiveRecurrent: every state recurrent with finite mean return time of the continuous-time chain, holding times included. For PS this ranges over all of , which is one communicating class.A trivializing formalization is ruled out: the state spaces are infinite (a finite-buffer chain is positive recurrent for every ), the rates are the paper's (with an "all copies must finish" rule the threshold would be ), and the only load hypothesis is .
The development needs Poisson processes built from exponential sequences, a strong law of large numbers for them, Arzelà–Ascoli on , a Lipschitz/a.e.-derivative argument for the maximum of finitely many functions, and a fluid-stability criterion for countable continuous-time chains. The last three are reusable well beyond this mission. Contributions of any of these, and of the milestone lemmas, are welcome.
Reinforcement learning with a generative model (a simulator that returns an independent next state for any queried state–action pair) is the standard setting for measuring how many samples are needed to plan in an unknown Markov decision process. The simplest algorithm is model-based planning: query each pair times, build the empirical transition kernel, and plan in the resulting empirical MDP. Azar, Munos and Kappen (2013) showed that total samples suffice and are necessary, but only for . Agarwal, Kakade and Yang (2020) extended the range to . A sample size barrier remained: for larger , no algorithm was known to be minimax optimal with fewer than samples.
Li, Wei, Chi and Chen (arXiv:2005.12900v8, Operations Research, 2024) remove the barrier: the sample size is minimax optimal over the full range . They give two planners. The first (Theorem 1) perturbs the rewards slightly at random. The second, the subject of this mission, leaves the rewards unchanged and instead chooses among near-optimal actions by a randomized but structured rule.
Timeline:
A finite discounted MDP has states , actions , a transition kernel , rewards and a discount factor . A deterministic policy has value , the expected discounted sum of rewards from , and Q-function . The optimal value is and .
The data are independent next states for every pair, and the empirical kernel is . The empirical MDP has optimal functions and .
The conservative planner (Algorithm 2) draws a threshold independently of the data and plays
the smallest-indexed action whose empirical Q-value is within of optimal.
There are universal constants such that, for every MDP as above, every and , with and
with probability at least over the data and ,
The constants are left unspecified, as in the paper.
The paper's own steps, in the order of §6.4:
Theorem 2 shows that the minimax sample size is reachable over the whole range of without altering the reward function: a planner can keep the model it estimated and only change how it breaks near-ties. The guarantee covers both value and Q-function suboptimality, and with a sample size proportional to rather than in the large- regime it allows a coarse but correct policy to be computed from very few samples.
None of these results is formalized. The mission produces a machine-checked account of the decoupling argument for data-dependent policies (absorbing MDPs, nets, stability of the tie-breaking rule), which the companion missions on Theorems 1 and 3 share. The paper omits the last step of the proof of Theorem 2 ("follows from an identical argument as in the proof of Theorem 1"); a formal proof has to supply it, including the analogue of Lemma 5 for , which the paper does not state.
The policy depends on all the data, so the standard concentration argument for a fixed policy (Lemma 1) does not apply to . A union bound over all deterministic policies costs a factor in the sample size, which is exactly the barrier. The leave-one-out construction removes the samples of one pair from the policy; it works only if the policy is stable under the small change of that this causes. The greedy policy is not stable when two actions nearly tie. The conservative rule is stable with high probability over (Lemma 8), but only because it takes the smallest near-optimal action: the set is stable, and a rule that picked an arbitrary member of it would not be.
All declarations live in the namespace BreakingSample.Conservative. The MDP layer reuses the platform's FoundationsML.ReinforcementLearning definitions (IsTransitionKernel, PolicyValue, QFunction); deterministic policies enter as point-mass stochastic policies, and is the maximum over the finite set of maps . Norms are sup norms on finite function types. The order on is an arbitrary linear order on a finite type.
Probability: a data set is a map with the product law, so probabilities of data events are finite sums. The threshold has the uniform law on ; joint probabilities are , with the outer measure for non-measurable sections. "With probability at least " is stated as an upper bound on the probability of the failure event. Because the policy defined by (10) is a predicate on policies, the conclusion is stated for every policy satisfying (10). The universal constants are quantified before all types and parameters. The goal adds , the standing assumption of (3); "the same assumptions of Theorem 1" is formalized with the goal's own constants .
A trivializing formalization is ruled out: is the smallest-index rule of (10), not an arbitrary policy within of optimal, and is random, not fixed.
Infrastructure that a complete development needs and that is reusable: Bellman optimality for finite MDPs with deterministic policies and real rewards, the resolvent identities, Bernstein's inequality for the empirical kernel, the absorbing-MDP construction, and the analogue of Lemma 5 for the conservative policy. Proofs of any milestone, and of the policy-evaluation lemmas, are welcome.
Demand, prices and click-through rates often follow seasonal cycles: weekly, monthly, yearly. A decision maker who repeatedly chooses among options whose expected payoffs repeat in time faces a non-stationary multi-armed bandit. Chen, Wang and Wang (arXiv:2005.08088v4, Operations Research, 2025) study the model in which each arm's mean reward is periodic with its own unknown period. They give a two-stage policy whose regret is , and a lower bound showing that no policy, even one told the periods, does better than . This mission formalizes that lower bound, Theorem 3 of the paper. A companion mission of the same series covers the upper bound.
Lower bounds of this kind fix what is achievable. For the stationary -armed bandit, the minimax regret is of order (Auer, Cesa-Bianchi, Freund and Schapire, 2002; Lattimore and Szepesvári, Bandit Algorithms, 2020, Ch. 15). In the periodic model a learner effectively faces "effective arms" (arm at each phase of its cycle), which suggests the rate . The paper proves the weaker but general bound , which matches the upper bound up to a factor and logarithms.
There are arms and epochs . An instance is a family of mean rewards . If arm is pulled at epoch , the reward is drawn from the Gaussian law , independently of the past given the arm.
A sequence has minimum period if for all and no smaller positive integer has this property.
A policy chooses the arm at epoch at random, from a distribution that depends on the previous arms and rewards. Its expected regret on is display (1) of the paper:
Three classes of instances appear, all with unit-variance Gaussian rewards and means in (Assumption 1):
The proof compares instances through the metric (B-48),
The periods satisfy Assumption 3 with the parameters (7): with and , , and for every .
For every policy there is with
Theorem 3 shows that knowing the periods does not remove the cost of learning them phase by phase: the regret must grow like , not like . Together with the paper's upper bound and the inequality , it shows the two-stage policy is near-optimal when is fixed. The intermediate results are reusable: Lemma 12 is a clean two-point Gaussian lower bound, Lemma 13 is a phase-decomposition argument that applies to any bandit model with known cyclic structure, and facts 1 and 2 give a continuity framework for the regret as a function of the instance.
The result has a published proof. As far as the platform's records show, none of it has been machine-checked. The stationary minimax lower bound of Lattimore and Szepesvári (a different family and constant) exists on the platform, together with the Bretagnolle–Huber inequality, the Gaussian KL divergence and the divergence decomposition, which this mission lists as tools.
The two-point argument of Lemma 12 is standard, but its constant needs , so small horizons must be handled separately. Lemma 13 decomposes the problem into phase problems; making this rigorous means showing that a policy on the periodic problem induces, on each phase, a policy on a stationary problem of horizon , with a history law that factorizes accordingly. The phase-wise instances produced by the decomposition need not have minimum period exactly (all phases may coincide), so a perturbation is needed to land in ; the constant has slack for it. Fact 2 asks for continuity of an integral against the law of a -round adaptive process, uniformly over all policies, which needs a domination argument that does not depend on the policy's kernels.
Fin K, 0-based: the paper's first arm is index . Epochs are 1-based natural numbers; history coordinate is epoch . Values of the means at are ignored.BanditAlgorithm.BanditPolicy K: one Markov kernel per round from the history to the next arm. The history law periodicMeasure reuses the platform's step kernel with the Gaussian bandit of the current epoch's means; with constant means it is BanditAlgorithm.banditMeasure of BanditAlgorithm.gaussianBandit. Lemma 12 is stated with the platform's banditRegret, , which equals (1) for Gaussian arms; the other statements use (1) directly.Welcome contributions: the bridge between periodicMeasure with constant means and banditMeasure, the phase decomposition of the history law, and the uniform continuity of the regret in the means.
The Riemann zeta function governs the distribution of prime numbers, and the size of on the critical line controls error terms throughout analytic number theory. In 1908 Ernst Lindelöf asked how fast can grow as and conjectured that it grows more slowly than every positive power of . This Lindelöf hypothesis is a consequence of the Riemann hypothesis but is strictly weaker in its formulation, and it is open. It has equivalent forms in terms of zeros of (Backlund) and in terms of moments of on the critical line, and it implies bounds for gaps between consecutive primes (Ingham) and the zero-density hypothesis.
Timeline (as recorded in the source, Wikipedia: Lindelöf hypothesis):
is the analytic continuation to of (). The Lindelöf hypothesis states that for every ,
For real the growth exponent is
taken in the extended reals. The source records that for , that (functional equation), and that is convex (Phragmén–Lindelöf). The Lindelöf hypothesis is the statement .
Zeros of are counted with multiplicity (order of vanishing). denotes the number of zeros with and . is the -th prime and .
This is the existing platform theorem lindelof_hypothesis, referenced as the goal. It is equivalent to the big- form above, which is the published definition RiemannVonMangoldt.LindelofHypothesis used by the milestones.
A proof would give, among the consequences listed in the source, prime gaps , the density hypothesis, and bounds for all moments of on the critical line. Each improvement of the exponent feeds into error terms for divisor problems and primes in short intervals.
On the formal side, Mathlib provides , its functional equation and the Phragmén–Lindelöf principle, which are the starting point for the milestones. The unconditional milestones (properties of , the convexity bound, the zero count in unit windows, the second moment) are classical theorems whose proofs can be formalized now; the bounds of Hardy–Littlewood and Bourgain and the density estimates are proved results with long proofs; the goal itself is open.
The convexity argument interpolates between the bound on and its reflection through the functional equation, and it cannot give better than . Every improvement requires cancellation in exponential sums of length about , and current methods (Weyl, van der Corput, Bombieri–Iwaniec, decoupling) save only a fixed power. The hypothesis demands square-root cancellation up to , which is far beyond these methods. Backlund's reformulation shows it is only "slightly" stronger than the known zero count in unit windows, yet that gap has not been closed.
is Mathlib's riemannZeta; the Riemann hypothesis is Mathlib's RiemannHypothesis. The definition file LindelofHypothesis_GrowthAndZeroCounts introduces as an infimum in EReal (so degenerate cases are , never a junk ), zero counts as ℕ∞-valued sums of analyticOrderAt riemannZeta over the zero set (so an infinite count is and upper bounds cannot hold vacuously), and with primes indexed from . Asymptotics are along atTop, with ; by this covers . Where the source writes the base is read as , and density bounds are stated with an implied constant. " is convex" is stated as: is finite and agrees with a convex real function. The source gives no -range for Huxley's estimate; the range of Huxley's theorem is used.
Contributions welcome: the basic theory of , Phragmén–Lindelöf for vertical strips specialized to , Jensen-type zero counting, mean-value theorems for Dirichlet polynomials, and exponential-sum estimates.
Counting solutions of polynomial equations over finite fields is one of the oldest themes of number theory, going back to Gauss's count of points on modulo a prime. In 1949 André Weil proposed a precise description of how these counts behave when the field is enlarged: for a smooth projective variety over , the generating function of its point counts — the zeta function — should be a rational function with integer polynomial factors, satisfy a functional equation, and have its zeros on prescribed "critical lines", in exact analogy with the Riemann hypothesis. These Weil conjectures organized several decades of work in algebraic geometry and directly motivated the construction of étale cohomology.
Timeline (as recorded in the source article, Wikipedia: Weil conjectures):
Let be a finite field with elements and characteristic . Let be a smooth projective variety of dimension over : a scheme with a structure morphism that is smooth of relative dimension , geometrically irreducible, and admits a closed immersion into some projective space over .
For let be the extension of of degree , and let
be the number of -morphisms . The zeta function of is the formal power series
so that .
There exist integer polynomials and multisets of nonzero complex numbers such that
with , , and over for . 2. Functional equation.
where is the Euler characteristic; moreover as multisets. 3. Riemann hypothesis. for all and all .
The historical partial results (Weil's theorem for curves; Dwork's rationality; Grothendieck's rationality and functional equation; Deligne's Riemann hypothesis) and the worked examples of the source (projective line, projective space, elliptic curves, the genus-2 curve over and the Weil polynomials of its Jacobian).
The Weil conjectures give sharp estimates for point counts, and through them bounds on exponential sums (Kloosterman sums, character sums), the Ramanujan–Petersson conjecture for holomorphic modular forms (Deligne 1971), and the hard Lefschetz theorem over finite fields. They are a standard input in analytic number theory, coding theory and cryptography.
All four statements have been proved since 1974. None of them has a machine-checked proof in Lean/Mathlib at present; Mathlib does not yet contain étale cohomology, Jacobians of curves, or the Hasse bound for elliptic curves over finite fields. This mission records faithful, compiling statements so that partial formalizations — the elementary examples, Hasse's theorem, Weil's theorem for curves via Riemann–Roch or Stepanov–Bombieri, Dwork's -adic rationality proof, and eventually the cohomological proofs — can be attached to a common target.
The examples with a cell decomposition (projective spaces, Grassmannians) reduce to counting points in affine spaces. Beyond them, even rationality is a theorem of substance: there is no elementary formula for , and the counts must be shown to satisfy a linear recurrence. The functional equation and the precise shape of the require a cohomology theory with Poincaré duality and a Lefschetz trace formula; the Riemann hypothesis requires, in addition, control of the absolute values of Frobenius eigenvalues, which in Deligne's proof uses Lefschetz pencils, monodromy and the "tensor power trick". For curves, Riemann–Roch and the Hasse–Weil bound (or Stepanov–Bombieri) suffice, but these too are absent from Mathlib.
k : Type with [Field k] [Finite k] [CharP k p], p prime; q = Nat.card k. Schemes live in Scheme.{0}.Proj of graded by total degree; "projective" means a closed immersion into some commuting with the structure maps. "Non-singular of dimension " is SmoothOfRelativeDimension n f; "variety" is GeometricallyIrreducible f.FiniteField.Extension k p m; is PowerSeries.subst of into PowerSeries.exp ℚ.Contributions welcome: the zeta function of projective space, Hasse's theorem, point counts and Weil polynomials for the examples, rationality for curves, and general infrastructure (Riemann–Roch for curves, Jacobians, étale cohomology).
Many service systems must route work to servers whose quality is not known in advance: crowdsourcing platforms matching job types to worker types, wireless schedulers assigning users to channels, call centers routing request classes to agent pools. Learning the unknown service rates is a multi-armed bandit problem, but the cost of a bad decision is not a lost reward. It is a longer queue, and a queue can recover from past mistakes when it empties. Krishnasamy, Sen, Johari and Shakkottai (arXiv:1604.06377v4, Operations Research 2021, doi:10.1287/opre.2020.1995) measure the cost of learning by the queue-regret, the expected excess queue length relative to a genie that knows the rates. Their analysis shows two regimes. Early on the regret grows like a bandit regret. After the system has learned enough to stabilize, queues regenerate and the regret decays. This mission formalizes their lower bound for the second regime: no reasonable learning policy can make the late-stage queue-regret decay faster than .
The lower bound adapts the classical consistency-based bandit lower bounds of Lai and Robbins (1985) and their non-asymptotic, hypothesis-testing form (Bubeck, Perchet and Rigollet 2013) to queue dynamics. The step from counts of suboptimal schedules to queue lengths is specific to queues.
A switch has queues and servers. Time is slotted, . In slot queue receives an arrival , and the link between queue and server offers a service . All of these are independent, and i.i.d. over slots. A problem instance is the pair , with every entry in .
In every slot the scheduler picks a matching : queue is assigned server , and distinct queues get distinct servers. The scheduler knows neither nor . Its decision in slot may use the past schedules, the services observed on the scheduled links in slots , and its own randomness. Queue receives and evolves as
Assumption 1 (unique optimal matching) says that each queue has a unique best server , and that implies . The genie always schedules . Its queues start from the same and see the same arrivals and offered services, with . The queue-regret of queue is .
Write , , , , , . With the Bernoulli divergence , display (2) of the paper defines
Let . For , a policy is -consistent (Definition 2) if for every instance with a unique optimal matching there is a constant with for all and all . Consistency rules out policies tuned to one instance, such as "always schedule a fixed matching", which would have zero regret on that instance and linear regret elsewhere.
For every instance with a unique optimal matching, every law of the initial queue lengths, every and every -consistent policy:
A companion item, Lemma 1 (p. 10), states : queue-regret never exceeds the bandit regret.
Theorem 3 shows that the paper's Q-UCB algorithm, whose late-stage queue-regret is (Theorem 5), is optimal in its dependence on up to polylogarithmic factors. It also separates queue-regret from bandit regret. The bandit regret of a consistent policy grows like , while the queue-regret decays to zero. The cost of learning in a queue is transient, but it cannot vanish faster than . The theorem holds for every initial law of the queues, so it does not depend on the system starting in steady state.
The proof is complete in the source (§9.1, pp. 37–42). As far as we know none of it is machine-checked. A formal development would also give the first formal bandit lower bound in which the consistency class must contain the alternative instances of a change-of-measure argument, here instances with two optimal servers swapped, together with a reusable model of a learning scheduler on a switch.
The obvious route is to bound the regret of each slot by the probability of a suboptimal schedule (Lemma 21), and to bound the number of suboptimal schedules from below by a Lai–Robbins argument. Both steps resist direct proof.
For the first step, and share arrivals and services but are not ordered pathwise, because the policy's services are independent across links. A comparison exists only in distribution.
For the second step, the alternative instance must again satisfy Assumption 1, so a single service rate cannot simply be raised. When server is the best server of another queue , the best servers of and must be swapped, and the divergence decomposition then involves two links.
The final step goes from a cumulative bound to an "infinitely often" bound, and only from a logarithmic lower bound on partial sums. A lower bound on cumulative regret does not give a bound for every large .
Queues and servers are Fin U and Fin K (0-based), with . The hypothesis is added: for the policy and the genie coincide and both sides are zero, and the minimum defining would range over an empty set. Slots are 1-based.
The probability space is canonical: with law . A seed holds one uniform per arrival, one per link and one for the scheduler, and , . A policy maps the history of past schedules and observed services, together with a private uniform seed, to a matching. The only constraint is measurability in the seed, so every randomized history-dependent policy is covered. The law of is arbitrary, as the paper notes after Theorem 3, so Assumption 3 is not used. Assumption 2 (stability under the optimal matching, for every ), which the paper assumes whenever queue-regret is evaluated (p. 8), is a hypothesis of Theorem 3 and of Lemmas 1 and 21. Lemma 19 and Corollary 20 concern schedule counts, which do not depend on the arrival rates.
is a Bochner integral of , which is bounded by . Expected counts are integrals under the seed law, since the schedule never observes arrivals or . and are set to when , where the divergence is . Corollary 20(c)'s becomes the sum over servers outside the range of . Fact 1 is stated for every real sequence: the printed "bounded" is not needed and does not hold in the application. "For infinitely many " is ∃ᶠ t in atTop.
-consistency quantifies over every service matrix in satisfying Assumption 1, and its constant is chosen after the instance. Requiring consistency on the given instance only would make Theorem 3 false, because the genie's own policy has . A constant chosen before the instance would make the hypothesis unsatisfiable.
A complete development needs the canonical seed space and its measurability, a chain rule for the KL divergence of the history laws, the Bretagnolle–Huber inequality (available), and an elementary harmonic-sum estimate. The switch model and the consistency class are reusable for the paper's early-stage lower bound and its upper bound. Proofs of any milestone, and alternative proofs of Lemma 21 that avoid the coupling, are welcome.
The source is the arXiv v4 preprint; the paper's proofs are in its §§8–9.
An indistinguishability obfuscator (iO) is a compiler that scrambles a program so that any two programs computing the same function become computationally indistinguishable after compilation. Garg, Gentry, Halevi, Raykova, Sahai and Waters gave the first candidate construction for all circuits (SIAM J. Comput. 45(3), 2016; conference version FOCS 2013). The candidate later became the starting point of a large body of work on iO, functional encryption and their applications (Sahai–Waters, STOC 2014).
The security of the candidate rests on a new assumption about garbled branching programs (the paper's Assumption 1, "Equivalent Program Indistinguishability"). Appendix C of the paper gives evidence for it: in an idealised generic colored matrix model, where an attacker can only add, scale and multiply the published matrices in an order that respects their colours, the assumption holds unconditionally. That unconditional statement is Theorem 6, and it is the target of this mission. It is an information-theoretic counting statement over finite fields; it involves no machines, no running times and no negligible functions.
Timeline. Barrington (1986) showed that width-5 permutation branching programs compute NC¹. Kilian (1988) randomised such programs by conjugating consecutive matrices with random invertible matrices. Garg, Gentry and Halevi (2013) proposed approximate multilinear maps. The present paper (2013) combined the three, adding a dummy program, bookend vectors and bundling scalars, and analysed the result in the generic colored matrix model. Later work (Barak et al. 2014; Brakerski–Rothblum 2014) proved security in a generic multilinear-map model for modified constructions.
A branching program of length on input bits consists of a map and, for every step and bit , a permutation matrix . On input it outputs iff . A partial assignment fixes the input bits in ; two partial assignments , are functionally equivalent if the program computes the same function of the remaining bits under both.
Fix a prime , and . The randomized program consists of the matrices and , together with bookend vectors , and their primed versions. Here the are uniform invertible matrices over ; is block diagonal with random diagonal entries and the block ; has the block (the "dummy program"). The vector is zero on its first entries and on its next , and their last five entries (and ) are random subject to . The bundling scalars are products of random 's arranged so that their products over each block agree.
In the generic colored matrix model each matrix carries a left and a right colour (: ; : ; : ; : ). A representation oracle holds the database : the bookends, one matrix per step and program for the fixed steps (bit ), and both for the free steps. An adversary sees only handles. It may ask to add two matrices of the same colours, scale one, or multiply two whose colours match. The oracle answers with the handle of an existing record whenever the result equals a stored matrix mod , so equality of matrices is all the adversary learns.
For every prime , branching program , functionally equivalent and adversary receiving at most handles,
for an absolute constant . No value of is fixed, as the paper gives none.
Theorem 6 says that the candidate cannot be broken by any attack that stays within linear algebra over the published matrices in the intended order: partial evaluations, mixing the primal and dummy programs, and mixing inputs that are inconsistent within a block are all detected or harmless. The proof explains the purpose of each design element: the bookend zero patterns kill the random diagonals, and the dummy program and bundling scalars defeat mixed-input attacks.
The theorem has a pen-and-paper proof in the paper and, as far as is known, no machine-checked proof. A formalization would pin down the model exactly: how ⊥ replies, handle reuse and adaptivity behave, and which distribution the bundling scalars follow. These are points the paper leaves informal, and the formal statement records them. The milestones are reusable on their own: the bookend identity and Lemma 2 are pure algebra, and the partial-evaluation bound is a Schwartz–Zippel application to block-diagonal matrix products.
The obvious argument says each new handle is a "new polynomial", and Schwartz–Zippel makes a collision unlikely. That argument fails for bookend products. There, a primal and a dummy evaluation on an accepting input are equal as field elements but different as formal expressions, so a simulator must identify them using only . No other cancellation may survive, including those between products that mix the two values of an input bit within a block, and those on rejected inputs, where the 5-vectors are correlated through . The bundling scalars are products of two uniform field elements, so they vanish with probability about , and the counting has to absorb such degenerate events. Finally, the adversary is adaptive: its later queries depend on earlier equality patterns, so the comparison of the two executions must go through a simulator that does not depend on .
Everything is over ZMod p with [Fact p.Prime]. Probabilities are counting fractions over finite product types; no measure theory is used. Steps, handles and -indices are 0-based. Branching programs output iff the ordered product of permutation matrices is the identity; this is the convention of §3, §4.2 and App. C, not the outputs of Definition 9. The bundling scalars follow the -procedure of p. 42. §4.1 instead says "random subject to the constraint", and over the two distributions differ; the proof analyses the -procedure. A malformed query (unknown handle, mismatched dimensions or colours) is answered ⊥ and leaves the database unchanged. Adversaries have coins uniform on Fin K, make adaptive queries and output a bit. The statistical distance between the views is expressed as the largest acceptance gap over all adversaries; this is equivalent, since every distinguisher of the views is an adversary's final decision. is taken to be , the number of handles a -query adversary receives. The page's in the partial-evaluation case is read as .
Trivializing formalizations are excluded. The constant comes before , so the bound cannot absorb the trivial distance . The oracle compares matrices mod together with dimensions and colours, never formal expressions, and it respects colours. The sampler keeps every random component of §4.1.
The development needs only Mathlib (matrices, GL, MvPolynomial, Schwartz–Zippel). Proofs of the milestones are welcome independently. A formal treatment of the paper's simulator (non-commutative formal polynomials, canonical forms) would be a reusable contribution for other generic-model arguments. The paper's PPT security reductions (Theorems 2–4) are out of scope; the mission formalizes the paper's evidence for Assumption 1, not the obfuscator's security.
In contextual dynamic pricing a seller posts a price for each arriving customer, observes only whether the customer buys, and must learn the demand from these binary responses while selling. The problem arises in e-commerce, insurance and consumer lending, where every customer comes with features (product attributes, customer characteristics) that shift the willingness to pay. Most regret analyses assume either that the noise distribution of the valuation is known up to a parameter, or that it belongs to a parametric family. Luo, Sun and Liu (arXiv:2109.07340, Mathematics of Operations Research, 2024) drop that assumption: the valuation is linear in the features plus a noise with an unknown distribution, and they give a policy, DIP, whose regret is bounded without parametric knowledge of the noise.
This mission formalizes the paper's main upper bound, Theorem 1, together with the chain of lemmas and propositions of its proof. The source is the arXiv v2 preprint (6 March 2023); all proofs are in its Appendix A.
At each period a customer arrives with a covariate , where on . The customer's valuation is , with an unknown parameter , for a known , and market noises drawn i.i.d. from an unknown CDF . The seller posts a price and observes ; the revenue is . The expected revenue of price at linear value is
The clairvoyant price maximizes over and is assumed to lie in . The regret of period is , and .
Two assumptions are made on . Assumption 1: is -Lipschitz. Assumption 2: there is a constant with for all , and .
The DIP policy (Algorithm 4) splits time into episodes of lengths and , , for . In episode it takes an estimate computed from episode (Inner Algorithm A), cuts into equal pieces with midpoints , and runs a UCB rule (Inner Algorithm B) over the candidate prices . The UCB step is analysed as a perturbed linear bandit (PLB): rewards whose parameters satisfy . The algorithm M-LinUCB (Algorithm 5) is optimistic linear UCB with forced exploration of new coordinates.
For every model satisfying the standing assumptions and Assumptions 1–2, every DIP configuration with and , there is such that every run of DIP satisfies, for all ,
where is the number of episodes. The printed statement reads ; the single logarithm is what the proof gives.
In the order of the proof: Lemma 1 (the pricing problem of one episode is a PLB with perturbation ); Lemma 2 (M-LinUCB on that PLB is Inner Algorithm B); Lemmas S1–S5 (weighted averages, the elliptical potential lemma, the shadow parameter, the self-normalized bound, a confidence ellipsoid); Lemma 3 (M-LinUCB on a PLB has regret with high probability); Proposition 4 (the discrete-part regret of one episode); Lemma S6 (the confidence term in form); Proposition 3 (the total regret of one episode, ). Lemmas S2 and S4 are already proved on the platform and are referenced.
The bound separates the cost of learning the unknown noise distribution, up to a logarithm, from the cost of estimating , which enters only through the estimation errors. Any estimator with a known error rate therefore gives an explicit regret rate for DIP: if with , the regret is (p. 19). The rate of the paper's logistic-regression estimator on adaptively collected data is not established; the authors study it by simulation. Lemma 3 is a regret bound for linear bandits with bounded parameter drift that is linear in the drift and otherwise, which the authors note is of independent interest.
The results are proved in the paper, not formalized. The two textbook lemmas the paper quotes, the elliptical potential lemma (S2) and the self-normalized bound (S4), are already proved on the platform; the paper's own results (Lemma 3, the PLB reduction, the episode analysis and Theorem 1) have no machine-checked proof. Faithfulness checks during drafting found printed slips that the formal statements correct and disclose: the unsquared norm in Lemma S2, the finite UCB of an unpulled arm in display (2), and a missing nonemptiness condition for the candidate price sets.
The obvious argument treats each episode as a linear bandit around the central parameter and invokes the standard optimistic regret bound. That fails because the parameter moves with the covariate through the estimation error ; the ridge estimate then tracks no fixed vector, and a general misspecified-bandit bound pays an extra factor in the drift term (Remark 5, p. 21), which destroys the rate once grows with the horizon. A second difficulty is bookkeeping: the per-episode bound must hold uniformly over the random estimate , over the growing discretization , and over the truncated last episode, before the episodes are summed.
Periods are 1-based; arm indices are Fin d, 0-based. Norms are written out: , coordinatewise. The probability space carries a filtration ; covariates and prices are -measurable (adaptive or adversarial covariates and randomized prices are allowed), and has CDF and is independent of . Conditional sub-Gaussianity is Mathlib's HasCondSubgaussianMGF, which needs a standard Borel sample space. Expectations are lower Lebesgue integrals of nonnegative regrets. "With probability at least " means a measurable event of probability at least on which the bound holds.
The standing assumptions are , , on , and maximizing the revenue over . Hypotheses added to the printed statements: (resp. ), which makes every candidate price set nonempty; in Proposition 3; in Lemma 3; finite action sets; a nonempty index set in Lemma S1. Algorithm 3 is read with forced exploration of unpulled arms, as Lemma 2 fixes. Inner Algorithm A is any measurable estimator of the previous episode's data with values in ; the paper's logistic regression with projection is one instance. Algorithms are run predicates that hold for every tie-breaking rule. The constants of Theorem 1, Proposition 3 and Lemma S6 are chosen before the processes, the estimate, and the horizon.
The formalization cannot be satisfied trivially: expectations are integrals of nonnegative quantities, so no non-integrability default applies; the run predicates are satisfiable (a sorry-free check accompanies the drafts); LinUCB is a closed form whose maximality over the confidence ellipsoid is itself a milestone, not a real supremum; and the noise CDF is pinned by .
A complete development needs the PLB analysis (Lemmas S3, S5, 3), which is reusable for any linear bandit with one-sparse actions, and the conditional Hoeffding step for Lemma 1, for which a platform theorem exists. Proofs of any milestone, and reusable lemmas on ridge estimates with diagonal designs, are welcome.
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.
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.
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.