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?
The Pontryagin maximum principle is the basic first-order necessary condition of optimal control: along an optimal control, the control value at almost every time extremizes a Hamiltonian built from the dynamics and an adjoint vector. The classical statement presupposes that an optimal control exists. For many problems none does: the set of trajectories is not closed, or the cost does not attain its infimum, and the classical principle then says nothing.
Ekeland's 1974 paper On the Variational Principle (DOI 10.1016/0022-247X(74)90025-0) proves a general result about lower semicontinuous functions on complete metric spaces (its Theorem 1.1, now called Ekeland's variational principle) and closes with an application to control theory in §7 (pp. 348–351): for every terminal-cost problem satisfying mild regularity and growth conditions, there are ε-optimal controls that satisfy the maximum principle up to ε, whether or not an optimal control exists. The argument equips the measurable controls with the metric "measure of the set where two controls differ", which has since become a standard device in nonsmooth and approximate optimal control. For the classical theory, Ekeland refers to the treatise of Pallu de la Barrière (Optimal Control Theory, Saunders, 1967).
Fix , a horizon , an initial state , and a nonempty compact metrizable space of control values, with its Borel σ-algebra. A control is a measurable map . The dynamics are a map , and the state obeys
A trajectory of (Lean: IsTrajectory f x₀ T u x) is a function continuous on with for all . The standing hypotheses are:
fx) are continuous on ;The terminal cost is given by a function , and the problem is to minimize over all controls. The adjoint vector along a pair (Lean: IsAdjoint fx g T u x p) solves the linear equation
where is the transpose. The control distance (Lean: ctrlDist T u₁ u₂) is
and the needle variation of a control at with value (Lean: needle T uε u₀ t₀ τ) equals on and elsewhere.
For every there is a control with trajectory and adjoint vector such that
The result. Theorem 7.1 decouples the maximum principle from existence of optimal controls. Any minimizing sequence can be replaced by one consisting of controls that satisfy the necessary condition up to a vanishing error, so approximate extremals are available for numerical schemes and for limiting arguments (relaxation, convergence of extremals) in problems without compactness or convexity of the velocity sets. The same scheme, a complete metric on controls plus Ekeland's principle plus needle variations, underlies later proofs of the maximum principle with state constraints and in nonsmooth settings.
Formalizing it. The theorem has a published proof, which the paper sketches in four pages and partly defers to classical results (local existence for measurable controls, differentiability of trajectories with respect to needle variations). Neither Mathlib nor the platform contains this theorem or a maximum principle for measurable controls with time-dependent dynamics; the nearest platform items assume an exact optimum, a running cost and globally Lipschitz autonomous dynamics. A formalization requires a Carathéodory theory of ODEs in Lean, the complete metric space of controls, and a rigorous version of the classical first-variation computation. Each of these is useful well beyond this paper.
The obvious argument fails at its first step: a minimizing sequence of controls has no convergent subsequence in any useful sense, because measurable controls with values in are not compact in the metric and their weak limits are relaxed controls, which are not controls. Ekeland's principle avoids compactness, but it needs a complete metric space on which the cost is lower semicontinuous. Completeness of (Lemma 7.2) and continuity of the cost (Lemma 7.3) both require care. Continuity must hold for trajectories driven by merely measurable controls, which converge only in measure. The needle derivative (Lemma 7.4) holds only at times where the trajectory satisfies the state equation in the classical sense, which is almost every time but not every time.
ℝ → K with Measurable u; only values on matter. Trajectories and adjoint vectors are functions ℝ → EuclideanSpace ℝ (Fin n), continuous on and solving the integral form of their equation. The paper uses the same form in (7.13). A definition that asks for a derivative at every time would be unsatisfiable for discontinuous controls and would make the goal vacuous; the integral form avoids this.f and fx on univ ×ˢ univ ×ˢ Icc 0 T together with HasFDerivAt (fun y => f y u t) (fx x u t) x. Hypothesis (b) is ∃ c, … with the order of arguments ; the page prints in (b), a slip.ContinuousLinearMap.adjoint, and is gradient g x.⨅; (7.4) and (7.15) are stated as "for every control with trajectory ".[Nonempty K] in the goal and milestone 5. With empty no control exists and the existential statements would be false.Welcome contributions include Carathéodory existence and uniqueness for ODEs with measurable time dependence, Gronwall-type estimates for absolutely continuous functions, the complete metric space of measurable maps under the disagreement measure, and differentiability of flows with respect to initial data.
In many sequential decision problems the learner sees side information before acting. A news site chooses an article for a visitor whose history and location it knows; an ad server chooses an advertisement for a query. Only the reward of the chosen action is observed. These are contextual bandit problems, and Chapter 4 of Bubeck and Cesa-Bianchi's monograph Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems (arXiv:1204.5721v2) surveys several of their formal versions. In a contextual problem the learner is compared with the best policy, a map from contexts to arms, rather than with the best single arm.
This mission covers three of the chapter's models. The first marks each round with a context from a finite set. In the second, experts give advice, as in prediction with expert advice. The third is the bandit multiclass problem: a linear classifier predicts one of labels and then learns only whether its prediction was right. The goal is the mistake bound of the Banditron (Kakade, Shalev-Shwartz and Tewari, ICML 2008). The bound shows that one bit of feedback per round suffices to compete with every linear classifier, at regret .
There are arms (or labels) and rounds .
Adversarial losses. At round an adversary assigns losses to the arms and may adapt to the forecaster's past plays . The forecaster draws at random from a distribution that depends on what it has observed, and it observes only . Expectations are over the forecaster's draws.
Side information. Each round carries a context from a finite set , and the sequence is fixed in advance. The pseudo-regret against context-to-arm maps is
The S-Exp3 forecaster runs one instance of Exp3 (Section 3.1 of the book) on each context.
Expert advice. At each round each of experts proposes a distribution over arms, which may depend on the forecaster's past plays. The contextual pseudo-regret is
Exp4 (Fig. 4.1) runs exponential weights over the experts with importance-weighted loss estimates.
Bandit multiclass. The examples are fixed in advance, with (Euclidean). A matrix classifies by . Its multiclass hinge loss on round is . Write for the cumulative hinge loss, for its average, and for the Frobenius norm. The multiclass Perceptron predicts and, after seeing , adds to row and subtracts it from row . The Banditron (p. 58) predicts from . It observes only and updates , where . Its number of mistakes is .
For , , every example sequence as above and every matrix ,
Theorem 4.7 shows that, on any sequence of examples, the bandit version of online multiclass classification costs at most mistakes beyond the hinge loss of the best linear classifier. The full-information Perceptron, by comparison, pays . The bound has no stochastic assumption and has explicit constants. Theorems 4.1–4.3 are the basic regret guarantees for side information and expert advice. Theorem 4.3 in particular lets learning algorithms serve as experts inside Exp4, which is the construction behind Theorem 4.5.
The mission produces machine-checked statements, and eventually proofs, of these results with fully explicit constants and an explicit model of adaptive adversaries and adaptive advice. To the curators' knowledge none of the Banditron, the multiclass Perceptron bound, S-Exp3 or Theorem 4.3 is formalized anywhere. The platform's Bandit Algorithms series has a proved Exp4 bound, but only for advice and rewards fixed in advance. The book proves all four milestones and the goal; two printed statements (4.2 and 4.3) contain misprints that this mission corrects.
The Banditron bound concerns a randomized process whose weight matrix depends on all earlier random predictions. The Perceptron argument tracks and . It carries over only in conditional expectation, and the second moment of the importance-weighted update is of order on rounds where and of order otherwise. Combining these into one inequality for and then for requires solving a quadratic inequality in the presence of expectations, and the constants must come out as printed. For the Exp3/Exp4 results, the obstacle is that losses and advice adapt to past plays. The standard potential argument has to be run conditionally on the history, and a version that fixes the losses in advance proves a weaker theorem.
Fin K. The law of the first plays is the product over sequences , and expectations are finite sums against it. The adversary and the experts are deterministic functions of past plays; an independent randomized adversary is a mixture of these. The examples of the Banditron are fixed.Useful reusable infrastructure: the path-law expectation for history-dependent sampling, the exponential-weights potential argument under adaptive losses, and Perceptron-type inner-product arguments for matrices. Proofs of any milestone and of the goal are welcome.
Many controlled systems are judged by a ratio of two long-run quantities rather than by a single one: cost per unit of output, cost per unit of time when the time spent in a state depends on the decision, cost per customer served, or expected cost per cycle of a renewal process. In a finite Markov decision model each of these is a quotient of two average costs per unit time. Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (DOI 10.1287/mnsc.9.1.16) introduced this ratio-of-costs criterion in its §4, prompted by the fractional linear program that its §3 uses to solve the total-cost problem as a linear program, and pointed to Klein's work on maintenance policies as an example of the problem.
The paper's §4 first observes that, restricted to stationary randomized procedures, the ratio criterion is a ratio of two linear functions of the stationary state-decision frequencies, so it can be minimized by the fractional linear programming lemma of §3. The question it then raises is the one this mission formalizes: is the procedure optimal over stationary procedures also optimal over all procedures, including history-dependent and randomized ones? Derman's Theorem 3 answers yes under an irreducibility assumption, by reducing the ratio problem to a family of ordinary average-cost problems with costs of either sign.
Timeline, as far as it bears on this mission:
A system is observed at times in one of finitely many states . After each observation one of the decisions is made, all of them available in every state. If the system is in state and decision is made, the next state is with probability , where .
A procedure chooses the decision at time at random, with probabilities that may depend on the whole past; the class of all procedures is . The class consists of the stationary randomized procedures, for which the probability of in state is a fixed number , whatever the past and the time. The class consists of the deterministic stationary procedures, those of with every ; it is finite. A procedure of turns the states into a Markov chain with transition probabilities .
Let and be two sets of costs incurred when decision is made in state . For a fixed procedure started at , let and be the expected costs at time . The ratio criterion is
For a single cost set with expected costs , the average cost per unit time is .
Assumption A says that for every procedure of all states belong to the same class of the induced Markov chain.
Under Assumption A, for every initial state there is a deterministic stationary procedure with
that is, for every procedure .
Theorem 3 justifies solving ratio problems over stationary procedures only. Combined with the display of milestone 4 it shows that the fractional linear program over stationary state-decision frequencies yields a procedure optimal against every procedure, including those that remember the past or randomize. The same reduction, minimizing and adjusting , underlies later parametric methods for fractional Markov decision problems and the analysis of semi-Markov decision processes, where the denominator is the expected sojourn time.
All four steps and the theorem are classical and proved on paper. None of them is formalized on Prove2Me: the platform has average-cost optimality statements with nonnegative costs (Sennott's Proposition 6.2.3) and Jewell's gain-rate results restricted to stationary policies, but no statement of a ratio criterion over history-dependent procedures. This mission produces the statement of Theorem 3, the signed-cost version of Theorem 1 that it uses, and the two translation steps between the ratio criterion and the average-cost criterion.
The obvious argument restricts to stationary procedures, where all Cesàro limits exist and the ratio criterion is a ratio of two linear functionals of a stationary distribution. It says nothing about a history-dependent procedure, whose averages and need not converge, and for which the limit superior of the ratio is not the ratio of the limits superior. The translation from the ratio to an average cost therefore works in one direction for every procedure (milestone 2) and in the other direction only for stationary ones (milestone 3). The other ingredient, optimality of a deterministic stationary procedure for the average-cost criterion against all procedures with costs of either sign (milestone 1), is the substance of Derman's Theorem 1 and requires a vanishing-discount or equivalent argument over history-dependent procedures.
The dynamics and the procedures come from the published definitions SennottDP_AvgFinite_Model: the system is an MDC S Act with [Fintype S] [Fintype Act] and the hypothesis ∀ s, M.A s = Finset.univ (all decisions available); the class is Policy M, history-dependent and randomized; is StationaryPolicy M through .toPolicy; the law of the history is histProb. The cost field M.C of that structure plays no role: the costs , and the signed cost of milestone 1 are explicit real arguments S → Act → ℝ.
The local definitions are: the expected cost at time for a real cost, as a finite sum over histories of length ; with Derman's normalization ( terms divided by ); as the limit superior of the ratio of partial sums; the induced matrix ; Assumption A as Matrix.IsIrreducible of for every row-stochastic ; and membership of a procedure in with probabilities . All limits superior are real, of bounded sequences; positivity of and is a hypothesis of every statement involving , which keeps the denominators positive.
The goal quantifies "for every initial state there is ", following the proof. The competitors in the goal and in milestone 1 range over all of Policy M; a version comparing only with stationary procedures is a different and easier theorem and does not close this mission. Assumption A is kept in the goal although the proof does not visibly use it, because the theorem states it.
Contributions welcome: proofs of the milestones, in particular the signed-cost Theorem 1 (which may reduce to Sennott's Proposition 6.2.3 by shifting costs by a constant), Cesàro limits for stationary procedures on finite chains (reusable for milestones 3 and 4), and the final compactness argument over the finite class .
Resource-constrained project scheduling asks for start times of the activities of a project that respect precedence-type time lags and the capacities of renewable resources (machines, crews, equipment). Classical project scheduling minimizes the project duration, a regular objective: delaying an activity never helps. Many objectives met in practice are not regular. The resource investment problem minimizes the cost of the resource capacities that must be procured; resource levelling problems minimize fluctuations of resource usage over time; the resource renting problem trades fixed procurement against time-dependent renting costs; net present value and earliness–tardiness objectives reward late as well as early starts. For such objectives the familiar fact that "some active schedule is optimal" fails, and algorithms need another finite set of candidate schedules that is guaranteed to contain an optimum.
Chapter 3 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003, doi:10.1007/978-3-540-24800-2), organizes the objective functions of project scheduling into seven classes and pairs each class with a class of schedules that contains an optimal schedule. This mission formalizes §3.3 of that chapter. The classification goes back to Neumann, Nübel and Schwindt (2000) and Zimmermann (2001); the two locally defined classes, and the matching schedule classes of quasiactive and quasistable schedules, are the book's device for covering discontinuous resource-based objectives.
A project consists of activities , , where and are fictitious activities marking the project beginning and completion. Activity has an integer duration (, otherwise). The project network has an arc set with integer weights ; a schedule is a vector of real start times with , , and it is time-feasible if for all . A maximum project duration is prescribed through a backward arc of weight , so . Each renewable resource has capacity , activity uses units while in progress, and is the total usage at time . The feasible region consists of the time-feasible schedules with for all and .
For an objective function , problem asks for an optimal schedule: some with for all .
A schedule induces the strict order of precedences it realizes. The equal-order set of is
a polytope with part of its boundary removed. The distinct equal-order sets partition into finitely many pieces.
Schedule classes are defined through shifts. A shift from a feasible to a feasible is order-preserving if ; it is a left-shift if . Two shifts from to and are opposite if with . A feasible schedule is active if no feasible left-shift exists, quasiactive if no order-preserving left-shift exists, stable if no pair of opposite shifts to feasible schedules exists, and quasistable if no pair of opposite order-preserving shifts exists.
Objective classes: is regular if implies ; quasiconcave on a set if for , ; lower semicontinuous if on . Then is locally regular (class 6) if it is lower semicontinuous and regular on every equal-order set , , and locally quasiconcave (class 7) if it is lower semicontinuous and quasiconcave on every such set.
For every locally quasiconcave ,
Quasiactive and quasistable schedules are finite in number: they are the minimal points and the vertices of the finitely many schedule polytopes. Theorem 3.3.13 therefore turns the minimization of any locally quasiconcave objective over a disconnected, non-convex feasible region into a finite search. Class 7 contains the resource levelling objectives and , the total variation of the resource profiles, and the resource renting objective (Propositions 3.3.10 and 3.3.12, and Nübel 2001). The enumeration schemes and decision sets of §3.5–3.7 rest on this result, and Theorem 3.3.9 plays the same role for class 6 (resource investment, changeover times).
The results are proved in the book and the cited papers. As far as a search of the platform shows, none of them, and none of the schedule classes, has a machine-checked formalization; Mathlib supplies lower semicontinuity and quasiconcavity but nothing about schedules. The mission produces a checked version of the classification theorems in the book's exact generality: general time lags (cycles in the network allowed), real start times, and arbitrary objectives given only by their class.
The optimum need not exist a priori: objectives of classes 6 and 7 are discontinuous, and the feasible region is a finite union of polytopes that is in general disconnected. Existence of a minimizer needs compactness of (which depends on the deadline arc and the network's path structure) together with lower semicontinuity.
The main obstacle is that the objective is only controlled piecewise. Quasiconcavity holds on each equal-order set separately, and an equal-order set is not closed: a schedule polytope also contains schedules inducing strictly larger orders, where the hypothesis on says nothing about its relation to the values on . The obvious argument, taking an optimal schedule and invoking quasiconcavity along the segment of a pair of opposite order-preserving shifts, only relates at points of one equal-order set, and it does not by itself produce a schedule that admits no such pair at all. The same issue arises for Theorem 3.3.9 with order-preserving left-shifts, which may cross from one equal-order set into another.
Activities are Fin (n + 2), with 0 and Fin.last (n + 1) fictitious. Start times are real; objective functions are total functions (Fin (n + 2) → ℝ) → ℝ whose regularity, quasiconcavity and lower semicontinuity are required only on the nonnegative orthant (lower semicontinuity is Mathlib's LowerSemicontinuousOn on the orthant). The deadline is the network's backward arc, as in §3.1. The project structure records the book's standing property (p. 8) that from each node there is a path to of length at least ; this bounds every activity by . The resource constraints are imposed for all , which under that property is the book's . The peak in the resource investment objective is a supremum in over of a nonempty finite set, hence attained.
"Optimal" always means minimizing over the whole feasible region , and the theorems quantify over every function in the class; a formalization with a fixed objective, or with optimality over a single polytope or a single equal-order set, would be a different and weaker statement. The schedule classes are defined through shifts, never as minimal or extreme points, so no statement is true by definition. The only hypothesis besides the class of is .
The mission restates locally the project model, the induced orders and the shift classes also drafted by the companion missions on schedule classes of this series. Useful contributions beyond the milestones: compactness of and closedness of the schedule polytopes, the representation of as a finite union of feasible order polytopes, and the finiteness of the sets of quasiactive and quasistable schedules.
In bandit convex optimization a forecaster repeatedly picks a point of a convex set , and an adversary picks a convex loss . The forecaster pays and observes only that number: it never sees the function, its gradient, or its value elsewhere. This is the model of online optimization with only function-value access, as in tuning a system online from measured costs, dynamic pricing with an unknown convex demand-cost curve, or routing with path costs observed only on the route taken. The question is how fast the forecaster can approach the best fixed point in hindsight.
Chapter 6 of Bubeck and Cesa-Bianchi's monograph (arXiv:1204.5721v2, Foundations and Trends in Machine Learning 5(1), 2012) treats the problem through spherical gradient estimates fed to projected gradient descent. The one-point method is due to Flaxman, Kalai and McMahan (SODA 2005, arXiv:cs/0408007), who obtained an regret bound. Agarwal, Dekel and Xiao (COLT 2010) showed that two function evaluations per round allow . Whether one-point feedback admits regret was open when the monograph was written (p. 94); Bubeck, Eldan and Lee (STOC 2017, arXiv:1607.03084) later obtained regret up to logarithmic and polynomial-in- factors for convex losses, with a different and much more involved algorithm.
Let be the closed Euclidean unit ball and the unit sphere, with unnormalized spherical measure , so that . Fix . For a loss , the smoothed loss is with uniform on .
The set is closed and convex with . The losses are -Lipschitz, differentiable and convex, and are fixed before the game (an oblivious adversary).
OSGD (Online Stochastic Gradient Descent) on a set with learning rate starts at and sets , where is a gradient estimate. With independent and uniform on :
OSGD runs on the shrunken set , so that the perturbed points stay in . The pseudo-regret is
If in addition on , and , , then one-point OSGD satisfies
The bound shows that a single function value per round suffices for sublinear regret against any oblivious sequence of Lipschitz convex losses, with a forecaster whose only operations are a random perturbation and a Euclidean projection. The smoothing identity of Lemmas 6.1–6.2 is the basic tool of zeroth-order (derivative-free) optimization, used well beyond bandits, and Theorem 6.1 is the benchmark for two-point methods.
All results are proved in the source. To the best of current knowledge none is formalized: the related items of the Introduction to Online Convex Optimization series on Prove2Me (Hazan's Lemma 6.7 and Theorem 6.9) were formalized with missing hypotheses and are recorded as disproved. This mission produces machine-checked statements with every hypothesis explicit, and the formal infrastructure (sphere measure calculus, a projected stochastic gradient analysis) for later zeroth-order results.
Two steps resist a direct formal treatment. First, Lemma 6.1 is a divergence-theorem identity on the ball; Mathlib has the sphere measure and polar coordinates, but its divergence theorem covers boxes rather than balls, so differentiating the ball average in requires either such a theorem or a direct argument about translates of the ball. Second, the regret analysis takes expectations of quantities that depend on the whole past: the iterate is a function of , and unbiasedness holds only conditionally, via independence of from the past. A pathwise gradient-descent inequality must be combined with this conditional expectation round by round, with measurability of the projected iterates established along the way. The naive approach of treating the estimate as the true gradient of fails: it is a gradient of , and the gap is handled only by Eq. (6.2) and Lemma 6.3.
Points are in EuclideanSpace ℝ (Fin d) with ; rounds are , sums run over Finset.Icc 1 n. is Mathlib's Measure.toSphere of Lebesgue measure; the uniform laws are normalized restrictions. Randomness lives on an arbitrary probability space; the directions are measurable, mutually independent (iIndepFun) and uniform on , and in Theorem 6.1 the pairs are independent with a fair sign independent of . A run of OSGD is a predicate (start at , each iterate a Euclidean projection onto ), which determines the run uniquely, so the forecaster uses only observed values and its own randomness. The losses are Lipschitz, differentiable and convex on all of ; the bound is on , because a convex function bounded on is constant. The minimum over is an infimum over the subtype , attained in every theorem.
Conventions and corrections, each stated in the item's Formalization Note:
The statements cannot be satisfied trivially: the run is pinned by its recursion, the losses are fixed before the randomness, the expectations are of bounded measurable functions (no zero-valued Bochner integrals), and the minimum is over the nonempty compact . Section 6.3 (Lemma 6.4, Theorem 6.3) is not included, because its algorithm box and proof use different stage lengths and its unimodality condition is stated on a smaller set than the proof uses.
Needed infrastructure: calculus of ball averages and sphere integrals, symmetry of the uniform sphere law, nonexpansiveness of projections onto closed convex sets, and conditional-expectation bookkeeping for adapted iterates. Each is reusable for zeroth-order optimization; contributions of any of them as separate lemmas are welcome.
Classifiers trained on images, speech and text can be made to change their prediction by perturbations of the input that are tiny in norm (Szegedy et al., 2014). Empirical defences against such adversarial examples have repeatedly been broken by stronger attacks (Athalye, Carlini, Wagner, 2018), which motivates certified defences: classifiers that come with a proof that their prediction at a given input cannot change inside a stated ball around it.
Randomized smoothing turns any classifier, however large or opaque, into one with such a certificate in the norm. It was introduced with weaker radii by Lecuyer et al. (2019) and Li et al. (2018). Cohen, Rosenfeld and Kolter (arXiv:1902.02918v2, ICML 2019) proved the radius that is now standard, and showed it cannot be enlarged. Their guarantee underlies most later work on certified robustness, including Salman et al. (2019).
This mission formalizes the robustness guarantee, Theorem 1 of that paper. Page numbers below are PDF pages of the arXiv v2 preprint, which has no printed page numbers.
Inputs are points of with the Euclidean norm and inner product . Classes form a set . A base classifier is a deterministic or random function . A random is described by the probabilities , which for each form a probability distribution on .
Fix a noise level and let be isotropic Gaussian noise. The class probabilities at are , and the smoothed classifier is
The paper leaves undefined when the maximizer is not unique. "" therefore means that every class other than has strictly smaller probability.
Write for the standard Gaussian cumulative distribution function and for its inverse. is a real number on , and , .
Suppose that at a specific there are a class and numbers with
Then for every with , where
The statement covers every base classifier and every set of classes. The radius is infinite when or .
The milestones are the paper's own steps, in attack order:
Theorem 1 turns three numbers at one input into a guarantee over a whole ball: a lower bound on the top-class probability, an upper bound on the other classes, and the noise level. These bounds can be estimated by sampling and certified with confidence intervals (the paper's CERTIFY procedure). That is what lets randomized smoothing certify ImageNet-scale networks, where exact verification methods do not scale. The companion result (Theorem 2, a separate mission of this series) shows that no larger ball can be certified from the same information.
The theorem has a short pen-and-paper proof; no machine-checked proof of it is recorded on Prove2Me. A formal development adds:
Every step is classical, so the difficulty lies in the missing infrastructure, not in the idea.
EuclideanSpace ℝ (Fin d). is the pushforward of Mathlib's stdGaussian under , with a hypothesis.f : ℝᵈ → PMF 𝒴 with measurable class probabilities; deterministic classifiers are point masses. is an arbitrary type, with no finiteness assumed. The class probability is the published Gaussian smoothing RandomGradFree.Shared.smoothing, applied to .Contributions are welcome at every level: proofs of the milestones, and general lemmas such as the Gaussian density, the law of linear functionals of a Gaussian vector and properties of the normal quantile. These lemmas are reusable well beyond this mission.
Exact and heuristic methods for resource-constrained project scheduling do not search the whole continuum of start-time vectors. They enumerate a finite candidate set that is guaranteed to contain an optimal schedule. For machine scheduling and precedence-only project scheduling the classical candidate sets (semiactive and active schedules) are defined by shifting single activities earlier. With general time lags — minimum and maximum delays between the starts of activities — several activities can be rigidly tied together, and single-activity shifts no longer describe the right candidate sets.
Neumann, Nübel and Schwindt (Neumann et al. 2000) introduced shifts of sets of activities and four resulting classes of schedules: active, semiactive, pseudoactive and quasiactive. Section 2.4 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (Springer 2003), characterizes each class geometrically as the minimal points of a subset of the feasible region. The branch-and-bound procedures of §2.5 of the book enumerate exactly these objects: each enumeration node is a strict order together with the minimal point of its order polyhedron.
A project has activities ; and are fictitious activities marking the project beginning and completion, and are the real activities. Activity has an integer duration , with and otherwise. Time lags are the arcs of the project network with integer weights . A schedule is a vector of real start times with and . It is time-feasible if for all ; these schedules form the polyhedron .
There are renewable resources with capacity ; activity uses units while it is in progress. With the active set , a schedule is resource-feasible if for every and every . The feasible region is . It is in general neither convex nor connected.
A schedule induces the strict order . For a strict order , the order polyhedron is . is feasible if . is the schedule polyhedron of .
A left-shift from to means componentwise and . For feasible , the shift is global; it is local if a continuous trajectory joins to ; it is order-preserving if and order-monotone if or . A feasible schedule is active, semiactive, pseudoactive or quasiactive if no global, local, order-monotone or order-preserving left-shift, respectively, starts at it. A minimal point of is a point such that no satisfies , .
For a feasible schedule :
Part (a) is close to a restatement of the definitions. The content lies in (b), which passes from trajectories to connected components; in (c), which replaces a condition on shifts by a condition on finitely many polyhedra; and in (d), which reduces quasiactivity to a single polyhedron.
The characterization makes each schedule class checkable and enumerable. By (d), deciding quasiactivity is a longest-path computation in the schedule network. Deciding activeness is NP-hard (Neumann et al. 2000); the same holds for semiactive and pseudoactive schedules, which is why exact algorithms enumerate the quasiactive schedules. Remark 2.4.10 and Proposition 2.10.2 then give the two facts every such algorithm relies on: an optimal schedule lies among the (integer-valued) quasiactive schedules, and all of them fit into the horizon . Regular objective functions other than the project duration (§2.10) inherit the same candidate sets.
On the formal side, the mission produces a reusable model of with real start times and general time lags: time-feasible and resource-feasible schedules, schedule-induced orders, order polyhedra and the four schedule classes. No part of this material is formalized on Prove2Me or, as far as is known, anywhere else. The results are all proved in the literature (Neumann et al. 2000; the book gives proofs or calls them obvious); the work here is to formalize them.
The obvious argument for (b) says "a trajectory stays in one component, so local shifts move within components". The converse needs that two schedules in the same connected component of are joined by a path inside . That is false for general sets and has to come from the structure of as a finite union of order polyhedra (the basic structural theorem of Bartusch, Möhring and Radermacher), which is not part of this mission's statements and must be proved on the way.
For (c), the difficulty is that an order-monotone shift may shrink the order . The proof has to produce, from a feasible sub-order whose polyhedron has a smaller minimal point, a shift that is short enough to keep every overlap of . This requires the resource feasibility of whole order polyhedra, i.e. that for feasible . Resource feasibility is a condition on all times , while the orders only record pairwise relations between activities.
Activities are Fin (n + 2), with 0 and Fin.last (n + 1) the fictitious ones. Durations are natural numbers, arc weights integers, and start times real. Resource requirements and capacities are natural numbers. The resource constraints hold for every ; (2.1.4) writes , but the book's proofs use the unrestricted form. Minimal points are Mathlib's Minimal for the componentwise order on Fin (n + 2) → ℝ. Components in (b) are connected components (connectedComponentIn), while local shifts are defined by continuous trajectories from the unit interval, as in Definition 2.4.3. The theorem is stated for feasible , since the schedule classes consist of feasible schedules by definition. The lower bound is a vector of real infima and is used only for nonempty order polyhedra.
Defining "active" as "minimal point of ", or any class through its right-hand side, would make the goal trivial. That is ruled out: every class is defined through the shifts of Definitions 2.4.1–2.4.6, including the trajectory condition and the orders .
Remark 2.4.8 (the minimal point of is the vector of longest path lengths in ) is not stated, since it needs path lengths and the reachability conventions of Remarks 1.1.2. Contributions of that network layer, and of the structural theorem (Theorem 2.3.7), are welcome as supporting lemmas.
For a real-analytic function on an open set and a critical point (so ), the Łojasiewicz gradient inequality says that there is an exponent such that stays bounded near . It is the standard tool for proving that bounded gradient trajectories have finite length and converge to a single critical point, and, in its descendants (the Kurdyka–Łojasiewicz property), for proving convergence of the whole iterate sequence of nonconvex descent methods: proximal gradient, alternating minimization, PALM, ADMM. Those algorithmic results all assume a nonsmooth version of the inequality, for functions that may take the value and are not differentiable.
Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007)) supplied that nonsmooth version. This mission formalizes their first main result, Theorem 3.1: the inequality at critical points of subanalytic functions that are continuous on a closed domain.
Timeline.
Write with its Euclidean norm. A function has domain .
Subanalytic sets (Definition 2.1). A set is semianalytic if every point of has a neighbourhood on which with real-analytic on . It is subanalytic if every point of has a neighbourhood such that is the projection onto of a bounded semianalytic subset of , . A function is subanalytic if its graph is subanalytic. Semialgebraic functions, and functions locally built from analytic ones by finitely many algebraic operations, max/min and compositions, are subanalytic.
Subdifferentials (Definition 2.10). The Fréchet subdifferential is the set of with (empty off ). The limiting subdifferential is the set of limits of along with .
Slope and critical points. The nonsmooth slope is , equal to when (equation (4)). The critical set is (Definition 2.11).
Let be subanalytic with closed domain and continuous, and let . Then there is such that
with the conventions and . In division-free form: there are and a neighbourhood of with for all and . The exponent is existential; the goal fixes no value of or .
The result. Theorem 3.1 is the nonsmooth Łojasiewicz inequality at critical points. With the subgradient in place of the gradient, it yields finite length of bounded trajectories of subgradient systems (Section 4 of the paper) and is the template for the Kurdyka–Łojasiewicz property that underlies convergence proofs for proximal and splitting methods on nonconvex, nonsmooth problems (e.g. Attouch–Bolte–Redont–Soubeyran 2010, Bolte–Sabach–Teboulle 2014). Those papers assume the KL property and cite this line of results to know it holds for semialgebraic and subanalytic objectives.
Formalizing it. The theorem is proved; this mission produces a machine-checked proof. To our knowledge no proof assistant has a formal definition of subanalytic sets or of the nonsmooth Łojasiewicz inequality. The definitions layer (semianalytic and subanalytic sets, the slope, the inequality) is reusable by any later formalization of KL-based convergence analyses, and the milestones on Remark 2.12 are general facts about limiting subdifferentials that apply well beyond subanalytic geometry.
The obvious argument restricts and to an analytic curve and compares their Puiseux expansions. That step needs three pieces of subanalytic geometry that no library has: curve selection, the structure of one-variable subanalytic functions (monotonicity and Puiseux expansions), and the fact that the sets built in the proof (sets of points with a subgradient satisfying an inequality, level-wise infima of ) are again subanalytic, which in the paper goes through global subanalyticity and the projection theorem. The second obstacle is that is not smooth: the classical proof differentiates along a curve, while here only Fréchet subgradients are available, and the chain rule along an analytic curve holds only almost everywhere. The constancy of on critical components, equation (6), is itself a nonsmooth Sard-type theorem whose published proof uses stratification. A solver who replaces subanalytic by semialgebraic, or assumes real-valued and , proves a different and much weaker statement.
EuclideanSpace ℝ (Fin n). The function is f : E → EReal with f x ≠ ⊥ for every x. The domain is {x | f x ≠ ⊤}; it is assumed closed, and f is assumed ContinuousOn it.NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff, which match Definition 2.10 for functions never equal to .AnalyticOnNhd ℝ. The boundedness of the semianalytic set in Definition 2.1(ii) is part of the definition: without it every projection of a semianalytic set would count.LojIneqAt f a θ: one constant and one neighbourhood of , quantified over all limiting subgradients. Under the value never works at a critical point, as under the paper's conventions.A learning algorithm is judged by its generalization error, its expected loss on a fresh example, which cannot be computed because the data distribution is unknown. Practitioners estimate it either by the empirical error on the training set or by the leave-one-out error, which retrains the algorithm once per example. Classical learning theory justifies these estimates through uniform convergence over the whole hypothesis space (VC dimension, covering numbers). That route says nothing useful about algorithms such as nearest-neighbour rules or regularized kernel methods, whose effective hypothesis space is huge or unknown.
An alternative is to bound the deviation through a property of the algorithm itself: how much its output changes when one training example is removed. This idea goes back to Rogers and Wagner (1978) and Devroye and Wagner (1979) for local rules, and Kearns and Ron (1999) gave it a name. Bousquet and Elisseeff (JMLR 2002) systematized it with several stability notions and corresponding bounds; their paper is the standard reference for algorithmic stability in learning theory. This mission formalizes its first family of results, the polynomial bounds of §4.1.
Let and let be a probability distribution on . A training set consists of examples drawn i.i.d. from . A learning algorithm maps a training set to a hypothesis ; it is deterministic and symmetric, meaning it does not depend on the order of the examples. A cost with defines the loss of a hypothesis at .
For each index , is with removed, and is with replaced by an independent fresh draw . The three error quantities are
Two stability notions (Definitions 3 and 4) control them. has hypothesis stability if for every , and pointwise hypothesis stability if for every .
For , under hypothesis stability and pointwise hypothesis stability , for every , each of the following holds with probability at least over :
Theorem 11 is the weakest-assumption bound in the paper: it requires only average-case stability, not the uniform (worst-case) stability behind the exponential bounds of §4.2. It shows that both the resubstitution and the deleted estimate are within of the risk whenever the stability parameters decay like , with no reference to the size of the hypothesis class. It also extends Devroye and Wagner's leave-one-out analysis for classification to bounded regression losses and to the empirical estimator. Later work on average stability and on generalization of stochastic gradient methods (for example Hardt, Recht and Singer, 2016) starts from these notions.
The result is proved in the paper; as far as is known it has no machine-checked proof. A formal development has two concrete payoffs. First, it fixes the constants: in checking the argument, two printed slips were found (the empirical constant in Theorem 11 and the third term of Lemma 25's first inequality), and the formal statements record the versions that the paper's proof actually establishes. Second, the Lemma 25 and Lemma 9 machinery — exchangeability of i.i.d. samples under renaming, and second-moment control through stability — is reusable for any later stability result.
The obvious route is the Efron–Stein (Steele) variance inequality, Theorem 1 of the paper. It bounds the variance of , not its second moment, and leaves the bias to be handled separately; the paper notes that it gives worse constants. The direct route of Appendix A instead expands and rewrites each correlation term by renaming i.i.d. variables: training points, fresh test points and replacement points are exchanged with one another, and the algorithm is retrained on sets with . Every renaming is a measure-preserving map on a product of copies of , and each must be justified by the symmetry of . Doing this rigorously, rather than as "a matter of renaming", is the core of the work. The leave-one-out case is only sketched in the paper ("it is easy to see"), so its formal proof has to be reconstructed.
Multiset (X × Y) → (X → Y'). Symmetry in the training set is built into the type, and the same algorithm acts on sets of every size, as and require. A sample is S : Fin m → X × Y with law (Measure.pi); fresh points , , are further independent coordinates, via product measures and .FoundationsML.Stability definitions (Loss, EmpiricalError, GeneralizationError).Contributions are welcome at every level: proofs of the milestones, a general exchangeability lemma for symmetric algorithms on product measures, and Markov/Chebyshev glue for the final step.
Learning from a finite sample is useful only if changing the sample has a controlled effect on the learned predictor. Uniform stability asks for a bound on the change in loss at every test point when one training example is removed. Bousquet and Elisseeff use this property to obtain generalization bounds for learning algorithms, and identify regularization as a source of stability in methods built from reproducing kernels. The present mission isolates their result for a squared norm penalty in a reproducing kernel Hilbert space (RKHS). It concerns the sensitivity of the optimizer itself, before any probability bound on a random training sample is applied. The result is Theorem 22 of Bousquet and Elisseeff (2002).
Let be an input space, a label space, and a real reproducing kernel Hilbert space of real-valued predictors on . A kernel and a feature representative express the reproducing identity and . Thus . The source assumes that all diagonal kernel values satisfy .
A labeled example is . Its loss under is , where is a real-valued cost. Let be the set of predictions that some element of can produce at some input. The loss is -admissible when is convex for every label and for all and . Here is a nonnegative Lipschitz constant. The definition compares any two attainable predictions, even when they arise at different inputs.
Fix a sample , a deleted index , and a regularization weight . The paper's full and truncated objectives, with squared RKHS norm regularization, are
The factor in both objectives is . Let and be minimizers of these respective objectives over all of . The statements allow any minimizer satisfying the relevant global optimality condition; they do not choose one by an arbitrary fallback rule.
The central target is the explicit deletion stability estimate of Theorem 22. For every test point ,
Its four milestones follow the paper's route through Lemma 20, the point-evaluation inequality (25), and the two quantitative inequalities displayed in the proof of Theorem 22. In particular, the intermediate RKHS distance bound is when . The main theorem uses , so it does not need a choice of sign for . These numerical constants are part of the target, rather than placeholders for unspecified bounds.
The theorem supplies a deterministic, uniform sensitivity estimate for kernel methods trained by squared norm regularization. The bound applies simultaneously to every test example and decreases as either the sample size or the regularization weight increases. It is one of the ingredients that lets the paper apply its earlier stability-to-generalization results to concrete learning procedures. The loss need not be bounded for this theorem; bounding it is a separate question addressed later in the paper.
The result is proved in the source article. This mission asks for a machine-checked version of its exact pairwise claim and the reusable infrastructure around it: the paper's admissibility condition, the two objectives, the general regularizer inequality, and the RKHS evaluation bound. The existing Prove2Me library already has definitions for loss, empirical error, and the RKHS reproducing identity, so the new definitions concentrate on what is specific to these pages. The related replace-one estimate in Mohri, Rostamizadeh and Talwalkar's Foundations of Machine Learning uses a different perturbation and constant; it is not interchangeable with this result.
The two minimizers solve different objectives, and the deleted example appears in only one of them. A comparison of their objective values alone does not directly give a bound on their distance in the Hilbert norm. The source also distinguishes an abstract convex class of functions in Lemma 20 from the full RKHS used in Theorem 22. A proof must keep those domains straight while preserving the precise normalization of the truncated objective. Another delicate point is that the kernel bound controls evaluations through the reproducing identity; a bound on is not by itself a bound on loss unless the admissibility condition is also used.
The Lean model uses an abstract complete real inner product space , an evaluation map , a feature map , and the published IsRKHSOf predicate tying these to . The completeness instance matches the source's Hilbert-space assumption. Samples have type Fin m → X × Y, so an index i : Fin m already forces . Minimization ranges over the entire for Theorem 22 and over the declared convex class for Lemma 20. The objective definitions use the published Loss and EmpiricalError objects. No probability measure or measurability assumption is needed for these deterministic assertions.
There is a printed mismatch that affects what “deletion” means. Theorem 22 names an algorithm defined by equation (26), which, run afresh on points, would normalize its data term by . Lemma 20 and the proof of Theorem 22 instead compare the full objective with equation (20), whose data term uses . The formalized goal states that comparison, with its explicit constant, and records the discrepancy for audit. This excludes the tempting shortcut of treating the two normalizations as identical. The regularizer is the genuine squared norm and the second minimizer is required to minimize the genuine truncated objective; neither a restricted hypothesis ball nor an artificially assumed distance bound enters the goal. Contributions that establish minimizer existence or connect the pairwise bound to an algorithmic selection would extend this core without changing its statement.
Eligibility traces are one of the basic mechanisms of reinforcement learning. A trace is a short-term memory vector with one component per weight. It records which components contributed to recent value estimates, so that an error observed now can be credited to the right components without storing the past. Chapter 12 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., 2018) organizes the topic around two ways of describing an algorithm. A forward view updates each state toward a target built from rewards that arrive later. A backward view makes an update at every step from the current error and the trace.
The chapter proves one exact equivalence between the two views itself, in §12.6: "This is the only equivalence of forward- and backward-views that we explicitly demonstrate in this book" (p. 301). The setting is linear Monte Carlo prediction, and the backward view uses a dutch trace. The same trace appears in true online TD(), whose exact equivalence to the online -return algorithm (van Seijen and Sutton, 2014; van Seijen et al., 2016) the book cites without proof. Of that proof, §12.6 "gives some of the flavor ... but is much simpler" (p. 301).
The older equivalence of §§12.1–12.2 goes back to Sutton (1988). If the weights are held fixed during an episode, the summed updates of TD() with accumulating traces equal the summed updates of the off-line -return algorithm. The book leaves it as Exercises 12.3–12.4.
Fix a dimension , a step size and an episode of length with feature vectors . The episode ends with a single return ("a single reward received at the end of the episode ... and ... no discounting", p. 301). The forward view is the linear gradient Monte Carlo, or LMS, rule (12.13): from an initial ,
Let be the fading matrix. The backward view keeps two vectors that are updated at each step in time without knowledge of . The dutch trace is , . The auxiliary vector is , with .
For the second part, an episode carries states and rewards, and is a differentiable value function with . For one fixed weight vector , define the following, with and :
The left side is the forward view after LMS updates. On the right, and are produced by the incremental recursions above. The goal is about the two algorithms, not only about the closed-form product identity.
The goal says that an -per-step algorithm reproduces the Monte Carlo/LMS result exactly. That algorithm never stores the feature vectors or the intermediate weight vectors. The book draws the conclusion that eligibility traces "are not specific to TD learning at all" (p. 303). The dutch trace in the case is the same object that true online TD() (12.11) uses for general . The fading-matrix products and their incremental forms are therefore the vocabulary of any later formalization of true online TD() and of the online -return algorithm.
Exercises 12.3–12.4 are the fixed-weight equivalence of TD() and the off-line -return algorithm. They are the standard justification for calling TD() an approximation of the -return algorithm. Exercise 12.1 and (12.3) are the identities the rest of the chapter uses to manipulate -returns.
On status: all of these results are known and elementary on paper, and the book prints the derivation of (12.14). To our knowledge none of them has a machine-checked proof, and the platform has no statement about -returns, eligibility traces or TD(). What this mission adds is formal statements with every convention fixed, including one correction to the printed text. It also adds reusable definitions of -step returns, -returns and traces.
The algebra is elementary. The difficulty lies in the conventions, and a careless reading of the page produces a false statement. The book initializes , and taken literally that makes the goal false. The -return is an infinite series, whose tail collapses only because every -step return that reaches past termination equals the full return. That convention has to be built into the definition of , together with the terminal value . Exercises 12.3 and 12.4 are true only when the weights stay fixed. With the algorithms' changing weights the -step returns (12.1) use , and neither identity holds. The boundary indices (, the empty product at , ) must come out right.
Namespace SuttonBartoRL.Traces. Vectors of §12.6 are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and is Matrix.vecMulVec x x. The ordered product fadeProd α x j t is , the identity when . Feature sequences are indexed by ; only enter. is a hypothesis wherever appears. The identities of §12.6 are stated for every real and , a harmless strengthening of the book's positive step size.
For §§12.1–12.2, weights are EuclideanSpace ℝ (Fin d), is Mathlib's gradient, and each is assumed differentiable in Exercise 12.4. An episode is a length , states and rewards. The value at time is . (12.2) is a tsum over of , and , the range the book gives with (12.2). Milestone 5 concludes summability, so the junk value of a divergent tsum cannot make it trivial. Exercises 12.3–12.4 take one weight binder w, used in every return, TD error and gradient. That is the book's fixed- assumption, stated in the binders.
Correction. The printed initialization (p. 302) contradicts the printed definition and (12.14). The counterexample is , , , , , : the forward view gives , while . The mission states the corrected result with , equivalently the same recursion started from . The printed text is kept verbatim in the milestone.
A trivializing formalization is ruled out: the goal is not the closed-form identity with and defined as the products and sums. Those vectors are defined by their -free incremental recursions, and the closed forms are separate milestones.
Out of scope: the equivalence of true online TD() and the online -return algorithm (cited, p. 300), the truncated-return identity (12.10), the error bound (12.8), and all convergence claims. Proofs of the milestones, and reuse of the definitions in later missions on true online TD(), are welcome.
Stochastic approximation algorithms are recursions driven by small steps and noise ; they include the Robbins–Monro scheme, stochastic gradient methods and learning dynamics in games. The ODE method studies their long-run behaviour by comparing a time-interpolation of the iterates with the trajectories of a deterministic dynamical system. In Benaïm's lecture notes (Benaïm 1999) this comparison is formalized by the notion of an asymptotic pseudotrajectory, introduced in Benaïm and Hirsch (1996): a path that, over every window of fixed length, shadows the deterministic orbit started at its current position with an error that vanishes as time goes to infinity.
The pathwise results of the earlier sections of the notes concern algorithms whose step sizes decrease fast enough, typically or . When the step sizes go to zero more slowly, the limit sets of the process can no longer be characterized precisely: with steps of order the process may fail to converge even when the chain recurrent set of the ODE consists of isolated equilibria. Section 10, which is mainly based on work of Benaïm and Schreiber, describes instead the statistical behaviour of such processes in terms of the deterministic dynamics. It introduces a weaker, conditional notion, the weak asymptotic pseudotrajectory, and proves in Theorem 10.1 that the empirical distribution of the time spent by the process in different regions of the state space accumulates only on invariant measures of the deterministic dynamics. This is an ergodic-theoretic counterpart of the limit-set theorems of Section 5.
A semiflow on a metric space is a continuous map , , with and for . Throughout, is a separable metric space with its Borel -algebra.
Let be a probability space and a nondecreasing family of sub--algebras. A process is a weak asymptotic pseudotrajectory of if
Let be the space of Borel probability measures on with the topology of weak convergence. A measure is -invariant if for every ; the set of invariant measures is . The occupation measure of the process at time is the random probability measure
and is the set of its weak limit points as .
If is a weak asymptotic pseudotrajectory of , there is a set with such that for all
No tightness is assumed, so may be empty; the statement asserts the inclusion, not nonemptiness.
Fix a uniformly continuous and , and set for . The milestones are the numbered displays of the proof on pp. 62–63:
The result. Theorem 10.1 locates the long-run statistics of a stochastic process that only shadows a deterministic semiflow in conditional probability. When the occupation measures are tight, for example when the path has compact closure, is nonempty, and the theorem restricts where the process spends its time to the supports of invariant measures. Right after the theorem the notes define the minimal center of attraction of the process from the supports of the measures in ; the conclusion applies to processes, such as slowly decreasing step-size algorithms, for which the pathwise limit-set theorem of Section 5 is not available.
Formalizing it. The theorem has a complete published proof. No machine-checked version of it, of weak asymptotic pseudotrajectories, or of occupation-measure limit theorems for continuous-time processes is known to exist. The mission produces a formal definition of progressively measurable weak asymptotic pseudotrajectories, occupation measures of measurable paths and their weak limit points, and a proof that combines a martingale law of large numbers in discrete time with weak convergence in .
The obvious route is to apply the pathwise argument for asymptotic pseudotrajectories along each path. It fails, because condition 2 controls only conditional probabilities: the deviation events may occur infinitely often along almost every path while their conditional probabilities tend to zero. The proof therefore has to work with averages and conditional expectations instead of with individual paths: a strong law of large numbers for bounded martingale differences transfers conditional statements to time averages, and this must be done for one test function and one horizon at a time. Passing from countably many test functions to invariance requires a countable family of uniformly continuous functions that determines weak convergence on the separable space , and the a.s. sets must be intersected over that family and over rational horizons. Measurability is a second difficulty: paths are not assumed continuous, so the integrals, suprema and conditional expectations involved must be shown to be well defined from progressive measurability alone.
Time is ; the semiflow is Mathlib's Flow ℝ≥0 M; the filtration is a Filtration ℝ≥0; is ProbabilityMeasure M with its topology of weak convergence. is a separable metric space with its Borel -algebra; it is not assumed compact, complete or Polish. Progressive measurability is stated literally for every . The conditional probability in condition 2 is the conditional expectation of the indicator of the deviation event, which is required to be measurable (the paper's presupposes an event); the supremum over is taken in . Invariance for the semiflow is for all , the form the proof establishes; for a flow it agrees with the definition of Section 8.3. Weak limit points are cluster points of as ; the occupation measure is a genuine probability measure for every measurable path and .
The following formalizations would trivialize the statement and are excluded by the definitions: an "occupation measure" equal to the zero measure for a non-measurable path; a conditional probability of a non-measurable event, which Lean evaluates to and which would make condition 2 vacuous; invariance defined through images , which need not be Borel for a semiflow; and a compactness or Polish assumption on , which the theorem does not make.
A complete development needs: Fubini-type measurability for progressively measurable processes, square-integrable martingale convergence and Kronecker's lemma (both largely in Mathlib), conditional expectations of time integrals, a convergence-determining countable family of uniformly continuous functions on a separable metric space, and the identification of weak convergence with convergence of integrals of bounded continuous functions. The martingale law of large numbers (Eqs. (47), (50)) and Eq. (53) are reusable outside this mission. Proofs of any milestone, and alternative arguments for the goal, are welcome.
A stochastic approximation algorithm updates an estimate by small noisy steps, , with step sizes and noise . Such recursions underlie stochastic gradient descent, adaptive control, reinforcement learning (Q-learning, temporal-difference methods) and learning in games (fictitious play, reinforcement models). The ODE method compares the long-run behaviour of the algorithm with that of the ordinary differential equation . Classical versions of this comparison (Ljung 1977, Kushner and Clark 1978) assume the ODE has a globally asymptotically stable equilibrium, or a Lyapunov function, and cannot describe algorithms whose ODE has periodic orbits, heteroclinic cycles or chaotic sets.
Benaïm and Hirsch (1996) replaced these special assumptions by a single dynamical statement: the interpolated algorithm is an asymptotic pseudotrajectory of the flow of , and the limit set of every precompact asymptotic pseudotrajectory is internally chain transitive. This mission formalizes that limit set theorem as it is presented in Michel Benaïm's lecture notes Dynamics of Stochastic Approximation Algorithms (Séminaire de Probabilités XXXIII, 1999).
Timeline. Bowen (1975) and Conley (1978) introduced -pseudo-orbits and chain recurrence, and Conley proved that the chain recurrent set of a flow on a compact space is internally chain recurrent. Benaïm (1996, SIAM J. Control Optim.) related limit sets of stochastic approximation processes to the chain recurrence of the ODE; Benaïm and Hirsch (1996) introduced asymptotic pseudotrajectories for semiflows on metric spaces and proved the limit set theorem in the form formalized here. The 1999 notes give a self-contained proof through the translation semiflow on a space of curves.
Let be a metric space. A semiflow on is a continuous map , , with and . A set is invariant if for every ; then denotes the restricted semiflow on .
A continuous curve is an asymptotic pseudotrajectory of if
and it is precompact if has compact closure. Its limit set is .
For , , a -pseudo-orbit from to consists of partial trajectories, given by points (and an endpoint ) and times with , for , and . One writes if such pseudo-orbits exist for all . A nonempty compact invariant set is internally chain transitive if for the restricted semiflow for all , so that all lie in ; it is internally chain recurrent if for for every . An attractor is a nonempty compact invariant set with a neighbourhood such that uniformly in .
For every semiflow on a metric space and every precompact asymptotic pseudotrajectory of ,
The result. Theorem 5.7 (i) is the bridge between probability and dynamics in the ODE method. Once a stochastic approximation process is shown to be an asymptotic pseudotrajectory (missions 2 to 4 of this series do that under martingale-noise conditions), every statement about its limit points becomes a statement about internally chain transitive sets of the ODE: convergence to equilibria when a Lyapunov function exists (Proposition 6.4), convergence to attractors with positive probability (Theorem 7.3), and the analysis of learning dynamics in games. The theorem is sharp in the sense that every internally chain transitive set is a limit set of some asymptotic pseudotrajectory (Theorem 5.7 (ii), proved in Benaïm and Hirsch 1996 and not part of this mission).
Formalizing it. The result is proved in the literature; it is not formalized. Mathlib has semiflows (Flow), omega limit sets and the compact-open topology, but no pseudo-orbits, chain recurrence, Conley's theory of attractors, or asymptotic pseudotrajectories. This mission produces that layer for semiflows on general metric spaces, which is reusable for any later formalization of the ODE method, of Conley theory, or of learning in games.
The obvious approach follows from a point to a point : returns near and near infinitely often, and on windows of length it is close to a trajectory, so concatenating windows gives a pseudo-orbit. The pseudo-orbit obtained this way has its points on the curve , not in ; this only shows that is chain transitive for on , a strictly weaker property. Producing pseudo-orbits whose points lie in itself is the central difficulty, and it is where precompactness of is used. Invariance , with equality, also needs a compactness argument, since a semiflow is not invertible.
A semiflow is Mathlib's Flow ℝ≥0 M on a [MetricSpace M]; is arbitrary, with no compactness, completeness or local compactness. Time is ℝ≥0. Curves are functions ℝ≥0 → M; continuity is part of being an asymptotic pseudotrajectory, and precompactness is IsCompact (closure (Set.range X)). Invariance is equality . Internally chain recurrent and internally chain transitive sets are nonempty by definition, and their pseudo-orbits are those of the restricted semiflow on the subtype , so every point of the pseudo-orbit lies in . Attractors converge uniformly on a neighbourhood. Lemma 3.1 and Theorem 3.2 are stated on (C(ℝ≥0, M), compact-open topology) with the half-line distance; the notes write , but with the convention for that version fails for semiflows (a periodic trajectory is a counterexample), and the notes themselves describe asymptotic pseudotrajectories as points of .
Ruled out: pseudo-orbits with no trajectory piece (), pseudo-orbits allowed to leave , invariance as mere inclusion , and any compactness assumption on . Each of these makes the goal weaker than the theorem of the notes.
A complete development needs: elementary properties of pseudo-orbits (concatenation, continuity estimates), Arzelà–Ascoli on C(ℝ≥0, M), Conley's attractor construction, and the conjugacy between and the translation semiflow on . Proofs of the milestones, alternative direct proofs of the goal (Benaïm 1996), and reusable lemmas about chain recurrence for Flow are all welcome.
A stochastic approximation algorithm is a recursion
in , driven by a vector field , decreasing step sizes and perturbations . Robbins–Monro root finding, stochastic gradient descent, adaptive filters, learning dynamics in games (fictitious play, reinforcement learning) and urn models all have this form. The ODE method, introduced by Ljung (1977) and developed by Kushner and Clark (1978), Métivier and Priouret (1987) and Kushner and Yin (1997), studies such a recursion by comparing it with the differential equation .
Benaïm and Hirsch (1996) gave the comparison a dynamical form: the continuous-time interpolation of is an asymptotic pseudotrajectory of the flow of . Proposition 4.1 of Benaïm's lecture notes (Séminaire de Probabilités XXXIII, 1999) states that deterministic comparison theorem under two assumptions: a noise condition (A1) and either bounded iterates (A2) or a Lipschitz, bounded vector field near the iterates (A2′). The notes then verify A1 almost surely for martingale noise (Propositions 4.2 and 4.4) and use the asymptotic pseudotrajectory property to describe limit sets, attractors and nonconvergence.
Let be continuous. It is globally integrable if through every point there is exactly one integral curve , ; the flow is the value at time of the integral curve through .
The step sizes satisfy , and . Set , , and . The affine interpolated process and the piecewise constant processes are, for ,
The noise enters through
A continuous is an asymptotic pseudotrajectory of if for every
No rate and no constant appear; the statement holds under either alternative.
with depending only on and on (through its Lipschitz constant and bound on the neighbourhood).
Proposition 4.1 separates the dynamics of a stochastic approximation algorithm from its noise. Any noise condition implying A1 almost surely (Propositions 4.2 and 4.4 of the notes for -bounded and subgaussian martingale differences) combines with it to give: almost every sample path, after interpolation, is an asymptotic pseudotrajectory of . The limit set theorem (Theorem 5.7: limit sets are internally chain transitive), the Lyapunov-function criterion (Proposition 6.4) and the attractor results (Section 7) then apply path by path. Estimate (11) gives the quantitative version used for rates.
The result is proved in the notes, building on Benaïm and Hirsch (1996). No machine-checked proof of it, or of the asymptotic pseudotrajectory framework, is known to exist. A formal proof would supply a checked bridge between discrete recursions with step sizes and flows of vector fields, which every ODE-method convergence proof crosses.
The obvious argument compares directly with the flow by Gronwall's inequality. It needs Lipschitz along both the interpolated path and the flow line, which holds under A2′ but not under A2, where is only continuous and solutions are unique without any Lipschitz bound. Under A2 the comparison must go through compactness instead: equicontinuity of the translates, identification of every limit point as an integral curve, and uniqueness of integral curves. The last step is where global integrability is used, and it cannot be replaced by a quantitative estimate.
Under A2′ the iterates may be unbounded, so no compactness is available, and the path and the flow line must be kept inside the region where is controlled for the whole window .
EuclideanSpace ℝ (Fin d); time is ℝ≥0 for the pseudotrajectory and ℝ inside integrals. Sequences are ℕ → · with the paper's indices; and are unused.Trivializing formalizations are ruled out: the goal keeps both alternatives A2 and A2′ (neither a global Lipschitz condition nor bounded iterates is assumed in place of the disjunction), is the explicit piecewise affine interpolation rather than any curve with the desired property, and the constant in (11) is fixed before the sequences, so it cannot depend on the run.
A complete development needs Gronwall's inequality (in Mathlib), Arzelà–Ascoli on , continuous dependence of solutions on initial data under uniqueness (Kamke's theorem, not in Mathlib), and interval integrals of step functions. The asymptotic pseudotrajectory definitions and Theorem 3.2 are reusable for the other missions on these notes. Proofs of individual milestones are welcome; Eq. (9) and the comparison of and are the natural entry points.
Classical generalization bounds for classifiers, built on the VC dimension, grow with the number of adjustable parameters. For neural networks this is at odds with practice: networks with many more weights than training examples often generalize well. Bartlett's 1998 paper (IEEE Trans. Inform. Theory 44(2), 525–536) explains part of this by measuring a real-valued classifier's confidence. If a hypothesis classifies most training examples correctly with a margin , its misclassification probability is controlled by a scale-sensitive dimension of the class at scale proportional to , not by its VC dimension. Later in the paper this yields bounds for networks with small weights that do not depend on the number of weights.
This mission formalizes the first of the paper's two main technical results, the margin bound of Theorem 2 (p. 527), together with the steps of its proof on pp. 527–528.
The fat-shattering dimension was introduced by Kearns and Schapire (JCSS 1994). Alon, Ben-David, Cesa-Bianchi and Haussler (J. ACM 1997) proved the scale-sensitive Sauer-type covering bound used here (Theorem 5 of the paper). Shawe-Taylor, Bartlett, Williamson and Anthony (IEEE Trans. Inform. Theory 1998) proved the zero-training-error version (Theorem 1 of the paper). Theorem 2 extends it to hypotheses that make margin errors on the training data.
Let be a set and a probability distribution on . The threshold function is for and for . For a real-valued hypothesis on , the misclassification probability is . For a sample drawn independently from and , the margin error estimate is
Let be a class of real functions on . Points are -shattered by if some has the following property: for every sign vector , some satisfies for all . The fat-shattering dimension is the largest such , possibly .
The proof uses the following objects:
Assume , , , and finite with . With probability at least over , every satisfies
A further item, Proposition 8 (p. 529), is the probabilistic device the paper uses to make such bounds uniform over .
Theorem 2 is the bound behind the paper's main message. Corollary 9 makes it uniform over , and Theorem 28 combines it with fat-shattering estimates for networks with bounded weights. Together they show that a network classifying the training data with a large margin generalizes at a rate governed by the size of its weights, not by its number of weights. The same template, a margin error plus a capacity term at scale , underlies later margin analyses of support vector machines and boosting.
All results in this mission are proved in the literature; none is open. None is machine-checked on this platform: the platform has Rademacher-complexity margin bounds, but no statement about fat-shattering dimension or sample covering numbers of real-valued classes. A complete formalization would provide a reusable library of these objects, with their basic inequalities between squashing, quantization, packing and covering. It would also give a checked version of the explicit constants and , which differ from those in later textbook treatments.
The bound is uniform over a possibly uncountable class , so a union bound over hypotheses does not apply. The obvious replacement is a union bound over a cover of . Two steps make it hard:
The quantization steps look routine but carry the factor-of-two losses that produce the constants , and .
The model is in the namespace BartlettNN.Margin.
Bool, read as through pm (true is ). . Samples are functions Fin m → X × Bool, indexed from , with law Measure.pi (fun _ => P). The margin estimate uses the strict inequality , and shattering uses .ℕ∞. A ℕ-valued supremum would be on an unbounded set, so the goal assumes fat H (γ/16) = d with d : ℕ.⊤ when no finite cover exists. and are suprema over all samples, with repetitions allowed. "-separated", which the paper leaves undefined, is read as distance .Real.log, is Real.logb 2, and is Real.exp 1.Measurability. The paper states "we ignore issues of measurability, and assume that all sets considered are measurable" (p. 526). This is made explicit, not removed, through three hypotheses:
Replacing these by countability of would weaken the theorem.
Corrections of the printed text.
Trivializing formalizations, ruled out. The following would each make the statements empty or different, and none is used:
ℕ-valued fat dimension or covering number;Real.sign in place of ;Infrastructure that a complete development needs, and contributions that are welcome:
The covering/packing and fat-shattering lemmas apply beyond this mission. Proofs of individual milestones, or of Theorem 5 in the generality of Alon et al., are useful contributions in their own right.
An airline sells the seats of one flight leg in several fare classes at different prices. Low-fare passengers usually book first, so the airline must decide how many seats to keep back, or protect, for later high-fare passengers. Peter Belobaba's 1987 MIT dissertation introduced the expected marginal seat revenue (EMSR) rule for this decision, and EMSR-type rules became a standard of airline revenue management practice (Talluri and van Ryzin 2004). A protection level is computed from a demand forecast, and forecasts are uncertain. Section 6.2 of the dissertation asks how the protection level moves when its inputs move: the mean of forecast demand, its standard deviation, and the ratio of the two fares. That question decides where forecasting effort pays off, and this mission formalizes the answers the dissertation gives for Gaussian demand.
This is the third mission in a series on the dissertation. The first treats marginal allocation among distinct fare classes, and the second the two-class nested protection level in the discrete model, including its revenue optimality. This mission takes the continuous Gaussian model of Chapter 6 on its own terms.
Let be the number of requests for a fare class, a real random variable with law . For a seat level the tail probability is
and for the fare of the class the expected marginal seat revenue is (Eqs. (6.1)–(6.2)).
There are two classes: class 1 with fare and class 2 with fare , where . Requests for class 1 are Gaussian with estimated mean and estimated standard deviation , written . A real number is an EMSR protection level for class 1 against class 2 when
The standardized level is the value "which has a probability of of being exceeded" by a standard normal variable:
In the Lean development these are tailProb, emsr, gaussianLaw rbar σ, stdNormal, IsProtectionLevel rbar σ f₁ f₂ S and IsStdNormalLevel f₁ f₂ Z, all in the namespace SeatInventory.Gaussian.
For and :
The goal states no numerical constant and no particular fare ratio; it fixes only the shape of the dependence.
The dissertation's constant-coefficient-of-variation form, Eq. (6.13), with , follows from (6.12) by substitution and is not stated separately.
The result gives every Gaussian protection level as a closed form in one standard normal quantile. From it come the three sensitivities that Sect. 6.2 uses to argue for better forecasts. The protection level moves one-for-one with mean demand. The standard deviation moves it in a direction fixed only by whether the discount fare is above or below half the full fare. A higher fare ratio always lowers it. The dissertation uses these facts, and its Figures 6.1 and 6.2, to argue that reducing the estimated standard deviation of demand narrows the range of protection levels a forecast can produce. The same quantile structure is behind Littlewood's rule and the newsvendor critical fractile, so the statements here are the Gaussian specialization of a pattern that recurs throughout revenue management and inventory theory.
All the statements are classical and easy to believe. None of them, to our knowledge, has a machine-checked proof. Mathlib provides the Gaussian law and its affine images, but no standard normal quantile and no statement that a Gaussian tail is a strictly decreasing bijection onto . Formalizing this mission produces both, in a form that can be used again wherever a normal critical fractile appears.
Most of the work is in the existence and uniqueness of the two tail solutions. The tail must be shown continuous, strictly decreasing, and to take every value in . Strictness needs the Gaussian density to be positive everywhere, and existence needs a limit argument at both ends. Monotonicity alone, which holds for every law (Eqs. (6.1)–(6.2)), gives neither, because a general law can have flat stretches and jumps in its tail. The relation then requires transporting the tail of to that of through the affine map , and the sign of requires the symmetry of , namely . Once uniqueness is available, each sensitivity statement follows from these facts. The tempting shortcut of reading as a definition is ruled out below.
gaussianReal rbar (σ^2), parameterised by the variance. Every theorem assumes ; at the law is a Dirac mass and (6.10) has no solution.Useful infrastructure, all reusable: the strict monotonicity, continuity and range of Gaussian tails; the standard normal quantile; and tail transport under affine maps. Contributions of these as separate lemmas are welcome.
An agent learning to control an unknown environment must balance rewards it can collect now against information that improves later decisions. In a finite Markov decision process (MDP), every action changes the distribution of the next state, so a mistaken transition estimate can affect decisions many steps later. Regret measures this loss against a policy that already knows the transition probabilities. The paper of Azar, Osband and Munos gives high-probability regret bounds for two variants of upper confidence bound value iteration (UCBVI) in finite-horizon reinforcement learning. This mission targets its Chernoff–Hoeffding variant, UCBVI-CH, whose bonus depends only on the horizon and the visit count. Theorem 1 improves the paper's cited earlier dependence on the number of states from to in the leading term for sufficiently many interactions. Azar, Osband and Munos, 2017, pp. 2, 4–5.
The paper was released in 2017 alongside work on the attainable dependence of episodic regret on the horizon , state count , action count , and total interaction time . Its second algorithm, UCBVI-BF, uses a variance-dependent bonus and is the subject of the next mission in this series. UCBVI-CH has a simpler bonus and its own explicit bound, making it a distinct mathematical target. Azar, Osband and Munos, 2017, pp. 1–5.
The state set and action set are finite and nonempty, with cardinalities and . A stationary transition kernel gives the probability of moving to state after action in state ; each row is nonnegative and sums to one. The known, deterministic reward lies in . An episode lasts steps. The environment chooses its starting state before episode and may base that choice on earlier episodes. It cannot see the current episode's future random draws. Azar, Osband and Munos, 2017, §2 and Assumption 1, pp. 2–3.
A policy selects an action from the current state and the step number. Its value is the expected sum of rewards from step through step when starting in state . The terminal value is , and is the maximum of over all such policies. Since the state, action and step sets are finite, this maximum is over a finite nonempty policy class. The paper's sentence describing rewards uses a shifted terminal convention; this series follows the reward steps of Algorithms 1–2. Azar, Osband and Munos, 2017, pp. 3–4.
At the start of episode , UCBVI-CH forms visit counts and from earlier completed transitions. On a visited pair it uses the empirical row . Algorithm 2 computes values backward from zero at the terminal step. For a visited pair, is the minimum of the preceding episode's , , and the empirical Bellman value plus Algorithm 3's bonus. For an unvisited pair, . A maximizing action is chosen at every state, including states outside the realized path. Azar, Osband and Munos, 2017, Algorithms 1–3, pp. 3–4.
For episodes and , regret sums the gap . The goal is the paper's printed bound, with its constants:
Algorithm 3 itself uses in its bonus . Both logarithms remain as printed. The probability is over the MDP's next-state draws, for every admissible starting-state rule and every way of breaking ties between maximizing actions. Azar, Osband and Munos, 2017, Algorithm 3, p. 4; Theorem 1, p. 5.
Four milestones retain the source's indexed attack path: the Bernstein bound (9) for the empirical value error, the count-deviation display before (11), Lemma 18 on optimism, and the weighted recursion displayed in the proof of Lemma 3. The last milestone preserves the signed weights that appear before the paper's final simplification. Azar, Osband and Munos, 2017, pp. 17, 20–21, 28.
Theorem 1 gives a finite-sample failure probability with explicit dependence on and . It covers a learner whose initial state can change between episodes, a feature that matters in episodic learning where the experimenter does not fix a single starting distribution. For the regime stated after Theorem 1, the leading rate is . This is a result claimed by the paper; the present Lean declarations are open proof targets, not machine-checked proofs of that claim. Azar, Osband and Munos, 2017, p. 5.
Formalizing the result creates reusable finite objects for adaptive interaction: a constructed probability law on complete paths, empirical transition counts pooled across steps, a policy value defined by its expected reward, and confidence events with their domains stated explicitly. The concentration and optimism milestones can then be investigated independently of the final regret bound. The later UCBVI-BF mission uses the same paper's model with a different bonus. Azar, Osband and Munos, 2017, pp. 3–5, 14–17.
The visit count is random and depends on earlier observations and decisions. A concentration inequality for a predetermined number of samples therefore does not immediately give a statement that holds at every episode start. The algorithm also reuses the previous episode's estimate through a minimum. Any optimism claim must account for this dependence across episodes as well as the backward dependence across steps. In the regret analysis, the terms called martingale differences can have either sign, so replacing a positive weight by a larger common bound can reverse an inequality. These are concrete obstacles to the printed chain of estimates. Azar, Osband and Munos, 2017, pp. 4, 17, 20–21, 28.
States, actions, steps, episodes and complete outcome arrays are finite. Probabilities are finite sums of products of transition rows. The transition-row predicate is a published general definition; this mission defines the paper-specific reward-bounded MDP, policies, UCBVI-CH recursion, and path law on top of it. The starting-state rule can inspect only earlier episodes. Greedy tie-breaking is universally quantified. is a maximum over policies, and the bonus is read only at positive counts. A model that assigns an arbitrary probability law, fixes one starting state, or omits Algorithm 2's minimum does not represent this target. Azar, Osband and Munos, 2017, pp. 2–4.
Lean uses steps and terminal index in place of the paper's algorithmic . The appendix sometimes puts the terminal value at . The weighted recursion therefore runs through the final reward step, rather than ending one step early. Its typical-state threshold is , as required by (34)–(36), whereas Appendix B.1 prints . The proof's correction term dominates its other terms under , which is made explicit in that milestone. The printed (11) loses a factor of two from the count display before it; only the preceding display is a milestone. Lemma 18 is stated under the empirical-model part of the confidence event and , the domain on which its bonus comparison holds. The weighted milestone retains its coefficients because the bracketed martingale terms can be negative. Azar, Osband and Munos, 2017, pp. 14–17, 20–21, 28.
The goal retains Theorem 1's constant . Appendix C.1 cites Lemmas 15 and 18, but the sketch of Lemma 15 does not track that constant explicitly. Formalizing the printed bound may therefore expose a gap in its proof; the mission records the claim without weakening its constants. Contributions establishing or repairing the explicit bound, as well as the four stated milestones and reusable finite concentration results, are within scope. Azar, Osband and Munos, 2017, pp. 5, 27, 29.
In the classical secretary problem a decision maker sees candidates in a uniformly random order and must accept or reject each one on arrival, irrevocably, aiming to accept a valuable one. Its online, random-order structure models hiring, selling an item to sequentially arriving buyers, and posting prices in online markets. Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009) study the discounted secretary problem, where the reward of a selection depends on when it is made: a candidate accepted late is worth less (or more) by a time-dependent factor, as with a seller whose revenue decays with time, or a firm that loses value the longer a position stays empty.
Timeline of the setting:
There are elements, indexed by . Element has a value , and each time has a discount . The elements arrive in a uniformly random order , a bijection from times to elements: element arrives at time . Selecting the element that arrives at time earns , and an algorithm selects at most one element.
The offline optimum on the order is . It is a random variable, and the benchmark is its expectation
For a real parameter , algorithm selects the first time at which and earns that product; if no time qualifies, it selects nothing and earns . It knows and , sees the values one at a time, and never sees the future of . Its expected value is .
The proof uses three derived objects:
For every , all discounts , all values and every real ,
Taking gives , a -competitive algorithm when the expected optimum is known.
The result. The discounted problem separates sharply by information: a logarithmic gap is unavoidable without prior knowledge, while knowledge of the single number , or of any lower estimate of it, closes the gap to a constant. The algorithm is a fixed posted threshold, so read as a mechanism it is a posted price, which is truthful for single-parameter agents (§1). The paper also notes that when all values are known, can be estimated by sampling (its Lemma A.1), which yields a constant-competitive algorithm in that setting. The companion lower bound (Theorem 4.6) shows that even complete knowledge of the values does not give a ratio better than .
Formalizing it. The result is proved on paper; no machine-checked proof is known. The formalization yields a checked version of the paper's counting argument on permutations (Claim 4.8) and of the tie-breaking step behind Eq. (4.3), and reusable finite random-order bookkeeping: expectations over as averages, threshold stopping rules, and the decomposition of an online algorithm's value by the time and element it selects.
The obvious argument fails when rarely selects. earns at least whenever it selects anything, so . That settles the case and nothing else: the probability of selecting can be tiny while is still large, because the optimum may be concentrated on a few orders with a large product. In that case the bound must come from comparing the algorithm with the optimum pair by pair: every time–element pair with must be realized by on a positive fraction of the orders.
Two points need care in a formal proof:
Neither (4.2) nor the map appears in the statements, so solvers may replace either with any argument they like.
Fin n; the paper's time is the index . An order is π : Equiv.Perm (Fin n), read as time ↦ element, as on p. 3. The instance [NeZero n] encodes , so the maximum over times is a genuine maximum (Finset.sup').Equiv.Perm (Fin n) and on first-hitting times are reusable beyond this mission.In the classical secretary problem a decision maker sees candidates in uniformly random order, learns each candidate's value on arrival, and must accept or reject it on the spot; the goal is to pick a valuable one. A simple sample-then-select rule picks the best candidate with probability at least , so the problem is constant-competitive. The secretary problem is also a model of online mechanism design: a rule that accepts the first agent above a threshold computed from earlier agents is a truthful posted-price mechanism (as the paper notes in §1).
Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009; authors' version) study the discounted secretary problem, where accepting at time is worth for a known discount function . Discounts model settings where a sale is worth more at some times than at others. The case had been studied before (Rasmussen and Pliska 1976); the paper asks what happens for arbitrary . Its answer has two sides: an -competitive algorithm, and the result of this mission, a lower bound showing that no online algorithm is better than -competitive. So, unlike the classical problem, the discounted problem with a general discount is not constant-competitive.
There are elements with values , and a discount function on the times. The elements arrive in a uniformly random order : element arrives at time . A randomized online stopping rule specifies, for each time and each sequence of values seen so far , a probability of stopping at if it has not stopped yet. Stopping at selects and earns ; the rule selects at most one element and may select none. The rule knows and , but it sees only values, only as they arrive, and it is not told which instance it is facing.
The expected value of is
and the benchmark is the expected offline optimum
which is itself a random variable averaged over the order. is -competitive on an instance when .
The hard family (§4.1.1 of the paper): fix an integer and put , , for , and . The step discount is on the times and on . The instance has elements of value and the rest ; is obtained from by raising of its values to , so has elements of value .
For every integer and every randomized online stopping rule for horizon and the step discount,
That is, no online rule is -competitive on all of .
The result separates the discounted secretary problem from its classical and weighted relatives, which admit constant-competitive algorithms (the paper's Theorem 3.4 and the -competitive classical rule). Together with the paper's upper bound (Theorem 4.4) it pins the competitive ratio for general discounts between and up to constants, and it motivates the paper's known- model (§4.2), where an estimate of restores a constant ratio. The construction is a template for lower bounds against randomized online algorithms in random-order models: geometrically nested instances that a rule cannot tell apart early, played against a discount that punishes waiting.
The theorem is proved in the paper, in about a page. To our knowledge no part of it has a machine-checked proof. This mission produces the formal model of randomized online stopping rules in the random-order discounted setting, a reusable object for the paper's other discounted results (the upper bound, and the lower bound with known values of Theorem 4.6), and a checked version of the lower bound with explicit constants.
The obvious attempt is to fix one instance and show that every rule loses on it. That fails: for any single instance there is a rule tuned to it (a rule that waits exactly as long as that instance warrants). The lower bound has to play the instances against each other. A rule that does well on must commit early, within the first steps, yet the rule cannot distinguish from during those steps except with probability . Making "cannot distinguish" precise is the central step: it needs a coupling of the two runs over the same random order and the same internal randomness, which works only because the rule's decision at time depends on the values observed so far and nothing else. The accounting then has to show that the rule's early earnings on and its late earnings are both small compared with , which uses and that dwarfs .
Fin n, 0-based: index is the paper's time , so the paper's block is the index range . The random order is π : Equiv.Perm (Fin n) read as time element, and every expectation over it is the finite average . Values and discounts are real.StoppingRule n: stopping probabilities indexed by time and the arrival-ordered value sequence, with the non-anticipation condition that depends only on . The theorem quantifies over all such rules, so it covers deterministic and randomized online algorithms that observe values only. A rule may depend on and but not on the instance index.Fin n), and competitiveness is multiplicative, , never a quotient.Fin n (the probability that a set of elements misses the first positions), the coupling of two value sequences that agree on a prefix, and elementary estimates on geometric sums. The rule model and the permutation-counting lemmas are reusable for the paper's other discounted results. Contributions of these supporting lemmas, as well as proofs of the milestones, are welcome.A correlated equilibrium is the equilibrium notion that arises when the players of a game take their actions on the advice of a common randomizing device, each player seeing only his own recommendation. It was introduced by Aumann in 1974 (Aumann 1974). Aumann's 1987 paper (Aumann 1987) gives the simple, finite form of the definition used today (Definition 2.1) and shows that the notion is what Bayesian rationality with a common prior predicts. On the way it records, as Proposition 2.3, the fact that makes correlated equilibrium tractable in practice: for a finite two-person game, the distributions over action pairs that come from correlated equilibria are exactly the solutions of an explicit finite system of linear inequalities.
That characterization is the starting point of the computational theory of correlated equilibria. Because the set is a polyhedron, an optimal correlated equilibrium can be found by linear programming, and no-swap-regret learning dynamics converge to this set (Foster and Vohra 1997; Hart and Mas-Colell 2000). In each of these works the linear-inequality description is taken as the definition; the paper's Proposition 2.3 is the bridge back to the strategic definition.
Player 1 has a finite set of actions and player 2 a finite set . For and , and are the two players' payoffs at the action pair .
A correlated strategy pair is a pair of functions , on a finite probability space : a finite set with nonnegative weights summing to . Chance draws and suggests the action to player . The pair is a correlated equilibrium (Definition 2.1, condition (2.2)) if no player gains by a deviation that depends only on his own suggestion: for every ,
and the analogous inequality holds for player 2 and every .
A distribution is a family with and . The distribution of a correlated strategy pair assigns to the probability . A correlated equilibrium distribution (c.e.d.) is the distribution of some correlated equilibrium on some finite probability space.
In the Lean development these are IsDistribution p, IsProbVec μ, IsCE h₁ h₂ μ f₁ f₂, distr μ f₁ f₂ and IsCED h₁ h₂ p, with h₁ j k and p j k .
For every distribution : is a correlated equilibrium distribution if and only if
A further statement, not a milestone, records the paper's example on p. 5: in the game of chicken (Figure 4) the distribution of Figure 5 is a c.e.d. with expected payoff .
The result. Proposition 2.3 turns an existential statement — there is some probability space and some correlated strategy pair that is an equilibrium and has distribution — into finitely many linear inequalities on alone. Consequently the set of c.e.d.'s is a compact convex polyhedron, membership is decidable by evaluating linear forms, and optimizing a linear objective over it is a linear program. The paper states the two-person case and remarks that "the principle, however, is no different in the general case".
Formalizing it. The proposition is classical and its proof is short; to our knowledge it has no machine-checked proof. The platform already has the linear-inequality (swap) form of correlated equilibrium for two-player games on Fin m × Fin n (Foster–Vohra 1997 missions) and Aumann's 1974 randomizing-structure model, but no statement that connects the strategic definition over arbitrary finite probability spaces with the linear system. This mission supplies that connection, so that results proved about the polyhedron apply to equilibria in Aumann's sense and conversely.
The mathematics is elementary; the care is in the statement. Two points need attention. First, the direction from the inequalities to a c.e.d. requires constructing a probability space and a correlated strategy pair whose distribution is the given ; the c.e.d. notion quantifies over probability spaces, not over distributions. Second, the paper's argument divides by the probability of a suggestion, which may be zero; the conditional formulation (milestone 2) holds only over possible suggestions, while (2.4) and (2.5) quantify over all actions and hold trivially at impossible ones. Deviations must be functions of the player's own suggestion: restricting to constant deviations gives coarse correlated equilibrium, which (2.4)–(2.5) do not characterize, and allowing arbitrary functions of gives a stronger notion.
Two players with finite action types S₁ S₂ : Type* (Fintype, DecidableEq); payoffs h₁ h₂ : S₁ → S₂ → ℝ; distributions p : S₁ → S₂ → ℝ with the sign and sum conditions as an explicit hypothesis of every statement about distributions. Finite probability spaces are finite types Γ : Type with a probability vector μ : Γ → ℝ; deviations are compositions φ ∘ f₁ with φ : S₁ → S₁. The conditional payoffs , use Lean's x / 0 = 0 and are only ever used at possible suggestions. Empty action sets admit no distribution, so the statements are then vacuous, exactly as in the paper.
A trivializing formalization is ruled out: "c.e.d." is the existential notion over finite probability spaces with a genuine probability vector and an equilibrium in the sense of Definition 2.1, not the inequalities themselves or the swap form on .
No infrastructure beyond finite sums and Finset.filter is needed. Contributions welcome: proofs of the milestones, and the -player generalization the paper alludes to.
An orthogonal projection onto a closed subspace is straightforward to describe when that subspace is given directly. It is less straightforward when the subspace is specified as the closed sum of two others: a vector can have contributions from both, and the two component projections generally do not commute. In §12 of Aronszajn's 1950 paper, this problem arises while expressing the reproducing kernel of a sum of two closed subspaces of a reproducing-kernel Hilbert space through their individual kernels. The projection formula is the analytic heart of that calculation. It also gives a series whose finite partial sums can be applied without first describing a basis for the closed sum.
Aronszajn states the result for closed subspaces of a complex Hilbert space of functions. The projection identity itself uses only Hilbert-space geometry; evaluation at a point and the reproducing property enter when the operator formula is translated into a kernel formula later in the section. This mission isolates the projection theorem so that the same formal result can be used both in that kernel calculation and in other settings with two closed subspaces.
Let be a complex Hilbert space and let be closed linear subspaces. The algebraic sum is the set of all with . It need not be closed. Write for its closure and for the intersection. All four subspaces are closed except possibly the algebraic sum itself. Let be the orthogonal projections onto , respectively. Operator products denote composition, with the rightmost factor applied first; is the identity.
The paper writes for , even when is nonzero, and uses a distinct dotted plus for the algebraic sum. These symbols can look like a direct sum in newer notation. Here the definitions of and remove that ambiguity. Aronszajn assumes complex scalars throughout Part I after §1, p. 343; the statements below keep that convention. Neither a topology on an underlying set of functions nor a measure is part of these operator assertions.
The goal is the strong projection series, §12, Eq. (7). For each ,
The sum means that its finite partial sums converge in the norm of for each fixed . No operator-norm limit is claimed. The first term of the sum, at , includes because both zero powers are identity operators.
Three source statements are milestones. Equation (1) is a finite identity that expresses a power of through a partial sum and a power of . The paragraph following Eq. (4) identifies the strong limit of as . The paragraph before Eq. (7) asserts that tends strongly to zero. Together these statements specify the finite and limiting parts of the displayed target. They require no assumption that is zero.
The formula describes the orthogonal projection onto a closed sum in terms of projections onto its two constituents. In Aronszajn's application, an orthogonal projection on a closed subspace determines that subspace's reproducing kernel; therefore the operator expansion supplies a kernel expansion without constructing a basis of the sum. It also makes explicit why an intersection term survives when the subspaces overlap. The result is proved in the 1950 paper; this mission asks for a Lean proof of that known result, with its convergence mode and closure convention made explicit.
A machine-checked development would provide a reusable complex-Hilbert-space statement for alternating projections and closed sums. Mathlib already provides closed submodules and their orthogonal projections, so the new contribution is the finite identity and the strong-limit claims connecting them. The resulting theorem can support the paper's later kernel expression, §12, Eq. (18), once the correspondence between bounded operators and kernels from §11 is available. Equation (18) is outside this mission's target list.
The algebraic sum of two closed subspaces can fail to be closed, so projecting onto it directly would leave the target undefined as a Hilbert-space orthogonal projection. Passing to its closure gives the correct target but does not imply the two projections commute or that their product has a uniform contraction factor. In particular, strong convergence of the powers and of the final series does not generally improve to convergence in operator norm. The later special case in §12, where the intersection is zero and the minimal angle is positive, has a stronger uniform-convergence conclusion; that extra angle condition is absent from Eq. (7).
The finite formula also has four terms per summand whose order matters. Reversing and , beginning the power at rather than , or omitting changes the statement. Even a proof of pointwise convergence of each selected term would not by itself establish the convergence of the bracketed partial sums in the target.
The Lean representation is an arbitrary complex Hilbert space E with two ClosedSubmodule ℂ E objects. Mathlib's Submodule.starProjection supplies and . Two small definitions name as projection onto the join of the closed submodules and as projection onto their meet. The closed-submodule join is the closure of the algebraic sum; the meet is the intersection. These definitions are computed from , not independently quantified projections. The theorem quantifies over every vector and uses Filter.Tendsto along natural-number partial sums, giving norm convergence of the resulting vectors.
The source's ambient class has a reproducing kernel, but no step in Eqs. (1)–(7) uses point evaluations. The formal statements therefore apply to any complex Hilbert space, including the paper's RKHS. The stronger scope is explicit here and does not assert a new kernel identity. The -th Lean partial sum uses indices for the paper's ; it has the same terms and is defined at as . The finite identity is stated only for , as its version is false in general.
Eq. (1) on p. 375 is printed without the opening bracket of the summand (only the closing bracket appears); the formalization reads it as in Eq. (4) on p. 376, where both brackets are printed. There are two printing slips on p. 377: a running sentence drops brackets from the power of , and it prints while discussing the projection . The formalization follows the bracketed expression in Eqs. (1) and (4), using ordinary operator subtraction. The corresponding milestone preserves the printed wording. No assumption from the later angle analysis, especially , is imported into these results. The series is stated through actual partial sums; it is not defined by an arbitrary RKHS chosen to have a desired kernel.
A directed polymer in a random environment is a simple random walk whose paths are reweighted by a random field of energies. It is a basic model of disordered statistical mechanics, and in dimension it belongs to the Kardar–Parisi–Zhang (KPZ) universality class: at fixed temperature the free energy fluctuates on the scale and is expected to follow Tracy–Widom laws. Comets and Yoshida (Ann. Probab. 34 (2006)) showed that in dimension every positive inverse temperature lies in the strong disorder regime, where the normalised partition function tends to zero. At the polymer is simply the random walk.
Alberts, Khanin and Quastel (arXiv:1202.4398, Ann. Probab. 42 (2014)) identified the regime in between. If the inverse temperature is scaled as , the partition function neither concentrates nor vanishes: it converges in law to a universal random variable, a Wiener chaos in a space–time white noise. That variable is the solution at time , integrated in space, of the stochastic heat equation with multiplicative noise, whose logarithm is the Hopf–Cole solution of the KPZ equation. The theorem therefore connects discrete polymers to the continuum KPZ equation under weak, -dependent disorder, with no assumption on the environment beyond exponential moments.
The environment is a family of i.i.d. real random variables on a probability space , with mean and variance . Write . The polymer is the symmetric simple random walk on started at , independent of , under the uniform measure on the step sequences. The energy of an -step path is , and the point-to-line partition function is
The modified partition function replaces by : .
On the continuum side, a white noise on is a centred Gaussian family , indexed by the Borel sets of finite Lebesgue measure, with . Its multiple stochastic integrals are continuous linear maps with for pairwise disjoint . Let be the heat kernel and . Put on , with , and zero elsewhere. The Wiener chaos (7) is
The discrete counterpart of is the weighted U-statistic of (29): a sum of products over distinct times, weighted by averages of over space–time rectangles of size .
If, in addition, for all for some , then for every
Under mean zero and variance one alone, .
In the order the proof uses them:
The theorem gives a universal scaling limit for the partition function in a regime where the polymer still moves diffusively but feels the disorder. As a corollary, converges in law, so the fluctuation exponent of the free energy is in this regime. The companion results (point-to-point partition functions, Theorem 2.2) show that the rescaled polymer path measure converges to a continuum directed random polymer. Letting grow then interpolates between Gaussian behaviour and the Tracy–Widom GUE fluctuations of the KPZ class. The U-statistic machinery of Section 4 (discrete chaos expansions in an i.i.d. space–time field converging to multiple Wiener–Itô integrals) applies to other discrete models with polynomial chaos expansions.
The theorem is proved in the paper. To our knowledge it has no machine-checked proof, and Mathlib has no space–time white noise, no multiple Wiener integrals, no Wiener chaos, no Lindeberg–Feller theorem for triangular arrays and no local limit theorem for the simple random walk. A complete formalization would build each of these and check the paper's argument, including two statements that are false as printed (see Formalization scope).
The obvious route is to expand in powers of and pass to the limit term by term. Two steps of that route do not go through as stated. First, the -th term is a degenerate U-statistic of order in the environment. Its convergence to is not a classical central limit theorem: it needs joint control of all orders and a density argument in , and the space–time discretisation must respect the parity of the walk, which is why the rectangles have spatial length . Second, exchanging the limit with the infinite sum over needs bounds on the discrete kernels that are uniform in and summable in . Pointwise convergence from the local limit theorem is not enough. Passing from to also requires a central limit theorem for a triangular array whose law depends on .
The environment is ω : ℕ × ℤ → Ω → ℝ, independent and identically distributed, square integrable, with mean and variance . Times are read. and are explicit averages over the step sequences. The white noise lives on , since only enters (7). is a family of continuous linear maps on characterised by its values on indicators of products of disjoint sets. Every limit theorem quantifies over all white noises and all such families, and a separate item asserts that one exists. and are sums in ; real powers , are Real.rpow; is Mathlib's cgf; convergence in law is TendstoInDistribution.
Normalisation of . The paper's normalisation of multiple integrals is not consistent (§3.2 and the remark on p. 19 differ by ). The formalization follows (7) and the variance computation on p. 6: for supported on , .
Corrected statements. Two milestones are stated in the corrected form that the paper's proof establishes:
Theorem 4.5 and Lemma 4.6 (perturbed environments) are not part of the milestone list. Theorem 4.5 is false as printed: mean zero and a variance tending to do not give a central limit theorem for a triangular array, and the Lindeberg condition named in its proof must be added. Lemma A.1 is stated for the point-to-line kernels only.
Trivializations ruled out. The limit is the chaos (7) built from a genuine white noise and its multiple integrals, not any random variable with a prescribed property. is pinned down by . Every infinite sum comes with a milestone proving its summability, and the partition function averages over all walk paths.
Infrastructure that would be reusable beyond this mission: space–time white noise and multiple Wiener–Itô integrals with their isometry, a Lindeberg–Feller central limit theorem, the local limit theorem for the simple random walk, and the Cramér–Wold device. Contributions of any of these, or of proofs of the milestones in any order, are welcome.
Electricity demand response asks consumers to lower their consumption during price events, when generation is expensive or scarce. Field trials such as the Low Carbon London experiment showed that consumers do react to price signals, but that the reaction is erratic: the average consumption falls while its variability stays high, and a producer that has to follow the load curve in real time pays for that variability. Aïd, Possamaï and Touzi (arXiv:1810.09063; Math. Oper. Res. 2022, doi:10.1287/moor.2021.1201) model this as a continuous-time principal–agent problem in which the consumer (the agent) controls both the level and the volatility of consumption, and the producer (the principal) designs a payment that rewards both.
The paper compares two benchmarks. In the second best, the producer observes only the consumption path and the consumer responds optimally to the contract; this is the subject of the companion mission of this series. In the first best, the producer dictates both the contract and the consumer's effort, subject only to the consumer's participation. The first best is the reference point against which the cost of moral hazard, the information rent, is measured. This mission formalizes the first-best value in closed form, Proposition 3.1 (i) of the paper.
The methodology follows the continuous-time principal–agent literature: Holmström and Milgrom (1987) for exponential utilities and linear contracts, Sannikov (2008) for the dynamic-programming view of the agent's continuation value, and Cvitanić, Possamaï and Touzi (2018) for contracts indexed on both the output and its quadratic variation.
Fix integers (usages for the mean effort and for the volatility effort), cost parameters , , nominal volatilities , effort bounds and , risk aversions , a marginal volatility cost , slopes , a horizon , an initial consumption and a reservation utility .
The consumer chooses a mean effort with values in and a responsiveness effort with values in , at cost
The consumption follows with , in the weak sense: is the canonical process on , and an admissible pair is a progressively measurable control with a probability measure under which starts at and solves the associated martingale problem.
The consumer values consumption by and the producer bears the generation cost ; write . For a payment made at time , the consumer's and the producer's criteria are
A contract is an -measurable with uniform exponential moments (2.5). The first-best value is
The consumer's Hamiltonians are and . Finally , , , and .
Assume . Then
The closed form shows how the first-best value depends on each parameter: on the energy value discrepancy through the mean-effort term, on the volatility cost and the effective risk aversion through the volatility Hamiltonian, and on the reservation utility only through the shift by . It is one half of the paper's information rent (Proposition 3.4), the gap between the first- and second-best values, and it is the benchmark against which the calibrated contracts of the paper's Section 4 are judged.
The result is proved in the paper, partly by appeal to standard stochastic control arguments. To our knowledge it has no machine-checked proof. A formal proof requires a verification theorem for an exponential-utility control problem in the weak formulation, and a risk-sharing argument with a pathwise quadratic-variation term in the contract; both are reusable beyond this paper.
The deterministic parts, Proposition 2.1 and the algebra that turns (A.5) and the value of into the goal, are calculus. The difficulty lies in the two stochastic steps. In (A.5), the producer's optimal payment for a given effort depends on ; it must be realised as a measurable function of the path that is a contract in the sense of (2.5), uniformly over all admissible laws, and the participation constraint must be shown to bind. In Proposition A.3 (i), the upper bound on must hold for every progressively measurable, path-dependent control, not only for Markov feedback controls; the paper invokes "standard stochastic control theory", which has to be made precise for controls of the volatility under a martingale-problem formulation, where no Brownian motion is given in advance.
The canonical space is with the coordinate σ-algebra and the canonical filtration; processes are indexed by . Admissible pairs are given by a martingale problem: almost surely, and both and its square minus are martingales. In the criteria, is replaced by its almost-sure value ; a contract remains any -measurable function of the path. Expectations of utilities are negated lower Lebesgue integrals of exponentials in , and every value is an extended-real supremum with . is read as , with indices in Fin N and Fin d.
The Hamiltonians are defined by their infima, never by their closed forms, so that Proposition 2.1 is not true by definition, and the first-best value is a supremum over the model's own objects, not a variable pinned by hypotheses. Three hypotheses are added to the page: (so ), (so is defined), and, for the goal only, , without which the printed exceeds and contradicts the paper's own proof. Misprints corrected and disclosed in the items: the closed form of in Proposition 2.1 is false for and is replaced by with ; the index range of is ; on p. 28, is and "(A.11)" is (A.6).
The parts (ii)–(iii) of Proposition 3.1, the optimal efforts and the optimal contract, are not stated. Contributions welcome: a verification theorem for controlled martingale problems with bounded coefficients, exponential moment bounds uniform over admissible laws, and a pathwise quadratic variation on the canonical space.
The Ising mixed -spin model assigns to each configuration the energy of a random polynomial whose covariance is . Its ground-state energy converges to the value of a variational problem, the zero-temperature Parisi formula (Auffinger–Chen 2017), in which a functional is minimized over non-decreasing order parameters . El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) ask how close a polynomial-time algorithm can get to this maximum. Their answer is an extended variational principle: the best value reachable by incremental approximate message passing is , where the space drops the monotonicity constraint.
The algorithm that reaches this value is built from a minimizer of over , and it runs along the set of times where is positive. Theorem 5 of the paper (p. 30) shows that this set is dense: a minimizer has full support. This mission formalizes that theorem and the first- and second-order optimality conditions it rests on (Section 6.1, pp. 22–31).
Timeline. Parisi proposed the variational formula in 1979. Talagrand (2006) and Panchenko (2013) proved it at positive temperature. Auffinger and Chen (2017) established the zero-temperature version with and proved that a minimizer over the monotone space exists. Jagannath and Tobasco (2016) developed the PDE and SDE tools for the Parisi functional that Section 6.1 of the present paper adapts to non-monotone order parameters. Montanari (2019) gave the first message passing algorithm for the Sherrington–Kirkpatrick case; the present paper (2020) extended it to general mixtures and introduced .
A mixture is with for some ; its derivatives , are the termwise differentiated power series, non-negative and non-decreasing on .
An order parameter is a function . The extended space is
with the weighted distance . The non-negative step functions are the finite sums with and .
For a terminal condition (convex, continuous, even, non-negative, differentiable off with on ) and , the Parisi PDE
has the explicit Cole–Hopf solution : on , with . For , is the limit of along step functions in the weighted distance. The Parisi functional is
Given a Brownian motion , the process solves , . The support of is , and is its closure in .
With , if satisfies , then
The path to the goal, in attack order:
The result. Full support identifies the extended variational principle as one whose minimizers are "nowhere flat". The algorithm of Theorem 3 in the paper follows through incremental steps whose size is set by , and it needs no special treatment of gaps where . The stationarity conditions (Corollaries 6.10–6.11) also characterize minimizers over the way the Auffinger–Chen conditions characterize minimizers over the monotone space. They are the starting point for comparing with the Parisi value.
Formalizing it. The theorem is proved in the paper; nothing here is open mathematics. The paper's proofs rely on cited PDE regularity (Jagannath–Tobasco 2016) and on standard SDE theory, often in one line. The mission produces a machine-checked chain from the explicit Cole–Hopf formula to the support theorem. Along the way it builds the Parisi PDE solution on a non-monotone class, a first-variation formula, and stationarity conditions, none of which have a formal counterpart. No formal statement of the Parisi functional or the Parisi PDE exists on Prove2Me (index search, 2026-10-03).
Two steps resist a direct argument. The first is the first variation (Proposition 6.8): differentiating in requires comparing the SDE for with the SDE for the perturbed parameter and controlling their difference uniformly, which needs bounds on that degenerate as . The second is the exclusion of gaps: on an interval where the PDE is a time-changed heat equation, and the contradiction comes from a strict inequality, which requires the law of to charge every interval (Lemma 6.12). The obvious idea of perturbing upward on a gap only yields the inequality (6.14), which is consistent with a gap; the second-order identity at the gap's endpoints is what closes the argument.
Conventions committed to in Lean:
eVariationOn for the total variation and IntegrableOn for the integral; the latter includes the a.e.-measurability that the paper takes for granted.gaussianReal 0 1. For , is a limit along the filter of step functions converging in the weighted distance; it is never "some solution of the PDE".derivs in . Lemma 6.2's weak-derivative claim is stated as "convex and 1-Lipschitz", its equivalent.EthierKurtz.SolvesBrownianSDE in dimension one, with coefficients extended by zero after time . The driver is assumed to be a standard Brownian motion (IsBrownianReal). Statements about hold for every strong solution, which by Lemma 6.5 is unique.closure (S γ) ∩ Ico 0 1. Right-continuity of , the paper's convention from p. 28, is a hypothesis.A trivializing formalization is excluded: and are the paper's objects, built from the data, so the goal cannot be met by choosing a convenient solution, and minimality over cannot be satisfied by a junk infimum.
Not formalized: the weak formulation (6.4) of Lemma 6.2, printed with a wrong boundary term; the stochastic-integral identity (6.7) of Lemma 6.5; the regularity Lemmas 6.3–6.4; Proposition 6.1(a). The paper's algorithmic Theorems 2–4 are out of scope, because they concern algorithms in an informal model of computation and an AMP state-evolution theory that is not part of this mission.
Useful infrastructure beyond this mission: the Cole–Hopf solution and its Lipschitz dependence on , the Parisi functional on , and the SDE (6.3). Contributions that formalize Itô's formula for these processes or the regularity of are welcome as supporting lemmas.
Demand response asks electricity consumers to lower or smooth their consumption when generation is expensive, in exchange for payments. Field trials such as Low Carbon London showed two effects of such incentives: consumers reduce their average consumption, and the variability of their response depends on how much effort they put into it. A producer who cannot observe the consumer's individual usages, only the aggregate consumption path, faces a moral hazard problem: the payment can depend only on what is observed.
Aïd, Possamaï and Touzi (arXiv:1810.09063v3, 2019; Math. Oper. Res. 2022) cast this as a continuous-time principal–agent problem in which the consumer controls both the drift and the volatility of his consumption, and the producer pays for reductions in both. The volatility channel is what makes the problem new: the classical Holmström–Milgrom model (Econometrica 1987) controls only the drift. The paper uses the general reduction of Cvitanić, Possamaï and Touzi (Finance Stoch. 2018) to optimal contracts with volatility control, and obtains the producer's value in closed form up to a scalar minimisation. This mission formalizes that closed form.
Fix integers , cost parameters and , nominal volatilities , effort bounds and , risk aversions , a marginal cost of volatility , marginal energy value and cost with , a horizon , an initial consumption and a reservation utility . Write and .
Consumption. is the canonical process on with its natural filtration . A control is progressively measurable, with (effort to reduce consumption) and (effort to reduce volatility). Under the consumption follows, in the weak sense,
Effort costs per unit time, with and .
Criteria. For a payment at time , the consumer's criterion is and the producer's is with . Contracts are the -measurable with exponential moments of order uniformly over the consumer's responses (2.5). The consumer's value is , and is the set of his optimal responses.
Second best. The producer offers , the consumer responds optimally, ties are broken in the producer's favour, and participation requires :
Hamiltonians. and .
Assume . With , ,
A companion statement, Corollary 3.1 (i), gives the explicit off-peak payment rates and when .
The closed form reduces an infinite-dimensional contracting problem, a supremum over all path-dependent payments and all consumer responses, to a deterministic one-dimensional minimisation at each time. It is the basis of the paper's comparisons: with the first-best value it measures the cost of moral hazard, and its minimiser gives the price of energy and of responsiveness that the optimal contract charges, which the paper calibrates on Low Carbon London data.
The result is proved on paper. No part of it is machine-checked. A complete formalization would give a checked instance of a continuous-time principal–agent theorem with volatility control. It would also fix, in exact terms, the conventions the paper leaves implicit (weak solutions, the effort cap), and the printed misprints that this mission corrects.
The deterministic milestones are calculus on boxes. The goal is not. The upper bound must hold for every -measurable contract, not only for contracts of a convenient form. The step that fails in a direct attempt is the representation of an arbitrary contract: one needs that every inducing an optimal response can be written as , an integral against and driven by the consumer's continuation certainty equivalent. This is the main theorem of Cvitanić–Possamaï–Touzi (2018) and rests on second-order backward SDEs; it has no counterpart in Mathlib. Restricting the supremum to linear or representable contracts at the outset would assume exactly that theorem. The lower bound needs, for the candidate contract, existence of the consumer's optimal response as a weak solution and a verification argument for the producer's HJB equation.
All objects live in the namespace DemandResponse.SecondBest, and all hypotheses are fields of a structure Params. Conventions:
Fin N, Fin d; , are allowed. when (the paper's ).The goal is an equality of extended reals between , defined from the model, and an explicit real number. A formalization that defines over a restricted class of contracts, or with a real-valued supremum that returns on unbounded sets, would trivialize or change it and is not the goal.
Needed infrastructure: continuous-time martingales on the canonical path space (Mathlib has Martingale and progressive measurability), existence of weak solutions with bounded coefficients, a representation theorem for contracts (Cvitanić–Possamaï–Touzi), and a verification theorem for the producer's HJB equation. The weak-formulation layer and the contract representation are reusable for any continuous-time principal–agent model with drift and volatility control. Contributions of any of these pieces, and proofs of the deterministic milestones, are welcome.