Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
In many production and service settings a single resource is shared by several parties, each judging the outcome only by how its own work is treated. Multi-agent scheduling studies this situation. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) introduced the two-agent single-machine model in which two agents, A and B, each own a set of jobs and each minimize their own objective. Their paper treats two questions: the constrained problem, minimizing A's objective subject to a bound on B's, and the Pareto problem, describing every schedule that cannot be improved for one agent without hurting the other.
For the Pareto problem the first quantity of interest is the number of distinct trade-offs, because the natural way to compute the whole front is to solve the constrained problem repeatedly with a decreasing bound (the paper's scheme PP, Figure 4, p. 239). Enumeration of this kind is polynomial exactly when the number of nondominated pairs is polynomially bounded. This mission formalizes the paper's bound for the case where both agents minimize a maximum of regular cost functions (§11.1, pp. 239–240).
Agent A owns the jobs and agent B owns , with . Every job has a processing time . All jobs are available at time . A schedule is an ordering of all jobs; the machine processes them in that order from time without idle time, so the completion time of a job is the sum of the processing times of the jobs up to and including it.
Each A-job carries a cost function and each B-job a cost function , all nondecreasing (regular). The agents' objectives are the maximum costs
This covers the makespan and maximum lateness of each agent as special cases.
A schedule is nondominated if no schedule satisfies and with at least one inequality strict. The pair of a nondominated schedule is a nondominated pair, and the schedule corresponds to that pair. Write for the set of nondominated pairs. Different nondominated schedules can share a pair; the problem asks for , with one schedule per pair. Job precedes job in if comes before in the ordering.
The paper prints the bound . It is off by one: with , unit processing times and , the schedules AB and BA give the two nondominated pairs and . The goal states , the bound the printed argument supports once the first schedule is counted.
The bound places among the two-agent problems whose Pareto front has polynomially many points. Combined with the polynomial algorithm for the constrained problem (Theorem 4.1 of the same paper), it means the full front can be listed with polynomially many constrained solves. The structural content is an order statement: as the bound on agent B tightens along the front, B-jobs overtake A-jobs and never fall back, so each of the (A-job, B-job) pairs changes order at most once. The same question for other pairs of objectives is the subject of later work on multi-agent scheduling, collected in the monograph of Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal (Springer 2014).
The result is published but, to our knowledge, has no machine-checked proof. Formalizing it also fixes the printed off-by-one error in the statement. The overtaking lemmas are of independent use for other pairs of regular min-max objectives.
The obvious argument walks along the front and charges each step to one (A-job, B-job) pair that changes order. Two things must be secured. First, the charged pair must change order in a consistent direction; schedules corresponding to a pair are not unique, and nothing forces two arbitrary representatives of different pairs to agree on the order of the jobs they do not charge. Lemma 11.2 asserts that representatives can be chosen so that no B-job falls back behind an A-job, and establishing it requires control over every job pair simultaneously, not one at a time as in Lemma 11.1. Second, a step must change at least one order. The tempting proof looks at a B-job attaining and argues that the jobs it overtakes include an A-job; this fails for an arbitrary choice of that B-job, since another B-job with a flatter cost function can be the one that moves. Finally, the count of reversals bounds the number of steps, not the number of pairs; the first pair has to be added.
Jobs are Fin nA ⊕ Fin nB (Sum.inl h is , Sum.inr k is , 0-based). A schedule is a duplicate-free list containing every job, and completion times are prefix sums of processing times; this is the published sequence model MooreLateJobs.Shared.completionTime (Moore 1968), reused as a reference item. Processing times are real and nonnegative; costs are real-valued and Monotone; so that both maxima exist. Nondominance compares against all schedules of all jobs. Precedence compares first positions in the list.
The count is over pairs, , measured with Set.encard, so finiteness is part of the goal. Counting nondominated schedules instead would be a different and false statement: permuting jobs inside a block often leaves both maxima unchanged. The printed bound is replaced by and the reason is given in the goal's statement; stating a larger bound "to be safe" or the printed one would make the mission either weaker than the paper's argument or false. The scheme PP and the choice of in it are not formalized; they are the paper's computation device, not part of the theorem. In the exchange claim the paper's σ and σ̃ are schedules of consecutive pairs; the milestone states it for any two nondominated schedules with the two strict inequalities, which includes that case. Running times are not formalized.
A complete development needs elementary facts about completion times when one job is moved within a sequence, the simultaneous statement of Lemma 11.2, and a counting argument along the front. Contributions of reusable lemmas about job moves in the sequence model are welcome.
Multivariate multipoint evaluation asks for the values of one polynomial at points of . Kedlaya and Umans showed that this problem is equivalent to modular composition, the computation of for univariate polynomials, and that fast algorithms for it yield the fastest known algorithms for factoring univariate polynomials over finite fields (Kedlaya–Umans, Dagstuhl Seminar Proceedings 08381, 2008; journal version SIAM J. Comput. 40(6), 2011, doi:10.1137/08073408X). Modular composition is the bottleneck of the factoring algorithms of von zur Gathen and Shoup (1992) and Kaltofen and Shoup (1998), so a near-linear multipoint evaluation algorithm translates directly into a faster factoring algorithm.
The paper gives two such algorithms. Section 4 works over any ring and is not algebraic: it lifts the problem to the integers and reduces modulo many small primes. Section 6, the subject of this mission, gives an algebraic algorithm, using only ring operations, for fields of small characteristic. Its correctness rests on one identity, Lemma 6.1, which lets the evaluation of the -variate at a point be read off from the evaluation of a single univariate polynomial at a related point of an extension ring.
Let be a prime and a finite field of characteristic . Fix integers and . Let be a power of with (the paper takes the least such power), and let be a polynomial of degree that is irreducible over . Then:
Three maps connect the problem to :
In the Lean development these are K, R, h, ι (the inclusion ), sigma i (), E, S, sigmaInv i ( on ), gAlpha, phi, pi, gIter () and fStar, in the namespace KedlayaUmans.FrobeniusLift.
For every with degree at most in each variable and every ,
The result. Lemma 6.1 is the correctness half of Theorem 6.2: to evaluate at points one computes the lifts , evaluates the one univariate polynomial at all of them by fast univariate multipoint evaluation, and projects back with . Since univariate multipoint evaluation runs in nearly linear time, the identity turns a multivariate problem into a univariate one at the cost of the degree growth . Corollary 6.3 turns this into an operation count of for every , provided and the characteristic satisfies .
Formalizing it. The lemma is proved in the paper; no machine-checked version is known to exist. This mission states it for the objects exactly as constructed in Section 6 (an explicit interpolant for , the canonical-representative projection for ) and splits its proof into the five steps above. The definitions of the rings and , the Frobenius powers on a ring that is not a field, and the Kronecker substitution into a quotient ring are reusable for formalizing other uses of the Frobenius-lift technique, such as the Parvaresh–Vardy codes and their Guruswami–Rudra instantiation, which the paper names as the inspiration for this algorithm (§1.5, p. 6).
The obvious attempt is to treat as evaluation at and push it through . This fails: is a unit, not zero, so evaluation at does not factor through , and is not a ring homomorphism. The identity holds only because the polynomial is already reduced modulo , which requires both the degree bound and the fact that raising to the power does not raise the degree of modulo . The second fact depends on being fixed by and on . The equality further needs that does not kill the leading coefficient in , a ring with possible zero divisors. Finally, interpolation must happen in , not a field, which is possible only because the nodes lie in the subfield .
F with [Field F] [Fintype F] [CharP F p], a prime ([Fact p.Prime]). is a polynomial over ZMod p with [Fact (Irreducible P)]; is P.natDegree and is p ^ P.natDegree. is AdjoinRoot of mapped to F; is never assumed to be a field and is never assumed irreducible over F.m ^ 2 * d < h, which contains the paper's case. is a hypothesis.IsPrimitiveRoot η (h - 1), equivalent to generating since .∀ i, f.degreeOf i ≤ d - 1.Fin m, starting at ; substitutes for .Lagrange.basis over the field at the nodes , mapped into , with coefficients . is the remainder modulo (AdjoinRoot.modByMonicHom) evaluated at .A formalization that takes to be any element satisfying (6.2), or defines as a ring homomorphism, would make the goal trivial or false; both are ruled out because and are explicit definitions with no hypotheses attached, and (6.1) and (6.2) are milestones to be proved.
Infrastructure a full proof needs: the Frobenius on polynomial rings in characteristic (, cf. Mathlib's expand and map_frobenius_expand), Lagrange interpolation transported along a ring homomorphism from a field, degree bounds for MvPolynomial.eval₂, and reducedness of (from separability of over the perfect field ). Proofs of any milestone, and alternative arguments, are welcome.
Multivariate multipoint evaluation asks for the values of a polynomial over a ring , with individual degrees at most , at given points of . Kedlaya and Umans showed that, over finite fields and rings , this problem can be solved in time nearly linear in the input size , for (Kedlaya–Umans 2008, §4). Through their reduction of modular composition, the computation of , to multipoint evaluation (§3 of the same paper), this gives the first nearly-linear-time algorithm for modular composition over finite fields. That in turn gives the fastest known algorithms for factoring univariate polynomials over , with bit operations for a randomized algorithm on degree- polynomials (abstract and §8).
Timeline. Brent and Kung (1978) gave the baby-step/giant-step algorithm for modular composition (J. ACM 25). Huang and Pan (1997) improved the exponent using fast rectangular matrix multiplication. Kaltofen and Shoup (1998) introduced the factoring framework that the factoring application builds on (Math. Comp. 67). Kedlaya and Umans (2008, SIAM J. Comput. 2011) gave the multimodular algorithm formalized here, together with an algebraic algorithm for small characteristic.
Let and write for the integers modulo . Every element of has a lift, its representative in . For , replaces each coefficient by its lift; lifts a point coordinatewise.
Algorithm MULTIMODULAR with degree parameter and rounds takes (degree at most in each variable) and a point . It lists the primes at most , reduces and modulo each , and evaluates the reductions . It does this directly when , and by recursion with rounds otherwise. It then returns, reduced modulo , the unique integer in congruent to modulo every .
Let be monic of degree and . The lift of is its representative of degree at most , with coefficients lifted to , an element of . Put
Algorithm MULTIMODULAR-FOR-EXTENSION-RING runs in four steps.
For monic of degree , , , , every of degree at most in each variable, and every :
In the order the paper's proofs use them:
The result makes multivariate multipoint evaluation exact and fast over every finite ring of the form , which includes every finite field . Combined with the paper's reduction from modular composition (Theorem 3.1) it yields modular composition of degree- polynomials over in bit operations (§7). That is the step on which the paper's improvements to univariate polynomial factorization, irreducibility testing and minimal-polynomial computation rest (§§7–8). The same algorithm gives a data structure answering polynomial-evaluation queries in time polylogarithmic in the degree (§5).
The theorem is proved in the paper; nothing in it is open. As far as is known, no part of it has been machine-checked. This mission formalizes the correctness of both algorithms exactly as the paper defines them, step for step, including the Chinese-remainder recombination, the explicit prime threshold , and the base- digit recovery. Lemma 2.4 is an explicit Chebyshev-type lower bound on the primorial, valid for all , and is reusable independently of this mission.
The recursion itself is routine. Two points carry the content. The first is the explicit prime threshold: the algorithm uses only primes up to , so its correctness depends on the explicit inequality of Lemma 2.4 for every , not on an asymptotic prime-number estimate. The small cases are part of the claim. The second is the extension-ring step: the integer produced over must determine the polynomial exactly. That needs simultaneous control of its degree and of every coefficient, against the specific constants and . A bound on evaluated at a point does not by itself suffice.
Lean represents as ZMod r with (NeZero r, excluding ZMod 0 = ℤ), polynomials as MvPolynomial (Fin m) _ with variables indexed , and as AdjoinRoot E for a monic E with E.natDegree. "Degree at most in each variable" is ∀ i, f.degreeOf i ≤ d - 1. is the natural logarithm; the paper does not fix a base, and the natural log is the strongest reading of Lemma 2.4. The primes for real are the primes . Each algorithm is defined for a single evaluation point, since the paper processes the points independently. The leaf evaluates at directly; that value is what Theorem 4.1's FFT algorithm outputs. is as printed on p. 15; p. 16 prints .
The hypotheses and are not written in the paper but are needed. For , , the threshold is , no prime is used, and MULTIMODULAR returns . For the inequality and the degree bound both fail.
Only correctness is formalized. Every running-time bound in Theorems 4.1, 4.2, 4.4 and Corollaries 4.3, 4.5 is out of scope. The Chinese-remainder step and the digit step are defined from the residues and from alone: an algorithm that evaluates in and reduces it, or that computes in directly, would make the theorems trivial and is not the algorithm stated here.
Needed infrastructure: explicit primorial lower bounds (Mathlib has primorial and Chebyshev's ), the Chinese remainder theorem for several moduli (ZMod.prodEquivPi), bounds on evaluations of polynomials with nonnegative coefficients, and uniqueness of base- representations of polynomials. Lemma 2.4 and the base- uniqueness are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 2.4.
Large optimization problems often split into blocks owned by different agents (subsystems of a power grid, vehicles in a formation, scenarios of a stochastic program) that are coupled only through a few linear constraints. Distributed optimization methods solve such problems by letting each agent work on its own block and exchanging a small amount of information, typically a vector of prices for the coupling constraints. The classical method of this kind is dual decomposition (Everett 1963; Bertsekas and Tsitsiklis, Parallel and Distributed Computation, 1989): fix the prices, let every agent solve its own subproblem, then update the prices by a gradient or Newton step on the concave dual function. Dual decomposition is reliable for strictly convex problems but has no convergence guarantee for nonconvex ones.
Houska, Frasch and Diehl (SIAM J. Optim. 26 (2016)) proposed ALADIN (augmented Lagrangian based alternating direction inexact Newton), which adds a proximal term to the agents' subproblems and replaces the price update by a coupled equality-constrained quadratic program. ALADIN is used in distributed model predictive control and in power-system optimization. Remark 4.2 and Appendix A of the paper explain where it sits relative to the classical method: if the proximal term is switched off (), the price update of ALADIN is exactly a regularized Newton step of dual decomposition. Lemma 5 is the precise statement of that equivalence, and it is the goal of this mission.
The problem (1.1) has blocks :
with , twice continuously differentiable, and . One iteration of Algorithm 2 (ALADIN) starts from a primal point and prices and does the following.
and the new prices are .
On the dual-decomposition side, (A.3) is the gradient of the dual function at , and the (inexact) dual Newton step (A.4) with a symmetric negative semidefinite scaling matrix and step size is
where plays the role of a Levenberg–Marquardt regularization parameter.
Assume every strictly convex, every convex, of full row rank, positive definite, and . Then for every , with
the matrix is invertible and
The result. Lemma 5 places ALADIN on a known map. With it inherits the convergence theory of dual decomposition for strictly convex problems for small step sizes, independently of how crude the approximations , are, as long as . It also reinterprets the augmented-Lagrangian parameter as the inverse of a dual Levenberg–Marquardt parameter, and it isolates the proximal term as the only ingredient that distinguishes ALADIN from dual decomposition and makes the nonconvex analysis of the paper possible.
Formalizing it. The lemma is proved in the paper; to our knowledge no machine-checked proof exists. A formal proof certifies an identity whose printed form contains a typo (see below), and produces reusable linear-algebra facts: the closed-form solution of an equality-constrained strictly convex quadratic program via the reduced inverse , the semidefiniteness of , and the closed-form maximizer of a regularized concave quadratic.
The proof is a chain of exact eliminations, and the work is in carrying each one out without losing a sign or a hypothesis. The step most easily done wrong is the minimization over : the constraint couples the block coordinates, the minimizer is expressed through the inverse of (invertible only because has full row rank). A second trap is the sign convention for : it must agree with footnote 4 (), or the conclusion flips. The tempting shortcut of treating the max–min dual of (3.3) abstractly runs into the fact that strong duality and attainment are not free; working from the KKT system of (3.3) avoids that.
Vectors are Fin n → ℝ; blocks are indexed by Fin N; matrices are Mathlib Matrix over Fin index types; the gradient is the vector of partial derivatives computed with fderiv. The step-1 output is a local minimizer of the decoupled problem together with KKT multipliers (the paper assumes LICQ for the lower-level constraints). The QP (3.3) and enter through the KKT system of (3.3), not through a closed-form expression: defining or by the formula of the conclusion would make the goal true by definition and is ruled out. is the formula (A.3); that it is the gradient of the dual function is a cited fact the lemma does not use. The invertibility of is part of the conclusion, because Mathlib's matrix inverse returns on a singular matrix.
Correction of (A.6). As printed, (A.6) has the bracket . This is a typo for , as in (A.5) on the same page and as the explicit minimization over forces; with the printed bracket the identity fails already for , , , . The mission uses the corrected matrix and writes the pseudo-inverse as an inverse, which it is under the hypotheses.
The hypotheses of strict convexity of , convexity of and are kept as on the page although the identity does not use them. The related platform draft GoldfarbIdnani.DualQP.properties_2_6_to_2_9 (not proved) states properties of the same reduced inverse; it is not imported. Proofs of the four milestones and of the goal are welcome; the milestones are self-contained matrix and calculus facts and can be attacked independently.
Training a neural network with nonsmooth activations (ReLU, max-pooling, absolute values) means running a stochastic gradient method in which the "gradient" is whatever the automatic differentiation library returns. For nonsmooth programs that output is in general neither a gradient nor a Clarke subgradient: the chain rule fails for the Clarke subdifferential, and the same function written in two ways can receive two different derivatives at the same point. Bolte and Pauwels (TSE Working Paper 1044, 2019; published in Mathematical Programming, 2021) introduced conservative set-valued fields as a class of generalized derivatives that is closed under the operations automatic differentiation performs and still carries enough information to analyse descent methods.
The framework is used in the analysis of nonsmooth automatic differentiation and of stochastic subgradient methods in machine learning (for instance Bolte and Pauwels, NeurIPS 2020). The present mission formalizes the first structural theorem of the theory.
Write for Euclidean space with inner product . A set-valued map assigns to each a subset ; it has closed graph if is closed in . A path is absolutely continuous if it is differentiable almost everywhere and ; it is a loop if .
Definition 1. is a conservative field if it has closed graph, nonempty compact values, and for every absolutely continuous loop
The integrand is Lebesgue measurable (Lemma 1), so the condition is that circulations along loops vanish, as for gradient fields in classical vector calculus, but with a maximum over the set in place of a single vector.
Definition 2. A function is a potential for (and is a conservative field for ) if for every and every absolutely continuous path from to
Examples: the gradient of a function; the Clarke subdifferential of a semialgebraic locally Lipschitz function; the output of forward or reverse mode automatic differentiation on a program built from definable elementary functions (the subject of the companion mission in this series).
If is a conservative field and a (locally Lipschitz continuous) potential for , then for Lebesgue-almost every , is differentiable at and
The result. Theorem 1 says that a conservative field, although set-valued and possibly far from any subdifferential, differs from the gradient of its potential only on a Lebesgue-null set. Several consequences in the paper rest on it: the Clarke subdifferential of is contained in the convex hull of every conservative field for , so it is the minimal convex-valued conservative field (Corollary 1), and a Fermat rule at local extrema of (Proposition 1). Combined with the companion result that automatic differentiation produces conservative fields, it implies that the derivatives returned by automatic differentiation agree with the gradient outside a Lebesgue-null set.
Formalizing it. The theorem is proved in the paper; this mission formalizes the known proof. No conservative-field calculus exists in Mathlib or on the platform. The mission produces the definitions of conservative fields and potentials in Lean, a measurability result for marginal functions of closed-graph set-valued maps along absolutely continuous paths, and an almost-everywhere identification of measurable selections with gradients that can be reused for other "derivative equals selection almost everywhere" statements.
The obvious argument runs: is locally Lipschitz, hence differentiable almost everywhere by Rademacher's theorem, and at a point of differentiability must be . The second step fails. Conservativity is an integral condition along curves, and it says nothing about the value of at an individual point of differentiability; a pointwise argument cannot exclude extra elements of . The identification therefore holds only almost everywhere and has to be extracted from integral information, which brings in three ingredients absent from Mathlib: measurability of for closed-graph compact-valued maps with no local boundedness assumption; measurable selections of such maps, including a countable family dense in every value (a Castaing representation); and, for Remark 3(d), the local boundedness of conservative fields (Borwein, Moors and Wang). Passing from "almost every point of every line" to "almost every point of " also requires measurability of the exceptional set, which is not automatic.
is EuclideanSpace ℝ (Fin p), Lebesgue measure is volume, and a set-valued map is EuclideanSpace ℝ (Fin p) → Set (EuclideanSpace ℝ (Fin p)). A path is a function ℝ → ℝ^p satisfying AbsolutelyContinuousOnInterval γ 0 1 (Mathlib's – definition on , equivalent there to the paper's); its values outside are irrelevant and is deriv γ. The maximum and minimum over are sSup and sInf of the image of a nonempty compact set, hence attained.
Since Lean's integral of a non-integrable function is , Definitions 1 and 2 require the circulation to be integrable in addition to having the stated integral; without this conjunct every field with non-integrable circulations would count as conservative, which is a trivializing reading excluded here. Likewise "" is formalized as differentiability of at together with set equality , because Lean's gradient is where is not differentiable. Definition 2 is the paper's form (2) with base point ; the min-form and the forms (3)–(4) are consequences, not definitions. Measurable selections appear as hypotheses (Borel measurable with ); their existence is not claimed by any milestone. The local Lipschitz hypothesis of Theorem 1 is kept as printed, and local (not global) Lipschitz continuity is used throughout.
Theorem numbers and pages refer to the TSE Working Paper 1044 version (October 2019), not to the Mathematical Programming typesetting.
Welcome contributions: a Castaing representation / Kuratowski–Ryll-Nardzewski selection theorem for closed-graph compact-valued maps on ; Rademacher's theorem for locally Lipschitz functions; Fubini-type "null on every line implies null" lemmas on EuclideanSpace; the fundamental theorem of calculus for absolutely continuous vector-valued paths.
Online covering models decisions that must be made as requirements arrive. A planner knows the cost of each available resource, but learns the requirements one at a time and cannot undo an allocation already made. This occurs, for example, when requests for network service or elements needing coverage appear over time. The central question is how much more an online fractional allocation can cost than a best allocation chosen after all requirements are known. Buchbinder and Naor study this question through a paired covering and packing linear program and give an online scheme for arbitrary nonnegative constraint coefficients, not only incidence coefficients in (Buchbinder and Naor, 2009, §§2–4).
The result targeted here is Theorem 4.1 of that paper. It concerns the fractional covering scheme of §4, before the separate extension to box constraints in §4.1. The theorem is a statement about the particular phased scheme, so the scheme's state and update rule form part of the mathematical setting. The online requirement also matters: after each new constraint, earlier allocations remain in force (Buchbinder and Naor, 2009, pp. 4, 8).
Let be a finite nonempty set of primal variables and let index constraints in arrival order. The known cost of variable is . Constraint has coefficient for variable ; when it arrives, the online algorithm learns its coefficients. The normalized offline covering problem minimizes over subject to for every constraint considered. Its packing dual maximizes over subject to for each . The finite data and sign conventions are those of Figure 1 (Buchbinder and Naor, 2009, pp. 3–4).
The scheme accepts a parameter and asks for coverage only to . It maintains a sequence of phases. The first phase bound is times the least ratio among the positive coefficients of the first constraint. The bound doubles at a restart. Within a phase, the vector begins at zero, the initial primal allocation is , and the allocation subsequently follows the exponential expression on page 8. The current phase may need to process constraints already seen in earlier phases. Old phase vectors are retained: the actual online allocation is the coordinatewise maximum of the current and all finished phase vectors. Thus resetting a phase does not retract an earlier allocation (Buchbinder and Naor, 2009, p. 8).
For every nonempty arrival prefix of length , a run of the phased scheme exists. Every completed run has output satisfying
and, for every nonnegative offline comparison vector satisfying for each ,
The paper states the ratio as . Its closing display on page 9 yields the explicit factor used here. The benchmark uses the unscaled covering constraints of Figure 1; replacing them with constraints at would change the guarantee (Buchbinder and Naor, 2009, Theorem 4.1 and proof, pp. 8–9).
The milestone list follows the four claims printed under Theorem 4.1. A finished phase has dual objective at least ; every phase dual vector satisfies the packing constraints; the sum of phase primal costs through the current phase is less than ; and the actual allocation covers every arrived constraint to . These are statements about the phase records of the scheme, including a partly processed round that ends in a restart (Buchbinder and Naor, 2009, pp. 8–9).
The theorem gives a cost guarantee for a general online covering problem while allowing arbitrary nonnegative coefficients. It separates the cost paid by an allocation from the level of coverage requested through . Its four claims identify the quantities that make the guarantee meaningful: the dual vector certifies a lower bound for an offline comparison, the phase costs control the online expenditure, and the output remains feasible as constraints arrive. The same primal–dual setting is used elsewhere in the paper for online packing and for applications of covering and packing methods (Buchbinder and Naor, 2009, §§3–5).
The paper proves Theorem 4.1. This mission asks for a machine-checked account of the known result and of the scheme to which it applies. A published formal restatement, OnlinePrimalDual.GeneralPacking.theorem14_3, already gives a ratio conclusion under an assumed ratio bound and an assumed weak-duality inequality; those hypotheses contain the main work needed here. The present goal instead quantifies over runs generated by the update rule and asks both that a run exists and that all such runs satisfy the guarantees. The published general instance definition is reused, so the finite covering and packing data have a shared interface.
An online allocation cannot be evaluated solely from its final vector. A phase restart resets the working dual vector and restarts the constraint scan, while allocations from completed phases still affect the actual output. A statement about arbitrary vectors with a presumed cost bound would leave out this behavior. The continuous update also requires a precise stopping event when coverage or the phase cost reaches its threshold. The cost guarantee is sensitive to which condition wins if both occur together, and to whether a phase can restart indefinitely. Those details must be represented before any claim about completed phases has the paper's meaning (Buchbinder and Naor, 2009, pp. 8–9).
Lean uses OnlinePrimalDual.GeneralPacking.GeneralInstance I (Fin m) for the coefficient matrix and costs. A nonempty finite type represents the primal variables; Fin m supplies the ordered constraints. The theorem assumes , , and a positive coefficient in every constraint. The last condition makes each arriving constraint coverable and makes the first ratio minimum nonempty; zero coefficients are omitted from that minimum. The paper treats infeasible all-zero rows implicitly. The minimum is over a finite nonempty set, so the real infimum in the Lean definition equals the ordinary minimum. All sums are finite and all logarithms are natural.
The run is an event relation with three events: arrival of one new constraint after all known constraints have been processed, completion of a covered round at its first stopping time, and restart at the cost cap while coverage remains deficient. A restart doubles , records the old phase, resets the dual variables, and resumes at the first known constraint. The state records the current phase and all finished phases; the output takes their coordinatewise maximum. A simultaneous coverage and cost event counts as covered. Reaching the cost cap models the continuous stopping time behind the paper's wording that the cost “exceeds” the bound. The theorem asserts run existence, so a ratio claim cannot hold merely because the run relation has no witness.
The explicit instantiation in this mission is , from the page 9 closing display. The first-phase case is bounded there by times the optimum and is included in the same stated coefficient. The comparison vector must satisfy the original level-one constraints. Theorem 4.2, which adds upper bounds on variables and appears in §4.1, is outside this mission. The run definition, phase-cost and coverage functions, and the four claims are reusable infrastructure for later work on continuous online primal–dual schemes.
Classical scheduling theory optimizes one objective for one decision maker. Many shop floors are shared: two departments, two customers or two firms submit jobs to the same machine, and each cares only about how its own jobs are treated. Agnetis, Mirchandani, Pacciarelli and Pacifici, Scheduling Problems with Two Competing Agents (Operations Research 52(2), 2004), set up this two-agent scheduling model and classified the complexity of its single-machine cases for the standard objectives (maximum of regular cost functions, number of late jobs, total weighted completion time). The paper started a line of research on multi-agent scheduling; its notation is the standard one in that literature.
This mission covers the paper's first case, §4: both agents measure a schedule by the largest cost among their own jobs. It is the case with a polynomial greedy algorithm, and it serves as the template for the paper's other cases.
Agent A owns jobs and agent B owns jobs . Each job has a processing time ; all jobs are available at time . A schedule is an ordering of all jobs, processed on one machine one after another from time without idle time, so the completion time is the sum of the processing times of and the jobs before it. Each A-job has a nondecreasing cost function and each B-job a nondecreasing (the costs are regular). The two objectives are
The constrained optimization problem asks for a schedule minimizing among those with (the feasible schedules). A schedule is nondominated if no schedule has and with one inequality strict.
The backward rule of §4 builds a schedule from the end. With the set of unscheduled jobs and the time at which the next job placed will end, it places last any unscheduled B-job with ; if there is none, it places last an unscheduled A-job of least ; if neither exists, it stops and declares the instance infeasible.
The paper justifies the rule by a reduction to Lawler's single-agent problem (Lawler 1973): every job gets one cost with values in , equal to for A-jobs, to for a B-job meeting the bound at time and to for one violating it.
Both parts hold for every tie-breaking. The printed theorem states a running time ; only the correctness half is a target.
The theorem shows that the two-agent problem with maximum-cost objectives is no harder than its single-agent counterpart: a greedy rule that gives priority to any B-job still within budget and otherwise serves agent A's cheapest job is optimal. Theorem 4.2 turns this into a point of the Pareto frontier with one more optimization, without the binary search over that §3 of the paper describes for the general case. In §11 the paper enumerates nondominated pairs by repeatedly solving the constrained problem, and §11.1 bounds their number for this case.
None of these results has a machine-checked proof that we know of. The single-agent theorem of Lawler is the subject of the published Prove2Me statement LawlerPrec.MinMax.lawler_rule_optimal, which is open; its costs are real-valued, so it does not apply directly to the costs of the reduction. This mission's results are self-contained and can be proved either through such a generalization or directly.
The rule is nondeterministic: any eligible B-job may be chosen, and ties among A-jobs are broken arbitrarily, so the optimality claim is about every possible output, not one canonical sequence. Lawler's exchange argument has to be carried through the extended-real costs, where a B-job's cost jumps from to at its deadline, and the ordering by B-first priority has to be shown to be one of Lawler's least-cost choices. The completeness half needs that a stuck state (no A-job left and every remaining B-job over budget at ) rules out every schedule, not just the rule's.
Fin nA ⊕ Fin nB (Sum.inl h is , Sum.inr k is , 0-based). Schedules and completion times reuse the published definition MooreLateJobs.Shared.completionTime (Moore 1968): a duplicate-free list containing every job, processed from time without idle time.IsBackwardRuleSeq): at every position of the sequence, with the jobs at positions and the completion time at position , the job there is an eligible B-job if one exists in , and otherwise an A-job of least in . "Ties are broken arbitrarily" means the property admits every choice. "The rule stops" means no sequence through that state has the property, so "the rule completes" is the existence of a complete sequence with the property.EReal with only maximum and order; "1|prec|f_max" is taken with the empty precedence relation. "Finite objective value" means the minimum is a real number.The definitions (two-agent model, maximum costs, constrained problem, nondominance) are reusable by the rest of this series. Proofs of the milestones, and a generalization of Lawler's theorem to extended-real costs, are welcome.
Multi-agent scheduling studies a machine shared by parties with their own jobs and their own objectives. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) introduced the two-agent single-machine model: agents and each own a set of jobs, and the schedule must serve both. The paper frames this within multiagent systems, where agents negotiate the use of a common resource over time, and its schedules are meant to support that negotiation: either the best schedule for one agent given what the other accepts, or the whole set of nondominated (Pareto-optimal) schedules. The paper classifies the complexity of the constrained problems for the classical regular objectives.
One of its polynomial cases concerns the number of late jobs on both sides: agent accepts schedules in which at most of its jobs are late, and agent minimizes the number of its own late jobs. For a single agent, minimizing the number of late jobs is solved by Moore's algorithm (Moore 1968), and a dynamic program of the Lawler–Moore type over jobs in due-date order solves related weighted versions (Lawler & Moore 1969). §7 of the 2004 paper adapts that dynamic program to two agents by tracking the number of late jobs of each agent separately.
There are jobs , all available at time . Job has a processing time , a due date , and an owner, agent or agent . A schedule is a sequence of all jobs processed on one machine from time without idle time or preemption; the completion time of is the sum of the processing times of and the jobs before it. Job is late if and early otherwise. denotes the number of late jobs of agent .
Given an integer , the problem asks for a schedule with (a feasible schedule) minimizing . An instance may have no feasible schedule at all.
The jobs are numbered in earliest-due-date (EDD) order, . A partial schedule of is described by its set of early jobs: the jobs of run first, in EDD order, each completing by its due date, and the other jobs of count as late. The table is the minimum completion time of the last early job over partial schedules of with at most late -jobs and at most late -jobs, and if there is none. It is computed by , at a negative index, and
when belongs to (with in place of when belongs to ), where if and otherwise.
For a feasible instance with jobs in EDD order, for some , and
is the optimal value of : some feasible schedule has exactly late -jobs, and every feasible schedule has at least .
A feasible instance has an optimal schedule whose early jobs come first, in EDD order, and whose late jobs come last.
For : if is finite, it is the minimum, attained, of over partial schedules of with at most late -jobs and at most late -jobs; if , there is no such partial schedule.
The theorem places among the polynomially solvable two-agent problems (Table 1 of the paper lists it as ), in contrast with , which the same paper shows binary NP-hard. Through the binary-search argument of §3.1, solving the constrained problem for every also yields the nondominated pairs of the corresponding Pareto problem.
The result is proved in the paper; to the knowledge of this mission it has no machine-checked proof. The mission produces a checked correctness proof of the table, including the boundary convention, which the printed text leaves incomplete (see below). Further welcome work: the complexity bound in an explicit cost model, and the weighted variant.
The table is defined over partial schedules, in which the jobs outside the early set are only counted as late, while the problem is posed over complete sequences, in which lateness is measured: a job declared late may finish on time once it is appended. The correctness of must bridge the two objects in both directions, and the bridge is the structural Lemma 7.1, which the printed proofs use without detail. Lemma 7.2 is an optimal-substructure claim: it requires that the early set of minimizing total processing time is also the right one to extend by , which holds only because of the EDD numbering. Finally, the printed boundary gives only ; the natural reading for makes Theorem 7.3 false, so the boundary must be read from the definition of , not from the display.
Fin n, 0-based, numbered in EDD order, with an owner label ag : Fin n → Agent; this follows the paper's single numbered list in §7 rather than separate index sets per agent. EDD order is the hypothesis Monotone d, ties allowed. Data are natural numbers.MooreLateJobs.Shared.completionTime (sequences without idle time) and late jobs the published MooreLateJobs.NumLate.lateSet (late iff ), reused as references with the data cast to .WithTop ℕ, with ⊤ for ; no large sentinel number is used. The boundary is for all , the value forced by the "at most" definition of ; a negative index gives ; early means , as in the recursion (the proof of Lemma 7.2 prints a strict "").Nat.find of the existence clause, which the goal asserts.Balanced truncation reduces a large control system to a small one by discarding the states that are both hard to reach and hard to observe. For linear systems "hard to reach" is measured exactly by the controllability Gramian : the minimal input energy needed to steer the system from to is . For bilinear systems, in which the input also multiplies the state, no such exact formula is known, and several papers have tried to describe the nonlinear controllability energy functional through state-dependent Gramians.
Gray and Mesko ([25] in the paper, 1998) and Condon and Ivanov ([11], 2005) stated that, for with sufficiently small, the gradient of is given by a state-dependent Gramian of the linearization, , and derived from this comparison inequalities between and the algebraic Gramian. Benner and Damm (SIAM J. Control Optim. 49(2), 2011, doi:10.1137/09075041X) observed that this formula needs an integrability condition that is not automatic, and gave an explicit two-dimensional system for which it fails (Example 3.3, pp. 697–698). This mission formalizes that counterexample.
A bilinear control system with state and input is
with real matrices and ; write for the -th column of . The system is locally controllable if the pair is controllable, that is, the Kalman matrix has rank .
Linearizing the system at a state and the input gives a linear system whose input matrix has columns . Its controllability Gramian is the solution of the Lyapunov equation
When is stable, (3.9) has exactly one solution for every , and it is symmetric. The claim under test is
A vector field on an open set is integrable (a gradient field) if for some real function .
Example 3.3 is the single-input system (, ) with
and a real parameter . In Lean these are exA, exN ν and exb (with exB the matrix ), equation (3.9) is IsLinGramian, and controllability is IsControllable.
For every , with solving (3.9) for every : the pair is controllable, and for every there is no with
The goal refutes every potential , not only , so it does not depend on how is defined; it is exactly the statement that the field is not integrable on any punctured neighbourhood of the origin, which is how (3.8) is claimed.
The result. The example shows that the state-dependent Gramian of the linearization does not, in general, describe the controllability energy of a bilinear system through (3.8), even for a locally controllable system and arbitrarily close to the origin. As a consequence, the inequalities and derived in [25, 11] from (3.8) lose their justification, and the comparison of with the algebraic Gramian requires the different argument the paper develops in its later sections. The example is a minimal one: two states, one input, one coupling parameter.
Formalizing it. The counterexample is proved in the paper by a hand computation through Kronecker products, and that computation contains a sign slip (see below); a machine-checked version settles the claim independently of it. The result is proved in the paper and, to our knowledge, has not been formalized anywhere. The general derivative formula (milestone 2) is reusable for any parametric Lyapunov equation.
The obvious route is to compute the Jacobian of at one point and observe that it is not symmetric. Two steps of this route need care. First, is defined only implicitly, through (3.9) at every point, so its differentiability in , and that of its inverse, must be derived from the invertibility of the Lyapunov operator and of near the point. Second, passing from "the Jacobian of is not symmetric" to " is not a gradient" requires the symmetry of second derivatives of a function that is only assumed differentiable with gradient on a punctured ball; the regularity of is inherited from that of , not assumed. The goal is also not a statement about a single point: it must hold for every radius , so the asymmetry must be exhibited at points arbitrarily close to the origin, where it is of order .
Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, the paper's indices are Fin m. In the goal the plane is EuclideanSpace ℝ (Fin 2) and the potential is required to satisfy HasGradientAt at each point of the punctured ball , with no further regularity.Matrix.inv, which returns at singular matrices; is invertible near the origin, and milestones 2–4 assume invertibility (or ) where they use it.Contributions welcome: proofs of the four milestones, in particular the smooth dependence of the solution of a Lyapunov equation on its right-hand side (milestone 2), which is general and reusable.
Progressive hedging separates a stochastic optimization problem by scenario, solves those smaller problems, and coordinates their first-stage decisions through weighted aggregation and price updates. It is useful when the full extensive formulation is too large to solve directly. For stochastic mixed-integer programs, its iterates can provide feasible decisions, but a feasible cost alone does not reveal how far that cost is from the global optimum. A lower bound gives the missing comparison: the difference between a feasible cost and a valid lower bound is an optimality gap. Branch-and-bound methods also use lower bounds to discard regions whose best possible cost cannot improve the current solution. These are the reasons the authors seek a bound available during a progressive-hedging run, rather than only after convergence. Gade et al., author manuscript, §§1–3.
The paper establishes lower bounds for two-stage stochastic mixed-integer programs, extends them to scenario bundles, and studies their behavior computationally. The mission concerns the mathematical statement that the price vector produced at each completed iteration is eligible for a decomposed lower bound. The paper was published in Mathematical Programming in 2016; the theorem and page labels here follow the authors' SAND2013-9195J manuscript. Gade et al., author manuscript.
Let be a finite set of scenarios and let be their probabilities, with . A first-stage decision is made before the scenario is known. Its first coordinates are nonnegative integers; the others are unrestricted reals. It incurs cost and must satisfy . After scenario is observed, a second-stage decision incurs cost . Its first coordinates are nonnegative integers, and it must satisfy . The recourse matrix is common to all scenarios. The scenario feasible set contains pairs satisfying these restrictions for one . Gade et al., §2, pp. 3–5.
In the extensive scenario formulation, each scenario has a copy of the first-stage vector, and a common vector enforces implementability through . Its optimum is . Algorithm 1 starts with zero prices , solves unpenalized scenario problems, and at iteration computes and . Later scenario solves add both and to their objectives. Here is the algorithm's scalar parameter. Gade et al., Algorithm 1, p. 6.
For any scenario prices , define the decomposed dual value by
Proposition 1 states that prices with satisfy . The price invariant in §3.1 states that the update maintains this weighted zero sum. The mission's goal combines these source claims at every completed iteration of Algorithm 1:
The formal goal is the lower-bound inequality; the zero-sum statement and Proposition 1 are its two milestones. Gade et al., Proposition 1, p. 6, and §3.1, p. 7.
For a partition of the scenarios, a bundle has probability . A bundle subproblem uses one first-stage vector for its scenarios and second-stage weights . Proposition 3 gives the corresponding inequality when . The proposal also records the bundle price invariant and the resulting inequality at each completed bundled iteration as companion statements. Gade et al., §3.3, pp. 9–10.
The scenario bound turns each price vector into an independent set of optimization problems whose weighted values certify a lower bound on the original mixed-integer optimum. The bound does not require the scenario first-stage decisions to agree at that iteration. The bundle result gives the same kind of certificate when several scenarios are solved together. These are the paper's known results, not new open mathematical conjectures. Gade et al., §§3.1 and 3.3.
Formalizing them requires a reusable interface for finite-support stochastic mixed-integer models, their scenario feasible sets, implementability equations, price systems, and finite prefixes of both algorithms. It also separates the general price-feasibility inequality from the algorithmic invariant. The mission currently proposes statements with open Lean proofs; it does not claim a machine-checked proof of these paper results.
An iteration of progressive hedging solves scenario problems with a quadratic proximal term, while the lower-bound calculation uses scenario problems without that term. Their objective values cannot simply be identified. The relevant connection is the price vector: to apply Proposition 1 at an arbitrary iteration, its weighted zero-sum condition must follow from the actual aggregation and price-update rules. The bundle version adds normalization by , so every bundle must have positive mass and the bundle weights must cover the full scenario distribution. Gade et al., §§3.1 and 3.3.
Lean represents vectors as Fin n → ℝ, linear constraints componentwise, and the extensive formulation with the weighted implementability equation printed in (15). The dimensions satisfy and , as required by the paper's spaces . The finite scenario weights are positive and sum to one. The first integer coordinates are nonnegative; every remaining real coordinate is free. The paper's assumptions that the SMIP has an attained finite optimum and each is nonempty are explicit in the goal and Propositions 1 and 3. The scenario and bundle subproblem values, and , live in the extended reals: an unbounded-below subproblem retains rather than acquiring an arbitrary real infimum. Gade et al., §§2–3.
An algorithm run is a finite prefix through its last aggregation and price update, with exact minimizers recorded as conditions on its sequences; a stopping test truncates the prefix. The proximal term is the Euclidean sum of squared coordinate differences. No positivity condition on is added to the lower-bound statements, since the page does not require one for these claims. Bundles form a partition, but equal bundle sizes are not required for the inequalities. Algorithm 2's printed w^ν(i) at initialization and Σ_i P_β x^ν(β) at aggregation are read with bundle indices. A bundle recourse vector is represented as a function on all scenarios, with only its coordinates inside the bundle constrained or used.
The exact equations of the scenario model and runs prevent a trivial encoding that assumes dual feasibility or the desired bound as part of a run. Contributions to the model, the price invariants, the extended-real weak-duality arguments, and the bundle extension are all within scope. The paper's convexified limit result (Proposition 2), its cited Theorem 1, and multi-stage Algorithm 3 are outside this mission.
Benders decomposition solves an optimization problem in two groups of variables by fixing one group, solving the remaining subproblem, and turning what the subproblem's solution proves into a constraint, the Benders cut, on the fixed variables. In the classical method of Benders (1962) the subproblem is a linear program and the cut comes from its LP dual. Many problems that decompose naturally have subproblems that are not linear programs: scheduling, satisfiability, 0-1 and constraint programs. Hooker and Ottosson (Math. Program. 96, 2003) replaced the LP dual by the inference dual, the problem of inferring the strongest bound on the objective from the constraints, and obtained a Benders scheme in which any sound inference method produces cuts. This logic-based Benders decomposition has since become a standard technique for planning and scheduling problems that combine an assignment master problem with combinatorial subproblems.
The correctness of the generic scheme rests on two short theorems of the paper. Theorem 1 says that if every cut is valid, then each of the algorithm's three ways of stopping reports the right answer. Theorem 2 says that the algorithm stops when the fixed variables range over a finite set. This mission formalizes both theorems, together with the facts used in the proof of Theorem 1.
An optimization problem (1) has a domain , a feasible set and a real-valued objective ; its value is . Optimal values lie in : an infeasible minimization has value , an unbounded one , and the reverse holds for maximization. For propositions about , implies with respect to , written , if holds at every where holds. The inference dual (2) of (1) is
In Benders decomposition the variables are pairs with , , and problem (6) is over . Fixing at a trial value gives the subproblem (7), over , with inference dual (8): s.t. . A bounding function defines the cut . The cut satisfies
(B1) if every feasible of (6) satisfies , and
(B2) if , the value obtained in the subproblem dual.
The cuts generated so far form the master problem (9): s.t. for every cut , .
The generic Benders algorithm (Figure 1 of the paper) starts with and some . While the subproblem dual at has a feasible , it formulates with and adds its cut. If the master is then infeasible, it stops and reports (6) infeasible. Otherwise it takes an optimal solution of the master and repeats. When the loop exits, the optimal value of (6) is reported as .
In Lean, LogicBenders.Generic.Setting defines all of these objects: optVal, subVal, IsDualFeasible, ValidCut, masterLHS, IsMasterOptimal and MasterInfeasible, and a Run with the predicates IsRun, StopsAtWhile and StopsAtMaster.
Assume (B1) for every cut the run has added. Then three statements hold.
If (B1) and (B2) hold, is finite, and the subproblem dual is solved to optimality, then no run of the algorithm continues forever.
Lemma 3 (p. 20) gives a criterion for a 0-1 inequality to imply the branching clause (29). The §4 statement (p. 7) characterizes when a feasible linear system implies .
Theorem 1 is what allows any sound inference method to supply Benders cuts. Correctness needs only (B1), so the method that derives the cuts (resolution, constraint propagation, a branch-and-bound proof, LP duality) never has to be re-verified at the level of the decomposition. The paper's specializations to satisfiability, 0-1 programming and machine scheduling, and much of the later literature on logic-based Benders, rely on this theorem when they check validity of their cuts and nothing more. Theorem 2 is the matching termination guarantee, and the example on p. 10 shows that the finiteness of cannot be dropped.
Both theorems are proved in the paper, and to the extent known no machine-checked version exists. A formalization makes the paper's implicit conventions precise: values in , what "the subproblem dual is infeasible" means when is always a feasible bound, and exactly which cuts the master contains at each iteration. It also exposes two gaps in the printed proofs. Theorem 1's first clause uses the attainment of the subproblem optimum without stating it. Theorem 2's printed proof claims the subproblem value increases at every iteration, which is false, although the theorem itself is true. The definitions form a small reusable layer for later formalizations of specific logic-based Benders schemes.
The mathematics is elementary, and the difficulty lies in stating it faithfully. Several readings of the statements are wrong. A "run" whose are not master optima for exactly the cuts generated so far makes Theorem 1 false. Optimal values taken as real infima turn the infeasible case into junk. Defining "dual infeasible" over the extended reals makes clause 3 vacuous. For Theorem 2, the obvious argument is the printed one, that (or ) increases strictly. It fails: with three values of and cuts equal to away from their own , the subproblem value can decrease between iterations while stays fixed. The printed argument therefore cannot be transcribed, and the theorem needs a proof the page does not give.
X stands for , Y for and D for . The feasible set is S : Set (X × Y) and the objective is f : X → Y → ℝ. Optimal values are EReal infima and suprema, with for infeasible and for unbounded problems.EReal, so is always feasible. "The subproblem dual is infeasible" is therefore stated as "no real is feasible". A master optimum means and is at most that maximum at every ; the value means the master is unbounded.ybar k, has bound zbar k, and adds cut k. The structure IsRun encodes Figure 1 exactly: zbar 0 = ⊥, every iteration finds a dual-feasible beta k > zbar k with cut k (ybar k) = beta k, and the next is a master optimum for exactly the cuts 0, …, k. An unconstrained "run", or a dual infeasibility that satisfies vacuously, would trivialize the goal, and both are ruled out by these definitions.A retailer choosing which variants of a product to stock (colours, sizes, models) faces a trade-off that operations management has studied since van Ryzin and Mahajan (1999): a deeper assortment attracts more purchases, but each added variant takes demand away from the variants already on the shelf. This loss is called cannibalization. In the standard model of consumer choice, the multinomial logit (MNL), cannibalization holds exactly: every variant's purchase probability falls when a variant is added.
The MNL assumes that a consumer who walks into a store buys either from that store or nothing. Real consumers can also leave to search elsewhere, and a deeper assortment makes them less likely to leave. Cachon, Terwiesch and Xu (working paper, 2002; published in Manufacturing & Service Operations Management, 2005, doi:10.1287/msom.1050.0088) add search to the MNL and ask whether cannibalization survives. Two forces now act on a variant's demand when the assortment expands: the share of buyers who choose it falls, and the share of consumers who stay in the store rises. This mission formalizes their answer for the first of their two search models, the independent assortment model, in which the outside option does not depend on what the retailer stocks.
There are possible variants ; the retailer stocks an assortment . A faux variant represents not buying.
Gumbel shocks. Fix a scale and let be Euler's constant. The zero-mean Gumbel law with scale has distribution function and density
Utilities. Variant has expected net utility (utility minus price), and the no-purchase option has (its price is ). A consumer's realised utilities are and , with independent and Gumbel. The preference of variant is , and .
No search. The consumer buys the variant of with the highest utility, or nothing if is higher. The probability that she buys is .
Search. A consumer may instead search at a cost and receive , where is another independent Gumbel shock that she has not yet observed. Having seen , the best utility in the store, she searches when the expected gain minus the expected loss is at least :
The independent-assortment demand is the probability that variant has the highest utility in , beats the no-purchase option, and the consumer does not search. Write (the search threshold), and .
For all and with ,
The goal leaves the utilities , , , the search cost , the scale and the number of variants arbitrary.
Theorem 1 says that under independent-assortment search the demand for every stocked variant is its MNL demand scaled by one common factor, the probability that the best option in the store clears the threshold . The threshold itself does not depend on the assortment. Theorem 2 then shows that the MNL's cannibalization effect dominates the retention effect of a deeper assortment, so each variant's demand still falls strictly when variants are added. The paper's later results on the shape of the profit function and on the structure of optimal assortments under search build on this closed form.
The paper's proofs are short but rely on steps it states without proof: the MNL formula is cited from Anderson, de Palma and Thisse (1992), the search rule is obtained "after rearranging terms", and the closed form follows from a change of variables. No machine-checked version of these steps is known. The mission produces a checked derivation of a logit-type closed form from an explicit random-utility model with an outside option and an endogenous stopping decision, at the paper's scale and with its centring constant .
Theorem 2 is not monotonicity of a single fraction. Adding a variant enlarges the denominator of and simultaneously raises the factor , so the sign of the change is a competition between the two, and a bound on either factor alone does not settle it. The comparison becomes one-dimensional only after Theorem 1 is available, and Theorem 1 itself requires computing a probability of an event defined by finitely many strict inequalities among independent Gumbel variables together with the consumer's search decision. That calculation is an iterated integral over the product law, with the decision rule, the mean of the Gumbel law and the change of variables each needing their own justification.
Fin n, 0-based (the paper's variant is index ). The no-purchase option is the extra index none of Option (Fin n). Assortments are Finset (Fin n), and is S ⊂ Splus.IsZeroMeanGumbel μ G says the probability measure G on ℝ has distribution function above; and is Real.eulerMascheroniConstant. Such a law exists for every (checked sorry-free locally).Option (Fin n) → ℝ with the product measure Measure.pi (fun _ => G). The search shock does not appear in it: the consumer decides before observing , so only its law enters, as integration against G in the search rule.noSearchProb) and (searchProb) are the real values of the probabilities of the choice events, with strict inequalities. The search event uses the paper's decision rule (the displayed integral), not the threshold ; the equivalence is a milestone. The closed form is the published RetailVariety.Structure.share.Ruled out. Demand defined by the closed form (3), which would make Theorem 1 true by definition and Theorem 2 a calculus fact; Theorem 2 with and ; a standard Gumbel law (scale , mean ) in place of the paper's zero-mean scale- law; and a model without the no-purchase option.
Infrastructure. A complete development needs the distribution theory of the Gumbel law (density, mean), choice probabilities of products of i.i.d. continuous variables as iterated integrals, and calculus for . The Gumbel and MNL lemmas are reusable for any logit-based choice model, including the other missions of this series. Contributions of proofs of any milestone, or of general MNL infrastructure that the milestones can import, are welcome.
A retailer that sells a product in many variants (colours, sizes, flavours) has to decide which variants to stock. This is the assortment planning problem. Each variant added to the shelf brings new demand. It also cannibalizes demand from the variants already stocked, and it lowers their cost efficiency, because operational costs (shelf space, handling, holding) usually show economies of scale. Cachon, Terwiesch and Xu, in Retail Assortment Planning in the Presence of Consumer Search (Wharton working paper, December 2002), study this trade-off under the multinomial logit (MNL) model of consumer choice. They compare a model without consumer search with two models in which consumers may leave to search elsewhere.
There are nonempty assortments of variants, so full enumeration is impractical. The retailer wants to know whether attention can be restricted to the popular assortments , the assortments made of the most preferred variants.
Timeline. Van Ryzin and Mahajan (Management Science 45(11), 1999, doi:10.1287/mnsc.45.11.1496) showed that, without search and with a cost derived from the newsvendor model, the profit change from adding a variant is quasi-convex in that variant's preference. As a consequence, the optimal assortment is a popular one. Cachon, Terwiesch and Xu (working paper 2002; Manufacturing & Service Operations Management 7(4), 2005, doi:10.1287/msom.1050.0088) extended the quasi-convexity to any concave increasing cost (Theorem 4 of the working paper), and then to search with independent assortments (Theorem 5). This mission formalizes Theorem 4.
Let be the possible variants. Variant has a preference ; in the paper , where is the variant's expected net utility and is the Gumbel scale. The no-purchase option has preference . With assortment , the MNL demand of variant is
Variant has margin (price minus purchase cost). Stocking it incurs an operational cost , where the cost function is concave and increasing on (the consumer population is normalised to , so demands lie in ). The profit of variant is , and the retailer's profit is .
Fix and a variant , and let . Treat 's preference as a variable. Write for variant 's demand with assortment , and for its profit. The loss on the variants already stocked is
and the net profit change from adding is . Adding is profitable exactly when . Write .
that is, every sublevel set is an interval. The goal holds for every concave increasing and every choice of margins, and assumes no differentiability.
The result. A quasi-convex function on an interval attains its maximum at an endpoint. So if adding a less preferred variant to is profitable, adding a more preferred variant (with ) is at least as profitable. With monotone margins, this exchange argument shows that an optimal assortment with variants consists of the most popular variants. The search for the optimal assortment then reduces from candidates to . The paper uses this structure again for the search model with independent assortments (Theorem 5) and in its analysis of a heuristic equilibrium (Theorem 8).
Formalizing it. The theorem is proved in the paper, and is not known to have been formalized anywhere. The mission produces a machine-checked proof for an arbitrary concave increasing cost, with per-variant margins. The paper's proof differentiates and writes a single common margin. A formal proof settles that neither assumption is needed. Van Ryzin and Mahajan's newsvendor-specific Lemma 1 is posed separately on Prove2Me (RetailVariety.Structure.lemma_1). It concerns a different function, a ratio on , and is not a special case of the statement here.
Adding changes every demand at once: 's own demand rises while all of 's demands fall, each through the shared denominator . The obvious approach is to show that is convex, and it fails: is in general not convex in , for example, when is linear and every margin equals some , is a positive multiple of the concave demand plus a constant. The paper's own argument goes through the derivative (6). It needs a derivative of , and its last step ("at most one with ") is literally false when the numerator of (6) vanishes on an interval, for instance when is linear with slope equal to a common margin, so that is constant. A rigorous proof must handle a non-differentiable concave , the endpoint where 's demand is , and a numerator that may be constant on stretches.
Fin n, 0-based (the paper's variant is index ). The no-purchase option is not a variant: is a separate real, with and for all .RetailVariety.Structure.share (from RetailVariety.Structure.Model), with assortments as Finset (Fin n). is share applied to the preference vector with 's entry replaced by the variable, on insert j S, and is assumed.ConcaveOn ℝ (Set.Icc 0 1) c, MonotoneOn c (Set.Icc 0 1)). Nothing is assumed about , so .m : Fin n → ℝ are arbitrary reals. The monotone-margin assumption of §3 is not needed and not imposed.QuasiconvexOn ℝ (Set.Ici 0). The domain is the closed half-line, including .deriv c. The goal does not.The following formalizations would trivialize the problem and are ruled out: a specific cost (newsvendor, power, linear); convexity instead of quasi-convexity; only on ; or a common margin imposed without need.
Contributions welcome: proofs of the milestones, a proof of the goal that avoids derivatives, and general lemmas on quasi-convex functions of one variable and on the algebra of MNL shares, which the companion missions of this series (I and III–V) can reuse.
Treewidth measures how closely a graph resembles a tree. Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (SIAM J. Comput. 45(2), 2016) study an algorithm for producing tree decompositions. Its headline result is algorithmic; this mission formalizes one combinatorial lemma used in its analysis.
In §4.3.2, p. 349, the authors isolate a purely combinatorial fact, Lemma 4.3, which bounds the number of nodes of a rooted tree in terms of a measure placed on its nodes. They use it for the partial tree decomposition built by FindPartialTD, with a measure of the form . This mission formalizes Lemma 4.3 and the steps of its proof. The lemma is self-contained and does not mention graphs or treewidth.
A rooted tree consists of a finite vertex set , a root , and a parent map defined on such that every vertex reaches by iterating . If , then is a child of and is the parent of . A vertex without children is a leaf. The descendants of are the vertices with for some (including itself), and the subtree rooted at is the tree they span; is its number of vertices, and .
A measure is any function . Lemma 4.3 considers measures with three properties, for a constant :
Throughout, .
Under properties (i)–(iii),
Each step is stated for an arbitrary vertex of , with the subtree in the role of the paper's tree.
The result. Lemma 4.3 converts two local conditions, superadditivity of the measure over the children of each node and geometric decay by a factor along each parent–child edge, into a global linear bound on the size of the tree. Superadditivity alone does not bound the size: a long path with constant measure satisfies (i) and (ii). Decay alone does not either: a star with many leaves satisfies (iii). The counting principle can also be used when a recursive construction splits a resource among child nodes while reducing that resource along every edge.
Formalizing it. The lemma is proved in the paper. The mission produces formal statements of the lemma and the main bounds in its proof, over a published, reusable encoding of finite rooted trees by parent maps. A complete development would also establish structural facts about descendants and children that can be reused for other results about finite rooted trees.
The summed bound for the children's subtrees contains the term . When , superadditivity alone does not give the target's final : a path with constant measure is a counterexample if geometric decay is omitted. Formalization also has to account for the fact that the reusable tree representation is a parent map on a finite type, rather than an inductively constructed tree.
The rooted tree is the published definition HarelTarjan.Compressed.RootedTree: a finite vertex type V with a root and a total parent map in which every vertex reaches the root, with the convention . is Fintype.card V, and is the published subtree size size T v (the number of descendants of , including ). The local definition file adds IsChild T v c ( and ) and children T v; the condition removes the pseudo-edge , so the root is never its own child.
Conventions: is real valued, as on the page; property (ii) is a sum over a possibly empty set of children; the constant of property (iii) is a parameter with the two hypotheses and , because the conclusion is stated with that same . The fraction is real division, and the hypothesis keeps it away from Lean's convention . The bound keeps the page's "".
A trivializing formalization is ruled out explicitly: the parent–child relation is directed by the root, so property (iii) constrains each edge in one direction only. A symmetric reading (" for all adjacent ") would be unsatisfiable for and make every statement vacuous; the hypotheses here are satisfied, for example, by the two-vertex tree with and .
A complete development needs the decomposition of size T v as and an induction principle for parent-map trees. Both are reusable for statements about rooted trees given by parent maps, and contributions of them as separate lemmas are welcome. The paper's subsequent application is outside this mission's scope.
Policy gradient methods optimize a parameterized policy for a Markov decision process by local search on its expected cost. The objective is nonconvex, so local search can in principle stall at a poor stationary point. Bhandari and Russo, Global Optimality Guarantees for Policy Gradient Methods show that for a broad family of control problems this does not happen, and, in quantitative form, that the objective is gradient dominated: its suboptimality is bounded by a multiple of the size of its gradient. The multiple involves a single problem-dependent quantity, the effective concentrability coefficient , which measures how well the initial state distribution covers the states that matter for optimal behaviour. Theorem 2 and the convergence rates of Theorem 5 of the paper are only informative when is finite, so sufficient conditions for a finite are what make those results usable. This mission formalizes the paper's three such conditions (Theorem 4).
Distribution-mismatch coefficients of this kind go back to Kakade and Langford (2002), and appear in the analyses of approximate dynamic programming by Scherrer and Geist (2014) and of policy gradient methods in finite MDPs by Agarwal et al. (2021).
A discounted Markov decision process consists of a measurable state space , nonempty feasible action sets , a bounded measurable per-period cost , a transition kernel , a discount factor and an initial probability distribution on . A feasible measurable stationary policy () picks an action in every state. Its cost-to-go is the expected discounted cost from , its discounted state-occupancy measure is
and its average cost is . The Bellman operator acts on bounded measurable functions by
An optimal policy minimizes at every state; . A policy class is indexed by a convex set , and .
The effective concentrability coefficient (Definition 3) is the smallest scalar such that
with , and if no scalar works. It converts a -weighted Bellman error into a -weighted optimality gap.
If for every measurable set , then satisfies (13); equivalently
(a) If is finite and for all , then . (c) If is a contraction with modulus in a norm with , then .
The element-wise inequalities , (5); the performance difference identity (29); the sup-norm bound (26); the occupancy-weighted inequality from the proof of part (b); and the contraction step from the proof of part (c).
Theorem 4 is what turns the paper's gradient-dominance theorem into a usable statement: with part (b), the constant in Theorem 2 is bounded by the worst-case likelihood ratio between the optimal policy's state distribution and the initial distribution, a quantity that can be checked without knowing the policy class. Part (a) shows that in finite problems any fully supported initial distribution suffices, and part (c) gives a route through weighted norms, used in the paper for optimal stopping (Lemma 13).
The results are proved in the paper. None of them is machine-checked. The mission produces a general-state-space formalization of the discounted cost MDP (kernels, occupancy measures, Bellman operators, measurable selection) together with the performance difference identity on measurable state spaces; existing formal developments of policy gradient theory on the platform are for finite MDPs only. The occupancy-measure and Bellman-operator layer is shared with the other missions of this series.
The argument for part (b) is short on paper, but each step is a measure-theoretic statement about infinite-horizon objects. The performance difference identity (29) exchanges an infinite discounted sum with integration against the chain's laws and needs the occupancy measure to be built from the -step kernels of the controlled chain. The change of measure from to needs the Bellman error to be nonnegative and integrable; its measurability is not automatic, because is a pointwise minimum over uncountably many actions, and is supplied by the measurable selection assumption. Part (c) needs the fixed-point property of the optimal cost-to-go, which again rests on measurable selection.
All statements use one Lean layer: MDP S A with measurable spaces S, A (a generalization of the paper's Borel subsets of Euclidean spaces), the cost and kernel given on all of , measurable stationary policies MPolicy S A, and costToGo, occupancy, loss, bellmanPi, bellmanOpt. The paper prints the Bellman operators (3)–(4) without the discount factor; every later use includes it, and so does the formalization. The optimal policy is a binder πstar with IsOptimal M πstar. Assumptions 1 and 2 of the paper are standing hypotheses of every main statement.
The coefficient is never formed as a number: "" is the predicate IsConcBound M Θ πθ πstar X, which says that satisfies (13); because the right-hand side of (13) is nondecreasing in the scalar, the two are equivalent. Part (b) quantifies over every with setwise, which is equivalent to ; a real-valued essential supremum is avoided because it reads exactly when the paper's bound is infinite. Part (a) assumes for every state, since otherwise is on paper and in Lean. Part (c) requires the norm comparison (21) on all bounded measurable functions, as its proof uses it on and , and encodes "a norm" by subadditivity, the one property used.
A formalization in which (13) or the occupancy-weighted inequality is assumed, or in which is a junk value of an empty infimum, would make the goal trivial; neither is used.
Contributions are welcome on every milestone, in particular on the performance difference identity and the measurability of the cost-to-go and of , which are reusable for any discounted MDP on a measurable state space.
When a controller acts on a system whose state is hidden, measurements may help it choose later actions, but the value of those measurements depends on the transition law, the observation mechanism, and the available controls. Åström's 1965 paper gave a finite-state formulation of this problem and compared the best expected loss under incomplete measurements with two limiting cases: exact state observations and no useful observations. The comparison, stated in (5.12), quantifies the value of the information available to the controller without requiring a particular numerical example. Åström, 1965.
The bounds are useful when an exact partially observed policy is difficult to calculate. The complete-information problem provides an optimistic benchmark, because a controller that sees the hidden state can condition its decision on more information. The open-loop problem provides a conservative benchmark, because it commits to a control schedule without responding to later measurements. Both auxiliary problems have simpler backward equations than the partially observed problem, as Åström notes in §V of the paper. Åström, 1965, pp. 190–193.
The hidden state belongs to a finite nonempty set , and the measured output belongs to a finite nonempty set . There are decision stages. At stage , a control is chosen from a nonempty compact set . Given state and control , the next state is with probability . At state , the observed output is with probability ; observations are conditionally independent given the state path. The stage loss is , with no fixed sign, terminal loss, or discount. The transition probabilities and loss are continuous in the control. Åström, 1965, §II.
An admissible control law may use the whole output history when choosing . Write for its expected total loss, computed from the joint law of the state and output paths, and write for the infimum of over every such admissible law. The distribution of is . After the first output , the belief is the conditional distribution of . More generally, is the conditional distribution of given outputs through time , when that history has positive probability.
Three backward values describe the information regimes. The partial-observation value obeys the Bayesian recursion (3.28). The complete-information value is the linear extension of the statewise recursion (5.4). The open-loop value obeys (5.7), in which the belief moves by prediction through without using an output. Each recursion has terminal value zero at . Åström, 1965, pp. 184, 190–191.
Theorem 2 identifies the partial-observation value with the original control problem: a selector attaining the minimum in (3.28) exists, and every such selector yields an admissible feedback law attaining . Theorem 4 gives the complete-information lower bound , and Theorem 5 gives the open-loop upper bound for every probability belief and every stage . Both inequalities apply to a general observation matrix. Åström, 1965, Theorems 2, 4 and 5.
The goal is the paper's expected-cost comparison (5.12), with its middle term explicitly identified as the minimum of the original problem:
Here the expectation is over the first measured output under and . An output with probability zero contributes zero. The left and right members represent, respectively, the costs with perfect state information and with no useful measurements. Åström, 1965, (5.12), p. 193.
For any model satisfying the stated finite-state assumptions, the two easier dynamic programs bracket the best achievable expected loss with partial information. The differences between these values are the paper's measures of the value of perfect state information and the value of incomplete state information, described immediately after (5.12). Because the loss may have either sign, these are order comparisons of minimal costs rather than bounds that depend on a nonnegativity convention. Åström, 1965, (5.13)–(5.14).
The mathematical result was established in the paper. This mission asks for machine-checked proofs of its finite-path model, the three value recursions, the identification of P.1's minimum, and the information bounds. The value functions are linked by shared definitions, so later finite-state partially observed control developments can reuse the pathwise cost and Bayes update instead of rebuilding them for each theorem.
The tempting comparison between the three Bellman equations cannot simply replace the posterior belief by its average: the controller may choose different actions after different observations, and the continuation value is generally nonlinear in the belief. The exact-information case must also be read at beliefs concentrated at a single state. Its value formula is linear in an arbitrary input belief by definition, but the partial-observation value need not equal that linear function away from those state vertices. A second issue is connecting a feedback solution of (3.28) to the original expected loss over all output-history laws; using a belief-defined objective at the outset would assume the identification that Theorem 2 establishes.
The Lean model uses finite state, output, and horizon types, a nonempty compact control set in , stochastic transition and observation rows, and continuous dependence on controls where the paper requires it. All probabilities and expectations are finite sums and products. A Fin N index of zero represents paper time one. The model starts from the law of , since §II introduces the law of but specifies neither a control at time zero nor the transition to . The transition controlled at time is therefore written with the paper's transition index . These conventions make the first-output expectation and (3.22) use the same timing.
The norm of is its norm, the sum of absolute coordinates. At an impossible output, Lean's totalized posterior is zero; the associated continuation term has weight zero. Conditional-probability claims apply only to positive-probability histories. Each minimum over controls is represented by a real infimum over . The compact control set is nonempty and the continuous costs are bounded on it, so this has the intended finite attained meaning on probability beliefs. The terminal values , and are zero.
The original objective is a separate pathwise expected cost, minimized over all admissible output-history laws. The target includes its equality with ; stating only an inequality between three unrelated Bellman solutions would omit the subject of (5.12). Reusable contributions include finite-path probability identities, the Bayes recursion, attainment for continuous control minima, and the three value comparisons. No special observation matrix is assumed in Theorems 4, 5, or the goal.
An online decision maker repeatedly chooses an action, observes an outcome, and receives a reward. In a Bayesian model, an unknown parameter controls the outcomes, and the decision maker begins with a prior distribution for that parameter. Thompson sampling acts by drawing a parameter from its current posterior distribution and choosing an action that would be best if that draw were correct. This makes it applicable when an agent can simulate a plausible model and optimize an action for that model. Russo, Van Roy, Kazerouni, Osband, and Wen explain this rule for general online decision problems in Section 4 of their tutorial.
The tutorial's Section 8.1.2 asks how to analyze the rule's expected regret. An upper confidence bound method chooses an action using an optimistic score and can analyze regret through the score's optimism and its uncertainty width. Thompson sampling does not choose its actions by maximizing such a score. Yet the tutorial shows that any score computed from the observed past can be used to split Thompson sampling's expected regret into the same two types of terms. The result is stated on pp. 72–73, equation (8.4) and the display that follows.
Let be a finite, nonempty set of actions, a finite set of outcomes, and a measurable parameter space. A prior probability measure is placed on the unknown parameter . If action is selected, the outcome is sampled from a probability kernel on . A known function turns an outcome into a reward. The mean reward of action under parameter is
For each , choose an action maximizing . This choice uses a fixed tie-break and is measurable. The same selector is used throughout the mission. A length- history records the first action–outcome pairs. A policy assigns an action distribution to every such history. The prior, the policy, and the outcome kernel together determine the law of all histories: first draw from , then choose each action from using the past history, and finally generate its outcome using .
After history , the posterior law of is obtained by reweighting the prior by the likelihood of the observed outcomes. Thompson sampling draws a parameter from this posterior and plays the selected optimum for that parameter. Thus the law of its next action, given , is the posterior law of given . The policy remains defined even for a history with zero likelihood; choices there do not affect expectations.
For a period , let be any real score that uses the action and the observed history . The score is fixed before the period's outcome or the unknown parameter can be inspected. The period regret is , with expectation taken over the prior, the policy's randomization, and the outcome process.
The first target makes posterior sampling precise. For every feasible history and action , the probability that Thompson sampling next plays , together with observing , equals the joint probability that the selected optimum is and the history is . Consequently, for every history-determined ,
This is equation (8.4) on p. 72. It asserts equality of unconditional expectations while preserving the fact that may depend on the past. It does not assert that and have the same joint law with .
The goal is the full chain of equalities displayed on p. 73:
The theorem holds for every score determined by the past history. In particular, need not be a confidence bound for the identity to hold. Being a useful upper confidence bound matters when one later estimates the two terms.
The equality permits analyses built around optimistic scores to be transferred to Thompson sampling. It separates expected regret into a term measuring whether the score falls below the true optimal mean and another measuring the gap between the score and the true mean at the sampled action. The tutorial cites Russo and Van Roy for the surrounding regret bounds; the identity here is the precise bridge used in that discussion.
The result is already proved in the tutorial. This mission seeks a machine-checked proof of its finite-action, finite-outcome form, including the posterior-sampling law, the policy-dependent history distribution, and the conditioning behind equation (8.4). The goal and milestones are open Lean statements, not completed machine-checked proofs. Their definitions can be reused in later finite Bayesian decision models with a general measurable parameter.
The central issue is that and are not interchangeable inside an expression that depends on . The sampled action and the selected optimum have the same distribution after conditioning on the observed past, but generally have different dependence on the true parameter. For example, replacing by would make the claimed equality false. A formal proof therefore has to respect the boundary between history-derived scores and parameter-dependent quantities, and it must use the same history law to interpret every expectation. Histories of zero probability also require a consistent posterior convention.
The Lean model uses finite action and outcome types and a general measurable parameter type. This is a disclosed specialization of the tutorial, which also allows infinite actions and more general outcome spaces. The kernel is nonnegative, sums to one over outcomes, and is measurable in . The prior is a probability measure. The reward function is real valued and bounded because its domain is finite. The optimal-action selector has measurable fibers and maximizes the mean reward for every parameter. These conditions make the integrands measurable and bounded, avoiding default values of nonintegrable Lean integrals.
Histories are functions from a finite period index to action–outcome pairs. Policies are normalized, nonnegative behavioural action probabilities. The likelihood of a history multiplies both its policy action factors and its kernel outcome factors. The posterior uses only outcome likelihood factors, which give the Bayes update on every positive-evidence history. The Thompson-sampling predicate enforces the posterior action probabilities on those histories and permits any normalized policy on impossible ones. Lean period denotes the tutorial's period .
The shared tie-break is essential: Thompson sampling and use the same selected maximizer. The score has type , so it cannot inspect or the current outcome. No definition is allowed to supply regret or the decomposition as a predetermined constant; the expectation is built from the prior, policy and outcome kernel. The development needs reusable definitions for the Bayesian model, finite histories, behavioural policies, likelihoods, posterior masses, and the two regret terms. Contributions proving probability matching, equation (8.4), and the final identity are welcome.
Policy gradient methods for Markov decision processes are frequently run on a regularized objective rather than on the cost of interest: a convex penalty on the action distribution is added to every single-period cost. Regularization smooths the problem, makes optimal policies strictly stochastic, and keeps iterates away from the boundary of the probability simplex, where gradients of common parameterizations vanish. Entropy and relative-entropy penalties are standard in this role; a unified treatment of regularized MDPs is given by Geist, Scherrer and Pietquin (2019), and Agarwal, Kakade, Lee and Mahajan (2021) analyse policy gradient with a log-barrier penalty added to the softmax objective.
Regularization changes the problem being solved. Anyone who uses it needs a quantitative answer to one question: how suboptimal, for the original costs, is a policy that is exactly optimal for the regularized costs? Bhandari and Russo (arXiv:1906.01786v3), whose main results establish that policy gradient objectives have no suboptimal stationary points under a closure condition, answer this question for a relative-entropy regularizer in finite MDPs (their Lemma 10). Bounds of this type for the negative-entropy regularizer are in Geist et al.; as Bhandari and Russo note (p. 20), those bounds do not apply to the unbounded log-barrier regularizer used here.
The state space is finite. There are deterministic actions , and an action is a probability vector . A policy chooses at each state; is the set of all such policies. Transitions are linear in the action,
where each is a probability vector. Each state has a nonnegative cost vector . For , the regularized cost is
where is the uniform distribution. The divergence is unless every , so takes values in .
Given a discount factor and an initial distribution , the discounted average cost of a policy is
is the unregularized cost. The discounted occupancy of is . and denote the optimal cost-to-go and state-action cost-to-go of the unregularized problem. The constant of the result is
If with , then
The result. Lemma 10 says that the price of regularization is of order as , with an explicit constant depending only on the cost scale and the effective horizon . Together with the paper's landscape results (Example 4 shows the regularized policy-iteration objective is strongly convex and the policy class is closed under policy improvement, so the regularized objective is gradient dominated), it turns convergence of first-order methods on the regularized problem into near-optimality for the original problem, and it gives a principled rule for choosing as a function of the target accuracy. The bound holds for the log-barrier (relative entropy from the uniform distribution) regularizer, which is unbounded on the simplex, a case the negative-entropy analyses do not cover.
Formalizing it. The result and its proof are published (arXiv:1906.01786v3; Operations Research, 2024). No machine-checked proof of Lemma 10 or of its steps is known. The mission produces Lean statements of the lemma and of the four steps of its proof, built on a published finite-MDP layer, and invites proofs. Step 2 relies on the duality-gap bound for log-barrier problems from interior-point theory, which the paper cites from Boyd and Vandenberghe; a formal proof of that bound (in the simplex case) is reusable for any log-barrier analysis.
The first idea, comparing with an unregularized optimal policy , fails: is typically deterministic, so and , giving no information. The comparison policy has to be built by hand: it must be strictly stochastic, nearly optimal for the unregularized problem, and have bounded divergence from the uniform distribution at every state. Each of these three properties is a separate argument: a duality-gap bound for a barrier problem on the simplex, a propagation of a one-step Bellman inequality to the whole horizon, and a quantitative lower bound on the smallest action probability of the barrier minimizer.
A second pitfall is the printed form of the lemma, whose right-hand side is ; since gives , that inequality is trivially true. The proof establishes, and the text on p. 20 announces, the bound against , which is the goal here.
States and deterministic actions are finite types S and I (nonempty, as on the page, so that is defined); . Policies, transition kernels, the occupation distributions, the cost-to-go and come from the published FoundationsML.ReinforcementLearning layer (IsPolicy, IsTransitionKernel, OccupationDist, PolicyValue, QFunction), with the cost vector passed in the reward slot: PolicyValue is a plain discounted sum, so this is the cost-to-go. Optimality is the cost-minimizing notion, defined locally.
, and take values in , with off the open simplex; real-valued junk such as never stands in for , and is never coerced to (that would make boundary policies look optimal). At the convention gives , and Lean's makes the goal's bound , the limit of the page's bound. is written as " for every policy ". The minimizer is a hypothesis (any minimizer); the barrier-greedy policy of (36) appears only in the milestones, never in the goal. A statement of the goal with the printed right-hand side , or one that assumes (35) or the divergence bound, would be a trivializing formalization and is ruled out.
Welcome contributions: proofs of the four milestones and the goal; a general Lean lemma that the discounted cost of a stationary policy in a finite MDP equals the occupancy-weighted single-period cost (milestone 1), which is reusable across policy gradient formalizations; and the log-barrier duality-gap bound on the simplex.
A failed buyer can leave a supplier with goods it can no longer sell through an existing order. A failed supplier can leave a buyer without inputs for future production. In a network, either loss can weaken another firm and start a sequence of defaults. Birge, Capponi and Chen model these effects together with two responses: suppliers reroute unsold goods to other buyers, and buyers seek replacement suppliers. Their accepted manuscript asks whether the resulting market decisions and the default cascade determine a single outcome. The issue matters when a network's resilience or fragility is measured from that outcome: a measure based on an unspecified equilibrium would not be well defined.
A supply chain order network has finitely many firms and goods . An order is the nonnegative quantity of good that firm promises to deliver to firm . The network also records each good's original price , each firm's initial equity , its safety stock and holding cost , and a realized net production cost . The realization is fixed throughout this mission; the source treats it as random when comparing network performance later in the paper. Rerouting one unit costs firm an amount ; an unfilled unit of demand incurs back-order cost . These costs and the orders and stocks are nonnegative. The basic model is on pp. 8–17 of the manuscript.
If firm defaults, a promised delivery to it is not made. Write for this undelivered order, and for firm 's total amount of good available to reroute. If a supplier defaults, write for the buyer 's lost input. After using safety stock, that buyer's unserved demand is , where . These are the quantities in equations (1)–(5).
The rerouted market for good contains firms with . At price , firm can sell up to . Aggregate demand at price is , with inverse demand . The sourcing market contains firms with . At switching cost , firm can replace up to units. Aggregate supply is , with inverse supply . In either market, an efficient allocation maximizes the stated integral objective over the capacity box, and allocates proportionally to capacity among firms quoting the same price or cost. A partial equilibrium additionally makes every active firm's quoted price or cost a best response to all nonnegative unilateral deviations. These are Definitions 2.1–2.2 and 3.1–3.2.
A firm's ex-post net worth combines original-order revenue, production and stock costs, rerouting revenue and cost, and back-order and replacement-supplier costs exactly as in equation (10). A firm defaults when its net worth is strictly negative. Starting with no undelivered orders or unserved demand, the update maps and mark all orders affected by firms that default after each market has reached its partial equilibrium. A market stable state is both the limit of that sequence and a fixed point of the update. A general equilibrium combines such a state with a partial equilibrium in every market (Definitions 3.3–3.4 and equation (18)).
The goal is Proposition 4.3, stated on p. 24:
The quadruple consists of rerouting prices , switching costs , undelivered orders , and unserved demand . The claim includes existence and uniqueness of the full outcome, not merely of its default set. The milestone list follows the paper's dependency path: Propositions A.3 and A.6 identify the unique efficient allocations in the two markets; Propositions 4.1 and 4.2 identify their partial equilibria; Lemma A.7 states that greater disruption cannot increase any firm's partial-equilibrium net worth; and Lemma A.8 states that the default updates are bounded and increasing. The numbered results and their equations are in the E-Companion, EC pp. 4–12, and the main text, p. 22.
Proposition 4.3 makes the network's outcome a function of its order commitments, stocks, prices, market functions, and realized production costs. Later comparisons of network structures can therefore refer to the equilibrium without choosing among several price or default profiles. The result also separates local market choice from the way losses spread through the network: a firm can reroute or switch optimally and still fail once the effects of other failures are accounted for.
The paper proves the result in its E-Companion, EC pp. 12–13. This mission concerns a Lean statement of that known result and the reusable definitions needed to check a proof. The draft propositions are open proof obligations; this proposal does not claim machine-checked proofs of them. The two market allocation predicates, the default update, and the cascade limit can also support later formal work on the paper's resilience results.
The market and network conditions interact. An arbitrary fixed point of the default update need not be the state reached from zero; using only the fixed-point equation loses the uniqueness asserted by the paper. Conversely, knowing a cascade limit does not by itself show that the limit is fixed, because the update changes discontinuously when a firm's net worth crosses zero. At the market level, the price and switching-cost equilibria must be established from optimization and best-response conditions. Writing the formulas for the claimed equilibrium prices into those definitions would leave the central market claims unproved.
Firms are Fin N and goods are Fin M, with ; the source numbers both from one, while Lean numbers them from zero. Orders and all default matrices are real valued and coordinatewise ordered. Active markets may be empty, as at the start of the cascade. Market objectives are ordinary real interval integrals over finite capacity boxes. The standing conditions include the paper's smoothness, concavity, and monotonicity assumptions on demand wherever it is positive and on the supply function, plus inverse identities and continuity on the quantity ranges used by the model. The inverse functions remain general data tied to and ; no linear demand or supply curve is imposed.
Several domain conventions make the displayed formulas meaningful. Assumption 2.1's minimum order is read over positive-order suppliers of a good; over all firms it would force zero safety stock whenever a nonsupplier exists. The inverse supply is nonnegative on feasible quantities, with , so the claimed switching cost belongs to the nonnegative strategy space. Demand inverse at zero is fixed to the reservation price. Assumptions 4.1–4.2 apply at each positive active-market total; for the general-equilibrium goal they are required for every binary profile the cascade can visit. Differentiability at those totals is explicit. Initial equity and the order, stock, holding, rerouting, and back-order data are nonnegative; the realized net production cost can have either sign. The model uses the p. 23 convention for prices and costs outside active markets.
An efficient allocation remains an optimizer of equations (7) or (9), with proportional tie handling; a partial equilibrium remains a best response to every admissible deviation. The general equilibrium includes both the limit from zero and the fixed-point condition. These clauses exclude an equilibrium that is true by definition or a fixed point unrelated to the default cascade. The source's informal statement that every firm “supplies, consumes, or purchases” a good has no separate activity flag in this model; a firm with no internal order can still have outside production or consumption represented in . Milestone statements involving arbitrary disruption profiles restrict them to the feasible order box , where the market inverses are defined.
A firm can lose a planned input when one of its suppliers defaults. Safety stock can absorb some of that loss, while the rest becomes demand for replacement supply. A network with more buyer and supplier links spreads orders across more firms, but the resulting benefit depends on which firms default, how much each link carries, and the price of replacement supply. Birge, Capponi, and Chen study this interaction in a supply chain model with firm defaults, switched demand, and market prices. Their Theorem 5.1 asserts that a particular order-preserving form of diversification improves the network's resilience. This mission formalizes that comparison in the notation and conventions of the accepted manuscript, including its E-Companion proof.
The question is relevant to supply chain design because adding a link alone does not specify how much business moves to it. The theorem compares two networks that retain each firm's total incoming and outgoing order quantities. It therefore isolates the effect of redistributing those orders among more partners. The result concerns a precise resilience metric: the fraction of a network's baseline out-of-stock cost reduced by holding safety stock. It does not claim that diversification prevents all defaults or reduces every component of systemic loss.
There are firms and goods. The order quantity is the amount of good that firm promises to deliver to firm . Good has price . Firm has initial equity and a unit holding cost for safety stock of good . Its realized net production cost is . Two networks and share prices, equity, holding costs, firms, and goods; their order quantities may differ. The source calls this five-part data a supply chain network, with a stock profile that is specialized here to a common scalar for the resilience comparison (§2, pp. 8–9; §5.1, p. 25).
A tiered network places each firm in a tier . A positive order of good runs from tier to tier . Tier 1 firms supply good 1, tier firms buy good , and every intermediate firm both buys and supplies its designated goods. The undirected graph underlying positive orders is connected. The model's supplier set contains firms delivering good to , and its buyer set contains firms receiving good from (§5.2–5.3, pp. 26–27).
For a common realization and safety stock , the fundamental-default set contains firms whose initial net worth is strictly negative:
The switched demand of firm for good is . The inverse supply function prices the aggregate replacement demand for good . Firm 's cost sums holding cost and switched-demand cost over every good. The network's resilience ratio is its aggregate reduction in this cost divided by aggregate cost at zero safety stock (§5.1, p. 25).
For each firm, is more diversified than when total incoming and outgoing orders are unchanged, and , and an expanded neighbor set divides orders into quantities no larger than the old quantities. Where a neighbor set is unchanged, its individual order quantities are unchanged. This is the complete condition of Definition 5.3, with the supplier good indexed as as required by §5.2.
The goal is Theorem 5.1: for two tiered networks sharing their non-order data and tier assignment,
for every admissible common safety stock and common realized production-cost vector . The three milestones are the tier-grouped expression for total cost, its order comparison between and , and equality of their zero-stock baseline costs. They are the steps of the displayed chain in the E-Companion, EC p. 18, rather than separate numbered lemmas.
The theorem gives an order-sensitive comparison of the paper's out-of-stock metric. It says that, under the stated redistribution constraints, the same amount of uniform safety stock offsets at least as large a fraction of baseline cost in the more diversified network. It supports comparisons of network designs with equal firm-level order totals. It does not rank networks with different equity, prices, or holding costs, and it does not address the paper's distinct contagion-based fragility metric (§5.1–5.3).
The result is proved in the paper; the open work here is its machine-checked formalization. The definitions of tiered order networks, fundamental defaults, switched demand, and the resilience ratio give reusable interfaces for later results about the same model. The draft Lean theorems state the full result and the three intermediate targets, with proofs left for solvers. The comparison also makes the paper's indexing and cost conventions explicit so those interfaces can be audited independently.
The default set depends on the order network, even though the two networks use the same realized costs. Thus a cost comparison cannot begin by treating defaulted firms as an unrelated common parameter. Moreover, switched demand takes a positive part after subtracting safety stock, and the inverse supply curve is evaluated at an aggregate across firms. Merely comparing individual orders or counting more links does not determine the resulting total cost. The final resilience ratio has a baseline-cost denominator that can be zero. The formalization has to cover that boundary case as well as positive baseline cost.
Firms use Fin N; goods and tiers use the paper's one-based natural-number indices. Both and are positive. Orders and holding costs are nonnegative, prices are nonnegative, and initial equity is nonnegative (the source assumes every firm is initially solvent, p. 9). A tiered network has only consecutive-tier positive orders, has activity appropriate to every firm's tier, and has a connected underlying undirected graph. The two networks share , , , the inverse supply curves, and the tier map. The source's tier-constant rerouting cost does not occur in the resilience metric and is not represented in these statements.
The paper prints Assumption 2.1 as a minimum over all firms. Since non-suppliers have zero orders, that literal reading would force and empty the theorem of its intended positive-stock content. The formalization reads the bound over actual suppliers, with . It uses monotone inverse supply curves, as implied by Assumption 2.3, and explicitly requires their values to be nonnegative for nonnegative demand; the latter is an additional convention corresponding to nonnegative inverse supply prices. These choices appear in the definitions and in the statement audit notes.
The printed supplier-order superscript in Definition 5.3 uses , while §5.2 says firm buys good ; the Lean definition uses the latter. The E-Companion's cost chain drops holding costs for goods a firm does not buy, although §5.1 sums them for all goods. The formalized cost and tier-grouped milestone retain the full sum. The paper states an almost-sure comparison under a random cost vector; its proof is pointwise, and the goal quantifies over every common realization. Each network computes its own default set. Lean sets , so a zero baseline cost requires no extra positive-denominator assumption. These conventions rule out a vacuous zero-stock reading or a cost formula weakened by omitting terms.
Competitive equilibrium is a way to divide goods when each participant has a budget reflecting her entitlement. With divisible goods, proportional value is a natural fairness target. Indivisible goods make that target unavailable in some markets: a single item cannot give two agents positive fractions of its value. The question becomes what fairness a market outcome can guarantee without dividing an item or assuming that agents value items additively. Babaioff, Nisan and Talgam-Cohen, §2.3 and §3 place this question in a discrete Fisher market, where budgets determine purchasing power but leftover money has no value to agents.
The paper introduces an -out-of- maximin share to express the entitlement of an agent whose budget is at least . Its Proposition 3.2 says that every competitive equilibrium provides this share. The result applies to any number of agents and to arbitrary cardinal preferences; it does not require the additive assumptions used for the paper's equilibrium existence results. The same paper compares the conclusion with the earlier one-out-of- guarantee for nearly equal budgets and explains that other rational shares can give a stronger benchmark in a given market. Babaioff, Nisan and Talgam-Cohen, §3.3
Let be a finite set of indivisible items and a finite set of agents. Agent has a valuation for each bundle and a positive budget . The budgets are normalized by . An allocation partitions all items: each item belongs to exactly one agent's bundle. A price vector gives each item a nonnegative real price , and the price of a bundle is . Babaioff, Nisan and Talgam-Cohen, §2.1–2.2
An allocated bundle is demanded when it costs at most and every bundle that strictly prefers costs more than . A competitive equilibrium (CE) is an allocation and price vector for which each agent demands her allocated bundle. Demand compares with every subset of , including bundles assigned to other agents and unions of several such bundles. Money is an allocation device in this model; an agent's valuation concerns her bundle alone. Babaioff, Nisan and Talgam-Cohen, Definition 2.1
For and , consider every partition of into labeled parts. Empty parts are permitted. For each partition, an adversary can leave the agent any parts, so the smallest value of a union of exactly parts is her guarantee for that partition. The agent chooses the partition that maximizes this worst-case value. This is her -out-of- maximin share. The allocation guarantees the share when is at least the resulting maximin value. Babaioff, Nisan and Talgam-Cohen, Theorem 1.2 and Definition 3.1
For every agent , every competitive equilibrium, and every pair of natural numbers with and , the goal is Proposition 3.2:
The three milestones record the paper's intermediate claims in order: the total price of all items is at most the total budget; among parts, some have price at most of the total; and a bundle an agent can afford is no better for her than the bundle she demands. The goal quantifies over every eligible rational share rather than selecting a single fixed denominator. Babaioff, Nisan and Talgam-Cohen, proof of Proposition 3.2
Two companions record the first welfare theorem, which makes a CE allocation Pareto optimal under strict preferences, and the appendix's coalition form of justified envy. The latter excludes the single case in which the comparing agent's bundle and the coalition's union are both empty, because the printed strict comparison is false there. These companions provide context for the equilibrium notion; neither changes the valuation generality of Proposition 3.2. Babaioff, Nisan and Talgam-Cohen, Theorem 2.4 and Claim A.8
The proposition gives a fairness conclusion conditional on equilibrium existence. It covers agents with different entitlements and nonadditive valuations, using a share that the agent herself evaluates through a partition of the items. The result does not assert that an equilibrium exists for every market. It says that any equilibrium already present meets all the stated rational-share benchmarks simultaneously. The paper uses this to relate competitive outcomes to maximin guarantees previously studied for nearly equal budgets. Babaioff, Nisan and Talgam-Cohen, §3
A machine-checked development would add a reusable account of finite allocations, bundle prices, demand, and maximin shares, plus a certified bridge between equilibrium and fairness. The draft Lean items in this mission are open statements with sorry; the local build checks their types and imports, not their mathematical proofs. The equivalence of the chosen maximin encoding with the finite max–min formula is checked separately in a sorry-free sanity file. Formal proofs of the goal and its milestones remain solver work.
The main formal issue is to keep the quantifiers and boundary cases aligned with the fairness definition. The guarantee concerns every partition into parts, including empty parts, and the worst choice among subsets of exactly parts. A benchmark formed from one convenient partition, from at most parts, or from a restricted family of affordable bundles would have a different meaning. The total price comparison also depends on every item being allocated exactly once. The appendix companion has a separate edge case: strict envy cannot follow from demand when the two compared bundles coincide as the empty set.
Items are Fin m, agents are Fin n, and valuations are real-valued functions on finite item sets. An allocation is a function from items to agents, so feasibility and market clearing are part of its type. A partition into parts is a function from items to Fin d; it allows empty parts. Prices and budgets are real. The goal assumes positive budgets with sum one, nonnegative prices through the CE predicate, and . The case is allowed; the budget condition implies . The Lean maximin guarantee is written as a quantified comparison rather than using a real supremum or infimum, avoiding default values on empty extrema. A sanity theorem relates it to the finite max–min expression under its proper domain conditions.
The paper's normalization and arbitrary-preference scope are retained in the goal. Strict preferences are used only for the first-welfare and appendix companions. There, injective valuations exclude the paper's exception for identical items, and the appendix claim additionally excludes the case in which the comparing agent's bundle and the coalition's union are both empty. The mission's setting is repeated locally because no published platform definition has the same bundle market and budget conventions; the related housing, divisible-goods, and convex-economy models use different objects.
Contributions should preserve full market clearing, demand over every item bundle, nonnegative prices, all -part partitions, and exactly selected parts. The definitions and finite averaging milestone can be reused in other fair-division developments. Proving the three source milestones and the goal, or improving the formal treatment of the appendix edge case, are within scope.
The cosmological constant was added by Einstein in 1917 to the field equations of general relativity so that a static, matter-filled, spatially closed universe would be a solution. It was sidelined after the discovery of cosmic expansion, invoked repeatedly for specific puzzles, and returned to the centre of cosmology after the supernova observations of 1998 showed that the expansion of the universe is accelerating. The centennial review of O'Raifeartaigh, O'Keeffe, Nahm and Mitton (EPJ H 43 (2018) 73) traces this history. Along the way it states, in numbered equations, the small body of mathematics on which the whole story rests: Seeliger's modified Poisson equation, Einstein's static universe, de Sitter's empty universe, Friedman's evolution equations, the Einstein–de Sitter model and critical density, and the deceleration parameter that links to an accelerating universe.
Timeline of the results formalized here, as presented in the review:
Time is a real variable . A homogeneous universe is described by a positive scale factor (radius) and a mean matter density . The constants are Newton's constant , the speed of light , Einstein's constant , the cosmological constant (the review's ) and a curvature index ( closed, flat, open). The pair is a Friedmann–Lemaître dust solution on a set of times if is near each and
For these are exactly the review's equations (15)–(16). The Hubble parameter is , the deceleration parameter is (eq. 26), the critical density is , and the density parameters are and (Section 5.1). For the Newtonian part, is the Laplacian on .
For every Friedmann–Lemaître dust solution, at every time with ,
and if the expansion is accelerating () while the density is non-negative, then . This is the statement through which accelerated expansion forces a positive cosmological constant, which the review's title points to.
Seeliger's no-bounded-potential paradox for (3) and the unique bounded solution of (4); Einstein's static universe (10); the bounded-potential criterion for the Newtonian limit (11); Eddington's instability of the Einstein world; de Sitter's solution B (13); Lemaître's exponential form (14); Friedman's first integral (17); the critical-density classification of curvature; recollapse of supercritical universes without ; the Einstein–de Sitter age ; and the matter-only deceleration law (25)–(28).
The goal is the formula used to read the sign of off measurements of ; it underlies the review's account of how the supernova data of 1998–1999 were interpreted as evidence for a positive cosmological constant. The milestones are the classical facts about that the review uses to explain each episode of its history: why Seeliger and Einstein needed a decay or cosmological term, why the static universe was abandoned, and how matter density, curvature and expansion rate are related. All of them are established results; the work in this mission is to formalize them faithfully in the review's own notation. Several related Friedmann-equation statements exist on the platform in other conventions; this mission keeps the review's equations verbatim, in particular with explicit and .
The algebraic statements (goal, static universe, de Sitter, classification) reduce to manipulations of the two equations, but they need care with derivatives and with the conventions . The analytic milestones are harder. Seeliger's statements require a Liouville-type theorem for bounded solutions of and of on all of ; such results are not readily available. Eddington's instability requires producing genuine nearby solutions of a nonlinear ODE system that leave a neighbourhood of the static state, not only a linearized computation. The recollapse and age statements need global arguments over an unbounded time interval.
All quantities are real numbers. The Friedmann–Lemaître predicate quantifies over a time set ; theorems specify (all of , a closed interval , a half-line, or a preconnected set). Derivatives are Lean's deriv; differentiability is enforced by requiring to be near each time of , so no junk derivative values enter. Division by zero is excluded explicitly where it matters (for instance in the goal, so that ). The Laplacian is defined from scratch as the sum of the three second partial derivatives on Euclidean three-space. Pressure is zero throughout (dust), as in the review's equations (15)–(16). The review often sets (eqs. 10, 13); the formal statements keep explicit, which reduces to the review's formulas at . Contributions of general-purpose lemmas (Liouville theorems, ODE instability criteria) are welcome.
In A Model of Leptons (Weinberg, Phys. Rev. Lett. 19, 1264 (1967)) Steven Weinberg proposed that the photon and the intermediate bosons of the weak interaction are gauge fields of a single symmetry group, , and that the visible differences between them — the photon is massless, the weak bosons are heavy, and their couplings differ — come from a spontaneously broken symmetry of the vacuum rather than of the Lagrangian. The Goldstone bosons that such a breaking would normally produce are removed by the gauge fields (the Higgs–Englert–Brout–Guralnik–Hagen–Kibble mechanism). This model became the leptonic sector of the Standard Model of particle physics.
The paper is three pages long and its quantitative content is a short chain of finite-dimensional algebra: after the scalar field is replaced by its vacuum value, the gauge-boson mass terms form a quadratic form whose diagonalization gives the charged boson , the neutral boson and the massless photon, together with formulas for their masses, for the electric charge and for the weak coupling constant. This mission formalizes that chain.
The model has two gauge couplings (for the isospin fields ) and (for the hypercharge field ), and a complex scalar doublet whose vacuum expectation value is with real. Replacing by in the Lagrangian (eq. (4) of the paper) leaves the spin-one mass terms (eq. (7))
At a fixed spacetime point we write the gauge fields as a vector . The mass terms are then for the symmetric mass-squared matrix
A field of definite mass is a linear combination whose coefficient vector satisfies . The paper's candidates are
with masses , , . The rationalized electric charge is , and the weak coupling constant is defined by . The electron gets the mass from its Yukawa coupling . The electric charge in the paper's conventions is , where is the third isospin component and the hypercharge.
The goal theorem states, for :
where are the coefficient vectors of , and, for all and all field values,
so the massless field is the photon and it couples to with strength .
The milestones follow the paper's numbered equations: eq. (7) as a quadratic form; eqs. (8)–(9) ( and ); eqs. (10), (12) ( and ); eqs. (11), (13) (photon massless); the orthonormality of (10)–(11); eq. (15) (the charge); eq. (16) (); ; ; the parameter-free forms of the bounds BeV, , BeV; and the tree-level vacuum condition .
The result itself. These formulas are the tree-level predictions that made the model testable: a massless photon, a charged and a neutral with , and the relations tying , , and to . The existence of the neutral boson (and its neutral currents) was the model's new prediction, later confirmed experimentally.
Formalizing it. The results are classical and fully proved on paper. The mission produces a machine-checked record of the paper's algebra, with every hypothesis stated (for example, that and are not both zero), and a reusable encoding of the electroweak boson mass matrix.
The mathematics is elementary; the difficulty lies in faithfulness. The paper's sign conventions are not fully consistent (substituting the vacuum value into eq. (4) as printed gives in the second mass term, while eq. (7) prints , which is the combination consistent with eq. (10)). The numerical claims (40 BeV, 80 BeV, ) depend on experimental inputs and on rounding. The formalization therefore takes eq. (7) as printed as its starting point and states the bounds in parameter-free form.
WeinbergLeptons_Model, in namespace WeinbergLeptons.Runtime monitoring checks a running system against a specification by inspecting its trace of events as it is produced. Policies on data, such as "every published report was approved within the last 10 days" or "each value stored in in reaches out within 5 time units", quantify over data values and constrain the time between events. Metric first-order temporal logic (MFOTL) expresses such policies: it extends first-order logic with past and future temporal operators that carry intervals of allowed time differences.
Basin, Klaedtke, Müller and Zălinescu (J. ACM 62(2), Article 15, 2015) give a monitor for MFOTL properties with bounded. It allows negation and quantification over the infinite domain without restriction, because every relation it manipulates is represented by a finite automaton: the input structures are automatic structures. The paper implements it in the prototype tool MonPoly-Reg (§6). Its correctness rests on Theorem 3.9: the monitor reports exactly the violations of , at every time point.
A signature has finitely many constants and predicates with arities. Formulas are built from and by , , and the temporal operators (previous), (next), (since) and (until), where is a nonempty interval of with . A formula is bounded if every in it has .
A temporal structure assigns to each time point relations and a time stamp ; constants are rigid, , and exceeds every bound. Satisfaction is Definition 2.2; for example holds at if holds at some with and holds at all . For with free variables , the satisfying set is
A domain representation is a regular language over a finite alphabet with a surjection whose equality relation is regular. A relation is regular if the words (the letter-by-letter convolution, padded with ) with form a regular language.
The monitor (Fig. 2) reads one element per loop iteration. It extends each to with auxiliary relations (and , for since and until) for every temporal subformula , built incrementally by the constructions of §3.4 once a list of pending triples says that enough of the future has been read. When is complete it outputs the set with , where is with each top-level temporal subformula replaced by the atom .
For every input satisfying the restrictions of §3.1 and every bounded :
where each output is followed by line 11 setting to the next index. This records counter values reached inside the while loop, including values that may never appear at a loop entry. Part (ii) excludes the vacuous reading of (i).
Theorem 3.9 makes a sound and complete monitor for the safety fragment , bounded: every violation at every time point is reported, nothing else is, and every output is a finitely represented (regular) set even though it may be infinite. It covers unrestricted negation and quantification, which finite-relation monitors (§4 of the paper) cannot handle. The incremental constructions of §3.4 are the template reused by later MFOTL monitors.
The paper gives a mathematical proof of its monitor's correctness. This mission asks for a Lean proof that checks the MFOTL semantics, automatic relations over , and the correctness of this particular monitor, including the until construction whose printed version is defective (see Formalization scope).
Two parts are hard. The regularity claims need the fundamental property of automatic structures: first-order definable relations are regular, which requires closure of padded convolution languages under Boolean operations, cylindrification, permutation of tracks and projection, the last with removal of trailing padding. The arithmetic constraints of the since and until constructions additionally need successor and offset relations definable from .
The scheduling argument is the other part. Correctness of a build at requires that every input relation, at time points up to for until, was built before and not discarded since. Following only the syntax of does not settle this: a needed relation for a subformula at a later time point may be built in the same iteration as 's.
The domain is , as §3.1 assumes. Relations are sets of lists of natural numbers, ordered by the sorted free variables. Interval upper bounds are in ; intervals carry the proof that they are nonempty. The representation is a single parameter shared by the hypothesis "every is regular" and the regularity claims of the conclusions; it is never chosen existentially. The binary predicate interpreted as is a hypothesis.
Two hypotheses on besides boundedness are the paper's own "without loss of generality" assumptions: each temporal subformula occurs once in (§3.6), and the direct subformulas of each , subformula have the same free variables (§3.4; achieved by padding with , as in §3.5). No other restriction is placed on .
The printed until construction (§3.4.4) is repaired: the guard of is " for all ", since the printed guard empties in the paper's own example of §3.5; keeps only tuples with , since otherwise a -witness at time point survives to time point when ; and time-stamp equations are encoded additively. Lemma 3.8(i) reads and adds . "Effectively computable" in Theorem 3.9(i) is not formalized. Part (ii) uses the output at index as the record of the line-11 increment to ; for , the counter is initialized by line 2. Loop-entry states alone can skip counter values reached within one iteration.
The monitor is a state machine whose builds and outputs are computed only from its store of relations; it never consults the satisfaction relation or satisfying sets. A formalization in which line 7 reads the semantics would turn Theorem 3.9(i) into a restatement of Lemma 3.4, and is ruled out. A build whose input is missing stores nothing, so a monitor that silently fails would violate (ii).
Contributions welcome: the theory of automatic relations (reusable beyond this mission), the semantic halves of Lemmas 3.4–3.8, and the scheduling invariants.
A set-valued predictor returns, for each input , a set of plausible responses rather than a single guess. Such sets are used wherever a model's output feeds a decision with asymmetric costs: a medical classifier that lists every diagnosis it cannot rule out, a segmentation model that marks every pixel that may belong to a tumour, a protein-structure predictor that reports a range of distances. Bates, Angelopoulos, Lei, Malik and Jordan, Distribution-Free, Risk-Controlling Prediction Sets (J. ACM 68(6), 2021), calibrate a nested family of such predictors so that a chosen loss is controlled with high probability, without distributional assumptions.
Calibration says nothing about which family to calibrate. Any nested family can be made risk-controlling; families differ in how large their sets are, and large sets are uninformative. §4 of the paper asks which family is best in the population: which predictor achieves a given risk with the smallest expected set size. For a weighted miscoverage loss (Theorem 7, §4.2) the answer thresholds a weighted conditional density, in the spirit of the optimality results of Sadinle, Lei and Wasserman (2019) for classification. Theorem 8 (§4.3) extends the answer to every loss of integral form. This mission formalizes Theorem 8.
Let take values in with law , marginal , and conditional law of given . Prediction sets are subsets of a measurable space (in the paper's examples ). A set-valued predictor is a map .
Fix a finite measure on and a nonnegative cost ; is the cost of leaving out of the prediction set when the true response is . The loss of a set is the total cost of what it leaves out,
and the risk of a predictor is (§2.1). Larger sets have smaller loss. The conditional expected cost of omitting at is
and for the threshold predictor of display (11) is
It includes exactly the points whose omission is expected to cost at least . The size of a set is its -measure, , and the expected size of a predictor is .
In Lean: setLoss μ ℓ y S, risk P μ ℓ T, condLoss κ ℓ x z, thresholdSet κ ℓ lam x and expSize P μ T in the namespace RiskControl.Optimal.
For every and every set-valued predictor (with measurable graph),
No constant is involved; the statement is uniform over , , and .
The result. Theorem 8 identifies the population-optimal shape of a set-valued predictor for every loss that charges for omitted points through a nonnegative cost and a finite measure. It justifies building nested families by thresholding an estimate of the conditional expected cost: if the estimate were exact, no other predictor with the same or smaller risk could have smaller sets on average. It contains the weighted-miscoverage case (Theorem 7) when is discrete and is counting measure, and it covers losses for which no such special case exists, such as costs that depend on the distance between and .
Formalizing it. The proof on p. 27 is a chain of eight displays. A machine-checked version settles the measure-theoretic points the chain passes over: the conditional expectation inside an integral over a random set, the cancellation of possibly infinite terms, and the range of . To our knowledge no formal proof of Theorem 8 or of the Neyman–Pearson-type optimality results it generalizes for set predictors exists in Lean or Mathlib.
The natural reading of the proof subtracts the quantity from both sides of the risk comparison to pass from complements to sets. Nothing in the setting makes this quantity finite, so that step is not valid as written, and a proof that follows the displays literally breaks there. The theorem itself does not need finiteness of , and no such hypothesis is in scope.
The other obstacle is measure-theoretic bookkeeping. The conditional expectation is indexed by a point of a second space, and must be a jointly measurable function of before it can be integrated over the random set ; here it is given by a regular conditional distribution, and every integral over needs the measurability of the graph of .
The development needs Mathlib's composition of a measure with a kernel, Tonelli's theorem for kernels and lower integrals over sections of a measurable set. Lemmas about expected -sizes of random sets (milestone 4) and about moving a kernel integral inside a set integral (milestone 1) are reusable beyond this mission. Proofs of the milestones, and of the goal by other routes, are welcome.