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 classical secretary problem asks how to select one valuable candidate when candidates arrive in random order and a decision must be made when each candidate appears. Many allocation settings have several goods of unequal quality instead of a single position. An employer may have roles of different desirability, or a seller may have placements with different visibility. In the weighted secretary problem, an agent's value is multiplied by the weight of the good assigned to that agent. The algorithm must decide irrevocably as agents arrive, while the benchmark sees every value before assigning goods. Babaioff, Dinitz, Gupta, Immorlica and Talwar study this model with arbitrary fixed agent values and a uniformly random arrival order, and give a constant competitive ratio independent of the number of agents and goods (authors' version, §§2–3).
The paper also studies time discounts and matroid constraints. This mission concerns its weighted-goods result, Theorem 3.4. The result combines an online allocation rule for several comparably valuable agents with the familiar one-choice secretary rule for an unusually valuable agent. These are distinct ways in which the sorted offline assignment can earn value; both are present even when the weights are fixed in advance. The weighted model matters because matching a valuable agent to an unsuitable good can lose value despite accepting the right agent.
There are agents , each with a nonnegative value , and goods indexed in decreasing order of nonnegative weight:
An assignment gives each good to at most one agent, and each agent receives at most one good. A good may remain unassigned, represented by with . Its value is . Agent values are arbitrary, not drawn independently from a distribution. The uncertainty is the arrival order , chosen uniformly from all permutations; an agent's value becomes visible on arrival, and an allocation decision cannot be revised.
The offline optimum, , assigns the heaviest good to the highest-valued agent, the next good to the next agent, and so on. If , the extra goods remain unassigned. A consistent tie break makes the ordering unique without changing the numerical value. This sorted assignment is defined directly; the mission does not replace it with an unconstrained variable said to be optimal.
The reservation algorithm draws a sample size , observes the first agents without allocation, and retains the best sampled agents. Positive values are grouped into value classes for integer . A sampled agent in class reserves one good in that class's contiguous block, with higher classes receiving heavier blocks. A later agent receives the heaviest unassigned good reserved for its class when one is available. The classical secretary rule instead observes the first agents, then selects the first later arrival better than every predecessor; its winner receives good .
The mission's goal is the exact guarantee of Theorem 3.4 for Algorithm , which runs the reservation algorithm with probability and the classical rule with probability :
Here the expectation covers the uniform arrival permutation, the independent binomial sample size used by the reservation branch, and the mixing coin. The multiplicative inequality expresses competitiveness even when an expected payoff is zero. It uses the explicit constant in the paper's proof rather than an instance-dependent or unspecified constant.
Four source results form the milestones. The classical secretary rule selects the maximum with probability at least . Lemma 3.2 compares the starting indices and of class- blocks in the reservation and optimum assignments. Lemma 3.1 says that if the optimum assigns at least two agents from class , the reservation rule assigns at least agents from that class in expectation. Lemma 3.3 converts this to expected value at least . The target retains the paper's class condition and both numerical fractions (authors' version, pp. 4–5).
Theorem 3.4 supplies a constant factor guarantee for irrevocable allocation when goods have different weights and agents arrive in random order. The factor does not grow with or . It separates the effects of uncertain arrivals from the offline matching of high values to high weights, and it supplies a benchmark for later variants with more complicated feasibility constraints. The paper extends the reservation idea to additional combinatorial settings, including partition-matroid variants in Appendix C (authors' version, Appendix C).
The theorem is proved in the source paper, while the Lean statements in this mission are proof obligations. Formalizing them requires checking that the random-order model, sample distribution, tie convention and assignments jointly express the same algorithm. A complete development will also establish reusable finite-average facts for random permutations and binomial samples, and structural facts about sorted assignments and reserved blocks. Those pieces can support other secretary problems in the series; the mission's specific promise remains the weighted algorithm's exact bound.
A count of how many agents a class receives does not by itself control the weighted value of those goods. Goods have unequal weights, and the value of assigning the next good changes with its position in a block. A class whose offline optimum receives several agents can also lose all its sampled members from the allocation phase. Thus a direct comparison of expected class counts with expected class values is insufficient. The paper's separate count, block-position and value statements identify the claims a solver must establish; the final theorem must also account for classes represented only once in the offline assignment (authors' version, p. 5).
Agents and goods are Fin n and Fin K; their indices start at zero in Lean, so paper time corresponds to Lean index . An arrival permutation maps time to agent. Values and weights are real and explicitly nonnegative, and weights are antitone in the good index. The finite sums defining expectations are normalized by for permutations and by for sample sizes. No measurability or integration convention is needed. For the goal, makes the heaviest good available; is allowed.
Equal values are ordered by smaller original agent index throughout the sorted optimum, the sample's top agents and the classical rule. The classical rule observes exactly arrivals, and zero-valued agents reserve no value-class goods. Positive values below one use negative integer class indices. The paper says only that class holds the values “between” and (p. 4, and again in Appendix C, p. 12); the mission fixes the half-open interval , so that the classes partition the positive reals (authors' version, pp. 4, 12). A reservation assignment is built from each post-sample agent's rank within its class, so a good is offered to at most one such agent. The theorem is about this concrete algorithm and the concrete sorted offline assignment; an arbitrary favorable policy or an optimum supplied as a hypothesis would not express the source result.
The development needs a finite assignment interface, a tie-aware rank order, value classes, the two online rules, and normalized finite expectations. The assignment and finite-average definitions are reusable. Contributions that prove the structural validity of the reservation assignment, the classical success guarantee, Lemmas 3.1–3.3, or the final combination all advance the stated target.
A martingale difference sequence is the standard model of a "fair" sequence of observations whose terms may depend on the past: each new term has conditional mean zero given everything observed before it. Laws of large numbers for such sequences underlie the analysis of stochastic approximation, sequential estimation and online learning, where the noise terms are dependent but conditionally centred.
Classical strong laws concern averages in which every observation keeps the same weight as the sample grows. Kazuoki Azuma's 1967 paper Weighted sums of certain dependent random variables (Tôhoku Math. J. 19) studies weighted sums of dependent variables, and is best known for the exponential moment bound that is now called the Azuma inequality (its display (2.4) together with Remark 1). Its Theorem 3 uses that bound to prove a strong law for weighted averages in which the weights are applied in reverse order, so that the oldest observation always receives the newest, largest weight.
Timeline:
Let be a probability space and an increasing family of sub--fields of . A sequence of real random variables is a sequence of martingale differences if, for every , is -measurable and integrable and almost surely. Theorem 3 assumes moreover almost surely for every .
Let be positive increasing weights: and . Put
The sums are the reversed weighted sums. In passing from to every existing term changes its weight, so is in general not a martingale. In the Lean development, is A a n, is Sbar a x n ω, and the martingale-difference property is IsMartingaleDiff μ ℱ x.
If is a sequence of martingale differences with a.s., is positive and nondecreasing, and
then
The milestones follow the paper's proof, in attack order.
The result. Theorem 3 shows that reversed weighting does not destroy the strong law, under a growth condition on the weights that is strictly weaker than the condition of the paper's Theorem 2: the paper reproduces an example of T. Tsuchikura satisfying (4.9) but not that condition. The condition allows rapidly growing weights, provided no single weight carries more than an share of the total. Milestone 2 is the one-sided Azuma inequality in the paper's conditional-expectation form, a tool used throughout probability, combinatorics and learning theory. Milestone 4 is a maximal inequality for a process that is not a martingale, where Doob's inequality cannot be used.
Formalizing it. The theorem is proved in the paper; this mission produces a machine-checked proof. Mathlib contains sub-Gaussian moment-generating-function bounds for martingale differences in a kernel formulation (HasCondSubgaussianMGF, which assumes a standard Borel space), and the Prove2Me platform has two-sided Azuma–Hoeffding inequalities under the same assumption. Neither states Remark 1 or the one-sided tail bound in the paper's conditional-expectation form on an arbitrary probability space, and no strong law for reversed weighted sums is formalized.
The obvious route to a strong law for a martingale, Doob's maximal inequality applied along a geometric subsequence, fails at the first step: is not a martingale, because each new step reweights all earlier terms. The maximum of over a block of indices therefore needs a separate maximal inequality, and it is there that the monotonicity of the weights is indispensable. A second difficulty is quantitative: the exponential tail bound must be summable over blocks whose growth is controlled only through (4.9), which is weaker than the variance-type condition of Theorem 2, so the block sizes and the constants , and have to be chosen to fit together.
Conventions committed to in Lean:
Finset.Icc 1 n, and , are never used. Every hypothesis on and is quantified over .Filtration ℕ. Its first -field plays the role of and is arbitrary rather than trivial; the paper's is a special case, so the formal statements are at least as general.IsLittleO along atTop). is not a hypothesis, since it follows from positivity and monotonicity.limsup is used anywhere.μ.real); conditional expectations are Mathlib's μ[f | ℱ n].A formalization of the goal that replaces by the direct sums , drops the monotonicity of the weights, or strengthens (4.9) to or to states a different theorem and does not count.
A complete development needs the Azuma moment bound in conditional-expectation form, conditional Chebyshev arguments on events, the Borel–Cantelli lemma (in Mathlib) and elementary real analysis of the blocks. The one-sided Azuma inequality and the maximal inequality (4.15) are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of the goal.
A finite Markov decision problem with discounting is solved by Howard's policy improvement routine: start from a stationary policy, switch to actions that do better against its value, repeat. When the discount factor tends to the total discounted income typically diverges, and the natural targets become the long-run average income and, among policies with the best average, the policy that does best in the transient phase. Howard treated this undiscounted case directly (Howard, 1960). David Blackwell's 1962 paper (Blackwell, 1962) treats as a limit of : it expands the discounted return of a stationary policy in powers of and reads off which policies remain good as . The two leading coefficients of that expansion, the gain and the bias , became the standard objects of average-reward and sensitive-discount optimality (Veinott, 1969; Puterman, 1994, Ch. 8–10).
Timeline. Howard (1960) gives policy iteration for discounted and average-income problems. Blackwell (1962) proves that some stationary policy is optimal for all near (his Theorem 5, the subject of a companion mission) and, in Theorem 4, characterizes the nearly optimal stationary policies through and . Miller and Veinott (1969) and Veinott (1969) extend the expansion to all orders (-discount optimality).
There are finitely many states and a finite nonempty set of actions. Action in state pays an income and moves the system to with probability . is the finite set of decision rules . A policy is a sequence of decision rules; uses every day, and uses first and then . For , is the vector and the Markov matrix . The discounted return of is the vector
and abbreviates . Vectors are compared coordinatewise; means and . A policy is β-optimal if its return dominates that of every policy, and is the return of a β-optimal policy. It is optimal if it is β-optimal for all sufficiently near , and nearly optimal if as .
For any Markov matrix , the limit matrix is the limit of , and the deviation matrix is . For a rule , and are those of , and
With , the set consists of the actions with , or with and ; consists of those with equality in both.
For any with for all :
Milestones: Lemma 1(b) (), Theorem 4(b) (improvement for β near 1), 4(c) (a sufficient condition for optimality), Lemma 2, and 4(d) (a sufficient condition for near optimality).
The mission also states, as intermediate results:
Theorem 4(e) says that near optimality for β near 1 is exactly lexicographic maximization: first of the average income , then of the bias . It justifies the two-level optimality equations used throughout average-reward dynamic programming and shows that, once the β = 1 improvement routine stops, the remaining problem is a bias maximization over the gain-optimal rules. Theorem 4(a) is the first two terms of the Laurent expansion of discounted values, the starting point of sensitive-discount optimality.
The results are classical and proved in the paper (Lemma 1 with a reference to Kemeny and Snell); no machine-checked proof of them is known on the platform. A complete development produces a multichain theory of Cesàro limit and deviation matrices of arbitrary finite Markov matrices, which Mathlib does not have, and the expansion of discounted returns near β = 1.
Lemma 1 must be proved for every Markov matrix, including reducible and periodic ones, where does not converge and the stationary distribution is not unique; arguments through the Perron–Frobenius eigenvector of an irreducible chain do not apply. In Theorem 4(e) the hard part is the existence of a single whose bias dominates every gain-optimal rule in every coordinate at once; a rule maximizing each coordinate separately is not enough. The final characterization compares a stationary policy with all policies, including time-dependent ones, through .
States and actions are finite nonempty types; incomes are real of any sign; a policy is a sequence ℕ → (St → Act) with π 0 the paper's . is a real tsum. is limUnder of the Cesàro means, and its existence is Lemma 1(a), not an assumption; is a matrix tsum, whose summability for is part of Lemma 1(d); uses Mathlib's total inverse, whose nonsingularity is also part of Lemma 1(d). and are defined by the closed forms and from the paper's proof, and Theorem 4(a) asserts that they are the unique solutions of the paper's defining systems. Limits "as β → 1" are along . "Nearly optimal" is encoded without : for every , for all β in some interval , every policy's return is at most in every coordinate; this is equivalent to because a β-optimal policy exists. "Optimal" (§4) and "β-optimal" (§3) are distinct definitions, and Theorem 3's β-dependent improvement set is distinct from the §4 set .
A formalization in which optimality or near optimality is tested only against stationary policies, or in which is assumed to exist or the chain to be irreducible, proves a different and easier theorem and does not meet the targets.
Contributions are welcome at every level: the Cesàro and Abel limit theory of finite Markov matrices (reusable well beyond this paper), the policy improvement theorem for fixed β, and the comparison arguments of Theorem 4. Theorem 3 and the Corollary are also drafted in the companion mission on Theorem 5 in another namespace.
Set cover is one of the basic covering problems of combinatorial optimization: given a ground set and a family of subsets with costs, choose a cheapest subfamily whose union contains every element. In many applications the elements to be covered are not known in advance but appear over time: requests for a service that must be served by opening facilities, clients that must be assigned to servers, or constraints of a covering program that are revealed one at a time. Each arriving element must be covered at once, and decisions cannot be undone. This is the online set cover problem, introduced by Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 39(2), 2009; conference version STOC 2003).
The quality of an online algorithm is measured by its competitive ratio: the worst case, over all arrival sequences, of the ratio between the algorithm's cost and the cost of an optimal offline cover of the elements that actually arrived. The paper gives a deterministic algorithm with ratio , where is the number of elements and the number of sets, and shows a nearly matching lower bound for deterministic algorithms. Its algorithm for the weighted case, analysed with a potential function, became a template for the online primal–dual method surveyed by Buchbinder and Naor (Found. Trends Theor. Comput. Sci. 3(2–3), 2009).
This mission formalizes the core of the weighted result: the algorithm that is given a value at least the optimal cost, and its guarantee (Theorem 3.4).
The ground set has elements and the family has sets; every set has a cost . Both are known to the algorithm in advance. For an element , denotes the sets containing . Elements of an unknown subset of arrive one at a time in a sequence ; on arrival each must be covered by a chosen set. The chosen family can only grow. is any family covering every arriving element, and .
The algorithm is given . It discards sets costing more than , buys sets costing at most outright, and rescales costs; on the resulting normalized instance and for every set (p. 365).
The algorithm keeps a weight for every set, initially ; the weight of an element is . With the set of covered elements and the indicator of , the potential is
with natural logarithms throughout. When arrives with nothing happens; otherwise the algorithm performs weight augmentation steps while . In a step, for each : (a) ; (b) if , add to when does not exceed its value before (a); (c) if has increased, return FAIL.
In Lean, the instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance over finite types X (elements) and T (sets), with the published elementWeight, coveredBy and potential. The run is OnlineSetCover.Weighted.Reachable inst α σ, the set of configurations reachable from initState σ under the transition relation Step.
On the normalized instance, with covering , , and , every reachable configuration is a running state (never FAIL) in which (i) every with is covered, and (ii)
The Proved platform theorem OnlinePrimalDual.OnlineSetCover.algorithm_correctness (the last paragraph of the proof of Theorem 3.4, with the invariant assumed) is included as a supporting reference.
Theorem 3.4 is the analysis of the subroutine; with the doubling over guesses of described on pp. 364–365 (which loses a factor of at most 4) it yields the paper's deterministic -competitive algorithm for weighted online set cover. The lower bound of Section 4 shows that no deterministic algorithm can do much better on general instances, so the result is close to the deterministic optimum. The technique, a potential that couples a fractional multiplicative-weights solution to a deterministic rounding, reappears in online covering and packing, online facility location and related problems.
The result is proved in the paper and restated in the Buchbinder–Naor monograph. On Prove2Me, the monograph's final step (from the invariant to the cost bound) is a Proved theorem, and its expectation form of the monotonicity lemma is Disproved because it omits the hypothesis . Neither the full statement about the algorithm's run nor Lemmas 3.1, 3.2 and the corrected Lemma 3.3 are formalized on the platform. This mission produces them, with the terms replaced by explicit expressions.
The cost bound in the last step is short once two facts about the run are available: that stays below , and that the fractional cost stays logarithmic. Neither is a local fact about one state. The first requires showing that, at every per-set step, one of the two deterministic choices (add or not) does not increase ; the paper proves this by a probabilistic argument over an auxiliary randomized choice, and the bound on the exponential term depends on the cost of the set being at most . The platform's earlier statement of this lemma, which omits that hypothesis, is Disproved. The second requires a bound on the number of augmentation steps over the whole run, which depends on the run's history and not on any single state. In Lean both are inductions over an operational semantics with real-valued exponentials and powers , where the initial bound is a genuine size condition on and .
The run is a small-step transition relation. A state records the weights, the cover, the number of augmentation steps begun, the elements not yet given, and the position inside the current step; FAIL is a separate terminal configuration. The order in which a step visits is arbitrary and may differ between steps; every statement holds for every order. "Throughout the algorithm" means every reachable configuration, including those between per-set substeps. Arrival sequences are arbitrary lists (repetitions allowed) of elements covered by .
Conventions: costs, weights and are real; and are the cardinalities of the finite types cast to ; is Real.log; and are real powers. The paper's asymptotic expressions are replaced by what its proofs establish:
The goal is a statement about the configurations the algorithm actually reaches from and the empty cover. Taking the invariant or the fractional-cost bound as a hypothesis on an arbitrary state would trivialize it, and is ruled out: those are exactly what the milestones establish. The doubling wrapper for unknown is not part of this mission.
A complete development needs an invariant for reachable states (positive weights, steps of an element processed in full), the per-set potential inequality, and the step-counting argument. The per-set inequality is reusable for the monograph's version of the algorithm. Contributions of proofs of any milestone, and of auxiliary invariants as separate lemmas, are welcome.
In the online set cover problem of Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 2009; preliminary version STOC 2003), a ground set and a family of subsets are known in advance, but the elements that actually need covering arrive one at a time, and each must be covered on arrival by sets chosen irrevocably. The paper's motivating example is a network of servers with activation costs: the set of potential clients is known, the clients that actually request service are not, and each request must be served on arrival.
The paper gives a deterministic online algorithm whose cost is within a factor of the offline optimum, where is the number of elements and the number of sets. Its Section 4 shows that this is close to optimal for deterministic algorithms: for all interesting values of and , every deterministic online algorithm has competitive ratio . The lower bound is the reason the product, rather than the of offline approximation (Feige 1998), is the right target online. The online primal–dual framework that grew out of this paper (Buchbinder and Naor 2009) cites it as the benchmark for online covering problems.
This mission formalizes the exact, non-asymptotic statements behind that lower bound: Propositions 4.1 and 4.2 of the paper.
A ground set and a family of distinct subsets of are fixed and known to the algorithm; . An adversary presents elements of one by one, choosing each after seeing the algorithm's previous responses. A deterministic online algorithm , on the arrival of , sees the earlier arrivals and , and adds a finite family of sets to its collection; sets are never removed. It is valid if after every arrival that lies in some member of , that element lies in a chosen set. After an arrival sequence the chosen collection is , and since every set has unit cost, the cost is . The offline optimum is the least number of members of covering the elements of . The competitive ratio of is at least when some arrival sequence has and .
Two families are used.
and the family consists of all ; it has members.
For all positive integers and all with
there is a family of exactly distinct subsets of an -element set such that for every valid deterministic online algorithm there is a nonempty arrival sequence , covered by a single member of , with
The goal leaves the instance existential, as the paper does, and keeps both bounds on and the bound on exactly as printed.
A supporting item (not a milestone) records the count of the block family.
The result. Proposition 4.2 is the exact statement behind the paper's lower bound: choosing of order and of order turns it into the asymptotic bound , which shows that the paper's algorithm is optimal among deterministic algorithms up to a factor. Without it, the gap between the achievable offline and the achieved online would be unexplained. Proposition 4.1 alone gives the matching bound when .
Formalizing it. Both propositions are proved in the paper; neither is formalized anywhere to our knowledge. The mission produces a reusable model of deterministic online algorithms against an adaptive adversary, with a validity notion and a cost, and machine-checked adversary arguments on it. The paper's proof tacitly lets the algorithm add one set per arrival; the statements here cover algorithms that add any number of sets per arrival, so a complete formalization also closes that gap.
The adversary must be adaptive, and the quantifiers are ordered instance, then algorithm, then arrival sequence. The obvious single-block argument (Proposition 4.1) forces only sets. To force sets with , the adversary must move to blocks that no chosen set has touched yet, which requires counting the blocks touched by the sets chosen so far. When an algorithm adds many sets at once, the paper's count "at most blocks after steps" no longer applies as written, and the stopping rule has to be phrased in terms of the cost already paid. The padding of Proposition 4.2 must reach exactly elements and exactly distinct sets without creating sets that help cover the adversary's elements.
The ground set is a Fin type: Fin (2^k) for Proposition 4.1, Fin (k r²) × Fin (2^k) (block, element) for the block family, Fin n for Proposition 4.2. A family is a Finset (Finset X), so its cardinality counts distinct sets. Bit (1-based) of is Nat.testBit j (i-1). An online algorithm is a function from (earlier arrivals in arrival order, current element) to the finite family of sets it adds; it may add any number of sets. Validity demands coverage only for elements that some member of the family contains. Costs are unit (the problem of Section 4 is unweighted).
The offline optimum is never encoded as an infimum: lower bounds exhibit a nonempty arrival sequence and a single covering set (), and the upper bound of Proposition 4.1 quantifies over all offline covers. This rules out the trivializing reading in which the empty arrival sequence satisfies as .
The statements contain no : every quantity is the paper's exact one. The asymptotic bound (8) under the range (7), whose final paragraph only sketches the choice of and , is excluded, as are the remarks on the trivial ratio- and algorithms.
Contributions welcome: proofs of the milestones; lemmas on the chosen collection (monotonicity, decomposition along a sequence); the count of the block family; and the padding construction of Proposition 4.2. The online-algorithm model is reusable for other deterministic online covering lower bounds.
Set cover asks for the fewest sets from a family of subsets of a ground set of elements whose union contains . It is NP-hard, and the best ratio achievable in polynomial time is (Feige 1998, doi:10.1145/285055.285059).
Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 39(2), 2009; preliminary version STOC 2003) introduced an online version. The instance is known in advance, but an adversary reveals elements one at a time, and each revealed element must be covered at once, by sets that can never be removed later. The set of elements that will actually be revealed is unknown. The paper's motivating example is a network of servers: the potential clients and the servers that can serve each client are known, but which clients will request service is not, and every activated server costs money.
The question is how much an algorithm loses against an offline adversary who knows and covers it with a family . This mission formalizes the paper's answer for unit costs (Section 2): a deterministic algorithm whose cover is within a factor of . Section 3 of the paper extends the algorithm to weighted sets and Section 4 proves a nearly matching lower bound; those are separate missions of this series.
An instance consists of a finite ground set with elements and a finite family of sets. For an element , is the collection of sets containing . Every set has cost , so the cost of a family is its number of members.
The adversary gives a sequence of elements (the given elements form ). A family covers if each element of lies in some member of it.
The algorithm keeps a weight for every set, initially , and a cover , initially empty. The weight of an element is , and is the set of elements covered by members of . The potential is
When the adversary gives an element :
Step (c) prescribes a property of the chosen sets, not the sets themselves. A run on is any sequence of iterations, one per arrival, in which every iteration makes an admissible choice.
For , every arrival sequence , and every family covering : a run of the algorithm on exists, and every run ends with a cover that covers every element of and satisfies
The paper states ; the displayed bound is the constant its proof produces. Because the bound holds for every covering family, it holds in particular for an optimal one.
Lemma 2.1. In every run, the number of iterations with a weight augmentation is at most
Lemma 2.2. In an iteration with a weight augmentation, from a state with positive weights, there is a family with such that
where is the potential before the iteration and the potential after it, computed with the augmented weights and the cover .
The theorem shows that online set cover over a known instance admits a deterministic -competitive algorithm. Section 4 of the paper shows this is nearly optimal: no deterministic algorithm achieves over a wide range of parameters. Its multiplicative weight updates were developed further into the online primal–dual framework for covering problems of Buchbinder and Naor (FnT TCS 3(2–3), 2009), whose Section 5.1 restates this algorithm.
The result is proved in the paper; it is not machine-checked. The Prove2Me platform has the weighted version's final counting step from the Buchbinder–Naor monograph, but no statement of Section 2. A complete development here gives a checked proof of the unweighted competitive ratio with an explicit constant, together with a reusable formal model of an online algorithm with a nondeterministic step, whose correctness includes the existence of an admissible choice at every step.
The central step is Lemma 2.2: a family of at most sets that keeps the potential from increasing must exist at every augmentation. The obvious rules fail. Adding every set of can exceed the cardinality bound, since may contain up to sets. Adding nothing, or a single set, can increase : every uncovered element sharing a set with has its weight raised, and its term grows by a factor up to . The paper's argument is non-constructive, and a formal proof must establish existence for a finite averaging statement over real powers of .
The second difficulty is that the algorithm is nondeterministic. A statement "every run has property P" is empty if no run exists, and the existence of a run is exactly Lemma 2.2 applied at every step under the invariants that weights stay positive and that each arriving element lies in some set. Feasibility (that every given element ends up covered) is not part of the algorithm's rule; it follows from the potential never increasing, which needs and a careful treatment of the initial potential, which is at most and equals when every element lies in every set.
The instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance (finite types E of elements and T of set indices, incidence elemSets), with the published elementWeight () and coveredBy (). Its positive cost field is not used: all sets have unit cost and the cover is measured by its cardinality. and . Weights are real numbers; is the real power.
The algorithm is the definition OnlineSetCover.Unweighted.Algorithm: a relation Step for one iteration (recording whether a weight augmentation occurred) and Run for a sequence of iterations from the initial state, counting augmentations. Arrival sequences are lists and may repeat elements.
Explicit forms of the paper's asymptotic and unspecified quantities:
The goal adds the hypothesis , which the paper's assumes tacitly: for no set may be added and the element is never covered.
Replacing the algorithm by the set of states whose potential is at most the initial one, or dropping the existence of a run from the goal, gives a weaker theorem; part (a) of the goal rules this out.
A complete development needs elementary real analysis (Real.rpow, Real.log, ), a finite probabilistic or averaging argument for Lemma 2.2, and induction over runs. Contributions are welcome on any milestone; a derandomized averaging lemma for Lemma 2.2 would be reusable in the weighted mission of this series.
The conditional logit model is the workhorse of discrete choice analysis: it is used to forecast travel mode shares, to estimate demand for differentiated products, and, in operations research, as the multinomial logit (MNL) choice model behind assortment optimization and revenue management. Its selection probabilities have the form . Daniel McFadden's 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior gave the model two behavioural foundations, one of which is the subject of this mission: the logit form is a consequence of a single axiom on how choice probabilities change when the set of available alternatives changes.
That axiom is Luce's choice axiom, which McFadden calls Independence of Irrelevant Alternatives (IIA): the relative odds of choosing one alternative over another do not depend on which other alternatives are present. Luce (1959) introduced it; McFadden (1974, §I) showed how, together with positivity and a mild condition on which alternative sets can occur, it yields the conditional logit form with a "utility indicator" shared by all alternative sets.
Timeline. Luce, Individual Choice Behavior (1959): the choice axiom and its ratio-scale representation. McFadden (1974, pp. 109–110): the derivation in the econometric setting with measured attributes , the binary-odds identities (5)–(10), and footnote 3, which removes an extra axiom (Axiom 3) by a universal benchmark alternative. McFadden (1974, pp. 111–112): the companion random-utility characterization by extreme-value shocks, treated in mission 2 of this series.
Let be the universe of objects of choice and the universe of vectors of measured attributes of decision-makers. An alternative set is a finite set ; a designated family of finite sets is the family of possible alternative sets. The selection probability is the probability that an individual drawn at random from the population, with attributes and facing , chooses . For every and possible , is a probability vector on . Whenever belong to a possible set, the pair is possible too, so binary choices are defined.
In Lean these are IsSelectionProb, PairsPossible, Axiom1, Axiom2, binProb, altSetV and IsUniversalBenchmark in the namespace McFadden1974.IIA.
Under Axioms 1 and 2 and a universal benchmark , with , for every , every possible (containing or not) and every :
The function is the same for all alternative sets; this is what distinguishes the goal from Equation (10).
The result. The goal identifies a testable axiom on choice probabilities, IIA, with a parametric functional form, the conditional logit model. It is what licenses the econometric specification estimated in the rest of McFadden's chapter, and it is the reason the MNL model is the default in assortment and pricing problems in operations research. It also makes the model's limitations precise: any population whose choices violate IIA (the auto/red-bus/blue-bus example on p. 113 of the chapter) cannot be logit.
Formalizing it. The result is classical and proved on paper. No machine-checked statement of it exists on the platform, which has the logit form only as a definition (soft-max, MNL revenue) and IIA only in Arrow's social-choice sense, a different axiom about preference aggregation. This mission produces a formal statement of the derivation with every standing assumption explicit, including two the paper leaves implicit: that selection probabilities are normalized on binary sets, and that binary subsets of possible sets are possible.
The algebra is elementary; the difficulty is bookkeeping of where each axiom may be applied. Axioms 1 and 2 are assumed only on possible alternative sets. Equation (10) needs the benchmark to lie in the alternative set, and the naive argument "pick as benchmark" produces a function that depends on the set through the choice of . The goal requires a single for all sets, including sets that do not contain , where neither Equation (10) nor the axioms on alone say anything about . A second subtlety is the diagonal: , so is set to by definition rather than read off a singleton choice.
Alternatives form a type X with decidable equality, alternative sets are Finset X, possible sets are a Set (Finset X), and selection probabilities are a real-valued function P : S → Finset X → X → ℝ. Only values P s B x with x ∈ B and B possible are constrained; no statement depends on the others. binProb sets the diagonal to 1/2. altSetV uses Real.log, which is 0 on non-positive arguments; under Axiom 2 on the binary sets its argument is always positive where it is used.
The probability-vector hypothesis on every possible set, binary sets included, is part of every statement: without it the zero function satisfies Axiom 1 vacuously and Equations (7)–(8) fail. The goal is stated with the explicit , never as "for each there is a ", which would only restate (10).
Nothing beyond Mathlib's finite sums, Real.exp and Real.log is needed. Proofs of the milestones and of the goal are welcome, as is a formal statement of the auto/bus example or of the converse (logit selection probabilities satisfy Axioms 1 and 2).
A set function on a finite ground set is submodular if it has diminishing returns, equivalently if for all . Cut functions of graphs and hypergraphs, coverage functions, entropy, and many facility-location and welfare objectives are submodular. Unconstrained Submodular Maximization (USM) asks, given a nonnegative submodular through a value oracle, for a set of maximum value. It contains Max-Cut, Max-DiCut and Max Facility Location as special cases, and it is a subroutine in algorithms for constrained submodular maximization.
Timeline:
Let be a finite ground set and a nonnegative submodular function. Write , and let denote a set attaining it.
Algorithm 1 (DeterministicUSM) fixes an arbitrary order of and maintains two solutions, starting from and . In iteration it computes
If it sets , ; otherwise , . A tie adds . After iterations , which is the output.
The analysis uses the hybrid sets , which agree with and on and with on . In Lean, the run is state f l i, the state after the first entries of the order l, and is optI O (state f l i).
For every nonnegative submodular and every order of ,
The result. Algorithm 1 is the deterministic member of the double greedy family. It makes one pass over the ground set with four value queries per element, and it guarantees of the optimum for every order, without the polynomial-but-large running time and the loss of local search. Its analysis, which charges the decrease of to the increases of and , is the template the paper then refines into the randomized -approximation (Theorem I.2) and its continuous counterpart on the multilinear extension. Theorem II.3 shows that is the exact ratio of this algorithm, so the improvement to requires randomization (or a different deterministic rule) rather than a sharper analysis.
Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal statement of the algorithm as printed, a checked proof of its guarantee for every order, and a checked tight instance. The definitions of the run and of are the same objects the randomized and fractional analyses reason about, so a complete development here is the first step toward the paper's main theorem.
The individual inequalities are short; the difficulty lies in the bookkeeping. Each step needs the invariants and , which follow from the order being an enumeration (no repetitions, every element present), and the identification of from in each branch of the algorithm. Summing Lemma II.2 needs a telescoping over the run defined as a fold. The naive idea of comparing with directly, without the hybrid sets, gives no bound: the greedy choices are made against and , not against . For Theorem II.3 the difficulty is producing an explicit instance, checking that it is submodular and nonnegative, and tracing the run, including the ties, which the algorithm resolves by adding.
X with decidable equality; subsets are Finset X; is real valued, Finset X → ℝ, and nonnegativity is the hypothesis ∀ S, 0 ≤ f S where the page uses it (the goal, the telescoped display and the tight example). Lemma II.1, Lemma II.2 and the hybrid-sequence milestone do not assume it.NonmonotoneSubmod.Shared.Submodular. The paper's main-text sentence ("for every and ") would force monotonicity when and is read as the footnote. is the published NonmonotoneSubmod.Shared.OPT f, the maximum of over all subsets.l with l.Nodup and ∀ x, x ∈ l; is l[i - 1]. Every statement quantifies over all such lists. No nonemptiness of is assumed: for an empty ground set the goal reads .O with ∀ S, f S ≤ f O.List.foldl over List.take, on membership in the states of the run, and on telescoping sums over . A reusable lemma "the run keeps and decides exactly " would serve all three missions of this paper. Contributions of proofs of any milestone, of the goal from the milestones, and of the tight instance (e.g. the paper's five-vertex directed cut function) are welcome.Weighted sums of dependent random variables occur when the weights change with the observation horizon. Even if each random variable is bounded and centered, allowing the weights in row to be chosen anew makes an almost-sure statement about all large different from a bound on a single finite sum. Kazuo Azuma's 1967 paper treats this situation under a finite-product moment condition called class [M]. Its first main theorem bounds every row of an arbitrary real triangular array at the scale given by that row's Euclidean norm and .
The condition is useful because it allows dependence. The paper notes that bounded martingale differences provide examples, but Theorem 1 is stated directly for class [M], without introducing a filtration in the result. The conclusion therefore records the property of the random variables actually used by this part of the paper, rather than restricting the mission to one familiar source of examples. Azuma, §1 and Theorem 1.
Fix a probability space . Let be real measurable random variables. They form a bounded multiplicative system with unit bounds if almost surely for every , and
The indices in are distinct. Taking a singleton shows ; taking sets of two, three, or more indices imposes the full condition used in the paper. Pairwise zero correlations by themselves do not state class [M]. All bounds and moment conditions are for the positive indices, so is outside the mathematical sequence. Azuma, p. 357, property [M].
For each , choose real coefficients . There is no relation required between different rows. Define the weighted sum and its weight norm by
Both definitions use the source's 1-based indices. A row of zero weights has and almost surely; such rows remain within the theorem. Azuma, p. 359, §3.
The goal is Theorem 1, display (3.1): for every bounded multiplicative system and every real triangular array,
The normalizing constant is exactly , and the upper bound is exactly . The mission does not assume that grows, converges, or stays positive. In Lean, the target is stated as the equivalent operational bound: for each , almost every outcome eventually satisfies . This includes zero-weight rows without assigning a meaning to a real quotient .
The milestone list follows results displayed in the paper: the corrected convexity inequality (2.2), Lemma 1's exponential moment estimate (2.1), the exponential estimate in the proof of Theorem 1 with its factor , and the almost-sure finite exponential series on the next page. Lemma 1 gives, for arbitrary real and ,
The paper prints (2.2) with a missing factor in its linear term. The mission records the printed text as provenance and states the corrected inequality in Lean; the printed version fails already when and . Azuma, pp. 357–360.
Theorem 1 turns an exponential moment bound for each finite weighted sum into a single almost-sure assertion along an entire triangular array. It gives a scale that adapts to the actual coefficients in each row: two arrays with different row norms receive different bounds, while no regularity across rows is required. The result is also the starting point for the weighted strong-law corollaries that follow it in the paper. Azuma, Theorem 1 and Corollary 1.
The mathematical theorem has been proved since 1967. This mission's remaining work is a machine-checked Lean proof of the exact theorem and its listed intermediate statements. A complete development would add reusable formal statements for bounded multiplicative systems and for their finite exponential moments. Those objects could support later work on dependent sums without importing a filtration or a stronger independence assumption. The proposal statements compile as open goals; compilation alone does not supply proofs.
The usual first step for independent bounded variables is to factor the exponential moment into one-variable expectations. Class [M] does not assume independence, so that factorization is unavailable. The condition controls every product with distinct indices, while allowing other dependence. The almost-sure conclusion must also hold when the coefficients change arbitrarily with : bounds that depend on one fixed row do not by themselves settle what happens for all sufficiently large rows. Finally, rows with require a statement that preserves the theorem rather than excluding them by an added positivity hypothesis.
The Lean development represents the probability law by a measure with IsProbabilityMeasure μ, and a random sequence by . It uses measurable variables and states the unit bound almost surely at every positive index. The class [M] predicate quantifies over every nonempty finite set of positive indices; no conditional expectations, filtration, symmetry, or independence hypotheses enter Theorem 1. Finite products and finite weighted sums use ordinary real multiplication and Finset.Icc 1 n. The triangular weights have type , and only entries with contribute.
The norm is the nonnegative real square root of the sum of squared weights. Real.log is zero at and in Lean, but the target is eventually quantified, so its asymptotic content concerns large . The exponential estimate is stated for . If , Lean's total division returns zero in the exponent's quotient; all weights in that row are zero, making this extension valid. In the almost-sure series, the term at index zero is set to zero. The source's limsup is represented by eventual inequalities for every positive excess, avoiding a real-valued limsup default on unbounded sequences.
The definition of class [M] includes every finite product, including singletons; replacing it by pairwise orthogonality would change the theorem. Measurability and the almost-sure unit bounds ensure that the finite products and the exponential functions in Lemma 1 are integrable, so their Lean integrals represent expectations. Contributions toward proofs of the corrected convexity bound, the moment estimate, the exponential series, and the final almost-sure step are all within scope. The finite-product predicate and the exponential estimate are reusable beyond this mission.
A learning algorithm generalizes when its error on fresh data is close to its error on the training sample. Bousquet and Elisseeff (JMLR 2, 2002) showed that a single property of the algorithm, uniform stability, controls this gap with exponential concentration: if removing any one example from a training set of size changes the loss of the output at every point by at most , the generalization error exceeds the empirical error by roughly with probability (their Theorem 12). The bound is useful only when , and the second half of the paper identifies algorithms with that rate: Tikhonov regularization in a reproducing kernel Hilbert space (Theorem 22), and relative-entropy regularization of mixtures (Theorem 24), the subject of this mission.
Mixtures arise whenever a learner outputs a distribution over a parametric base class instead of a single hypothesis: Bayesian posterior averaging, Gibbs and randomized classifiers, exponential weights. Regularizing by the relative entropy to a prior is the maximum-a-posteriori reading of these procedures, and Theorem 24 is one of the earliest results showing that such posteriors are uniformly stable with rate . The same mechanism (entropic regularization, stability through Pinsker's inequality) reappears in PAC-Bayesian analysis and in the stability of exponential-weights methods.
Let be a measurable space with a reference measure , and write for integration against . A base class is indexed by , and is the loss of the base hypothesis at an example .
The algorithm outputs a density with respect to : a measurable, nonnegative, integrable with . denotes the set of all densities. A density is scored by the averaged loss
the expected loss of a randomized predictor that draws from . The relative entropy of to is
with when is not absolutely continuous with respect to or the integrand is not integrable.
Fix a prior , a parameter , and a training set . The algorithm returns a minimizer over of
For an index , the truncated objective is , and denotes one of its minimizers over .
For every minimizer of (29), every minimizer of the truncated objective, and every example ,
Theorem 24 places entropy-regularized posteriors among the algorithms to which the paper's exponential generalization bound applies: combined with Theorem 12 it gives, for the averaged loss, a deviation of order . The proof also yields the bound , which by itself gives classification stability for base hypotheses with values in (remark after Theorem 24, p. 518).
The result is proved in the paper; no machine-checked proof is known to exist. A formalization produces reusable pieces that Mathlib does not have: Pinsker's inequality for densities in form (Mathlib has the Kullback–Leibler divergence InformationTheory.klDiv, but not Pinsker), the Bregman identity for the relative entropy, and a stability statement for minimizers over a space of probability densities.
The paper derives Theorem 24 from Lemma 21, which is stated for a regularizer that is defined and differentiable on a vector space. The relative entropy is defined only on the convex set of densities and is not differentiable at densities that vanish on a set of positive measure, so the general lemma does not literally apply, and the identity needs integrability conditions that the page does not state. A complete proof of the goal must either justify that application on the set of densities, or work directly with the minimizers, which requires identifying them and handling the values of . Pinsker's inequality itself requires a separate argument at the level of general measures.
IsDensity ν g: measurable, nonnegative, integrable, total mass one, with respect to a σ-finite reference measure ν. The integral is always against ν, never Lebesgue measure.r : Θ → Z → ℝ, measurable in θ, with 0 ≤ r ≤ M; the paper's costs are nonnegative (p. 502).InformationTheory.klDiv of the measures g · ν and g' · ν, in ℝ≥0∞. The objectives (29) and its truncation take values in ℝ≥0∞. A formalization that converts to a real number with toReal would send to and make the worst densities minimizers; that reading is excluded.f minimizes (29) and f' minimizes the truncated objective over all densities, for the given S : Fin m → Z and i : Fin m.Contributions welcome: proofs of Pinsker's inequality for klDiv (reusable far beyond this mission), of the Bregman identity, of Lemma 21, and of the goal by any route.
An agent can learn to act in an unknown environment by repeatedly running a finite episode, observing the states reached after its actions, and updating its model of the environment. The agent must trade off rewards in the current episode against information that may improve later decisions. A regret bound measures the cumulative value lost relative to an optimal policy that knows the true transition probabilities. Its dependence on the number of states, actions, episode steps, and interactions says how much exploration that uncertainty can force.
Azar, Osband, and Munos study this question for a finite-horizon Markov decision process with known, bounded rewards and an unknown, stationary transition kernel. Their UCBVI algorithm estimates action values from observed transitions and adds an exploration bonus. Their second version, UCBVI-BF, uses the empirical variance of the next-state value in that bonus. Their Theorem 2 gives an explicit high-probability regret bound whose leading dependence on the horizon is smaller than the bound they give for the simpler UCBVI-CH bonus. The paper states that, in a sufficiently long-run regime, its leading order matches the cited lower-bound scale up to logarithmic factors. This mission targets the explicit theorem, including its lower-order terms, rather than only that asymptotic comparison.
Let and be nonempty finite state and action sets with cardinalities and . A stationary transition kernel is a probability distribution on next states for every current state and action . The reward is deterministic, known to the learner, and lies in . These are the conditions of Assumption 1 and §2. Episodes have steps; episodes comprise interactions.
A policy chooses an action for each state and step. Its value is the expected reward from step through the final step when the state at is ; the terminal value is . The optimal value ranges over all deterministic policies of this form. At the start of episode , the environment may choose the initial state using the completed episodes. The learner then fixes a policy , observes transitions during the episode, and updates counts for the next episode. Its regret is
For each state-action pair, counts transitions to in episodes before , and . When the latter is positive, . The count records previous episodes whose state at step was . Algorithms 2 and 4 compute optimistic backward from zero terminal value, take a minimum with the previous episode's estimate and with , and choose a maximizing action at every state. Previously unseen pairs receive . The Bernstein–Freedman bonus uses the empirical variance of under and an additional term based on ; the algorithm uses .
The goal is Theorem 2 on p. 5. For any MDP and interaction described above and every , write . The target is the exact bad-event form of the printed high-probability bound:
The milestone list contains three empirical-transition deviations from the proof of Lemma 1: Eq. (9) for a value-weighted transition error, the displayed count bound before Eq. (11), and Eq. (12) for the full transition row's error. It also contains Lemma 2's variance comparison and Eq. (26), which relates cumulative conditional next-value variance to the variance of an episode return. These are source-indexed targets, with their printed constants retained.
The theorem gives a quantitative guarantee for a particular executable decision rule: its regret grows sublinearly in in the leading term, with explicit dependence on , , and . The result lets one compare the horizon dependence of a variance-sensitive bonus with a value-agnostic bonus under the same finite-horizon model. It also fixes which logarithm belongs in the algorithm and which appears in the reported bound; replacing either changes the claim.
A formal proof would connect a fully specified adaptive interaction to its finite probability law, empirical counts, backward value iteration, and the stated high-probability conclusion. The local prior-art search found reusable transition-kernel vocabulary and general concentration tools, but no published formal statement of this exact UCBVI-BF algorithm or theorem. The mission's finite path and variance definitions can also support other episodic reinforcement-learning bounds that use conditional variance.
The bonus is computed using a value function that itself depends on earlier observations and the same episode's backward recursion. A concentration inequality for a fixed transition row and a fixed test function therefore does not directly control every value estimate encountered by the algorithm. The number of samples in a row is also random and changes with the learner's past actions. The regret compares a policy's value at an environment-chosen initial state with a supremum over all policies, while the learner's greedy action must be defined at states it never visits. These dependencies are the central obstacle to turning local concentration statements into the episode-level bound.
The Lean model uses finite sums rather than measure theory. A published predicate supplies the stationary, real-valued transition kernel; a local MDP adds the known deterministic reward. State and action types are finite and nonempty. Policies are deterministic and depend on the step. The supremum defining ranges over their finite function type. A theorem quantifies over every maximizing tie-breaking rule and every initial-state rule that reads only completed episodes. The probability of an event is constructed as a sum over finite outcome sequences, each weighted by the product of true transition probabilities. Counts use all past transitions and no current or future outcomes. These choices rule out a trivialization that assumes the desired law or optimizes over an unbounded class of arbitrary functions.
Lean indexes the steps from zero, while the paper indexes them from one. The last observed next state is kept because Algorithm 4 counts states at the terminal index . At , Algorithm 4's quotient is interpreted as infinite and the capped term is ; Lean's ordinary division by zero would incorrectly produce zero. The algorithm uses , while Theorem 2's bound uses . For Eq. (26), the appendix ends its sums at under a shifted terminal convention; the local statement includes all reward steps and the terminal value used by Algorithm 2. The milestone text remains the printed text. The count milestone is the display before Eq. (11), since Eq. (11) drops a factor of under the square root present in that display.
Theorem 2 retains its printed term. The appendix's displayed Lemma 13 calculation does not reproduce that second-order constant when propagated to Lemma 14; this is a source proof gap, not a hypothesis of the theorem. Work on the probability normalization, random-count concentration, adaptive value estimates, variance identity, and a valid route to the printed explicit constants is welcome. A proof with altered constants or an asymptotic-only conclusion would be a different target.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The source proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It uses the same density estimate as the companion entry, for with (explicit Selberg sieve, weighted first moment, eighth moment of the singular-series factor, Hölder). It then replaces Schnirelmann's sumset inequality by Mann's theorem, for sets containing :
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from . Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The source proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It keeps the explicit Selberg sieve and Schnirelmann's original sumset inequality from the entry, and improves only the density estimate:
Only Chebyshev-type prime bounds, the Selberg upper-bound sieve, Hölder's inequality and Schnirelmann's inequality are used.
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from . Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The source proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It keeps the explicit Selberg sieve and Schnirelmann's original sumset inequality from the entry, and improves the density estimate:
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from . Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.
Optimization problems with orthonormality constraints arise throughout numerical linear algebra and its applications: computing a few eigenvectors or singular vectors, Procrustes problems in statistics and shape analysis, orthogonal factor rotation, independent component analysis, and the orthogonality constraints of electronic-structure calculations. The feasible set of such a problem is the Stiefel manifold of orthonormal -frames in . Riemannian optimization algorithms on this manifold (Riemannian gradient, Newton and trust-region methods; see Absil, Mahony and Sepulchre, Optimization Algorithms on Matrix Manifolds, 2008) take a step in a tangent direction and then need a retraction: a map that brings the updated point back onto the manifold while agreeing with the geometry to first order.
The most natural way to come back to a constraint set is to take the nearest point. P.-A. Absil and J. Malick, Projection-like retractions on matrix manifolds (SIAM J. Optim. 22(1), 2012; the mission follows the authors' version, HAL hal-00651608v2), show in their Proposition 3.2 that the metric projection onto a smooth submanifold yields a retraction, and then work out the projection explicitly for several matrix manifolds. For the Stiefel manifold, their Proposition 3.4 identifies the projection with a factor of the singular value decomposition, equivalently with the orthonormal factor of the polar decomposition. The paper notes that this result was mentioned without proof in Higham's survey of matrix nearness problems, and gives a proof along the lines of Horn and Johnson, Matrix Analysis, §7.4.
Section 4.5 of the same paper treats a second, "orthographic" retraction on the Stiefel manifold, which corrects a tangent step by a normal vector instead of projecting; for the orthogonal group (the case ) it admits a closed form through a matrix square root (Proposition 4.12).
Fix natural numbers . Matrices are real, and carries the Frobenius norm
The Stiefel manifold is
the set of matrices with orthonormal columns; is the orthogonal group .
The singular values of are , the square roots of the eigenvalues of . A singular value decomposition of is a factorization with , , and zero off its diagonal, with nonnegative nonincreasing diagonal entries. For every singular value equals ; in particular .
A projection of onto is a point with for all . A polar decomposition of is a factorization with and symmetric positive definite.
Let and let satisfy . For every singular value decomposition ,
and is the of the polar decomposition : it is the orthonormal factor of every polar decomposition of , and a polar decomposition with this factor exists.
The statement asserts existence, uniqueness and the closed form of the projection on the whole open ball of radius , for whichever singular value decomposition is supplied.
for , skew-symmetric and symmetric with ; and Proposition 4.12,
stated as: is the unique symmetric correction of smallest Frobenius norm.
Proposition 3.4 makes the projective retraction on the Stiefel manifold computable from one singular value decomposition of an matrix, and identifies it with the polar factor, which is also what many numerical codes already compute for re-orthonormalization. Combined with Proposition 3.2 of the paper, it yields a second-order-accurate retraction usable in any Riemannian algorithm on . The same statement is the orthogonal Procrustes problem in the special case of a full-rank target: the nearest orthonormal frame to .
The result is classical and proved; the paper's argument is short but cites two external facts (Weyl's perturbation bound for singular values and the uniqueness of the polar decomposition). To our knowledge no machine-checked proof of the nearest-orthonormal-frame property, of the uniqueness of the polar factor, or of the closed form of Proposition 4.12 exists in Mathlib or on this platform. A formalization produces reusable pieces: the trace inequality over the Stiefel manifold, the uniqueness of the polar decomposition, and the full-rank property near , all of which recur in matrix analysis and in the analysis of Riemannian algorithms.
Existence of a nearest point is easy (the Stiefel manifold is compact), and attainment of the trace bound is a direct computation. The content is in two places. First, the bound for every requires transporting by the orthogonal factors of the singular value decomposition and bounding diagonal entries of a matrix with orthonormal columns. Second, uniqueness does not follow from the trace argument: when is rank deficient there are many maximizers. Uniqueness needs both a perturbation bound (singular values are 1-Lipschitz in the Frobenius norm, so near ) and the uniqueness of the polar factor, which in turn rests on the uniqueness of the positive-semidefinite square root of . Mathlib has singular values of linear maps and the spectral theorem but, at the pinned revision, neither Weyl's inequality for singular values nor the polar decomposition.
For Proposition 4.12, the printed proof compares only two solutions of (4.14), while (4.14) has other symmetric solutions (mixed signs of the square roots, or non-diagonal ones on repeated eigenvalues); minimality must be proved against all of them.
Matrices are Matrix (Fin n) (Fin m) ℝ with the Frobenius norm brought in by open scoped Matrix.Norms.Frobenius. The Stiefel manifold is the set stiefel n m of matrices with Xᵀ * X = 1. Singular values are Mathlib's LinearMap.singularValues of Matrix.toEuclideanLin X, re-indexed to be 1-based as on the page (sv X m is ). A singular value decomposition is the predicate IsSVD X U S V of display (3.5), and is U * E * Vᵀ with E the rectangular identity (frameOfSVD U V). The projection is the set of nearest points, using the published predicate RandomGradFree.Nonsmooth.IsMetricProjection; "exists and is unique" is equality of that set with a singleton. Positive definiteness is Mathlib's Matrix.PosDef, which over includes symmetry.
Standing assumptions and added hypotheses: is the page's assumption of §3.3; is added so that is meaningful. The radius is with strict inequality, kept in that form although its value is . Two misprints of the page are corrected in the Lean and kept in the verbatim milestone texts: the display of Proposition 3.4 reads for , and the distance identity reads for . The uniqueness of the polar factor is stated for positive semidefinite factors under the rank hypothesis, which contains the positive definite case of Proposition 3.4. The matrix square root of §4.5 is defined through Mathlib's spectral theorem; Proposition 4.12 is stated for every admissible symmetric correction, and is vacuous only when no symmetric correction exists.
A trivializing formalization is ruled out: the projection is not taken as a hypothesis or chosen by definition; the goal asserts that the nearest-point set equals the singleton of the explicit matrix, for every singular value decomposition supplied, so neither existence nor uniqueness can be assumed away.
Contributions welcome beyond the stated items: Weyl's inequality in Mathlib's singular-value API, existence of a singular value decomposition in the matrix form (3.5), and the polar decomposition with its uniqueness, all reusable well beyond this mission.
Blackwell approachability is the vector-payoff analogue of von Neumann's minimax theorem. In a repeated game where each round's outcome is a vector , a player wants the running average of these vectors to converge to a target set , whatever the opponent does. Blackwell (1956) showed when this is possible, and approachability has since become a standard tool for calibrated forecasting, regret minimization with respect to general benchmarks, and learning in games.
Online linear optimization (OLO) is the problem of choosing points in a fixed decision set against a sequence of linear losses , with performance measured by regret against the best fixed point in hindsight. Algorithms with regret — "no-regret" algorithms such as online gradient descent (Zinkevich, 2003) — are among the most studied objects of machine learning.
Abernethy, Bartlett and Hazan (COLT 2011) showed that the two problems are algorithmically equivalent: each can be converted into the other with explicit control of the rates. This mission covers the direction from OLO to approachability.
Timeline:
A Blackwell instance consists of compact convex sets , , a payoff that is affine in each argument (biaffine), and a closed convex target set . Write for the Euclidean distance to a set, and for the closed Euclidean ball of radius .
A halfspace oracle takes a halfspace and returns a point ; it is valid if for every halfspace , for all .
A set is a cone if for all , . For , , and the polar cone of is .
An OLO algorithm maps past loss vectors to a point , and its regret is
Algorithm 2 runs on when is a cone: at round it sets , plays , observes , and feeds back to .
When is compact but not a cone, it is lifted: with and the concatenation, put and , and run Algorithm 2 on .
For a Blackwell instance with nonempty and compact, any valid halfspace oracle for the lifted instance, any OLO algorithm with values in , any and any , the run of Algorithm 2 on the lifted instance satisfies
The bound holds for every and every adversary, with no rate assumed for ; a no-regret then gives approachability.
The result. Corollary 18 turns any no-regret algorithm into an approachability strategy for a compact convex target, provided a valid halfspace oracle is available, with rate . Combined with online gradient descent it gives an approachability rate, and through the choice of OLO algorithm it lets approachability inherit the computational efficiency of online learning. The paper uses this route to build an efficient calibrated forecaster (Section 5). Together with the converse reduction (Theorem 16), it shows that the two problems are equivalent.
Formalizing it. The results are proved in the paper; none of them has been machine-checked. Formalizing them requires the conic duality formula for distances (Lemma 13), a quantitative lifting lemma (Lemma 14) and the bookkeeping of an interactive protocol. The proof of Lemma 14 on the page is a sketch: it refers to an undefined point and uses a triangle-similarity argument, so a complete proof is new work.
The reduction's core is Lemma 13: the distance to a cone is a maximum of a linear function over the polar cone's unit ball. Lemma 13 needs projection onto a cone in Euclidean space; for a non-closed cone the projection may not exist, and the argument must go through the closure. The lifting Lemma 14 is a geometric statement whose page proof relies on a picture and an undefined point, so the factor 2 has no complete written argument. Finally, connecting the average lifted payoff to the lift of the average payoff, and the halfspace guarantee to the regret, requires keeping the round indexing and the oracle's validity domain exactly aligned.
All spaces are EuclideanSpace ℝ (Fin d). The concatenation lives in EuclideanSpace ℝ (Fin (d+1)) with coordinate 0 equal to , so ; a product type with the sup norm would change every distance and is ruled out. Distances are Metric.infDist. The polar cone uses the paper's sign (), the negative of Mathlib's innerDual. A halfspace is the pair ; a valid oracle must answer every halfspace containing , including , not only the halfspaces the algorithm happens to query. The OLO algorithm is a map from histories Fin t → ℝᴰ with values in at every history. Rounds are , and the run of Algorithm 2 is given as hypotheses on sequences , which exist and are unique by recursion. The minimum in the regret and are written as sInf/sSup of images over nonempty compact sets, where they are attained.
Hypotheses added relative to the page: and in the goal; in Lemma 13 (the empty set is a cone under Definition 11 and the identity fails for it); in Lemma 14. Corrected misprints, each disclosed in the item's note: "" in Corollary 18 and (9) denotes the regret of the OLO algorithm on the lifted losses; Lemma 14's "" has a stray ; is the maximal norm of the set, not its diameter. The oracle in the goal is a valid oracle for the lifted instance, which is what applying Algorithm 2 to requires.
A formalization in which the oracle is valid only at the run's own queries, the OLO algorithm is unconstrained, the regret's minimum ranges over all of , or the middle term of the goal is dropped, is a different statement and is ruled out.
The development needs: the dual formula for the distance to a convex cone, nearest-point projection onto closed convex sets (in Mathlib), compactness of polar-cone slices, and finite sums of biaffine payoffs. The cone layer (Lemma 13) is reusable for the converse direction of the paper and for conic duality generally. Proofs of any milestone, and of the bridge from an oracle for the original instance to one for the lifted instance, are welcome.
Reinforcement learning methods estimate the value function of a policy : the expected discounted sum of future rewards from each state. When the state space is large, cannot be stored as a table and is approximated by a parametrized function. The most studied case is linear function approximation, where each state carries a feature vector and the estimate is . Temporal-difference learning with this approximation, linear semi-gradient TD(0), is one of the basic algorithms of the field, and Chapter 9 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) presents its analysis: where the algorithm can converge, why that point exists, and how good it is.
The history is short. Sutton (1988, doi:10.1007/BF00115009) introduced TD learning and showed positive definiteness of the matrix governing its expected update. Dayan (1992, doi:10.1007/BF00992701) extended convergence to TD(λ). Tsitsiklis and Van Roy (1997, doi:10.1109/9.580874) proved convergence with probability one for linear TD(λ) under on-policy sampling and bounded the error of the limit. Bradtke and Barto (1996) introduced least-squares TD (LSTD), which computes the same limit directly.
A finite Markov decision process has finite sets of states , actions and rewards , and dynamics , the probability of next state and reward after action in state . A policy is a probability distribution over actions for each state. It induces a Markov chain on states with transition matrix , , and expected one-step reward . For a discount rate , the true value is , the expected discounted return.
A state distribution is stationary if ; write . The feature matrix is the matrix with rows . The mean square value error of a weight vector is
Linear semi-gradient TD(0) updates . In steady state its expected update involves
and the TD fixed point is . A real square matrix , not necessarily symmetric, is positive definite if for every . The key matrix is .
Under the hypotheses above, with every and linearly independent feature columns, is invertible, , and
Positive definiteness of is the reason on-policy linear TD(0) is stable: it makes the expected iteration contract toward the fixed point for small step sizes, and it guarantees that the fixed point exists and is unique. The error bound (9.14) quantifies the price of bootstrapping: the limit of TD can be worse than the best linear approximation, but by at most the factor . The same objects , and the key matrix reappear in LSTD, in the analysis of off-policy divergence (Chapter 11 of the book, where is no longer the stationary distribution of and positive definiteness fails), and in gradient-TD methods.
All results here are known. The book gives the positive definiteness argument in a box and cites (9.14) without proof. None of them has a machine-checked proof on the platform; the general Woodbury identity (FamousTheorems.woodbury_identity) is available, and (9.22) is its rank-one case written for the LSTD recursion. The mission produces a formal account of the finite-state theory of linear TD(0), with every hypothesis the book leaves implicit stated.
The key matrix is not symmetric, so the usual tools for symmetric positive definite matrices do not apply directly, and is positive definite only because of the specific interplay between and : if is replaced by a non-stationary distribution the claim is false (this is the off-policy counterexample of Chapter 11). The error bound (9.14) is not a consequence of positive definiteness alone. The TD fixed point is not the minimizer of , and has to be compared with the error of the -weighted projection of , which requires controlling in the -weighted norm. The book gives no argument for this step.
The Lean development lives in the namespace SuttonBartoRL.LinearTD. The MDP has four-argument dynamics with a finite reward set and one action set for all states; policies are stochastic. is defined from expected discounted returns as the series , never from a Bellman equation or from . and are defined as the book's steady-state expectations (9.11), as finite sums over , and ; the matrix form is a milestone, not a definition. Features are a matrix Matrix S (Fin d) ℝ with rows ; linear independence of its columns is LinearIndependent ℝ Xᵀ. Positive definiteness is a custom predicate , not Mathlib's Matrix.PosDef, which requires symmetry. The minimum in (9.14) is expressed by quantifying over every . The matrix inverse is Mathlib's, which is zero on singular matrices; the goal therefore asserts invertibility of explicitly.
Hypotheses the book leaves implicit and the statements make explicit: (the continuing case); a stationary distribution of the chain induced by with for every (otherwise the key matrix is only positive semidefinite); linearly independent feature columns (the book's "degenerate cases", p. 205). The box calls the off-diagonal entries of the key matrix "negative"; they are zero wherever , so the criterion is stated with nonpositive entries. The book's sentence that "ensures that is always invertible" (p. 229) is false in general, because the summands are not positive semidefinite: with , , , , one gets . It is not stated; (9.22) carries invertibility of and a nonzero denominator as hypotheses.
A statement in which is defined as the solution of the projected equation, or in which is assumed invertible or positive definite, would make the goal trivial or empty; neither is done. Convergence of the stochastic algorithm with probability one is not stated, since the book says it needs conditions and a step-size schedule it does not give. The bound for the episodic case and for other bootstrapping methods (p. 208) is stated only by reference in the book and is not a target.
Useful infrastructure: the -weighted inner product and orthogonal projection onto the column space of , the non-expansiveness of a stochastic matrix in the norm of its stationary distribution, and the positive definiteness criterion for non-symmetric matrices. All of these are reusable in the off-policy and average-reward chapters of the book. Contributions of these lemmas, and of alternative proofs of the milestones, are welcome.
The simplex method solves linear programs by moving between vertices of a feasible polyhedron. Its worst-case number of moves can grow exponentially, yet it often performs well on ordinary inputs. Worst-case examples alone therefore give an incomplete account of the method’s behavior. Spielman and Teng introduced smoothed analysis to measure expected performance after small random perturbations of an arbitrary input. Their result for a two-phase shadow-vertex simplex method gives a polynomial bound in the input dimensions and inverse perturbation scale. The pinned preprint is the source for every theorem number and constant in this mission.
The paper separates a geometric result about the expected size of a polytope’s shadow (Theorem 4.0.1) from the algorithmic result here (Theorem 5.0.1). That separation matters: a plane chosen before perturbation and a plane chosen by a running algorithm have different distributions. This mission addresses the latter. It complements the standard-form simplex theorems already formalized in the Introduction to Linear Optimization series and the worst-case Klee–Minty result in the Smale’s Ninth Problem mission; those results concern different algorithms or input models and are context rather than imported statements.
A linear program is specified by vectors , right-hand sides , and an objective vector :
The paper’s two-phase shadow-vertex method first draws a collection of -element subsets of and chooses one whose constraint matrix has the largest smallest singular value. It sets a power-of-two scale from the input norm and a power-of-two scale from that singular value. These determine positive relaxed right-hand sides : for and otherwise. A coefficient vector is chosen uniformly from . The first phase solves the relaxed program LP′ from the objective .
The second phase uses a lifted program LP⁺ in . For each original constraint it forms and , together with two artificial constraints at first coordinates and . LP⁺ connects LP′ to the original program and makes infeasibility detectable. Its shadow is taken in the plane of and .
For positive right-hand sides, an optimal polar simplex is a -subset of constraints whose scaled vectors form a facet of and whose unscaled cone contains an objective . The shadow for objectives is the union of these simplices over all in . Its size bounds the number of polar pivots. In Section 5 the paper writes for the first-phase shadow size and for the second-phase shadow size without the two artificial pivots.
The input is perturbed by independent Gaussians: each coordinate of and each has its prescribed center and common standard deviation , where . The algorithm has separate random choices of and .
The immediate targets bound the two phases: Lemma 5.2.1 gives an explicit expectation bound for and Lemma 5.3.1 gives one for . Lemma 5.1.1 and its corollaries control the chance that the chosen basis has a very small singular value. Corollary 4.3.3 extends the geometric shadow bound to positive, unequal right-hand sides and general Gaussian covariance. These are the mission’s milestone targets.
The goal is the shape of Theorem 5.0.1. With , there are a single polynomial and a positive constant such that, for all and all centers and objectives,
The polynomial is uniform over the dimensions and inputs; its coefficients are not prescribed. The bound on implies the corresponding result for the actual pivot count through the paper’s step-to-shadow comparison. The goal is stated with a positive center scale , the case in which the paper’s Gaussian rescaling applies.
The theorem places the number of pivots of a complete simplex method under one explicit perturbation model, including the work needed to find a starting feasible basis and handle an arbitrary right-hand side. The trivial binomial bound is retained because it controls rare events in the proof and is part of the stated result. The polynomial bound says that even when the unperturbed LP is adversarial, Gaussian noise of a controlled scale makes the expected shadow-size cost polynomial.
The paper proves the mathematical result. This mission asks for machine-checked proofs of its statement and the listed milestones; the draft Lean declarations are targets with sorry, not completed proofs. The reusable formal infrastructure is the finite polar simplex and shadow construction, product Gaussian input law, smallest-singular-value events for sampled minors, and the uniform truncated-simplex coefficient law. The two shadow-size lemmas also require explicit handling of measurable finite-valued counts and their expectations.
The basic shadow estimate fixes its projection plane before perturbing the constraints. In LP′, the initial objective uses a basis selected after the perturbation, so the relevant plane depends on the random LP. The fixed-plane theorem cannot be substituted directly. For LP⁺, the normalized lifted vectors are nonlinear functions of Gaussian data; they are generally not Gaussian vectors. Thus the same shadow estimate does not apply directly to their law either. A further issue is that a poor sampled basis can make very large. These are distinct obstacles, reflected in the milestone groups from Sections 5.1, 5.2, and 5.3.
Vectors are EuclideanSpace ℝ (Fin d), constraints are Fin n → EuclideanSpace ℝ (Fin d), and index families are finite sets of Fin n. The paper’s starts at one; Fin n starts at zero. The Gaussian constructor receives variance , not standard deviation . The draws are rounded upward and are independent uniform draws with replacement. Equal singular values are resolved by the first sampled set. The uniform law on is represented by normalized independent exponential weights followed by the affine shift that imposes .
The Lean definition of is exactly the Section 5 shadow-size upper bound , computed from the sampled LP data. It is not an arbitrary cost variable. The actual algorithmic step bound needs the paper’s polar algorithm and Lemma 3.3.5. The goal explicitly asks for inner and outer integrability so Lean’s default value for a nonintegrable Bochner integral cannot make the result vacuous. The source’s all-zero center scale is excluded because it gives zero perturbation and defeats the rescaling used in Theorem 5.0.1.
For LP⁺ the vectors live in , so the two LP⁺ milestone bounds use . The preprint prints in those calls even though the preceding extension theorem would be applied in dimension . Lemma 5.2.1 is written as an inequality: its printed equality is stronger than the bound established on page 71. These corrections are visible in the theorem titles and notes. Contributions that prove the exact statements, establish the measurability and Gaussian law facts, or formalize the step-to-shadow comparison are welcome.
Open networks of single-server queues with general interarrival and service distributions are the standard model of job shops, communication networks and service systems. Outside the product-form (Jackson) case their queue-length distributions are not known in closed form. When every station is close to saturation, a heavy-traffic limit replaces the network by a diffusion process. Martin I. Reiman's paper Open Queueing Networks in Heavy Traffic (Mathematics of Operations Research 9(3), 1984) proves such a limit for the vector of queue lengths of a general open network. The limit is a reflected Brownian motion on the nonnegative orthant. That process has since become the default diffusion approximation for open networks, and it is the starting point of later work on its stationary distribution and on control of networks in heavy traffic.
Timeline:
(These attributions follow Reiman's own account, pp. 441–442 of the 1984 paper.)
There are single-server stations and a nonempty set of stations that receive customers from outside. The primitives are mutually independent sequences of IID random variables: interarrival times (), service times , and routing indicators . When the th customer served at station finishes, it moves to station , or leaves if . The parameters are the service rates , the service-time variances , the arrival rates (with for ), and the interarrival variances . The routing matrix , , has spectral radius strictly less than one, so every customer eventually leaves.
Let be the number of exogenous arrivals to station by time , and the number of service completions at in units of busy time. Let , with . The queue length and the busy time are the unique solution of
A sequence of such networks, indexed by , shares , and . Its parameters converge to finite limits . With , the heavy-traffic condition is
Moments of order of the interarrival and service times are bounded uniformly in . The scaled queue length is , .
Let be a Brownian motion with drift and covariance matrix , where
Let be its reflection with reflection matrix . Then
The goal fixes no constants beyond the parameters' limits. It is stated for every network sequence satisfying (20)–(26).
The milestones follow the paper's proof, in order:
Theorem 1 justifies the diffusion approximation of a heavily loaded open network. Writing reduces questions about the network to questions about one reflected Brownian motion, whose data are explicit functions of the first two moments of the primitives and of the routing matrix. The same limit, with Lemma 2, gives the paper's Theorem 2 on sojourn times. It is the model case for the multiclass heavy-traffic theory that followed.
The result has been proved since 1984. No machine-checked version exists. The mission's contributions would be:
The obvious route applies a functional central limit theorem to directly. That fails because is not a sum of independent terms: each station serves only while its queue is nonempty, so the service process is evaluated at the random busy time , which depends on the whole network. The proof therefore has to separate the netput process, which obeys a central limit theorem, from the regulator . It then has to show that the random time change converges to the identity, i.e. that idleness vanishes on the diffusion scale. Weak convergence must also be transported through a reflection map that is defined on all of but is known to be continuous only at continuous paths.
The Lean development uses the following conventions:
Fin K, vectors are row vectors Fin K → ℝ, and a row vector times a matrix is Matrix.vecMul.Fin (K+1), with 0 meaning "leaves" and j.succ meaning station .iIndep of their σ-algebras), IID within each sequence, everywhere positive and square integrable.ℕ; (25)–(26) are imposed for , (22) and (26) over , and is the same for all .Added hypotheses, each implicit on the page:
No positivity hypothesis on the limits is added: (25) and (26) bound the means of the service and interarrival times, so the limits are positive.
The statement is not to be weakened. Ruled out are:
Each of these is a different theorem.
Useful contributions, all reusable beyond this mission:
A hotel sells rooms of several types, in limited numbers, to guests who each want one room. The revenue-optimal way to sell is known only in special cases: for buyers with several private values, optimal mechanisms can be randomized, involve lotteries, and lack a closed form (Manelli–Vincent 2007; Chawla, Hartline, Kleinberg 2007). In practice sellers post prices. The question is how much revenue posting prices gives up.
Chawla, Hartline, Malec and Sivan (arXiv:0907.2435v2, STOC 2010) answer it for a broad class of single- and multi-parameter problems. For unit-demand buyers of multiple copies of multiple items they show that a menu of posted prices, offered to the buyers in whatever order they arrive, earns at least of the revenue of any deterministic truthful mechanism (Theorem 14). This mission formalizes that result together with the two steps it is built from: a reduction from the multi-parameter problem to a single-parameter one with "copies" of each buyer (Lemma 3, Theorem 4), and an order-oblivious pricing for the intersection of two partition matroids (Theorem 13).
Single-parameter problem (BSMD). Finitely many agents have independent private values , each with a density on a bounded interval. A seller may serve any set in a downward-closed set system . A deterministic mechanism maps reported values to a served set and payments ; it is truthful if reporting the true value is a dominant strategy and no agent ends with negative utility. Its expected revenue is . For prices , agent desires service if , and is the class of maximal feasible sets of desiring agents. The order-oblivious revenue is
a lower bound on the revenue of posting the prices to the agents in an adversarial order.
Multi-parameter unit-demand problem (BMUMD). There are buyers and a finite set of services, partitioned into the groups of services targeted at buyer . Buyer has value for each , all values independent with , and the set system is unit-demand: for feasible . A mechanism is truthful if no buyer gains by misreporting its whole vector , and individually rational if a buyer receiving pays at most and a buyer receiving nothing pays .
Copies. The instance replaces each buyer by single-parameter agents, one per service with value , under the same .
Price menus. Given prices and an arrival order , the price-menu mechanism approaches the buyers in order; buyer is offered the services of that can still be feasibly allocated, at prices , and buys a utility-maximizing one if some has .
Multiple copies of items. With items and copies of item , services are pairs and a set of services is feasible if it gives each buyer at most one item and uses at most copies of : the intersection of two partition matroids.
For regular distributions there are prices such that, for every arrival order , the price-menu mechanism is truthful and
for every individually rational, truthful deterministic mechanism .
The result shows that for unit-demand buyers, a seller loses at most a constant factor by replacing the optimal, possibly opaque, truthful mechanism with a menu of prices that does not depend on the order in which buyers arrive. The reduction of Theorem 4 is generic: any order-oblivious pricing for the single-parameter instance with copies, under any unit-demand constraint, transfers to the multi-parameter instance with the same factor. Theorem 13 supplies one such pricing for the intersection of two partition matroids, which is exactly the shape of the multi-unit, multi-item constraint.
All results here are proved in the paper and none is formalized elsewhere; the platform has Myerson's single-unit optimal auction and weak monotonicity in an abstract quasilinear model (Börgers), but no posted-price approximation, no copies reduction, and no order-oblivious revenue. The formal development adds a machine-checked account of the reduction (in particular that the price-menu mechanism is truthful and allocates a maximal feasible set for every order), a precise version of the probabilistic claim behind the constant , and reusable definitions of order-oblivious revenue and of multi-parameter truthfulness with the paper's individual rationality.
Lemma 3 needs more than the observation that the copies instance has more competition: one must build a truthful single-parameter mechanism with at least the same revenue. The allocation is copied, but the payments must be threshold payments of the copies mechanism, and showing they dominate the original payments uses both weak monotonicity and the paper's individual rationality, through the taxation principle.
Theorem 13 compares order-oblivious revenue with Myerson's revenue through the bound of Lemma 2, at prices built from Myerson's service probabilities scaled by . The step that is easy to get wrong is the probability that an agent is considered: the events "part is not full" and "part is not full" depend on overlapping agents, so the product bound does not follow from Markov's inequality alone; it holds because both events are decreasing in the set of desiring agents (Harris' inequality). The comparison must also be uniform: one set of prices must serve against every truthful mechanism, which requires an optimal mechanism to exist.
Needed infrastructure, reusable beyond this mission: Myerson's characterization of truthful single-parameter mechanisms and the revenue–virtual-surplus identity for densities on intervals, Harris' inequality for product measures, and the taxation principle for deterministic multi-parameter mechanisms. Contributions on any of these are welcome.
Many statistical procedures minimize an average observed loss. This treats two candidates with the same average as equally attractive even when one has much more variable losses across the sample. Adding a multiple of the empirical standard deviation can distinguish them, but the resulting objective need not be convex even when each individual loss is convex. Duchi and Namkoong study a distributionally robust alternative: they maximize expected loss over a small neighborhood of the empirical distribution, then minimize that worst-case value. Their paper identifies when this convex robust value agrees exactly with the mean-plus-standard-deviation expression and how far apart the two can be otherwise. The finite-sample statement is Theorem 1 of the pinned preprint.
The relation matters to someone choosing a loss function for stochastic optimization. The variance expression has a direct statistical interpretation, while the robust expression preserves convexity in a decision parameter when the loss is convex. Theorem 1 makes the relationship quantitative for a single bounded random variable, before the paper turns to uniform guarantees over whole classes of losses. This mission isolates that first step and its finite optimization model.
Take observed real values , with . Their empirical mean and empirical variance are
The variance uses , not the unbiased-estimator factor . A weight vector is feasible when its entries are nonnegative, sum to one, and satisfy
This is the paper's χ² neighborhood of the uniform empirical weights. Its robust sample expectation is
For a random variable with law supported on , write and . An independent sample supplies the vector . The paper describes through a -divergence from the empirical distribution, with ; its finite maximization problem (8) is the weight-vector form used here. The preprint, pp. 2 and 5–7 fixes these conventions.
For every sample in , the robust value lies between the empirical mean plus a corrected variance penalty and the full penalty:
This is inequality (10). The correction is explicit, so this target records more than an asymptotic approximation.
When and the sample size obeys
the goal is the high-probability equality
This is Theorem 1's equality (11) with the missing -dependent sample-size requirement supplied from the proof. The exact expansion is the mission goal; display (30), inequality (10), and Lemma A.2 form the milestone list, and the exact value under condition (9) is a further statement of the mission.
The deterministic result states how large the discrepancy between a convex robust risk and a variance penalty can be for any bounded sample. The equality says that, with the stated confidence, no discrepancy remains once the population variance and sample size make the penalty compatible with nonnegative probability weights. These are the numerical facts later sections need when they move from one loss variable to families of losses and minimizers. The claims and constants come from Theorem 1 and Section 2.1.
The paper develops arguments for these results, although its printed (11) needs the correction described below; the statements in this mission have no machine-checked proofs yet. The formalization work includes the finite χ² feasible set, its real supremum, exact handling of tied observations, empirical moments with the paper's normalization, and a product-law event for the probability estimate. The Samson concentration milestone is reusable for other bounded independent-coordinate models. Solvers can also contribute a different route to the corrected exact expansion; the goal concerns the statement, not one chosen argument.
Without the nonnegativity requirement on , optimizing a linear function over the centered Euclidean ball gives the mean plus a standard-deviation term. The candidate weights can become negative when a sample coordinate is far below the mean, so that calculation alone cannot certify the robust value. Condition (9) records precisely when the candidate is feasible. The probability target then needs a quantitative guarantee that the sample variance is large enough often enough, with the stated exponential constant. A pointwise inequality for a fixed sample does not by itself yield that probability estimate. These are separate obligations in Section 2.1 and Appendix A.
The sample is a function Fin n → ℝ; feasible weights have the same type. chiSqBall, robustSup, empMean, and empVar mirror equations (8) and the definitions on p. 6. Every theorem assumes and , so the weight ball is nonempty and its real supremum is bounded. The high-probability theorem uses a probability measure on the reals, supported on , and the independent product measure on Fin n → ℝ. Its conclusion bounds the measure of the event on which equality fails. The positive population variance hypothesis makes division by and meaningful. The deterministic bounds include every sample in the interval and use .
The paper prints the threshold without in (11), but its Appendix A invokes the corresponding inequality, and the printed claim fails for sufficiently large . The goal includes that term. The paper's route through Lemmas A.1 and A.4 contains misprinted lower-tail and moment claims, so those are not milestones. Lemma A.3's displayed (31b) is also omitted because its correction term has the wrong scaling; the corrected goal stands as a target to establish independently. These discrepancies are detailed in the local moderation notes and the pinned source, pp. 7 and 32–35.
No hypothesis may force the bad event to be empty, and the robust value must optimize over all feasible weights, not a selected optimizer. The supporting definitions are intended for reuse in later missions on uniform variance expansions. Contributions to the finite optimization facts, the concentration statement, and the probability goal are welcome.
Most physical supply chains hold stock at several levels: a factory warehouse feeds a regional depot, which feeds a retail outlet. Each level orders from the one above it, and a shortage upstream delays replenishment downstream. Optimizing such a multi-echelon system by dynamic programming looks hopeless, because the state is a vector of stock levels and stock in transit at every installation, and the value function of a two-installation system with a two-period shipping lag already depends on three continuous variables.
Andrew J. Clark and Herbert Scarf (Management Science 6(4):475–490, 1960) showed that for a serial system this curse of dimensionality disappears. Working with echelon stock (the stock at a level plus everything below it or in transit to a lower level), the optimal system cost separates into the cost of the lowest installation, optimized as if it stood alone, plus a function of echelon stock only. The result is the foundation of multi-echelon inventory theory: the echelon base-stock policies used in practice, the stationary analyses of Federgruen and Zipkin (1984) and Chen and Zheng (1994), and textbook treatments (Zipkin, Foundations of Inventory Management, 2000; Snyder and Shen, Fundamentals of Supply Chain Theory) all descend from it.
Timeline. Arrow, Harris and Marschak (1951) and Arrow, Karlin and Scarf (1958) set up periodic-review inventory models with discounted costs. Karlin and Scarf (1958) treated a single installation with a delivery lag, reducing it to a problem without lag (the paper's facts 1–3). Clark and Scarf (1960) proved the decomposition for serial systems with linear shipping costs and a setup cost permitted only at the top. Federgruen and Zipkin (1984) extended it to infinite horizons and Chen and Zheng (1994) gave a lower-bound proof that reaches more general structures.
Two installations are in series. Customer demand occurs only at installation 1; its demand in each period is non-negative with density on , independent across periods, and excess demand is backlogged. Installation 2 ships to installation 1 with a two-period lead time at unit cost . The system orders units from outside at cost for and (eq. (5)); these arrive at installation 2 one period later. Costs periods ahead are discounted by , .
The state at the start of a period is : is the stock on hand at installation 1, the stock that reaches installation 1 next period, and the echelon-2 stock (on hand at both installations plus in transit), so . Installation 1 pays the expected holding and shortage cost (1),
and echelon 2 pays a natural one-period cost (Assumption 3).
With periods remaining, the optimal system cost satisfies, with ,
where is installation 1's target (stock on hand plus in transit after shipping). Installation 1 in isolation, buying at unit cost with a two-period lag, has optimal cost , :
In Lean these are ClarkScarf.Serial.Model.sysCost and isoCost; the expressions in braces are sysObj and isoObj, indexed by for the problem with periods remaining.
There are functions with such that, for all and ,
and installation 1 acts optimally by aiming at an isolated-optimal target and taking , as much as installation 2 can supply. The goal fixes no form for and needs no critical numbers.
The result. Theorem 1 replaces one three-dimensional dynamic program by two one-dimensional ones. Installation 1 solves its own problem (15), whose solution is a critical-number policy, and echelon 2 solves a single-installation problem in with one-period cost . When is convex the augmented cost is convex (the paper remarks this for Expression (10)), so the echelon-2 policy is of type by Scarf's theorem, and the whole system runs on echelon base-stock rules. Every later serial-system result, finite or infinite horizon, uses this decomposition or its proof idea, and the "induced penalty" is the prototype of the penalty functions used in the multi-echelon literature.
Formalizing it. The theorem is classical and proved, but no machine-checked version exists. The published platform items on Clark–Scarf are a stationary single-period decomposition with normal demand and a disproved infinite-horizon base-stock recursion, neither of which is this finite-horizon dynamic program. A formal development produces the value functions (14)–(15) with real infima and set integrals, the measurability and integrability of value functions defined by infima, the convexity propagation through the recursion (7), and the decomposition itself, which are reusable for any finite-horizon inventory recursion with lead times.
The obvious induction on substitutes (16) into (14) and separates the minimizations over and . The separation is immediate; the hard step is that the constrained minimum over differs from the unconstrained one by an amount that a priori depends on . Showing that it depends on alone is the content of Theorem 1; nothing in the separation step itself rules out a dependence on . On the measure-theoretic side, every value function is defined by an infimum over an uncountable set and then integrated against . Its measurability and integrability are not automatic, and they must be established before any identity between integrals can be manipulated.
Everything lives in ClarkScarf.Serial, one definition file Def_ClarkScarf_Serial_Model and seven theorem files. Conventions committed to:
structure Model whose fields carry the data and the standing hypotheses: ; with ; and two additions the page leaves implicit, disclosed in each statement: a finite demand mean (otherwise (1) is infinite for ) and non-negative, continuous and of at most linear growth (Assumption 3 leaves unspecified; these make every expectation in (14) finite and measurable). No discount bound , no convexity of , no and no sign condition on is assumed.A formalization in which the feasible set of (14) is empty, in which the expectations are junk zeros of non-integrable integrands, or in which may depend on would make (16) trivial; the domain restriction, the integrability conditions and the order rule these out. A sorry-free check (not part of the mission) verifies and and exhibits a model with exponential demand satisfying all hypotheses.
Needed infrastructure: Fubini-type rearrangement of iterated set integrals against a density, integrability of functions of linear growth against a finite-mean density, convexity preserved under infimal projection and under convolution with a density, and measurability of infimum-defined functions. Contributions of these general lemmas, of the base cases , and of any milestone are welcome.
Routing and network optimization often require the length of the best route between every ordered pair of points. Robert W. Floyd's Algorithm 97 gives a compact procedure for this task: it receives a matrix of direct-link lengths and changes the matrix in place until each entry is meant to represent a shortest-path length. The procedure is a small historical source for an algorithm now used as a standard all-pairs shortest-path routine. Its published text consists of the ALGOL code and a short explanatory comment, without a correctness proof.
The same page contains Floyd's Algorithm 96, a Boolean procedure for ancestor relations. Its output records whether a chain of parent links connects two individuals. Floyd cites Warshall's theorem on Boolean matrices in both comments. The Boolean procedure and the length procedure use the same order of three loops; together they expose the distinction between discovering that a route exists and determining its best length. This mission formalizes both claims from Floyd's published page, with the shortest-path statement as its goal.
A directed network has numbered points. Its length matrix assigns a real number to a direct link from to . The value means that the direct link is absent. Links may have negative lengths, and the initial diagonal entries are unrestricted. The paper's matrix index range is ; the Lean development uses in the same order.
A path from to is a sequence with links. The points are distinct, as are . Thus a path between different points has no repeated point, while a path from a point to itself is a simple closed path with at least one link. Its length is ; a missing link gives length . Write for the minimum length among these paths, taking when there is no finite-length path. Since , this is a minimum over a finite family.
The no-negative-cycle condition says that every closed path has nonnegative length. Individual links can still be negative. This condition matters because, in a network with a negative cycle, repeated travel around that cycle can keep reducing a walk's length. Floyd's comment does not state the condition, although the claimed output needs it.
Algorithm 97 scans a pivot , then row , then column , each in increasing order. It enters the column scan when the current is finite; if the current is also finite, it computes and replaces when . Every replacement affects subsequent reads of the same matrix. Algorithm 96 makes the corresponding Boolean update: when and are true, it sets to true.
For Algorithm 96, let be the transitive closure of the initial parent relation , using chains of one or more links. Its comment asserts
For Algorithm 97, the separate unreachable-pair sentence asserts that, whenever no finite-length path runs from to ,
This second target needs no condition on cycle lengths. Both statements are milestones because they are claims printed in the two algorithm comments, rather than lemmas invented for the formalization.
The goal is the whole output claim of Algorithm 97. For every , every matrix with no negative cycle, and all points ,
The equality includes paths with negative individual links, diagonal entries, and unreachable pairs. It fixes the entire final matrix, rather than only an upper or lower bound.
The goal connects an explicit in-place matrix program with a route-based definition of shortest length. Once established, it permits later formal developments to use the procedure as a justified all-pairs distance computation, including networks whose individual links have negative lengths. The Boolean milestone similarly identifies the final state of an ancestor procedure with the transitive closure of the initial relation. Neither assertion requires treating an implementation's output as the definition of the mathematical answer.
Floyd's 1962 paper states these outcomes but supplies no proof. This mission supplies precise Lean statements and definitions for a proof to target. A completed machine-checked development would establish the published procedure's correctness under the missing necessary premise. The statements in this proposal are currently open theorem targets; compiling their declarations checks syntax and types, not their proofs. Supporting work on finite paths, cycle decompositions, and matrix updates can be reused in other finite directed-network arguments.
The array is changed in place. During a pivot's sweep, an entry used in a later update may already differ from its value at the start of that pivot. The test on is evaluated before the column loop, but the same entry is read again within every column iteration. A proof based only on a simultaneous, out-of-place matrix recurrence does not directly describe these reads. Negative individual links also prevent arguments that rely on every update decreasing only through a nonnegative segment. The no-negative-cycle condition must control what happens when a proposed route returns to a point already visited.
Points are Fin n, including the empty network at and the single-point network at . Lengths are WithTop ℝ, where ⊤ represents the paper's ₁₀10 sentinel as mathematical infinity. The paper's literal sentinel is ; a finite bound cannot represent arbitrarily long paths, so this mission uses infinity in its goal. The ALGOL real operations are represented by exact real arithmetic. The printed procedure's loop order, strict comparison, two finiteness guards, and immediate assignments are part of the Lean definition.
The initial diagonal is not normalized. Therefore a path from to itself has at least one link, and the final diagonal denotes a shortest closed-path length when one exists. The Boolean comment's “is true if” is read as an equivalence, supported by its following explanation of the final matrix; chains have one or more links, matching Lean's Relation.TransGen.
The sole added hypothesis in the main goal is absence of negative cycles. It is necessary: with one point and self-link length , the procedure changes that entry to , although the shortest simple closed path has length . No nonnegative-link or zero-diagonal premise is imposed. The unreachable-pair milestone omits the cycle hypothesis because its claim holds without it. The benchmark is a finite minimum of summed link lengths, defined independently of Algorithm 97; defining it from the procedure or its recurrence would empty the goal of its intended content. Contributions proving the printed algorithms' statements, or establishing reusable finite-path and update results needed for them, fit this scope.
Long-running projects such as construction, plant engineering or software development involve payments to and from the contractor at many points in time: disbursements when activities are carried out, progress payments when milestones are reached. When the planning horizon is long, money received later is worth less, and the natural financial objective is the net present value of all cash flows. Scheduling a project to maximize its net present value subject to minimum and maximum time lags was studied by Russell (1970) and Grinold (1972), and the problem is the prototype of a nonregular objective: delaying an activity can be profitable, because disbursements lose value when they are postponed.
This mission follows Chapter 3 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003). The book shows that the net present value objective belongs to the class of binary-monotone objective functions (§3.3.5), and it uses this in §3.9.1 to give a combinatorial optimality criterion for the resource-free problem: a vertex schedule is optimal exactly when the subprojects cut off by the arcs of a spanning tree have net present values of the right sign (Proposition 3.9.2). That criterion drives the book's parametric analysis of the net present value as a function of the discount rate and the deadline.
A project consists of activities , , where is the project beginning and the project completion. Activity has an integer duration , with and otherwise. Temporal constraints are the arcs of a project network : an arc with integer weight requires for the start times . A maximum project duration is the arc with weight . The time-feasible region is
Let be the discount rate ( for an interest rate ) and the cash flow of activity , paid at its completion time . The problem (3.9.1) is
and a minimizer is a time-optimal schedule. A vertex of is an extreme point. A spanning tree is associated with if , has arcs and a connected underlying undirected graph, and is the unique solution of , for . Deleting a tree arc splits into two subtrees; is the node set of the one not containing . The arc is forward if the tree path from passes it from to and backward otherwise, and
is the net present value of the subproject . Finally, is binary-monotone if it is monotone on every line with direction (Definition 3.3.2).
Assume every node is reached from by a path of nonnegative length (the standing convention of §1.2) and let be a vertex of .
The book states "if and only if … for each arc of the corresponding spanning tree", where the corresponding tree is chosen using optimality. The two directions above are the reading that makes the statement well defined: sufficiency for every associated tree, necessity for some associated tree.
Proposition 3.9.2 turns a nonconvex continuous optimization problem into a finite check on a spanning tree. Read as an economic statement, it says that at an optimal schedule no subproject with positive net present value can be started earlier and no subproject with negative net present value can be postponed. The book builds on it the parametric procedure of §3.9.1, which tracks the optimal tree as the discount rate or the deadline varies (Propositions 3.9.3 and 3.9.4), and the steepest descent method of §3.5.2 terminates exactly when the criterion holds.
The results are proved in the book, partly by reference to network optimization (Ahuja et al., 1993) and to Schwindt and Zimmermann (2001, 2002). None of them is formalized on the platform or, as far as is known, anywhere else. A formal proof would give the first machine-checked optimality certificate for a nonregular project scheduling objective, and the spanning-tree description of vertices (Proposition 3.2.16) is shared with Mission VI of this series.
The objective is neither convex nor concave when cash flows of both signs occur, so local optimality at a vertex does not imply global optimality by a convexity argument, and a first-order check along the edges of is not obviously enough. The criterion is also not a statement about one tree: a degenerate vertex, where more than temporal constraints are binding, has several associated trees, and the sign conditions may hold on some and fail on others. Necessity therefore requires producing a suitable tree, not checking a given one. Finally, the combinatorial objects (the subtree , forward and backward orientation relative to the root) have to be connected to the geometry of through Proposition 3.2.16, whose proof in the book is a citation.
Activities are Fin (n + 2) with 0 the project beginning and Fin.last (n+1) the project completion; start times are real; durations are natural numbers and arc weights integers. The deadline is a structure field together with the backward arc of weight . is Real.rpow, and every statement assumes as the book does (p. 203). Vertices are Set.extremePoints ℝ. A spanning tree is a Finset of arcs whose SimpleGraph.fromRel is connected; is the set of nodes not reachable from once the arc is deleted.
Three readings are committed and disclosed in the item statements. Necessity is stated only for : at the objective is constant, every schedule is optimal, and the sign conditions can fail on every tree. The standing convention of §1.2 (a path of nonnegative length from to every node) is a hypothesis of Proposition 3.2.16 and of the goal; without it a vertex can be fixed by rather than by arcs of , and necessity fails. The existence of an optimal vertex assumes nonempty and bounded, which the book asserts in §3.1. Chapter 3's resource constraints do not occur in this mission, which concerns only.
The goal cannot be discharged by choosing the tree freely: associated trees must consist of arcs of that are binding at and determine uniquely, and sufficiency must hold for every such tree. Contributions welcome beyond the milestones: a proof of Proposition 3.2.16 reusable by Mission VI, and a general lemma relating binding spanning trees of difference constraints to extreme points.
Semidefinite programs (SDPs) arise as convex relaxations of combinatorial problems such as maximum cut and the Lovász theta function, and in control and eigenvalue optimization. Interior-point methods solve them reliably but manipulate dense matrices, which limits the size of the instances they can handle. Burer and Monteiro (Math. Program. 95 (2003)) proposed replacing the matrix variable by a factorization with having only columns, and solving the resulting nonconvex program by a first-order augmented Lagrangian method. The approach rests on a theorem of Barvinok (1995) and Pataki (1998): an SDP with linear constraints has an optimal solution of rank with , so a small number of columns suffices.
Because the factorized problem is nonconvex, a local minimum it returns is not automatically a solution of the SDP. Section 2 of the paper gives conditions under which it is. This mission formalizes those conditions, culminating in Proposition 2.5, which justifies the paper's strategy of increasing the rank one column at a time.
For real matrices, the trace inner product is . The data are symmetric matrices and a vector . The primal SDP and dual SDP are
The standing assumptions of the paper are that are linearly independent and that there are feasible and with .
For a positive integer , the low-rank program is
Its Lagrangian is , and . A feasible is a local minimum if it minimizes the objective among nearby feasible points; it is a regular point if are linearly independent; it is a stationary point with multiplier if . The injection of is , obtained by appending a zero column.
Let and let be a regular local minimum of with multiplier , , . If is a local minimum of , then
Proposition 2.5 is a certificate of global optimality for a nonconvex problem obtained from local information alone. It is the basis of the rank-increase scheme described on p. 8 of the paper: compute a local minimum of for a small ; if the zero-column extension is still a local minimum of , the current point solves the SDP; otherwise a better point of exists and is increased. Proposition 2.4 gives the companion test, valid for every : positive semidefiniteness of the multiplier matrix at a stationary point. These statements underlie the later convergence analysis of the method (Burer & Monteiro 2005) and the literature on benign landscapes of low-rank SDP formulations (Boumal, Voroninski & Bandeira 2016).
The results are proved in the paper. What this mission adds is a machine-checked version of the full chain from the standard-form SDP to the rank-increase certificate, including the matrix calculus (9), the first- and second-order necessary conditions for an equality-constrained program over rectangular matrices, and SDP complementary slackness in standard form. No machine-checked proof of these results is recorded in Mathlib or on the platform.
The SDP side (Propositions 2.1 and 2.4) is linear algebra: weak duality and the fact that the trace inner product of two positive semidefinite matrices is nonnegative. The substance lies in Proposition 2.3. The feasible set of is a variety cut out by quadratic equations, and the multiplier rule and, especially, the second-order necessary condition require a constraint qualification and a curve in the feasible set realizing every tangent direction. Mathlib provides a first-order Lagrange multiplier rule, but not the second-order condition on the tangent space. A naive attempt to read Proposition 2.5 off Proposition 2.4 fails: local minimality of alone does not make positive semidefinite (when is below the minimal optimal rank, it is not); the hypothesis on is indispensable.
Matrices are Matrix (Fin n) (Fin r) ℝ with 0-based indices. The trace inner product is frob A B = trace(Aᵀ * B), defined for rectangular matrices. The data carry explicit symmetry hypotheses C.IsSymm and (A i).IsSymm; without them the formulas (9) are false. Primal feasibility uses Mathlib's PosSemidef, which over includes symmetry. Optimality for (1) and (3) is defined relative to their entire feasible sets. The standing assumptions are a separate predicate carried as a hypothesis by Propositions 2.1, 2.3, 2.4 and 2.5, and every statement about carries and (or ). Gradients are Fréchet derivatives under the Frobenius norm, identified with matrices through the trace inner product; local minima use IsLocalMinOn on the feasible set of together with feasibility. The injection appends the zero column as the last column.
The statement admits several trivializing encodings, all excluded here: optimality defined relative to the factorized feasible set instead of the whole SDP, an empty or unconstrained (an unconstrained local minimum or a local minimum without feasibility), a stationarity notion that already includes , and an injection other than the zero-column extension.
A complete development needs the matrix calculus of , a second-order necessary optimality condition under linear independence of the constraint gradients, and standard-form SDP weak duality and complementary slackness; all of these are reusable well beyond this mission. Proofs of individual milestones, in particular the derivative formulas and Proposition 2.4, are welcome independently of the goal.