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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Stochastic programs often optimize a decision that changes several random outcomes at once. A reference outcome may be acceptable even when no fixed threshold captures its risk: one wants the new outcome to be preferable under every increasing concave assessment of gains. Second order stochastic dominance expresses that comparison. Dentcheva and Ruszczyński study optimization with several such constraints, each imposed on a nonlinear outcome operator, and show how the constraint multipliers can be represented by utility functions rather than scalar penalties (Dentcheva–Ruszczyński, 2004). Their earlier paper, Optimization with stochastic dominance constraints, treats the pure dominance case without the nonlinear decision map; the present result adds decision dependent outcomes, multiple constraints, and split variables. Ogryczak and Ruszczyński's second performance function supplies the stochastic order used here (Ogryczak–Ruszczyński, 2002).
The utility interpretation matters when a modeler wants a certificate explaining why a solution satisfies a risk preference expressed by dominance. The theorem identifies a concave utility for each binding dominance constraint and an essentially bounded multiplier for each comparison between the split outcome and the outcome produced by the decision. The source is a revised April 2003 author manuscript, later published in Mathematical Programming in 2004; the page and equation numbers below follow that manuscript (author manuscript).
Work on a probability space . An integrable random outcome is a measurable real function with finite expected absolute value; denotes these outcomes, and denotes essentially bounded ones. The decisions lie in a convex set inside a separable locally convex Hausdorff real vector space . An integrable objective outcome and integrable constraint outcomes depend continuously in the norm on . Almost every realized map and is concave and continuous on all of . Fixed integrable outcomes serve as references; the th comparison is required over a bounded interval .
For an outcome , its second performance function is the area below its distribution function:
The split program (11)–(14) chooses and to maximize , subject to for every , and almost surely. Larger outcomes are preferred, so a dominating has the smaller curve. The split variables expose the dominance and decision coupling as separate constraints (manuscript, pp. 3–4).
The utility cone consists of concave nondecreasing functions that vanish for and are affine with a nonnegative slope for . Given in these cones and , the Lagrangian is
Uniform dominance means one decision makes every dominance inequality uniformly strict on its interval: for each , has a positive lower bound over (Definition 1, p. 7).
Theorem 2 is the goal. Under uniform dominance, every optimum of the split program admits and nonnegative with
Conversely, an attained Lagrangian maximum satisfying the split constraints and these complementarity equations is a primal optimum. The milestone list follows the source's measure multiplier equations (23)–(24), the measure to utility identity (25), Theorem 1's expected concave subgradient characterization, and the converse's weak duality inequality (manuscript, pp. 5, 8–10).
The result gives a concrete optimality certificate in a program whose constraints compare entire outcome distributions. Each utility multiplier represents the active part of one dominance constraint. Each accounts for the almost sure inequality linking a split outcome to the decision. The equalities show exactly where those constraints are complementary, while the Lagrangian maximum compares the proposed solution with all integrable split outcomes. The paper derives a dual problem from the same Lagrangian in its following section (manuscript, p. 11).
The mathematical theorem is proved in the paper. This mission seeks a machine checked version of its definitions, measure identity, subgradient statement, and both directions of Theorem 2. The published second performance definition is reused as a reference; the nonlinear split program and its utility and measure Lagrangians require a development specific to this paper. The 2003 pure dominance mission contains related local drafts, but those items are not published and cannot currently be imported as platform theorems.
The dominance inequality contains a continuum of thresholds for each outcome. A scalar multiplier at one threshold cannot capture the whole constraint, while the dual object for continuous functions on is a measure. The split inequality lives in , where the nonnegative cone has empty interior, so an ordinary interior point argument applied to all constraints at once does not match the paper's setting. The source also needs a subgradient of expected concave utility represented by an almost surely selected, essentially bounded random vector; the conclusion is stronger than merely knowing that the expected objective has a deterministic supporting functional (manuscript, pp. 5–9).
The Lean development keeps the general separable locally convex Hausdorff decision space, the convex set , and a finite index type for the dominance constraints. Operators are function representatives with explicit integrability, continuity in , and samplewise concavity and continuity. Almost sure comparisons use the probability measure ; the null set for each realization condition precedes the quantifier over decisions. Split outcomes range only over integrable functions, and utility multipliers range over the exact cone . The condition includes almost sure strong measurability and essential boundedness. Maxima in Theorems 1 and 2 are attained maxima, expressed by membership and comparison against every competitor, never a real supremum with a default value.
The source prints a strictly positive affine slope in its definition of , but immediately calls this class a cone and later uses the zero measure. The formalization uses ; with , Theorem 2 is false for a slack dominance constraint. Uniform dominance is expressed as a positive lower bound rather than a real infimum. The measure milestone uses finite nonnegative measures supported on closed intervals, including endpoint atoms. These conditions exclude default zero integrals, an empty interval disguised by an infimum, and a vacuous utility class. Contributions to the measure to utility correspondence, integration identities, and expected concave subgradient infrastructure can be reused beyond this program.
Regularized least squares (RLS) in a reproducing kernel Hilbert space is a basic estimator of nonparametric regression and of kernel-based learning. Its learning rate is the speed at which the expected excess risk goes to zero as the sample size grows. A rate is useful only if it is known to be optimal, and optimality is a lower-bound statement about all learning algorithms.
Caponnetto and De Vito (Found. Comput. Math. 7 (2007)) prove two kinds of lower bound. The first is a minimax lower rate (their Theorem 2): for every algorithm and every , some distribution in the prior is hard. Their Section 2 (p. 6) points out a weakness of this notion: the bad distribution may change with . A practitioner, however, faces one fixed unknown distribution and asks how the error decreases as data accumulate. The individual lower rate answers that question. It asks for a single distribution, chosen against the algorithm but not depending on , on which the expected excess risk stays above along infinitely many .
The notion comes from nonparametric regression. Györfi, Kohler, Krzyżak and Walk (A Distribution-Free Theory of Nonparametric Regression, Springer 2002, §3, Theorem 3.3) proved individual lower rates for classes of smooth regression functions. Theorem 3 of Caponnetto–De Vito carries the result to vector-valued RKHS with the spectral priors . Theorem 1 of the same paper shows that these priors are learned by RLS at rate .
The input space is Polish. The output space is a real Hilbert space of finite dimension . The hypothesis space is a separable real Hilbert space of functions in which evaluation is continuous, so that for bounded operators . Hypothesis 1 asks that be measurable and that for every .
A distribution on has marginal and conditional distributions . The risk of is
Hypothesis 2 asks for square-integrable outputs, a minimizer of over , and a Bernstein-type moment bound on the noise with constants .
The operator on satisfies . Its nonzero eigenvalues are , with orthonormal eigenvectors .
For positive constants and parameters , , the prior (Definition 1) is the set of probability measures satisfying three conditions:
A learning algorithm is a sequence of maps , and is its output on a sample of size drawn from .
For every ,
Equivalently, there is such that every algorithm admits one with expected excess risk at least for infinitely many . The constant may depend on the prior and on , but not on the algorithm.
with and . Every such distribution belongs to the prior. 3. (63) (p. 27). Under these distributions, with . 4. (68) (p. 28, corrected). for , where . 5. (67) (pp. 28–30). Averaged over independent fair signs , the expected number of sign errors over , weighted by , is at least .
Theorem 3 shows that no algorithm, RLS included, converges on every fixed distribution of faster than , for any . For this exponent is arbitrarily close to the exponent of the upper rate of Theorem 1, so RLS with the regularization parameter of Theorem 1 is near-optimal even in the individual sense. The paper notes (p. 6) that full individual optimality would still need an upper rate in expectation or an individual lower rate in probability; that question is outside this mission.
The theorem is proved on paper and has been cited widely. To our knowledge no part of it has been machine-checked. A formalization would produce:
A minimax argument picks a hard distribution for each , and that is not allowed here: the distribution must be fixed before varies. The obvious repair, taking the worst distribution for one and keeping it, fails, because a distribution that is hard at sample size can be easy at sample size .
What has to be shown is a lower bound that holds for one distribution simultaneously along infinitely many sample sizes. Bounds that hold separately at each , with a distribution that may depend on , do not combine into such a bound.
A second difficulty arises in any reduction to a coordinatewise testing problem: each observation depends on all spectral coordinates of the regression function at once, so testing one coordinate is not literally the problem of Proposition 7.
is Mathlib's RKHS ℝ H X Y, with = RKHS.kerFun H x and finite-dimensional. The paper's is written Sig.
t (n-1).InPrior encodes , including "probability measure".lintegrals of nonnegative quantities, and samples are Fin ℓ → X × Y under the product measure.stdGaussian Y.Two parts of the print are corrected, and both corrections are stated in the items.
The goal mentions none of , , or . It is the lower rate (3) for the full prior with . A formalization that fixed the algorithm, let the distribution depend on , or let the constant depend on the algorithm would prove a different, weaker statement.
A complete development needs:
Reusable pieces include Proposition 7, the Bayes-error monotonicity argument on p. 29, and the identification of the risk minimizer of a Gaussian-noise model. Contributions on any milestone are welcome, as are proofs of the measurability facts (elements of are measurable under Hypothesis 1).
Regularized least squares (RLS), also called kernel ridge regression, is one of the standard estimators of statistical learning: given a sample of input–output pairs, it fits a function from a reproducing kernel Hilbert space by minimizing the empirical squared error plus a multiple of the squared norm. Caponnetto and De Vito (FoCM 2007) proved that, over a class of distributions described by two parameters — the decay of the eigenvalues of the kernel's covariance operator and the smoothness of the regression function relative to it — RLS with a well-chosen regularization parameter converges at the rate in the sample size (their Theorem 1). An upper rate on its own does not say whether another method could do better. This mission formalizes the matching minimax lower rate (their Theorem 2): when the output space is finite dimensional, no learning algorithm whatsoever converges faster than uniformly over the class. Together the two theorems say that RLS is rate-optimal, and they are the reference point for later work on spectral regularization, early stopping and distributed kernel methods.
The paper's lower bound adapts the minimax analysis of DeVore, Kerkyacharian, Picard and Temlyakov (FoCM 2006) to the vector-valued RKHS setting.
Inputs lie in a Polish space and outputs in a real Hilbert space of finite dimension . The hypothesis space is a separable Hilbert space of functions in which evaluation is continuous; is the adjoint of evaluation at , so . Hypothesis 1 asks that be measurable and that for every .
A distribution on has risk . Hypothesis 2 asks that , that the risk has a minimizer (taken of minimal norm), and that the noise satisfies a Bernstein moment condition with constants . With the marginal of , the operator on has the quadratic form and a spectral decomposition .
The prior (Definition 1, with fixed positive , and ) is the set of probability measures satisfying Hypothesis 2 with such that
the infimum over all learning algorithms . The constant in front of the rate is left free, so the goal asserts only the exponent.
The result. Theorem 2 shows that the exponent attained by RLS cannot be improved by any estimator over when ; for RLS is optimal up to a logarithmic factor. It separates what is a property of the problem class from what is a property of the algorithm: improvements to kernel methods must change the class (stronger assumptions) rather than the rate. The construction — a packing of the source class measured in the -norm, combined with a KL bound for an explicit noise model — is the template reused in many later lower bounds for kernel and inverse-problem estimators.
Formalizing it. The result has been proved since 2007; no machine-checked version exists. A formal proof needs the information-theoretic lower-bound machinery (a Fano-type inequality for many hypotheses), a Varshamov–Gilbert-type packing of the Hamming cube, KL divergence between explicit mixtures, and the spectral description of the covariance operator of a vector-valued RKHS. Each of these is reusable well beyond this paper. The mission also makes precise the paper's implicit conventions (see below), which a pen-and-paper reader fills in silently.
The upper half of the argument is not the hard part; the hard part is that the lower bound is uniform over all measurable algorithms, which no direct computation reaches. The step that does not follow from the paper alone is Theorem 5: its proof invokes Lemma 3.3 and Eq. 3.12 of DeVore et al., a Fano-type inequality bounding the probability of correct identification among hypotheses with pairwise KL divergence at most a given level. That lemma is not stated in the paper and is not in Mathlib; it must be formalized. A second obstacle is the packing (Proposition 6), whose proof is a probabilistic union bound with Hoeffding's inequality. A naive attempt to prove Theorem 2 by exhibiting a single bad distribution fails: for any fixed some algorithm (the constant one returning ) has zero excess risk, so the bad distribution must depend on the algorithm, and the order of quantifiers is essential.
Mathlib's RKHS ℝ H X Y provides the function space with continuous evaluation, RKHS.kerFun is , and InformationTheory.klDiv is the Kullback–Leibler information. The operator is never built as an operator-valued Bochner integral: it is recorded through its quadratic form and an eigen-system indexed by from (the paper's is t (n-1)). The trace in Hypothesis 1 is a series over a Hilbert basis of ; the conditional law in Hypothesis 2 is Measure.condKernel, and the moment integral there is a lintegral. in the goal is .
Conventions and added hypotheses, each implicit on the page:
The goal is the –– unfolding of the limit and mentions neither , the KL bound nor the packing, so it cannot be discharged by any of the milestones' constructions in isolation; the distribution is chosen after the algorithm, never before it.
Contributions welcome: a general Fano/DeVore-type lemma for finitely many hypotheses, the Varshamov–Gilbert bound, KL ≤ χ² for finite mixtures, and lemmas relating covForm to the excess risk.
Regularized least squares (RLS, also called kernel ridge regression or Tikhonov regularization) is the simplest learning algorithm built on a reproducing kernel Hilbert space. Given examples drawn independently from an unknown distribution , it returns the function in a hypothesis space that minimizes the empirical squared error plus times the squared norm. It is used in regression, in multi-task learning with vector-valued outputs, and as the reference case for spectral regularization methods.
The basic statistical question is how fast the excess risk of the RLS estimator goes to zero as grows, and how to choose to get that speed. Caponnetto and De Vito (FoCM 2007) answered it for a family of priors described by two numbers: the decay rate of the eigenvalues of the covariance operator of the input distribution and the regularity of the target function. Their Theorem 1 gives the upper rate ; Theorems 2 and 3 show that no algorithm does better when the output space is finite dimensional. This mission formalizes the upper rate.
Timeline. Cucker and Smale (2002) and De Vito, Caponnetto and Rosasco (2005) gave rates for RLS that did not depend on the eigenvalue decay of . Zhang (2005) introduced the effective dimension as the complexity measure. Caponnetto and De Vito (authors' copy dated 2006, published 2007) combined it with a source condition to obtain rates that are optimal over , for vector-valued outputs. Steinwart, Hush and Scovel (2009) and Fischer and Steinwart (2020) later extended the analysis to other norms and to .
The input space is a Polish space and the output space is a real separable Hilbert space. The hypothesis space is a real separable Hilbert space of functions in which evaluation at each point is continuous. For , is the adjoint of evaluation at , so . Hypothesis 1 adds a measurability condition and a uniform trace bound .
A distribution on has marginal and conditional laws . The expected risk of is . Hypothesis 2 asks that , that attains its infimum over at some (the minimizer of minimal norm is used), and that the noise satisfies a Bernstein moment condition with constants .
The covariance operator is positive and trace class, with and eigen-decomposition , . The prior , for and , consists of the satisfying Hypothesis 2, with for some (source condition), and with for all (eigenvalue decay).
The RLS estimator minimizes over .
With and for , and for ,
The statement fixes the rate, not the constants: the threshold absorbs every constant of the prior.
provided and , where , , and . 4. Proposition 3: on , , and .
The result. Theorem 1 says that RLS with chosen from achieves the rate uniformly over the prior, and the companion lower bounds show this is the minimax rate for and finite-dimensional . The rate interpolates between the parametric rate (fast eigenvalue decay, smooth target) and slower nonparametric rates, and it identifies the effective dimension, rather than the dimension of , as the quantity that governs complexity. Theorem 4 is a non-asymptotic bound of independent use; it is the template for later analyses of spectral regularization, gradient descent with early stopping, and random-feature approximations of kernel methods.
The formalization. The result is proved on paper; no machine-checked proof of a kernel ridge regression rate is known to exist. A formal development requires a Bernstein inequality in Hilbert spaces, spectral calculus for a trace-class operator defined from a measure, and the operator-perturbation argument of Theorem 4. Two printed constants are corrected here: Theorem 4's proof yields , not , and Proposition 3's bound on has in place of . The paper also states Theorem 1 for ; that branch fails for and is not posed.
The obvious argument bounds by uniform concentration of around and multiplies by . That gives a variance term that ignores the eigenvalue decay of , and hence a rate that does not improve with . The optimal rate needs the variance measured through , which requires controlling in operator norm with high probability. This in turn needs concentration of in Hilbert–Schmidt norm, and the condition under which the empirical operator is close enough to . The noise is unbounded, so only the moment condition (9) is available, and the concentration step must use moment bounds rather than boundedness.
is Mathlib's RKHS ℝ H X Y, and is RKHS.kerFun H x. The trace in Hypothesis 1 is computed in a fixed Hilbert basis of . is the first marginal and is condKernel. The operator is not built as an operator-valued integral. It enters through its quadratic form and through an eigen-system , indexed from , so (17) reads . The effective dimension is . Samples are Fin ℓ → X × Y under the product measure, and probabilities of events are outer measures. "With probability at least " is stated as "the bad event has measure at most ". The noise condition and the moments of Proposition 2 are integrals of nonnegative functions with values in .
The hypotheses the paper uses but does not display are added: positivity of , and integrability of the random variable in Proposition 2. The RLS estimator of the goal is any family of minimizers of (18) for ; at and the parameter is degenerate. The goal quantifies uniformly: is chosen before , and the estimator is fixed before . The goal must not be replaced by a statement about or by Theorem 4's event: it is the uniform rate for the estimator itself.
Reusable infrastructure: Hilbert-space Bernstein inequalities (Proposition 2 alone is a valuable target), spectral calculus for compact positive operators given by a quadratic form, and the representer/normal equation for vector-valued RLS. Contributions of proofs for any milestone, and of supporting lemmas about trace-class operators and effective dimension, are welcome.
Many statistical parameters are defined implicitly, as the root of an estimating equation : a mean, a quantile, a regression coefficient, the minimizer of an expected loss. Owen's empirical likelihood builds confidence regions for such parameters by asking how far the empirical distribution of the data must be reweighted before the equation holds, and the profile of that distance has a chi-squared limit (Owen, Empirical Likelihood, 2001).
Blanchet, Kang and Murthy replace reweighting by transport: they measure how much the data must be moved, in the sense of optimal transport, before the equation holds. The resulting Robust Wasserstein Profile (RWP) function plays the role of the empirical-likelihood profile, and its value at the true parameter is exactly the smallest radius of a Wasserstein ball around the data that contains a distribution satisfying the estimating equation. Its asymptotic law is therefore what is needed to choose the radius of Wasserstein distributionally robust estimators, such as the square-root LASSO and regularized logistic regression, in a data-driven way (arXiv:1610.05627, §§1, 3, 4). This mission formalizes the paper's main limit theorem, Theorem 3.
Let be a cost. The optimal transport cost between probability laws and on is
the infimum over all joint laws of a pair with the given marginals (Eq. (7)). In this mission with and , and denotes the conjugate exponent, .
Let be an estimating function, and let be i.i.d. random vectors in with . With the empirical distribution of , the RWP function is
Write for the Jacobian of , and for the norm of the row vector , . The assumptions are:
A sequence is asymptotically stochastically bounded by , written , if for every continuous, bounded, non-decreasing .
Let . Under A1)–A4),
where for
and for
The formal goal also asserts that is finite and measurable and that both maxima are attained; these are facts the paper's statement presupposes.
Theorem 3 gives the rate at which the RWP function at the true parameter vanishes and an explicit random variable bounding its rescaled limit. The -quantile of yields a radius for which the Wasserstein ball around contains, with asymptotic probability at least , a law satisfying the estimating equation at (§3.1, (19)); this is the paper's prescription for the regularization parameter of square-root LASSO and of regularized logistic regression (§4). Example 3 (p. 14) shows the bound is sharp for the mean: . Matching lower bounds (Propositions 4 and 5) need further assumptions and are not part of this mission.
The result is proved in the paper; no machine-checked version of it, or of any RWP or empirical-likelihood limit theorem, is known to exist. A formalization would check the duality argument for the problem of moments, the passage from the dual representation to a localized maximization, and the continuous-mapping step, and would produce reusable statements: strong duality for transport-cost moment problems, the closed form of the conjugate of , and a uniform law of large numbers over a compact parameter set.
The obvious route is to apply the central limit theorem to and pass to the limit inside the dual representation (31). This fails as stated, for two reasons. First, the supremum in (31) is over all of , and convergence of the objective on compact sets does not control the supremum; Lemma 2 is needed, and it uses A4) through a lower bound on that is uniform over the unit sphere. Second, the penalty involves the derivative of at points that are not localized, with no moment assumption on ; the proof must truncate to and to a specific near-optimal , and then remove the truncation. The case differs: the inner supremum is or , and the limit becomes a maximization over a constraint set.
Vectors are Fin k → ℝ; and norms are Mathlib's PiLp norms, so is allowed, with and p.HolderConjugate q. The samples are a sequence W : ℕ → Ω → (Fin m → ℝ), mutually independent (iIndepFun) and identically distributed with W 0, which plays the role of ; uses through the published empiricalDistribution. Distinct samples are not assumed in Theorem 3; Proposition 3 and (31) keep the §3.1 assumption of distinct samples. Transport costs and are -valued lower Lebesgue integrals and infima; is computed in the extended reals with the moment in . 's law is multivariateGaussian 0 Cov on EuclideanSpace ℝ (Fin r).
The goal is a conjunction: finiteness of for , its a.e.-measurability, attainment of the maxima in , and the limsup bound. Without the first three, a real-valued formalization could hold for the wrong reason (an infinite converted to , a non-measurable integrand integrated to , or an unbounded supremum replaced by ); the conjunction rules this out.
Readings of the page recorded in the items: A1) says while (17) and the proof of Lemma 2 use , and is used; Proposition 3 is stated for a cost that is finite everywhere, the setting of §3, because for a cost that is infinite on part of the space the interior condition on does not imply the Slater condition used in App. B; Lemmas 2 and 3 state the standing assumptions A1), A3) and i.i.d. sampling that their statements leave implicit. The localized weak limit (45) is not a milestone: its penalty depends on a -dependent near-optimal direction that is not stated precisely enough on the page.
Needed infrastructure: the multivariate central limit theorem (Mathlib has the real-valued one), Hölder duality for PiLp norms, a strong-duality theorem for moment problems (Proposition 7, quoted from Isii and Karlin–Studden), and a uniform law of large numbers. The duality results and the conjugate formula (42) are reusable beyond this mission. Proofs of any milestone, and lemmas that serve them, are welcome.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's earlier values ( down to ) came from Schnirelmann's method with every constant written out, using only weak Chebyshev lower bounds for . This entry keeps the same machinery as the entry but feeds it Chebyshev's sharper lower bound with , obtained from the weights at . No zeta-zero input is used.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in.
Let and . We show , then conclude with Mann's theorem as in the entry. Write for the scale.
PrimeNumberTheoremAnd library with explicit bounds for and ). Since , this gives . On its own it covers through .The argument stays elementary: no prime number theorem and no zeros of or -functions. New reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Already proved on the platform: Schnir.sieve_ineq, Schnir.G_lower, Schnir.basis_of_density. Mathlib supplies the Chebyshev function with and the Λ² sieve framework.
PrimeNumberTheoremAnd (PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean).Controlled Markov processes with the average cost criterion model systems that run indefinitely, such as queues, inventories, maintenance and communication networks, where only the long-run cost per unit time matters. The standard route to an optimal stationary policy goes through the average cost optimality equation (ACOE). The ACOE is usually obtained by the vanishing discount method: solve the discounted problem for each discount factor and let . The method works only when the differences of discounted values stay bounded as . Conditions that guarantee this are therefore central in the survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993), §5).
This mission formalizes one such condition, due to Ross: if the mean return time to a fixed state is bounded uniformly over all stationary policies and initial states, the differential discounted value functions are bounded uniformly in the discount factor and the state.
Timeline. Derman (Management Sci. 9 (1962); survey reference [38]) and Derman–Veinott (Ann. Math. Statist. 38 (1967); survey reference [43]) introduced recurrence conditions of this kind for countable-state processes. Ross (Ann. Math. Statist. 39 (1968), survey reference [147]; Introduction to Stochastic Dynamic Programming, 1983, survey reference [150]) showed, for bounded costs, that under a Derman–Veinott type recurrence condition is bounded uniformly in , and obtained a bounded solution of the ACOE by letting (survey, pp. 291 and 301). Later work replaced the condition with weaker ones (survey Assumptions 5.1–5.3) and with Sennott's conditions (survey Theorem 5.9).
The state space is . In each state , an action is chosen from a nonempty compact set of a metric space . The one-stage cost is nonnegative and the next state is drawn from the transition law . For fixed , the maps and are continuous on . A policy chooses the action at time at random, given the whole history, and must choose from . A stationary deterministic policy is a map with . and denote the law and the expectation of the controlled process started at .
For a discount factor , the discounted cost and the optimal discounted cost are
A policy is -discount optimal if for all . The differential discounted value function is
measured relative to the fixed state . The return time to is
with if the process never returns. Throughout, as in §5.1 of the survey, the cost is bounded: on admissible pairs.
If there is a constant with
then there is a constant such that
This is the theorem as printed: it asserts only uniform boundedness and fixes no constant.
The result. Theorem 5.3 verifies the hypothesis of the vanishing discount theorem (Theorem 5.2 of the survey) from a condition on the uncontrolled dynamics of stationary policies. Theorem 5.2 then gives a bounded solution of the ACOE, an average optimal stationary policy, and the limit . Mean return times can often be estimated directly, for instance through Foster–Lyapunov drift arguments on queues, which makes (5.7) checkable in applications. The explicit bound also controls the span of the relative value function.
Formalizing it. The result is proved in the literature; to our knowledge it has not been machine-checked. A formal proof needs discounted dynamic programming on a countable state space with compact action sets, the existence of optimal stationary policies (Theorem 2.1 (iii), which the survey cites without proof), and the strong Markov property of the controlled chain at a return time. All of these are reusable well beyond this mission.
The estimates (5.9) and (5.10) are elementary once (5.8) and the existence of are available. The weight lies elsewhere.
ℕ; the action space is a metric space with its Borel -algebra. The model CMP carries compact nonempty , a nonnegative measurable cost, and continuity of and on , the standing assumptions of §5.Kernel.trajMeasure. is an infimum over all such policies, not over Markov or stationary policies only.trajMeasure, and return-time estimates.Most stochastic programs of practical size, such as two-stage recourse models in energy, finance or supply-chain planning, cannot be solved exactly: the expectation in the objective is a high-dimensional integral. The standard remedy is sample average approximation (SAA): replace the expectation by an average over a Monte Carlo sample and solve the resulting deterministic problem. This produces a candidate solution but says nothing about how good it is. A decision maker needs a statistical certificate: an interval that contains the candidate's optimality gap with a prescribed probability.
Mak, Morton and Wood (Oper. Res. Lett. 24, 1999) built such a certificate from independent SAA replications, which requires solving at least 30 optimization problems. Bayraksan and Morton (preprint January 2005, published in Math. Program. 108, 2006) showed that a single replication suffices asymptotically, and gave two variants that use two replications. This mission formalizes their validity theorems.
Let be a random vector with distribution on a measurable space , let be a set of decisions, and let be a cost. The stochastic program is
Its optimal set is , and the optimality gap of a candidate is . The paper assumes throughout:
Let be i.i.d. copies of , and write . The SAA problem is (SP), with an optimal solution . The gap estimator is (display (2)), and the sample variance of the differences is
with population counterpart . Finally is defined by .
The single replication procedure (SRP) solves (SP) once and reports the one-sided interval (display (5)). The I2RP takes the variance from a second, independent sample and its own minimizer . The A2RP runs the SRP on both halves of a sample of size , averages the gaps and the variances as in (10), and scales by .
Under (A1)–(A3), for and , provided or (see Formalization scope),
The milestones follow the paper's own proof:
Theorem 3 (p. 9) and Theorem 4 (p. 10) are the same coverage statement for the I2RP and the A2RP. Three further statements are included: the negative bias of display (1), the pathwise bound for , and the consistency of the pooled variance.
Theorem 2 makes a single SAA solve enough for an asymptotically valid upper confidence bound on the optimality gap. It cuts the computational cost of the multiple-replication procedure by a factor of about thirty, and it needs no asymptotic normality of , which typically fails when (SP) has several optimal solutions. The two-replication variants lessen the small-sample under-coverage of the SRP. The single- and two-replication estimators were later reused in sequential sampling procedures for SAA.
As far as is known, none of these results has been machine-checked. A complete formalization needs a uniform strong law of large numbers over a compact parameter set, which is a reusable result in its own right, together with the SAA consistency theory and a central-limit argument for a statistic that is not itself asymptotically normal.
The obvious route would be to show that is asymptotically normal and apply a standard confidence-interval argument. That fails: is a minimum of sample averages, and when is not a singleton its limit law is the law of a minimum of correlated Gaussians, not a Gaussian. The paper's argument has to bound the coverage from below without that limit law. It also needs to control the sample variance at a random, non-convergent minimizer , which only accumulates on . The uniform strong law (Rubinstein–Shapiro, Lemma A1) on which both consistency statements rest is not in Mathlib.
The Lean development uses these conventions:
EuclideanSpace ℝ (Fin d). The paper's is renamed because is the sample size.ξ : ℕ → Ω → Ξ on a probability space , 0-based: is ξ (i-1). The second sample of Theorems 3–4 is ξ n, …, ξ (2n-1), exactly as printed, and the A2RP's "random" partition is this fixed one, which has the same joint law.ℝ≥0∞-valued, so the liminf in (6) is genuine. Proposition 1 (iii) is stated in its equivalent -form, which avoids real liminf/limsup junk values.cdf (gaussianReal 0 1) zα = 1 - α.Standing assumptions and pins. Every goal-level statement carries (A1)–(A3) and the i.i.d. hypothesis. Three hypotheses are made explicit that the paper leaves implicit:
At the factors , and evaluate to Lean's ; every coverage statement is a liminf and ignores them.
Several encodings would trivialize the statement, and all are ruled out. The minimizer must minimize the SAA problem of its own sample: a free , or one fitted to the other sample, would change the theorem. The second sample must not be replaced by an independent sequence. The quantile must not be pinned through an sInf. Positivity of is a hypothesis only of the -bound, as on p. 8.
One correction of the paper. Theorems 2 and 4 are stated for every , but for the paper's argument (replace by ) needs , and without it both statements are false: for , , , and , the SRP coverage tends to about and the A2RP coverage to , both below . The Lean goal and Theorem 4 therefore carry the hypothesis ", or for some ". Theorem 3 is stated as printed.
Contributions are welcome at every level. The most reusable one is the uniform strong law of large numbers for Carathéodory integrands on a compact set with an integrable envelope, which also serves other SAA consistency results.
Large call centers route several types of customers to a common pool of agents. When the pool is large and highly utilized, the relevant asymptotic regime is the quality-and-efficiency-driven (QED) or Halfin–Whitt regime (Halfin & Whitt 1981). The number of servers grows while the offered load stays within of . Waiting is then neither negligible nor overwhelming (Gans, Koole & Mandelbaum 2003).
Which class should a freed agent serve next? Exact optimization of a multi-class many-server queue with abandonment is intractable. The standard route is to solve a limiting diffusion control problem and translate its optimal control back into a policy for the queue. Atar, Mandelbaum and Reiman (Ann. Appl. Probab. 2004) carried this out for customer classes, exponential service and abandonment, general renewal arrivals and general convex-type holding costs. They proved that the translated policy is asymptotically optimal. This mission formalizes that result for the preemptive policy.
Context:
There are customer classes and identical servers.
Primitives.
State. is the number of class- customers in the system, the number in service and the number waiting. The dynamics are
Policies.
Scaling and cost. In the QED scaling with . With the centred processes are , and . The cost is
The limiting control problem. It controls
where the control takes values in the simplex and is a -dimensional Brownian motion. The data are and . Its value is the infimum of , with .
HJB equation and the proposed policy. The HJB equation is with . Let be a measurable selection of its minimizers. The proposed preemptive policy (P-SCP) sets the queue vector to , an integer rounding, and falls back to a static priority rule when that is infeasible.
For a solution of the HJB equation, a measurable minimizer selection , and initial states with :
This holds for every sequence of work-conserving admissible SCPs, and the left-hand limit exists and is finite. No constants are hard-coded.
The milestones follow the proof:
The result. Theorem 2(i) justifies using the diffusion control problem as a design tool for multi-class many-server systems. The policy is explicit given , and it is optimal in the limit against all non-anticipating work-conserving policies, including those that use the full history and the time of the next arrival. The proof also identifies the limit cost with .
Formalizing it. The result is proved on paper, with some steps (Proposition 1, the principle of optimality, the time-change and martingale limit theorems) given as sketches or citations. No part of it is machine-checked. A formalization requires:
Each of these is reusable well beyond this paper.
The obvious argument would show that converges to the controlled diffusion and pass the costs to the limit. This fails for two reasons:
The proof instead compares every policy with the HJB solution through Itô's formula on the prelimit processes. This needs:
Existence of a classical HJB solution on all of , with only Hölder-continuous costs and polynomial growth, rests on a bounded-domain existence theorem for fully nonlinear elliptic equations.
The Lean development commits to the following conventions.
Fin k with ; paper class is index , so "class " (highest priority, rounding remainder of ) is the last index. Vectors are Fin k → ℝ and is the paper's norm; the paper's on vectors is read the same way.Ω : Type (universe 0). "Complete filtered probability space" means complete with all null sets in . Brownian motion is Mathlib's IsBrownianReal per coordinate, with independence and the -Brownian property stated explicitly. is the infimum over systems and their controlled processes.CouplingConverges of the published BellWilliams2001.ThresholdPolicy.Paths; convergence to a deterministic limit is UocInProb.The goal hypothesizes and with the pointwise identity for all . An arbitrary "optimal Markov control policy" may differ from a minimizer selection on the Lebesgue-null lattice where lives, and that formalization would make the goal false. Restricting the comparators to feedback, Markov or nonpreemptive policies, fixing , dropping abandonment, specializing to Poisson arrivals or linear costs, or imposing a common initial split would each trivialize or weaken the statement and is ruled out.
Not formalized:
Contributions are welcome on any milestone, and especially on infrastructure: Poisson and renewal processes, functional central limit theorems in Skorokhod space, classical solvability of elliptic HJB equations, and measurable selection of minimizers.
A controlled Markov process run under the long-run average cost criterion asks for a policy minimizing the asymptotic cost per stage. When every stationary policy induces a single recurrent class, the optimal average cost is a constant and is characterized by one equation, the average cost optimality equation (ACOE). In general it is not: under some policies the state process splits into several ergodic classes, different classes have different optimal costs, and the optimal average cost is a function of the initial state. This is the multichain case.
For finite models, Howard ([Dynamic Programming and Markov Processes, 1960, pp. 61–62]) introduced a pair of coupled equations for this situation: one for the gain function alone, and one, the ACOE, for together with a relative value function . Denardo and Fox (1968) developed the approach for finite multichain Markov renewal programs. For general Borel models, Yushkevich (1973) and Dynkin and Yushkevich (1979) introduced canonical triplets: a gain , a terminal cost and a policy such that is optimal for every finite horizon with terminal cost , and the optimal -stage cost is exactly . The survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993), §6.1) states the link between the two notions as Theorem 6.2 and proves it on p. 317.
A controlled Markov process is a five-tuple :
A history is . An admissible policy is a sequence of stochastic kernels on with ; the class of all of them is . A stationary deterministic policy is a measurable map with . An initial state and a policy determine a probability measure on trajectories, with expectation . For a terminal cost and ,
denotes the bounded measurable real functions on . For and , the triplet is canonical if
Let , , and bounded on . Then is a canonical triplet if and only if, for all ,
and attains the infimum in both (6.6) and (6.7).
The result. Theorem 6.2 turns a statement about every finite horizon and every history-dependent randomized policy into two pointwise equations in and a pointwise selection condition on . A canonical policy is -stage optimal for every with terminal cost ; dividing (6.4) by shows that its average cost is . In the paper this is the entry point of Theorem 6.3, which shows that a canonical policy is strong average optimal and that is the optimal average cost, without any recurrence assumption. Equation (6.6) is the condition that makes behave as a constant in the optimization; when is constant it holds trivially, and Theorem 6.2 specializes to the bounded ACOE with a minimizing selector.
Formalizing it. The theorem is proved in the paper (and earlier by Yushkevich). This mission formalizes that proof on a general Borel model with history-dependent randomized policies and path measures built by the Ionescu-Tulcea theorem. Prove2Me has no formalization of the multichain coupled equations or of canonical triplets beyond finite models. The finite-horizon dynamic programming inequality of milestone 2, for policies that may use the whole history, is reusable in any finite-horizon or average-cost development on Borel spaces.
The algebra in the proof takes a few lines. The work is in two probabilistic facts that the paper uses without comment.
The first is the Markov decomposition of the -stage cost: conditioning on the first state–action pair turns the remaining stages into an -stage problem started from the next state. For a stationary policy the continuation is the same policy. For a history-dependent policy, the continuation is a policy that depends measurably on . Expressing this on the Ionescu-Tulcea measure is where the effort goes.
The second is the identity . On a Borel model, need not be measurable and the infimum need not be attained by a measurable selector. That is why the paper usually works with semicontinuous models (p. 288). Theorem 6.2 avoids the issue: only the inequality is needed, under the measurability that supplies, and the reverse direction is supplied by the given . A first attempt that proves the full identity for general Borel models runs into measurable selection problems that the theorem never needs.
BorelCMP S A has standard Borel S and Borel A, compact nonempty U x with measurable graph, a measurable cost c : S × A → ℝ with c ≥ 0 on K, and a Markov kernel P. c and P are total on S × A; only values on K enter. No continuity of c or P is assumed: Theorem 6.2 does not use Assumptions 2.2, 2.3 or 6.1.Policy M is the paper's : history-dependent, randomized, with admissibility . StationaryPolicy M is (measurable with ). The infimum ranges over all of Policy M. Restricting it to stationary policies would make sufficiency trivial and necessity false, and is not what the paper states.Kernel.trajMeasure at the first step, the shifted (continuation) policy and its measurability in the first state–action pair, and bounded-convergence bookkeeping for the Bochner integrals. These are reusable for every finite-horizon statement on this model. Proofs of the milestones are welcome independently. So are alternative proofs of the goal that bypass milestone 2 and argue directly with the canonical policy.Infinite horizon dynamic programming asks for the least expected cost of controlling a stochastic system forever, and for a policy attaining it. On finite or countable state spaces the theory has been classical since Bellman, Blackwell (1965) and Strauch (1966). Many models in operations research, inventory control, queueing and economics have continuous states and controls, however, and there the Bellman equation raises a question the countable theory never meets: the optimal cost need not be Borel-measurable, so its expectation under the transition law, which the equation requires, may not be defined.
Bertsekas and Shreve (1978) settled this question by working with lower semianalytic cost functions and universally measurable policies. In that framework the optimal cost is always measurable enough to be integrated, and the optimality equation holds with no continuity or compactness assumption. Chapter 9 of their book treats the infinite horizon model under the three classical cost structures: nonnegative costs (P), nonpositive costs (N), and bounded discounted costs (D).
Timeline:
An infinite horizon stochastic optimal control model (SM) is an eight-tuple . The state space , the control space and the disturbance space are nonempty Borel spaces, that is, spaces homeomorphic to Borel subsets of complete separable metric spaces. The control constraint assigns to each state a nonempty set , and the set is analytic. The disturbance kernel is a Borel stochastic kernel and the system function is Borel. The discount factor is , and the one-stage cost is lower semianalytic: each sublevel set is analytic. The state moves by , with transition kernel .
A policy chooses at random from a universally measurable stochastic kernel concentrated on ; is the set of all policies. A policy is Markov if each depends only on , and it is stationary if, moreover, for all . Writing for the law of started from , the cost of and the optimal cost are
For , the dynamic programming operators are
The three cases are (P) on ; (N) on ; (D) and on for some real .
Under each of (P), (N) and (D),
The optimality equation is the basic structural fact of infinite horizon control. Corollary 9.12.1 uses it to construct optimal stationary policies from minimizers in the equation. The existence results for -optimal policies (Propositions 9.19 and 9.20), the convergence analysis of value iteration in Section 9.5, and the reduction of imperfect state information problems in Chapter 10 all build on it. It holds for arbitrary Borel models, with no continuity or compactness assumption.
All results of the mission were proved in 1978. None of them has a machine-checked proof: Mathlib has stochastic kernels and the Ionescu-Tulcea construction for measurable kernels, but no theory of lower semianalytic functions, universally measurable kernels, or dynamic programming on Borel spaces. A formal development would fix the measurability bookkeeping on which the textbook proofs rest and supply a reusable substrate for the stochastic control papers that cite this book.
Under (D), is a contraction on bounded functions, and its fixed point is the limit of value iteration. That argument, however, gives a fixed point only within a fixed class of measurable functions. Showing that this fixed point equals requires knowing that belongs to the class and that history-dependent randomized policies do no better. Under (P), value iteration can converge to the wrong limit (Example 1 of the chapter: while ). Even when each is Borel, may fail to be (Example 2). So cannot be obtained as a limit of the finite horizon equations, and the natural class of Borel functions is not closed under the partial minimization that defines .
The book's route lifts (SM) to a deterministic model on the space of probability measures , where no measurability restriction is needed, and transfers the results back. Making this transfer rigorous requires that the cost of a randomized policy be a measurable functional of its law, and that the infimum over policies preserve lower semianalyticity.
The draft fixes the following conventions.
AnalyticSet. A set is universally measurable if it is null-measurable for every probability measure.EReal. The book's convention is implemented explicitly, because Mathlib's EReal sets . The integral of an extended-real function is with the same convention.The goal admits a trivializing formalization that this draft rules out. is not defined as a fixed point of , nor as the limit of ; it is the infimum of the costs of all policies, which under (P) can differ from that limit.
A complete development needs universally measurable kernels and their compositions on product spaces, measurability of for universally measurable integrands, the measurable selection theorem of Jankov and von Neumann, and the closure of lower semianalytic functions under partial infimum. These are the subject of the series' mission on Chapter 7, and they are reusable for any stochastic control model on Borel spaces. Contributions are welcome at any level: these foundations, the Markov reduction (Proposition 9.1), or the case-by-case arguments.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's earlier values ( down to ) came from Schnirelmann's method with every constant written out. Those arguments stall near because the medium range relies only on a Chebyshev lower bound for . This entry adds the small-shift idea of Riesel and Vaughan, which removes that bottleneck without any zeta-zero input.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in.
Let and . We show , then conclude with Mann's theorem as in the entry. Write for the scale.
The argument stays elementary: no prime number theorem and no zeros of or -functions. New reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Already proved on the platform: Schnir.sieve_ineq, Schnir.G_lower, Schnir.pi_lower, Schnir.basis_of_density. Mathlib supplies the Chebyshev bounds (Chebyshev.psi_ge', Chebyshev.theta_le_log4_mul_x) and the Λ² sieve framework (Mathlib.NumberTheory.SelbergSieve).
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's earlier values ( down to ) came from Schnirelmann's method with every constant written out. Those arguments stall near because the medium range relies only on a Chebyshev lower bound for . This entry adds the small-shift idea of Riesel and Vaughan, which removes that bottleneck without any zeta-zero input.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in.
Let and . We show , then conclude with Mann's theorem as in the entry. Write for the scale.
The argument stays elementary: no prime number theorem and no zeros of or -functions. New reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Already proved on the platform: Schnir.sieve_ineq, Schnir.G_lower, Schnir.pi_lower, Schnir.basis_of_density. Mathlib supplies the Chebyshev bounds (Chebyshev.psi_ge', Chebyshev.theta_le_log4_mul_x) and the Λ² sieve framework (Mathlib.NumberTheory.SelbergSieve).
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The argument proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It follows the companion entry, with every parameter pushed to the limit of the same tools. Let and . We show :
About is the floor of this method: the medium range relies on the Chebyshev constant , which forces the sieve threshold below and so inflates the sieve coefficient.
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization. Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. All the ingredients above except the moment bound and the final assembly are already proved on the platform (Schnir.sieve_ineq, Schnir.G_lower, Schnir.pi_lower, Schnir.basis_of_density).
This mission formalizes A. Connes, J. Feldman and B. Weiss, An amenable equivalence relation is generated by a single transformation, Ergodic Theory Dynam. Systems 1 (1981) 431–450 (doi:10.1017/S014338570000136X).
A countable group acting on a measure space partitions it into countable orbits, and much of ergodic theory studies actions only through this orbit equivalence relation. The simplest relations are those of a single transformation, the orbits of an action of . Connes, Feldman and Weiss characterize exactly which relations are of this kind, up to null sets: the amenable ones, those carrying an invariant mean. Since the orbit relation of any action of a countable amenable group is amenable, every such action is orbit equivalent to an action of . The same theorem gives the uniqueness of Cartan subalgebras in hyperfinite von Neumann algebras.
On this platform it is the missing link in the Lodha–Moore mission, which passes between Lodha and Moore's definition of a -amenable relation (an orbit relation of off a null set) and the invariant-mean definition of the Monod bundle: one direction is proved, the other (LodhaMoore.isMuAmenable_of_isAmenableRel) is this mission's goal in Lodha and Moore's language.
Timeline.
is a standard Borel space with a -finite measure . A discrete measured equivalence relation (IsDiscreteMeasured μ R) is a Borel equivalence relation whose classes are countable and for which is quasi-invariant: the saturation of a null Borel set is null.
carries the measure , the counting measure on the class of (relMeasure), and the module , the density of against its image under (module). A partial transformation of is a Borel bijection between Borel subsets of whose graph lies in (Monod.PartialTransformation).
is amenable (Monod.IsAmenableRel) when it has a left invariant mean: a positive normalized map from bounded functions on to bounded functions on with for every partial transformation (Definitions 5–6). is of type I (IsTypeI) when, off a null saturated set, its quotient is a standard Borel space, and hyperfinite (IsHyperfinite) when, off a null set, it is a countable increasing union of type I equivalence relations (Definition 1). A finite subequivalence relation (IsFiniteSubrelation) is a Borel that is an equivalence relation with finite classes on .
For amenable there are a non-singular Borel automorphism of and a null set with
The result. Theorem 10 turns amenability, which is usually easy to check, into hyperfiniteness, which is the structure one wants: for instance, the action of on the projective line, or of any discrete group on with amenable, is generated by a single transformation. On this platform it closes the open direction, LodhaMoore.isMuAmenable_of_isAmenableRel, and with it Lodha and Moore's Theorem 2.1.
Formalizing it. No machine-checked proof of the theorem exists, in Mathlib or elsewhere as far as a search finds; Mathlib has no theory of countable Borel equivalence relations. A complete development builds that theory from the descriptive set theory Mathlib has.
The theorem is about relations without a group. The obvious route, through a countable group generating and an amenability of that group, is unavailable: the orbit relation of a nonamenable group, such as acting on the projective line, can be amenable, and there is no group whose Følner sets one could use. The Følner sets of Lemma 8 have to be produced from the invariant mean on the relation itself, which needs duality between and and convexity arguments. Underneath, even the basic facts used in §§1–3 (that is a countable union of graphs of Borel automorphisms, that is a measure, that saturations of Borel sets are Borel) rest on the Lusin–Novikov uniformization theorem, which is not in Mathlib. It is published here as standalone theorems: a Borel set with countable sections is a countable union of Borel graphs, and a countable-to-one Borel map is injective on countably many Borel pieces covering its domain.
All statements carry the hypotheses of §1: standard Borel (StandardBorelSpace), -finite, a Borel equivalence relation with countable classes and quasi-invariant. Lemmas 8 and 9 take a probability measure, as the paper's proof of Lemma 9 does. “Up to a null set” is read as “off a -null Borel set of points”, which by quasi-invariance agrees with the paper's -null sets. Amenability is the published Monod definition, an invariant mean on bounded measurable functions modulo null sets; it is not trivial (the relation of for a countable dense subring of is not amenable, Monod.not_isAmenableRel_mob).
The definitions are in the definition bundle ConnesFeldmanWeiss. Reusable beyond this mission: the Feldman–Moore theorem and the basic theory of countable Borel equivalence relations, both welcome as standalone theorems.
What is left out. Proposition 7 and Corollary 11 need the von Neumann algebra of a relation and its Cartan subalgebras, which Mathlib does not have. The final part of the paper (Lemma 15 to Corollary 21) treats relations with uncountable classes through transverse functions, including foliations; it is a different setting with its own definitions.
Nguyen and Tang study the irreversible catalytic network , , a simple reaction–diffusion system with both a positive and a boundary equilibrium (catalyst used up). They settle every mass regime but one and leave it as a conjecture (AIM problem 416).
Timeline. 2021: Fellner–Morgan–Tang give global classical solutions with uniform bounds. 2026: Nguyen–Tang prove convergence for and and local results in between, conjecturing global attraction there.
On a bounded connected smooth domain with and :
with homogeneous Neumann conditions and strictly positive compatible initial data. The masses , are conserved. The equilibria are the positive one and the boundary one .
If , every classical solution converges uniformly on to the positive equilibrium (no rate required).
This is the last open regime of Nguyen–Tang's stability analysis. Strict positivity is essential: with the solution stays away from the positive equilibrium.
For there is no positive lower bound on , so entropy dissipation can degenerate near the boundary equilibrium (), and the local results do not exclude trajectories approaching it.
is EuclideanSpace ℝ (Fin n) and is Mathlib's Laplacian. The domain is for a function with on ; the Neumann condition is the derivative within in the direction . Solutions are continuous on and for , and convergence is TendstoUniformlyOn. The goal quantifies over classical solutions; their existence is proved in the literature (Fellner–Morgan–Tang; Nguyen–Tang, Theorem 2.1) but is not part of this statement.
Gustafson, Meinert and Melcher construct axisymmetric saddle points of the micromagnetic energy of a spherical shell in two ways (a heat flow, and continuation from an explicit solution at ). Their Remark 3.18 conjectures that a single uniqueness statement identifies the two; it is problem 241 of the AIM open problem list.
Timeline. 2016: Kravchuk et al. propose the model. 2025: Gustafson–Meinert–Melcher construct the saddle points and state the conjecture.
For anisotropy the energy of is . An axisymmetric field with profile is critical exactly when
The hemispheric class adds , , .
For every there is exactly one smooth profile in that solves (2.6) and induces a smooth map . The statement may be proved or disproved.
Uniqueness would identify the two constructions as one saddle branch; a counterexample would give further degree-zero critical points of .
(2.6) is singular at both poles and is a two-point boundary condition, so standard ODE uniqueness does not apply, and the paper's comparison arguments only control solutions in the wedge . Numerical evidence (shooting) finds at , besides , a second solution in the class with (similarly at ), which leaves the wedge.
Profiles are functions ; all conditions, and the uniqueness, are imposed on only (values outside are unconstrained, so uniqueness on would be trivially false). Smoothness is ContDiffOn ℝ ∞ on . "Induces a smooth map" means the field extended to as a function of is there; this excludes profiles with a cone singularity at a pole. The paper's uses piecewise profiles; by its Corollary 2.7 it has the same solutions.
A Costas array is a permutation matrix in which the difference vectors between distinct dots are pairwise distinct; such arrays are frequency-hopping patterns for sonar and radar (Costas, 1984). Rubio and Torres ask whether their -dimensional version can stay Costas in every window of its periodic extension, and conjecture that this happens only in the smallest order.
Timeline. 1984: Taylor proves that 2D periodic Costas arrays have order . 2023: Rubio–Torres prove the odd-order and 3D cases, give examples, and state Conjecture 1.
Let , , with all sides , and a bijection; the dots are . The array is Costas if the difference vectors between distinct dots are distinct, and periodic Costas if moreover, after repeating the dots periodically over , the dots inside every translate have distinct difference vectors.
Conjecture 1: if and defines a periodic Costas array, then
equivalently every . The condition is a normalization ( swaps the boxes).
A proof would give the multidimensional analogue of Taylor's theorem; a counterexample would give periodic distinct-difference patterns of non-power-of-two order.
The Rubio–Torres counting argument needs a bound that is available only when is one-dimensional, which is why it stops at . Computational evidence: an exhaustive window check reports that the array with dots is periodic Costas, which would disprove the conjecture.
A point of is a pair ; boxes are 1-based; is a total function whose values off are unused. Differences are plain integer vectors (not reduced modulo the sides), windows range over all , and and sides are part of the definition, so no degenerate case holds vacuously.
Many estimation procedures in statistics, and most stochastic optimization models in operations research, have the same shape: a decision or parameter is chosen to minimize an expected loss under a distribution that is not known. In practice is replaced by an estimate built from the information available at stage (an empirical measure, a smoothed or parametric fit, a Bayesian posterior), and the minimizer of the estimated problem is used in place of the true one. The basic question is whether this is justified: do the estimated solutions converge to a true solution, and the estimated optimal values to the true optimal value, as information accumulates?
For maximum likelihood this is Wald's consistency theorem (Wald 1949); Huber extended it to M-estimators under non-standard conditions (Huber 1967). Both settings are unconstrained, or constrained to an open set, and assume finite-valued criteria. Constrained least squares, and Huber regression with inequality constraints, variance-component models with Heywood cases, and two-stage stochastic programs with recourse all lead instead to criteria that take the value off a closed feasible set and are only lower semicontinuous in .
J. Dupačová and R. Wets (IIASA WP-86-41, 1986; journal version Ann. Statist. 16 (1988)) proved consistency in this generality by combining epi-convergence of functions with the theory of measurable multifunctions and normal integrands. This mission formalizes their §3.
is a Polish space with its Borel -field and is a probability measure on it. The integrand is , and the true problem is to minimize
with the convention that whenever is not bounded above by a summable function. The effective domain of a function is , and .
Information arrives on a probability space with an increasing sequence of -fields . Each sample yields probability measures on , and is -measurable for every Borel : the estimate at stage uses only stage- information. The estimated problem minimizes
A sequence epi-converges to if, at every , along every sequence , and along some sequence .
The standing hypotheses are Assumption 3.4: with closed and nonempty; is continuous for ; is lower semicontinuous; and is locally lower Lipschitz on with a bounded continuous modulus . Assumption 3.5 asks that, for -almost every , converge in distribution to , that be uniformly tight along for each , and that for all .
Let be compact, suppose -a.s. for every , and suppose . Then there are -measurable selections of with
The goal does not assume that has a unique global minimizer, and it does not assume convexity.
In attack order:
The result separates two things: the statistical input, which is only convergence in distribution of plus a tightness condition, and the variational output, which is convergence of optimal values and solutions. It therefore applies to any estimator that converges weakly almost surely: empirical measures, kernel estimates, parametric fits. It also covers constrained and nonsmooth problems: the feasible set enters through off , and only lower semicontinuity in is required. Asymptotic distribution results for constrained estimators, such as the second part of the same paper and the subsequent literature on sample average approximation, start from this consistency.
The theorem is proved on paper. To the best of current knowledge none of it is machine-checked. Mathlib has weak convergence of probability measures, lower semicontinuity and extended-real integrals. It does not have epi-convergence, Effros-measurable multifunctions, normal integrands or the Kuratowski–Ryll-Nardzewski selection theorem. A formal proof produces these as reusable components. It also has to supply the details that the paper's proof of Theorem 3.8 leaves as a sketch.
Pointwise convergence is not enough to move minimizers to the limit, and uniform convergence fails because is off and need not be bounded. Epi-convergence is the right notion. Proving it needs a liminf inequality along moving points under moving measures . That combines Fatou's lemma, the lower Lipschitz bound and the tightness condition, and the integrands are extended-real-valued, so care is needed.
The second difficulty is measurability. The exceptional null set lies in but not in , so "-measurable" has to be understood on a full-measure set in the trace -field. The paper's argument for Theorem 3.8 appeals to continuity of in the epi-topology, and it remarks itself that Theorem 3.7 gives this only along sequences satisfying Assumption 3.5. A solver will have to rebuild this step, for example through the normal-integrand structure of .
EuclideanSpace ℝ (Fin n) with its Euclidean norm.EReal-valued. Every expectation is the mission's expect: when , and otherwise, both computed as Lebesgue integrals of -valued functions. A Bochner integral, which would assign to non-integrable functions, is never used for or .Pν k and 𝔽 k are the paper's and , and is a separate argument.The hypotheses are not vacuous. A sorry-free check verifies all of them, including those of the goal, for with Dirac measures. Defining the expectation through a Bochner integral, or dropping (which makes every all of ), would trivialize or change the statements; the definitions above rule both out.
Contributions are welcome on any milestone. Proposition 3.1 (Kuratowski–Ryll-Nardzewski for -valued multifunctions) and Proposition 3.3 (deterministic epi-convergence facts) are independent of the probabilistic setting and reusable beyond this mission.
Many sequential decision problems ask a learner to choose, round after round, a combination of items: a set of ads out of , a path in a network, a matching. After each choice the learner sees the loss of the items it used, not of those it did not. This is online combinatorial optimization with semi-bandit feedback. It contains the classical adversarial multi-armed bandit (choose one of arms) and is a standard model in online advertising, routing and ranking.
Chapter 5 of Bubeck and Cesa-Bianchi's monograph arXiv:1204.5721v2 treats this problem with one algorithm, Online Stochastic Mirror Descent (OSMD). Every regret bound in the chapter comes from a single mirror-descent inequality, specialized through the choice of a convex "regularizer". The chapter's capstone, Theorem 5.7, shows that a polynomial regularizer gives pseudo-regret with no logarithmic factor. For this is the minimax-optimal rate of the adversarial bandit, first attained by the INF strategy of Audibert and Bubeck (2009). The semi-bandit version is due to Audibert, Bubeck and Lugosi (2014).
Vectors live in . The arm set is a nonempty with for every , and . An oblivious adversary fixes loss vectors . In round the learner plays a random arm , pays , and observes . The pseudo-regret is
A Legendre function on , for a nonempty open convex , is a continuous that is strictly convex and on and whose gradient norm tends to at . Its Bregman divergence is , and its Legendre–Fenchel transform is .
Online Mirror Descent with learning rate and vectors starts at . It then sets and . OSMD uses a random estimate of the loss. In the semi-bandit case it plays with and uses
A -potential is a convex, , increasing with , and . It defines the Legendre function on . With this is the negative entropy.
For every -potential and non-negative unbiased estimates,
For with , the estimate (5.5) and ,
Theorem 5.7 is the sharpest semi-bandit bound in the monograph. It shows that removing the factor of the exponential-weights analysis (Theorem 5.6) is a matter of the regularizer, not of a new algorithm. The same OSMD template gives the Euclidean-ball bound of Theorem 5.8 and is reused for bandit convex optimization in Chapter 6. Lemma 5.1, Lemma 5.2 and Theorem 5.3 are the standard mirror-descent toolkit, used throughout online learning and optimization.
All results of the chapter are proved in the book. Lemmas 5.1 and 5.2 are cited from Cesa-Bianchi and Lugosi (2006). None of them is formalized on Prove2Me. The published mirror-descent bound of Bandit Algorithms XII treats linear losses with a comparator inside and Euclidean-space vectors; it is not Theorem 5.3. The mission adds a machine-checked version of the whole chain, from Legendre duality to the explicit constant , with two of the printed statements corrected (below).
The pathwise mirror-descent inequality is a telescoping argument, but several of its steps rest on convex analysis that Mathlib does not package. One is the existence and interior location of Bregman projections onto a set that touches the boundary of . Another is the differentiability of on the open dual space and the identity . A third is the closed form of for a potential defined through an improper integral of .
The probabilistic step is not a martingale argument. Only conditioning on the current iterate is available. The estimate (5.5) divides by , so its integrability and unbiasedness have to be derived from the fact that the iterates stay in the open orthant. Finally, the explicit constant requires a Hölder step, , and the matching bound .
Vectors are Fin d → ℝ. The arm set is a Set of vectors with coordinate sum , and is convexHull ℝ C. Rounds are , sums run over Finset.Icc 1 n, and index is unused. A randomized run is a family of measurable processes on a probability space, with the deterministic OMD recursion holding on every sample path. is the coordinatewise conditional expectation given , which is exactly what the book's proofs use. Losses are oblivious, so is stated as "for every , ". is valued in EReal, and is evaluated only on the open dual space, where is finite. Wherever an expectation of a possibly non-integrable quantity appears on a right-hand side, its integrability is assumed: the book's bound is then and trivial, while Lean's integral would be .
Corrections and instantiations, each labelled in the item's Formalization Note:
A trivializing formalization would let , or the estimate be junk values: an OSMD step at , a Lean division , or a regret written as a real infimum over an unbounded set. Here every run is the book's algorithm on the open orthant, and each bound is stated against every comparator in .
Reusable beyond this mission: the Legendre/Bregman layer, the OMD run predicate and the -potential layer. Proofs of Lemmas 5.1 and 5.2 in this generality would be welcome additions to the library.
In the adversarial (non-stochastic) multi-armed bandit problem a forecaster repeatedly chooses one of actions while an opponent sets the rewards, and only the reward of the chosen action is revealed. The model was proposed as a way of playing an unknown repeated game: Baños (1968) studied the repeated game in which the player observes only its own payoff, which is exactly the bandit problem against an opponent who reacts to the player's past moves. It is the basic model of online decision making under partial feedback without statistical assumptions, and it underlies regret minimization in games, adversarial routing and online advertising. Chapter 3 of Bubeck and Cesa-Bianchi's monograph (arXiv:1204.5721v2) collects its fundamental results: the Exp3 forecaster of Auer, Cesa-Bianchi, Freund and Schapire (SIAM J. Comput. 2002), its high-probability variant Exp3.P, and the minimax lower bound.
There are arms and rounds . At each round an adversary assigns a gain to every arm ; the forecaster picks an arm , possibly at random, and observes only . The adversary may be non-oblivious (adaptive): may depend on the forecaster's past actions. A forecaster rule maps the past actions to a probability vector on the arms, and a run is a sequence of random arms with given the past. The regret is the random variable
and, in the loss version , the pseudo-regret is . Since the maximum sits inside the expectation, in the gain version, and against an adaptive adversary the two can differ.
Exp3 draws from exponential weights of importance-weighted cumulative loss estimates . Exp3.P uses biased gain estimates and mixes in the uniform distribution:
With , , , against every adaptive adversary,
The goal bounds the expected regret, not the pseudo-regret, against an opponent that adapts to the forecaster's randomized past choices. A pseudo-regret bound says nothing about in that setting, and the book obtains the expected-regret bound by first proving a high-probability bound valid at every confidence level, (3.11), and integrating its tail. Together with Theorem 3.4 the chapter shows that is the minimax rate of adversarial bandits up to a factor. Lemma 3.1, the concentration of biased importance-weighted estimates, holds for any forecaster rule and is the step that turns exponential weights into a high-probability guarantee.
All results are proved in the book. On the formal side, the platform has the pseudo-regret bound of Exp3 against an oblivious adversary (a fixed reward table, Bandit Algorithms V) and an Exp3-IX high-probability bound; it has no Exp3.P, no regret bound against adaptive adversaries and no Bernoulli lower bound. This mission adds an explicit model of adaptive adversaries and randomized forecaster runs, and the chapter's statements with the book's exact constants.
Against an adaptive adversary the gains are random and depend on the forecaster's own past draws, so the argument used for a fixed reward table (take expectations of an inequality that holds for every fixed sequence) does not control : the maximum over arms does not commute with the expectation. Unbiased estimates do not help either, because the variance of is of order , which can be arbitrarily large; even with uniform mixing at rate the cumulative variance is of order . The bias and the mixing have to be tuned jointly so that the estimate concentrates while the exponential-weights analysis survives, and the constants , and come out of that tuning. The lower bound needs an information-theoretic comparison of a forecaster's behaviour on Bernoulli instances, against forecasters that may be randomized.
Arms are Fin K with ; rounds are numbered ; logarithms are natural. Action sequences are functions Fin K whose entry is ignored. An adversary is a structure holding values in that may depend on the past actions only (gains for Exp3.P, losses for Exp3); a randomized adversary with independent external randomness reduces to this case by conditioning. A run of a forecaster rule on a probability space is pinned down by the cylinder identity , which determines the law of . "With probability at least " is for , and is the Bochner integral of the bounded, measurable regret. The lower bounds use a stochastic model in which the forecaster sees past actions and the rewards of the played arms, and rewards are i.i.d. product Bernoulli.
Constants and conventions:
A trivializing formalization is ruled out: the forecasters are fixed rules of the observed history drawn with fresh randomness, the adversary is not restricted to a fixed sequence, and the lower bounds quantify over all forecasters and exhibit the instance.
Welcome contributions: a reusable construction of runs (existence of a probability space carrying a run for every rule), the supermartingale form of Lemma 3.1, the exponential-weights potential argument, a tail-integration lemma , and a KL/Pinsker comparison for bandit runs.
Many service systems route several classes of work to servers with overlapping skills: call centers with cross-trained agents, manufacturing cells with flexible machines, computing clusters with heterogeneous processors. Choosing which server works on which class at each moment is a dynamic scheduling problem. Exact optimal policies are out of reach except in toy cases, so heavy-traffic theory replaces the queueing system by a Brownian control problem, solves that limit problem, and then asks for a policy in the original system whose performance converges to the Brownian optimum. This programme was proposed by Harrison (Harrison 1988), and the parallel server system studied here is the example Harrison used (Harrison, Ann. Appl. Probab. 1998) to show that the greedy static priority rule can be very inefficient.
Bell and Williams (2001) gave the first proof of asymptotic optimality of a continuous-review policy for this system, with renewal arrivals and general service times. Harrison (1998) had treated Poisson arrivals and deterministic service times with a discrete-review policy and a pathwise criterion. Harrison and López (Queueing Systems, 1999) identified the complete resource pooling condition for general parallel server systems. The threshold policy and the proof method of Bell and Williams were later extended to multiserver systems (Bell and Williams, Electron. J. Probab., 2005).
There are two job classes and two servers. Server 1 serves class 1 (activity 1); server 2 serves class 1 (activity 2) and class 2 (activity 3). A sequence of such systems is indexed by . On a probability space, i.i.d. sequences () and (), , are fixed: strictly positive, mutually independent, with mean one and finite variances . In system the interarrival times are and the service times are . The renewal processes and count arrivals and potential service completions.
A scheduling control policy is an allocation , where is the time devoted to activity in . Each is a random variable, each is continuous and nondecreasing from , and so are the idle times and . The queue lengths
must be nonnegative. Policies may anticipate the future. The rates satisfy Assumption 3.1: , , and the rates converge at rate to limits with second-order parameters . Assumption 3.2 is , and Assumption 3.3 gives finite exponential moments near . With the cost is
The threshold policy with works as follows. Server 1 works whenever it has a class 1 job available. Server 2 serves class 1 with preemptive-resume priority when more than class 1 jobs are present, and otherwise serves class 2. The Brownian benchmark is built from a two-dimensional Brownian motion with drift and diagonal covariance, from , and from the reflected process with . Its cost is .
For larger than a constant that depends only on the model data, and for every sequence of scheduling control policies,
A further draft theorem states that Definition 5.1 determines an admissible allocation, unique pathwise, whenever .
The theorem proves that a simple state-dependent rule, which sends server 2 to class 1 only when the class 1 queue exceeds a logarithmic safety stock, is asymptotically optimal among all policies, including those that anticipate the future. The limiting cost is the explicit optimum of the Brownian control problem. The proof gives a template for heavy-traffic asymptotic optimality under complete resource pooling: a lower bound valid for every policy, and state-space collapse under the proposed policy. The residual process analysis of Section 7 shows how a threshold of order makes starvation of server 1 negligible on the diffusion time scale.
The paper's results are proved but not machine-checked; no formal proof exists in any proof assistant. The mission asks for formal statements of the paper's main theorem and its supporting lemmas, followed by formal proofs. Parts of the development are independent of the paper: the one-dimensional Skorokhod map, renewal large deviation bounds, and convergence encodings on path space.
The lower bound must hold for arbitrary, possibly anticipating, policies, so no Markov structure is available. The argument has to pass through fluid limits of an arbitrary cost-minimizing subsequence and a pathwise minimality property, and Fatou's lemma for the limit needs uniform control. For the upper bound, the obvious approach, a static priority rule, is known to fail: it starves server 1 and produces a large class 1 queue. With a threshold policy, the hard step is to show that the class 1 queue, once at the threshold, rarely moves away from it over a time interval of length . That requires large deviation estimates for renewal processes started at random, multiparameter stopping times. Showing that converges to , rather than only that the processes converge in distribution, also requires uniform integrability of the scaled queue lengths.
Classes and activities are indexed by Fin 2 and Fin 3. The i.i.d. sequences keep the paper's index base , and the systems are indexed by with , . Time is real, and every condition is imposed for . Admissibility is exactly (11)–(14). Measurability in (11) is with respect to the completion of , since the paper's space is complete. Finiteness of the renewal processes everywhere on , which the paper obtains by discarding a null set, is a hypothesis. Queue lengths are real, costs are lower Lebesgue integrals in , counting processes take values in , and , take values in the extended reals.
The constant is existential and is chosen after the model data and before , the policies and the Brownian motions. The threshold relations are required only for the systems with , which are all but finitely many. Each convergence to a deterministic limit (Theorem 7.1, Lemmas 8.1 and 9.3) is stated as u.o.c. convergence in probability, the paper's own equivalence (p. 633). Theorem 5.2 is stated in coupling form: there are copies of the processes on one probability space, with Skorokhod paths and the same laws, that converge almost surely uniformly on compacts. This is equivalent to weak convergence in to a limit with continuous paths. is defined by (44) from an arbitrary pair of independent standard Brownian motions (Mathlib's IsBrownianReal), not by a closed form.
Two formalizations would make the goal trivial, and both are excluded. Leaving out the requirement that actually follow the policy would make the goal false or empty. Narrowing the class of competing policies, for example to non-anticipating ones, would weaken the theorem. A draft theorem also states that the threshold allocation exists and is unique pathwise, so the hypothesis on can be satisfied.
The development needs renewal theory (functional central limit theorems, Cramér bounds), multiparameter stopping times, tightness in , the Skorokhod representation theorem, the reflection map, and properties of reflected Brownian motion. Contributions are welcome at every level: proofs of milestones, reusable lemmas on renewal processes and the Skorokhod map, and further lemmas of the paper (Lemmas 7.5, 7.6 and 9.2 are not yet stated).
The ground-state energy of a mixed -spin spin glass, , converges almost surely to the infimum of the Parisi functional over non-decreasing order parameters (Auffinger–Chen 2017). El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) study algorithms that find near-optimal configurations. They introduce incremental approximate message passing (IAMP) and show that, among a broad class of such algorithms, the best achievable energy is the infimum of the Parisi functional over a larger space of order parameters (their Theorem 4).
The upper bound in Theorem 4 is reduced, in Section 4 of the paper, to a stochastic optimal control problem. The energy reached by a message-passing algorithm becomes the objective of a control problem driven by a Brownian motion, with a terminal constraint and a variance constraint. The variance constraint is removed by a Lagrange multiplier . Proposition 4.1 states that the resulting Lagrangian value is exactly the Parisi functional . This mission formalizes that duality and the verification argument behind it (Section 7).
Mixture. Real coefficients define the mixture , with the standing assumption for some . Its derivatives , are nonnegative and nondecreasing on .
Order parameters. is the set of nonnegative step functions
Put .
Parisi PDE and functional. solves
For it is given explicitly by the Cole–Hopf recursion: with and , for ,
The Parisi functional is .
Control problem. Let be a standard Brownian motion. A control is a process on , progressively measurable for the filtration of , with . The value is
Candidate value function. With ,
Proposition 7.1 at together with milestone 4 gives the goal.
The result. By integration by parts (Eq. (4.4) of the paper), bounds the value of the constrained control problem (4.2). That problem in turn bounds the asymptotic energy of every message-passing algorithm in the class of Theorem 4. Proposition 4.1 turns the bound into , which is the analytic core of the optimality statement for IAMP. It is also an instance of a broader principle: the Parisi functional has a stochastic-control representation (Jagannath–Tobasco 2016).
Formalizing it. The result is proved in the paper; no machine-checked version exists. A complete formalization needs a verification theorem for a control problem with a state constraint (), Itô's formula for a function that is only piecewise in time, and quantitative regularity of the Cole–Hopf solution. Each of these is reusable well beyond spin glasses.
The value function is not known to be smooth, and the dynamic-programming equation (4.6) is only heuristic. The proof therefore guesses a solution and verifies it. Two steps carry the difficulty.
First, the guess is a Legendre transform. Its regularity, and the sign that makes the HJB supremum finite, rest on strict convexity and bounded curvature of (Lemma 7.2). These must be proved by induction through the Cole–Hopf recursion, including the steps with .
Second, the verification argument applies Itô's formula to , where is a martingale confined to and is only in time between the jumps of . The boundary needs a dominated-convergence argument, and attaining the supremum needs an explicit optimal feedback control built from an SDE.
gaussianReal 0 1.deriv/iteratedDeriv. Time derivatives are right derivatives, because jumps.IsBrownianReal process on , with each measurable. The filtration is .Peng1990.SMP.IsItoIntegral (horizon ), whose integrability class is exactly .IsLUB), never as a real sSup. A default value of an empty or unbounded supremum therefore cannot make a statement trivially true.The paper's algorithmic results (Theorems 2–4, Corollary 2.2) are out of scope. They need the AMP and state-evolution machinery of Section 5 and Appendix A, and an informal model of computation. The optional bound (4.4) is not stated.
Welcome contributions include the regularity of Cole–Hopf solutions (Gaussian convolution, log-moment-generating functions), a general verification theorem for one-dimensional controlled martingales with a terminal state constraint, and Itô's formula for functions.
The mixed -spin model is a random polynomial on the hypercube : a centered Gaussian process with covariance . Its maximum is a canonical random optimization problem; for it is the ground state of the Sherrington–Kirkpatrick model. Auffinger and Chen (AC17) proved that converges almost surely to the infimum of the zero-temperature Parisi functional over a space of non-decreasing order parameters.
El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) characterize what a class of message-passing algorithms achieves on this problem. The answer is the infimum of the same functional over a larger space of order parameters that need not be monotone. Whether these algorithms reach the true optimum is therefore the question whether . The paper proves this equality under the no-overlap gap assumption, that the Parisi minimizer over can be taken strictly increasing (Assumption 2, p. 8). This is believed to hold for the Sherrington–Kirkpatrick model and to fail for pure -spin models with . This mission formalizes that equality, stated as a property of the minimizer.
Timeline. Parisi's formula (1979) was proved by Talagrand (2006) and Panchenko (2013). Auffinger and Chen (2017) gave its zero-temperature form (1.7). Jagannath and Tobasco (JT16) gave a PDE and variational treatment of the Parisi functional at positive temperature, including its convexity. Montanari (Mon19) gave a message-passing algorithm for the Sherrington–Kirkpatrick model under no overlap gap. El Alaoui, Montanari and Sellke (2020) extended it to mixed -spin models and introduced the extended principle over .
A mixture is with for some , with derivatives and given by the termwise series. Order parameters are functions , in one of two spaces:
Here is total variation on , and .
For a step function with (the space ), the Parisi PDE
is solved explicitly by the Cole–Hopf recursion (7.3). It is a Gaussian log-moment-generating step on each piece, and a heat-semigroup step where . For general , is the limit of along step functions in the weighted norm . The Parisi functional is
The process is the strong solution of , (Eq. (6.3)), driven by a standard Brownian motion .
If is strictly increasing on and for every , then
Since , this is the paper's main result 2 (p. 4), under no overlap gap.
The result. The goal identifies the value reached by the paper's message-passing algorithm with the ground-state energy whenever the Parisi minimizer is strictly increasing. Combined with the paper's algorithmic theorem, it yields a -approximation of in time linear in the input size, for the Sherrington–Kirkpatrick model and any other mixture with no overlap gap (Corollary 2.2). It also gives a structural fact about the variational problem: when the minimizer is strictly increasing, the monotonicity constraint in is not binding.
Formalizing it. The result is proved in the paper, but the proof leans on an external citation ([JT16, Theorem 20]) for convexity of on . It also applies the first-variation formula in a direction that does not meet that formula's stated hypotheses. A machine-checked development closes both gaps. No part of this theory (the Parisi PDE, its Cole–Hopf solution, or the extended functional) has been formalized before, to our knowledge.
The obvious argument is: convexity plus stationarity gives a global minimum. Both inputs are hard. Stationarity (Lemma 6.15) needs the first variation of in directions that keep monotone. That variation is a derivative of the solution of a nonlinear PDE with respect to its coefficient, expressed through an SDE driven by that solution's own gradient. Convexity of on is not visible from the formula: is defined through a limit of nested Cole–Hopf recursions, and the paper does not prove it, citing a positive-temperature argument instead. Finally, the goal needs the first variation in the direction , which is generally non-zero near , where may blow up. Proposition 6.8 as stated excludes such directions.
c : ℕ → ℝ with and for some . and are explicit power series.eVariationOn; finiteness of integrals is IntegrableOn (which includes measurability).gaussianReal 0 1.limUnder of the Cole–Hopf values along step-function data converging to in the weighted distance. is deriv in .EthierKurtz.SolvesBrownianSDE in dimension one, with coefficients extended by after time . Brownian motion is Mathlib's IsBrownianReal, and expectations are Bochner integrals.Contributions welcome: Cole–Hopf regularity (smoothness and the bound ), the Lipschitz estimate in that makes well defined, well-posedness of the SDE, and Itô calculus for the first variation. The Cole–Hopf layer and the SDE well-posedness are reusable for the companion missions on the full-support theorem and the stochastic-control duality of the same paper.
A branching random walk is the simplest model of a population that both reproduces and moves: every particle dies and leaves a random cloud of children displaced relative to it. Its extreme particles control the speed of travelling waves in reaction–diffusion equations (the KPP/Fisher equation), the free energy of directed polymers on trees, the cover and hitting times of random walks on trees, and the maxima of log-correlated fields such as the two-dimensional Gaussian free field. The basic quantity is the position of the leftmost particle at time .
Timeline.
Let be a point process on : a random, possibly infinite, collection of points. Start one particle at . At time it dies and leaves children at the points of ; each particle of generation then dies and leaves children at the points of an independent copy of , translated to its own position. Vertices of the genealogical tree (a Galton–Watson tree) are labelled by finite words ; is the generation, the ancestor at generation , and the position.
The paper works in the boundary case
and assumes throughout that is non-lattice and that
with and . The objects of the main theorem are the minimum (with ) and the derivative martingale
which converges almost surely to a limit , strictly positive on non-extinction. A standard example: two children with i.i.d. normal displacements of mean and variance .
There is a constant such that for every real ,
The constant is not specified numerically. It is the product of the constants below.
The theorem identifies the limit law of the extreme particle: converges in law, on the event of survival, to a Gumbel variable shifted by . It is the input for the study of the whole extremal process of the branching random walk seen from its leftmost particle (Madaule, J. Theoret. Probab., 2017), and it is the discrete-time counterpart of the Bramson and Lalley–Sellke results that later work on log-correlated fields takes as its template. The correction and the role of the derivative martingale are the signature of the boundary case, and of log-correlated extremes generally.
The result is proved and published. It has not been formalized: Mathlib has no branching processes, no Galton–Watson trees with positions, no renewal theory, and no derivative martingale. This mission produces the first machine-checkable statement of the convergence-in-law theorem and of the intermediate results it rests on. A complete development would also give reusable formal versions of the many-to-one lemma and of renewal theory for ladder heights.
The first-moment computation through the many-to-one lemma gives the wrong centring. It predicts that the minimum sits near , because the expected number of particles below a level is dominated by rare realisations. The true centring only appears after restricting to particles whose ancestral path stays above a barrier, and this restriction requires random-walk estimates (ballot theorems and local limit theorems for walks conditioned to stay positive) that hold uniformly in a window of starting points. A second difficulty is that the limit must be identified, not only shown to exist. Tightness and subsequence arguments do not give the factor ; the identification needs the precise tail of Proposition 4.1, with a known constant, and the almost-sure behaviour of the sum over the stopping line .
List ℕ. The branching random walk is any family of independent measurable configurations of law on a probability space. Every theorem holds for every such realisation, and a canonical realisation exists (product space).Out of scope: the spine-measure lemmas (Lemmas 2.3, 3.3, 3.8–3.10, 4.3), Propositions 2.1–2.2 cited from Lyons, and Appendices B–C. Contributions are welcome on all milestones. The many-to-one lemma and the renewal statement are independent of the rest and are natural first targets.