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?
A risk measure assigns to a random financial position the amount of cash that has to be added to it to make it acceptable. Value-at-Risk ignores the size of losses beyond a quantile, and Conditional Value-at-Risk weighs all losses beyond a threshold equally. Utility-based shortfall risk (UBSR), introduced by Föllmer and Schied (Convex measures of risk and trading constraints, Finance and Stochastics, 2002), replaces the quantile by an expected loss for a convex loss chosen by the user. It is a convex risk measure and it is invariant under randomization. It is also elicitable, and it is the only elicitable convex risk measure (Föllmer and Weber, The axiomatic approach to risk measures for capital determination, Annual Review of Financial Economics, 2015, Theorem 8.6). Its link with convex acceptance sets is worked out by Weber (Mathematical Finance, 2006). It has been used for credit risk under the Normal Copula Model and for portfolio optimization.
In practice the law of is unknown and only samples arrive, one at a time. Dunkel and Weber (Stochastic root finding and efficient estimation of convex risk measures, Operations Research, 2010) cast UBSR estimation as stochastic root finding and proposed a stochastic approximation scheme that uses the quantile function of , with an asymptotic analysis. Hegde, Menon, Prashanth and Jagannathan (arXiv:2111.08805v3, 2023; Mathematics of Operations Research, 2025) give a non-asymptotic analysis: a projected stochastic approximation scheme driven by i.i.d. samples of , with an explicit bound on its mean-squared error (their Theorem 1). This mission formalizes that theorem and the steps of its proof.
Let be a probability space and a random variable with almost surely. Fix a convex, differentiable loss and a risk level . The acceptance set is , and the utility-based shortfall risk of is
(OnlineUBSR.acceptanceSet, OnlineUBSR.ubsr). Put (OnlineUBSR.gFun). Assumption 1 gives with ; then is finite and is the unique root of in .
The estimator uses samples , independent and each distributed as , step sizes , a starting point and the projection (OnlineUBSR.proj):
(OnlineUBSR.iterate). The noise is (OnlineUBSR.noise) and (OnlineUBSR.iterSigma). Assumption 3 asks for with on , and Assumption 4 for with a.s. for every .
With and , for every ,
The constant is the printed . The proof's last line reaches only , so a sharper version of the final summation is part of the mission (milestone (32)–(33)).
In proof order: is finite and the unique root of (§3); the projection step (26); the representation with (27); ; the conditional one-step inequality (28); the scalar bound (29); the one-step inequality in expectation (30); the unrolled bound for a general step sequence; the logarithm and Basel bounds for (31); and the noise sum for , together with the step (32) and the conclusion of (33) ((32)–(33), sharpened).
Theorem 1 gives a non-asymptotic rate for estimating UBSR from streaming samples, with every constant explicit and without access to the quantile function of . It matches the asymptotic rate of Dunkel and Weber's estimator. The initial error decays like , faster than the noise term. The paper uses it to bound the error of UBSR estimates inside gradient schemes for UBSR optimization (its Lemma 1 and Theorems 5–6), so the bound propagates into those rates.
The result is proved on paper. Formalizing it gives a checked shortfall risk with a free risk level, a checked projected Robbins–Monro analysis with an explicit constant, and a check of the proof's details: three hypotheses as printed are too weak (see Formalization scope), and the printed constant needs a sharper summation than the paper's. To our knowledge no machine-checked proof of this theorem, or of a non-asymptotic mean-squared error bound for projected stochastic approximation with explicit constants, exists.
The skeleton is the classical one-step contraction followed by unrolling. Three steps are not routine:
Everything lives in the namespace OnlineUBSR. Expectations are Bochner integrals and conditional expectations are Mathlib's condExp. Under the hypotheses all integrands are bounded a.s., so no junk value occurs. is the real sInf of (2). The step sequence is indexed from (a 0 unread) and so are the samples (ξ (n+1) forms ). The starting point is deterministic. Powers are real powers. Samples are mutually independent (iIndepFun) and identically distributed with (IdentDistrib).
Three hypotheses are corrected, each with a counterexample to the printed form in the item statements:
One reading is fixed: uses the fresh sample , as display (26) implies. Monotonicity of is not assumed, except for the global uniqueness clause of the §3 milestone. The milestones from (26) to the unrolled bound hold for any positive step sequence, as the paper notes on p.21.
There is no trivializing formalization: a verification file exhibits an instance satisfying every hypothesis of the goal, with . Other files check that is a sub-σ-algebra, that and are integrable, and that the corrected Assumption 3 agrees with the printed one for and follows from pointwise bounds on .
Needed infrastructure, all in Mathlib: conditional expectation and independence (condExp, iIndepFun, IdentDistrib, the independence lemma for conditional expectations), differentiation under the integral sign, the fundamental theorem of calculus for interval integrals, hasSum_zeta_two, and harmonic-sum bounds. Contributions to every milestone are welcome. The summation lemmas ((31), (32)–(33)) and the conditional-expectation steps (the centring lemma, (28)) are independent of each other.
Fair division of divisible items usually assumes that everything being shared is desirable. Many allocation problems also involve bads (chores): tasks, liabilities or emissions cuts that some or all participants would rather avoid. A mixed manna contains both. The competitive equilibrium is the standard fair and efficient solution concept for goods: it is envy-free when budgets are equal and Pareto optimal. For a mixed manna, Bogomolnaia, Moulin, Sandomirskiy and Yanovskaya showed that competitive allocations still exist and keep these properties (Econometrica 2017). Their equilibrium set can be disconnected and is not given by a convex program, so computing an equilibrium is a real question.
Chaudhury, Garg, McGlaughlin and Mehta (arXiv:2008.02753, 2020; Mathematics of Operations Research, 2023) give a complementary pivot algorithm for exchange markets with a mixed manna under separable piecewise-linear concave utilities. Its correctness is the subject of this mission.
Timeline:
There are finite sets of agents and of divisible items. Agent brings of item , and each item has unit supply, . Agent values item through a separable piecewise-linear concave (SPLC) function . Its segments have strictly decreasing slopes and lengths , and the last segment is infinite. Item is a good () if some agent has , and a bad () otherwise. On a bad every slope is negative, with disutility .
A competitive equilibrium is a price vector and an allocation such that each maximizes subject to , , and every item clears, . Bads get negative prices, so agents earn money by taking chores. The paper assumes that the desire for each good exceeds 1, that each agent brings some good and some bad (Condition 1), and that the economy graph is strongly connected (Condition 2). In that graph, when is non-satiated for a good that brings.
The algorithm works on the augmented LCP (14). Its variables are : shifted prices (relative price for goods, for bads), spendings , agent variables , supplementary prices , and Lemke's scalar . The parameters are , a large , coefficients and last-segment length . Write for the polyhedron of LCP (14). Algorithm 1 starts at the primary ray and walks from vertex to vertex of along edges of the LCP's solution set, pivoting at the double label, until . Every vertex with , , decodes to the equilibrium , .
for every instance meeting the standing assumptions, every , all sufficiently large , every admissible and every .
Theorem 14 gives a constructive proof that competitive equilibria of a mixed manna exist under strong connectivity, and that a rational instance has a rational equilibrium (Theorem 21). It also places the problem in PPAD (Theorem 22) and gives an odd number of equilibria for nondegenerate instances (Theorem 23). Experiments in the paper find the algorithm practical. Unlike convex-programming methods, it applies to exchange (not only Fisher) markets with chores.
The result is proved in the paper but has not been formalized. A Lean development would check the delicate parts: the treatment of secondary rays and of the spurious degenerate solution, and the limiting arguments of Lemmas 16–18. The formalization already corrects three printed statements. Lemma 15's bound fails at solutions where every bad has ; Lean checks a counterexample on the paper's Example 6. Lemma 7's first half fails for equilibria with the wrong sign pattern, which an equality budget admits. Lemma 16's printed conclusion "" contradicts its own proof and is read as "".
The obvious argument is the one that works for goods: Lemke's scheme follows a path, and the path ends either at a solution or on a secondary ray. For goods-only LCPs, copositivity-type arguments exclude secondary rays. Here secondary rays exist. Setting on any subset of bads, with everything else zero, gives one. The LCP also has a solution that is not an equilibrium. So the proof must track the path itself: it must show that the walk from the primary ray never sets any price to its bound. This uses the economy graph (Lemma 16) and limits along the last edge (Lemmas 17–18). The termination argument also depends on nondegeneracy away from , while is inherently degenerate: summing the market-clearing rows gives an identity.
Agents and items are finite types, and every quantity is real. Segments are indexed from 0. A segment of a good carries variables only if the agent's first slope on it is positive. The utility uses the infinite last segment, and the LCP uses length . The budget in the equilibrium definition is an equality, and prices are not normalized, so is an equilibrium whenever is.
The printed hypothesis "U, W, L have no polynomial relationship" is undefined. Read as algebraic independence it never holds, since , and the goal would be vacuous. It is therefore replaced by the conclusion of Theorem 11, which is all the proof uses: every vertex of with , , is nondegenerate, meaning exactly as many inequalities are tight as there are variables. Algorithm 1 is encoded as a Lemke path: a sequence of distinct vertices from , each consecutive segment inside the LCP's solution set, with before the end. A goal that only asserts that an equilibrium exists, or that some solution has , is not Theorem 14. The goal requires both the termination clause and the correctness clause for every such path. "Sufficiently large " is an existential threshold depending on the instance and . The randomly drawn and the "small" are generalized to every admissible value.
A complete development needs vertices, edges and degeneracy of polyhedra, Lemke's path-following lemma (two edges of the solution set at a nondegenerate vertex), and the KKT characterization of optimal SPLC bundles. The polyhedral and Lemke-path parts are reusable for other LCP-based algorithms. Contributions to any milestone, or to the optimal-bundle characterization of §4, are welcome.
Many optimization problems ask for the largest root of a concave function of one real variable that can only be accessed through oracles. In linear fractional combinatorial optimization, minimizing a ratio over reduces to finding the largest root of the concave, piecewise linear function . The same reduction underlies parametric submodular minimization, minimum-ratio cycles, and the feasibility of two variables per inequality (2VPI) linear systems. The classical tool is the Newton–Dinkelbach method: from the current point it follows a supergradient to the root of the tangent line and repeats. Its strongly polynomial iteration bounds go back to Radzik's analysis of fractional combinatorial optimization.
Dadush, Koh, Natura and Végh (arXiv:2004.08634v4, 2021; later in Mathematics of Operations Research, 2022) add a look-ahead step to the method. They analyse it through a Bregman divergence and obtain a strongly polynomial algorithm for 2VPI feasibility and for deterministic Markov decision processes. This mission formalizes the core of that analysis: the look-ahead method halves a Bregman divergence every two iterations.
Timeline:
Let and let be a proper concave function with effective domain . For the set of supergradients is
Assume that has a root or attains its maximum, and let
the largest root if one exists, and otherwise the largest maximizer.
Algorithm 1 (Look-aheadNewton) receives and with and . While , it does the following.
The Bregman divergence of (Definition 3.2) is
It is nonnegative and may be .
For every iteration of Algorithm 1,
This holds for every proper concave for which exists, for every valid start, for every answer of the oracle, and up to the last iterate.
Milestones 1–5 are stated for runs that may mix standard and successful look-ahead steps freely, which covers the classical method and Algorithm 1. Milestone 6 needs Algorithm 1's rule.
Lemma 3.4 turns the Bregman divergence into a potential that halves every two iterations. Theorem 3.6 of the paper combines it with a lemma of Radzik on geometrically decreasing sequences (Lemma 3.5) and so bounds the look-ahead method by iterations for linear fractional combinatorial optimization. Theorem 4.11 uses it inside each phase of a 2VPI algorithm, which gives a strongly polynomial algorithm for 2VPI feasibility and for deterministic MDPs. A formal proof of the lemma is the reusable core of both arguments.
The paper proves the lemma on half a page of inequalities, and Lemmas 3.1 and 3.3 in the appendix. No machine-checked proof of any of them is known. The mission also builds the infrastructure that later missions need: supergradients and Bregman divergences of extended-real concave functions on the line, and an oracle-level model of the method's runs. Theorem 3.6 and the 2VPI results would build on these definitions.
The paper writes "It is easy to verify that Lemmas 3.1 and 3.3 also hold for Algorithm 1"; for the formal proof this step has to be done explicitly. Concave functions here are not differentiable. Supergradients are arbitrary oracle answers, can be unbounded or empty at the boundary of the domain, and the divergence can be infinite at the start. A proof that implicitly uses derivatives, or a fixed choice of supergradient, does not cover the statement.
The two-case structure of Lemma 3.4 hides a subtle step. After a failed look-ahead, the claim needs an argument that a guess strictly between and would have passed the test for every possible oracle answer. That requires interiority, continuity of concave functions on the interior of the domain, and the defining property of in both the root and the no-root case.
A proper concave is a pair (dom, f) with f : ℝ → ℝ and ConcaveOn ℝ dom f; "" is dom. Supergradients (superdiff) quantify over dom. The divergence (bregman) is EReal-valued, and the supremum is an EReal supremum, so the value is represented faithfully. is a hypothesis IsDeltaStar (a greatest element via IsGreatest), never a real sSup.
A run (IsRun) is a 1-indexed sequence , whose input is valid and whose consecutive pairs satisfy a one-step relation. In LookAheadStep (Algorithm 1) and RelaxedStep (standard or successful look-ahead), oracle answers are existentially chosen at every call. An empty superdifferential at the Newton point ends the run; at the look-ahead point it counts as a failed look-ahead. Infima and suprema of are written IsLeast/IsGreatest.
Several shortcuts would trivialize the goal or weaken it, and none is used:
A sanity file checks a concrete run with both kinds of look-ahead, the divergence values along it, and a start with infinite divergence.
Welcome contributions: one-dimensional facts about concave functions (one-sided derivatives as extreme supergradients, continuity on the interior), proofs of the milestones in order, and a proof of the goal from them.
A security agency guards a network of roads, pipelines or corridors against an infiltrator who needs a fixed amount of uninterrupted time at one spot to do damage. The agency moves a single patroller at bounded speed and wants to maximize the probability of catching the attack in progress. Patrolling games model this as a zero-sum game between a Patroller and an Attacker. The discrete version on graphs was introduced by Alpern, Morton and Papadaki (2011); the continuous version, where both the network and time are continuous, was studied on the line segment by Alpern, Lidbetter, Morton and Papadaki (2016), and Garrec (2019) proved that the continuous game always has a value. The mission formalizes the main general result of Alpern, Bui, Lidbetter and Papadaki, Continuous Patrolling Games (arXiv:2008.07369v2): the exact value of the game on every network when the attack is short compared with the network's cycles and leaf arcs.
Timeline: 2011, discrete patrolling games on graphs (Alpern, Morton, Papadaki); 2016, the continuous game on a line segment (Alpern, Lidbetter, Morton, Papadaki); 2019, existence of the value on general networks and its solution on Eulerian networks (Garrec); 2022, this paper: networks without leaves for attacks no longer than the girth, every network for attacks no longer than the generalized girth, trees under a leaf condition, and symmetric skewed stars.
A network is built from a finite connected multigraph (loops and parallel edges allowed) by giving every edge a length and identifying it with an open interval of that length. Its points are the vertices and the interior points of the edges; its metric is the minimum length of a path from to ; its length measure is Lebesgue measure on each edge, and is its total length. A leaf node is a vertex of degree , and is the number of leaf nodes. The line segment is excluded.
The game has an attack duration .
A circuit is a closed path of distinct arcs; the girth is the shortest circuit length ( for a tree). The generalized girth counts a leaf arc of length as a circuit of length :
Two strategies carry the solution. The independent attack strategy on the set of leaf nodes attacks a random leaf at a start time uniform on with probability , and otherwise attacks a uniformly random point of at time , where is the set of points within of a leaf. The leaf-pausing double tour follows a closed tour that traverses every arc twice and turns back only at leaf nodes, pausing for time at each leaf; the Patroller repeats it periodically from a uniformly random starting phase.
For every network and every with ,
the randomized periodic extension of guarantees this interception probability for every admissible tour , and the independent attack strategy on the leaf nodes holds every patrol to it. The value is stated as equality of the lower and upper values, so the statement includes existence.
Theorem 6 solves the continuous patrolling game for all sufficiently short attacks on every network, since . It extends the paper's Theorem 4 on networks without leaves (, value ) to networks with leaves, and specialized to trees it gives the equality case of the paper's Corollary 2. The formula has a direct reading: leaves cost the Patroller as if each added of extra length, because a leaf must be revisited after turning back.
The result is proved in the paper; none of it has a machine-checked proof. Formalizing it requires the metric and measure theory of finite metric graphs, a measure-theoretic definition of mixed strategies in a game with continuum strategy sets, and a graph-theoretic tour construction (a refinement of Euler's theorem). The tour result of Theorem 3 is classical (the paper credits Sabidussi, 1977, with an earlier proof); Lemma 3 gives a new elementary proof.
The value formula follows from two matching bounds, and each is delicate. On the Attacker side, the paper's proof of Theorem 1 sorts patrols by where they spend the attack window (inside , inside , or crossing from to a leaf) and balances them through the choice of ; a complete proof has to handle every patrol, including ones that cross between and several times. On the Patroller side, the double tour must revisit every point at least later, which fails for a tour that turns back in the middle of an arc; the non-backtracking property of and the girth condition are exactly what rule this out, and constructing needs control over the transitions of an Eulerian tour at every node. Both bounds also need measurability of the interception events, which is not automatic for arbitrary random patrols.
The Lean development lives in the namespace ContPatrol.
MetricGraph V E (finite types, src/tgt maps, positive len) satisfying IsNetwork: at least one edge, connected, and not a line segment. Vertices of degree are allowed, so the circle is one loop at a degree-2 vertex; leaf-arc lengths, girth and tour reversals are defined so that subdividing an arc changes nothing.dist is the shortest-path distance and lengthMeasure is Lebesgue measure on the edges.lowerValue and upperValue are the sup of Patroller guarantees and the inf of Attacker guarantees; "" means both equal . The value's existence is not assumed.No statement is vacuous: the sanity checks prove that constant paths are patrols and jumps are not, that a Dirac attack cannot hold the Patroller below , that , and that the circle satisfies exactly for .
Needed infrastructure: shortest paths and Lipschitz paths on metric graphs, Fubini on (patrol, attack) pairs, measurability of interception events, and Eulerian tours of multigraphs with loops. The metric-graph layer and the Euler-tour lemma are reusable beyond this mission. Proofs of any milestone, and lemmas on the metric (triangle inequality, Borel structure), are welcome.
Internal theft is a recurring cost of retail operations: a store manager who handles both the stock and the till can divert inventory or its procurement budget before customers arrive, and can skim cash after sales are made. Survey figures quoted by Chen, Tian and Zuo put internal theft among the leading sources of retail loss, and a common managerial response is to raise prices to recover the lost margin. The paper (Chen–Tian–Zuo 2025) asks what a firm that designs the manager's compensation optimally should do with its price and its capacity as theft becomes more efficient.
The model joins two lines of work. Optimal-contracting models with cash diversion and limited liability (Innes 1990; de Véricourt–Gromb 2018, 2019) show that debt-like contracts deter ex ante diversion; price-setting newsvendor models (Petruzzi–Dada 1999) describe how a monopolist prices against random multiplicative demand. Here both forms of theft act at once, and the firm chooses commission, capacity and price jointly.
A principal (the firm) gives an agent (the store manager) capacity at unit cost and sets a retail price . Demand is multiplicative, with , , where the nonnegative shock has a continuous, invertible distribution. The firm observes neither the deployed capacity nor the realized revenue.
The agent's utility is . The principal's problem (5)–(7) maximizes over , subject to being a best response of the agent; ties are broken in the principal's favour. An optimal pair is the price and capacity of an optimal solution.
The threshold commission plays the role of a debt contract. With , the reduced value of a price is the function of Corollary 1, built from the quantiles , and . For the main theorem, is uniform on with .
Fix and uniform demand. There are thresholds and functions with
such that are constant on ; on , strictly decreases and strictly increases; and on , strictly increases and strictly decreases. The thresholds are not given in closed form, so the goal survives any sharper description of them.
The theorem reverses the intuition that a firm should pass theft losses on to consumers. When ex post theft is mild, the optimal commission is debt-like and the price does not respond. As cash diversion becomes more efficient, the firm first lowers its price and expands capacity, and only later raises the price; in the last regime () the optimal commission is a fixed revenue share. The earlier milestones are reusable on their own: Lemma 1 is a revelation-principle style reduction for joint ex ante/ex post diversion, and Lemmas 1–2 with Proposition 1 hold for any continuous demand law.
The result is proved in the paper (main text and e-companion); none of it has been machine-checked. A formal development would also settle three points the printed text leaves open: Lemma 2 needs the "or improved" correction when the expected repayment is negative; the second branch of (13) should read ; and the strict inequality is not covered by the paper's argument at , where .
The obvious route is to optimize over threshold contracts and differentiate the closed-form price. That does not prove the theorem. The goal is about the original problem, in which the agent may divert capacity and under-report revenue with any measurable reporting rule, and the firm may use any nondecreasing rule with limited liability. Reaching the closed forms needs a replacement argument over arbitrary reporting functions (Lemma 1), a replication argument over an infinite-dimensional contract space (Lemma 2), and a case analysis of concave newsvendor problems with an incentive constraint at a fixed price (Proposition 1). The price problem is then piecewise, glued at , and its third branch has an interior optimum whose monotonicity depends on the sign of . Uniqueness of the optimal pair is asserted but not proved separately in the paper: it requires that stealing is strictly dominated and that each branch has a unique maximizer. Finally needs to vanish inside whenever .
All statements live in namespace RetailTheft. The model is a structure Params with and the law of ; and (lam) are explicit arguments. Expectations are Bochner integrals against ; demand uses Real.rpow. Committed conventions:
Monotone on with for ; reports are measurable with ;A formalization in which the agent cannot steal, or in which "optimal" means the argmax of , would make Lemmas 1–2 and Proposition 1 disappear from the goal; the definitions rule this out. The thresholds are arbitrary reals: at one needs .
A complete development needs: integrals of bounded monotone compositions against a probability law, quantile functions of continuous laws, concave newsvendor optimization, and one-variable calculus for the price branches. The newsvendor and quantile lemmas are reusable beyond this mission. Contributions of proofs for any milestone, of the uniqueness argument, and of the case of are welcome.
Data has become cheap to collect and store, yet firms still rely on people to design tests, analyse the results and report them, and those people often want a particular decision. Alonso and Câmara (Management Science 70(5), 2024) ask how a firm should organize this work. Should the person who designs a test also report it? How often should reports be audited? How hard should falsifying data be?
The model joins two strands of the persuasion literature. In the first, a sender commits to a public experiment (Kamenica–Gentzkow 2011). In the second, the sender may tamper with the result or the receiver may fail to observe it, as in costly misreporting (Kartik 2009) and in persuasion through weak institutions (Lipnowski–Ravid–Shishkin 2022). Its central claim runs against the usual view of data integrity: the principal should not eliminate tampering, because a credible doubt about reports is what forces the designer to run an informative test.
A state has prior . A principal chooses between the status quo , worth to her, and an innovation , worth . So she approves only at a posterior of at least , and means she retains the status quo uninformed. A designer and an agent both gain from .
The principal fixes a task allocation (integration or separation ), an audit intensity and a cost distribution of tampering costs on . The designer then picks a status-quo experiment , a pass/fail test with outcomes , and type-I error . The agent sees and a cost , and may pay to report after . With probability the audit is conclusive and the principal sees .
An outcome records the experiment, the tampering probability, and the approval probabilities after an unaudited and an audited . In a continuation equilibrium, the agent best-responds to the gain , so , and the principal best-responds to Bayesian posteriors, mixing only at . The designer's payoff is times the approval probability, minus the expected tampering cost under integration only. The commitment experiment has type-I error .
The goal is Proposition 7:
Every designer-optimal outcome of every design gives the principal at most , and every optimal design has and . The policy , with mass at and at , attains under both task allocations with zero expected tampering cost. Another policy is also optimal, and a dual internal–external audit attains the same value.
The milestones are the steps of the paper's argument, in proof order:
The result gives a closed-form audit intensity that depends only on the principal's threshold, always lies strictly between and , and is independent of the prior. It separates the two audit layers: the internal audit's strength depends on the prior, and its result must stay hidden from the principal, since the designer would otherwise pick the commitment experiment.
The proposition is proved on paper; no machine-checked proof of it is known. The formalization adds three things. It pins down the equilibrium selection on which the statement depends, it records the corrections below against the printed text, and it gives a reusable template for an audited persuasion game with atomic cost distributions.
The obvious route computes the designer's best experiment from the threshold equation (6) and optimizes over it. That route fails exactly where the theorem lives: the optimal policy is atomic, so (6) need not have a solution, and at many continuation equilibria coexist. The argument has to work with the agent's tie conditions directly and quantify over every deviation of the designer, for every cost distribution. A second difficulty is that at the optimum the designer is exactly indifferent between and the commitment experiment, so the order of the selections matters.
Everything is in the namespace OrgAnalytics, with lam, mu, qH for , and the model is the single definition OrgAnalytics.Model. A cost distribution is a probability measure on with no mass below ; atoms are allowed, and no density is assumed.
The conventions, each declared on the items that use it, are:
The statements are not trivial readings of the formulas: the designer's choice is an argmax over all continuation equilibria, the principal's utility is her primitive expected payoff, and the closed forms are theorems. Keeping and rules out the degenerate cases. All this is elementary real analysis plus masses of half-lines and one set integral, so the proofs need no new library. Contributions of proofs of the milestones in any order are welcome; a general lemma on two-point cost distributions would be reusable across them.
When a team's reward depends on the total effort of its members and the reward is shared equally, every member bears her own effort cost but receives only a small share of what that effort adds. With a continuum of members, each member's effort has no effect on the shared reward, so in a Nash equilibrium nobody works: the extreme case of free riding. Firms, sales forces and research groups counter this with relative performance criteria (RPCs), rules that redistribute the reward according to each member's performance relative to the rest of the team.
Zhou's paper (SSRN 3742584, version of November 13, 2022; later published in Mathematics of Operations Research, doi:10.1287/moor.2022.1337) asks which RPC is optimal, meaning that under it some Nash equilibrium gives every member the value of full cooperation. It answers this in one period (§2), in discrete time with common noise (§3), and then for a two-layer mean-field game (§4): a continuum of teams competes, each team's reward depends on its achievement relative to the other teams, and inside each team the members play the contribution game under an RPC that the team chooses. The paper calls the two-layer formulation its main mathematical contribution. This mission formalizes §3–§4, ending with the two-layer equilibrium theorem.
There are periods. On a probability space, with is a member's idiosyncratic noise and with is the team's common noise. is independent of , and are independent. Write . A control is a sequence of nonnegative efforts. It lies in if is -measurable, and in if may also depend on . Effort in period produces the random performance , with . Effort costs , where is strictly increasing and strictly convex with .
The team's reward is , where is the team's aggregate effort; its achievement is . A team using while all other teams use receives
where is the intensity of competition among teams. A team-wise equilibrium is a control .
Inside a team, a member using , while her teammates use and all members of other teams use , is paid under the ratio-based RPC with weight :
Here and are the team aggregates. A pair is an equilibrium of the two-layer game if maximizes over , and if its payoff equals . The second condition says that the team cannot do better with another RPC.
Under Assumption 4.1, there is a team-wise equilibrium . It is unique up to almost-sure equality, it satisfies , and is an equilibrium of the two-layer game for
Theorem 4.2 characterizes the optimal intra-team incentive explicitly. The first term of is the weight of the single-team problem (Theorem 3.1). The second term is the extra intra-team competition that competition among teams calls for, and it increases with .
The results are proved in the paper. Their proofs run through a stochastic first-order condition, Komlós-type compactness for existence, an envelope theorem along a backward induction, Dini's theorem, and an intermediate-value fixed-point argument. None of them has been machine-checked. A formalization would also settle the hypotheses. The printed Lemma 3.1 and Theorem 3.1 omit concavity of the reward and are false without it. The mission states them with concavity added; the counterexample is given in the milestone statements. The goal itself is unaffected, because Assumption 4.1 contains concavity.
The obvious argument for Theorem 3.1(a) differentiates under the conditional expectation. Continuous differentiability and finiteness of the conditional expectation of do not justify this; concavity does, through monotone difference quotients. For Theorem 4.1, the team-wise equilibrium is a fixed point of a map from the other teams' average achievement to at the team's optimum. That map is not obviously continuous. Its continuity needs convergence of optimal feedback controls under perturbation of the reward (Lemmas 4.3–4.5), and its monotonicity needs comparison results for value-function derivatives (Lemmas 4.2, 4.6). Existence in the centralized problem needs a compactness argument in , because the control set is not compact.
X ω k is . Controls are families of real random variables measurable for the prefix -algebras.All definitions are local: Mathlib supplies conditional expectation, regular conditional distributions, independence and convexity, but no stochastic-control or game vocabulary. A full development needs:
These are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Theorem 4.1, are welcome.
Display advertising is sold impression by impression in real-time auctions. A publisher rarely sells to advertisers directly: advertisers delegate bidding to intermediaries, ad exchanges, which collect their clients' bids in an internal auction and then bid on the winner's behalf in the publisher's header auction. Since the industry's move to first-price auctions, both layers are first-price auctions, and each layer shades its bids. Zeithammer and Choi (Management Science, 2024) ask what this two-tier bid shading does to the publisher's choice of reserve price and to everyone's surplus. Their answer is a form of double marginalization, the classical channel inefficiency in which successive margins hurt both the upstream seller and the downstream buyers, here produced by auctions at every level rather than by posted prices.
A publisher sells one impression in a first-price sealed-bid auction with reserve price . Four advertisers have private valuations drawn independently from a distribution on with density . The virtual value is ; is regular if is increasing. The generalized hazard rate of the maximum of draws is
Direct benchmark. The advertisers bid themselves, using the symmetric equilibrium bid of a four-bidder first-price auction with reserve,
With the highest valuation (law ), the publisher earns , and each advertiser earns .
Auction of auctions. Two exchanges each represent two advertisers. Each runs an internal first-price auction with the same reserve, so its advertisers still bid . The exchange then bids in the header auction and keeps the difference between its internal winning bid and its own header bid. In terms of the highest valuation among its two advertisers, its equilibrium bid is
and the publisher earns . The allocation is unchanged (the highest-value advertiser still wins), so each advertiser's profit at reserve is again . The pseudo hazard rate governs the publisher's reserve in this arrangement. A monopoly exchange representing all four advertisers pays exactly the reserve, so .
An optimal reserve of an arrangement is a maximizer of the corresponding publisher revenue over : for , for .
For every regular , every maximizer of and every maximizer of on ,
Proposition 2 says that exchange intermediation with first-price auctions at both levels makes the publisher and the advertisers worse off together, even though at any fixed reserve the allocation is efficient. Proposition 1 locates the mechanism: the publisher responds to the exchanges' extra shading by raising the reserve above the Myerson level, which reduces sales. These results underpin the paper's later comparisons: commission-based exchange compensation that coordinates the channel (Proposition 4), the failure of the Bulow–Klemperer comparison in the presence of exchanges (Proposition 3), and the extension to exchanges with advertisers each (Proposition 5).
The results are proved in the paper; none of them is formalized elsewhere. The mission produces machine-checked statements of the model and of the chain from Lemma 2 to Proposition 2, with each paper statement placed in its exact domain. It also records one correction. The paper calls "increasing" for every regular ; that clause is false for some regular distributions (for instance the one with , for which decreases on ). The mission states that clause under the hypothesis of Claim 1, increasing, which the paper's proof uses. The other clauses of Proposition 1, and Proposition 2, hold for every regular and are stated at that strength.
The paper's proof of compares the roots of and and needs to be increasing, which regularity alone does not provide. Under regularity alone an argument must work with the revenue itself: its derivative in and the sign of on . Computing that derivative is the main analytic step. is a triple integral in which the reserve appears in every lower limit and inside the integrand at every level (through inside ). The divisions by and also need control near when .
Lemma 2 is an equilibrium statement. The exchange's best response has to be checked against every bid , including bids outside the range of . Uniqueness among increasing strategies cannot assume differentiability of the strategy, which the paper's first-order derivation (A33)–(A39) does assume.
The valuation distribution is a structure holding the density , continuous on , nonnegative, strictly positive on , with integral ; . Endpoint values or are allowed. Regularity is weak monotonicity of on . Every integral is written with the density . The formulas (3), (4), (5), (8), (13), (18) and (19) are transcribed literally; the closed forms of the uniform case and the rewritten integrals (A16)–(A17) are not used as definitions.
Optimal reserves are arbitrary maximizers (IsMaxOn on ) of the transcribed revenues, quantified universally; neither uniqueness nor a first-order condition is assumed. Defining or as roots of or would empty Proposition 2 of its model content and is excluded.
The advertisers' equilibrium in the auction of auctions, eq. (10) (they keep bidding ), is argued in prose in the paper and is taken as the model: the exchanges' payoff uses the internal winning bid , and by (16) the advertisers' profit in every arrangement is at the reserve set there. The exchanges' header auction is encoded in terms of types: the rival's type has law , it stays out below , and ties lose (a null event under increasing strategies).
The development needs only Mathlib's interval integrals, derivatives and order theory. Contributions are welcome on the calculus of parameter-dependent interval integrals (Leibniz rule with variable limits), which every revenue statement uses, and on an envelope-theorem argument for first-price equilibria that does not assume differentiable strategies.
A provider of a subscription service, such as a cloud platform or a software suite, releases better technology over time. Existing customers do not move to the newest release for free: migrating has a cost, and they compare the benefit with the price they are offered. The provider must decide how much to charge new customers and how much to charge those who upgrade, and it may treat the two differently. Kash, Key and Zoumpoulis study this problem in a model where customers are myopic and the quality of a technology class grows linearly with the time of its introduction (SSRN 3934603, later published in Operations Research). The paper's first main result, formalized here, characterizes the optimal prices for given introduction times and gives an algorithm that computes them. The pricing of a single product under a monotone hazard rate is the classical setting of Myerson (1981). This mission concerns the dynamic extension in which each customer is sold a chain of upgrades.
Time is discrete. Customers arrive with unit mass in each period and stay for periods. A customer has a type with density and c.d.f. , and enjoys benefit per period from technology class , where is the time of the -th introduction. Here is a finite or infinite schedule, and class means opting out.
A price vector charges per period for class to a customer with upgrade experience , the number of upgrades she has made. A new customer picks the class maximizing among those available, with ties going to the latest class. An existing customer may move only from the previous class to the current one, at the time of its introduction, and does so if the move is myopically no worse after paying the switching cost . This gives her class and experience in her -th period at time . Revenue at time is
and for a discount factor .
The type law satisfies Assumption 2: the support of is , or if , and is monotonically decreasing on it. Let maximize , let be the virtual valuation, and let .
OptimalLumping works on an index range . It starts from and repeatedly picks the largest out-of-order , adds the constraint to a lumping, and replaces on the resulting block by . DiscriminatoryPricing sets and .
For every , , , every type law satisfying Assumption 2, every finite or infinite schedule, and every bounding the upgrade experience, OptimalLumping has a terminating run for every . For every family of terminating runs, the prices of DiscriminatoryPricing satisfy
the maximum being over all real price functions with a summable revenue series.
The path runs through the slice revenue of customers arriving between two introductions: Observation 1 (which prices it depends on), the decomposition of total revenue into slices, the threshold form of a slice with the explicit coefficients and , and Lemma 1, which turns the maximum over prices into problem (12):
Then come the structure of (12) (log-concavity of , quasiconcavity of the joint terms, the first-order maximizer, attainment of the maximum), Lemmas 2 and 3 on lumpings, and the correctness of OptimalLumping from Appendix F.
The theorem gives a closed-form description of optimal upgrade prices. Each is the previous price plus the value of the quality step at a threshold type, minus the switching cost. The thresholds depend on the type law only through , and the lumping itself does not depend on the law at all. The optimal lumping is computed in time quadratic in , which is what makes the fixed-schedule problem tractable, and the paper's results on introduction timing take these optimal prices as given.
Theorem 1 is proved on paper; no machine-checked proof of it is known. Its proof has statements that the paper leaves implicit: that exists, that problem (12) attains its maximum, and that the loop of OptimalLumping can terminate, since the printed does not fix a tie-break. This mission makes each of these a target. It also adds a vocabulary of monotone hazard rate, virtual valuation and log-concave survival functions on a possibly unbounded support. On the platform, the single-unit theorem MechanismDesign.Auctions.myerson_optimal_auction is proved in a different vocabulary.
The obvious argument treats each upgrade threshold on its own: the objective of (12) is separable, so one would set for every . That fails as soon as introduction intervals increase somewhere, because these unconstrained optima are then out of order, while only a customer who took one upgrade can take the next. The order constraints bind on a set of indices that must be determined, and there are exponentially many candidate sets. A second difficulty sits before problem (12): the comparison is against all real prices, including prices at which new customers buy older classes or upgrade thresholds carry slack, and all of these have to be shown no better.
The types are real numbers and is an extended nonnegative real. The number of introductions is in , prices are a total function , and class always costs . Assumption 2 is stated on with there, so that Lean's does not exclude Beta. Thresholds lie in the support.
Algorithm 1 is the printed loop, encoded as a relation in which each iteration chooses any maximizer. Defining its output as a chosen optimal lumping would make the goal hold by definition, and is ruled out. The comparison in the goal is guarded by summability, since Lean assigns a non-summable series the sum . Prices are unrestricted in sign and form.
Indices of zero weight occur in most schedules. There the block value reads in the source and in Lean; the corresponding prices enter no revenue, and the goal carries no positivity hypothesis.
A complete development needs bookkeeping of customer states over time, tail bounds for log-concave survival functions, and order arguments for lumpings. The log-concavity results and the lemma on lumpings are reusable beyond this mission. Contributions to any milestone, and supporting lemmas on hazard rates and quasiconcavity, are welcome.
A distributionally robust functional evaluates a random cost by its worst expectation over a set of probability measures, the ambiguity set: . Functionals of this form are the dual representation of coherent risk measures and the objective of distributionally robust optimization. Multistage decision problems need a conditional version, evaluated given the information available at an intermediate stage, and two constructions are in use. The distributionally robust one conditions every measure of on the information (Shapiro, Minimax and risk averse multistage stochastic programming, doi:10.1016/j.ejor.2011.11.005). The risk-averse one, standard in the theory of conditional risk mappings (Ruszczyński and Shapiro, doi:10.1287/moor.1060.0204), prescribes a separate ambiguity set for each piece of information. Pichler and Shapiro (doi:10.1137/21M1390517) observed that the two differ.
Shapiro and Pichler, Conditional Distributionally Robust Functionals (manuscript of October 9, 2022; published in Operations Research, 2024, doi:10.1287/opre.2023.2470) compare them systematically. This mission formalizes the comparison result of their §2 for finitely generated information, Proposition 2.1.
Let be a measurable space and a finite partition of : finitely many nonempty measurable sets, pairwise disjoint, covering . They generate a finite sigma subalgebra ; a -measurable variable is constant on each atom and is written through its values . For a probability measure with , the conditional probability is (2.4).
In Lean these are CondDRO.FinitePartition, CondDRO.condDRF, CondDRO.condRM, CondDRO.inducedSets and CondDRO.mixture.
For arbitrary nonempty sets of probability measures supported on , every positive probability vector , and every measurable integrable under all these measures,
Nothing is fixed: neither , nor the partition, nor the sets , nor .
Proposition 2.1 says that every conditional risk measure built from atom-wise ambiguity sets is a conditional distributionally robust functional, for an ambiguity set on whose atom probabilities can be any positive vector. The converse direction (milestone 3) says that every conditional distributionally robust functional is a conditional risk measure. Together they identify the two classes of conditional functionals for finite , which is what allows the paper to transfer properties between them (strict monotonicity in Proposition 3.1, conditional law invariance in Proposition 3.2) and to compare nested functionals in multistage problems.
The result is proved in the paper by a two-sentence argument; it has no machine-checked proof. The mission produces a formal definition layer for conditional ambiguity sets over finite partitions, reusable for nested distributionally robust functionals and multistage stochastic programming, and a checked version of the identification with every convention made explicit.
The obvious argument is to observe that restricted to is . The steps that need care are the ones the paper leaves implicit: each must put no mass outside , which uses disjointness of the atoms; recovering an arbitrary needs a member of every other , so nonemptiness of all the sets is essential; and positivity of every is essential, since with the supremum in (2.6) runs over an empty set while (2.7) does not. The formal proof must also move between the conditional measure, the restricted integral and the extended-real supremum over an image set.
Fintype).Measure Ω with IsProbabilityMeasure hypotheses; "supported on " is ; is Mathlib's ProbabilityTheory.cond.EReal. The paper assumes finite; the formal statements do not, and specialize to the paper's when it is.Contributions welcome: proofs of the three milestones and the goal, and lemmas on sums and restrictions of measures with disjoint supports.
Firms that sell through a sales division or a retail store face two frictions at once. The local agent knows the market better than headquarters (adverse selection), and the agent's selling effort is costly and unobserved (moral hazard). Since Laffont and Tirole (1986) and Rao (1990), the standard remedy has been a menu of linear commission contracts (MLC): the agent picks a commission rate and a base payment from a menu, and the choice reveals her information. That theory usually assumes the firm observes true demand and that inventory is not an issue.
In practice, the firm often sees only sales, which are demand censored by the available inventory, and the inventory decision is sometimes delegated to the sales division. Each of these looks like a loss for the firm: censoring destroys information, and delegation adds an incentive problem. Song, Lai and Xiao (MSOM 2024) show that, under two monotonicity conditions, neither loss materializes. The firm's optimal profit is the same in all four settings.
A risk-neutral agent sells at unit price . She privately observes the market condition , which has a density on that interval, distribution function , and inverse hazard rate , assumed decreasing. A -type agent who chooses output pays the output cost , where is the cost of effort and the effort needed for output . Demand is , with a shock . Inventory costs the firm and the agent per unit, and sales are . Assumption 1 asks , , to be with , ; , ; and , , , , , , . Subscripts denote partial derivatives. The agent's outputs are , and the sign conditions are read on that domain.
Write and . The virtual surplus is
There are four direct-mechanism problems. Under control, the firm sets and pays on demand (PCD) or on sales (PCS). Under delegation, the agent requests and is paid (PDD) or (PDS). In each problem the firm maximizes its expected profit over all mechanisms satisfying incentive compatibility (IC) and individual rationality (IR). Let solve system (1):
and set . Condition (D) says is nondecreasing in . Condition (S) says the same of .
Under Conditions (D) and (S), each of the four problems attains its maximum, and
The goal holds for any nonnegative solution of (1). That solution need not be unique.
The result separates two questions that operations practice often merges. The first is what the firm must learn about the market. The second is who should order inventory. Proposition 6 says neither affects the attainable profit once the commission rates are monotone in type. The optimal menus are explicit, and the delegated versions add only a quadratic or linear inventory term to the base payment. Firms such as Wal-Mart centralize inventory, while others delegate it to stores. The paper's managerial claim is that this organizational choice need not cost efficiency, provided the contract is adjusted.
The paper's proofs are informal in places: an envelope theorem applied pointwise, and uniqueness asserted from strict concavity. A machine-checked version settles exactly which hypotheses carry the argument. None of these results is known to have a machine-checked proof. The mission also builds reusable infrastructure: the integral-form envelope identity for screening with a general cost , and concavity of expected newsvendor sales for general concave demand.
The upper bound needs the envelope identity for an arbitrary incentive-compatible mechanism. The obvious route differentiates and fails, because can have kinks. Lemma 2 is formalized in integral form: the pointwise derivative is false for kinked . The working argument shows that (IC) forces to be monotone, hence Lipschitz, and then integrates by parts against .
Attainment needs, in each setting:
The sales-based delegation case (DS) couples output and inventory. The paper's printed proof of this case repeats the demand-based one, so it has to be redone. A second trap is that the paper's claim that (1) has a unique solution is false in general. When the density of vanishes at the critical fractile, a whole interval of solves (1). Only is unique.
The model is one Lean structure. Its components are:
Further conventions:
IsGreatest) of the set of attainable profits, never as a supremum or a closed form.Defining the optimal profits through (1), or restricting the problems to linear menus, would make the goal a tautology. The integrability clauses rule out junk payments whose Lean integral is .
Contributions are welcome on any milestone. The envelope identity and the concavity of are independent of the rest.
A service system that sees several types of customers must decide whom to serve first. When the cost of waiting grows linearly in the wait, the answer has been known since Cox and Smith (1961): serve the types in decreasing order of , the waiting-cost rate times the service rate. This -rule is a fixed priority ordering, and under it serving all types first-come-first-served (FCFS) is never optimal.
Many waiting costs are not linear. Patients, callers and customers tolerate a short wait and object to a long one, and empirical work on emergency departments finds marginal waiting costs that grow with the wait. Van Mieghem (1995, Ann. Appl. Probab. 5(3):809–833) shows that for convex costs a dynamic rule, the generalized -rule, is asymptotically optimal in heavy traffic, but that rule needs every customer's elapsed wait and the exact cost functions. Ouyang, Argon and Ziya (2021) ask the practical question for fixed priorities: given two customer types, should one of them get priority, and if so which, or should they be pooled and served FCFS? Their answer for quadratic costs is the goal of this mission.
A single server serves types of customers. Customers arrive in a Poisson process of rate ; each arrival is of type with probability , independently. Type- service times are i.i.d. with law on , mean and moments ; . The traffic intensities are , the system is stable, , and .
A fixed-priority policy of the class assigns each type a priority order. The server never idles while a customer is present, never preempts a service, starts the present customer of smallest order, and serves customers of equal order FCFS. Starting from the policy in which type has order , fix two adjacent types and compare three policies: (type first), (the two orders switched), and (types and pooled and served FCFS).
A type- customer who waits in queue costs . The long-run average cost of a policy is
where is the waiting time of the th type- arrival from the initial state . The steady-state waiting time is the limit in distribution of as . Assumption 1 asks . The comparison runs through two indices,
with .
If on with for , then ,
and: if then ; if then ; otherwise . The three costs exist.
Proposition 3 generalizes the -rule to quadratic costs and shows a qualitative change: pooling two types under FCFS can be strictly better than prioritizing either, and it is never the worst of the three. With linear costs it recovers the classical rule. Its conditions involve only the first three service moments, the arrival data and the two cost functions of the compared types, so they can be evaluated in practice; Corollary 1 of the paper turns them into explicit intervals for .
The result is proved in the paper, partly by citing classical queueing theory (Takács 1964 for the waiting-time moments, Kleinrock 1965 for conservation, a regenerative ergodic theorem for (1) = (2)). None of it is machine-checked. A formal development needs a sample-path model of the multiclass nonpreemptive priority queue, which no library currently has, and would make these classical facts available for other scheduling results.
Given the milestones, the goal is algebra: Proposition 2 plus (A.10) and a case split. The difficulty is in the queueing facts. The step (1) = (2) needs a regenerative structure of the customer-indexed waiting sequence and the identification of its cycle averages with the limit law. Lemma A.1(a) is a distributional, not a pathwise, identity: the residual service found by a lower-priority arrival depends on the order inside the pair. Lemma A.1(c) and (A.8)–(A.9) need the first two moments of the nonpreemptive priority waiting time, which the paper takes from Takács' transform formulas; a sample-path derivation has to pass through busy periods of the higher-priority classes. Simply manipulating the definitions of and cannot work: their values are fixed by the queue, and every sign in Proposition 3 rests on (A.10).
Types are Fin K (0-based): the paper's pair is the pair with , its is rhoBar k and its is rhoBar (k+2). Randomness is a sequence of i.i.d. marks (exponential interarrival time, type, one potential service time per type). The policy is an order map Fin K → ℕ, and waitingTime computes the sample path by recursion over service starts, FCFS within an order.
IsLongRunAvgCost: the almost-sure limit from every initial state). The identity (2) is the first milestone, not a definition.IsSteadyStateLaw, from every initial state). Expectations are integrals against that law; Takács' formulas, Lemma A.1(c) and (A.8)–(A.9) are theorems, never definitions.A formalization in which is defined by (2), or by its moments, would make the milestones definitional and the goal an algebra exercise; that is excluded by construction. Contributions are welcome on the regenerative argument for (1) = (2), on Kleinrock's conservation law, and on the moment formulas of the nonpreemptive priority queue, all of which are reusable beyond this mission.
A mathematical program with complementarity constraints (MPCC) minimizes a smooth function subject to constraints of the form , , . MPCCs arise in generalized Nash equilibrium problems, bilevel optimization and semi-infinite programming. Their feasible sets are nonsmooth: standard constraint qualifications fail at every feasible point, so the theory and algorithms of nonlinear programming (NLP) do not apply directly.
The Scholtes regularization (Scholtes 2001) relaxes to with a parameter and solves a sequence of regular NLPs as . Numerical comparisons rank it among the most effective regularizations (Hoheisel–Kanzow–Schwartz 2013). Scholtes showed that limits of KKT points of the regularized problems are C-stationary for the MPCC. Lämmel and Shikhman (arXiv:2501.07383v2) ask a finer question: does the regularization preserve the topological type of stationary points, measured by Morse-theoretic indices?
Timeline:
Fix and functions and , . The MPCC feasible set is , and the regularized set is .
At the indices split into (), () and the biactive set . The point is C-stationary with multipliers if and on . It is nondegenerate if MPCC-LICQ holds (NDC1), on (NDC2), and the Hessian of the Lagrange function is nonsingular on the tangent space (NDC3). Its C-index is : is the number of negative eigenvalues of , and is the number of biactive indices with both multipliers negative. NDC4 asks on and on .
For the regularized problem, a KKT point with multipliers is nondegenerate if LICQ holds, all active multipliers are positive, and is nonsingular on . Its quadratic index is the number of negative eigenvalues of that restriction.
Let and let be nondegenerate KKT points of the regularization with parameter and quadratic index , with . If is a nondegenerate C-stationary point with multipliers , then
and if NDC4 holds. All three conclusions are part of the goal.
Theorem 1 says that the Scholtes regularization cannot create spurious saddle points in the limit beyond what vanishing multipliers allow. If nondegenerate local minimizers () of the regularized problems converge to a nondegenerate C-stationary point, that point has C-index and is therefore a local minimizer of the MPCC (p.6 of the paper). Under NDC4, which holds generically (Proposition 2 of the paper), the regularization preserves the index exactly; this is the basis for the well-posedness result (Theorem 2) and for the comparison with earlier convergence theory in the paper. Example 2 of the paper shows that without NDC4 the lower bound is attained with .
The results are proved in the paper; none of them has a machine-checked proof. The mission produces a reusable Lean vocabulary for MPCC and its regularization (active sets, MPCC-LICQ, C-stationarity, restricted Hessians, quadratic and C-indices) and formal statements of Proposition 1, Corollary 1 and Theorem 1. It is also the first formal account of index counting on restricted Hessians in this setting.
The obvious argument compares the quadratic forms and on the tangent spaces and passes to the limit. It fails for two reasons. First, the tangent spaces and have different dimensions: a biactive index contributes two constraints at but only one, the product constraint, at when its multipliers are negative. Second, the multiplier of a biactive index with negative multipliers is unbounded as , so does not converge. The extra negative directions come from a blow-up along the hyperbolas , and they account exactly for the biactive index. Indices with vanishing multiplier can be active in either way along the sequence, and this is the source of the gap in (11).
The printed proof works in a normalized coordinate system and its inclusion (18) between two tangent spaces does not hold in general (it fails when an index with is in ); a complete proof must use the product row of in place of the coordinate row there.
is EuclideanSpace ℝ (Fin n) and indices are Fin κ (0-based). The data and their regularity are the structure ScholtesStab.MPCC n κ. There are no other constraints. Differentials are fderiv, Hessians are fderiv ℝ (fderiv ℝ L). Multipliers are total functions Fin κ → ℝ, and only their values on the relevant index sets are used. Linear independence is that of indexed families, so for a biactive index both gradients count. The number of negative eigenvalues of a restricted Hessian is negIndex, the largest dimension of a subspace of the tangent space on which the form is negative definite; by Sylvester's law of inertia this is the eigenvalue count. Nonsingularity of the restriction is NonsingularOn, which is not nonsingularity on all of . " for " is a sequence , , . The multipliers of each are existential; they are unique under LICQ. The inequality (11) is stated in .
A trivializing formalization is ruled out: the limit point is required to be nondegenerate C-stationary with the given multipliers, every approximating point must be a nondegenerate KKT point of the same quadratic index, and the C-index is computed on the tangent space , not on .
The milestones from the proof are stated in general coordinates. The paper's simplification is not assumed, and the terms are kept. A full proof needs convergence of multipliers under LICQ, perturbation of subspaces, inertia arguments for restricted forms, and the blow-up analysis of Step 5. Contributions of reusable inertia lemmas for negIndex (monotonicity, continuity of the negative index under convergence of forms on converging subspaces) are welcome independently of this mission.
Data centers and communication networks spend a large share of their operating cost on energy. A powered-on device pays a fixed idle cost, and with speed scaling it pays a power cost that grows like in its load , with typically between and . Andrews, Fernández Anta, Zhang and Zhao (IEEE/ACM Trans. Networking 20(1), 2012) proposed the cost model for a used device. It is concave for small loads and convex for large ones, so an algorithm must aggregate demand in one regime and spread it in the other: the costs exhibit (dis)economies of scale.
Nagarajan and Wang (arXiv:2007.07721, published in Mathematics of Operations Research, 2024) study this model online. Requests arrive one at a time, and each must be served irrevocably on arrival. The requests may be routing paths, Steiner trees or set-connectivity subgraphs, and the device parameters may differ from resource to resource.
Timeline:
A finite set of resources serves requests. Request comes with a collection of replies and a weight vector with . A solution chooses a reply for each . The load of resource is . Each resource has the (D)oS cost
and the objective is . The parameters are , the load at which both terms are equal, and .
In the online setting, request must receive its reply on arrival, knowing only requests . The algorithm may query a -approximate min-cost oracle: for any request and costs it returns some with . With weighted power costs the same model is the input of Theorem 6, with .
For the deterministic online algorithm of §5, with final loads , and for every solution with loads ,
This gives the printed ratio . The goal also asserts that every reply lies in its .
The ratio depends neither on the number of resources nor on the number of requests, which was the case in earlier online routing work under (D)oS costs. With an exact oracle it is . Theorem 2 of the paper shows that no deterministic online algorithm does better than , so the guarantee is tight up to the base of the exponential. Because the reply collections are abstract, the theorem covers routing, Steiner forest and set connectivity, directed or undirected, and it extends to the REP costs of Theorem 3.
The result is proved in the paper. Nothing in this mission has a machine-checked proof yet. The mission's contribution is a checked proof of the explicit constant , together with reusable statements of online primal-dual dual fitting for convex covering programs with an exponential number of variables.
The obvious argument fails twice. First, is not convex, so convex-relaxation duality does not apply to it directly. Lemma 1 replaces by the convex , but only at loads or at least . On the sandwich fails, so the integrality of replies and are essential, and a fractional argument cannot be lifted without them. Second, the relaxation (P) has a polynomially large integrality gap. The greedy rule with costs is not competitive, and the extra linear terms in (20) are what make dual fitting work. The bound must also hold when differs between resources, so every exponent comparison passes through . Finally, the doubled instance uses in two senses: the linear copies, and the resources with exponent . The two coincide only when no equals .
Resources form a Fintype. Requests are Fin N-indexed values with a Finset (Finset E) of replies and weights E → ℝ. The oracle is a function of the request and a cost vector, required to return a member of and to be a -approximation for every nonnegative cost vector on the instance's requests. The algorithms are explicit online recursions with one oracle call per request, which is how "deterministic", "online" and "polynomial time relative to the oracle" are carried. Powers are Real.rpow, and is Real.exp 1. The maxima and are taken with , which matters only when . Every competitive bound is stated against every solution, not against an argmin.
The statements cannot be satisfied vacuously. The oracle hypothesis is met by the exact argmin oracle with whenever every is nonempty, and the (D)oS cost is charged only at positive load, as in (1).
A complete development needs finite sums, real powers, Young's inequality (in Mathlib), the elementary inequality at (16), and convexity of . The weak-duality lemma and the dual-fitting bounds apply beyond this mission to other online covering problems with power costs. Contributions are welcome on every milestone, in particular a proof of the inequality at (16) and of Lemma 3 for arbitrary .
Multi-echelon supply chains are rarely run by a single firm. A manufacturer of a finished product buys a component from a supplier, and each firm places its own safety stock. The guaranteed-service model of safety-stock placement, going back to Simpson (1958) and developed by Graves and Willems (2000), lets a planner choose, for each stage, the service time it promises to its downstream customer; the safety stock of a stage then depends only on the time it must cover. When one decision-maker controls the whole chain, the optimal service times solve an integer program. Schoenmeyr and Graves ask what happens when two firms each control a part of the chain and negotiate only the one service time between them, and show that nothing is lost if they pick that number well: the centralized optimum decomposes into two independent subproblems linked by a single scalar. This separation result, display (8) of the paper, is the starting point of its contract and bargaining analysis.
A serial system has stages ; stage serves the customer and stage is the most upstream. Time is discrete. Stage has a lead time and a holding cost per unit per period; the average demand per period is , and is a demand bound, the largest demand that must be covered over periods (display (2) of the paper). Each stage quotes an integer service time , with the exogenous boundary values (to the customer) and (for the inputs into stage ). The net replenishment time of stage is
and its safety stock costs . The global program (6) is
Now player 1 controls stages and player 2 controls stages , with , and is the service time between them. For a given , player 1 solves (7): the same program restricted to stages with boundary conditions , . Player 2 solves : the same program on stages with , . In Lean the data form a GSCoord.SerialSystem, and the optimal values are valP, valP1, valP2.
The minimum is attained: some achieves it, and no does better. The statement holds for every lead-time vector, every demand bound, every cost and every pair of boundary values, including infeasible instances, where both sides are .
Display (8) says that the decentralized system is incentive compatible: once the players agree on the right , each one's private optimum is its part of the system optimum. The paper uses this to design contracts in §3 (a price on the service time under full information, a Stackelberg menu, a Nash-bargaining price), and Appendix III extends (8) to two acyclic networks joined by a single link. Every one of those results assumes (8).
The result is proved in the paper (Appendix II); the platform has no machine-checked version of it or of its steps. This mission formalizes it for general data: the demand bound is an arbitrary function, with no concavity, and the costs carry no sign conditions, so the formal statement covers every instance of the paper's model. The definitions of the guaranteed-service programs , , with integer service times are new on the platform and reusable for the paper's §3 results and for other guaranteed-service models.
The mathematics is a partial minimization argument, and the obstacles are in the bookkeeping. First, the two subprograms share the coordinate , so gluing a feasible point of to one of requires splicing two service-time vectors at that index and checking every constraint row on both sides. Second, the values live in the extended reals, where ; the step "the minimum of a sum of independent programs is the sum of their minima" needs the fact that no program value is , which is true because each feasible set is finite (every free service time is boxed between and ), but this is content, not a hypothesis. Third, "min" in (8) and in step (B) is an attained minimum over infinitely many ; attainment follows only because a feasible is bounded by . The naive reading of (8) as an equation of infima drops this attainment and is not the paper's statement.
EReal, for an infeasible program. "min" is IsLeast.SupplyChainTheory.gs_all_or_nothing (the all-or-nothing property) and the definitions Def_SupplyChainTheory_multiechelon, Def_SimpsonInv_Vertex_Setting, Def_GravesWillems_Serial_programP fix a square-root demand bound or real service times, which this paper does not assume.Steady-state means of Markov chains are estimated by simulation throughout operations research and statistics: queue lengths and waiting times in stochastic networks, posterior expectations in Markov chain Monte Carlo, volumes of convex bodies. The standard estimator is a time average of one long run after a burn-in period. It is biased, because the chain does not start in its stationary distribution, and its successive terms are correlated, so confidence intervals from batch means or independent replications rest on asymptotic approximations (Asmussen and Glynn 2007, Ch. IV).
An unbiased estimator with finite variance and finite expected cost removes these difficulties: independent copies can be averaged in parallel, and a confidence interval follows from the central limit theorem for i.i.d. samples. Rhee and Glynn (2015) introduced randomized multilevel Monte Carlo (RMLMC) estimators that are unbiased for limits of biased sequences, and Glynn and Rhee (2014) applied them to contractive Markov chains. Kahalé (arXiv:2209.09581v1, 2022) builds an unbiased modification of the time average itself, under a coupling assumption, and shows that it loses essentially nothing in efficiency against the conventional time average. This mission formalizes that result.
A Markov chain on a measurable state space is given by a deterministic starting point and a measurable update map :
where are independent and identically distributed random variables with values in a measurable space . A measurable function is given with square-integrable for every .
Coupled chains. For an integer , the chain started at time is , : it starts at and follows . In Lean this is coupledChain g x₀ U i m. For the chains and are driven by the same last noise variables.
Assumption A1. There is a positive non-increasing sequence with
The tail sums (nuBar ν j) carry all constants. Under A1 the limit exists (Theorem 2.1).
Estimators. For and burn-ins :
timeAvgEstimator);levelEstimator);singleTermEstimator);debiasedEstimator).The parameters are for , , (levelProb), and (coinProb). Under the paper's cost model, in which costs , the expected costs are for (costZ) and for (costFhat).
Under A1, for every and : is square-integrable, , , and
In proof order: shift invariance of the coupled chains (Proposition B.1); the standard deviation bound for time averages (Lemma 2.1); the tail bound (Proposition C.1); existence of with bias and mean-square-error bounds (Theorem 2.1); ((E.1)); the effect of changing the burn-in (Lemma E.1, Lemma 3.1); the Rhee–Glynn single term estimator (Theorem 3.1); bounds on and on the level increments (Lemmas F.1, F.2); cost and second moment of for an arbitrary level law (Lemma 3.2); admissibility of the chosen ((3.6)–(3.8)); the same with the chosen (Lemma 3.3); and the variance identity (H.3) for .
Theorem 3.2 gives an estimator of a steady-state mean that is exactly unbiased, has finite variance and finite expected cost, and whose work-normalized variance is within a lower-order term of that of the conventional time average. Choosing makes the second term of (3.11) vanish as , so when is bounded below, is asymptotically at least as efficient as up to a factor arbitrarily close to (p.10). Independent replications of then yield valid confidence intervals without bias corrections. Theorem 2.1 and Lemma 2.1, on the way, give explicit non-asymptotic bias and mean-square-error bounds for conventional time averages under A1 alone.
The result is proved in the paper (published in Mathematics of Operations Research, 2024; the mission follows the arXiv v1 preprint). None of it is formalized: the platform has no randomized multilevel estimator, no chain driven by a bi-infinite i.i.d. sequence, and no bias bound for time averages. The mission produces a machine-checked version of the full argument with the paper's explicit constants, and the general pieces, Theorem 3.1 and (H.3), are reusable for any RMLMC analysis.
The argument is elementary in its tools but combines many of them. Proposition B.1 needs the invariance of the law of a bi-infinite i.i.d. sequence under shifts, transported through the measurable recursion that defines the chain. Lemma 2.1 is a dyadic induction in which two halves of a time average are independent because they are measurable functions of disjoint blocks of noise, which uses that is deterministic. Theorem 3.1 exchanges an expectation with a sum over the random level ; Fubini applies only after Cauchy–Schwarz bounds by the finite series in its hypothesis. The rest is careful bookkeeping of series in , square roots and floors, and the constants 5, 26, 25, 796, 20, 9 and 8610 must come out exactly.
A first idea, applying a Markov chain central limit theorem or a mixing-time bound, does not work: A1 is not a mixing assumption and no stationary distribution is assumed to exist, only the limit of expectations, which the theorem must itself construct.
The probability space carries the noise , the level , the copy and the coin ; the standing model is the structure ChainModel, and Assumption A1 the structure AssumptionA1, with (2.5) stated as a lower Lebesgue integral. "Decreasing" in A1 is read as non-increasing. are two natural numbers b ≤ b' with 2 * b' ≤ k. enters as a hypothesis that it is the limit of ; Theorem 2.1 proves that such a limit exists. Variances are ProbabilityTheory.variance, standard deviations their square roots. and are the paper's cost model taken as definitions; no machine model is formalized.
The conclusions state square-integrability of and convergence of the series defining , so that the variance and the cost bound are not Lean's junk values . A proved non-vacuity check (not uploaded) exhibits the model and A1 on a product of Gaussians and shows .
Needed infrastructure: shift invariance for iIndepFun families indexed by , independence of functions of disjoint blocks, variance of sums of independent variables, Fubini over a discrete random index, and tail estimates for tsum. The general results (Theorem 3.1, (H.3), Proposition C.1) are reusable beyond this paper. Contributions of proofs of any milestone, in any order, are welcome.
International trade is financed largely by banks, and a trade loan is risky until the goods reach the buyer. Under the Basel II internal-ratings-based approach, a bank that issues a risky loan must set aside regulatory capital against it, and that capital is costly. Information technologies such as blockchain-based trade platforms let the bank observe the progress of an order, so it can reprice the loan once part of the risk has resolved. Lee, Tang, Yang and Zhang (SSRN 3632563; later in Manufacturing & Service Operations Management, doi:10.1287/msom.2022.1102) model this as dynamic trade finance (DTF): a loan whose interest rate drops once the bank verifies that the order passed its first step. Their Proposition 3 gives the value of DTF in closed form and says how it depends on process reliability, liquidation values, capital cost and the delay in verifying information. This mission formalizes that proposition and the chain of results it rests on, in the SSRN version of February 2022.
A seller borrows a principal to fill an order. The order goes through two steps. Step is passed with probability (Step 2 conditional on Step 1); if the order fails at Step , the bank recovers the liquidation value , with , where is the wholesale price the buyer pays on success. Step 1 takes a time and Step 2 a time . The bank learns that Step 1 was passed only after an information delay with . The three clocks are independent, and passing is independent of the clocks. Interest compounds continuously and the risk-free rate is zero. The frictionless value of the order is .
Until the bank verifies Step 1, it must hold capital . After verification it holds . Capital costs per unit time, with . Holding one unit of capital until time costs . The bank prices loans competitively by Eq. (2): expected repayment = principal + expected net cost of capital (NCC).
The value of DTF is , both payoffs taken at competitively priced loans. The expected information delay is .
For all admissible parameters and every competitive UF rate and competitive DTF schedule (both of which exist),
Moreover, is strictly increasing in , , and , and strictly decreasing in . The marginal benefit is strictly decreasing in and and strictly increasing in , and . Each monotonicity holds over the parameter's whole admissible interval.
The formula separates the sources of DTF's value. DTF helps only through the capital released when Step 1 is verified, which is per unit, weighted by the chance that Step 1 passes. It vanishes without a capital cost (), and it shrinks as verification slows. The paper uses this to argue that faster information verification, the service FinTech platforms sell, is worth most to reliable suppliers, to high-capital-cost banks and to processes whose second step is long. Without the closed form, these comparative statics would rest only on numerical experiments.
The mission adds a machine-checked version of the whole chain. It covers exponential moment computations over independent clocks, the elimination of the equilibrium rates, and calculus in the delay. Two misprints in the proof are corrected: the second derivative (70) lacks a factor , and the cross derivative (73) has the wrong sign. The standing assumption is corrected to the strict inequality, since at equality the expected capital cost is infinite. None of these results has a formal proof yet.
Each identity is elementary on paper. The work is in the probability. The DTF quantities are expectations over the region jointly with , so they need joint independence, product measures and Fubini. The UF rate is pinned down only after showing that the larger root of the pricing quadratic lies where the expected repayment is infinite, which needs a non-integrability argument for exponential moments beyond the convergence domain. The obvious shortcut, treating as the formula and differentiating, proves only the comparative statics of a formula. The goal also requires showing that the formula equals for every pair of competitive rates.
All declarations live in the namespace DynTradeFinance. Parameters form a structure Params, with the field lam for , and the standing assumptions form Params.Admissible. The clocks are random variables on an arbitrary probability space with Mathlib laws expMeasure (HasLaw) and joint independence (iIndepFun). Passing probabilities enter as the weights of the paper's mixtures, not as Bernoulli variables. Expectations are Bochner integrals. In the model's definitions every term is written ; milestone 4 uses Mathlib's conditional measure. The competitive-pricing predicates require the repayment to be integrable, so Lean's convention that a non-integrable function integrates to cannot create spurious competitive rates. Monotonicity claims are strict and range over full intervals, never over sample values.
A complete development needs exponential moments of sums of independent exponential variables, integrals over , and one-variable calculus. A Mathlib-style lemma for and , together with its divergence for , would be reusable well beyond this mission. Contributions toward milestones 1 and 4 are especially welcome.
Classifiers that reach high accuracy on test data can often be fooled by perturbations of the input that are small in some norm. Training a classifier to resist such perturbations (adversarial training) typically lowers its accuracy on unperturbed data, and part of the literature argues that this robust–standard accuracy tradeoff is unavoidable: for some data distributions, no classifier is both optimal in standard accuracy and robust (Tsipras et al., 2019). Javanmard and Mehrabi ask whether the tradeoff persists when the data has the structure that real images are believed to have: high-dimensional features generated from a low-dimensional latent manifold (arXiv:2110.11950v2). Their main result for the Gaussian mixture model says no: in high dimension, if the latent structure is strong enough relative to the adversary's power, the Bayes-optimal classifier, which has the least standard risk, also has vanishing additional risk under attack. This mission formalizes that result and the chain of statements in its proof.
A classifier is a Borel function . For a feature–label pair with joint law , the standard risk is . An adversary of power may replace by any with , where ; the adversarial risk is
and the boundary risk is : the probability that a correctly classified point has a misclassified point within distance .
In the latent Gaussian mixture model (5), a label is with probability and with probability ; given , a latent vector is drawn from , and the observed feature is , where has full column rank and acts entrywise with derivative for a constant . The learner sees but not . With , its Moore–Penrose inverse and , the Bayes-optimal classifier is (Corollary 2.3)
denotes the smallest nonzero singular value of .
Fix and , and let every parameter of the model (, , , , ) and the adversary's power depend on the ambient dimension . If
then . No rate, no bound on or , and no fixed latent dimension is assumed.
for adversaries.
The theorem shows that the robust–standard tradeoff is not a law of nature for structured data: the classifier that is optimal for standard accuracy is asymptotically optimal for robust accuracy as well, whenever (7) holds. Condition (7) quantifies "enough latent structure": must grow faster than the adversary's power, inflated by for adversaries. For example, with the identity, unit-norm rows and equal singular values, (7) for reads . The non-asymptotic milestone gives an explicit, dimension-free bound that holds for every instance and is reusable in finite-sample statements.
The paper proves the result on paper; no machine-checked proof of it is known. A complete formalization also yields reusable infrastructure: the Bayes-optimality of for arbitrary laws, risk notions for norm-bounded adversaries, the Moore–Penrose inverse of a real matrix and its square root, and the Hölder comparison of and norms.
The boundary event of is that the statistic lies within a thin slab next to the threshold . Two steps carry the content. First, the perturbation of must be pulled back through the nonlinear map , which is only possible because makes Lipschitz with constant . Second, the latent Gaussian is degenerate in when , so the posterior and the slab statistic must be computed through the pseudo-inverse and its square root, and the slab width must be related to the standard deviation and to . A bound via the distance of to the decision boundary in alone does not work: the boundary is curved when is nonlinear, and only the latent coordinates make the statistic one-dimensional Gaussian. In Lean, the pseudo-inverse, the PSD square root and the singular values all need some infrastructure.
Features are vectors Fin d → ℝ; the joint law of is a measure on , built for model (5) as the mixture of the pushforwards of (independent standard normal coordinates) under , weighted by and . The sign is -valued with , the tie of the paper's proof of Proposition 2.2. The adversarial event is written as "some in the closed ball has ", which is the infimum condition for -valued . is Function.invFun φ, the inverse under the standing assumption. is the matrix satisfying the four Penrose conditions; is the continuous functional calculus square root; is the last of the singular values of ; operator norms are . The model assumptions in Theorem 3.1 are required only for all large ; a version requiring them at every would be vacuous. The classifier in Theorem 3.1 is the explicit formula , not an arbitrary minimizer of the standard risk, which could differ off the support of the data.
All definitions are local to this mission. Contributions welcome: proofs of the milestones in order, a general Moore–Penrose API for real matrices, the Hölder comparison of norms, and the Bayes-optimality of , which applies well beyond this paper.
The minimum cut of a graph and the minimum - cut are among the oldest problems of combinatorial optimization, and both are polynomial. Between them lies the minimum -Steiner cut: given a graph , nonnegative edge weights and a set of terminals, find a cheapest cut that separates at least two terminals. The polyhedral picture is much less even than the algorithmic one. For , the max-flow min-cut theorem gives a complete inequality description of the --cut dominant (Conforti and Kaibel, equation (1)). For , the cut dominant, no description in the original variables is known, even for planar graphs, in contrast to the cut polytope of a planar graph (Barahona and Mahjoub, 1986). Conforti, Fiorini and Pashkovich, 2016 characterized by forbidden minors the graphs whose cut dominant has a description with right-hand sides at most two.
Conforti and Kaibel interpolate between these extremes by the number of terminals. Their first main result says that the facets of these polyhedra have finite complexity in : for each , finitely many inequalities generate all non-trivial facets for all graphs with at most terminals, by two simple operations.
A Steiner graph is a connected finite simple graph with , . For , the cut is the set of edges with exactly one end in , and it is a -Steiner cut if . The cut polytope is the convex hull of the incidence vectors of the -Steiner cuts in , and the -Steiner cut dominant is
For , is the minimum -weight of a -Steiner cut, and the cuts attaining it are the roots of . A vector is in minimum integer form if it is integral with coprime components. is facet inducing with facet weights if is in minimum integer form and defines a facet; equivalently, has a basis of roots of .
Subdivision replaces an edge by a path through a new non-terminal , giving both new edges the weight of . Gluing identifies a terminal of with a terminal of ; the common node may stay a terminal or not, and the new weights are the minimum integer form of . A facet inducing graph is irreducible if it has no cut node and no non-terminal of degree two. A graph is constructable from a family if it arises from a member of by a sequence in which each step subdivides the current graph or glues it with a member of .
For each there is a finite family of weighted irreducible facet inducing Steiner graphs with at most terminals such that, for all Steiner graphs with at most terminals:
every irreducible one is isomorphic to a member of , the facet defining inequalities with of are exactly the positive multiples of the facet weights of the constructable subgraphs , and
The family depends on only. The goal leaves unspecified: the paper determines the facets explicitly only for (its Main Result II, not part of this mission), and a statement of finite generation stays valid whatever the list turns out to be.
Remarks 1–2, the characterization of facet weights on p.4 and Proposition 1 (facets and their structure); Lemmas 1, 3, 4 and Theorem 1 with Proposition 2 (laminar root bases); Propositions 3–4 and Theorems 2–3 (the operations and their inverses); Remark 3, Lemma 6 and Theorem 4 (finite generation).
The result turns a question about all graphs into one about finitely many objects for each number of terminals. It classifies facets of cut dominants by a complexity parameter, the Steiner degree: the smallest for which an inequality already defines a facet with terminals. A direct consequence in the paper (Theorem 5, not part of this mission) bounds right-hand sides and coefficients in minimum integer form by a function of . Via blocking duality, this also speaks to the vertices of subtour relaxation polyhedra.
The result is proved in the paper. It has not been formalized on this platform: a search on 2026-10-30 found neither the goal nor any milestone. A proof of the goal would machine-check the whole chain of §§2–6, including Remark 3, which the paper states without proof, and Remark 2, which it leaves informal.
The obvious bound on a facet uses the dimension: affinely independent cuts. This says nothing on the size of , and a facet inducing graph can be arbitrarily large, so finiteness cannot hold for facet inducing graphs themselves. Two things must happen. First, the operations must be inverted: a graph that has a cut node or a non-terminal of degree two must split into smaller facet inducing graphs whose weights recombine exactly. Second, what remains must be bounded, and this is where the central difficulty lies. A root basis is an arbitrary set of cuts, which carries no size information. The uncrossing of two roots works only one way or the other, depending on the position of the terminals (Lemma 4), so the standard uncrossing of submodular functions does not apply as it stands, although a laminar structure is what would make the size of countable.
A weighted Steiner graph is the structure WSG: a finite vertex type in Type, a SimpleGraph, connectivity, , and weights . Graphs are simple, as in the paper. Positivity and minimum integer form are clauses of IsFacetInducing, not of the structure, and the root basis is expressed as the roots spanning ; the theorem facetInducing_iff_definesFacet connects it to DefinesFacet. A cut is a real vector on G.edgeSet, and a root is kept as its defining set , since laminarity concerns sets. Dimensions compare finrank (vectorSpan …) additively, and is a real infimum over the nonempty finite set of Steiner cuts. Subdivision and gluing are relations across vertex types through embeddings, so they hold up to isomorphism. Constructable is the linear inductive notion of the page.
The goal is not trivial by choice of , since is finite and fixed before the graph. Non-trivial means right-hand side .
Solvers need the convex geometry of a full-dimensional dominant, including the face dimension argument of Remark 1 and a separation argument for the description of the dominant, then graph surgery on SimpleGraph across vertex types. Reusable parts: laminar families and uncrossing, cut nodes and components, and face lemmas for dominants. Contributions on any milestone are welcome.
Scheduling a shared resource among many queues is the basic control problem of communication networks, data centers and input-queued switches. MaxWeight is the standard policy: it is throughput optimal, and it needs no knowledge of the arrival rates. Exact steady-state analysis is hopeless for such systems, so performance is studied in heavy traffic, as the load approaches the boundary of the capacity region.
The classical theory requires complete resource pooling (CRP): the system behaves in the limit like a single queue. Under CRP the heavy-traffic behaviour of the generalized switch was found by Stolyar through diffusion limits (2004) and by Eryilmaz and Srikant through the drift method (2012). Without CRP, a diffusion approach leads to a multidimensional reflected Brownian motion, whose steady state is not known in closed form. Maguluri and Srikant (2016) obtained the mean sum of queue lengths in an input-queued switch without CRP by the drift method. Hurtado-Lange and Maguluri extend this to the generalized switch (arXiv:1904.10096; Mathematics of Operations Research, 2022).
There are queues in discrete time. In each slot a channel state is drawn from a finite set with law , independently of the past. A service vector is selected from the finite set by MaxWeight, that is, for the current queue vector . Then arrivals occur, and the queues are served: , where is the unused service. The arrivals are i.i.d. in time and bounded by a constant, and may be correlated across queues.
The capacity region is the polytope
with , , . Fix on the boundary of with positive coordinates. The family indexed by has mean arrival rate . Let be the set of facets through , the cone and the subspace generated by , a matrix whose columns are a basis of these normals, and . CRP is the case . Let be a steady state of the queue vector, the covariance matrix of the arrivals, and the covariance matrix of , where .
For every , the mean is finite, there is with and
and if then
Lemma 1 (MaxWeight attains ); Lemma 4 (Hajek's drift bound); Proposition 2 (state space collapse, uniformly in ); finiteness of ; Lemmas 2 and 3; Claims 1 and 2; and the estimates (42), (44), (45) of the terms of the drift identity.
The theorem gives the exact heavy-traffic constant for a whole class of systems without CRP: the input-queued switch under correlated arrivals, full-dimensional collapse, parallel-server systems, the N-system and ad hoc networks are corollaries in the paper. It shows that the limit depends on the arrival covariance only through its projection on , and it requires no diffusion limit.
The result is proved in the paper. The machine-checked proof is the remaining work, and it adds three things. The paper's argument has gaps that this mission resolves: Theorem 1 is false as printed when has a zero coordinate. Take , one channel state, , , and with mean . The printed limit is for every , but at the true limit is . The mission requires , which is equivalent to the paper's own claim on p.6 that lies in the interior of . Also, Proposition 2 and Lemma 4 are stated uniformly in , because the proof of Theorem 1 needs a constant that does not depend on ; the printed quantifiers do not give that. Finally, the formalization produces a general drift theorem for Markov chains. No machine-checked proof of these results is known.
The obvious Lyapunov argument for the collapse bound fails on two counts. The drift of must be negative with a margin that does not vanish as , although the drift of itself vanishes at rate . And a bound for each fixed is not enough: the constants of the exponential moment must depend on the drift parameters alone. Mathlib has no drift theory, so Lemma 4 is a first target. A second difficulty is that is a cone, not a subspace, so the projection on is not linear, and the identities that are immediate in the CRP case do not carry over.
The source is arXiv:1904.10096v4, and all numbering follows it; the journal version was not consulted. Vectors are Fin n → ℝ, and expectations are series under a PMF. The channel state, the schedule and the arrivals are drawn in this order, so arrivals are independent of the rest given . A tie-breaking rule is any law on the arg max. The steady state is any PMF fixed by the one-step kernel, with no irreducibility assumed; its existence is not claimed. The description of need not be minimal. is any basis, and is restricted to . The Lean statements carry HasExpect clauses because a series that is not summable has sum , and is the Euclidean distance to , not a sup-norm distance.
The trivializing readings are excluded: is existential only together with , and the steady state is tied to the MaxWeight step. A separate check exhibits a full family, so the hypotheses are satisfiable.
Reusable beyond this mission: Lemma 4 and the moment bounds it gives, and the projection facts about . Proofs of any milestone, and alternative routes to Proposition 2, are welcome.
The statistical query (SQ) model describes algorithms that never see individual samples of a distribution ; they only ask for approximate expectations of functions of their choice. It was introduced by Kearns for noise-tolerant learning (Kearns 1998), and it has since become the standard abstraction for algorithms that can be run under local differential privacy, under limited communication, or with noisy data: any SQ algorithm can be simulated in each of these settings, and lower bounds for SQ algorithms explain why many statistical problems resist efficient algorithms.
Feldman, Guzmán and Vempala (arXiv:1512.09170v2, 2016; later Math. Oper. Res. 2021) study the most basic statistical task in this model, estimating the mean vector of a distribution on , and use it to obtain SQ versions of first-order methods for stochastic convex optimization. Their main quantitative question is: how accurate must the statistical queries be, as a function of the dimension and the target error , to estimate the mean in a given norm? This mission formalizes their answer for the norms with , which uses the variance-sensitive oracle VSTAT.
For and write (lqNorm q x) and for the unit ball. For , is the conjugate exponent.
A statistical query is a function . The oracle (Definition 2.1) answers a query with any value satisfying
(vstatTol n p). Its tolerance mimics the error of an empirical average of samples, so it is small for queries whose mean is near or .
A non-adaptive SQ algorithm with queries (NonadaptiveSQ d m) fixes measurable queries in advance and maps the answer vector to an estimate . It solves mean estimation with error using (SolvesLqMeanEstimation q ε n A) if for every probability distribution supported on and every answer vector that may return, .
The proof splits a vector into positive and negative parts (posPart, negPart) and those into rings of dynamic range : keeps the coordinates with (ringPart j), and keeps those with (ringInf k), where (ringDepth d q).
For every , and there is a non-adaptive SQ algorithm with queries that solves mean estimation with error using
The paper states it for every ; at it allows zero queries and is false, so the goal assumes .
Theorem 3.15 shows that mean estimation for needs only queries of estimation complexity , which the paper calls nearly optimal in comparison with its lower bounds (§3.2, Table 1). Through the reductions of §3 it gives SQ algorithms for stochastic linear optimization over balls, and through §4 for stochastic convex optimization with first-order methods in the corresponding geometry; through the simulations of §6 these become locally differentially private and low-communication algorithms.
The paper gives a complete, elementary proof, so nothing here is open. No part of it is machine-checked: the platform has no statistical query vocabulary with the VSTAT oracle, no mean estimation statements, and no finite-dimensional interpolation inequalities of the form of Lemma 3.12. The mission produces a checked version of a quantitative SQ upper bound, with corrected constants and boundary cases where the printed text is wrong (Lemma 3.12(2) needs in the minimum; eq. (3) is an inequality; the step needs rather than ).
The obvious algorithm queries each coordinate once. With tolerance per coordinate, the error can be , which forces and hence estimation complexity polynomial in . The difficulty is to exploit that a vector in has few large coordinates: VSTAT's error is small exactly for queries whose mean is near , but naive coordinate-wise use still accumulates error from the many coordinates whose mean is tiny. The proof must combine three things: splitting by magnitude into rings, rescaling each ring so the query fills , and discarding small answers so that tiny means contribute no error. The bookkeeping of exponents (, , ) across estimates, with possibly negative for small , is where the printed argument has gaps.
Vectors are Fin d → ℝ; powers are Real.rpow; the logarithm is Real.logb 2. Distributions are Borel probability measures on Fin d → ℝ, "supported on " means almost surely, and means are Bochner integrals. The VSTAT parameter is a real number. An algorithm is deterministic and non-adaptive, and it must succeed against every answer vector the oracle may return, not only the true means; replacing this by an existential over answers would make the goal trivial. The query count is with a natural number. The integer is negative for small , and the ring sum is then empty.
Needed infrastructure: the definitions in this mission (lqNorm, vstatTol, NonadaptiveSQ, ValidVSTATAnswers, SolvesLqMeanEstimation, rings and thresholds), real-power inequalities for finite sums, and integrals of bounded vector-valued functions. The SQ definitions are reusable for the paper's other upper bounds (Theorems 3.4, 3.5, 3.9, 3.13). Contributions to every milestone are welcome; the milestones on finite sums (Lemma 3.12, Lemma 3.16, eqs. (3), (4)) are independent of measure theory.
Mean field games (MFGs), introduced by Lasry and Lions and by Huang, Malhamé and Caines in 2006–2007, describe the limit of symmetric stochastic games with many small players. A representative player optimizes against the distribution of the population, and an equilibrium is a distribution that reproduces itself when every player best responds to it. Existence of equilibria is usually proved with Schauder- or Kakutani-type fixed point theorems, which need convexity and compactness, and uniqueness needs monotonicity conditions of Lasry–Lions type.
Dianetti, Ferrari, Fischer and Nendel (arXiv:2201.07850, Mathematics of Operations Research, 2023) take the order-theoretic route of submodular (or supermodular) games, going back to Topkis (1979) and Vives (1990): when the cost of a player has decreasing differences in her own strategy and the distribution of the others, best responses are monotone and Tarski's fixed point theorem gives least and greatest equilibria without convexity. Their Section 2 isolates an abstract model that covers discrete-time finite-state MFGs, MFGs with singular controls, MFGs with reflecting boundaries and MFGs of optimal stopping (Sections 4–7 of the paper). This mission formalizes that abstract model and its main theorem.
Timeline:
Let be a complete lattice (every nonempty subset has a least upper bound and a greatest lower bound) that is also Dedekind super complete: every nonempty has a countable subset with the same supremum, and a countable subset with the same infimum. stands for the possible distributions of the players.
Let be a topological space, the strategies of the representative player, with a map that sends a strategy to the distribution it induces, and a cost functional . For write
the best-response set. A mean field game equilibrium is a with ; denotes the set of equilibria.
The hypotheses are:
The learning procedures are , and , .
In Lean these are SubmodMFG.DedekindSuperComplete, argminSet, bestResponse, equilibria, Assumption21, Assumption23, Assumption25, lowerLearning and upperLearning.
Under Assumptions 2.1 and 2.3:
and if every is a singleton, is a nonempty complete lattice. If moreover Assumption 2.5 holds,
Theorem 2.6 reduces existence of extremal MFG equilibria to checking Assumptions 2.1 and 2.3 for a concrete model, and their computation to checking Assumption 2.5. The paper does this for four classes of MFGs, so a formal proof of Theorem 2.6 is the shared core of all of them. The learning clauses also give a constructive approximation scheme (iterate the least or greatest best response from the bottom or top distribution), a learning procedure à la Topkis that needs no uniqueness of equilibria.
The theorem is proved in the paper (pp.6–8). As far as a search of the platform shows, it has not been formalized. The Prove2Me library has Zhou's fixed point theorem for increasing correspondences with subcomplete values and Topkis's existence theorem for finite supermodular games; neither applies, because the best-response sets here are only directed with attained infima and suprema, not subcomplete sublattices, and neither has a learning statement. A formal proof would be an order-theoretic MFG layer that later missions on concrete MFGs (Sections 4–7) could import.
The obvious approach applies a fixed point theorem to the best-response correspondence , but is an arbitrary subset of : it is neither a subcomplete sublattice nor closed under suprema in general, so neither Tarski's theorem nor Zhou's theorem for correspondences applies to as given. The central step is to show that and , infima and suprema over possibly uncountable sets, are themselves best responses (Lemma 2.4 c)). Directedness controls only finite meets and joins, and the topology lives on while the order lives on , so the step has to connect the two through . Countable, finite and empty best-response families all need care.
For b) and c), the map is not assumed order-continuous, so Kleene's iteration theorem does not apply: the supremum of the lower learning sequence is not automatically a fixed point. Showing that it is an equilibrium, and the least one, is where Assumption 2.5 must be used.
is a Mathlib CompleteLattice; is a type with a TopologicalSpace; is curried, J : E → L → ℝ. The operations are existentially quantified and has no order. The argmin is global. Subsequences are strictly increasing maps . The of Assumption 2.5 is taken in EReal, so sequences unbounded below are not given Mathlib's junk real liminf. The first sentence of Assumption 2.5 is required only along strictly monotone sequences, which is weaker than the paper's hypothesis under either reading of "increasing". carries no topology, so "converges to " is the order statement . " is a complete lattice" is meant in the order induced from (least upper and greatest lower bounds inside ), not as a complete sublattice of .
A trivial formalization is ruled out: a verification file shows that the model , , satisfies every hypothesis (including Assumption 2.5) and has .
The needed infrastructure is Mathlib's fixed point theory (OrderHom.lfp, OrderHom.gfp, fixedPoints.completeLattice) and elementary sequence and subsequence arguments. Proofs of the milestones, alternative arguments (for example via Zhou-type fixed point theorems for directed correspondences), and reusable lemmas about Dedekind super complete lattices are all welcome.
A semidefinite program (SDP) minimizes a linear function of a symmetric matrix under linear constraints and positive semidefiniteness. In parametric SDP the data depend on a parameter, often time. The motivating example of Bellon, Henrion, Kungurtsev and Mareček comes from power systems: semidefinite relaxations of alternating-current optimal power flow are widely used, and a transmission system operator must track the trajectory of solutions as supply and demand vary (Lavaei–Low 2012). Understanding how such a trajectory can behave is a prerequisite for tracking algorithms with performance guarantees.
Around a point satisfying strict complementarity and uniqueness, the implicit function theorem gives a smooth curve of solutions. Sensitivity results exist when the data vary linearly (Goldfarb–Scheinberg 1999; Hauenstein–Mohammad-Nezhad–Tang–Terlaky 2022). The paper assumes only continuous data and asks which local behaviours the trajectory can show at all.
Let . For let be symmetric matrices and . With the trace pairing , the operator and its adjoint , the primal and dual problems are
The feasible maps , and the optimal maps , send to sets of matrices; dual points are recorded by alone. A set-valued map is single-valued at if is a singleton and multi-valued if is neither empty nor a singleton. Continuity means Painlevé–Kuratowski continuity: outer and inner semicontinuity, defined by sequences of times in .
The standing assumptions are: LICQ with uniformly bounded norm of and of its pseudo-inverse (Assumption 3.1), primal and dual strict feasibility at every (Assumption 3.2), and continuity of the data on (Assumption 3.3).
The paper names six kinds of point : regular, non-differentiable, discontinuous isolated multiple, discontinuous non-isolated multiple, continuous bifurcation, and irregular accumulation.
Under Assumptions 3.1–3.3, let and . If is single-valued on for some , then
and the same holds for . As printed the theorem is false, so the goal is a corrected statement. A continuous linear program embedded in satisfies all three assumptions, and its optimal map is continuous everywhere and single-valued exactly on ; since no point of it satisfies Definition 3.10, is none of the six printed types. The correction changes only Definition 3.11: its second bullet asks for a right-sided continuous loss of uniqueness, which is Definition 3.10 without its left condition, and the sentence "At these times, either … appears" is not a condition. The paper's own example on p.23 uses "continuous bifurcation point" in exactly this right-sided sense.
Each correction comes with a one-dimensional counterexample recorded on the item.
The result turns "what can happen to an SDP solution along a path" into a finite list. A path-following method that holds a unique solution up to time meets one of six situations and no others. Continuity of the feasible maps and outer semicontinuity of the optimal maps also make discontinuities of an optimal map exactly losses of inner semicontinuity, so that the classification can be read as a list of the ways uniqueness or continuity can fail.
The formalization adds three things. It repairs the classification, whose proof case A3 asserts bifurcations that need not exist. It records exactly which hypotheses each continuity result uses: three results of Section 2.2 need LICQ although their printed statements omit it. And it provides a reusable formal account of Painlevé–Kuratowski continuity for parametric conic problems. The results are proved in the paper, apart from the corrections above; no machine-checked proof of them was found.
The natural first argument is that when uniqueness is lost continuously, the switching time is a continuous bifurcation point. That fails: the alternating case can have multi-valued times immediately to the left of every switching time, so no left single-valued neighbourhood exists. This is why the correction is needed.
The analytic core is continuity of the feasible maps under a moving operator : a small perturbation of a feasible point on the boundary of the cone need not stay positive semidefinite. A further obstacle is the dual half of Theorem 2.16, which assumes no LICQ, so the multipliers of a convergent sequence of dual matrices may diverge.
Matrices are Matrix (Fin n) (Fin n) ℝ, with symmetry of the data as a hypothesis, and A : Fin m → ℝ → Matrix (Fin n) (Fin n) ℝ. The interval is Set.Ioo ti tf, and every interval and sequence in the definitions lies in it, so data off cannot enter. Optimal sets are defined by minimality and maximality, so no real infimum or supremum occurs. Single-valued excludes the empty set, as does multi-valued. Differentiability at concerns the unique-element function near , entrywise, and never a selection. The six types are stated for a general map, so the two clauses of the goal share them. The dual clause concerns sets of .
Theorem 2.16 states the non-emptiness that Definition 2.10 builds into "set-valued map". The sequential continuity notions are vacuous for the empty map, so a statement without it would be false.
All definitions are local to the namespace ParamSDPTraj. The Painlevé–Kuratowski predicates are stated for a general topological space and are reusable. A complete development needs the matrix order and eigenvalue results of Mathlib, a Weyl inequality and SDP strong duality; the last two are available as Matrix.IsHermitian.sorted_eigenvalues_le_add_of_re_dotProduct_le and ConvexOptimization.sdp_strong_duality. Proofs of the milestones and of the goal are welcome in any order.
A decision maker holds a prior over a finite set of states, observes a signal, and moves to a posterior by Bayes' rule. Repeating this step is the standard model of learning in decision theory and in repeated games of incomplete information. Hellman and Levy (Dense Orbits of the Bayesian Updating Group Action) study this process through topological dynamics: each signal acts on the simplex of beliefs by an invertible map, so the signals generate a group, and the question is how large the set of beliefs reachable from a given prior is. The answer feeds into the existence of stationary equilibria in repeated games, which is where the authors' earlier work on smoothness of orbit relations (Hellman and Levy, 2019) meets this one.
The source used here is the authors' final accepted manuscript of November 30, 2020 (Enlighten 227272). The version of record in Mathematics of Operations Research (2022, doi:10.1287/moor.2021.1134) is not the citation basis, and all numbering refers to the manuscript.
Let be a finite set of states and a finite set of signals. Write for the simplex of probability vectors on , with coordinates , and for its interior, the with for all .
A signalling structure is a matrix with each row a probability distribution on with full support. The entry is the probability of signal in state . A signal acts by the Bayes operator
which is a bijection of . Let be the group generated by the under composition. Its elements include inverse operators, so a word in need not correspond to any sequence of observations. The orbit of is . The structure is generic if the numbers are algebraically independent over .
If , then for every generic signalling structure and every ,
Density gives generically that the orbits have recurrent points, so by a theorem the paper records (Theorem 4.1) the orbit relation on the simplex is not smooth when there are enough signals. That limits the reach of the smoothness-based results of Hellman and Levy (2019) for repeated games of incomplete information. The condition is sharp for this theorem: Proposition 3.6 of the paper shows that orbits are not dense when . The whole group is needed, since the paper's examples show that forward orbits, and forward together with backward orbits, can fail to be dense.
Formalizing the result produces a clean Lean account of Bayesian updating as a group action. It also produces the multi-dimensional inhomogeneous Kronecker theorem. At the pinned Mathlib revision, only the one-dimensional density statement is available, so this is reusable independently of the paper.
The theorem is proved in the paper and has no machine-checked proof that this mission knows of. Three points of the manuscript need care, and the items state the corrected forms:
That generic structures exist is Proposition 2.3 of the paper. It is not on the proof path of the goal and is not part of this mission, so the mission does not establish that its hypothesis is satisfiable.
The natural attempt approximates the target log-odds by integer combinations of the columns of the matrix . When those combinations form a discrete lattice, so they are not dense in , and this first idea fails. The freedom that rescues the statement is the common factor removed by normalization, and handling it requires an inhomogeneous Diophantine theorem in several dimensions together with a non-vanishing statement for polynomials in the matrix entries. Mathlib has neither in this form.
is stdSimplex ℝ K as a subtype with the subspace topology, and density is in that space. The interior is positivity of every coordinate, never the topological interior in , which is empty. A signalling structure bundles rows in and positivity, so no logarithm or division is on a non-positive number. is an Equiv.Perm of the simplex with an explicit inverse, and is Subgroup.closure of the range of the operators. Words are lists of pairs with signs in , with the head applied first, and exponents are integer powers. Algebraic independence is over , of the family indexed by . In Lemma 3.8 the matrix is any positive matrix, is one integer for all states, and is unbounded.
The trivializing encodings are excluded: is not defined as the set of normalized products, the orbit is under the group and not the forward semigroup, and density is not taken in the ambient space. The paper's "at least two signals" is not a hypothesis, because genericity implies it for non-empty .
The development needs no published definition. Kronecker's theorem and the algebraic-independence milestone are independent of the Bayesian model and reusable. Contributions toward either are welcome on their own, as is any sharper form of the band estimate.
Manufacturers who own production capacity and jobs to process can pool their machines. If jobs may be split, meaning processed simultaneously on several machines, a group of manufacturers behaves like a single machine whose speed is the total speed of the group's machines. Pooling then lowers the group's total completion time, and the question is how to share that cost so that no subgroup would rather leave. In cooperative game theory this is the question of whether the core is nonempty.
Alon and Anily (MSOM 25(6), 2023) study this parallel machines scheduling (PMS) game for the scheduling problem . The game is subadditive but neither monotone nor concave, and in some instances every core allocation must pay at least one player (their Example 4). So the standard sufficient conditions for a nonempty core, such as concavity (Shapley 1971) or a known nonnegative allocation rule, do not apply. The paper proves that the game is nonetheless totally balanced: the core of the game and of every one of its subgames is nonempty.
A cooperative cost game consists of a finite set of players and a characteristic function with . A cost allocation is in the core of the subgame on when
The game is totally balanced when every subgame has a core allocation.
In the PMS game, player owns machines of total speed and a set of jobs. Job has a processing requirement and a father , and every player owns at least one job. For a coalition , let be its jobs, , , and the requirements of in nondecreasing order. The cost of is equation (1) of the paper:
which is the minimum total completion time when processes its jobs on its pooled machines in shortest-processing-time order.
The analysis splits players. A game is generated from by splitting players when every player is replaced by a nonempty set of subplayers and . The constrained game only constrains the feasible coalitions . Splitting each player into its jobs gives the constrained PMS game. Its marginal increments are , with the jobs indexed in nondecreasing order of requirement and . The constrained basic games use the – requirement vector whose first entries are . Splitting further into unit-speed job players gives the UCB games, and the elementary objects are the unit-speed games: players with a unit-speed machine and a job of requirement , and players with a unit-speed machine and a job of requirement .
The goal holds for every finite player set, every assignment of positive rational speeds, and every finite list of nonnegative requirements with any owner map onto .
Total balancedness gives every group of manufacturers, not only the grand coalition, a stable way to share its pooled scheduling cost. The proof is constructive. It writes the game as a nonnegative combination of 0–1 games, and this decomposition is what the paper's basic core (Theorem 5, a line segment of core allocations) is built from. The authors suggest that the same method applies to other sequencing and PMS games in which the order of the players matters.
The paper's proof is on paper only, and no part of it has been machine-checked. The formalization would provide a checked development of the reduction chain (decomposition, core additivity and scaling, splitting players, the unit-speed characterization). Several printed statements on that chain need repair, and the Lean statements record the repairs: core property (i) is misprinted, the printed definition of counts the wrong indices, and Theorem 2's "the core is a singleton" for fails for , where it holds only for the symmetric core.
Lemma 1, Theorem 1, the core properties and Observation 1 are finite-sum manipulations. The obvious approach to the goal, exhibiting a simple nonnegative allocation such as each player's stand-alone cost scaled down, fails: Example 4 has no nonnegative core allocation at all. Concavity-based arguments fail as well, because the game is not concave. The difficulty is concentrated in Theorem 2. To show that both extreme symmetric allocations satisfy every coalitional constraint, one must control with over the integer grid , . Theorem 3 then has to transport core allocations through two levels of player splitting while keeping track of the feasible coalitions.
Players form an arbitrary Fintype N, and is not assumed. Jobs are Fin ψ with requirements p : Fin ψ → ℝ and a surjective father map f : Fin ψ → N. Speeds are v : N → ℚ, positive and cast to ℝ; only the total speed of a player's machines enters. is defined by equation (1) on the sorted requirements, so the goal needs no ordering of the jobs, and . The core is the cost core (). Total balancedness quantifies over every coalition and every , and a statement about the grand coalition alone would be the weaker property "balanced". A splitting scheme is a surjective father map, and total balancedness of a constrained game is required for every feasible coalition with feasible subcoalitions , . The CB games, the unit-speed games and are defined as PMS costs through (1), not through their closed forms, so Theorem 1 and Theorem 2 cannot hold by definition. Lean indices are 0-based, so Lean job is the paper's . Assumption 1 appears only in Theorem 3, as a natural number with .
Everything is built on Mathlib's Finset sums, Multiset.sort, ℚ and ℝ. The cost-game core, splitting and the core properties are reusable for other cost-sharing games. Contributions are welcome on any milestone, and in particular on general lemmas about and on the integer-grid estimates behind Theorem 2.