Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Unmanned aerial vehicles, spacecraft and other mission-critical systems carry a sensor that reports their health imperfectly. While a mission runs, an operator must decide at each sampling epoch whether to abort and pay a mission failure cost, or to continue and risk losing the system. A wrong decision in either direction is expensive, and the decision has to be made online. Sun, Hu and Ye model this as a partially observable stopping problem with general sojourn-time laws, and approximate it by a finite Markovian surrogate that can be solved exactly (arXiv:2505.03225v1). Phase-type approximation of semi-Markov decision problems is common in reliability; what a user needs to know is whether the policy computed on the surrogate is good in the real system, not only whether the two optimal values are close. Khaleghei and Kim (2021) prove the value statement for a maintenance problem. The theorem here addresses the policy.
A system runs for sampling periods of length , so the mission time is . Its state is healthy, defective or failed (states ), with . Let , and be independent, with continuous on . The system fails at if ; otherwise it turns defective at and fails at .
At time a signal is observed. It is if the system has failed, and otherwise lies in , with for . The signals are conditionally independent given the failure process.
A decision rule is a map for , with required when . It determines the stopping time . Aborting at takes a rescue time with , and finishing takes . Problem (1) minimizes , where
The surrogate replaces and by the Erlang mixtures and of (3) and (2), with shapes satisfying . They give a chain on with initial law (4) and rate matrix (5), (6), whose clusters are healthy, defective and failed, and signals driven by the same matrix . Problem (7) is Problem (1) for this system.
Let solve (1) and solve (7), both pinned at positive-probability histories by comparing the two costs-to-go. For every ,
the realized cost converges -almost surely, and
The first equality of (8) says that the surrogate's rules are asymptotically optimal when applied in the original non-Markovian system. It licenses solving the finite surrogate for a large and deploying the resulting rule. The second equality is the classical convergence of optimal values.
Formalizing the theorem adds to the platform a policy-convergence result for a phase-type approximation, weak convergence of Erlang mixtures, which the platform does not have, and a finite-horizon dynamic programming principle for stopping problems with partial observation. The result is proved in the paper, except for the convergence of the mixture, which it cites from Wiens (1979). None of these has a machine-checked proof on Prove2Me.
The surrogate's state space grows with , so nothing can be read off a single chain. The probability spaces differ with , so convergence must pass through laws. The relevant conditional laws sit inside a backward recursion, conditioning on events whose probability also moves with ; a history that is null in the limit may have positive probability under every surrogate. The natural functionals, the state at a fixed time and the signal kernel, are discontinuous in the transition times, so the continuous mapping theorem does not apply directly, and only an almost-everywhere version does, with , having no atoms. The obvious route of comparing the policies directly fails, because the policies are only pinned by the costs-to-go.
The paper's first clause of Proposition 1 is false as printed: the chain may be absorbed from the healthy cluster and never reach the defective one, so its hitting time is infinite with positive probability, while is finite. The milestone states the minimal correction, the law of the cluster process, which is also what the proof of Theorem 1 uses.
The sentence "We assume the set of optimal actions is unique" (p.11) is read as at every positive-probability history , which is how the proof uses it (pp.EC.3–EC.4). Read as a singleton set of minimizers, it is unsatisfiable for : rules at histories after an earlier abort do not affect the cost. The surrogate's rules may break ties in any way, which covers the strict rule of p.EC.2 and the smallest stopping time of p.15.
Conventions in Lean: states of the surrogate are -based, so the Lean state is the page's ; the stopping time is an index, not a real division; rules are Bool-valued; conditional probabilities are ratios, always guarded by positive probability of the history under the law in question; ranges over , with each surrogate on its own space. have no atoms, and densities are not assumed. The chain's law is required on the finite set of times the problem reads; a genuine chain satisfies this. Assumptions 1 and 2 are not used, and neither is the monotonicity in Assumption 3.
A vacuous formalization is ruled out: a clause of the goal binds the rules to Problems (1) and (7), and the hypotheses hold at a concrete instance with , , .
Needed: the Erlang mixture, finite-dimensional laws of a chain with a random start, a mapping theorem for almost-everywhere-continuous functions, weak convergence of products, and the backward induction. The Erlang-mixture convergence and the mapping theorem are reusable beyond this mission. Proofs of any milestone, and sharper variants, are welcome.
A seller offering several substitutable products must decide whether to charge one common price or a different price for each product. Customers may compare every product's net utility, or they may buy the cheapest product that they can afford. The second behavior is min-buying: a customer checks whether each product's valuation covers its price and selects the cheapest acceptable product. The distinction changes how inexpensive products divert purchases from expensive ones. Cui, Hamilton, Lamperski, and Ganjizadeh Tari study the resulting value of uniform pricing in symmetric and asymmetric valuation environments. The source for this mission is the September 27, 2026 manuscript, including its electronic companion.
There are products. A customer has a nonnegative random valuation vector . A feasible price vector has nonnegative coordinates. The customer's payment is the smallest among products satisfying , or zero if there is no acceptable product. Equal prices create no payment ambiguity. This defines expected differentiated-pricing revenue and uniform-pricing revenue .
The optimal revenues are and . The source explicitly assumes that these optima are finite, attained, and that . The formal model records those conditions. It does not impose finite expected valuations: fixed finite prices have bounded payments even for valuation laws with infinite first moments. General joint probability measures describe dependent valuations; product measures describe independent valuations.
A law is exchangeable when permuting its product coordinates leaves it unchanged. It is affiliated when it has a joint density or probability mass function satisfying for every pair of valuation vectors. A nonnegative marginal law is regular when its revenue-quantile curve is concave. Regularity uses interior quantiles, with endpoint conventions stated explicitly; it is not replaced by the stronger monotone-hazard-rate condition.
For independent, absolutely continuous regular valuation distributions, the target is
The constant is defined exactly. Let and for , and let solve
Then is the unique point in with . The main target includes this nondegenerate root characterization, the universal guarantee, and sharpness: for every there is a finite independent continuous regular instance with . The number of products can vary with . The manuscript's decimal is explanatory; no decimal is substituted for the exact constant. These are the two conclusions of Theorem 4, p.17.
Theorems 1 and 2, pp.10 and 13, assert for IID valuations and for exchangeable affiliated valuations, respectively. Supporting targets state the stronger policy comparison proved in the manuscript: every price vector is dominated by a uniform price selected from that vector. Theorem 3, p.15, gives an exchangeable nonnegative valuation law for every positive such that
This last construction is discrete and does not carry a density assumption.
The milestone list includes the independent-revenue identities, the affiliated conditional-threshold comparison, Lemmas 1–4 on triangular and canonical distributions, Lemmas EC.1–EC.2 on rejection probabilities and continuous approximation, and the analytic properties used to specify the exact constant. Additional interface targets identify the concrete triangular probability laws and connect the canonical continuation formulas to actual min-buying revenues. All main results and numbered supporting lemmas of the source are represented in this one mission.
The symmetric results specify settings where charging different prices gives no revenue advantage. The asymmetric result gives an exact worst-case guarantee and establishes that a better universal fraction cannot hold throughout the stated regular class. The exchangeable lower bound distinguishes symmetry alone from symmetry combined with affiliation. These interpretations follow from the paper's statements and comparisons in Sections 3–4.
The formalization makes the customer payment rule, probability classes, optimization assumptions, and sharpness quantifiers explicit. It also separates an ODE-defined constant from its numerical approximation. The current deliverable consists of locally compiled definitions and open theorem statements, with independent blind read-backs. Statement compilation is not a proof of a theorem; completed Lean proofs are the mission's remaining work.
Atomic cap distributions require inclusive purchasing and strict rejection probabilities. Substituting a right-continuous CDF for strict rejection at a cap would change the revenue. Affiliation must be used in its density-or-mass-function meaning; the conditional-tail comparison is a theorem to establish. Discrete order statistics can contain ties and need the corresponding multiplicity treatment. The tightness claim must ultimately hold for continuous regular distributions, although several intermediate extremal distributions have atoms. The continuous approximation lemma is therefore part of the target list.
The exact constant requires existence, uniqueness, and maximum properties of its concrete integral benchmark. Those properties are separate conclusions, not hypotheses of the market model. The canonical continuation value is revenue from the designated cap prices; it is not defined to equal the optimal differentiated revenue.
Valuation and price vectors are real functions on a finite index type. Joint laws are probability measures; no finite support or moment restriction is inserted into the general pricing theorems. The original continuous-market conventions and positive attained optimum conditions are explicit where used. Atomic triangular laws and the exchangeable lower-bound witness have their appropriate separate scopes. Prices are optimized over all nonnegative real vectors, with no fixed ordering imposed on the feasible set; sorted order is required only in formulas that use it.
Regularity is concavity of for , avoiding undefined endpoint quantiles. For a nonnegative curve this is equivalent to concavity of its zero-endpoint extension. Affiliation covers both a Lebesgue density and a probability mass function on real-valued vectors. The ODE benchmark is an explicit integrating-factor integral; the main goal proves that its root is unique and lies strictly between zero and one. No desired revenue comparison or extremal bound is assumed inside a definition.
Reusable components include the min-buying payment model, strict-rejection identities, quantile regularity, exchangeability and affiliation, triangular laws, and finite-to-continuous comparison. Proofs of these components and of the paper's complete targets are welcome. All code targets Lean 4.33.1 and the pinned Mathlib environment.
A proof that an output exists can contain enough information to compute that output. Classical proofs make this connection less direct: an existence claim may be established through a contradiction without displaying its witness. This mission formalizes the extraction method of Berger, Buchholz, and Schwichtenberg in Refined program extraction from classical proofs (2002), especially Sections 2–5 and Corollary 5.3. The paper allows certain assumptions to remain unproved and permits specifications beyond quantifier-free formulas.
The formal language has natural-number and boolean types, function types, and System T terms built from variables, constants, application, abstraction, and primitive recursion. A separate typing judgment checks which type a term has. Formulas are built from boolean atoms, falsity, implication, and universal quantification. The extended language also contains a distinguished propositional symbol .
An object variable is a parameter of a formula or a program; an assumption variable labels a hypothesis in a proof. These are different roles. A proof with no free assumption variables may still contain free object parameters. The formalization represents derivability by proof terms and an inductive judgment. The systems and differ by the availability of ex falso; superscript permits the extra propositional symbol.
Two mutually defined syntactic classes identify the permitted assumptions and specifications. Definite formulas include atomic formulas, suitable implications, and universal quantifications. Goal formulas include atomic formulas, suitable implications, and universal quantifications subject to the paper's relevance restrictions. The constructors in IsDefiniteFormula and IsGoalFormula specify these restrictions explicitly.
Write for replacing falsity by . The assignment associates either a program type or the symbol to a formula, taking . A comprehension term substitutes a program into an ordinary formula . Modified realizability relates a program to a formula , written ; its clause for is . When the assigned type is , the realizer is the omitted symbol .
The first milestones formalize the logical infrastructure: Lemmas 2.1–2.3, Lemmas 3.1–3.2, and the refined translation theorem, Theorem 3.3. The soundness milestone, Theorem 4.1, asks for a derivation of
from the realizability translations of the free assumptions of a derivation . Theorems 5.1 and 5.2 state the computational consequence under supplied realizers and the existence of uniform realizers for definite and goal formulas.
The main target is Corollary 5.3. Let be definite formulas, let be a goal formula, and let be fresh for the assumptions. Choose formula realizers before choosing a proof . For every admissibly named derivation
the extracted program exists and the well-typed output satisfies
Arguments assigned are omitted. The chosen realizers may retain the formulas' free object parameters. The final goal combinator abstracts .
The mathematical extraction result is proved in the paper. This mission asks for a machine-checked formalization of that result and its supporting logical transformations. It makes the actual extracted term part of the specification: correctness must apply to the term computed from the supplied derivation.
All six milestones and the main target, corrected Corollary 5.3, are now Proved on Prove2me. On 1 November 2026, the complete proof of corrected Theorem 4.1 was accepted, resolving the previously accepted reductions for Theorems 5.1 and 5.2 and Corollary 5.3. The mission has no open proof dependencies. The soundness submission matches the exact published statement and uses only Lean’s standard axioms, with no proof holes or additional freshness premises.
The accepted proofs include capture-avoiding substitution, compatibility with formula conversion, extraction typing and free-variable bounds, the natural-number and Boolean induction realizers, and the parameter-renaming argument needed for unrestricted soundness.
Named variables make scope part of the mathematical work. Formula conversion may rename a binder without changing the proof term, so inspecting only the variable names written in that proof cannot justify capture-sensitive substitution. Universal introduction also requires freshness for undischarged assumptions. Finally, uniformity in the comprehension term does not mean that a realizing program is closed with respect to the specification's free parameters. Each of these distinctions must survive composition of the extraction results.
The development uses Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. BBS2002_Arithmetic supplies syntax, substitution, conversion, and derivability. BBS2002_Extraction supplies the formula classes, type assignment, and structural extraction. BBS2002_V2_Realizability supplies the corrected realizability translation and naming convention. The revised targets use namespace BBS2002.V2; the first three accepted milestones retain their original names.
The V2 translation chooses fresh bound variables and preserves free parameters. Its indexed realizers distinguish an omitted argument from a term without supplying a default term at an invalid input. Extraction admissibility requires a typed closed dummy term, consistent assumption labels, and separation between assumption labels and object-variable identifiers within the proof. It imposes no global separation from comprehension parameters.
The November 2026 correction replaces the original Theorems 4.1, 5.1, 5.2 and the main target. The changes address variable capture, the missing freshness condition for assumptions, and an incorrect closedness requirement on uniform realizers. The former targets are retained as deprecated historical records. The revised Corollary 5.3 explicitly exhibits successful raw extraction, rather than relying on a default result when extraction fails. These corrections were checked against the source and accompanied by an independent code-only read-back and concrete regression examples; all corrected targets now have accepted proofs.
Reusable contributions include substitution and conversion lemmas, preservation of typing and free variables, hygienic proof transformations, and the realizability soundness proof. A conditional reduction must record its open dependencies and must not be reported as a completed proof.
Ulrich Berger, Wilfried Buchholz, and Helmut Schwichtenberg, Refined program extraction from classical proofs, Annals of Pure and Applied Logic 114(1–3), 2002, pp. 3–25. The mission's theorem page references use the author's preprint pagination: Sections 2–5, pp. 3–14; Theorem 4.1, p. 12; Theorems 5.1–5.2, pp. 12–14; Corollary 5.3, p. 14.
Global commodity trade separates supply from consumption by months of shipping. Australia and Brazil supply most of the world's iron ore, while China, Japan and South Korea consume over 80% of it. Importers therefore sign long-term contracts before they know the demand they will serve. Under the traditional fixed-price contract (FPC) the price is set at signing. Under the contingent-price contract (CPC) the price is pegged to an index and stays open until delivery, which exposes the importer to the index.
Conventional wisdom treats that exposure as a cost. Xing, Liu, Zhang and Zhao (Management Science, 2024) show a mechanism in the other direction. The unrealized CPC price is correlated with demand, so a firm's demand forecast also tells it something about its cost. They call this the price-learning effect. A larger price volatility strengthens it, and past a threshold a larger price volatility raises equilibrium profits. The model builds on the Gaussian duopoly literature on private information, which goes back to Vives (1984).
Two firms order a commodity and resell it in one market. With quantities , firm with rival faces the market-clearing price
Under the FPC the firm pays the known price , and under the CPC it pays . Its realized profit is , with or .
The noises are centered and jointly Gaussian. The pair has standard deviations and correlation . Firm observes the private signal , where . The pair has correlation and is independent of .
The relative price volatility is . The derived constants are
Each assignment of contracts gives a Cournot subgame: CC, CF, FC or FF, with the first letter firm 's. A strategy maps the firm's signal to a real quantity. A Bayesian Nash equilibrium is a profile from which no firm gains by deviating to any measurable, square-integrable strategy. The ex ante profit is the expectation of at the equilibrium of subgame .
Let and hold every parameter except fixed. Equilibria of CC and FC exist at every . In the CC subgame, on either side of ,
strictly so when . In the FC subgame with , and are strictly decreasing below, and strictly increasing above, the thresholds
The strictness hypothesis in (a) is a correction: the printed proposition omits it, and at equality is constant in . An instance is , , , , .
The result reverses the usual reading of volatility in procurement. Volatility is a cost only while it is small. Beyond in CC, firms lean on cost-side updating and their quantities track the contract price more closely. This is why the paper's later results, on contract choice, predict that significant price volatility pushes firms towards the CPC. The closed forms (6)–(8) also separate each profit into an efficiency component and an information benefit, which the rest of the paper uses.
The result is proved in the published paper, and no machine-checked proof of it is known to exist. The proofs are in the paper's Appendix, which is not part of the source file used here, so every statement of this mission was checked independently of them. Formalizing the result adds the correction to (a), and a complete account of the conventions the paper leaves implicit: the joint law of the noises, the sign of the quantities, and uniqueness up to null sets.
The monotonicity itself is elementary once (6)–(8) are known. The work lies before it, in two places.
The first is Gaussian regression for a four-dimensional law with correlated forecast noises, which gives Lemma 1.
The second is that the equilibrium quantifies over every admissible strategy, while the closed forms are affine. Solving the coefficient equations of the affine ansatz, the obvious first step, proves neither that the affine profile beats non-affine deviations nor that no non-affine equilibrium exists. Lemma 2 claims both, among strategies unrestricted in sign, so the corner analysis of ordinary Cournot models plays no role.
Everything is in the namespace CommodityCPC. BayesianGame is a general object: a prior, real signals, payoffs, admissible strategies, ex ante payoff and IsBNE. Params holds with their standing assumptions; are arbitrary reals. The volatility is a separate argument, and . The space is with four independent standard normals, and the noises are explicit linear forms in them, realizing the joint law above. The Lean name for is lam.
Quantities are real and unrestricted in sign. The paper's affine strategies are negative with positive probability, so a nonnegativity constraint would contradict Lemma 2, and its remark that standard deviations are "sufficiently smaller" than has no formal content. Equilibrium is ex ante, and uniqueness is -almost sure on .
A trivializing formalization is ruled out: the equilibrium and are primitives, never defined through (1)–(8), deviations are not restricted to affine strategies, and the goal includes existence so that its comparisons of equilibria are not vacuous.
The development needs Mathlib's Gaussian measures, conditional expectation and spaces. Gaussian regression for jointly normal vectors and the uniqueness argument for quadratic Bayesian games are reusable beyond this mission. Proofs of the goal, of any milestone, or of intermediate lemmas are welcome.
In two-stage robust optimization a decision maker fixes a here-and-now decision , an adversary then picks an uncertain parameter from an uncertainty set , and finally a wait-and-see decision is chosen with knowledge of . When the objective and constraints are linear in , a large toolbox is available: linear decision rules, Fourier–Motzkin elimination, Benders decomposition, column-and-constraint generation (Zeng and Zhao 2013). When enters through convex nonlinear functions , none of these applies directly, and even imposing a linear decision rule leads to maximizing a convex function over a polyhedron, which is NP-hard in general.
de Ruiter, Zhen and den Hertog (2023) show that for a polyhedral uncertainty set and fixed recourse the nonlinear problem is equivalent to a two-stage robust problem whose adjustable variable enters linearly. This extends the consecutive dualization of Bertsimas and de Ruiter (2016), which treats the linear case, to convex recourse.
Vectors are real column vectors. The data are a set ; functions and , , all convex; arbitrary real functions on , , , with rows ; affine maps and ; a recourse matrix ; and a nonempty polyhedral uncertainty set with , .
The primal problem (1) is
Write (primalValue) for the value of , the part.
The convex conjugate of is , and denotes its perspective, closed at . The dual uncertainty set is
and the dualized model (6) is with
(dualValue). Assumption 1 (relatively complete recourse) asks that for every and some satisfies the constraints of (1), strictly for each whose is nonlinear.
Under (2), (3), convexity and Assumption 1,
Both clauses are part of the goal: the feasible here-and-now decisions coincide, and so do the optimal values.
Model (6) is a two-stage robust problem in which the adjustable variable appears linearly and the convex structure of the recourse has moved into the new uncertainty set . Every technique for adjustable robust linear problems therefore applies to it. The paper uses (6) to derive a tractable linear-decision-rule approximation (8), to recover primal linear decision rules (Theorem 2) and to compute lower bounds from scenarios (Theorem 3). Each of these rests on the exact equivalence of Theorem 1. When all , and are affine, Theorem 1 coincides with Theorem 1 of Bertsimas and de Ruiter (2016).
The theorem is proved in the paper's e-companion; no machine-checked version exists. A formal proof checks the two-step duality chain in the extended reals, including cases the paper does not discuss: an unbounded (both values ), an empty (both values ), and constraints with affine , which need no strict feasibility.
The obvious argument is "Lagrange duality in , then LP duality in , then swap the two suprema", and each step needs care. Lagrange duality without a gap requires a constraint qualification. Assumption 1 gives only a refined Slater point, strict for the non-affine constraints and merely feasible for the affine ones, so the textbook Slater theorem, which demands strictness everywhere, does not apply. The conjugate of must be written as an infimal convolution of perspectives, including weights , where the naive convention gives the wrong set. LP duality must be used in its extended form, since the dual can be infeasible while the primal is unbounded. Finally, the notion of "feasible" in Theorem 1 must be the finiteness of the worst-case value: the scenario-wise reading (a for every , a for every -point) is false already for a one-dimensional instance with .
All vectors are Fin n → ℝ, the index is Fin (m1+1), and the rows , , are Fin m1, paired with f i.succ, g i.succ. The data are bundled in the structure DualTwoStageRO.Problem; convexity of the and nonemptiness of are hypotheses of the theorems. Every optimal value is in EReal: an infimum over an empty set is and a supremum over an empty set is , so no junk real value can make the goal vacuous. "Feasible for (1)" is and "feasible for (6)" is . The perspective of at is at and otherwise. "Nonlinear " is read as "non-affine ". is free. No dimension is assumed positive, may be unbounded, and is arbitrary. is the printed set; restricting it to points where the -problem is feasible, or computing values in ℝ with sSup/sInf, would trivialize or falsify the goal.
A complete development needs Lagrangian duality with a refined Slater condition, the conjugate of a sum of finite convex functions, and LP duality in the extended reals. All three are reusable beyond this mission. Proofs of the milestones and alternative routes to the goal are welcome.
Integer linear programs are NP-hard in general, and one of the best-known tractable classes is the one where is totally unimodular (TU): every square submatrix has determinant in . It is a long-standing open question whether integer programs with a -modular constraint matrix (full column rank, all subdeterminants bounded by in absolute value) are efficiently solvable for constant . Beyond the TU case, progress exists only for (Artmann, Weismantel and Zenklusen, STOC 2017), whose proof reduces bimodular programs to TU programs with a parity constraint.
A natural intermediate class is that of congruency-constrained TU problems: a TU system together with one constraint . For prime these are equivalent to integer programs whose subdeterminants lie in (p.1 of the paper). Nägele, Santiago and Zenklusen (arXiv:2109.03148) give the first algorithm beyond parity constraints.
Timeline:
Let be totally unimodular, , , . The CCTUF problem (congruency-constrained TU feasibility) with asks to show infeasibility of, or find a solution of,
The R-CCTUF problem replaces the single residue by a set of target residues: for some . The larger , the easier the problem; is an ordinary TU problem. The optimization version CCTU minimizes over the same set and must report infeasibility, unboundedness (arbitrarily small objective values) or a minimizer.
An algorithm is randomized in the paper's sense (footnote 4) if it always correctly reports infeasibility and finds a solution of a feasible problem with probability at least , the number of variables.
The goal fixes the modulus and nothing else: , and the integers are arbitrary, rows may repeat, and one program serves all instances.
Theorem 1 is the first polynomial algorithm for congruency-constrained TU problems beyond parity, and so the first result for the -subdeterminant integer programs mentioned above. Its general form, Theorem 2, climbs two steps of the hierarchy of R-CCTUF problems for every prime modulus; the recursion it introduces (patterns over pairs of scalar products, controlled with the Cauchy–Davenport inequality) is the paper's main methodological contribution. Theorem 1 is proved in the paper; nothing in it has a machine-checked proof. The formalization would add a cost model for integer algorithms with coins and oracles, Seymour's decomposition as an algorithmic statement, network matrices, and integer decomposition in TU cones, none of which exist on the platform in this form.
The natural algorithm guesses the two scalar products that couple the blocks of a 1-, 2- or 3-sum and recurses on both blocks. This is polynomial only when the decomposition is balanced; Seymour's theorem guarantees only two columns on the smaller side, so the recursion depth can be linear and the enumeration exponential. The paper avoids this by solving the small side completely, analysing the resulting pattern of feasible residues, and either progressing in the number of target residues (which needs prime) or replacing the small side by two variables. The base blocks rest on results from other papers: randomized exact-length circulations (Camerini–Galbiati–Maffioli) for network matrices, and congruency-constrained submodular minimization for their transposes. These are part of the proof, not assumptions, and have no Lean substrate.
All algorithmic statements use one machine, CongruencyTU.Machine: a RAM over integer registers with unit-cost , integer division and remainder (Lean's Euclidean conventions), comparison, indirect addressing, coin flips, an oracle instruction, and halting. Strongly polynomial means one program, fixed before the input, whose cost is at most and whose registers have bit length at most ; the bit-length clause is essential, since unit-cost multiplication would otherwise compute with exponentially long numbers. Integer remainder is unit-cost on purpose: with only and comparisons, Theorem 1 is false already for a fixed-dimension instance whose feasibility is . Randomness is a uniform coin string of length equal to the cost bound; probabilities are fractions of coin strings, compared in . "Constant modulus" means the program may depend on but not on the instance. Instances are lists of integers (dimensions, the matrix row by row, , , or ), and outputs are for "infeasible" or for a solution .
No cited algorithm (Tardos' strongly polynomial LP algorithm, Camerini–Galbiati–Maffioli, Nägele–Sudakov–Zenklusen, Seymour's decomposition algorithm) appears as a hypothesis: a statement assuming them would be conditional. Theorem 22 is an oracle reduction, quantified over every oracle that solves the smaller problems. Lemma 8 is stated with singleton intervals allowed, since the printed version (strict ) is false for , , .
Problems of form (1) are given with totally unimodular 3-sum summands; network matrices use a spanning tree on ; the core of Definition 51 is any submatrix reached by deletions to which no deletion applies. Contributions are welcome on every layer: the cost model's basic programs (arithmetic on lists, Gaussian elimination with bounded bit sizes), Tardos' algorithm, Seymour's decomposition, network-matrix recognition, the combinatorial lemmas (Lemmas 8, 57, Theorem 19), and the pattern analysis.
Systems that serve jobs with deadlines and can adjust their capacity on the fly, such as electric-vehicle charging stations and cloud data centers, pay for both the level and the volatility of the resource they draw. A charging station that buys energy on the day-ahead market needs a predictable power draw, and peaks strain the grid. Nakahira, Ferragut and Wierman (arXiv:2004.12280v2, 2020; Operations Research, 2023) ask which distributed scheduling rule, one that sets each job's service rate from that job's own remaining demand and remaining time, minimizes the stationary variance of the total service capacity. They also allow demands and deadlines to be violated at a price.
Before this paper, optimality results for such schedulers were known only in special settings: a static single server, or deterministic worst-case models. The paper's results are exact and in closed form for stationary Poisson arrivals: Exact Scheduling (Theorem 1), a rate cap at for soft demands (Theorem 2), a rate cap at with deadline extension for soft deadlines (Theorem 3), and their combination, Generalized Exact Scheduling (Theorem 4).
A job has an arrival time , a service demand and a sojourn time , so its deadline is . The job types lie in a bounded set and have a probability law on . Jobs arrive as a Poisson random measure on with intensity : arrivals at rate on , with independent types.
A rate profile is the service rate of a job of type when its remaining time is (form (14)); starts at and becomes negative after the deadline. A job served by receives units of service, and its deadline extension is . The service capacity is the sum of the rates of all jobs present at time . With a unit cost per unit of unmet demand and per unit of extension, the objective is
the stationary variance of plus the long-run rates of the two penalties. A policy of form (4) is a function of remaining demand and remaining time ; it produces a rate profile through the trajectory of each job.
With equal to if , to if and , and to if and :
attained by the profile (96), which Generalized Exact Scheduling (25) produces along every trajectory. If , the minimizer is unique almost everywhere.
Theorem 4 says that the optimal trade-off between capacity volatility, unmet demand and late completion is decided job by job, from local information only. A job is served at its flat rate when that rate is below both thresholds. Otherwise the rate is capped at and part of the demand is dropped, when demand is the cheaper constraint to violate, or it is capped at and the deadline is extended. The closed form of the optimal cost gives the exact value of relaxing each constraint, and it contains Theorems 1 to 3 as special cases.
The result is proved in the paper; nothing here is open. Nothing in it is machine-checked. A formalization would add to the library a Poisson random measure with Campbell's first- and second-moment formulas, the variance formula for an infinite-server system with time-varying rates (a form of Brumelle's formula), and a complete optimality proof for a stochastic scheduler. Three printed statements are corrected along the way (next section), so the formal version is also the first correct statement of the theorem.
The obvious argument is to minimize job by job with Cauchy–Schwarz, and that is the core of the proof. It is not the whole proof. First, the variance of must be computed from the point process: Campbell's formula for a random measure needs simple-function approximation together with independence on disjoint sets, and Mathlib has neither the formula nor the random measure. Second, the penalties cannot be read at a fixed time. sums over jobs whose deadline is exactly , which is almost surely empty, so a literal reading makes serving nothing free; the objective must use long-run rates. Third, the uniqueness clause requires an equality analysis of the per-job minimization, which is not unique at . Fourth, realizing the optimal profile by a policy of form (4) is an ODE statement with a singular right-hand side as and a discontinuous one at after the deadline.
Arrival times range over and stationary quantities are limits as : is the of the -valued variance of , and each penalty is the of . Lemma 2 and (81) prove that these are limits. The continuity equation (5) is not formalized. Sums over jobs are integrals against . Costs live in , and the extension is an -valued supremum, so a job served forever costs . Feasibility contains (constraint (80)). The mark law is any probability measure on , not necessarily a density. The lower bound ranges over all measurable rate profiles of form (14), which contain the realized rates of every policy of form (4).
Three printed statements are false and are corrected. The third line of (25) reads " otherwise", which keeps serving a job after its deadline when and costs instead of at ; the corrected policy stops at the deadline in that regime. The indicators of (26) are reversed, and they are replaced by those matching (25) and (96). Theorem 7 assumes only , which does not give absolute convergence, so the formula carries the added hypothesis . Uniqueness is claimed only for , where it holds.
and the penalty rates are computed from the point process and never defined by their closed forms, which are milestone conclusions. A definition of as would make Lemma 2 trivial and is excluded. Existence of a Poisson random measure is classical but not in Mathlib; contributions constructing one, or proving Campbell's formula, are reusable well beyond this mission.
Active disturbance rejection control (ADRC) is a feedback design in which an observer estimates, in real time, not only the state of an uncertain plant but also its total disturbance: the combined effect of unmodelled dynamics, external disturbances and the mismatch between the true and the nominal control gains. The controller cancels this estimate and then applies a nominal stabilizing law. The method is used in motion control, power electronics, chemical process control and MEMS gyroscopes, and its practice ran well ahead of its theory. Before this paper, global convergence of a closed loop with a nonlinear ADRC had been proved only for a class of SISO systems without zero dynamics (Guo–Zhao, CCDC 2012, reference [9] of the paper), the nonlinear observer alone had been analysed without feedback (Guo–Zhao 2011), and semiglobal results existed for linear observers. Guo and Zhao (SIAM J. Control Optim. 51 (2013)) treat MIMO systems with zero dynamics and nonlinear observers, and prove a global convergence theorem, Theorem 3.1, which is the goal of this mission.
The plant has subsystems. Subsystem has states in a chain of integrators driven by an unknown function and by the controls :
where is the zero dynamics and a bounded disturbance with bounded derivative. The gains are unknown; the designer knows an invertible nominal matrix with inverse . The reference is a signal with , typically produced by a tracking differentiator.
The extended state observer (ESO) has states and gain :
with . The feedback ADRC(G) is , , where and defines a stable reference model. The last observer state estimates the extended state .
Assumption A2 gives Lyapunov functions for the observer error dynamics, A3 gives Lyapunov functions for the reference model, GA1 bounds the derivatives of , GA3 bounds the growth of , and condition (3.1) says the gain mismatch is small:
There are , depending on the signals only through a bound on them, such that for some , every and every solution, eventually
The goal fixes no constant: it asserts the shape, uniform in the initial value.
The milestones follow the proof: the error equations (3.6); the bound (3.9) on the derivative of the extended state; the Lyapunov estimates (3.15), (3.17) and the two-case sign lemma (3.18)–(3.20); then, given an a priori bound on , the estimates (3.21), (3.23), (3.25) for the observer error; and, given , the estimates (3.27), (3.29) for the tracking error.
Theorem 3.1 is a global separation principle for nonlinear ADRC: a high-gain observer and an observer-based feedback can be designed separately, and from any initial value the closed loop tracks the reference with error while the observer recovers the total disturbance. The paper's examples (Example 5.1, Proposition 5.3 on linear output regulation) use it to design observers.
No ADRC or extended-state-observer result is formalized on the platform or, to our knowledge, elsewhere. A complete development would be the platform's first convergence proof for a closed-loop observer and controller.
As printed, the theorem needs three corrections, each forced by a counterexample that satisfies every printed assumption. (i) GA2 lets the gains vary in time while may grow. With , , , , , , , simulation of the closed loop at shows growing linearly in . The formalization takes constant. (ii) In (3.1), appears with its sign. Replacing by leaves the loop unchanged and flips the sign of the sum, so with , the printed condition holds while the closed-loop matrix has an eigenvalue at . The formalization uses . (iii) A1 bounds only, but the feedback uses and the proof uses . A reference with spiking at late times breaks the observer bound, so the formalization bounds all components and . Two readings complete the setting: , since the printed makes A2 unsatisfiable, and positivity of . Several displays of the proof also carry slips ((3.13) drops a term from , (3.16)–(3.20) write for , (3.23) lacks the initial-value factor); the milestones state the corrected versions.
The proof is a chain of ODE estimates with explicit constants, but three steps are hard. First, the bound (3.9) requires differentiating the extended state along the closed loop across coupled subsystems; as printed, the computation (3.8) has sign and term slips. Second, the paper passes from " outside the ball of radius " to " eventually", which does not follow: a decreasing confines the solution to a sublevel set of , not to the ball. The proof needs an -independent ultimate bound obtained by a sublevel-set argument, and this step is not posed as a milestone. Third, is only Lipschitz, so the extended state is only locally Lipschitz in time. The comparison arguments for and must work almost everywhere, and is not differentiable where .
Indices are 0-based (Fin (n i), Fin (n i + 1), with the page's at Fin.last). All vectors live in EuclideanSpace, so every norm is Euclidean, as in the factor of (3.1). Solutions are trajectories with one-sided derivatives within (HasDerivWithinAt … (Set.Ici 0)), and the theorem quantifies over every solution with a free initial value. The time derivative is never a Lean deriv: milestones about it hold "for every derivative, wherever one exists". Minima and maxima over subsystems are Finset.inf'/sup' over the nonempty Fin m.
The goal is not trivial. are chosen before , the solution and the signals, and no boundedness of the solution is assumed. A proved sanity check exhibits data satisfying every hypothesis together with a solution of the closed loop.
The definitions layer holds the data structure, Assumptions A2 and A3, the hypothesis bundle, the closed loop, the error coordinates and the constants . Reusable beyond this mission: comparison lemmas for under almost everywhere, and a Lipschitz chain rule bound for derivatives of . Proofs of any milestone, of the missing ultimate-boundedness step and of the goal are welcome.
Overproduction is a central environmental problem of the fashion industry: garments and fabric that do not sell, called deadstock, are commonly incinerated or sent to landfill, and most of a garment's footprint comes from making the fabric. Quick response, in which finished goods are produced after demand is observed, is widely promoted as a remedy because it reduces excess production of finished goods. Long and Gui ask what quick response does upstream, to the amount of fabric a firm buys. Their first main finding is that a firm with quick response holds fewer leftover finished goods but more leftover fabric, and that total deadstock goes up. The operational value of quick response is studied by Fisher and Raman (1996) and Cachon and Swinney (2011), among others; the question here is its environmental side.
A firm sells one product at a fixed price . The market size is random with cdf on support , and a realization gives demand . Fabric costs per unit, regular production costs per unit, and . One unit of product uses one unit of fabric.
In the benchmark model the firm chooses fabric and production with before is known, and earns
In the quick response model the firm may also produce from leftover fabric after seeing , at the higher unit cost with . Its stage-2 rule is if , and otherwise, and it earns
Optimal decisions and are the maximizers of these profits. Deadstock finished goods are in model . Deadstock fabric is with quick response, and in the benchmark model, where all fabric is used.
For every ,
and as decreases, decreases while and increase. The goal is stated for every admissible law of and asserts that optimal decisions exist.
The result separates two effects that public discussion merges: quick response reduces waste at the finished-goods stage and increases it at the fabric stage, and the second effect dominates. The paper builds on this in its life cycle analysis and in its study of upcycling and of waste-reduction policy. A policy maker who counts only leftover garments would reach the opposite conclusion.
The result is proved in the paper; no machine-checked proof is known, and a search of this platform found neither this statement nor its model. Formalizing it adds a two-stage newsvendor with a raw-material stage and recourse production, over a general continuous demand law, with exact comparative statics in the recourse cost. The platform's existing newsvendor results concern other models.
The natural first argument is that quick response matches supply to demand, so every kind of leftover should fall. It fails because the firm's fabric order is itself a decision, and the option to produce later raises the value of holding fabric. A comparison of the two models therefore has to compare optimizers of two different problems, across a regime change at .
Three obstacles are specific to formalization. The problem is a constrained two-variable maximization whose constraint binds in one regime and is slack in the other, and the case changes the objective itself. The law of is assumed to have no atoms but need not have a density, whereas the paper's proofs differentiate integrals against . Strictness and uniqueness rest on the support condition and do not hold for a general cdf.
The law of is a probability measure on , with the Mathlib cdf μ. The paper's phrase "on support " is read as: , is carried by , charges every open subinterval of , and has no atoms. Continuity of is needed for the fractile equations to have solutions. The parameter structure also records , and , which the model implies.
Decisions range over . Optimal decisions are maximizers of the expected profits and are never defined by critical-fractile formulas, which would make most targets arithmetic. The benchmark fabric deadstock is defined as the unused fabric at a decision, so at the optimum is a consequence. Statements hold for every optimal pair; existence is asserted separately, so they are not vacuous.
"Decreases" and "increases" in are weak over all , because the quantities are constant on . The targets add strictness for with , which is what the paper's proof shows.
A complete development needs a newsvendor library for a general law on a bounded interval: properties of and , and quantiles of a continuous cdf. That library is reusable beyond this mission. Contributions of such general lemmas are welcome, as are proofs of the milestones in any order.
Fresh produce is perishable, and its demand depends on how fresh it is. A grocery retailer that orders strawberries before demand is realized does not, in a traditional supply chain, know how long ago the batch was harvested or how it was stored, so the freshness of what she sells is itself a source of demand uncertainty. Blockchain-based traceability systems, such as the food traceability platform that Walmart and IBM launched on Hyperledger Fabric, record that upstream information and make it visible to the retailer before she orders. Keskin, Li and Song (Management Science, 2024) ask how much such freshness transparency is worth to the retailer, and answer it in closed form in a newsvendor model with normally distributed freshness and demand shocks. Their Theorem 1 is the paper's headline profit result; the later sections (food waste, smart contracts, pricing, dual sourcing) build on the same model.
A retailer sells a perishable product over one period. She orders units at the unit wholesale price , sells at the unit retail price , loses unmet demand, and salvages each leftover unit at the unit salvage value (possibly zero or negative). With demand her profit is
Demand depends on the freshness state of the batch:
with and the demand shock independent, baseline demand and freshness sensitivity . Write and for the standard normal density and distribution function, for the critical ratio, for the safety factor, and for the standard deviation of .
The blockchain retailer observes before ordering. She maximizes and earns ; her expected profit is . The traditional retailer knows only the distribution of ; she maximizes and earns .
All four clauses are part of the goal, for every admissible parameter tuple.
Theorem 1 turns the value of information into a single formula. The profit gain from transparency is proportional to the reduction in the standard deviation of the demand the retailer plans against, scaled by the overage–underage cost and by . It is strictly positive for every parameter tuple, and its comparative statics (Proposition 1: increasing in and , decreasing in ) follow by differentiation. The expected-sales computations of its proof are reused verbatim in the proof of the paper's food-waste result (Theorem 2, p.ec12), so a formal version of Theorem 1 and its milestones is the base for the rest of §2.
The result is proved in the paper; nothing here is open. To the best of current knowledge none of these statements has a machine-checked proof. The mission produces: a formal newsvendor profit with salvage and real-valued orders; the normal partial-expectation identities of Lemma EC.1, which recur throughout inventory theory; a formal proof that the critical-fractile order is the unique optimum for normal demand; and the closed-form value of freshness transparency.
The computation in the paper is short, but it rests on facts that are routine on paper and not available as such in Lean. The newsvendor optimality step is a first-order condition for an expected profit whose integrand is not differentiable in , and uniqueness of the optimum depends on the normal distribution function being strictly increasing. Lemma EC.1 is an improper integral of against the Gaussian density, which Mathlib provides only as a measure and a density, not as these partial expectations. Case 2 needs the law of , which combines affine images of Gaussians with the convolution of independent Gaussians. Case 1 then needs to be integrable, which holds only because is affine in ; the supremum in the definition must first be shown to be attained, or the integral is of an unknown function. A first idea, applying a generic "newsvendor critical fractile" lemma, does not apply verbatim: the order quantity ranges over all of and the salvage value may be negative.
Lean namespace BlockchainNV. The parameters and their standing inequalities form a structure Params (, , , , , , ). The random model IsModel places and on an arbitrary measurable space with HasLaw X (gaussianReal μX (σX^2).toNNReal) P, HasLaw ε (gaussianReal 0 (σ^2).toNNReal) P and IndepFun X ε P; Mathlib's Gaussian takes the variance. is gaussianPDFReal 0 1 and is cdf (gaussianReal 0 1). The safety factor is a real z with the hypothesis , which determines it. and are sSup of the expected profit over all ; milestones 4 and 9 assert that the suprema are attained maxima, so the sSup is not Lean's junk value. is the Bochner integral . The order quantity and the demand are unrestricted reals, as in the paper's base model: restricting would change for small and falsify the first clause.
The positivity of and is not optional: with the Gaussian becomes a Dirac mass and . Clause 3 follows from clauses 1–2 by algebra and clause 4 from ; the content of the goal is in clauses 1 and 2.
Infrastructure that a complete development needs and that is reusable beyond this mission: the normal partial expectations, the first-order optimality of the newsvendor with general salvage value, and the law of an affine combination of independent Gaussians. Contributions of any of these as standalone lemmas are welcome.
A classical Markov decision process (MDP) chooses a policy that maximizes the expected cumulative reward. In many applications the expectation is the wrong summary: a clinician choosing when to start a treatment, or an investor facing ruin, cares about the bad outcomes, and two policies with equal means can have very different lower tails. A natural replacement is a quantile of the cumulative reward: maximize the reward level that is exceeded with probability at least . This is the value-at-risk criterion of finance, and the median for .
Expectations decompose additively over time, which is what makes backward dynamic programming work for the classical MDP (Bertsekas 1995). Quantiles do not: the quantile of a sum is not the sum of quantiles, and the quantile-optimal policy in general depends on the whole history, not only on the current state. Li, Zhong and Brandeau (Operations Research, 2022) show that a dynamic program still exists if the value function is indexed by both the state and the quantile level. This mission formalizes that result.
A model on a finite state set and a finite action set consists of transition laws on , rewards depending on the current state, the action and the next state, and nonempty sets of admissible actions, for every time . The laws and rewards may change with (the model is non-stationary).
A policy is deterministic and history dependent: maps the state history to an admissible action . Over a horizon and from a start state , the policy induces a law on state paths and hence a law on the cumulative reward .
For a law on and , the -quantile is ; the endpoints are the essential infimum and the essential supremum . The optimal value function is
and the intermediate value is the same maximum over policies whose first action is .
The one-step problem is
The variable is the quantile level assigned to the branch .
Set and for . Then for every model, every horizon , every start state and every ,
the maximum over all admissible history-dependent policies being attained.
Theorem 2 turns a maximization over history-dependent policies, a set whose size grows exponentially in , into a backward recursion whose state is a pair . The recursion produces the whole function at each stage, so one pass gives the optimal quantile value for every start state and every level at once. This is the basis of the paper's algorithm (§4), its augmented-state optimal policy (Theorem 3), its CVaR extension (Theorem 4) and its infinite-horizon results (Theorems 6–7). Lemma 2, the quantile of a mixture as an optimization over component levels, is a statement about random variables that does not involve MDPs and can be used on its own.
The paper's proofs are in an appendix that is not part of the cited preprint artifact, and none of these results has a machine-checked proof. Formalizing them also fixes the statement: as printed, the budget makes Lemma 2, Theorem 1 and Theorem 2 false at boundary levels (a one-step example with rewards and of probability each gives the value at , while the true median is ). The mission states the corrected problem with a strict budget, which coincides with the printed one at .
The obvious argument, conditioning on the next state and optimizing the continuation separately, works for expectations because is linear. For quantiles the decomposition is Lemma 2, and the delicate part is the boundary: which levels are allowed, how atoms of the component laws interact with the budget, and what happens at and , where the quantile becomes an essential infimum or supremum. The printed budget gets exactly this wrong.
The second difficulty is the policy class. The optimal policy is history dependent, so the interchange "maximum over policies of a minimum over branches equals the minimum over branches of the maximum over continuation policies" requires that the continuations after different next states can be chosen independently, and that the resulting supremum is attained. A Markov-policy formalization would state a different and generally false theorem.
All values are in EReal; there is no junk value for empty or unbounded suprema. The quantile uses footnote 1's essential infimum and supremum at . The model is given by kernels P : ℕ → S → A → PMF S, rewards r : ℕ → S → A → S → ℝ and admissible sets adm : ℕ → S → Set A that are nonempty; S and A are Fintypes. The paper's formulation of Assumption 1 induces exactly such a model, and every such model is one. Policies are (t : ℕ) → (Fin (t+1) → S) → A. The law of the cumulative reward is a finite sum of Dirac masses over state paths starting at . The time- value uses the model shifted by , with a fresh policy whose histories start at . The recursion value dpValue and the optimal value optValue are distinct definitions; Theorem 2 identifies them at .
The goal is stated as IsGreatest, covering every horizon including and every , endpoints included. opt is an EReal supremum, so Lemma 2, Theorem 1 and (6) also state that the page's maxima are attained. It cannot be met by a degenerate encoding: an admissible policy always exists, and the reward law is a probability measure. A verification file checks that the printed budget gives on the counterexample while the corrected one gives at most .
Reusable beyond this mission: the EReal quantile with its Lemma 1 properties, and Lemma 2 as a statement about mixtures. Contributions welcome: proofs of Lemma 1 and Lemma 2, the law decomposition (7), and the induction combining Theorem 1 and (6).
This paper develops systematic approaches to obtain -divergence inequalities, dealing with pairs of probability measures defined on arbitrary alphabets. Functional domination is one such approach, where special emphasis is placed on finding the best possible constant upper bounding a ratio of -divergences. Another approach used for the derivation of bounds among -divergences relies on moment inequalities and the logarithmic-convexity property, which results in tight bounds on the relative entropy and Bhattacharyya distance in terms of divergences. A rich variety of bounds are shown to hold under boundedness assumptions on the relative information. Special attention is devoted to the total variation distance and its relation to the relative information and relative entropy, including "reverse Pinsker inequalities," as well as on the divergence, which generalizes the total variation distance. Pinsker's inequality is extended for this type of -divergence, a result which leads to an inequality linking the relative entropy and relative information spectrum. Integral expressions of the Rényi divergence in terms of the relative information spectrum are derived, leading to bounds on the Rényi divergence in terms of either the variational distance or relative entropy.
This mission is the statement-level formalization of -divergence Inequalities (arXiv:1508.00335v7). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
66 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: Functional domination: Df<=kappa_bar Dg, and if f and g are differentiable at 1 with both derivatives zero, the supremal ratio equals kappa_bar (Theorem 1, PDF p. 13). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
10 results of the paper are not stated yet, because the library lacks an interface they need:
We consider a class of evolution equations in Lindblad form, which model the dynamics of dissipative quantum mechanical systems with mean-field interaction. Particularly, this class includes the so-called Quantum Fokker-Planck-Poisson model. The existence and uniqueness of global-in-time, mass preserving solutions is proved, thus establishing the existence of a nonlinear conservative quantum dynamical semigroup. The mathematical difficulties stem from combining an unbounded Lindblad generator with the Hartree nonlinearity.
This mission is the statement-level formalization of Quantum dynamical semigroups for diffusion models with Hartree interaction (arXiv:math-ph/0309052v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Quadratic position–momentum operators: minimal and maximal realizations coincide (Lemma 3.3; (3.8)–(3.9), PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
12 results of the paper are not stated yet, because the library lacks an interface they need:
We present a spectral sequence connecting the continuous and 'locally continuous' group cohomologies for topological groups. As an application it is shown that for contractible topological groups these cohomology concepts coincide. Similar results for k-groups and smooth cochains on Lie groups are also obtained.
This mission is the statement-level formalization of A Spectral Sequence Connecting Continuous With Locally Continuous Group Cohomology (arXiv:1110.0994v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Introduction, unnumbered theorem; Corollary 3.17: contractible-group comparison (Introduction, unnumbered theorem; Corollary 3.17: contractible-group comparison, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
97 results of the paper are not stated yet, because the library lacks an interface they need:
We define submersions f between manifolds M and N modelled on locally convex spaces. If the range N is finite-dimensional or a Banach manifold, then these coincide with the naive notion of a submersion. We study pre-images of submanifolds under submersions and pre-images under mappings whose differentials have dense image. An infinite-dimensional version of the constant rank theorem is provided. We also construct manifold structures on homogeneous spaces G/H of infinite-dimensional Lie groups. Some fundamentals of immersions between infinite-dimensional manifolds are developed as well.
This mission is the statement-level formalization of Fundamentals of submersions and immersions between infinite-dimensional manifolds (arXiv:1502.05795v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Regular locally convex manifolds embed into a point-indexed product (Theorem J, PDF p. 9). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
29 results of the paper are not stated yet, because the library lacks an interface they need:
This paper classifies the blocks of the cyclotomic Hecke algebras of type G(r,1,n) over an arbitrary field. Rather than working with the Hecke algebras directly we work instead with the cyclotomic Schur algebras. The advantage of these algebras is that the cyclotomic Jantzen sum formula gives an easy combinatorial characterization of the blocks of the cyclotomic Schur algebras. We obtain an explicit description of the blocks by analyzing the combinatorics of `Jantzen equivalence'. We remark that a proof of the classification of the blocks of the cyclotomic Hecke algebras was announced in 1999. Unfortunately, Cox has discovered that this previous proof is incomplete.
This mission is the statement-level formalization of Blocks of cyclotomic Hecke algebras (arXiv:math/0607451v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Cyclotomic and affine block membership coincide (Theorem A, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
14 results of the paper are not stated yet, because the library lacks an interface they need:
This paper introduces the notion of calibrated representations for affine Hecke algebras and classifies and constructs all finite dimensional irreducible calibrated representations. The main results are that (1) irreducible calibrated representations are indexed by placed skew shapes, (2) the dimension of an irreducible calibrated representation is the number of standard Young tableaux corresponding to the placed skew shape and (3) each irreducible calibrated representation is constructed explicitly by formulas which describe the action of each generator of the affine Hecke algebra on a specific basis in the representation space. This construction is a generalization of A. Young's seminormal construction of the irreducible representations of the symmetric group. In this sense Young's construction has been generalized to arbitrary Lie type.
This mission is the statement-level formalization of Calibrated representations of affine Hecke algebras (arXiv:math/0401323v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Explicit construction, dimension, and classification (Abstract; Theorems 3.1 and 4.5, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need:
We define the notion of {\em classifying space} of a topological stack and show that every topological stack \X has a classifying space X which is a topological space well-defined up to weak homotopy equivalence. Under a certain paracompactness condition on \X, we show that X is actually well-defined up to homotopy equivalence. These results are formulated in terms of functors from the category of topological stacks to the (weak) homotopy category of topological spaces. We prove similar results for (small) diagrams of topological stacks.
This mission is the statement-level formalization of Homotopy types of topological stacks (arXiv:0808.3799v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Restriction of an adjunction to full subcategories (Lemma 7.4, PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
59 results of the paper are not stated yet, because the library lacks an interface they need:
Bike-sharing systems such as New York's Citi Bike place bikes in docks at fixed stations. Over a day, demand pushes bikes away from some stations and toward others, and customers who find no bike, or no empty dock to return one, leave dissatisfied. Operators rebalance bikes by truck overnight, but the number of docks at each station is a strategic decision that can be changed only rarely and at a cost. Freund, Henderson and Shmoys (arXiv:1611.09304, Operations Research 2022) model this decision as a discrete optimization problem over the allocation of docks and bikes, show that the station costs have a discrete-convexity property called multimodularity, and give a discrete gradient-descent algorithm that solves the problem exactly, also under a limit on the number of docks that may be moved. The analysis was used with data from Citi Bike to recommend dock reallocations.
The model is general: the algorithm and its proof use only multimodularity of the station costs, so the result is a statement about minimizing separable multimodular functions under budget and movement constraints.
There is a finite set of stations. An allocation puts empty docks and bikes at station , so station has docks. A customer arriving at a station either rents a bike () or returns one (); a renter at an empty station, or a returner at a full one, is dissatisfied. For an arrival sequence , the user dissatisfaction function counts the dissatisfied customers when the station starts with empty docks and bikes. A demand profile is a probability distribution over arrival sequences, and the station cost is .
A function is multimodular if, wherever the arguments are nonnegative,
Station must hold between and docks. With a bike budget and docks in total, an allocation is feasible for problem (P3) if every station is within its bounds, , and . The objective is . The dock-move distance between two allocations is , the number of docks to be moved, irrespective of bikes. Problem (P2) adds the operational constraint that the solution be within dock-move distance of the current allocation .
A dock-move from to moves one empty dock (), one full dock (), one dock from to together with a bike from a third station to (), or one dock from to while a bike moves from to (). The neighborhood consists of all results of one dock-move. An allocation is bike-optimal if no reallocation of bikes with the same docks at every station is better.
Algorithm 3 first places bikes optimally for the current docks with a greedy routine (Algorithm 1), giving , and then repeatedly moves to the best allocation in the neighborhood (Algorithm 2), stopping when no neighbor is better. Its iterates are .
For every finite set of stations with multimodular costs, every feasible start and every run of Algorithm 3 (any tie-breaking), and every :
and moreover a stationary iterate is optimal for (P3), is optimal for (P3), and the run is constant from iteration on. With this solves (P2) for every movement budget with a single run.
The milestones follow the paper's proof: multimodularity of the station UDF (Lemma 2.1) and of the depot cost; the implied inequalities (4)–(6); convexity in the number of bikes (Fact 1) and the exchange property of separable convex functions (Fact 2); correctness of Algorithm 1; preservation of bike-optimality by a best dock-move (Lemma 3.1) and along the run; the station inequalities used in Lemma 3.3; the exchange Lemma 3.3; Lemma 3.2 and the optimality of local optima for (P3); Lemma 3.4 (local optimality in the next ball); and Lemma C.1.
Theorem 1 says that one greedy run answers every movement budget at once: the -th iterate is the best allocation reachable by moving docks. This makes the trade-off between reallocation effort and customer dissatisfaction computable as a whole curve, which is how the paper's case studies use it. The theorem also underlies the paper's faster scaling algorithms (Theorems 2 and 3), whose proofs build on it.
The result is proved in the paper; it has no machine-checked proof. The proof history is instructive: the authors' earlier version derived Theorem 1 from the claim that local optima inside the ball are optimal in the ball, which is false (Remark, p.20, citing a counterexample of Shioura 2018, who also gives an alternative correctness proof through M-convexity). A formal proof would settle the corrected argument. The formalization also repairs two printed statements: Definition 1's convention , under which Lemma 2.1 fails, and the gloss of "next choice of the gradient-descent algorithm" in Lemma 3.4.
The obvious argument is: each step is a best local improvement, a local optimum is globally optimal (Lemma 3.2), hence each iterate is optimal in its ball. This fails, because a neighbor of a ball optimum that improves may leave the ball, and local optimality inside a ball does not imply optimality in the ball. The paper's proof instead takes a better allocation closest to and applies the exchange Lemma 3.3 to rather than to , then rules out both places the exchanged allocation can lie. Lemma 3.4 alone runs five pages: a dock-move out of can interact with the up to three stations changed in the previous step in many ways, each handled by a chain of the multimodular inequalities.
Stations form a Fintype S with decidable equality. Costs are real functions g i : ℤ → ℤ → ℝ, multimodular on the quadrant; the paper's value off the band is replaced by requiring feasibility (Feasible) of every allocation compared. Allocations are integer vectors with explicit nonnegativity. "Dock-move distance at most " is dockGap a a₀ ≤ 2 * r, where dockGap sums the absolute differences of dock counts. Algorithms 1–3 are relations, so every tie-breaking is covered, and a stopped run is a constant sequence. Neighbors move a dock between two distinct stations. The ball is centered at the initial allocation.
The goal is stated for any family of multimodular costs; it specializes to the paper's problem through Lemma 2.1 and the depot lemma. It cannot be trivialized: the verification file shows a run of Algorithm 3 that moves, under multimodular costs and a feasible start, and the multimodularity hypothesis is on the whole quadrant, not only on the band (the band reading makes Theorem 1 false).
Everything is built on Finset.sum, Relation.ReflTransGen and PMF; no discrete-convex-analysis library is required. Contributions are welcome on any milestone: the inequality lemmas (Fact 1, the implied inequalities, the station inequalities) are short and reusable for other multimodular-cost models, Fact 2 is a general lemma on separable convex resource allocation, and Lemmas 3.3 and 3.4 carry the combinatorial core.
Most real-options models of capacity investment assume that the firm finances the outlay at the risk-free rate, or that capital comes from a competitive market. Many firms, in particular young and small ones, have no equity and borrow from a lender with market power. Huberts, Wen, Dawid, Huisman and Kort (Management Science, 2025) model this as a dynamic game. The lender announces a coupon scheme, the coupon rate it will charge as a function of the demand level at which the firm invests. The firm then chooses when to invest and how much capacity to install. Without a bankruptcy option, the paper solves the game in closed form (Proposition 1). The timing is the same as under internal financing (Huisman and Kort, 2015), but the capacity is halved. This is a dynamic, financial counterpart of the static double marginalization of successive monopolies (Spengler, 1950).
The paper connects two literatures. One is real options with capacity choice (Dixit and Pindyck, 1994; Huisman and Kort, 2015). The other is debt financing of investment, with endogenous default following Leland (1994). Earlier models in which the input supplier has market power (de Villemeur, Ruble and Versaevel, 2014) fix the size of the investment. In this model the size is a choice as well.
The demand level is a geometric Brownian motion , where is a standard Brownian motion and . The inverse demand is . After installing capacity at unit cost , with the outlay borrowed from the lender, the firm earns the profit flow , where is the coupon rate. Payoffs are discounted at the risk-free rate . The parameters satisfy , , , and .
In the no-bankruptcy scenario the firm pays the coupon forever. At an investment level and a finite coupon :
A coupon scheme takes values in , where means that financing is refused. The firm uses an investment threshold : starting from it waits until demand first reaches , at the time , and otherwise it invests at once. Its payoff is or , and the lender's payoff is defined in the same way with . Finally, is the larger root of .
With , the lender's optimal coupon scheme is
from every initial demand level, against every optimal response of the firm. Under this scheme the firm waits until demand reaches (the unique optimal threshold) and invests immediately above it, with capacity . At the trigger,
These are steps of the proof, each anchored to the body text that defines or asserts the object.
Proposition 1 makes the cost of external financing with a market-powered lender explicit. The coupon rate exceeds the risk-free rate, the capacity is half of what an internally financed monopolist installs, and the timing does not change. Two effects cancel exactly: a higher coupon delays investment, while the coupon's dependence on the investment level accelerates it. As a result, welfare is lower than under internal financing (Table 1 of the paper). The no-bankruptcy case is also the benchmark for the bankruptcy-option analysis of §3.2 and §4, which the paper carries out numerically.
The proposition is proved in the paper's Online Appendix. This mission formalizes the statement and the proof steps named in the body. None of it has a machine-checked proof yet. Milestone 1, the first-passage Laplace transform of a geometric Brownian motion, is a standard fact that is used throughout real-options theory and is reusable beyond this mission.
The calculus is elementary once milestones 1 and 2 are available. The difficulty is in the probability and in the game. Milestone 1 needs optional stopping for the martingale in continuous time, including on paths that never reach the level when . Mathlib's optional stopping theorem is stated for discrete time. Milestone 2 needs Fubini–Tonelli and the moment .
The game has a second source of difficulty. The lender's optimality ranges over every coupon scheme, including schemes for which the firm's best threshold is not where the lender wants it. A first attempt maximizes the lender's value pointwise in the coupon. That fails, because the pointwise maximizer need not induce the firm to invest at the lender's preferred level. The proof has to show that, without bankruptcy, the firm's and the lender's preferred thresholds under coincide.
All objects are in the namespace DebtDoubleMarg. The Brownian motion is Mathlib's ProbabilityTheory.IsBrownianReal (time ) on an arbitrary probability space. The geometric Brownian motion is its explicit exponential. The hitting time is a pathwise infimum in , and its discount factor is when the level is never reached. Coupons live in WithTop ℝ, and an infinite coupon gives both players zero. The firm's strategies are thresholds, as in the paper (p.6, endnote 6). is a chosen maximizer, whose existence and uniqueness are milestone 3. Only the paper's no-bankruptcy scenario (Proposition 1) is formalized. Propositions 2–5 and the numerical Results concern the bankruptcy option and are out of scope.
None of the payoffs (, , , , , firm-optimality) is defined by its closed form. Each is defined by its expectation or its optimization problem, so the goal cannot be reduced to algebra by unfolding definitions. Only , , the scheme (6) and are transcribed, because the statements name them. The goal also asserts that is optimal for the firm and that the sizes are unique maximizers, so its universal clauses are not vacuous.
Welcome contributions include a continuous-time optional stopping theorem for Brownian functionals, the expectation of a discounted geometric Brownian motion, and proofs of the milestones in order.
A non-parametric choice model describes customers by a probability distribution over rankings of products: a customer offered a subset of products buys the one ranked highest among them. Revenue management and assortment planning use such models because they impose no functional form on substitution behaviour (Farias, Jagabathula and Shah, 2013; van Ryzin and Vulcano, 2015). Estimating one from sales data means finding a distribution over the rankings whose induced purchase probabilities are close to the observed frequencies. Two features make this hard in practice: the set of rankings is exponentially large, and the observed frequencies are themselves only estimates, refined as more transactions arrive.
Ho-Nguyen and Kılınç-Karzan (arXiv:1702.05702v5) treat the estimation problem as a convex-concave saddle-point problem whose data are revealed through a sequence of estimates , a joint estimation and optimization (JEO) setting. Their framework bounds the error of an aggregated primal-dual iterate on the true data by quantities computable from the estimated data, and their primal-oracle algorithms produce sparse ranking distributions whose sparsity is controlled by the iteration count. This mission formalizes the core certificate of that framework, Corollary 1, together with the steps leading to it.
Let and be convex compact sets and let be a real function, defined for every data value in a parameter space, that is convex in and concave in . Define the primal and dual objectives
and the primal problem . The SP gap of a pair is
An algorithm runs for rounds. In round it uses the current data estimate to produce . Nonnegative weights with aggregate the iterates into the weighted averages and . Three error terms appear:
A primal-oracle algorithm picks first and then . In the choice-model application and is the convex hull of the ranking vectors, so this step is a linear program over with a vertex solution.
For arbitrary , data , weights with and primal-oracle steps ,
No rate, constant or special form of is fixed: the statement holds for every convex-concave , every horizon and every nonnegative weight sequence with .
Corollary 1 turns any no-regret algorithm for the dual player into an estimator for the primal problem on the true data. With standard online convex optimization methods , and under a Lipschitz condition on in the data the terms vanish as (Theorem 2 of the paper). In the choice-model application each primal step adds at most one ranking to the support of the estimated distribution, so the corollary gives an explicit trade-off between accuracy and sparsity of the fitted model.
The paper proves the result on paper; no machine-checked version exists. The mission produces a formal statement of the saddle-point certificate in the general convex-concave setting, independent of the choice-model application, so that later formalizations of specific regret bounds (online gradient descent, mirror descent, follow-the-leader) can be combined with it to give end-to-end convergence guarantees for primal-oracle schemes.
The algebra of the argument is short. The work is in the analysis that the paper leaves implicit: every "max" and "min" must be shown finite, and the paper assumes no continuity of . A convex function on a compact convex set need not attain its minimum and need not be continuous at the boundary, so compactness alone does not give attained extrema. Finiteness of , , and follows from the existence of affine minorants (subgradients at relative-interior points) of convex functions on compact convex subsets of , a fact that is not a one-line Mathlib lemma. The data-error terms are suprema of differences of concave (resp. convex) functions and can genuinely be infinite; these are excluded explicitly. The natural shortcut through Sion's minimax theorem is unavailable: its semicontinuity hypotheses are not among the paper's assumptions.
are Fin N → ℝ, Fin k → ℝ; the data space is an arbitrary type P; the horizon is Fin T. Every max/min is the real sSup/sInf of an image set. The goal assumes 0 < ∑ t, θ t and that the two images defining and are bounded above; when either is unbounded the paper's right side is and the bound is empty. No continuity, differentiability or special form of is assumed. The SP gap is defined by the second expression of the paper's (9), , which dominates the first expression by weak duality and so gives the stronger bounds without any minimax theorem. The primal-oracle condition is encoded as together with minimality of over , so the statement cannot be satisfied by points outside .
A complete development needs: Jensen's inequality for convex and concave functions on finite convex combinations (ConvexOn.map_sum_le), lower boundedness of convex functions on compact convex sets in finite dimension, and elementary lemmas on sSup/sInf of sums. The boundedness lemma is reusable well beyond this mission. Proofs of the milestones, and of auxiliary finiteness lemmas, are welcome.
Electricity is traded in two stages. In a day-ahead market generators commit quantities for a delivery period; at delivery, deviations between committed and actual production are settled in a real-time imbalance market at an imbalance price. As the share of wind and solar grows, the generators with the lowest marginal cost are also those with the largest forecast errors, and in several markets they already supply most of the demand in many hours. A generator of this kind can raise the day-ahead price by committing less than it expects to produce and selling the rest in real time. Whether it gains from doing so depends on how the imbalance price is set. European regulation asks that imbalance prices support competitive behaviour (Article 52 of the EU electricity balancing guideline), but the two families of rules in use, single pricing and dual pricing, were compared mostly by simulation before this paper.
Ghiassi-Farrokhfal, Belo, Hesamzadeh and Bunn (MSOM 2023) model this market with strategic low-cost generators and one nonstrategic expensive generator, show that the usual single price leads to under-commitment (their Theorem 1), compare it with two dual-pricing rules, and then propose an optimal pricing rule under which under-commitment disappears (Theorem 5). This mission formalizes Theorem 5 together with the model it rests on.
There are low-cost generators (LCGs) with zero marginal cost, indexed by , and one high-cost generator (HCG). Expected demand is normalized to ; the realized demand is . LCG expects to produce and actually produces . The market share of the LCGs is . The forecast errors are random variables on a probability space with mean and finite variance; they may be correlated in any way.
In Stage 1 each LCG chooses an offer adjustment and commits . The HCG schedules the rest, with , and the Stage-1 price is its marginal cost . In Stage 2 LCG trades the difference and the HCG adjusts by , where . Its marginal cost at delivery is with , so its total cost, the area under the marginal-cost curves, is
Since demand is inelastic, the efficient outcome minimizes cost, and the deadweight loss is , the extra cost of producing the same total partly as a real-time adjustment.
The optimal pricing (OP) rule charges LCG the imbalance price
and LCG chooses to maximize its expected profit .
Under the OP rule:
The statement covers every , every share vector and every joint law of the errors with finite second moments.
Theorem 5 says that the market power of renewable generators in the day-ahead market can be removed by the imbalance rule alone, without caps or monitoring: subtracting from the single price exactly offsets the gain an LCG makes on its Stage-1 sales by under-committing. The remaining deadweight loss is then the part caused by forecast errors, which no offer strategy can remove, so the rule attains the efficiency bound of Eq. (6). The paper's simulations (§7) show the effect against single pricing and two dual-pricing rules.
The proof is in an online appendix that is not part of the source used here, and no machine-checked version exists. Formalizing it checks a mechanism-design claim end to end, from the cost model through the expectations. The faithfulness work already found two places where the printed statement is stronger than what holds: "any LCG … choosing " cannot mean that is the unique equilibrium (other equilibria exist, one with positive deadweight loss), and the expected-loss formula of Lemma 1 and Theorem 5 needs to be uncorrelated with the aggregate error (a two-point counterexample gives against the printed ). The goal states the corrected theorem; the counterexamples are recorded in the item statements.
The algebra is short once the expected profit is written as a quadratic in the offers. The work is in the expectations. Every product of forecast errors must be shown integrable from square integrability, and the cross terms such as and vanish only because of the zero means. Moving between Bochner integrals and Mathlib's variance and covariance needs the means to be zero. The natural first attempt, expanding into , silently drops , and that is false without the covariance condition. The equilibrium clauses need the deviation to be unilateral and to range over the offer box, whose upper end depends on all the shares.
All declarations are in the namespace ImbalPricing. The market is a structure Market Ω N with fields μ, γ, α₁, α₂, ε, ν. The predicate Market.Standing collects exactly the standing assumptions: , , , , IsProbabilityMeasure μ, MemLp · 2 μ for and every , and zero means. The covariance condition is not part of it and appears only where it is needed. LCGs are indexed by Fin N. Expectations are Bochner integrals; Var and Cov are ProbabilityTheory.variance and ProbabilityTheory.covariance. The HCG cost is the oriented interval integral of Eq. (3), so the closed forms of Eqs. (3)–(4) are theorems, not definitions. The OP profit is defined as an expectation, not by its closed form. Equilibrium is the general predicate IsPureNash on strategy sets offerBox with payoffs profitOP. Prices and costs are linear as printed (no floor at zero on the marginal cost), and the paper's bounds , which only keep quantities nonnegative, are replaced by square integrability.
Without MemLp the integrals of non-integrable products would be and the identities would hold vacuously; the standing assumptions rule this out, and an explicit market satisfying them is checked. The goal contains no uniqueness clause, because uniqueness is false.
Reusable pieces: the IsPureNash predicate, and the expectation lemmas for quadratic forms in square-integrable random variables with zero mean. Contributions of proofs of any milestone are welcome; Lemma 1 and the closed-form profit are the natural first steps.
Many risk measures used in stochastic optimization are not expectations of a single function but composite functionals: expectations nested inside one another. The mean–semideviation of order , , and higher-order inverse risk measures are of this form. When the law of the data is known only through a sample, every nested expectation has to be estimated, and the plain sample average is not the only choice: replacing the empirical measure by a smoothed version (a kernel estimator, for instance) can reduce bias. Dentcheva, Lin and Penev (arXiv:2201.01338v1, later in Operations Research, 2023) prove that optimization problems built from such estimators are strongly consistent, whichever levels are smoothed. This mission formalizes that result and the stability theory it rests on.
Earlier work established the central limit theorem for empirical composite estimators (Dentcheva, Penev, Ruszczyński 2017); the consistency of smoothed and mixed estimators of optimal values and solutions is the contribution of the present paper.
Decisions are vectors and data are random vectors in with law and . Fix dimensions and functions
jointly continuous in and -integrable in . The composite functional is
and the problem is over a closed set , with solution set , assumed nonempty and bounded. A compact with and compact are fixed so that each inner expectation maps into the interior of .
Replacing at level by a measure gives the perturbed objective , its optimal value and its solution set over . Given an i.i.d. sample with empirical measure and smoothing measures , the mixed estimator uses for the levels in an index set and for the others:
Its optimal value is and its solution set . Distances between sets are the excess and the Pompeiu–Hausdorff distance .
Suppose the smoothed levels have components admitting moduli of continuity on , uniformly over , the unsmoothed levels have a -integrable envelope , and satisfies Assumption 6 (weak convergence to with uniformly integrable first moments). If, almost surely, is nonempty and contained in for large, then almost surely
and when is a singleton. No rate and no constant is fixed; the statement covers every , including (the empirical estimator) and the fully smoothed case.
The theorem justifies using kernel and other convolution estimators inside composite risk-averse optimization: the optimal value and every optimal solution of the smoothed problem are strongly consistent, with no boundedness of the integrands at the smoothed levels. Theorems 3 and 4 are general stability results for nested expectations under perturbation of each level's measure, and apply to any estimation scheme that converges in those metrics. The paper's bias comparisons between smoothed and empirical estimators (§4) presuppose this consistency.
The results are proved on paper; none of them has a machine-checked proof. A formalization produces checked statements of the stability theorems with every hypothesis explicit. Writing them out exposed four places where the printed statements need a correction (nonempty perturbed solution sets, continuity of the limit level maps in Theorem 3, the first-moment claim on p.11, and monotonicity of a subadditive modulus), each recorded with a counterexample in the item it affects.
The obvious argument, "each level converges, so the composition converges", fails twice. First, convergence at each fixed does not pass through the nesting: the inner level's output moves, so uniform convergence on , together with continuity of the limit maps and the interior conditions keeping the inner values inside , is required. Second, at the smoothed levels the integrands are unbounded and only uniformly continuous, so neither the Glivenko–Cantelli argument nor bounded weak convergence applies; uniform convergence over the class needs weak convergence plus convergence of first moments, and for these hold only almost surely and only because the tails of are uniformly integrable. Convergence of optimal values and solution sets over the possibly unbounded further needs the estimated solution sets to be nonempty and to stay in .
is EuclideanSpace ℝ (Fin d). The dimension family is m : ℕ → ℕ with m 0 = 1; levels are 1-based, f j for and a separate fLast for . The composite is a recursion nestStage over stages, shared by the true functional, the perturbed objective, the empirical estimator and the mixed estimator. Optimal values are infima over and solution sets are sets of minimizers; every theorem assumes them attained (nonempty solution sets), so the infimum is never a junk value. and take values in , so can only make a conclusion easier when the solution set is nonempty, which the hypotheses guarantee. Convergence in and is written as "for every , eventually, uniformly over the class". Weak convergence is tested against bounded continuous functions. The sample is X : ℕ → Ω → ℝ^m with iIndepFun and HasLaw, indexed from 0; is deterministic, and the inner limit of Assumption 6 is a limsup.
A trivializing formalization would drop nonemptiness of the estimated solution sets, under which the assumption is vacuous and the statement false; the formal statements assume it explicitly.
A complete development needs a uniform strong law of large numbers over a compact parameter set with an integrable envelope, weak convergence of empirical measures (Varadarajan), uniformity over equicontinuous classes with uniformly integrable growth, and Berge-type continuity of parametric minima. These are reusable well beyond this mission, and contributions of any of them are welcome, as are proofs of the individual milestones.
Display advertising is sold in two ways. Reservation contracts guarantee an advertiser a volume of impressions at a fixed price, negotiated in advance. Programmatic auctions (ad exchanges) sell impressions one at a time, efficiently, but at a price and with an allocation that the advertiser does not know in advance. Advertisers with fixed campaign budgets are risk-averse about both. Cohen, Désir, Korula and Sivan (SSRN 3088600; Management Science, doi:10.1287/mnsc.2022.4542) propose a Market-Maker contract that combines the two. A buyer pays a fixed price now, and the seller procures the unit inside the same auction. They then ask whether such a contract can help the seller without hurting anyone. This mission formalizes their main answer, Theorem 3, together with the chain of results it rests on.
A seller sells identical units. On a probability space , an outcome is a random list of nonnegative unit values. The number of units demanded is random and the values may be correlated. A buyer with demand and value contributes copies of , the paper's per-unit reduction (Assumption 2). Without a contract, the highest units win the -th price auction and each pays the clearing price , the -th highest unit value ( if at most units are demanded). Every buyer knows the law of .
Buyers are risk-averse with a common model, either mean-variance with parameter or CARA with parameter . A buyer with value who joins the auction gets
Buying the contract at price gives , resp. . A buyer opts for the contract if and ; ties go to the contract. With and the mean and variance of , the Market-Maker price is
With the contract at , the contract units are served first. The other units compete in the -th price auction for the remaining units. The seller's revenue is the sum of prices paid, the efficiency is the sum of allocated values, and the welfare is the buyers' utilities plus the revenue. denotes the top of the support of .
Assume almost surely, for every , and . Then at :
The three hypotheses of clause 3 correct the printed statement, which is false without them (counterexamples are in the goal's statement). The hypothesis includes the case where and are independent, which is the case the paper's proof treats.
Theorem 3 says the seller can add a guaranteed-price product to an efficient auction and strictly gain revenue. No buyer loses utility and the allocation stays efficient: the high-value buyers pay a risk premium that equals the value they place on removing price uncertainty. Theorem 1 is independently useful. It shows that the uniform-price multi-unit auction stays truthful for mean-variance bidders, whose preferences violate the von Neumann–Morgenstern axioms, so truthfulness in expectation does not follow from truthfulness outcome by outcome.
The paper's proofs are informal and treat and as uncorrelated, although the model allows correlated values and a random number of buyers. A formal proof establishes the theorem in the corrected form above, under no density assumption, for every market given as a random list of unit values. No part of the paper has been formalized before.
The obvious argument for Theorem 1 is that misreporting lowers the payoff in every outcome. That suffices for CARA but not for mean-variance: a misreport lowers the mean but can also lower the variance, and the utility subtracts times the variance. The proof needs the inequality between the relative drops of variance and mean (Step 2), for every law of the clearing price and both directions of misreporting.
For Theorem 3, the obvious argument "the contract buyers pay instead of the clearing price" fails in expectation when the number of contract buyers is correlated with the clearing price. The market side also needs care. One must show that the contract buyers are almost surely strictly above the clearing price, which uses Corollary 2 and the absence of an atom at . One must then show that removing them leaves the -th price unchanged, a statement about order statistics of lists with ties.
The Lean development (namespace MarketMakerAds) represents:
riskUtility, the variance written as an integral;is natural-number subtraction; the theorem proves almost surely. Theorems 1 and 2 hold for every law whose negative part has a finite second moment, and for both tie rules at the reported value.
The revenue is computed from the two-stage outcome, not defined as . The purchase rule is the utility comparison, not a threshold on . Without these two choices, clauses 1 and 3 of the goal would hold by unfolding definitions.
A complete development needs:
The list lemmas and the truthfulness results for mean-variance bidders can be reused outside this paper. Proofs of any milestone are welcome, as are alternative proofs of Theorem 1 that avoid the case split on the direction of misreporting.
A partially observable Markov decision process (POMDP) models a controller that acts on a system whose state it cannot see: it observes only signals correlated with the state. POMDPs are the standard model for planning under uncertainty in robotics, machine maintenance, medical decision-making and verification of probabilistic systems. When the controller is evaluated over an infinite horizon by its long-run average reward, the natural question is how much memory a good controller needs. A controller that must remember the whole history cannot be implemented; a controller with finitely many internal states can.
For fully observable Markov decision processes, stationary strategies are optimal for the long-run average reward (Blackwell 1962). For POMDPs, ε-optimality of finite-memory strategies was known only in special cases: belief-stationary strategies suffice in blind or ergodic POMDPs, and in general the controller's belief ranges over an infinite set. Chatterjee, Saona and Ziliotto (arXiv:1904.13360, published in Mathematics of Operations Research, 2022) prove that for every finite POMDP with the liminf-average objective and every ε > 0, some finite-memory strategy is ε-optimal.
Timeline of the inputs used here:
A POMDP is with finite state space , finite action set , finite signal set , transition function and reward function . Given an initial belief , the initial state is drawn from . At each stage the decision-maker plays an action , receives the unobserved reward , and the pair is drawn from ; only the signal is observed.
A history before stage is , and a (pure) strategy is a map . The strategy and the initial belief induce a law on plays. The long-run payoff and the value are
A strategy is ε-optimal if . It has finite memory if it is generated by a finite-state transducer: a finite set , an initial memory , an action map and an update map , with and .
For every finite POMDP , every initial belief and every ,
No bound on the memory size is part of the statement; by Remark 2.10 of the paper, none exists in terms of the data of .
The theorem shows that long-run average POMDPs, unlike their limsup counterparts (Proposition 3.4 of the paper), can be approximately solved by finite controllers. Two consequences are drawn in the paper: approximating the long-run value is recursively enumerable (Corollary 3.2), and the value is lower semicontinuous in the transition function (Corollary 3.10), so ε-optimal finite-memory controllers are robust to small model errors (Lemma 3.9).
The result is proved, in a published paper. No machine-checked proof of it, or of its inputs from Venel and Ziliotto, is known. A formalization adds a Lean development of POMDPs with history-dependent strategies built on Mathlib's Ionescu-Tulcea construction, of beliefs and Bayes updating, of invariant measures on the belief simplex, and of the super-support construction.
The obvious approach is to play an optimal strategy and remember only the current belief, or a finite approximation of it. This fails: the belief takes infinitely many values, an optimal strategy need not be a function of the belief, and finite-recall strategies are not enough in general (Proposition 2.12). Remembering the support of the belief is not enough either (Example 4.5): the controller must remember from which value class of initial states the current mass came, which is what the super-support records.
The second difficulty is the passage from almost-sure ergodic behaviour of a strategy that is not finite-memory to an expected-payoff bound for a block strategy, which needs a uniform block length over the finitely many reachable super-supports and an exact accounting of mass through the blocks (Lemmas 6.8 and 6.9). The input Lemma 5.3 rests on the uniform convergence of and on the invariant-measure lemma of Venel and Ziliotto, which are proved in another paper and are milestones here.
PMF (K × S), a joint law of next state and signal with no positivity assumption; takes values in . Beliefs are stdSimplex ℝ K.Kernel.trajMeasure on ℕ → PlayStep A S K, where coordinate is and coordinate carries . Histories are chronological lists; strategies are functions List (A × S) → A on histories of every length; Lean stages are indexed from .∫ or ⨆.rep of representative histories.Reusable parts: the POMDP play law, beliefs and Bayes updates, and the theorem that a finite-memory strategy's expected averages converge (a finite Markov chain ergodic argument). Proofs of any milestone are welcome, as are proofs of the Venel–Ziliotto inputs from their own source.