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.
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?
Retailers of seasonal goods (fashion, electronics, holiday items) sell a fixed stock over a short season and routinely cut prices toward its end. A markdown of this kind segments the market over time: customers with high valuations buy early at a premium price, and customers with lower valuations are served later at a discount price. Aviv and Pazgal (MSOM 2008) study how much such two-price schemes are worth when customers arrive over time, differ in their valuations, and may or may not anticipate the discount.
To measure the value of price segmentation, the paper compares every two-price scheme with the best fixed-price policy, a single price held for the whole season. Its benchmark is the case of myopic customers, who never delay a purchase strategically. Proposition 3 of the paper computes this benchmark in closed form in the simplest nontrivial setting: exponentially distributed valuations that do not decline over the season, and unlimited inventory. The resulting formula explains the pattern of the paper's Table 1, where the benefit of segmentation grows with the heterogeneity of valuations and with a late discount time.
A seller offers a product during the season ; throughout this mission , so time is measured as a fraction of the season. Customers arrive as a Poisson process with rate . Customer has a base valuation drawn independently from a distribution with tail , and values the product at at time , where is the decline factor. The paper reparametrizes it as , the fraction of the base valuation left at the end of the season.
In the numerical study, is a Gamma law with mean and coefficient of variation (standard deviation over mean): shape and rate . The paper sets . For this is the exponential law with mean one, for .
A contingent two-price policy posts the premium price on , where is fixed, and a discount price from time on. A myopic customer arriving at buys at if his valuation is at least ; otherwise he waits and buys at if his valuation is then at least . Customers arriving at or after buy if their valuation is at least . The numbers of customers in these groups are Poisson with means
With unlimited inventory, the expected revenue of the policy is
and the expected revenue of a single price is (Eq. (9) of the paper). The optimal values are and .
Suppose , and (unlimited inventory), with and . Then
Both maxima are attained. The goal states the two optimal values; it does not fix the optimal prices.
Proposition 3 gives the relative benefit of contingent pricing over a single price, , as a function of the discount time alone. It increases in and is largest at , where it equals . This is the paper's analytic anchor for its numerical findings: segmentation is most valuable when valuations are heterogeneous and customers are carried to the discount at little cost, and a late discount exposes more customers to the premium price. Under strategic customers the same quantity serves as an upper bound on the benefit of segmentation (§6.1 of the paper).
The result is proved in the paper, in a short appendix argument that states the reduced problem and its solution without the calculus. No machine-checked version exists. Formalizing it produces a reusable Lean encoding of the paper's segment rates as integrals of a valuation tail, a Gamma valuation law through Mathlib's gammaMeasure, and a complete verification that the integral model reduces to the two-variable problem and that the stated prices are its unique maximizer.
The obvious route is to write the revenue in closed form and set the gradient to zero. Two steps of that route are not automatic. First, the reduction requires evaluating the three integrals with the piecewise tail of the exponential law, including the inside , and the reduced formula is valid only for nonnegative prices; negative prices must be handled separately in the model itself, where the tail equals one. Second, the reduced objective is not concave on the region , so a stationary point is not automatically a global maximizer, and the boundary and unbounded directions have to be ruled out. Uniqueness of the maximizer, which the paper asserts, fails at and needs .
All declarations sit in the namespace SeasonalPricing.MyopicExp. Time, prices and rates are real numbers. The season is with and . Integrals are interval integrals. The valuation tail is gammaValuationTail μ c x = 1 - cdf (gammaMeasure (1/c^2) (1/(μ c^2))) x, used at . The hypothesis is decayRatio α 1 = 1 with .
Readings of the paper's informal words:
IsGreatest), not a supremum.The Gamma density printed on p. 349 has the exponent , a misprint for ; at the exponent is either way.
A trivializing formalization would state the goal on the reduced two-variable function, dropping the model: the goal here is about built from and the Gamma tail, and about built from Eq. (9). The platform's BuyingToBundle.monopolyRevenue (definition monopoly_pricing) is a related object, ; with and , equals times it for the exponential law, but it is a supremum without arrivals or time and is not reused.
Contributions welcome: closed forms of the segment rates for the exponential tail, a general lemma that negative prices are dominated, and the two-variable maximization.
Retailers of fashion and seasonal goods sell at a premium price early in the season and mark the remaining stock down later. When customers anticipate the markdown, some of them who would buy at the premium price instead wait, trading a lower price against the risk that the item sells out and against the decline of their own valuation over the season. How forward-looking ("strategic") customers respond to a markdown policy is the first question any model of such pricing has to answer, because the seller's optimal prices depend on it.
Aviv and Pazgal (MSOM 2008) model a seller with a fixed inventory, Poisson arrivals of customers with heterogeneous, exponentially declining valuations, and two pricing regimes: contingent pricing, where the discount depends on the inventory left at the markdown time, and announced fixed discounts. The first step of their analysis of contingent pricing is Theorem 1: whatever the other customers do, a customer's best response is a threshold rule on his current valuation, with a threshold that rises as the markdown approaches. Their numerical study of equilibria and of the value of price commitment (§§4.2–7) is built on this reduction.
A seller holds units over a season split at a fixed time with . On the premium price applies. At time the seller observes the remaining inventory and charges the discount menu price , where for . Customer has a base valuation and valuation at time , with a common decline factor .
A customer arriving at either buys immediately at or waits until , when he requests a unit if the discounted price leaves him a nonnegative surplus. Waiting is uncertain in two ways: the remaining inventory is random, and when fewer units remain than customers request them, units are rationed at random. A belief is a probability mass function of on together with allocation probabilities , , where is the event that the customer is allocated a unit. It is determined by the other customers' strategies, which are arbitrary.
With , the expected surplus of waiting of a customer with current valuation is
The paper's purchase rule (p. 344): buy immediately iff the current surplus is nonnegative and at least .
Assume , and or . For every the equation
has a unique solution ; a customer arriving at buys immediately under the purchase rule if and only if ; and the threshold function is nondecreasing in .
Theorem 1 reduces a customer's strategy, a function of arrival time and valuation, to one threshold function on . The segment sizes of §4.2, the seller's menu problem (3), the equilibrium iteration (4) and the closed form of Proposition 2 are all written in terms of ; without Theorem 1 none of them is defined. Corollary 1, that the threshold rises toward the markdown, is what the paper calls "useful in our analyses below"; the customer segments of Figure 1 are drawn with it.
The result is proved in the paper, with a short appendix argument. No machine-checked version exists. The mission produces a formal statement and proof of the reduction for an arbitrary belief, which fixes the exact hypotheses under which it holds: the paper's slope bound needs either valuation decline () or imperfect availability, and the monotonicity of the threshold needs a nonnegative premium price. A formal and threshold are the starting point for formalizing the equilibrium and pricing results of the paper.
The mathematics is one-dimensional. The difficulty is in stating it exactly. is piecewise linear with a kink wherever crosses a menu price, so the paper's derivative is only a one-sided derivative, and the uniqueness argument has to use increments. The paper's bound "slope " is false when and a unit is allocated with certainty; then (2) has either no finite solution or a half-line of them. The threshold's monotonicity in rests on increasing in for fixed , which needs ; with a negative premium price the threshold can decrease. The naive reading of "optimal to use a threshold" as an abstract fixed-point fact about any monotone function with slope below one discards the model and is not the goal.
Lean namespace SeasonalPricing.Contingent. Time, prices and valuations are real numbers. The belief is a pair pmf alloc : ℕ → ℝ restricted to {0, …, Q} (IsInventoryBelief), not a random variable on a probability space; only the law of enters (2). The menu is p2 : ℕ → ℝ with required on only; never matters because . The belief does not depend on the arrival time, as in Eq. (4) of the paper. waitingSurplus is with written Real.exp (-(α * (T - t))); buysNow is the purchase rule, stated on the current valuation .
Readings of the paper's words:
∃!). The paper's "" includes only in the case excluded by the added hypothesis.MonotoneOn), since is constant on an initial interval whenever no menu price is reachable (p. 347).Added hypotheses, both named in the statements: or , the one hypothesis the paper's proof uses without stating it; and , the model's convention that prices are nonnegative. Only the branch of the threshold is stated: for the paper's is the model's rule for late customers. The belief enters through the explicit sum; a formalization with an unspecified monotone , or with defined by choice inside a definition, is not the target.
No new library is needed beyond finite sums, max and Real.exp. A lemma on unique roots of for with increments bounded by , , is reusable. Proofs of the milestones and the goal, in any order, are welcome.
In a two-person zero-sum game with objective randomization, whatever one player gains the other loses: the value of the game is the most player 1 can guarantee and the least player 2 can hold him to, and no arrangement between the players can give player 1 more than and player 2 more than at the same time. Aumann's 1974 paper (doi:10.1016/0304-4068(74)90037-8) replaces objective coin flips by ordinary events of the world, about which players may hold different subjective probabilities and may be differently informed. Sect. 6 of the paper shows that this breaks the zero-sum logic: once the players disagree about the probability of events they can observe, a zero-sum game becomes, in expectation as each player computes it, a game in which both can gain.
The phenomenon is the game-theoretic form of betting between people who disagree: two players with different beliefs can each expect to profit from the same wager. Aumann's proposition identifies exactly what information structure makes such an agreement possible inside a given zero-sum game, and shows by an example that informing only one player of a subjective event is not enough. The same paper introduced correlated equilibrium; the companion mission of this series formalizes its two-person result on subjective mixed equilibria (Proposition 5.1).
A game has a finite set of players, a finite set of pure strategies for each player, a finite set of outcomes and an outcome function from onto . Player has a utility ; write for .
A randomizing structure consists of a set of states of the world with a -field of events, a sub--field for each player (the events regarding which is informed), and a probability measure on for each player (the subjective probability of ). A strategy of is a map whose level sets lie in . For a profile of strategies, player 's payoff is computed under his own beliefs:
An event is objective if all coincide, and subjective otherwise. It is -secret if and every other player regards as independent of every event in the -field generated by the , . It is public if it lies in every . A measure is non-atomic on a -field if every event of of positive measure contains an event of of strictly smaller positive measure; a roulette is a sub--field of on which every is non-atomic, and a public roulette is a roulette of public events. Throughout, Assumption II holds: every player has a -field of -secret events on which every is non-atomic.
The game is two-person zero-sum if and for all . Its value is player 1's payoff at a Nash equilibrium of the classical mixed extension; by the minimax theorem all such equilibria give the payoff pair .
Let be a two-person zero-sum game with value , and assume
Then there is a pair of strategies with
The pair is not an equilibrium: it is an agreement that each player, by his own beliefs, strictly prefers to playing the game.
a special case of the goal in which the players share both the subjective event and the correlating device.
The proposition shows that the value of a zero-sum game is a property of objective randomization, not of the game alone. With subjective randomization available to both players, the conflict of a zero-sum game can be resolved by agreement, so the classical prediction (each player receives his security level) is not robust to disagreement about probabilities. The counterexample on p. 81 (the game with matrix rows and ) shows that hypothesis (6.3) is needed for both players, and the paper notes that in any specific game only one player need use a subjective strategy, though which one depends on the game.
Lemmas 4.2, 4.4 and 7.1 are the model's basic existence results for objective randomization: every probability can be realised by an event that is secret (or public) and independent of finitely many given events. They are used throughout the paper, including in the companion mission.
The paper's proofs are published and accepted; none of these statements has a machine-checked proof. This mission produces the formal statements and invites complete proofs; Lemma 7.1 requires Lyapunov's convexity theorem for finite-dimensional non-atomic vector measures, which is not in Mathlib.
The central difficulty for the goal is that (6.3) gives each player only some subjective event, of unknown size and in his own information field, while (6.4) requires strict gains for both players under two different measures at once. The obvious approach, betting on one subjective event, gives one player a strict gain but, when that event is not known to the other player, the other player cannot condition his choice on it; the example on p. 81 shows that one-sided information genuinely fails. Both inequalities must be arranged simultaneously, and the strategies must remain measurable with respect to each player's own information.
For Lemma 7.1, a non-atomic scalar measure takes every value in , but the lemma asks for one event with prescribed values under measures and further measures simultaneously; this is the range of a vector measure, not of a scalar one.
0, 1 : Fin 2 (the paper's 1, 2). S 0, S 1, X are finite types and g is surjective.mΩ, an explicit parameter of RandomizingStructure; are σ-fields below it, and each is a probability measure on . Probabilities are ℝ≥0∞-valued; "probability " is ENNReal.ofReal α with .NoAtoms, which would trivialize the roulette hypotheses.IsValue u g v requires for a Nash equilibrium of the mixed extension (AGT.IsMixedNash from the published definition agt_games). A free would make the goal false. The minimax theorem is the published AGT.zero_sum_minimax.Needed infrastructure: Lyapunov's theorem (or a direct argument for the finite-dimensional case), manipulation of σ-fields generated by families of sub-σ-fields, and computation of for strategies with finitely many values. Lyapunov's theorem is reusable far beyond this mission. Contributions of any milestone are welcome.
A sorting network is a sorting procedure whose sequence of comparisons is fixed in advance, independently of the data. Its depth, the number of rounds of simultaneous comparisons on disjoint pairs, is the parallel running time. Sorting networks are used in parallel and hardware sorting, in switching networks, and in cryptography, where a data-independent (oblivious) sequence of operations is required. How small the depth can be as a function of the number of inputs is a basic question of parallel computation.
Timeline:
There are registers holding elements of a linearly ordered set. An elementary step (a comparator) with compares the contents of and and exchanges them if the content of is larger. Afterwards holds the minimum and the maximum of the two, and every other register is unchanged. A parallel step is a set of comparators in which no register occurs twice, so it has at most comparators. A comparator network is a finite sequence of parallel steps, fixed before the input is seen. Its depth is the number of parallel steps and its size the total number of comparators. sorts if for every input the output satisfies .
The construction runs on the tree of finite - sequences, whose levels are ordered lexicographically. A chain on level assigns to every node of that level a set of registers, with the sets pairwise disjoint and of a common size . A ⟨k, ε⟩ expander on ⟨A, B⟩, for disjoint register sets and , is a bipartite graph between and of maximum degree in which every nonempty has more than neighbours, and symmetrically for . The Lean development uses the names ComparatorNetwork, compareExchange, IsChain, chainN, IsExpander, IsLowerSection for these objects.
The constant is absolute and is not fixed. Any explicit value would be invalidated by the next improvement, and the paper gives none.
The result. The AKS theorem settles the asymptotic depth of sorting networks at and their size at . It gives an -time sorting algorithm with processors that performs only data-independent comparisons. It is the standard reference point for oblivious sorting in parallel algorithms, circuit complexity (sorting is in via comparators) and oblivious RAM constructions. Lemma 4, the ε-halver property of expander comparisons, is the component that later constructions (Paterson) reuse.
Formalizing it. The theorem has been proved since 1983. No Lean proof of the AKS theorem is known. Mathlib has no expander graphs in the ⟨k, ε⟩ sense and no sorting networks. The mission asks for a formal proof of the headline theorem by any route (the AKS construction or Paterson's variant), and for formal proofs of the paper's verified lemmas as reusable components. The expander lemma needs either an explicit family (Margulis; Gabber–Galil) or a probabilistic existence argument, both substantial on their own.
Every elementary argument stalls at depth : recursive merging needs merge rounds, and merging two sorted lists by a comparator network needs depth . A depth of therefore cannot come from exact merging. It must come from constant-depth approximate operations (ε-halvers, which require bounded-degree expanders) combined with a mechanism that corrects the errors they leave. In the paper this mechanism is a movement of registers up and down a binary tree, controlled by a family of constants chosen in a fixed order ("", p. 2). The accounting that shows the misplaced elements decay geometrically is the hard part. Several intermediate lemmas of the paper are false as printed, so the paper's text is not a checklist to transcribe.
Conventions committed to in Lean:
Fin n, and contents lie in an arbitrary linearly ordered type. A network is a List of layers, each a List (Fin n × Fin n) of comparators with distinct endpoints, and no register occurs twice in a layer. A comparator puts the minimum into , and both directions and are allowed. Sorts means the output is monotone for every linearly ordered type and every input, not only for permutations.Real.logb 2 n, and the goal is stated for . The constant is quantified before .Fin (2^i), with numeric order equal to lexicographic order. A chain is a Fin (2^i) → Finset R.Trivializing formalizations are ruled out. The goal is not "for every there is a network of depth " with the constant chosen after , which is true for trivial reasons. Layers without the disjointness condition would let a single layer contain a whole insertion sort. A bound on the number of comparisons alone, with unbounded depth, is a different and much older result; the goal states both the depth and the size bound.
The mission states the AKS theorem and the paper's lemmas that are correct as stated. It does not formalize the AKS algorithm itself (, , the operations CH1–CH4, IMP) or its intermediate Lemmas 5–11 and 13–15. Those depend on unspecified constants constrained only by "sufficiently small" chains, and Lemmas 5, 10 and 12(b) are false as printed. A solver may of course define the algorithm, with pinned constants, as part of a proof.
Contributions welcome: a library of comparator networks (composition, the 0-1 principle, depth of Batcher's networks), existence of bounded-degree bipartite expanders, the ε-halver lemma, and any complete proof of the goal. The network and expander definitions are independent of this paper and reusable.
Richard Bellman's survey The theory of dynamic programming (Bull. Amer. Math. Soc. 60 (1954), 503–515, DOI 10.1090/s0002-9904-1954-09848-8) introduced dynamic programming to a general mathematical audience. It states the principle of optimality (§2, p. 504): "An optimal policy has the property that whatever the initial state and initial decisions are, the remaining decisions must constitute an optimal policy with regard to the state resulting from the first decisions", and derives from it the functional equations of finite and infinite stochastic decision processes, (4.2) and (5.1) (p. 506).
The survey illustrates the method on a small number of worked examples. The second of them, §8 "Stochastic gold mining" (pp. 508–509), is the one with a sharp answer: a two-armed sequential allocation problem with an absorbing failure state, whose optimal policy is a simple index rule. It is an early instance of the allocation-index phenomenon later made general by Gittins and Jones (1974) and Gittins (1979), and the paper itself notes (p. 509) that the rule "is not valid generally in more complicated decision processes", citing a counterexample of Karlin and Shapiro. The full treatment is in Bellman's RAND report R-245 and his 1957 book Dynamic Programming.
Two gold mines, Anaconda () and Bonanza (), hold amounts and of gold. A single machine can be used in either mine. A use in Anaconda succeeds with probability : it then mines a fraction of the gold currently in Anaconda and the machine stays undamaged. With probability it mines nothing and the machine is destroyed. Bonanza behaves the same way with probability and fraction . While the machine works, the operator chooses the next mine; the aim is to maximize the expected amount mined before the machine is destroyed.
The only information the operator ever receives is that the machine still works. A policy is therefore a choice sequence : the mine for use number , applied if uses succeeded. With , the numbers of - and -uses among the first , use collects if and if , and does so with probability (, ). The expected return is
and Bellman's (8.1) defines the optimal return
In Lean these are expectedReturn p q r s σ x y and optimalReturn p q r s x y in the namespace BellmanTheoryDP.GoldMining.
Write and for the two branches of (8.2). For and :
The paper prints the rule with and in the denominators:
a. For , choose A, b. For , choose B, c. For , choose either.
and glosses it as "the locus of points where immediate expected gain over immediate expected loss is the same for both choices". The immediate expected loss is the probability of destroying the machine, (resp. ), not . As printed the rule is false: with , , , , , the printed indices are , but . The mission's goal is the corrected rule, the one the paper describes in words.
"Using this prescription, may be computed recurrently": the choice sequence generated by applying the corrected rule to the current amounts at every use satisfies .
The decision rule reduces an optimization over infinite sequences to comparing two explicit numbers, one per mine, each depending only on that mine's own data. This is the defining property of an index policy, and gold mining is one of the earliest problems where it was observed. The functional equation (8.2) is the concrete form, for this process, of the infinite-horizon equation (5.1) that the paper states formally.
Formalizing the example yields a complete machine-checked instance of the principle of optimality for an infinite-horizon stochastic process whose state space (the amounts left in the two mines) is infinite, where the supremum over policies is not attained trivially and the finite-horizon recursion does not apply directly. It also records, with a checked statement, the correction of the misprint in (8.3). No machine-checked proof of (8.2) or (8.3) is known to exist.
The equation (8.2) looks immediate, and the paper calls it "easily seen". The informal argument treats as the value of an optimal policy, but is a supremum over infinite sequences that need not be attained a priori, and the return of a sequence is an infinite series. The finite-horizon recursion (4.2) does not apply as it stands, because the process has no last stage and its state space, the amounts left in the two mines, is infinite.
The rule (8.3) compares the two optimal continuations and , which are themselves unknown. A comparison of the one-step gains alone does not decide it, as the misprinted rule shows. Parts a and b are strict preferences, so it is not enough to show that one choice is at least as good as the other.
Mine; a policy is a function ℕ → Mine (ChoiceSeq). All quantities are real numbers. Randomized policies are mixtures of choice sequences and give no larger return, so they are not modelled. No restriction to stationary or Markov policies is made: is the supremum over all sequences.tsum and a real iSup. For the parameter ranges above the terms are nonnegative, the partial sums are bounded by , and the family is bounded above, so neither Lean default value (0 for a divergent series or an unbounded supremum) arises; this is stated as the auxiliary theorem expectedReturn_le_add.AllocationIndices.two_discount_index_policy_optimal (Gittins et al., Theorem 3.4) concerns Markov bandits whose rewards are discounted by at global time ; gold mining multiplies by the success probability of each use of the mine used, so it is a different model and is not reused. BertsekasDP.dp_algorithm_optimality is finite-horizon and does not give (8.2).Contributions welcome: proofs of the auxiliary theorems, of (8.2), of the decision rule, and of the optimality of the index policy.
In the contextual bandit problem a learner repeatedly observes a context, picks one of actions, and sees the reward of that action only. Against a finite class of policies, statistically optimal regret of order has been known since EXP4 (Auer et al., 2002), but EXP4 maintains a weight per policy and costs time per round. For the large policy classes used in practice (linear classifiers, trees), that is prohibitive.
The oracle-efficient line of work accesses only through a cost-sensitive classification oracle (an arg max oracle, AMO). The RandomizedUCB algorithm of Dudík et al. (2011) obtains optimal regret with polynomially many oracle calls by solving a convex program in each round, but the number of calls is large. Agarwal, Hsu, Kale, Langford, Li and Schapire (2014) replace that solver by a coordinate descent method whose number of iterations, and hence of oracle calls, is bounded independently of . Their algorithm, ILOVETOCONBANDITS, and its practical variant are now standard references for oracle-based exploration.
This mission formalizes the optimization half of that paper: Algorithm 2 solves the per-epoch problem (OP) after at most coordinate steps.
Let be the actions, any set of contexts, and a finite nonempty set of policies. A history is a sequence of records with the observed reward and the probability with which was chosen. Write .
The inverse propensity scoring estimate (Eq. (1)) is
the estimated regret is , and for a minimum probability one sets with .
Weights are vectors ; is the set of nonnegative with . The smoothed projection of is
The optimization problem (OP) asks for with
Algorithm 2 starts from and loops. With , and : if it rescales by (Eq. (4)); then, if some has , it adds
to (Step 8) and repeats; otherwise it halts and outputs .
The analysis uses the potential (Eq. (6)), with and uniform on ,
For , Algorithm 2 with satisfies: every run executes Step 8 at most
times, whatever policy each Step 8 chooses among those with ; and when it halts, its output solves (OP). The bound depends on only, not on or .
The result. Theorem 3 is what makes ILOVETOCONBANDITS computationally efficient: each call of Algorithm 2 is implemented with one AMO call per iteration (Lemma 1 of the paper), so the oracle complexity of an epoch is . Combined with the epoch schedule and warm start, this gives the paper's total of oracle calls over rounds. Theorem 3 also gives a constructive proof that (OP) is feasible for every history, which the regret analysis (a separate mission in this series) assumes.
Formalizing it. The result is proved in the paper, with complete proofs of Lemmas 5–7 in Appendix D. No machine-checked version is known. The formalization would give a checked termination bound for a coordinate descent method on a non-smooth feasibility problem, with a fully explicit constant, and a verified definition of the unnormalized relative entropy potential that is reusable for other smoothed-projection analyses (e.g. RandomizedUCB-type convex programs).
Termination cannot be read off the constraints. Step 8 raises one weight and can push the total weight above 1, after which Step 5 shrinks every coordinate, so no constraint and no single weight moves monotonically along a run. The number of policies that violate (3) can also go up after a step. Bounding the number of iterations therefore needs a global quantity that tracks progress through both kinds of step. The rescaling step is the harder of the two: it lowers every at once, which pushes the relative-entropy term the wrong way, and it must be offset by the drop in the regret term. Knowing that (OP) is feasible, or that some convex function has a minimizer, bounds nothing about how many steps a particular method takes; that is the obvious approach, and it gives no count.
Fin K with ; contexts form an arbitrary type (no measure is needed: Theorem 3 is deterministic). is a nonempty Finset (X → Fin K); weights are real functions on its subtype.Fin t with (0-based indices). The paper allows ; the formalization requires , since Eq. (1) divides by it.Many sequential decisions are personalised: a physician chooses a drug dose for each arriving patient, a platform chooses which offer to show each arriving user. Each decision is made after observing a vector of covariates describing the individual, and its outcome is observed only for the option chosen. This is the contextual (covariate) bandit problem, studied in operations research and machine learning since Auer (JMLR 2002) and Goldenshluger and Zeevi (Stochastic Systems 2013).
In medical and e-commerce applications the covariate vector is often high-dimensional: the number of covariates is comparable to or larger than the number of decisions that will ever be made, while the outcome of each option depends on a few of them. Low-dimensional bandit algorithms then incur regret that grows polynomially with . Bastani and Bayati (Operations Research 2020) proposed the LASSO Bandit, which estimates each option's reward model with the LASSO, and proved a regret bound that grows only logarithmically in . The paper evaluates the method on warfarin dosing data.
Timeline:
There are arms with unknown parameters . At each time a covariate vector arrives; the are i.i.d. with law and take values in a fixed set . If arm is pulled, the reward is , where the noises are independent, -subgaussian ( for all ), and independent of the covariates. A policy chooses the arm from and the past covariates, arms and observed rewards. Its cumulative expected regret is
The sparsity is the smallest integer with for all .
The four assumptions are: (1) on and ; (2) a margin condition ; (3) arm optimality: every arm is either suboptimal by a margin at every covariate, or optimal by margin on a region of probability at least ; (4) a compatibility condition: the conditional second-moment matrix of each optimal arm lies in the set of matrices with whenever .
The LASSO estimator on samples is any minimizer of . The LASSO Bandit forces arm at the prescribed times . At every other time it keeps the arms whose forced-sample estimate is within of the best. Among them it plays the arm with the largest all-sample estimate , trained on every past pull of the arm, with .
For , , , , and ,
with the explicit constants , of the paper (p. 285).
The theorem shows that exploiting sparsity makes the regret depend on the ambient dimension only through , while its dependence on the horizon is within one factor of the lower bound known in low dimension. Proposition 1 is a LASSO oracle inequality for adapted designs, where each row may depend on earlier observations. It applies whenever a LASSO is fitted to data gathered by a feedback policy: adaptive experiments, dynamic pricing, sequential treatment assignment.
The results are proved in the paper and its online appendix; none of them has a machine-checked proof. This mission produces a formal model of the covariate bandit with a non-anticipating algorithm, a formal LASSO for adapted designs, and, when complete, a verified regret bound with every constant explicit. Proposition 1 and Lemma 1 are reusable beyond bandits.
The all-sample estimator is trained on the times at which the algorithm chose an arm, and those choices depend on earlier estimates. Its design rows are therefore neither independent nor identically distributed, and the standard LASSO analysis, which starts from i.i.d. rows and a restricted-eigenvalue bound on their population covariance, does not apply. The forced samples are i.i.d. but only in number, too few for the rate the regret bound needs. Controlling the compatibility constant of the adaptively selected sample covariance, and the martingale noise term, is where the naive argument breaks.
Arms are Fin K (paper arm is i.val + 1), coordinates Fin d, times are natural numbers from . The model is a structure IsCovariateNoiseModel on a probability space: i.i.d. measurable covariates in a measurable set , independent subgaussian noises (Mathlib's HasSubgaussianMGF with parameter ), noise independent of covariates. Assumptions 1–4 are separate predicates. is Mathlib's sup norm, logarithms are natural, and is the uncentred conditional second moment.
The LASSO minimizer and the arg max need not be unique, so the algorithm takes a selection rule and a tie-breaking rule as parameters, and the theorems hold for all of them. Each round reads only the current covariate, the past covariates, the past arms and their observed rewards. The regret theorem and Proposition 3, whose data set is chosen by the algorithm, require both rules to be measurable. Otherwise the trajectory would not be a random variable, and the expectations in could be integrals of non-measurable functions, which Lean evaluates to and which would make the goal trivially true. For the same reason every assumption constant is required to be positive, and is imposed on the horizon. Only the explicit inequality of Theorem 1 is stated, not the trailing or . Proposition 2 is stated for optimal arms (see its note).
A complete development needs matrix concentration for bounded i.i.d. rows, the Azuma–Hoeffding inequality, and the deterministic LASSO basic inequality under a compatibility condition. Contributions of any of these as standalone lemmas are welcome.
In a contextual bandit problem a learner repeatedly observes a context (a user, a patient, a query), chooses one of actions, and observes the reward of the chosen action only. It competes with the best policy of a fixed class of maps from contexts to actions. This is the standard model for news and advertisement recommendation, adaptive clinical assignment and other interactive decision problems in which counterfactual rewards are never observed.
Two requirements pull against each other. Statistically, the optimal regret against a finite class is of order , attained by the exponential-weights algorithm Exp4 (Auer et al. 2002), whose running time is linear in per round. Computationally, practical policy classes are exponentially large and are accessed only through a supervised learning routine. Agarwal, Hsu, Kale, Langford, Li and Schapire (2014) give ILOVETOCONBANDITS, which reaches the optimal regret while touching only through an arg-max oracle, and only times in rounds.
Timeline. Exp4 (2002) attains against adversarial rewards with running time . Epsilon-greedy and Epoch-Greedy (Langford and Zhang 2007) are oracle-efficient but have regret of order . Exp4.P (Beygelzimer et al. 2011) proves the optimal bound with high probability. RandomizedUCB (Dudík et al. 2011) is the first oracle-based algorithm with optimal regret in the i.i.d. model, but its number of oracle calls is a large polynomial in . ILOVETOCONBANDITS (2014) keeps the regret and reduces the calls to .
There are actions, a measurable context space , and a finite nonempty policy class of measurable maps . A distribution on generates context/reward-vector pairs , , independently. In round the learner sees , draws an action with probability , and observes only . The history is the list of records , .
The expected reward of a policy is , is any maximizer over , and . The regret after rounds is the empirical cumulative quantity .
The inverse propensity scoring estimate is , and . For nonnegative weights on with total mass at most one, the smoothed projection is .
ILOVETOCONBANDITS takes an epoch schedule and , sets and . At the end of epoch (round ) it chooses weights solving the optimization problem (OP): with ,
During epoch it puts the leftover mass on the empirical maximizer , obtaining a distribution , and draws .
Assume for and let , , , , and . For every , with probability at least ,
It holds for every (OP)-solution selection and every tie-breaking rule. Since once , this is the paper's .
Freedman's inequality (Lemma 9); the uniform deviation of true from empirical variances (Lemma 10); the deviation of the IPS estimates (Lemma 11); on the event where both deviations hold, the variance bound (Lemma 12), the two-sided comparison of and (Lemma 13), and the low regret of the sampling distribution (Lemma 14); and the deterministic sums of the (Lemmas 15, 16).
The theorem shows that optimal regret in the i.i.d. contextual bandit problem does not require enumerating the policy class: a sequence of convex feasibility problems, each solvable with few oracle calls (Theorem 3, the companion mission), suffices. The inverse-propensity variance constraint of (OP) and the epoch-and-warm-start structure became the template for later oracle-based methods, and the paper's Online Cover variant is implemented in the Vowpal Wabbit learning system.
The result is proved in the paper; none of it is formalized. The platform holds Exp4 (Bandit Algorithms VIII, adversarial rewards and expert advice) and SquareCB (Foundations of RL II, regression oracles), both different algorithms in different models, and Azuma–Hoeffding (bounded_diff_martingale_two_sided), which the proof of Lemma 17 uses. This mission adds the first inverse-propensity estimator, the first oracle-based policy-class bandit algorithm, and Freedman's inequality with a conditional-variance sum. Several statements are proved in the paper only in outline: Lemma 10 has a proof sketch that defers to Dudík et al. (2011), and the paper asserts without spelling out how the first case of (14) follows from Lemma 11.
The regret of the algorithm depends on the quality of its own data. The estimates have variance governed by the distributions the algorithm chose earlier, and those distributions were chosen from the estimates. A direct union bound over with the worst-case variance gives regret of order , the Epoch-Greedy rate. The argument that avoids this must show that a policy with large variance was already known to be bad, and the estimated and true regrets must be compared inductively over epochs with constants that do not grow (). The inequality must also hold for every solution of (OP), not a particular one.
The martingale structure requires care: the action of round is drawn from a distribution that depends on the whole past and must not look at , and Lemma 10 must hold uniformly over all distributions on , not just finitely supported ones.
The formalization commits to the following representation and conventions.
Fin K with 0 < K (NeZero K); is a nonempty Finset (X → Fin K) of measurable maps; weights on are real functions on its subtype. is a probability measure on X × (Fin K → ℝ) with rewards in almost surely.Real.log.A statement about "a policy mixture with small regret", about the pseudo-regret of the chosen policies, about a specially chosen (OP) solution, or about actions that may depend on is not Theorem 2; none of these is accepted. With these constants the bound exceeds unless is very large, which is a property of the paper's constants, not of the encoding.
Needed infrastructure: Freedman's inequality for the natural filtration, a uniform-over-distributions concentration argument (the probabilistic method of Dudík et al.), measurability of the algorithm's run, and Azuma–Hoeffding. Freedman's inequality and the IPS estimator are reusable beyond this mission. Proofs of any milestone, and sharper or cleaner restatements proved as separate lemmas, are welcome.
A retailer or manufacturer that stocks several grades of the same item (memory chips of different speeds, steel of different strengths, seats in fare classes) can often meet demand for a lower grade with a higher one when the lower grade runs out. This downward substitution changes the stocking decision: each product now protects the demand of every class below it, so the optimal stock of one product depends on the stock of all the others, and the single-product newsvendor answer no longer applies product by product.
Bassok, Anupindi and Akella (Operations Research 47(4), 1999) set up a single-period model with products and full downward substitution and showed that the optimal ordering policy still has a simple structure: there is a base-stock vector ; products below it are ordered up to it, and a product already at or above its base-stock level is not ordered at all. Earlier work on multiproduct ordering, Veinott (1965) and Ignall and Veinott (1969), gave monotonicity conditions through a substitute matrix condition on the Hessian of the cost, which is hard to verify for a general -product substitution structure; the paper works instead with concavity, submodularity and explicit first partial derivatives. Two-product substitution models had been analysed by McGillivray and Silver (1978) and Parlar and Goyal (1984).
There are products and demand classes, both numbered . Class can be served by product whenever , at a unit substitution cost when . Each class has unit revenue and unit backorder cost ; each product has unit purchase cost and effective unit salvage value (salvage value minus holding cost, possibly negative). Put if , if , and . The standing assumptions are: (1) for ; (2) for ; (3) for .
The sequence of events: the starting inventory is observed; stock is raised to at unit costs ; the demand vector is realized; stock is allocated to classes; leftovers are salvaged. For fixed and the allocation is the linear program
subject to , , and , where is the amount of product given to class , the shortage of class and the leftover of product . The expected profit is
and the ordering problem is ; a maximizer is an optimal level .
Allocation Algorithm (A) serves the classes in the order , class first from product and then from the leftovers of products . The subproblem shortage is the unmet demand of class when (A) runs on the classes with the products only; means for all . The paper's first partial derivatives of are sums of salvage values, substitution costs and the , weighted by probabilities of such shortage events.
With a maximizer of over , every optimal level for every starting inventory satisfies
Theorems 1 and 2 give the optimal ordering policy of the substitution model its base-stock form: a vector , computed once, determines the decision for every starting inventory in the region and fixes the order of every overstocked product elsewhere. The paper builds its bounds on , its iterative algorithm for two products and its computational study of the value of substitution (§3) on this structure. Proposition 1 turns the second-stage linear program into a closed-form greedy allocation, which is what makes the derivative formula (4) explicit.
The results are proved in the paper, but none of them has been machine-checked. Several steps of the paper are informal: Proposition 1 is proved by reference to Monge sequences of transportation problems, the proof of Theorem 2 treats only the adjacent pair , and the paper uses independence of demand classes, densities and a unique optimal level without stating them. A formal development makes these hypotheses explicit and checks each step. The model, the greedy allocation and the shortage calculus are reusable for other multi-product newsvendor and assortment models.
The obvious argument for Theorem 2 is the one-dimensional one: if then at , so product should not be raised. It fails because depends on the other coordinates: at some products are raised above and others kept at , and concavity plus submodularity alone do not control the sign. For a general concave submodular function the conclusion is false; a three-variable quadratic in which raising one coordinate lowers the optimal level of a second one, which in turn raises the marginal value of the first, is a counterexample. The proof has to use the specific structure of the substitution model, through the pairwise comparison of the partial derivatives in Eq. (4). The derivative formula itself requires a careful account of how an extra unit of product propagates through the greedy allocation of every later class.
Products and classes are indexed by Fin N (the paper's index is Lean index ); stocks, demands and prices are real. The allocation LP is encoded with the upward arcs , , forbidden (fixed to ), as in the paper's proof of Proposition 1; is the supremum of the LP objective. The demand law is a product . Submodularity is the lattice inequality , which is equivalent to the paper's nonpositive cross partials (Definition 2) for twice differentiable functions. Derivatives are stated with HasDerivAt, and the derivative inequalities of Lemmas 2 and 5 in the stronger monotone form, so that no statement is made true by a junk value of deriv. The "…" in Eq. (4) and in the lemmas are expanded as finite sums with the general term inferred from the printed first and last terms.
Hypotheses the paper uses without stating, made explicit here:
The goal quantifies over every maximizer of and every optimal ; it is not an existence statement, and is not chosen by the prover. Without the full-support hypothesis the universal statement fails already for one product (a flat-topped profit). Lemmas 4 and 6 of the paper are not included: under the definitions used here both are false as printed (small two- and three-product computations with exponential demands show it), and Theorem 3 comes after the goal and fails as printed for .
A proof needs integrals of piecewise-linear functions of the demand vector, differentiation under the integral sign, and facts about product measures. Contributions of any of the milestones, and of general lemmas on the greedy allocation (monotonicity of in and ), are welcome.
Many US school districts assign children to public schools centrally. Each family ranks the schools. Each school ranks the children by priority, which is set by state or local law (siblings, walking distance, a lottery). A procedure then turns these rankings into an assignment. Abdulkadiroğlu and Sönmez (Columbia Economics Discussion Paper 0203-18, 2003; published in the American Economic Review 93(3), 2003) cast this as a mechanism design problem. They showed that the mechanisms then in use in Boston, Columbus and Minneapolis gave families reasons to misreport their preferences. They proposed two alternatives: the student-optimal stable mechanism of Gale and Shapley, and a school-choice version of Shapley and Scarf's top trading cycles (TTC) mechanism.
Many districts also operate under controlled choice: court-ordered or voluntary rules that keep the racial or ethnic composition of each school within bounds. In Minneapolis, for instance, a 100-seat school could admit at most 75 majority and at most 55 minority students (paper, Section III). Such rules are implemented as type-specific quotas. Section III.B of the paper modifies TTC to respect these quotas. It proves that the modified mechanism keeps both properties that recommend TTC: it wastes nothing beyond what the quotas force (constrained efficiency, Proposition 6), and truth-telling is a dominant strategy (strategy-proofness, Proposition 7). This mission formalizes those two results.
There is a finite set of students and a finite set of schools. School has a capacity , and the total number of seats suffices: . Each student has a strict preference over all schools, encoded as a ranking with rank the favourite. Each school has a strict priority ranking over all students, with rank the highest priority. Each student belongs to exactly one type , and school has a type quota for each type .
An assignment gives each student a school or nothing (, worse than every school). It satisfies the controlled choice constraints if every school receives at most students, and at most students of each type . An assignment is constrained efficient if no assignment satisfying the constraints makes every student weakly better off and some student strictly better off.
The top trading cycles mechanism with type-specific quotas, , runs in steps. Each school keeps a counter (initially ) and one type counter for each type (initially ). A school is removed when reaches zero. At each step:
A direct mechanism is strategy-proof if no student can ever gain by misreporting her preference, whatever the others report.
For every student , every profile of announced preferences and every alternative report ,
This holds for all capacities without shortage, all quotas, all types and all priorities. The priorities are fixed data, not reported.
Strategy-proofness is what lets a district publish a simple instruction: rank the schools in your true order. A strategy-proof mechanism does not reward families who can afford to gather information and game the system. Proposition 7 shows that this guarantee survives the addition of flexible diversity quotas, which many districts are legally bound to impose. Proposition 6 shows that the quotas cost nothing beyond the losses they themselves cause. Both results were proved in 2003 by pen and paper. The published proof of Proposition 7 is a short adaptation of the proof of Proposition 4 (strategy-proofness of plain TTC). It rests on a lemma about how the algorithm's intermediate states depend on one student's report.
To our knowledge neither result has a machine-checked proof. The related platform theorem AGT.ttc_strategyproof concerns the Shapley–Scarf housing market, where every agent owns one house and the mechanism selects the core. It does not cover capacities, priorities or quotas. A formal proof here would check the adaptation that the paper leaves to the reader, and would give a reusable formal model of cycle-clearing allocation algorithms with multiple counters.
The algorithm clears all cycles of a step at once, and a student's report changes the graph at every step she is present. The paper's argument compares two whole runs of the algorithm, under the true report and under a misreport, step by step. That comparison needs precise control of which parts of the state a single student's report can influence, and when. A local argument about one step does not suffice. The student's outcome can depend on cycles that form several steps after the two runs could first have diverged.
With quotas, the pointing graph also depends on the type counters. A school can be present but closed to one type, and a school points to its best remaining student even when it has no room for her type. The comparison must therefore track the type counters as well as the set of remaining schools. Efficiency cannot be read off step by step against unrestricted matchings either: every competing assignment must satisfy both the capacity and the quota constraints.
Students, schools and types are finite types; no nonemptiness is assumed. Preferences and priorities are bijective rankings onto Fin, so strictness is built in. Rank is the favourite or the highest priority. The no-shortage condition appears in every theorem, as the standing assumption of Section I. No relation between and is imposed, which generalises the paper.
The algorithm is a concrete, total definition: a state with remaining students, counters, type counters and partial assignments, a step map that clears all cycles simultaneously, and iterations. run … t is the state at the beginning of the paper's Step .
The paper's step is undefined when a remaining student has no remaining school with room for her type. She cannot point, and the promised cycle may not exist. The formalization adopts one convention: at the beginning of each step, such a stuck student is removed unassigned, and her outcome is , ranked below every school. Counters only decrease, so a stuck student stays stuck. Whenever nobody gets stuck, the algorithm is exactly the paper's, and when every quota is at least the capacity it is plain TTC. The goal and Proposition 6 are stated for assignments that may leave students unassigned. When everyone is assigned, they coincide with the paper's statements over matchings.
The formalization does not add a hypothesis that the run never gets stuck. Such a hypothesis would restrict the algorithm's own behaviour and could make the theorems vacuous. Nor may strategy-proofness be weakened to comparisons at the truthful profile only: the others' reports and the misreport are arbitrary.
Contributions welcome: invariants of the step map (counters bounded by the initial values, assigned students leave for good), the cycle-existence lemma for functional graphs on finite sets, and the comparison lemma. These pieces are shared with the plain-TTC mission of this series.
Public school districts in many US cities let families rank schools and then assign seats by a centralized procedure. Each school has a limited number of seats, and state or local law gives some students priority at some schools, for example for a sibling already enrolled or for living within walking distance. Abdulkadiroğlu and Sönmez (Columbia Economics Discussion Paper 0203-18, 2003; published in the American Economic Review 93(3), 2003) framed this as a mechanism design problem and showed that the mechanism then used in Boston rewards families who misreport their preferences. They proposed two replacements with written proofs of their properties. This mission covers the second one, the top trading cycles mechanism, and its two properties: every outcome is Pareto efficient, and no student can gain by misreporting.
The paper drew on earlier results for simpler allocation problems:
A school choice problem consists of a finite set of students, a finite set of schools, a capacity for each school, a strict preference of each student over all schools, and a strict priority ordering of each school over all students. The standing assumption is that there is no shortage of seats:
Preferences are rankings: is the rank of for student , with rank the favourite. Priorities are rankings of students in the same way, with rank the highest priority. A matching is a map with for every school . A matching is Pareto efficient if no other matching gives every student a weakly better school () and some student a strictly better one.
A direct mechanism maps the reported preference profile, together with the fixed priorities and capacities, to a matching. It is strategy-proof if no student can ever obtain a school she strictly prefers by changing her own report while the others keep theirs.
The top trading cycles algorithm keeps a counter of free seats at each school, starting at . A school is remaining while . At each step every remaining student points to her favourite remaining school, and every remaining school points to the remaining student with the highest priority for it. A cycle is a list of distinct schools and students in which points to , points to , and so on, and points to . Every student on a cycle is assigned the school she points to and is removed. Each school on a cycle loses one seat. All cycles present at a step are cleared at that same step. The top trading cycles mechanism returns the resulting assignment.
For all capacities with no shortage, all priorities, every profile , every student and every alternative report , student is assigned schools and , and
Strategy-proofness means truthful reporting is a dominant strategy for every student. Families need no information about other families' reports. Under the Boston mechanism, ranking a popular school first can cost a student her priority at her second choice. Proposition 3 separates the top trading cycles mechanism from the Gale–Shapley student-optimal stable mechanism, which is also strategy-proof but can select Pareto dominated matchings.
The results are proved in the paper, in short prose arguments in its Appendix. To the best of our knowledge they have no machine-checked proof. The platform already has the housing-market version, AGT.ttc_strategyproof, but that statement covers one house per agent with the mechanism characterised as the core. Capacities, school priorities and the step-by-step algorithm are absent from it. This mission produces a checked account of the algorithm with capacities and counters, together with its termination and invariance properties.
The paper's argument moves from the step at which student leaves under one report to the step at which she leaves under another. It relies on the claim that the cycles formed before either step are unaffected by 's report. Informally, is not on a cycle yet, so what she points to does not matter. Formally, "the same cycles form" requires comparing two runs of a simultaneous-clearing procedure step by step. At each step one has to show that the set of cycles, and hence the counters and the remaining schools, agree, even though points to different schools in the two runs. Reasoning about a single cycle at a time does not work, because the algorithm clears all cycles of a step at once. Termination is also not immediate: without the no-shortage condition the algorithm can leave students unassigned. Seats are counted with multiplicity, so a school can stay in the market for several steps.
Everything lives in the namespace SchoolChoice.TTC. Students and schools are arbitrary finite types with decidable equality; the set of students may be empty. Capacities are q : S → ℕ, and a school of capacity zero is never remaining. A preference is a bijection S ≃ Fin (card S) and a priority is a bijection I ≃ Fin (card I), in both cases with rank 0 the best. Strictness and completeness of both therefore hold by construction, and every school is acceptable. A state of the algorithm consists of the remaining students, the counters and the assignments made so far. run q pri P t is the state after t completed steps, which is the beginning of the paper's Step t + 1. The mechanism ttc q pri P : I → Option S reads off the assignment after card I steps. Every theorem assumes card I ≤ ∑ s, q s.
The algorithm is a concrete, deterministic definition that clears all cycles at every step. The mechanism is not defined as "some Pareto efficient matching" or characterised by properties, since that would make Proposition 3 trivial. The goal asserts that both outcomes exist, so an unassigned outcome cannot satisfy it vacuously. The misreport, the other students' reports and the priorities are all universally quantified.
A complete development needs termination of the algorithm, a combinatorial account of the pointing graph (cycles in a finite functional graph), and the step-by-step invariance argument of the Lemma. The last two are reusable for the type-specific quota variant and for other trading-cycle mechanisms. Contributions of intermediate lemmas are welcome: counter invariants such as "the sum of the counters is at least the number of remaining students", monotonicity of the remaining sets, and the fact that a student on a cycle receives her favourite remaining school.
Retailers that sell the same product can raise their joint profit by pooling: stock left over at one location is shipped to meet unmet demand at another, and stock can be held in shared warehouses until demand is known (Eppen 1979; Eppen and Schrage 1981). When the retailers are independent firms, pooling creates two questions at once. After demand is realized, the extra profit from shipping must be split in a way no group of retailers would reject. Before demand is realized, each retailer chooses its own stock, and that choice depends on how the split will be made. A split that is fair ex post may lead to stocking decisions that are poor for the system as a whole.
Anupindi, Bassok and Zemel (MSOM 2001) model the ex-post split as a cooperative game, the ex-ante stocking as a non-cooperative game, and ask whether a single allocation rule can serve both. Their framework is a standard reference for "coopetition" models in supply chains, where firms compete on stocking decisions and cooperate on redistribution.
There are retailers and warehouses . Retailer has unit cost , revenue and salvage value ; warehouse has purchasing cost and salvage value . Shipping from location to retailer costs per unit, and a fraction of the customers at accept service from .
Before demand, retailer chooses a position : local stock and claims on warehouse stock, so warehouse holds . A profile is . Demand is random with law . After demand, retailer has local sales , residual inventory and residual demand .
The snapshot allocation game SAG gives each coalition the value : the optimal value of the linear program (6), which ships units from to at profit per unit, subject to , and . Its core is the set of allocations with for every and (7).
An allocation rule AR- assigns surplus ; retailer earns
and expects . A Nash equilibrium (10) is a profile at which no retailer gains by changing its own position. The first-best profile maximizes the expected centralized profit , where .
The fractional rule AR-f (11) pays with fixed shares , . The dual allocation (8) is for optimal dual prices of (6) for . The modified rule AR-c is with .
For a first-best profile and a measurable choice of dual prices at ,
with integrable side payments.
The goal answers the paper's central question positively: there is an allocation mechanism under which the centrally optimal stock levels are an equilibrium of the decentralized stocking game, while every ex-post split of the pooling surplus is stable against all coalitions. Theorem 4.1 is the ex-post half: shadow prices of the shipping LP give a stable split for every realization, independently of who owns which units. The paper also shows (Proposition 5.1, not included here) that the dual allocation alone does not induce first-best stocking, which is why the side payments of Theorem 5.1 are needed.
The results are proved in the paper; Theorem 4.1 is proved there only by reference to the LP-game literature (Owen 1975; Samet and Zemel 1984). None of them has a machine-checked proof. The mission would produce the first formal treatment on Prove2Me of a linear-production (LP) game and its core, and of a model combining a cooperative second stage with a non-cooperative first stage.
Theorem 4.1 is an instance of Owen's theorem on LP games, but the instance is not a standard linear production game: coalition LPs have variables only on arcs inside the coalition, warehouse capacity is limited to the coalition's own claims, and the acceptance constraint divides by , which may be zero, so the general theorem cannot be quoted as it stands. The paper leaves the dual of (6) unwritten, and Mathlib has no ready-made LP duality in this form.
The stochastic layer is the other obstacle. Expected payoffs are integrals, and the side payment is built from a choice of dual prices for each demand realization. Its integrability requires measurability of that choice and of the LP value as a function of demand; neither is given by the paper, which treats the side payments as "constants".
Retailers are Fin N, warehouses Fin W, locations Fin N ⊕ Fin W; quantities, prices and demands are real numbers; demand is a probability measure on Fin N → ℝ; expectations are Bochner integrals. is the real supremum of (6a) over the feasible set, and profiles are required to be nonnegative, which makes the feasible set nonempty and bounded. Arcs with carry no shipment. The core is the platform definition Supermodularity.Cooperative.Core. The dual of (6) is written out explicitly (the paper does not state it). The paper's continuous-CDF assumption is not used and is dropped.
Pinned readings:
Not acceptable: a core without the efficiency equation (7b); a feasible set that lets sell to customers who balk; an arbitrary side payment instead of the constructed one; or a Nash equilibrium evaluated through non-integrable payoffs, whose Bochner integral is and makes every profile an equilibrium.
Useful infrastructure: finite-dimensional LP duality in inequality form, measurable selection of LP optimal solutions, and continuity of LP values in the right-hand side. All of it can be reused in other LP-game and two-stage stochastic programming missions.
A polyhedral cone can be described in two ways: as the set of nonnegative combinations of finitely many vectors (a finitely generated cone), or as the intersection of finitely many closed half-spaces through the origin. That the two descriptions give the same class of sets is the Minkowski–Weyl theorem. It is the structural basis of linear programming: the simplex method, LP duality, Farkas' lemma, and the vertex/facet description of polytopes used throughout combinatorial optimization all rest on it.
Hermann Weyl's 1935 paper Elementare Theorie der konvexen Polyeder (Comment. Math. Helv. 7, 290–306) gives an elementary, self-contained proof of both directions. Its first result, which Weyl calls the Hauptsatz (main theorem, Satz 1), is the direction "finitely generated ⇒ finite intersection of half-spaces", in a sharp form: the half-spaces needed are exactly the extreme supports of the generating set, i.e. its facets. Its sharpening, Satz 2, bounds the number of generators needed to represent a point by the dimension . This mission formalizes §§1–2 of the paper (pp. 290–295): the Hauptsatz, its sharpening, and the steps of Weyl's inductive proof.
Timeline:
Points of are -tuples , and . A vector determines the half-space ; positive multiples of give the same half-space.
A point system is a finite set of points of . It is non-degenerate if its points do not all satisfy one equation with , i.e. the only orthogonal to every point of is .
A half-space () is a support of if every point of lies in it. It is an extreme support if, in addition, equality holds at linearly independent points of .
A point is representable by if it is a nonnegative combination of the points of :
The set of points lying in all extreme supports of is Weyl's konvexe Pyramide. In the Lean development these objects are Representable, NonDegenerate, IsSupport and IsExtremeSupport in the namespace WeylPolyhedra.Pyramid, with points of type Fin n → ℝ and written α ⬝ᵥ x.
For a finite non-degenerate and a point with for every extreme support of ,
Under the same hypotheses, is representable by . Satz 2 contains Satz 1.
Satz 1 together with its trivial converse identifies the cone generated by with the intersection of its extreme-support half-spaces. This is one half of the Minkowski–Weyl theorem for cones, and it names the half-spaces: they are the facets of the cone. Satz 2 adds the conic form of Carathéodory's theorem: every point of a cone generated by a finite spanning set in is a nonnegative combination of at most generators. In linear programming this is the statement that a feasible system has a basic feasible solution. The second mission in this series, on §§3–4 of the paper, uses Satz 1 to prove that a bounded region cut out by finitely many inequalities is the convex hull of finitely many points, and conversely.
On formalization status: Mathlib defines finitely generated and dually finitely generated pointed cones (PointedCone, PointedCone.DualFG) and proves Carathéodory's theorem for convex hulls (convexHull_eq_union), but, at the pinned revision, it does not prove the Minkowski–Weyl theorem or the facet description of a finitely generated cone. The results are classical and proved in the paper; this mission produces machine-checked proofs of them, in Weyl's formulation with extreme supports, together with the intermediate steps of his induction.
The hypothesis only controls against the extreme supports, not against every support. Showing that lies in the cone generated by whenever holds for every support is the conic Farkas lemma, which follows from a separating hyperplane argument. Here that argument is not enough: a separating hyperplane is a support, but in general not an extreme one, and the statement is about the finitely many extreme ones. The proof has to produce, for a point outside the cone, a violated extreme support, which requires control over the facet structure of the cone.
The dimension count of Satz 2 is a second difficulty. An induction on the dimension naturally gives generators in one case and in another (a point of a half-space needs one generator on each side), and Weyl notes that he could not avoid a detour to recover the bound . The case where has no extreme support at all must also be handled separately; it is not vacuous, since can then generate all of .
Conventions committed to in Lean:
Fin n → ℝ; points and normals share this type (the dual space is identified with , as in the paper). The pairing is dotProduct, written α ⬝ᵥ x.Finset (Fin n → ℝ). The zero vector is not excluded.α ≠ 0. Extreme supports require a subset T ⊆ S with T.card = n - 1 whose elements are linearly independent in the vector space .Fin (m+1) → ℝ, the extreme support is (Fin.last m), is projected by Fin.init, and is given together with hypotheses that it is the attained minimum. The hypothesis is made explicit.Replacing extreme supports by all supports in the hypothesis of Satz 1 or Satz 2 would turn the goal into a much weaker theorem (the conic Farkas lemma plus Carathéodory) and is not an admissible formalization. Dropping non-degeneracy makes Satz 1 false: for the extreme supports are , and satisfies both without being a nonnegative multiple of .
A complete development needs basic linear algebra over Fin n → ℝ (hyperplanes through independent points, projection to a coordinate hyperplane) and finite minimisation. The facet description of finitely generated cones, conic Carathéodory and the finiteness of facets are reusable beyond this mission, including for the second mission of the series. Contributions of lemmas on PointedCone that connect Representable with PointedCone.span are welcome.
Market equilibrium is the central solution concept of general equilibrium theory: prices at which every agent buys a utility-maximizing bundle and supply meets demand. Arrow and Debreu (1954) proved that equilibria exist under mild conditions on endowments and utilities, and a line of work in algorithmic game theory asks how hard it is to compute them. For linear utilities an equilibrium can be computed in polynomial time, and there is an efficiently checkable condition for its existence. The next natural class, additively separable piecewise-linear concave utilities, models diminishing marginal utility and is the class most used in applications.
Vazirani and Yannakakis (J. ACM 58(3), 2011) settle the complexity of this class. They show that equilibria are rational whenever they exist (Theorems 4.1 and 5.1), that computing an equilibrium under the standard sufficient conditions is PPAD-complete (Theorems 6.1 and 7.1, building on Chen, Dai, Du and Teng 2009), and — the subject of this mission — that deciding whether an equilibrium exists at all is NP-complete (Theorem 8.1). The hardness half rests on an explicit construction: from an instance of Exact Cover by 3-Sets, a market whose equilibria encode exact covers.
An Arrow–Debreu market has a finite set of agents and a finite set of divisible goods. Agent owns an endowment of each good and has utility , where each is a piecewise-linear concave utility function: slopes on consecutive pieces of lengths , followed by a last piece of slope until infinity ( means the function goes flat).
At prices , agent 's income is . An optimal bundle is an affordable maximizing among affordable bundles, bought only along the pieces of that carry utility. A price equilibrium is a price vector in the unit simplex (, ) together with an allocation of optimal bundles such that for every good . It is an -approximate equilibrium if instead for every .
An X3C instance is a family of -element subsets of ; an exact cover is a subfamily in which every element of lies in exactly one set. Following the paper, is a multiple of , , and .
The market has goods (good , goods , goods ) and agents, with :
All other utility functions are flat.
This is the mathematical content of the NP-hardness half of Theorem 8.1, assembled by the paper from Lemmas 8.2 and 8.3.
Theorem 8.1 shows that there is no efficiently checkable necessary and sufficient condition for the existence of an equilibrium in piecewise-linear concave markets unless P = NP, in contrast with the linear case. Together with the PPAD results of the same paper it separates two questions: under the classical sufficient conditions an equilibrium exists and finding one is PPAD-complete; without them, even deciding existence is NP-hard, and remains so for -approximate equilibria. The construction illustrates the technique the paper uses for both of its negative results: well-chosen piecewise-linear pieces make an agent buy a segment wholly or not at all, depending on how prices compare, which gives the equilibrium problem a discrete character.
The result is proved in the paper. To our knowledge no part of it has been machine-checked. This mission formalizes the reduction's correctness at full strength, including the approximate version, which requires quantitative control of clearing errors that the exact version does not.
The direction "exact cover ⇒ equilibrium" is an explicit verification: prescribed prices and an allocation, and a check that every bundle is optimal, which for separable piecewise-linear utilities is a bang-per-buck comparison. The converse is the substantial part. An arbitrary approximate equilibrium must be shown to have the rigid price structure — every price in , good at , unused sets at — before a counting argument on agent 's savings forces . Each step is an excess-demand argument in which the error times the supply must be compared with quantities of order ; this is where and the exponent enter, and why the approximate statement does not follow from the exact one. Optimality of bundles is a statement about all affordable bundles, so each claim needs the structure of optimal bundles under piecewise-linear concave utility, which is not in Mathlib.
Lean namespace PLCMarkets.ExactCover. Market data (endowments, slopes, lengths) are rationals; prices and allocations are reals. Goods and agents of are small inductive types named as in the paper; indices are 0-based. Supplies are not normalized to , so clearing is ; prices are normalized to the simplex in both equilibrium notions, as in the proof of Lemma 8.3. The family is indexed and may repeat a set; exact cover and the disjointness of count indices.
Standing hypotheses of every theorem: each has three elements, , , — the paper's own "without loss of generality" assumptions (p. 10:19). Two conventions depart from the printed page, both necessary and both disclosed on the items:
Trivializing encodings are excluded: optimality of bundles is part of both equilibrium notions (without it the endowment itself clears every market), clearing is relative and per good, and the goal quantifies only over and , with an explicit function of .
Out of scope: the complexity-class statement "NP-complete" and NP membership (which comes from the rationality theorems of the companion mission); polynomial-time computability of the construction and string encodings of markets; and the Fisher market of §8, whose half of Lemmas 8.2 and 8.3 is a natural follow-up. Reusable infrastructure: piecewise-linear concave utilities, Arrow–Debreu markets with exact and approximate equilibria, and bang-per-buck characterizations of optimal bundles. Contributions proving that characterization as a standalone lemma are welcome.
A Fisher market is the simplest model of a market in which prices are set by supply and demand: buyers bring money, sellers bring goods, and a price vector is an equilibrium when every buyer, spending her money optimally at those prices, leaves every good exactly sold out. Computing equilibria is one of the central questions of algorithmic game theory, because a polynomial-time algorithm is what would make the equilibrium concept usable as a prediction or as a pricing mechanism.
For linear utilities an equilibrium always exists, is rational, and can be computed in polynomial time (Eisenberg and Gale 1959; Devanur, Papadimitriou, Saberi and Vazirani, J. ACM 2008, https://doi.org/10.1145/1411509.1411512). The next natural class, additively separable, piecewise-linear, concave utilities, captures diminishing marginal utility and is the class studied by Vazirani and Yannakakis (J. ACM 58(3), Article 10, 2011, https://doi.org/10.1145/1970392.1970394). Their paper shows that equilibria in this class are hard to compute (PPAD-complete) and that deciding whether one exists is NP-complete. Both results rest on a structural fact proved first: whenever such a market has an equilibrium at all, it has one whose prices are rational numbers of polynomial bit length. That fact is the subject of this mission.
Timeline:
There are buyers and divisible goods , one unit of each good. Buyer has a rational budget . For each buyer and good a function gives the utility that derives from an amount of good . It is piecewise linear and concave: it is given by a finite list of bounded segments with rational amounts , followed by a last, unbounded segment, with rational slopes . The function has slope on and slope afterwards. Buyer 's utility for a bundle is additively separable:
Given prices , a bundle is optimal for buyer if and no bundle with has . The prices are equilibrium prices if there is an allocation that gives each buyer an optimal bundle and sells every good exactly: for every .
The bit size of a rational number in lowest terms is the binary length of plus that of . The encoding size of a market is plus the bit sizes of all budgets, slopes and amounts, plus the number of bounded segments.
For the intermediate results, fix positive prices . The bang per buck of a segment of good is and its value is (infinite for an unbounded segment). Sorting buyer 's segments by decreasing bang per buck into classes of equal bang per buck, the first class at which the cumulative value exceeds is her flexible class. Segments of strictly larger bang per buck are forced, the others undesirable. From these the paper defines (value of the forced segments), , (the part of good not taken by forced segments), and a network from a source through goods and buyers to a sink.
There is a polynomial such that for every Fisher market as above,
The polynomial is fixed before the market. Nothing beyond the existence of some real equilibrium is assumed.
The result is what makes the existence problem for these markets a problem in NP: a rational equilibrium of polynomial size is a certificate that can be checked, with Lemma 3.1, by one max-flow computation. The same rationality statement underlies the paper's PPAD-membership proof and its NP-completeness result for existence. It also marks the boundary with markets whose equilibria can be irrational, as happens for some non-separable utilities. In that sense it shows that separable piecewise-linear concave utilities keep the "linear" character of the problem even though computing an equilibrium becomes hard.
All three statements are proved in the source, and none of them has a machine-checked proof on the platform or, as far as is known, anywhere else. The mission produces the first formal account of piecewise-linear Fisher markets: the model, the forced/flexible/undesirable classification of segments, the max-flow test for equilibrium, and the linear program of §4. It also forces precision where the paper is informal. The §4 bang-per-buck inequalities are printed with their directions reversed, and the claim about optimal LP solutions needs positive prices. The formal statements record each of these choices.
The obvious argument is: "equilibria are solutions of a linear system, so a rational one exists". It fails as stated, because the set of equilibrium prices is not a polyhedron. Which segments a buyer buys depends on the prices themselves, through the ordering of the ratios , so the equilibrium conditions are a finite union of polyhedral pieces glued along the price-dependent ordering. The work is to freeze the combinatorial structure of one given equilibrium and to show that the resulting fixed linear program still certifies equilibrium at every one of its optimal points. That second step is what Lemma 3.1 is for. The polynomial bit bound then needs a quantitative bound on the vertices of a rational LP, uniform in the market's encoding.
Buyers and goods are Fin n and Fin g. Budgets, slopes and amounts are rationals (ℚ). Prices and allocations are reals (ℝ), so that "admits rational prices" is a real conclusion: the goal returns q : Fin g → ℚ whose cast is an equilibrium. The committed conventions are:
(slope, amount) pairs of bounded segments together with the slope of its last, unbounded segment ("the last (infinite) segment", §6), with nonnegative slopes, positive amounts and nonincreasing slopes, stored inside the market structure;Hypotheses added relative to the page, each disclosed in its statement:
The §2 condition on p. 10:7 is a sufficient condition for existence and is deliberately not a hypothesis of the goal, which assumes only that an equilibrium exists. Complexity-class statements ("in NP", "PPAD-complete") are out of scope. What is formalized is the explicit polynomial bit bound, with a polynomial chosen before the market. A goal with the polynomial chosen after the market, an encoding size that ignores the bits of the data, or an equilibrium notion without utility-maximizing bundles would be trivially satisfiable. The statements rule all three out.
Beyond this mission, a complete development needs LP theory with rational data: existence of optimal basic solutions and determinant bounds on their bit size. Existing platform results that may serve as substrate include SmaleNinth.exists_square_subsystem and SmaleNinth.abs_det_le_factorial_mul_pow. Contributions welcome: proofs of the milestones, a reusable bit-size theory for rational LP vertices, and the Arrow–Debreu analogue (Theorem 5.1).
The traveling salesman problem asks for a shortest closed route visiting every node of a weighted complete graph exactly once. It is NP-hard, so practitioners use fast heuristics, and the basic question about a heuristic is how far from optimal its tour can be. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case analysis of the simple constructive heuristics under the triangle inequality: nearest neighbor, the family of insertion methods, and several variants.
Insertion methods build a tour by growing it one node at a time. They are among the most widely used construction heuristics in practice and in textbooks, and they differ only in the rule that chooses which node to insert next: the nearest one, the cheapest one, the farthest one, a random one, or any other. This mission formalizes the paper's result that holds for the whole family at once, regardless of that rule: every insertion method produces a tour at most times longer than an optimal one (Theorem 3, p. 571).
Timeline. 1977: Rosenkrantz, Stearns and Lewis prove for every insertion method (Theorem 3), for nearest neighbor (Theorem 1), both from a shared counting lemma (Lemma 1), and the constant for nearest and cheapest insertion (Theorem 4). 1994: Bafna, Kalyanasundaram and Pruhs (Theoretical Computer Science 125, 1994) give instances on which some insertion methods reach ratio , so the logarithmic growth cannot be replaced by a constant for the family as a whole.
A traveling salesman graph with nodes consists of a finite node set with and a distance with , and for all nodes (the triangle inequality). A tour visits every node once and returns to its start; its length is the sum of its edge lengths, and OPTIMAL is the least length of a tour.
A subtour is a tour on a subset of the nodes; a single node is a tour without edges. Given a subtour and a node , TOUR is obtained by choosing an edge of minimizing
and replacing it by the edges and ; if is a single node , TOUR is the two-node tour . COST is the length of TOUR minus the length of .
An insertion method constructs subtours with a single node and for some node , . The final tour is the approximation, and INSERT denotes its length. No rule for choosing the is fixed, and ties between minimizing edges are broken arbitrarily.
Write for the logarithm to base 2 and for the least integer .
For every traveling salesman graph with nodes and every run of every insertion method,
The result. Theorem 3 is a guarantee for an entire class of algorithms rather than for one. Any rule for choosing the next node, including rules designed for speed or for empirical quality, inherits a worst-case ratio of from the insertion step alone. The rule matters only for improving on that: nearest and cheapest insertion achieve the constant (Theorem 4 and its corollary, the subject of the third mission of this series), while the logarithmic bound remains the best general statement for other rules, such as farthest or arbitrary insertion. Lemma 1 is reusable on its own: it converts "every node carries a charge bounded by half the optimum and by its distance to other nodes" into a logarithmic bound, and the same lemma yields the nearest neighbor bound of Theorem 1.
Formalizing it. The theorem has been proved since 1977; the work here is a machine-checked proof of the known argument together with a reusable library for subtours, insertion and insertion costs. The companion nearest neighbor bound (Theorem 1) is already on the platform as SupplyChainTheory.nearest_neighbor_bound (proved), and nearest insertion with constant 2 as SupplyChainTheory.nearest_insertion_bound; neither covers arbitrary insertion methods or states Lemma 1 separately.
The per-step facts are local: each insertion is cheap relative to a node already present (Lemma 2) and relative to OPTIMAL (3.12). The obvious way to combine them, adding up costs each at most OPTIMAL, gives only the ratio . The logarithm comes from a global counting argument over all nodes simultaneously (Lemma 1), in which OPTIMAL is compared with tours on nested subsets of nodes of doubling size, and the per-node charges must be matched against the edges of those tours. Formally, the delicate parts are the bookkeeping of subtours as they grow (that every earlier node lies on the current subtour, and that the insertion cost equals the length increase), the shortcutting of a tour to an arbitrary subset, and the ceiling-of-logarithm arithmetic.
Nodes are Fin n; a tour of all nodes is a permutation τ : Equiv.Perm (Fin n), and OPTIMAL is the minimum of the tour length over the finite, nonempty set of permutations. Subtours are duplicate-free lists of nodes, with closed length . TOUR is encoded as inserting at a list position whose resulting length is minimal among all positions; inserting at a position removes exactly one edge of and raises the length by exactly , so this is the paper's rule, with every tie-breaking allowed. COST is the minimum length increase over positions. The paper's 1-based subtour index is kept (, final). is Nat.clog 2 n. All quantities are real.
Conventions and deviations, each disclosed in the item statements:
The goal quantifies over every run: any choice of the inserted nodes and any minimizing insertion position. Adding a selection rule (nearest, cheapest) or fixing a tie-breaking would state a weaker, different theorem; restricting to instances with OPTIMAL or to a fixed small would trivialize it.
Reusable beyond this mission: the subtour and insertion library (closed length of a list, TOUR, COST, insertion runs) and Lemma 1, which also yields Theorem 1. Contributions welcome: proofs of the milestones, general lemmas about the closed length of List.insertIdx and of filtered lists, and a proof of Theorem 1 from this mission's Lemma 1.
In robust stochastic optimization a decision maker chooses a decision whose outcome depends on a random vector , but knows only the first two moments of : its mean vector and its covariance matrix . The decision is evaluated by its worst-case expected utility over every distribution consistent with those moments. This model is standard in portfolio selection, where estimated means and covariances are the usual inputs, and in pricing and inventory problems with mean-variance information. It goes back to Scarf's min-max newsvendor (1958) and the Chebyshev-type moment bounds of Bertsimas and Popescu (2005).
For a linear outcome , such as the return of a portfolio with weights , the robust objective is
an optimization over an infinite-dimensional set of -variate distributions. Popescu (2007) showed that this problem depends on and only through the scalar mean and variance . The multivariate robust problem then reduces to a univariate moment problem, and for many utilities to a parametric quadratic program. The reduction rests on one structural fact, the general projection property, which this mission formalizes.
Fix a dimension . A law on is a Borel probability measure on . For a vector and a real matrix , the mean-covariance class is the set of laws under which every coordinate has a finite second moment and
Writing means that the law of lies in . For the superscript is dropped: for real and , is the set of laws on with finite second moment, mean and variance .
For a vector , the -projection sends the law of to the law of the scalar , that is, to the pushforward of under . Write and . The matrix is positive semidefinite, , when for all (and is symmetric); denotes its positive semidefinite square root.
For every , every and every nonzero , the -projection maps into and onto :
The "into" half says every projected law has the right mean and variance. The "onto" half says that every univariate law with mean and variance , however heavy-tailed or irregular, is the law of for some . The degenerate case is included.
The result. Theorem 1 immediately yields Proposition 1 of the paper: for every objective ,
with minima in the wide sense of infima. The robust objective is therefore a function of alone, which makes every robust mean-covariance problem with a linear outcome a bicriteria mean-variance problem. The paper's later results use this: the two-point and one-point support properties, the parametric quadratic programming solution, and the portfolio applications (bonus schemes, value at risk). The projection property holds with no assumption on , so it serves non-concave, discontinuous and quantile-based objectives alike.
Formalizing it. The theorem is proved in the paper; no machine-checked version is known. The mission produces a formal definition of mean-covariance classes that treats integrability honestly, a proof of the projection property, and through it a formally verified reduction of multivariate moment-robust problems to univariate ones. The paper's own construction of the lifted vector has a gap (see Difficulty), so a formal proof also records a corrected argument.
The into half is a computation with linearity of expectation. The difficulty is entirely in the onto half. Given an arbitrary univariate law with prescribed mean and variance, one must build an -variate law with a prescribed full covariance matrix whose one-dimensional marginal in direction is exactly the given law. This is a coupling problem: the obvious approach, taking independent coordinates, fixes the marginal in direction as a convolution and cannot reproduce an arbitrary target. Taking supported on the line through in a single direction reproduces the target law but has a rank-one covariance and fails whenever has rank above one.
The paper's appendix constructs the lift through conditional distributions of the remaining coordinates given the projected one. As printed, the conditional second-moment requirement it imposes cannot hold for unbounded targets, so that argument does not go through verbatim. The milestone for the lift states only the claim, not the printed construction.
The integrability bookkeeping is real work: every intermediate law must be shown to have finite second moments before its moments can be computed.
EuclideanSpace ℝ (Fin n) with its Borel σ-algebra; is the inner product ; is x.ofLp ⬝ᵥ S *ᵥ x.ofLp, where the matrix is named S (the symbol Σ is reserved in Lean).MemLp … 2), so that means and covariances are genuine integrals, not the default value that Lean assigns to non-integrable functions. The univariate class is parametrized by the variance , not by .P.map (fun R => ⟪x, R⟫) under a continuous map. "Pathwise" identities in the paper become equalities of pushforward laws, or pointwise algebraic identities.CFC.sqrt S, acting through Matrix.toEuclideanCLM, as in Mathlib's multivariateGaussian.Set.MapsTo ∧ Set.SurjOn with both classes explicit. Its only hypotheses are and , as in the paper. No bound on , no invertibility of and no positivity of is assumed. Restricting the target to Gaussian, bounded or finitely supported laws, or dropping the finite-second-moment clause (which would admit Cauchy laws as "mean 0, variance 0"), would trivialize or change the theorem and is ruled out.Needed infrastructure: moments of pushforwards under linear and affine maps, a covariance calculus for coordinates of random vectors, and a coupling that realizes the isotropic lift. Mathlib's multivariateGaussian, stdGaussian and CFC.sqrt are available. A reusable lemma "the covariance of is " would serve beyond this mission. Related platform work on moment-based ambiguity sets: Wasserstein Distributionally Robust Optimization II. Contributions of any milestone, and alternative proofs of the lift, are welcome.
Stochastic approximation finds a root of an unknown map from noisy evaluations , by the Robbins–Monro recursion . It underlies stochastic gradient descent, recursive estimation in statistics, adaptive control and simulation-based optimization. The classical theory (Sacks 1958) shows that the fastest attainable rate, with and the noise covariance, is achieved by the matrix step , which requires knowing .
Polyak and Juditsky (SIAM J. Control Optim. 30 (1992) 838–855) proved that the same optimal covariance is attained without any knowledge of : run the recursion with scalar steps that decrease more slowly than and output the running average of the iterates. Ruppert (Cornell ORIE technical report, 1988) obtained the one-dimensional case independently. The method, known as Polyak–Ruppert averaging, is the standard device for variance reduction in stochastic approximation.
Timeline:
Let be a filtered probability space and an adapted -valued noise process. Given a nonrandom and step sizes , algorithm (7) is
The error is and the estimation error is .
The hypotheses are:
The linear case, algorithm (2), is with every eigenvalue of having positive real part.
Under Assumptions 3.1–3.4,
Theorem 2 shows that averaging turns a robust, slowly-stepped recursion into an asymptotically efficient estimator. The covariance is the lower bound for this class of problems: for linear recursive estimates with independent noise it is the bound of [26] in the paper. Downstream, the result is what is invoked for the asymptotic efficiency of averaged stochastic gradient descent (Theorem 3 of the paper) and of recursive M-estimators in regression (Theorem 4).
The result is proved, with a published proof, but has no machine-checked version. As far as a search of the platform shows, no statement of Theorem 1 or Theorem 2 exists on Prove2Me. The platform does have a scalar martingale central limit theorem (Martingale.clt_of_mds, proved, with unconditional Lindeberg condition), which is usable through the Cramér–Wold device. Formalizing Theorem 2 also requires the Robbins–Siegmund almost-supermartingale theorem, a multivariate CLT for martingale differences under conditional Lindeberg and conditional covariance conditions, and the Kronecker lemma. Mathlib has none of these three in the required form, and each is reusable well beyond this mission. Non-asymptotic SGD rates already on the platform (the Bottou–Curtis–Nocedal and Lan missions) are different results.
The obvious approach analyses directly. It fails: with steps decreasing more slowly than , diverges, and only the average has the rate. The average must be compared with the averaged noise through the matrix sums of Lemma 1, whose bounds are uniform in both indices. Those bounds rely on the step condition in a quantitative way.
The nonlinear case adds a second difficulty. The iterates are first shown to converge almost surely, by a Lyapunov argument. The nonlinear error is then transferred to a linearised process at the scale, which needs a summability estimate on obtained through stopping times. A central limit theorem for the linear process alone does not give the result, because the linearisation error must vanish after multiplication by .
Points are in EuclideanSpace ℝ (Fin N) and matrices are Matrix (Fin N) (Fin N) ℝ, acting through Matrix.toEuclideanLin. Matrix norms are operator norms. Conditional expectations are MeasureTheory.condExp on a Filtration ℕ. "Given " is written with shifted indices ( given ). The algorithm is a recursive definition from , with unused and averaging . Convergence in distribution is TendstoInDistribution to multivariateGaussian 0 V. Convergence of conditional covariances in probability is entrywise TendstoInMeasure. A limsup or supremum "tending to 0 in probability" is unfolded into its – definition.
Corrections of the printed text, each used by the paper's own proof:
Several formalizations would make the goal trivial, and all are ruled out:
Welcome contributions: the Robbins–Siegmund theorem, a vector martingale CLT under conditional Lindeberg conditions, the Kronecker lemma, and the matrix estimates of Lemma 1.
The edit distance between two strings is the least total cost of a sequence of single-character insertions, deletions and replacements turning one string into the other. It is the basic similarity measure of spelling correction, file comparison and biological sequence alignment. Wagner and Fischer (JACM 1974) showed that it can be computed by filling a matrix in time. Masek and Paterson (J. Comput. System Sci. 1980) gave the first asymptotic improvement: for a finite alphabet and edit costs that are integral multiples of a common constant, the edit distance can be computed in time , that is for two strings of length .
Timeline:
Let be an alphabet and the null string. For a string , is its length, its -th character, and , with .
An edit operation is a pair of strings of length at most one: a replacement (, possibly ), a deletion () or an insertion (). results from via if and . An edit sequence takes to if there are strings with via . A cost function assigns a nonnegative real to every edit operation, , and
Write , , , and for the entries of the edit matrix. The cost function is normalized if for every edit operation.
A step is a difference of two adjacent matrix entries, (vertical) or (horizontal). The cost set is , and is discrete if every element of is an integral multiple of one constant .
Algorithm Y takes two strings of length and two step vectors of length (the left column and top row of an block) and fills a matrix of vertical steps and of horizontal steps by the recurrence of Corollary 1, returning the right column and bottom row . Algorithm Z cuts and into blocks of length , starts from the deletion costs of and the insertion costs of , obtains the steps of each block from Algorithm Y's output ("Fetch"), and returns the sum of the steps along the left column and the bottom row.
For a finite alphabet and a nonnegative, normalized cost function with discrete , there is a finite set such that for all and all with , ,
is fixed before , and . The second clause says that Algorithm Y's table need only range over , whose size does not depend on the strings; this is what the running-time bound rests on.
The result was the first algorithm for edit distance faster than quadratic, and its method (tabulate every possible small block of a dynamic program, described by differences rather than values) became the standard way of shaving a logarithmic factor from string dynamic programs. The discreteness hypothesis is where the method's power ends: Section 4 of the paper shows that with costs and the number of distinct steps grows without bound.
The results are proved in the paper; none of them is formalized. The Mathlib revision of this mission contains no edit-distance module. A formalization produces a definition of edit distance as a minimum over edit sequences, a machine-checked proof of the Wagner–Fischer recurrence for that definition under the normalization the paper assumes, and a checked proof that the four-Russians block assembly is correct and draws on a finite, string-independent table.
The hardest step is Theorem 2 for defined as a minimum over arbitrary edit sequences. An edit sequence may insert a character and later replace or delete it, or edit the same position many times, so the edit matrix's three-term recurrence does not follow by looking at the last operation. The upper bound is direct; the lower bound needs a normal form for edit sequences, and it fails without normalization: with , and all insertions and deletions costing , while the recurrence gives .
The goal is then an induction over blocks that must keep track of which matrix entries each block's input and output vectors represent, with block boundaries at multiples of and the first row and column handled by Theorem 1.
Strings are List α; characters are 1-based in all statements, as in the paper ( is A[i-1]). An edit operation is a structure with two Option α fields, not both none. is sInf of the set of costs of edit sequences taking to (nonempty, and bounded below for ). Costs are real-valued with an explicit nonnegativity hypothesis. Normalization is a hypothesis on Theorems 1, 2, Corollary 1, the Algorithm Y lemma and the goal; Lemmas 3 and 4 hold without it. The finite alphabet is [Fintype α] on Lemma 4 and the goal; Lemma 3 is stated for arbitrary upper bounds , , which implies the paper's version with maxima. The paper's standing assumption serves only the running time and is dropped. Step vectors are functions on Fin m.
Pinned statements. The paper states a running time on a logarithmic-cost RAM; the goal formalizes the two facts that bound rests on, correctness and a finite table domain fixed before the strings. The RAM model, operation counts, the choice , the padding reduction for , and the edit-path recovery of Section 2.3 are not formalized. Algorithm Y's result is a function (blockY); the Store/Fetch memory is not modelled.
The edit distance must stay the minimum over edit sequences: defining it by the Wagner–Fischer recurrence would make Theorems 1 and 2 true by definition and reduce the goal to a comparison of two recurrences. Algorithms Y and Z are transcribed from the pseudo-code and never refer to .
Useful beyond this mission: the §1.1 definitions and Theorems 1–2 are a general edit-distance library (the second mission of this series defines the same objects). Contributions of lemmas about normal forms of edit sequences, the triangle inequality for , and attainment of the minimum are welcome.
A maximal independent set (MIS) of a graph is a set of pairwise non-adjacent vertices to which no further vertex can be added. Sequentially an MIS is found greedily in linear time, but the greedy scan is inherently serial. Whether an MIS can be computed by a fast parallel algorithm was a central question of parallel complexity in the early 1980s: Karp and Wigderson gave the first NC algorithm (STOC 1984), and Luby's paper, SIAM J. Comput. 15(4):1036–1053, 1986, gave a much simpler one. MIS is a subroutine of many parallel and distributed graph algorithms (colouring, matching, symmetry breaking), and Luby's randomized algorithm remains the standard one in distributed computing.
The paper's second contribution, the subject of this mission, is a general method for removing randomness: analyse the randomized algorithm under pairwise independence only, then realize pairwise independent random variables on a sample space of polynomial size and try every sample point in parallel. The same method, often attributed jointly to Luby (1986) and to Alon, Babai and Itai (J. Algorithms 7, 1986), became a standard tool of derandomization.
Let be a finite simple graph with vertices labelled . The algorithm keeps a set (initially empty) and the current graph , the subgraph of induced on (initially ). For the neighbourhood is . Each execution of the loop body selects an independent set , adds it to , and deletes from ; the loop runs while . Write for the degree of in , for the number of edges of before the -th execution, and .
Algorithm B's select step draws a coin for each vertex, with , puts , and removes from the endpoint of smaller degree of every edge inside (both endpoints on a tie).
The sample space. Fix a prime with . The sample points are the pairs with , each of probability . With , the coin of vertex at is iff , so , and distinct coins are pairwise independent.
Algorithm D. Each execution of the loop body first moves the isolated vertices of into . Then:
No random bits are used.
For every graph on vertices, every prime with , and every run of Algorithm D (every tie-break among maximum-degree vertices and every maximizing sample point), the loop body is executed exactly times, with
and the output is a maximal independent set of .
The goal is the deterministic half of Luby's result: an MIS is computed in parallel rounds with no randomness, which places MIS in deterministic NC. The pairwise-independent analysis (Lemmas C, D, Theorems 2, 3) is the reusable part: it shows that the Monte Carlo algorithm's progress guarantee survives when mutual independence is weakened to pairwise independence, which is what makes a sample space of size sufficient. Lemmas 1 and 2 are the standard construction of pairwise independent variables with prescribed rational marginals.
All of these results are proved in the paper. None is formalized on the platform. A related but different object is the platform's dot-product hash family (AlmostLossless.pairwiseIndependent_dotHash), which has uniform marginals over a field and is not the -point matrix space with prescribed marginals . The companion mission A Simple Parallel Algorithm for the Maximal Independent Set Problem I formalizes Theorem 1, the mutually independent analysis of Algorithms A and B.
The obvious route to Theorem 2 repeats the proof of Lemma B, which lower-bounds by a product over independent events. Under pairwise independence the probability of an intersection of three or more coin events is not determined by the marginals, so that product argument fails, and the constant degrades from to .
The round bound needs a separate argument for high-degree vertices. The rounded probabilities are close to only when is large, which is why vertices of degree at least are handled by Case 1. Counting the Case 1 rounds uses the vertex count of the original graph, not of the current one. Correctness at termination requires an invariant linking , and across both kinds of rounds and the deletion of isolated vertices.
Vertices are Fin n with labels , which is §4.2's indexing of ; the label enters as a residue, and labels are distinct mod because . The current graph is the induced subgraph kept on the full vertex type, with deleted vertices isolated. One execution of the loop body is a relation between states that leaves the maximizing vertex (Case 1) and the maximizing sample point (Case 2) free, as the page does, and a run is any sequence of states starting at that follows the relation while . The goal asks for the first index with , so a statement about a later state or a bound on without termination does not meet it.
The conditions and are encoded exactly as and in . is natural-number division. The printed code tests , which puts residues in and contradicts stated on the same page; the formalization uses the strict test.
Lemmas C, D and Theorems 2, 3 quantify over every probability space carrying measurable, pairwise independent (IndepFun for each pair of distinct vertices) coins with the stated marginals at vertices of positive degree. Replacing pairwise by mutual independence, or fixing the probability space, would weaken them. They are stated for a fixed current graph, that is, as the expectation conditional on the state before the round, which is what their proofs establish. Expectations are Bochner integrals of a function with finitely many values and are therefore genuine. Lemma 2 carries the hypothesis , implicit on the page.
The development needs the induced subgraph and degree bookkeeping from Mathlib's SimpleGraph, pairwise independence from ProbabilityTheory.IndepFun, finite counting in ZMod q, and real logarithms. The pairwise-independent analysis (Lemma C to Theorem 3) and the sample-space lemmas are reusable beyond this mission. Contributions to any milestone are welcome.
Interior point methods for a linear program with follow the central path of the logarithmic barrier , where is the slack vector. Renegar's path-following analysis (1988) gives iterations, and for decades this was the best bound for methods whose iterations cost a linear system solve. Vaidya's volumetric barrier and the hybrid volumetric barriers of Vaidya and of Anstreicher (references [45] and [2] of the paper) reached iterations at the price of more expensive linear algebra. Nesterov and Nemirovski showed that a universal barrier gives iterations, but that barrier cannot be evaluated efficiently.
Lee and Sidford (FOCS 2014; full version arXiv:1312.6677) obtained iterations, each costing linear system solves, by following a weighted central path whose weights are recomputed from the slacks. The weights come from a weight function , defined as the minimizer of a regularized D-optimal-design problem. This mission is about that weight function and the theorem (Theorem 1 of the paper) certifying its properties. The companion mission, Path-Finding Methods for Linear Programming I, formalizes the path-following framework (Theorem 5 of §IV.C) that consumes these properties.
Fix with full column rank, , and . For vectors write , , , and . For a matrix let .
Projection matrix and slack sensitivity (Definition 2, p. 428). The projection matrix is , and the slack sensitivity is
Weight function (Definition 4, p. 428). A map is a weight function with constants if it is differentiable and, for every , with , the Jacobian of at , and :
The regularized objective (6), p. 429. For ,
At this is the D-optimal design problem, dual to computing the John ellipsoid of the polytope (§V.B).
With
the objective has a unique minimizer over for every , and the resulting is a weight function with
A supporting (non-milestone) item states the existence and uniqueness of the minimizer on its own.
The result. Theorem 1 is the input that turns the weighted path-following framework into an -iteration method: the framework needs -sized steps in (p. 428), and Theorem 1 makes that . The step consistency bound is what allows the weights to be recomputed after each Newton step without losing centrality. The same construction underlies later work on Lewis-weight barriers and on fast approximate John ellipsoids and maximum flow (§VIII of the paper).
Formalizing it. The theorem is proved in the full version of the paper (arXiv:1312.6677); the FOCS extended abstract contains no proofs. No part of it has a machine-checked proof. A complete formalization would give a verified account of leverage-score calculus (sums of leverage scores equal the rank; derivatives of projection matrices), of the convexity of for , and of differentiability of an argmin via the implicit function theorem, none of which is currently packaged in Mathlib in this form.
Size and slack sensitivity are statements about the minimizer, which is only characterized implicitly; they require precise matrix calculus for and a comparison between the matrices (which defines ) and (which defines ). The specific values of and matter here: the unregularized choice , makes the problem degenerate (p. 429).
The hard part is step consistency. The Jacobian of an argmin is available only implicitly, as the solution of a linear system obtained by differentiating the optimality condition. A bound on that depends on is easy to get and useless: the theorem needs the operator norm of in the -norm to be at most as soon as exceeds , and an bound with only an additive loss.
Existence and differentiability of the minimizer are conclusions, not hypotheses. The minimization is over an open orthant on which the objective is not obviously coercive or strictly convex for , and differentiability of requires the Hessian of at the minimizer to be invertible.
Vectors are Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; inverses are Matrix.inv, is Real.log (Matrix.det …), is Real.rpow, is Real.logb 2, the Jacobian is fderiv ℝ g s, and is Mathlib's sup norm on Fin m → ℝ.
Conventions and pinned hypotheses:
A.rank = n is assumed in every theorem. The paper never states it, but without it is singular and every formula is undefined (in Lean, Matrix.inv and Real.log would return junk ).Ruling out trivializations: the goal does not assume to be a weight function or to be differentiable, and it does not replace by an arbitrary weight function; differentiability is a conclusion (a predicate using fderiv without it would make step consistency hold vacuously wherever fails to be differentiable).
Useful infrastructure, reusable beyond this mission: leverage scores and their sum; derivatives of and of projection matrices; convexity of in (related to the published ConvexOptimization.log_det_concaveOn); differentiability of the argmin of a strictly convex smooth function. Contributions of these as separate theorems are welcome, as is a proof of any single bullet of Theorem 1.
Interior point methods solve a linear program by following a central path: a curve of minimizers of a penalized objective that trades off cost against distance from the boundary of the feasible region. The classical analysis of path following with the logarithmic barrier needs iterations for a program with constraints, where is the bit complexity of the input (Renegar 1988). For programs with many more constraints than variables, can be far larger than the dimension or the rank of the constraint matrix, and the factor is then the bottleneck.
Lee and Sidford (FOCS 2014) reduce the iteration count to by following a weighted central path in which each constraint carries its own positive weight, and the weights are re-computed as the algorithm moves. Their improved maximum-flow algorithm is an application of the same method.
Timeline. Karmarkar (1984) gave the first polynomial-time interior point method for linear programming. Renegar (1988) showed that path following with the logarithmic barrier needs iterations. Nesterov and Nemirovskii (1994) showed that a universal self-concordant barrier yields iterations, but that barrier is not known to be efficiently computable. Lee and Sidford (2014) achieved iterations, each reducible to linear-system solves.
This mission covers the first half of that framework (§IV of the paper): the weighted central path, the weighted Newton step, and the centering theorem that shows a single step followed by re-weighting makes constant-factor progress.
Let , , , and consider the linear program
The slack of a point is , and the interior is , the points with all slacks strictly positive. For a path parameter and a vector of positive weights , the weighted penalized objective is
A pair is feasible if and .
Write , and . The Newton step and the centrality are
The matrix is the Hessian of in , and is its gradient; exactly when minimizes .
For slacks and weights the projection matrix is and the slack sensitivity is
A weight function (Definition 4) is a differentiable map from slacks to weights with constants (size, a bound on ), (slack sensitivity, ), (step consistency, two inequalities on the Jacobian of that hold for every ), and uniformity .
Let be a weight function for with constants , let , , and
If , then and
The theorem is stated for every weight function, not for the specific one constructed in §V of the paper; that construction is the subject of a separate mission.
For feasible and , the split step , satisfies, whenever ,
with , and the new pair is feasible.
For feasible and :
Theorem 5 is the centering half of the weighted path-following method. Combined with Lemma 1, it shows that the path parameter can be doubled, while staying close to the weighted central path, in a number of steps of the form (5) controlled by , and . The paper then constructs (§V, Theorem 1) a weight function with , and logarithmic in , which yields the iteration bound. The theorem isolates exactly which properties of a weighting scheme are needed, so it applies to any weight function satisfying Definition 4.
The FOCS extended abstract states these results without proofs; the proofs are in the arXiv full version (arXiv:1312.6677). The results are proved on paper. No machine-checked formalization of weighted path following, or of the Lee–Sidford framework, is known. A formal proof would check the constants , , and as stated in the extended abstract, and would produce reusable Lean infrastructure for Newton steps of barrier functions with explicit matrix formulas.
The standard analysis of Newton's method on a self-concordant barrier gives quadratic convergence of centrality for a fixed barrier. Here the barrier changes during the step: the weights are reset to , so the new centrality is measured with respect to a different Hessian and a different gradient. The obvious argument, analysing the step at fixed weights and then treating the re-weighting as a small perturbation, does not give a contraction factor independent of : without control of how reacts to changes in the slacks, the re-weighting can undo the progress of the step. The step-consistency conditions of Definition 4 are the only hypotheses that control this reaction, and they are pointwise bounds on the Jacobian of , while the step moves the slacks by a finite amount.
Vectors are Fin n → ℝ and Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, and products are Matrix.mulVec and dotProduct. is the diagonal matrix of reciprocals, the diagonal matrices of , and . The Newton step and centrality are defined by the explicit formulas (3) and (4), not by derivatives of ; the centrality uses the Hessian-norm form of (4). The Jacobian is the Fréchet derivative fderiv ℝ g s, and is Mathlib's sup norm.
Conventions fixed where the paper is silent:
A.rank = n. The paper uses without comment; the inverse exists for positive slacks and weights exactly when has full column rank. Lean's matrix inverse is on singular matrices, which would make , and vanish and every statement trivially true; the rank hypothesis rules this trivializing reading out.Fin m (attained for , equal to for ).A complete development needs basic facts about weighted norms and the projection matrix , spectral comparison of the matrices for nearby slacks and weights, and calculus for vector-valued maps on the positive orthant. The weighted-norm and projection-matrix material is reusable for any interior point analysis. Proofs of the milestones, alternative arguments, and sharper constants are welcome.
A large engineering or construction project is a set of jobs with precedence constraints, and most jobs can be finished faster at a higher cost (overtime, more crews, faster equipment). Planners want to know, for every possible project duration, the cheapest way to meet it. The resulting trade-off between duration and direct cost is what management compares with overhead, penalties and market losses when it picks a schedule.
J. E. Kelley, Jr. and M. R. Walker introduced the critical-path method (CPM) in 1959, from work at du Pont and Remington Rand (Kelley and Walker 1959). Alongside the critical-path computation, they modelled each job's cost as a linear function of its duration and posed the choice of durations as a parametric linear program. They stated that its optimal value, as a function of the project duration , is a non-increasing, piecewise linear, convex function, which they called the project cost curve. The 1959 paper gives no proof and defers the detailed development to a separate paper (Kelley 1961). Fulkerson (1961) gave a network-flow algorithm that computes the curve. Time–cost trade-off analysis ("crashing") has been a standard part of project management since then.
A project network has events labelled with . Event is the origin and event the terminus. A finite set of jobs is given, each an ordered pair : an arrow from event to event . As in the paper, labels increase along arrows ( for every ), the origin precedes every event, and the terminus follows every event.
For job durations , the earliest event times are given by recursion (1):
and is the earliest project completion time.
Each job has a crash duration and a normal duration with , and a linear job cost with , . The project (direct) cost is
A schedule for is a pair with
Let be the set of for which a schedule exists. For the project cost curve is the minimum of (7) over schedules for . Write (all jobs crashed) and (all jobs normal).
Piecewise linear means finitely many breakpoints with , and affine pieces on and on . The goal fixes no breakpoints or slopes. It asserts only the shape the paper claims, on the whole of .
The cost curve is the output of CPM's cost analysis. Its convexity is what makes the paper's parametric procedure valid: jobs are expedited in order of increasing marginal cost, and the curve is traced from down to one linear piece at a time. Monotonicity justifies reading the curve as a trade-off. Piecewise linearity with finitely many pieces means the whole curve is determined by finitely many characteristic schedules, the vertices plotted in the paper's Fig. 3. The milestones identify the domain of the curve, show that it is well defined, and fix its right end at the all-normal solution.
These facts are classical: they follow from parametric linear programming, and Kelley (1961) and Fulkerson (1961) develop them in detail. No machine-checked proof of them is known. Prove2Me has a related result, LinearOptimization.lp_optimal_cost_convex_in_rhs (Bertsimas–Tsitsiklis, Theorem 5.1): convexity of the optimal cost of a standard-form LP in its right-hand side. It covers convexity only, for a different LP form, and says nothing about monotonicity or finitely many pieces. This mission adds a formal model of CPM's time–cost program and the full three-part shape theorem.
Convexity alone follows from the usual argument: a convex combination of optimal schedules for two durations is a schedule for the combined duration. Monotonicity needs the structure of the network: when increases, only the constraints (8) on jobs ending at the terminus loosen, because no job leaves the terminus. The hard part is piecewise linearity with finitely many pieces. Convexity does not imply it, and a general result on value functions of linear programs has to be tied to this specific program, whose right-hand side depends on only through . The domain is also unbounded, so the argument must show that the curve is eventually a single affine (in fact constant) piece. It cannot just produce finitely many pieces on a compact interval.
Events are Fin (n + 1) with origin 0 and terminus Fin.last n, and 1 ≤ n. Jobs are a Finset of ordered pairs, with at most one job per ordered pair. The standing assumptions of pp. 161–162 are fields of ProjectNetwork: labels increase along jobs, and reachability via Relation.ReflTransGen from the origin and to the terminus. Times and durations are real. Job data are functions Fin (n+1) → Fin (n+1) → ℝ, constrained and read only on . The hypotheses , and are fields of JobData. Recursion (1) is earliest, defined by well-founded recursion on the label. It uses a fallback value for an event without predecessors, which occurs only at the origin. The paper's is written lam. Constraint (9) fixes exactly, and the event times are otherwise unconstrained.
The goal takes with the hypothesis that is the least element of the set of costs of schedules for , for every . All three conclusions are stated on only. This rules out the trivializing formalizations:
The goal keeps , as the page does throughout §3, although monotonicity and convexity would hold without it.
Disclosed readings:
A complete development needs:
The one-variable notion IsPiecewiseLinearOn and the facts on earliest event times can be reused in scheduling missions. Proofs of the milestones, of any of the three goal conjuncts separately, and general lemmas on parametric LP value functions are all welcome.
Not formalized: general piecewise linear convex job costs (deferred by the paper to its references [7], [8]), and the primal–dual procedure itself (a method, not a claim).
The sample complexity of a learning problem is the number of labelled examples needed to learn to a prescribed accuracy with a prescribed confidence. In Valiant's probably approximately correct (PAC) model it is the basic quantity of statistical learning theory: it says how much data is necessary and sufficient, as a function of the complexity of the hypothesis class, when the target concept belongs to that class (the realizable case).
For a class of Vapnik–Chervonenkis (VC) dimension the answer was known up to a logarithmic factor for about 25 years:
Let be a set with a -algebra and . A classifier is a measurable map ; the concept space is a set of classifiers with . A finite sequence is shattered by if every labelling is realized by some ; the VC dimension is the largest such , assumed finite (then ).
A data set is a finite sequence of pairs in , and is the set of with for all . For a probability measure and a target , the error of is , where . A learning algorithm maps data sets to classifiers.
For , the sample complexity (Definition 1) is the least such that some algorithm satisfies, for every probability measure on and every , with independent with law ,
and if there is no such .
The learner of the paper uses three ingredients. A sample-consistent learner returns an element of whenever that set is nonempty. The majority vote is . The subsample algorithm returns if ; otherwise it splits into a head of points and three blocks of points, and returns the concatenation of , and . The learned classifier is .
The paper states Theorem 2 as with a numerical constant; its proof establishes the bound above with , and that explicit form is the goal. Improving the constant would give a stronger theorem; this statement stays valid.
Together with the classical lower bound, Theorem 2 gives : the realizable PAC sample complexity is determined up to a numerical constant by the VC dimension alone. It settles a question open since 1989, shows that the factor in the classical bounds is an artifact of empirical risk minimization rather than of the learning problem, and supplies an explicit, simple learner that attains the optimal rate. Later work on optimal learners (majority votes over bagged or subsampled ERMs, optimal learning in other settings) builds on this construction.
The result is proved on paper. To our knowledge no proof assistant contains it, and the formal libraries lack parts of its infrastructure: the classical bound for consistent learners (Lemma 4), multiplicative Chernoff bounds for empirical counts, and conditioning on independent parts of an i.i.d. sample. This mission produces a machine-checked statement of the optimal bound with the paper's explicit constant, a verified formal model of the learner, and reusable components for these three.
The obvious approach is to sharpen the analysis of a single consistent classifier, as in the classical bound. Decades of effort along these lines did not remove the factor, and the paper removes it only by aggregating many classifiers. The error of a majority vote is not controlled by the errors of its voters one at a time. The proof controls the probability that two voters trained on overlapping subsamples err at the same point, which requires tracking which parts of the sample are independent of which trained classifiers through a recursion of depth . In a formal development the difficult parts are the conditional-independence bookkeeping for random subsamples of a product measure, the induction over the sample size with a data set that varies with the level, and the numerical constants, which are tight (the key comparison is ).
Bool (true for ); data sets are lists and is concatenation; is a set of measurable functions with ; the VC dimension is a supremum in , assumed equal to a natural number . The i.i.d. sample is the product measure on . "With probability at least " is stated as a bound on the outer measure of the failure event. takes values in , so the goal is stated as , which is equivalent. Ties in the majority vote go to , as printed.An organization whose members hold private information faces two problems at once. The first is the team problem of Marschak and Radner: choose the rules by which members observe, communicate and decide so as to maximize the expected payoff of the organization as a whole (Marschak–Radner 1972). The second is the incentive problem: a member who is paid by their own results has no reason to follow those rules, and in particular no reason to report truthfully what they have observed. Theodore Groves' Incentives in Teams (Econometrica 41(4), 1973) connected the two. For a decentralized firm in which subunits report to a head, it exhibits compensation rules that make the team-optimal behaviour, truthful messages included, each subunit manager's unique best reply.
The construction is the origin of what is now called the Groves scheme, and with Vickrey's second-price auction (Vickrey 1961) and Clarke's pivot rule (Clarke 1971) it forms the Vickrey–Clarke–Groves (VCG) family of mechanisms.
Timeline:
The organization consists of a head (component ) and finitely many subunits . Each component has its own random component state , and the components are independent: the state of the environment is distributed according to the product law (Condition S.2).
Every member plays a strategy made of an observation strategy on its own state, a message strategy and a decision strategy (Condition S.3). Communication runs only between the head and each subunit, in one exchange: the head observes and sends to subunit ; the subunit, with information , sends back ; the head's information is (3.1). Decisions are and .
The organization payoff is a sum of components (Condition S.4),
and . Each accrues directly to subunit (Condition S.5). Strategy sets are given; denotes with subunit 's strategy replaced by . Two strategies are equivalent if for every .
Assumption A requires a maximizing over such that, for each subunit, whenever is not equivalent to .
An incentive structure pays subunit the amount . The class (3.2) consists of those of the form : own payoff plus a compensation computed from the head's information only. is optimal (2.6) if maximizes over , uniquely up to equivalence.
With , the sum running over all components other than and the expectation taken under (3.3), the structure lies in and satisfies, for every subunit and every ,
It holds for every satisfying Assumption A, all strategy sets and all constants .
Theorem 1 shows that a head who knows only the messages it receives can nonetheless align every subunit's interest with the organization's, without monitoring decisions or observations. It is an early statement that expected-externality payments make truthful communication an equilibrium of a decentralized organization, and the Bayesian, team-theoretic counterpart of the dominant-strategy results of Vickrey and Clarke. Its structure (own payoff plus a transfer depending only on the others' reported information) is the template later characterized by Green and Laffont and generalized by d'Aspremont and Gérard-Varet.
Theorem 1 is proved in the paper; nothing here is open mathematically. What the mission adds is a machine-checked version with every modelling choice explicit: how information is generated by the message protocol, what the conditional expectation in (3.3) means on events of probability zero, and which equivalence "uniquely" refers to. No machine-checked proof of Theorem 1 is known to the platform. The platform's AGT.vcg_incentive_compatible treats the complete-information, direct-revelation analogue (deterministic valuations, dominant strategies), a different model with a different conclusion.
The tempting argument conditions on the head's information under and compares it with the head's information under a deviation. That comparison fails when a deviating subunit sends a message that never sends: the conditioning event then has probability zero under , and the conditional expectation of (3.3) is not determined by the joint law. A second obstacle is that the head's information under a deviation differs from the information under in every coordinate the deviation touches, while the compensation is computed as if were played; the statement to be proved compares expectations taken under two different joint strategies, and the one-exchange protocol makes the head's messages, and hence every subunit's information, depend on the head's own state. Treating these dependencies loosely either produces a circular definition of the information functions (as (3.1) is printed) or a statement that fails on events of probability zero.
Contributions welcome: proofs of the milestones, and reusable finite-probability facts (conditioning on product events, iterated expectation over a coordinate) stated for product weights.