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?
Assortment optimization asks a retailer which set of products to offer, out of a ground set , when customers choose among the offered products according to a choice model; the expected revenue is a set function of the assortment. Under the multinomial logit model and its mixtures, is neither monotone nor submodular, so the classical theory of submodular maximization (Nemhauser, Wolsey and Fisher 1978) does not apply, and the field has developed algorithms tailored to individual choice models. The revenue functions of a broad class of random-utility models are, however, subadditive, .
Subadditivity alone is too weak for optimization: Dobzinski, Nisan and Schapira (2010) show that with polynomially many value queries no algorithm approximates monotone subadditive maximization under a cardinality constraint better than . Udwani (arXiv:2107.02743v5) introduces a structural property between subadditivity and submodularity, the submodular order, which several assortment problems satisfy (mixtures of multinomial logit with customization, Markov chain choice models) and which restores constant-factor approximation. This mission formalizes the paper's cardinality-constrained algorithm and its guarantee.
Let be a finite ground set of elements and a set function with the normalization . It is monotone if whenever . The marginal value of given is .
An order is a bijection from to the indices ; one reads it from left to right. A set lies to the right of if every element of has a larger index than every element of . Sets are -nested if every element of lies to the right of . The order is a submodular order of if
and a weak submodular order if this holds whenever, in addition, are -nested. A function is submodular exactly when every order is a submodular order.
The problem is to maximize subject to , with optimal value , given access to only through a value oracle that returns for a queried set .
Threshold Add scans the elements once in increasing -index, starting from , and adds the current element whenever and . Algorithm 1 sets , runs Threshold Add with the thresholds for , , and returns the best of the sets.
There is an absolute constant such that for every ground set with every order , every , every and every monotone subadditive with for which is a weak submodular order, the output of Algorithm 1 satisfies
and Algorithm 1 makes at most oracle queries. The constant is left unfixed, so the goal asserts the order of growth of the paper.
and the more general family indexed by a permutation . 2. The query count (p.20): Threshold Add makes at most queries, Algorithm 1 at most . 3. The steps of the approximation proof (p.21): for Threshold Add; the rejection bound ; inequality (5); the guarantee for a single threshold in ; the case ; and the existence of a grid threshold in that window otherwise.
Theorem 2 is the first constant-factor guarantee for a class of monotone subadditive functions that contains the monotone submodular functions and the revenue functions of several assortment problems. The paper's Theorem 3 shows that cannot be beaten with polynomially many queries, even under a strong submodular order, so the factor is the right one. The same theorem yields the paper's results for assortment optimization under mixtures of multinomial logit models with customization, and for streaming submodular maximization, where the arrival order acts as a submodular order. Lemma 1 and Corollary 2 are the structural bounds behind all the algorithms of the paper, including those for budget and matroid constraints.
The result is proved in the paper; to the best of current knowledge none of it has a machine-checked proof. Formalizing it fixes the definitions of submodular order, nested sets and interleaved partitions, and it pins down three places where the printed text needs a correction: the formula defining interleaved partitions, the loop length of Algorithm 1 at , and the last term of inequality (5). Each correction is recorded with a counterexample on the affected item.
The obvious argument for threshold algorithms, as for submodular functions, compares the output with the optimal set element by element using diminishing returns. A submodular order gives diminishing returns only for sets lying to the right of , and a weak order only for nested pairs, so the familiar inequality fails in general. The difficulty is that every diminishing-returns step of the comparison must involve a set lying to the right of everything accumulated before it, and the optimal set and the output are interleaved arbitrarily along . A second, quieter difficulty is bookkeeping: the guarantee concerns the execution of an algorithm and its number of oracle queries, so the formalization must model the algorithm as an object whose queries can be counted.
The ground set is a Fintype α with an order π : α ≃ Fin n, subsets are Finset α and is Finset α → ℝ. "To the right of" and "-nested" are ∀-comparisons of indices, vacuous when a set is empty, which is how the paper applies them. is a finite maximum over the sets with at most elements.
Algorithms are terms of a value-oracle program type: a program either returns a result or queries a set and continues with a program depending on the answer. Algorithms 1 and 2 are built from , , and only and never from ; the query count is a function of the program and . A formalization in which the algorithm receives directly would make the query bound vacuous, and this one rules that out. Threshold Add keeps the value of its current set and uses without a query; "best of" returns the first maximizer. is , which agrees with the paper whenever is monotone with .
Interleaved partitions are blocks O E : Fin m → Finset α covering in which every element of an earlier block precedes every element of a later block; empty blocks are allowed. The query bound reads as , since the printed bound vanishes at .
The development needs only Mathlib's finite sets, sums and real logarithms. The program type and its query count are reusable for any value-oracle algorithm, and Lemma 1 for any analysis under a submodular order (budget and matroid constraints in the same paper). Proofs of any milestone, and of further results of the paper (Theorems 4 and 5, Corollary 3), are welcome.
Many optimization problems are posed with data that are known only approximately: a probability distribution estimated from biased samples, a model calibrated on corrupted measurements, a constraint whose right-hand side will shift. Solving the problem with the on-hand data and hoping for the best can fail badly. The paper's opening examples (§2) show that a vanishing change in a distribution can move the optimal solution of an expectation-minimization problem by a fixed amount. Robust formulations do not help when the shift raises the expectation functions, because a worst case only raises them further.
J. O. Royset, L. L. Chen and E. Eckstrand (arXiv:2204.04762, v4 2023; Mathematics of Operations Research, 2025) take a different route. They embed the actual problem in a family of perturbed problems and optimize jointly over the decision and the perturbation, with a linear "price" on the perturbation. This is Rockafellian relaxation, named after R. T. Rockafellar, whose perturbation framework for duality (Rockafellar–Wets, Variational Analysis, 1998, Ch. 11) it builds on. The mission formalizes the paper's §3: the definitions, the characterizations of exactness (Propositions 3.2 and 3.3) and the convergence theorem (Theorem 3.7) that justifies solving perturbed approximating problems in place of the unknown actual one.
The actual problem is to minimize over . For with values in the paper writes for the infimum, for the effective domain, and, for ,
A Rockafellian for the actual problem is a function with for all . The first argument is a perturbation. The min-value function is , and its conjugate is . For the relaxed problem (3.2) is
Its optimal value is . The Rockafellian is exact, supported by (Definition 3.1) if for all , and strictly exact if the inequality is strict for .
In practice only approximations of a Rockafellian are available, for example built from an estimated distribution. They epi-converge to if (3.8) for every , and (3.9) every has some with . The are (strictly) limit-exact (Definition 3.6), supported by , if their epi-limit is a (strictly) exact Rockafellian supported by . The approximating problem (3.7) minimizes .
Let , , (the goal only needs , ), and . Let be a cluster point of . If the are strictly limit-exact, supported by , then
If the epi-converge to an exact Rockafellian supported by , then satisfies the optimality condition (3.5):
Both clauses are part of the goal. Neither assumes properness, lower semicontinuity or convexity of , or , and neither assumes that the sequence converges.
Theorem 3.7 says that the approximating problems, which are the only ones a decision-maker can solve, are asymptotically equivalent to the actual problem whenever the chosen Rockafellians are strictly limit-exact. It is the abstract result behind §4 of the paper. There, Theorem 4.4 (φ-divergence perturbations of distributions), Theorem 4.5 (support uncertainty) and Theorem 4.6 (ℓ₁ Rockafellians) each verify the limit-exactness hypothesis in a concrete setting and then obtain convergence of solutions from Theorem 3.7. The second clause covers the non-strict case, in which only an optimality condition survives in the limit.
The results are proved in the paper, partly by reference to Royset–Wets, An Optimization Primer, 2021, Theorem 5.5, for proper functions, with the extension to functions taking left as "the arguments … carry over". None of them has a machine-checked proof. A formal proof would close that gap explicitly and provide reusable -valued infrastructure: ε-argmin with the domain condition, epi-convergence, tilting, and the argmin-of-epi-limit theorem. This infrastructure serves any later formalization of epi-convergence arguments in stochastic programming.
The obvious argument for (A.2) uses and the recovery sequences of (3.9). It goes through in the reals, but every step must be checked in . The limit may equal at some points. A liminf along a subsequence has to be compared with (3.8), which speaks of full sequences. And the conclusion has to come from , not from properness. A cluster point is not a limit, so the subsequence must be completed to a full sequence converging to before (3.8) applies.
For the characterization results, the identities and the splitting (A.1) involve infima of -valued functions shifted by finite linear terms. These are routine only once the extended arithmetic has been pinned down.
(Fin m → ℝ) × (Fin n → ℝ) with the product topology, which has the same convergent sequences as the Euclidean norm. is y ⬝ᵥ u. Values are in EReal, and infima and suprema are taken in that complete lattice.PerspEpi.SeqEpiConv, and the effective domain is the published AubinLipschitz.effDom. A cluster point is MapClusterPt, runs over from , and , which the paper does not define, is relaxed to 0 ≤ ε ν and ε → 0, which hold on every reading.Welcome contributions: proofs of the milestones in the order listed, general EReal lemmas (liminf and limsup under real shifts converging to a limit, infimum of a real shift), and a general first-countable version of the argmin-of-epi-limit theorem.
A firm that must buy a fixed quantity of a commodity often faces suppliers one at a time: a quote arrives, the firm decides how much to buy at that price, and the decision cannot be revisited. Electricity procurement, cloud capacity and spot markets for raw materials all have this shape. When the marginal cost of buying grows with the amount bought from one supplier (congestion, convex production costs), the natural model charges for buying from supplier , with .
This is a minimization prophet inequality: the buyer is compared with a prophet who sees every price in advance. The classical prophet inequality (Krengel–Sucheston 1977, Samuel-Cahn 1984) is a maximization problem with a single accepted item. Its minimization version behaves badly: without further assumptions, no online policy is within a bounded factor of the prophet (Esfandiari, HajiAghayi, Liaghat, Monemizadeh 2015). Qin, Vardi and Wierman (MOR 2024, doi:10.1287/moor.2021.0173) allow fractional purchases, monomial costs, and an in-house production option: the buyer can always produce the commodity itself at a known price. Their Theorem 2 computes the exact competitive ratio in that case.
There are sellers, met in the order . Seller 's price coefficient is a random variable with known law , and are independent. Seller is the buyer's own production, with . The other sellers' laws belong to the class of all probability distributions with support in , for a fixed . No upper bound and no moment condition are imposed.
A policy observes and then buys , with . Its cost is
The prophet pays . The competitive ratio with in-house production is
with the infimum over policies outside the supremum over distributions. Throughout, , and is the power mean.
Both inequalities are needed: no policy does better on every instance, and some policy achieves the value on every instance.
The theorem gives an exact, closed-form competitive ratio for a sequential procurement problem with unbounded price risk. Its value depends only on , and the price floor , and it is finite even when the external prices have infinite mean. Without in-house production, the paper's Theorem 3 shows that the ratio grows with the upper end of the price range. So the in-house option is what makes the problem robust to price spikes, and Theorem 2 measures that effect exactly. The paper's Corollary 1 states the linear-cost value , obtained as the limit of (3). The proof also shows that the gap is already achieved by the simple policy that buys everything in-house: on worst-case instances, adaptivity gains nothing.
The paper's proof is informal at two points that a formal development must make precise. The upper bound applies Lemma 2 with and with infinite means. The lower bound reads several limits as equalities, and it uses DP optimality by citation. In addition, the recursion (25) is printed with the exponent , which makes Lemma 8 false as printed; the mission states the corrected exponent (Lemma 8's title records the correction). None of the results has a machine-checked proof.
The upper bound is the easy half: it only needs a single policy and a pointwise lower bound on . The lower bound carries the weight. It must hold against every measurable causal policy, however adaptive, and comparing a policy with the prophet realization by realization does not work: the policy's loss comes from rare high prices it cannot foresee, not from any single price vector. So the optimal adaptive cost has to be known exactly. That is a finite-horizon dynamic program with continuous controls over arbitrary price laws, whose optimality the paper only cites (milestone 5), and whose closed form needs a backward induction in real powers (milestone 6). The final step takes two limits whose order matters: for fixed , then . Exchanging them, or treating the page's limit statements as equalities at finite , gives false statements.
Sellers are Fin n with ; Lean's seller 0 is the paper's in-house seller . Prices are real; an instance is a family of probability measures ν : Fin n → Measure ℝ with ν 0 = dirac 1 and for the other sellers, and the joint law is the product measure. Policies are families of measurable maps that depend only on and sum to for every price vector. Expectations of costs are lower Lebesgue integrals, and the ratio is computed in , so policies with infinite expected cost are allowed and give ratio . is the real infimum over the simplex. The DP objects use 0-based stages.
The trivializing readings are ruled out. The policy class and the instance class are nonempty (the all-in-house policy and the long-shot instance are admissible), and on every instance, so the ratio is never a junk value. The infimum is taken outside the supremum, so a policy cannot depend on the instance.
A complete development needs Hölder or Lagrangian arguments in finite dimension (Lemma 1), Jensen with its equality case on an interval (Lemma 2), Fubini on product measures (Lemma 3), a finite-horizon dynamic programming theorem for measurable policies with interval controls (milestone 5), and real-power calculus (Lemma 8). The DP optimality statement and the extremal Lemma 2 are reusable beyond this mission. Contributions that prove any milestone, or that factor out general lemmas (finite-horizon DP over product measures, the Jensen equality case), are welcome.
Many simulation estimators are biased, and the bias is controlled by a tuning parameter that also controls the noise. A central finite difference for the derivative of an expectation is the standard example: a perturbation size gives a bias of order and a variance of order . Simulation budgets are then spent on a trade-off. Choosing as the right power of the number of runs gives the best order of the mean squared error (Fox and Glynn, 1989; Glynn and Whitt, 1992). The best constant requires the model's bias and noise coefficients, which are unknown in practice. Debiasing methods such as multilevel Monte Carlo (Giles, 2008; Rhee and Glynn, 2015) remove the bias when runs at consecutive levels can be coupled.
Lam, Zhang and Zhang (arXiv:1902.04673v1) ask what can be gained without coupling and without those coefficients, by weighting independent runs made at different tuning parameters. They measure the gain against the plain sample average, in a minimax sense.
Fix . Each run at tuning parameter outputs
where , and as . The class of all such outputs, with arbitrary , and higher-order terms, is (SimulationOutput q₁ q₂).
Let and . The baseline averages independent runs at the single value ; its mean squared error is . The weighted estimator is with , where is any real triangular array; its mean squared error is . The asymptotic risk ratio is
A designer picks and a calibration in , and the adversary answers with a model in and a .
This is Theorem 8, part 1, of the paper.
The value is attained at and at weights with two decay rates,
where comes from an explicit matrix and an optimal solution of a one-dimensional problem (24). This is Theorem 8, part 2. Both parts form the one goal theorem, theorem_8.
In the order of the argument: the asymptotic MSE of the baseline (Theorem 1); the bias-variance form of (31); the need for ; the closed form of a minimum-norm problem (67); the reduction of (60) to (24); the asymptotics of ; the scaled limit of (75); the uniform floor; the limit of (76) with ; the negligibility of errors (81), (82); the lower bound for every configuration; and the value of the ratio at .
The value tells how much an estimator can improve on the sample average with no knowledge of and . For central finite differences (, ) with it is , for every model and every ; for forward differences () with it is . The form of is a design rule that uses only , and . The restricted classes treated earlier in the paper, recursive and averaged estimators, have a minimax ratio above (Theorems 3 to 7), so the gain comes from the general weighted class.
The theorem is proved in the paper. No machine-checked version is known to exist, and the platform held no statement on this subject when this mission was drafted. The mission produces a reusable formal account of biased simulation outputs and their mean squared errors under independent runs at varying parameters, and a checked minimax value. The array also attains the value, so optimal weights are not unique; the goal does not claim uniqueness.
The obvious route is to replace by its leading terms and optimize. That fails to be a proof at three places. The matrix has entries on different scales, and the remainders of order are what decide feasibility in (24). Problem (24) is nonconvex, its feasible set can be disconnected or, at finite , empty, and the claims concern every selection of minimizers, for which there is no formula. The weights take both signs, so the terms of the model cannot be bounded termwise against the main sum, and they meet the early runs, where is not small and nothing is known about the bias beyond finiteness.
A model is the number , the constants , , and for each a probability law on with finite second moment; the conditions on and the variance are stated along . Independent runs are coordinates under Measure.pi over Fin n, and index is run . and are integrals of squared errors. The risk ratio and the value lie in ℝ≥0∞. The inner max is a supremum, which need not be attained for a general array; the outer min is IsLeast. The inverse in is Matrix's, and it is genuine for . Optimality of is required for all large , as (24) can be infeasible at finite .
A trivializing formalization is excluded: the mean squared errors are not defined by a formula, the weights are chosen before the model, is free, and the remainders of the model are arbitrary.
A complete development needs the second-moment calculus for product measures, sharp asymptotics of for , and asymptotics of a inverse. The first two are reusable beyond this mission. Contributions toward any milestone are welcome, including proofs that take a different route from Appendix C.
Many estimation problems ask for the solution of a linear fixed-point equation on a high- or infinite-dimensional space, when only noisy unbiased samples of and are available. The leading example is policy evaluation in reinforcement learning: the value function of a Markov reward process solves the Bellman equation , and temporal-difference (TD) learning with linear function approximation estimates it within a -dimensional subspace of features. Galerkin methods for elliptic equations and linear regression with a misspecified model have the same structure. Because the search is restricted to , every such method pays an approximation error in addition to the statistical error of finite data.
Timeline of the approximation-error question:
Let be a real Hilbert space, a bounded linear operator with boundedly invertible, , and the unique solution of . Let be a subspace with orthonormal basis , with coordinate map and adjoint . The projected operator is the matrix (projMat), and
is assumed throughout (kappa). The projected fixed point solves , so (vbar).
The data are i.i.d. pairs with , , and the second-moment bounds of Assumption 1(W): for unit and . Stochastic approximation with stepsize runs from , and the Polyak–Ruppert average is (theta, vIter, vhat). The instance-dependent quantities are the approximation factor
(alphaFactor), the noise covariance (SigmaStar), and
(En, Hn).
Eq. (45a), obtained from Lemma 3 (a bound through ) and Lemma 4 (that norm is at most of the matrix in ).
Lemma 5 bounds for the raw iterates, Lemma 6 decomposes , and Eq. (45b) gives
for , and above a threshold.
There are universal constants such that, under the conditions above, for every
The goal is stated with every printed term, for an arbitrary Hilbert space and subspace. The printed sample-size condition does not suffice, and two hypotheses are added (see Formalization scope).
Theorem 1 separates the error of averaged stochastic approximation into an approximation part and a statistical part, each with an instance-dependent constant. The factor can be much smaller than worst-case contraction factors, and the paper's lower bounds (Theorems 2–4) show that no estimator using the same information achieves a smaller factor, and that is the local minimax rate. Applied to TD(0) with linear features, it gives instance-optimal guarantees for policy evaluation; applied to Galerkin approximations and linear regression, it recovers and sharpens known bounds.
On the formal side, the platform has Polyak–Juditsky's asymptotic normality for averaged linear stochastic approximation and asymptotic results for TD, but no finite-sample oracle inequality for projected fixed-point equations. Theorem 1 is proved on paper, not formalized anywhere known. The mission's corrections make the formal target a true statement: the printed version is refuted by one-dimensional examples.
The deterministic part needs operator algebra on in a possibly non-separable Hilbert space: inverting on all of and comparing an operator norm on with an eigenvalue of a matrix, where (not ) enters. The stochastic part is a second-moment analysis of a random linear recursion: the iterate is a product of random matrices, and its expectation must be controlled through independence of the next observation from the past. The averaged error requires a martingale orthogonality argument plus a bound on the telescoping remainder, and every constant must be tracked to land on universal . The obvious route of reading the burn-in step on p.31 as stated fails: with the printed threshold the initialization bias is not dominated by the variance, which is why the corrected goal carries an extra threshold.
φ : OrthonormalBasis (Fin d) ℝ S with . is a unit and are hypotheses; is the closed-form projected fixed point.IsObsModel), with Assumption 1(W) in these coordinates. This covers every instance of the paper.LowRankMEG.lam · 1 (largest eigenvalue of a symmetric matrix). is natural-number division, is deterministic, expectations of squared norms are lower Lebesgue integrals in .Min-sum set cover asks for an order of the elements of a ground set that minimizes the average time at which a hyperedge is first covered. Feige, Lovász and Tetali showed that the greedy algorithm is a 4-approximation and that no better constant is possible unless P = NP (Feige, Lovász, Tetali 2004). Min-sum vertex cover, pipelined set cover, precedence-constrained min-sum set cover and ordinary set cover are relatives of it. Happach and Schulz observe that all of them are single-machine scheduling problems with a mixture of AND-precedence constraints (a job waits for all of its predecessors) and OR-precedence constraints (a job waits for at least one of its predecessors) (Happach, Schulz, arXiv:2001.07011v1, pp.1–3). For min-sum set cover the vertices are jobs of length 1 and weight 0. The hyperedges are jobs of length 0 and weight 1, and each hyperedge has its vertices as OR-predecessors.
The paper gives one LP-based algorithm for this whole class. Its guarantee depends on a single structural parameter: the largest number of OR-predecessors of a job.
The jobs are . Job has a processing time and a weight . The AND-arcs form an acyclic digraph. The OR-arcs define , the OR-predecessors of , which may be empty.
A schedule is a vector of completion times on one machine. Job runs without interruption in , no two jobs overlap, and the machine starts at time 0. The schedule is feasible if
Idle time is allowed. The objective is .
An OR-arc is redundant if another OR-predecessor is a transitive AND-predecessor of , since always finishes first. With redundant arcs removed,
The algorithm works on a normalized instance. Weights on are moved to new zero-length successors in , the jobs that can complete at time 0 are set aside, and the processing times are scaled to integers. For it solves the time-indexed LP (1) with variables , , . For general it solves the interval-indexed LP (5) over the intervals , . For an optimal , the -point of is (the -interval for LP (5)). For and , the -schedule sorts the -jobs by and the -jobs by . Ties are broken along the precedences and otherwise arbitrarily, and the jobs are processed in this order without idle time.
For every instance with , LP (1) of the normalized instance has an optimal solution. For every optimal and every , -schedules exist and are feasible. An explicit set of at most candidate values of , with , contains a such that every tie-breaking gives
For every and rational , the same holds with LP (5), , at most candidates, , and the ratio .
The guarantee is stated for every optimal LP solution and every tie-breaking. The cost counts the weights of all jobs of the original instance.
The milestones follow the paper's proof:
For min-sum vertex cover, where every hyperedge has two vertices, the theorem gives a 4-approximation even under precedence constraints (Corollary 1, p.9). For min-sum set cover it gives a -approximation, where is the largest hyperedge. The same analysis covers AND-only scheduling (, ratio 2) and mixed AND/OR constraints. With release dates added, the bound becomes (Lemma 4, not in this mission).
Theorem 1 is proved in the paper. To this mission's knowledge it has no machine-checked proof, and Prove2Me has no prior formalization of OR-precedence scheduling. The mission adds a model of AND/OR-precedence schedules, the two LP relaxations, -points of an LP solution, and the derandomization by candidate values of . It also corrects constraint (5f): as printed, LP (5) is infeasible on some instances.
The analysis is short, but every object it uses has edges. Three points need care.
The normalization is also not routine. Deleting a zero-length job literally can remove the cheapest OR-predecessor of another job and raise the optimum. The mission therefore sets aside the least closed set of jobs that can complete at time 0.
A, B, jobs A ⊕ B. Processing times are in ℚ≥0 (part (i) assumes them in ) and weights are in ℝ≥0. The AND-arcs are relations inside A and inside B with acyclic transitive closure (Acyclic).C : N → ℝ, feasible as above. The comparison is with every feasible schedule, not with an infimum.σ : N ≃ Fin |N|, and its list schedule is .sInf over ℕ, and .x_jl = 0 when .Contributions are welcome on any milestone. The reusable parts are the LP relaxation lemmas, the -point integral identities (2) and (27), and the derandomization lemma.
Many contracts in finance and insurance give their holder several exercise rights that must be used at distinct dates: swing options in energy markets, flexible interest-rate caps, partial surrender options in life insurance. Valuing such a contract is an optimal multiple stopping problem. When the model itself is uncertain, or when the holder is risk averse, the value is not an expectation but a nonlinear evaluation: a robust (worst-case) expectation over a set of priors, a recursive coherent risk measure, or a -expectation. Laeven, Schoenmakers, Schweizer and Stadje (arXiv:2006.01802v2) treat all of these at once through a dynamic monetary utility functional (DMU) and prove an additive dual representation of the value in terms of martingales, with no stopping times in it.
Timeline of the dual approach this mission builds on:
Let be a filtered probability space and an exercise horizon. Positions form a linear subspace of that is closed under and and contains every indicator , . A DMU is a family , , satisfying
Two further properties are used. (P1) is subadditivity, . (P2) is sensitivity: and imply . All (in)equalities between random variables hold almost surely.
A reward is adapted with ; it may take either sign. A -martingale is an adapted with , and is the set of those with . The holder of rights chooses stopping times , and the upper Snell envelope is
The -Doob martingale of has and increments .
Let satisfy (C1)–(C4) and (P1), let be adapted and . Then the envelopes exist, satisfy the Bellman principle
and, for every with and with ,
The infimum is attained at . If is also sensitive, then equals the pathwise maximum at these martingales almost surely.
In proof order: (C5)–(C6); optional sampling for -martingales (Lemma 2.1); the stopped functional (Lemma 2.2); the first display of the proof of Proposition A.2; weak duality for one right (Lemma B.1); its -right version (B.1); weak duality (B.3)–(B.4); the -Doob decomposition (2.4)–(2.5); the Bellman principle (3.5) with existence and attainment of the envelopes; the backward recursion (4.13) of Proposition 4.4; and the pathwise upper bound of p.41.
The theorem replaces a supremum over -tuples of stopping times by an infimum over martingales, evaluated pathwise. Any choice of martingales therefore gives an upper bound on the value of the contract, and a near-optimal choice gives a tight one. Under sensitivity the optimal martingales are surely optimal: the pathwise maximum is already constant given . These facts drive the primal–dual algorithm and its convergence analysis in §4 and the explicit upper and lower bounds in a Brownian–Poisson filtration in §5. With the conditional expectation, the theorem recovers the known pathwise dual for linear multiple stopping.
The result is proved in the paper; to the authors' knowledge none of it is formalized. A machine-checked version adds three things. It verifies the Bellman principle (3.5) and the existence of the essential suprema for , which the paper states without proof. It records the correct reading of the problem after the last date. And it repairs one step of the published argument (next section).
The weak-duality half goes by induction on through stopped functionals . Each step needs (C2)–(C4) to commute with indicators of events , and subadditivity to remove the martingale penalty. Since is nonlinear, no linearity of expectation is available, and every exchange must be justified from the axioms.
The obvious argument for the pathwise upper bound fails. The printed proof (p.41) telescopes the Doob increments and bounds each bracket by . That inequality is false: take , , , , ; the bracket equals . The theorem itself is unaffected. The bound follows instead by backward induction on the date and the number of rights through the recursion (4.13), using only (3.5) and the definition of the Doob martingales.
A second subtlety is the end of the time grid. If rights may lapse at the last date and can be negative, two natural readings of the paper's extension ", for " disagree, and under one of them (3.5) fails. The mission therefore works on an arbitrary exercise horizon , which covers both the original problem (, ) and the extended problem ().
Random variables are classes in Ω →ₘ[P] ℝ, so every (in)equality is almost sure. Essential suprema and infima are IsLUB and IsGLB in this lattice, and the pathwise maximum is a finite lattice supremum Finset.sup' over the tuples . A stopped value is the class of . Stopping times are -valued Mathlib IsStoppingTimes, and stopping vectors are ordered almost surely, with the optimum attained by a surely ordered vector. Rights are indexed from , so the paper's superscript becomes L - k. The clause (C2) includes , which the paper presupposes when it evaluates .
At the Bellman principle keeps only its first branch: the remaining rights must be exercised at . This is not a change of the theorem. With and , for , every date has , and those again satisfy (C1)–(C4), (P1) and (P2).
The goal is an existence statement for the envelopes, so it cannot hold vacuously, and the essential supremum is not assumed to exist. The identity functional with the constant filtration satisfies every hypothesis, so none of them is contradictory.
The definitions (DMU, -martingale, stopped values, stopping vectors, Snell envelopes, -Doob martingale, pathwise dual maximum) are reusable for any discrete-time nonlinear optimal stopping development. Contributions of every milestone are welcome. The Bellman principle with existence and attainment, and the backward recursion (4.13), are the most self-contained.
Block coordinate descent (BCD) minimizes a function on by taking a gradient step in one block of coordinates at a time. It is a standard method for large problems, and its convergence theory for smooth and convex objectives is well developed (Beck & Tetruashvili, 2013). Many optimization problems, however, are posed on a Riemannian manifold: orthogonal or Stiefel matrices in Procrustes problems and PCA, products of spheres in tensor problems. A manifold has no global coordinates, so BCD does not transfer directly.
Gutman and Ho-Nguyen (arXiv:1912.10627v3, 2020; Mathematics of Operations Research, 2023) propose tangent subspace descent (TSD). In each inner step it projects the Riemannian gradient onto a subspace of the current tangent space and moves along the exponential map. They show that naive spanning conditions on the subspaces do not make TSD converge (their Theorems 3.2 and 3.3), and introduce a deterministic condition, the -gap ensuring condition, under which it does. This mission formalizes that deterministic convergence theorem (Theorem 4.5) and the lemmas leading to it.
The manifold is abstracted to a Riemannian setting: a metric space ; for each a finite-dimensional real inner product space with norm ; an exponential map ; and for each with a linear isometry (parallel transport). Two axioms hold: , and any two points are joined by some with and . A gradient field is -smooth if whenever , and is geodesically convex if for every minimal-norm with .
Algorithm 1 runs outer iterations with inner steps each:
where is the orthogonal projection onto a subspace of chosen by a selection rule. Transporting each projection back to the start of the loop gives on , and the seminorm .
Assumption 4.1 (block smoothness) asks for constants with along the iterates. Assumption 4.2 (-gap ensuring) asks that whenever , there is an orthogonal decomposition of with and . Write for the extreme and
With stepsizes , attained, and :
every limit point of is stationary, and if is geodesically convex and the sublevel set has diameter at most ,
Theorem 4.5 gives TSD the guarantees of Euclidean BCD: stationarity at rate and an optimality gap for geodesically convex objectives. The gap ensuring condition is checkable for concrete rules: the paper verifies it for product manifolds (recovering cyclic BCD) and constructs a deterministic rule on the orthogonal group (its Theorem 6.1), whose convergence follows from Theorem 4.5.
The result is proved in the paper; none of it is machine-checked. The mission produces a checked version of the deterministic analysis and records three minimal corrections found while checking it. Theorem 4.5 needs and part 1 of Lemma 4.4 needs : without them a rule whose lines are orthogonal to the gradient satisfies every printed hypothesis while the iterates stall. Proposition 4.2 needs the proviso , which Remark 4.1 states. Each correction carries a two-dimensional counterexample in its item.
Each step of the paper's proof is elementary (triangle and Cauchy–Schwarz inequalities, counting, telescoping). The difficulty is that every quantity lives in a different tangent space: the projection of step acts on , the gap condition is checked on , and the two are related only through transports indexed by points of the manifold. The natural first idea, comparing gradients and projections in one fixed space as in Euclidean BCD, is unavailable; the transported projections are not an orthogonal decomposition in general, and the proof must control their deviation from one (Proposition 4.2) and the drift of the transported gradients (Lemma 4.3). The other delicate point is part 1 of Theorem 4.5, where far-step iterations are counted separately from near-step ones; the printed count is off by one, and the bound holds by applying the argument to .
All statements live over an abstract RiemSetting (M a metric space, fibres T x finite-dimensional real inner product spaces, exp, transports T x ≃ₗᵢ[ℝ] T y indexed by a proof of exp x v = y) with the two axioms above. Every connected, geodesically complete Riemannian manifold is an instance; Mathlib has no exponential map or parallel transport, so the results are stated for this abstraction. The gradient is a field given as data. A run of Algorithm 1 (TSDRun) carries its iterates, stepsizes, selected subspaces and a connecting vector for each transport back to ; Assumptions 4.1 and 4.2 are imposed along the run. The outer index is the paper's; the inner index is Fin m, shifted by one. The conclusions use , not . The diameter bound is a pairwise distance bound, not Metric.diam, which is on unbounded sets; is a real number below that attains. "" and "" are stated with explicit constants that contain nowhere and only through , which keeps the dependence on .
The hypotheses are not vacuous: a proved check shows Euclidean space with satisfies every hypothesis of the goal with a nonzero initial gradient, and another shows the decomposition clause of Assumption 4.2 fails when two inner steps select the same line.
A complete development needs elementary inner-product facts about orthogonal projections and operator norms, the two-case decrease, and a counting and telescoping argument; nothing beyond Mathlib's inner product space library. Proofs of the milestones and the goal are welcome, as are alternative arguments. The randomized analysis (Theorem 5.2) and the rule (Theorem 6.1) are not part of this mission.
In large populations of anonymous agents (commuters choosing routes, users choosing servers, customers choosing a bar), each individual has a negligible effect on the others, and the natural equilibrium notion is the Wardrop equilibrium (WE): only cheapest actions carry mass. A mediator such as a navigation app may instead recommend actions at random, correlating the recommendations across agents. Such mediated outcomes are correlated Wardrop equilibria (CWE), and their coarse version (CCWE) describes the long-run behaviour of populations using no-regret learning. A basic question for the designer of such a mediator is whether correlation can produce anything other than a mixture of ordinary equilibria.
Koessler, Scarsini and Tomala (arXiv:2107.06312, Mathematics of Operations Research, 2025) study Bayes correlated Wardrop equilibria as limits of correlated equilibria of large finite games. Their Proposition 4 answers the question above for complete-information games with a convex potential: correlation, even coarse correlation, adds nothing, and all equilibria have the same costs. The result extends a theorem of Neyman (1997) on correlated equilibria of finite-player potential games with convex action sets to nonatomic games with finite action sets, and it covers coarse correlated equilibria, which Neyman's setting does not reduce to Nash equilibria.
A nonatomic game has a finite set of populations, a size for each population, a finite action set for each population, and continuous cost functions . A flow profile records the mass of population playing ; the flow set is
and is the cost of action to a member of population .
For every game, , and the first inclusion can be strict (the El Farol game, Example 1 of the paper).
If has a convex potential, then
any two WE satisfy for all , and for every CCWE and every WE , -almost every has for all . The statement has no constants. It covers every finite set of populations and actions, every positive size and every continuous cost family with a convex (not necessarily strictly convex) potential.
The result. Proposition 4 says that in convex-potential games a mediator, however it correlates recommendations, can only implement mixtures of Wardrop equilibria, so mediation has no value for any welfare objective. This generalizes Díaz et al. (2009), who showed for a class of routing games that the best CWE is no cheaper than the best WE. Combined with the paper's convergence result (Proposition 1), it implies that correlated equilibria of large finite congestion games concentrate near mixtures of Wardrop equilibria (Corollary 2). The CCWE clause implies that no-regret flow sequences have empirical distributions accumulating on (Corollary 3). The cost clause generalizes the uniqueness of equilibrium costs in congestion games with nondecreasing costs (Roughgarden 2007, Theorem 18.8) from one-dimensional loads to arbitrary convex potentials.
Formalizing it. The result is proved on paper; no machine-checked version is known. The mission adds abstract nonatomic population games, correlated and coarse correlated Wardrop equilibria and convex potentials, which do not exist on the platform in this generality (only routing-specific models do). The formalization also corrects the printed Lagrangian. The printed omits , and with it no saddle point exists.
The first half of the proof (every CCWE is a distribution over minimizers of ) integrates the gradient inequality against and turns a strict inequality summed over populations into a violation of (4.3) for one population and one action. The bookkeeping between the sum over populations, the integral and the minimum over actions is where a careless argument goes wrong.
The cost clause is the harder half. is only convex, so WE need not be unique, and a naive argument ("the minimizer is unique") fails. Gradients at two minimizers of a convex function coincide only along the directions the constraint set allows, so one needs KKT multipliers, the saddle-point form of the convex program, the exchange property, and a support argument on the relative interior of the (convex) set of WE. The final passage from the relative interior to all of uses continuity of the costs.
Flow profiles live in the dependent function space (Flow A, a finite-dimensional normed space), and is the subtype FlowSet γ. Costs are continuous functions on this subtype. is ProbabilityMeasure on the subtype with its Borel σ-algebra, so every integrand in (4.2), (4.3) and is continuous on a compact space and the integrals are genuine. is "-almost every flow is a WE", which equals since is closed. The partial derivative is fderiv ℝ Φ y applied to the unit vector . The potential is a function on the whole flow space, and only its values on matter. The goal is the complete-information game of §4: there is no state .
"Convex potential" is read as convexity on an open convex neighbourhood of . Convexity on alone is too weak, because it makes the cost clause false: vanishes on and is a potential for , whose WE and have different costs. "The same costs profiles" is read as equality of every cost , not only those of actions with positive flow. The KKT milestone takes , since the printed KKT list omits . The populations and action sets may be empty, in which case the statements hold for trivial reasons. This is the paper's generality, not a loophole.
A complete development needs: compactness of and integrability of continuous functions on it; first-order characterization of convex functions on open convex sets; KKT for a convex program with linear constraints; relative interiors of convex sets in finite dimensions. The definitions of nonatomic games, (coarse) correlated Wardrop equilibria and potentials are reusable for the paper's other results (Propositions 1–3, Corollaries 2–3) and for other population-game papers. Contributions to any milestone are welcome; milestones 4, 7 and 8 are self-contained convex-analysis facts.
Maximizing a set function is a basic task in combinatorial optimization and algorithmic game theory. Computing an agent's demand under prices amounts to maximizing , which need not be monotone even when the valuation is. XOS functions generalize submodular functions, and they are studied in combinatorial auctions, where they are usually assumed monotone (Lehmann, Lehmann, Nisan 2006). Filmus, Kawase, Kobayashi and Yamaguchi study the non-monotone unconstrained problem in the value oracle model, where the function can be accessed only by asking for its value on a set (arXiv:1811.09045v3). Their second tight bound, the subject of this mission, determines the approximation ratio achievable in polynomial time as a function of a structural parameter of the input, the width.
Let be a nonempty finite set of size . A set function is XOS if there are additive functions , with , such that
Here means . Both and may take negative values. When such a representation is fixed, is its width, and a function with a representation of width is -XOS. For , a set is an -maximizer of if .
For a fixed representation, is the set of clauses attaining at , and is the clique with respect to .
An algorithm receives , and sees only through its oracle. It knows neither the clauses nor .
There is one deterministic value-oracle algorithm and one absolute constant such that, for every , every and every -XOS function on elements, the output satisfies
and, for , is an exact maximizer with . The algorithm is not told . It removes the elements with and then runs Algorithm 4 of the paper.
The milestones follow the paper's order:
If the clauses are given, maximization is immediate: . The theorem shows that an oracle hiding the clauses costs a factor and no more in polynomial time. Theorem 5 of the same paper shows that for a ratio below needs exponentially many oracle calls, even for randomized algorithms, so the bound is tight, and the case is the exact boundary between polynomial solvability and hardness. The algorithm is also adaptive to the width: no bound on is needed in advance.
The result is proved in the paper, published in Mathematics of Operations Research, and is not known to have a machine-checked proof. This mission asks for such a proof, on top of a concrete oracle cost semantics in which the claimed running time is a theorem about a program. The lower bound, Theorem 5, and the results for unbounded width are not part of this mission.
The obvious approach is to recover the clauses and then apply the §1 formula, and it fails: an oracle value reveals only the maximum at one set, the same has many representations, and the width is unknown. The elementary candidates are not enough either. Taking the best of sets that cover gives only a -maximizer, by the pigeonhole bound, and improving the ratio from to is the main step, because the optimum need not be comparable with any single set the algorithm computes. A width-free guarantee adds a further requirement: one candidate family has to work for every for which is -XOS, including representations with repeated clauses. Finally, the cost bound is about an algorithm that does not know , so its dependence on exists only through the analysis.
Ground sets are finite: Fintype E with Nonempty E in the goal, and in the milestones the Finset L.toFinset of a repetition-free list . Subsets are Finset E, and is a function Finset E → ℝ. A representation is a family w : Fin k → E → ℝ with no sign condition, and the maximum is stated with IsGreatest, so width has no representation and is a consequence. The width in IsKXOS k f is exact, and clauses may repeat.
An algorithm is a value of the inductive type OracleProg E α, with constructors for returning, querying a set, and one elementary step. No constructor mentions : this is what makes the theorem a statement about value-oracle algorithms, since a Lean function of could return a maximizer for free and make the theorem empty. The cost is computed by run f p, and is the number of oracle calls plus elementary steps. A query costs whatever the size of the set, and comparisons of oracle answers are unit-cost real operations. The charges of every program are recorded in its docstring: set operations that are not on one element are charged their size. The algorithms are the programs growClique, cliquePhase, buildY, alg3, alg4 and xosMax, transcribed line by line, with "pick" and "foreach" in list order and the first best candidate at Line 10. The theorem is about xosMax L for every enumeration , with quantified before the ground set, , and . There is no positivity hypothesis on the goal.
OracleProg with its run and run_bind is reusable for other value-oracle algorithms. Contributions of general lemmas on foldlM costs, and of alternative proofs of the milestones, are welcome.
A model trained to minimize average loss can perform badly on a subpopulation: a minority group in a language corpus, or a demographic underrepresented in a medical or vision dataset. Marginal distributionally robust optimization asks for good performance on every sufficiently large subpopulation of the covariates, without knowing which subpopulations matter. Duchi, Hashimoto and Namkoong introduce this formulation and analyze an estimator for it. It is relevant to fairness, to robustness under covariate shift, and to the analogue of observational studies in causal inference. Compared with joint robustness over (Duchi and Namkoong 2021), the marginal formulation does not chase label noise.
Let with and , and let be the loss of a parameter (Assumption A1). Fix . A potential minority subpopulation is a law on such that the covariate marginal decomposes as for some and some law ; write for the set of these. The worst-case subpopulation risk is
It is the conditional value-at-risk of the conditional risk . For and , its upper bound is the risk .
Assumption A3 says that and a version of the conditional risk are -Lipschitz. Writing for the -Hölder functions on , the population objective is
Its sample version is the infimum over of the convex function of display (15). The marginal DRO estimator minimizes .
There are depending only on such that, with probability at least , every empirical minimizer satisfies
for and , with the paper's constant (17).
In proof order: CVaR duality (Lemma D.1); the dual form of (Lemma 2.1); the bound and its variational form (display (9)); the Hölder-restricted objective (Lemma 3.2); the convex form of the plug-in (Lemma 4.1); Hölder extension (first display of Appendix D.7); the uniform plug-in bound (Lemma 4.2); Wasserstein concentration (Lemma D.3); and the deterministic chain of Appendix D.8, which is (18) with in place of .
Theorem 1 certifies a convex, implementable procedure for a risk that cannot be estimated directly without replicate labels: its minimizer's worst-case risk is controlled by a bound that is nearly optimal over , at the rate . The paper's Theorem 2 shows that this exponential dependence on dimension cannot be avoided.
The result is proved on paper; no machine-checked proof is known to exist. The present mission also records three corrections to the arXiv text: the coefficient of (15) is rather than ; the constants must depend on ; and Lemma 4.2 needs truncation at and a different constant. The first two change the goal; each is backed by an explicit counterexample, recorded in the corresponding statement. The journal version was not consulted. The formalization would therefore settle the corrected statements.
The obstacle is that is not observed: without replicates at a single , a plain empirical average cannot estimate it, and replacing it by yields the conservative joint formulation. The variational form moves the conditional expectation onto a test function, but the optimal test function has a denominator that can vanish, and only then does the Hölder radius matter. Uniform control then requires an empirical-process argument over a Hölder class in dimension , at Hölder exponents , where the sharp concentration results of Fournier and Guillin are stated for the transport cost rather than for the dual supremum used here, so Lemma D.3 is a target of its own.
The Lean development works on (EuclideanSpace ℝ (Fin d) × ℝ) with the Euclidean distance written out (dist2), since Mathlib's product metric is the supremum metric. The sets are bounded, and need not be measurable or closed; is carried by . The conditional risk is a data function , a version of Mathlib's condExp given the first coordinate (IsCondRisk), Lipschitz on . Empirical means are finite sums, and is its dual supremum (holderDev). Theorem 1 bounds the outer measure of the samples at which some minimizer violates (18), so it needs no measurable selection. The constants are quantified before . A trivializing reading is ruled out on both ends: a constant depending on the data would make the theorem empty, and eLpNorm keeps non-integrable out of (12).
Route for solvers: milestone 9 gives (18) with on every sample in ; the comparison for turns into the goal, and milestone 8 at bounds the rest. The cases and are deterministic.
The development needs CVaR duality, duality for conditional risks, Hölder extension (McShane on the metric ), finite-dimensional convex duality, and concentration of the dual Wasserstein distance. McDiarmid's inequality is on the platform. The Hölder extension, the CVaR duality and the Wasserstein bound are reusable beyond this mission, and supporting lemmas for them are welcome.
The Nash social welfare of an allocation of indivisible items is the geometric mean of the agents' valuations. Nash proposed it for the bargaining problem as the objective characterized by a set of natural axioms, and it has since become a standard objective in fair division because it balances efficiency against fairness. Maximizing it exactly is NP-hard, already for additive valuations, so the research question is how well it can be approximated in polynomial time.
For additive valuations, constant-factor approximations are obtained by computing a market equilibrium of a related Fisher market and rounding it (Cole and Gkatzelis, 2015; Cole et al., 2017). Garg, Hoefer and Mehlhorn (arXiv:1707.04428v3) extend this approach to budget-additive valuations, in which agent values a bundle at with a utility cap . The associated market has both utility limits for buyers and earning limits for sellers, a model the paper studies on its own (existence via money clearing, an FPTAS, PLS and PPAD membership). The rounding result was the first constant-factor approximation for this class of valuations.
An instance has a finite set of agents, a finite set of items, values and caps . An integral allocation gives each item to at most one agent, and agent has budget-additive valuation
The Fisher market of the instance has divisible goods in unit supply, buyers with budget , linear values and utility cap , and sellers with earning cap . Given prices , good is a maximum bang-per-buck (MBB) good of if and for all . A thrifty and modest equilibrium (Definition 2.1) requires that every buyer buy a utility-maximizing affordable bundle consisting of MBB goods and worth at most , that each good be allocated at most its modest supply , and that unsold supply have price . A buyer is capped if it reaches ; is the set of capped buyers, and the buyers interested in some good of price . The market is money clearing if every set of buyers has total budget at most the total earning cap of the goods they value.
The rounding procedure (§4.1.2, Appendix B) works on the allocation graph , assumed to be a forest. It roots every tree at an agent, lets each good keep only its largest child agent and only if a threshold holds ( with active budget , or on zero-price trees), gives childless goods to their parents, and then, recursively from each root, gives the root its most valuable child good and every other good to its child agent. Every root choice and tie-break is allowed.
For every instance, every thrifty and modest equilibrium of its market, every run of the rounding procedure with output , and every integral allocation ,
Neither money clearing nor is assumed: without money clearing every integral allocation has welfare .
The theorem shows that a fractional relaxation in the form of a market equilibrium with both utility and earning limits loses only a constant factor against the integral optimum for budget-additive valuations, and that a simple tree-rounding procedure realizes this factor. Combined with the paper's FPTAS for approximate equilibria (§4.1.3), it gives a polynomial-time -approximation (Corollary 4.1). The upper bound of Theorem 4.1 is stated in terms of equilibrium prices and caps only, so it serves as a certificate for any allocation.
The results are proved in the paper; Lemmas B.1–B.4 have their proofs omitted as "almost completely identical" to Lemmas 4.4–4.7. None of them has a machine-checked proof. A formalization fixes the conventions the text leaves implicit (zero prices and infinite MBB ratios, the unboxed demand problem, the meaning of a tree "at the beginning of step (b)"), checks the omitted appendix proofs, and records one correction: Lemma 4.3(d) as printed fails for goods of price .
The obvious argument, giving every good to a buyer of it, fails because a good may be shared by many buyers and each loses value. The rounding removes children and reassigns goods along a recursion path, and the root of each recursive step must take one child good, which can cost its children more than half their value. The losses compound along the recursion path, and the bound must still be paid for by quantities of the equilibrium alone (caps of capped agents, prices above ). Comparing with the integral optimum is a separate difficulty: the optimum is not an equilibrium quantity, and Theorem 4.1 is needed to bound it by one.
Agents and items are finite types, data are real numbers, and integral allocations are maps Option B. The MBB condition is cross-multiplied (), so zero prices need no infinity; the modest supply at price is ; the demand problem maximizes over all affordable without a box; allocations satisfy only . Milestones carry the standing assumptions of §4.1 (, money clearing, normalization for ) as hypotheses. A run of the procedure is a record of its free choices (an orientation of the forest from root agents, a largest child per good, a greedy pick per agent) together with a validity predicate; kept children, the forest after preprocessing, its components, the recursion path and the output allocation are defined from it. Every statement quantifies over all valid runs; a valid run exists only when the allocation graph is a forest.
The goal is not vacuous: one agent with one item and has an equilibrium and a run giving the agent the item, and a two-agent zero-price instance shows runs with a kept and with a cut child (verification files).
Needed infrastructure: finite sums and products, connected components of simple graphs, and an AM–GM inequality (in Mathlib). Contributions of proofs of any milestone, and of the existence of a valid run for every forest, are welcome.
Many linear programs in operations research have a small number of constraints and an astronomically large number of columns: cutting-stock patterns, rankings in nonparametric choice estimation, state–action pairs of a Markov decision process. The standard remedy is column generation, which needs a problem-specific pricing subproblem. Akchen and Mišić (arXiv:2007.10461v5, forthcoming in Operations Research) study a simpler alternative: draw column indices at random from a distribution on and solve the LP restricted to the sampled columns. Their main guarantee bounds the loss of optimality of this column-randomized linear program with high probability, at a rate that does not depend on . The proof technique adapts the random-features analysis of Rahimi and Recht (Advances in Neural Information Processing Systems, 2009) from unconstrained regression to constrained LPs, repairing feasibility by LP sensitivity analysis.
The complete problem is the standard-form LP
with an real matrix. Throughout (§3.1, p.6), is feasible and bounded, , and . Its dual is . A basis is a set of indices with nonsingular, and the basic dual solution for is , feasible or not. Write for the optimal value of a problem and for its optimality gap. Norms are , , , and .
A sample is , drawn from : the indices are independent and each equals with probability . Repeats are allowed. With and , the column-randomized LP and its dual are
For the distributional counterpart is
Let bound for every basic solution of . For every , with probability at least over : if is feasible and , then
It holds for every , every probability vector (zero entries allowed), every and every .
The bound separates two sources of error. depends only on how well the sampling distribution covers a good solution, and the paper bounds it separately for structured and random instances (Theorems 3–6). The second term is distribution-free and decays at rate . Together they give the finite-sample justification for solving huge LPs by sampling columns, which the paper applies to cutting stock and choice-model estimation.
The result is proved in the paper; nothing in this mission is open mathematically. No part of it is formalized on Prove2Me: the platform has McDiarmid's inequality and LP strong duality, but no column-sampled LP, no distributional counterpart, and no vector concentration bound of the Rahimi–Recht type. Lemma EC.1 is cited in the paper without proof, so a formal proof also checks the external ingredient.
The obvious argument fails at feasibility. The sparsified vector is a good estimate of , but in general, so is not feasible for and does not bound . The paper repairs this by comparing with the problem whose right-hand side is , at a price of for an optimal dual of . That price is then controlled uniformly only because has a basic optimal solution, which requires and accounts for the rank condition in the event. On the probabilistic side, Lemma EC.1 needs McDiarmid's inequality on a product space together with a variance bound for a vector-valued mean in a Euclidean space. Neither fits an off-the-shelf scalar concentration lemma.
All indices are 0-based (Fin m, Fin n, Fin K). The sample is an ordered tuple J : Fin K → Fin n under the product measure sampleMeasure ξ K, built from on Fin n with the discrete σ-algebra. "With probability at least " is ENNReal.ofReal (1 - δ) ≤ sampleMeasure ξ K S, where the event is the implication "( feasible and ) → bound", as Appendix A (p.ec3) states. It is not a conditional probability. Optimal values are real infima (lpValue, vJ, vDistr). Because sInf of an empty or unbounded set is 0 in Lean, every statement carries what makes them true minima: feasible and bounded (standing), feasible (inside the event), and feasible (hdistr). When is infeasible, and the paper's claim is vacuous. is . Basic dual solutions are indexed by an injective β : Fin m → Fin n with linearly independent columns and the equations , which avoids the matrix inverse. The norms are explicit sums and suprema.
No hypothesis trivializes the goal. The proved sanity file checks that the encodings mean what they say. In the identity example of p.ec3, is infeasible for every sample. A LP has the true value . A two-column instance has . The sampling measure is a probability measure. The -hypothesis is satisfiable.
The definitions split into general standard-form LP objects (ColumnRandLP.StandardLP), norms (ColumnRandLP.Norms) and the paper's model (ColumnRandLP.Model). The LP layer and Lemmas EC.1–EC.3 are reusable beyond this mission. Formal proofs of any milestone are welcome, as are alternative routes to Lemma EC.1 (for instance through a Hilbert-space bounded-differences inequality).
A retailer chooses which products to offer, its assortment, and customers then buy one of the offered products or nothing. The probabilities are given by a discrete choice model, which in practice is estimated from data and is therefore uncertain. Robust assortment optimization handles this by maximizing the worst-case expected revenue over an uncertainty set of model parameters. Rusmevichientong and Topaloglu (Oper. Res. 2012) studied it for the multinomial logit (MNL) model.
Wang, Peura and Wiesemann (Oper. Res. 2024) ask whether the retailer can do better by randomizing: drawing the assortment from a lottery chosen before nature picks the worst-case parameter. Randomized strategies are known to help against an adversary in other robust problems, for example in "dice"-sion making (Delage, Kuhn and Wiesemann, Manag. Sci. 2019) and in mixed-integer distributionally robust optimization (Delage and Saif, INFORMS J. Comput. 2022). The paper's Theorem 1 gives an exact, model-free characterization of the instances where randomization brings no gain. Sections 4–6 of the paper apply it to the MNL, Markov chain and preference-ranking models.
An instance is a tuple with the following parts.
The expected revenue of under the realization is , and its worst case is . The deterministic robust value is
A randomized assortment is a probability vector over the admissible assortments. Its expected revenue is and its worst case is . The randomized robust value is
By Definition 1, the instance is randomization-receptive if and randomization-proof otherwise. The proof works with the set of revenue vectors and its convex hull .
Assume that is lower semicontinuous on for every . Then the instance is randomization-proof if and only if
where is the set of probability distributions on . The "if" half is stated for every instance, without the semicontinuity hypothesis, since it holds as printed.
The correction. The paper assumes only that is compact, and as printed the "only if" half is false. Take , , , , and a choice model with for and at . This instance satisfies every stated assumption and is randomization-proof: , with every minimum attained. Yet forces , and then . The added hypothesis is the minimal repair. It follows from continuity of , which holds in all three models the paper studies, so none of the paper's applications is lost.
Theorem 1 replaces a statement about all lotteries by a single certificate, a distribution on the uncertainty set. A distribution that caps every assortment's expected revenue at proves that no randomized strategy beats the best deterministic one. Its absence proves that some lottery does. The paper derives from it that strong duality implies randomization-proofness (Corollary 1), and it underlies the analysis of when randomization pays under the MNL, Markov chain and preference-ranking models.
The result is proved in the paper, apart from the gap above, but has not been formalized. The mission adds the corrected statement with its counterexample. It also provides a model-free Lean layer for robust assortment problems (instances, deterministic and randomized robust values, randomization-proofness) that model-specific developments can instantiate.
The "if" half is short: a dominated point of bounds the worst case of every lottery. The "only if" half carries the difficulty. A minimax theorem on delivers a minimizer only in the closure of . That point need not be the revenue vector of any distribution on , and the counterexample above is exactly this failure. Lower semicontinuity is what lets a limit point be dominated by an actual revenue vector. A second step needs care: the expectation vector of an arbitrary Borel probability measure on must be shown to lie in itself, not merely in its closure.
Products are Fin n and is Option (Fin n), with none the no-purchase alternative. Assortments are Finset (Fin n), and is a Finset of them. is a set in a finite-dimensional real normed space with its Borel σ-algebra. The standing assumptions form the predicate Instance.IsValid. Minima and maxima are written as real ⨅/⨆. They are bounded for valid instances, and the milestones state attainment with IsLeast/IsGreatest. is stdSimplex ℝ 𝒮, indexed by the admissible assortments only. is ProbabilityMeasure 𝒰, and the condition also requires -integrability, which holds automatically under the hypotheses.
The values and are defined as the paper's max–min values, never through or . Defining them through a dual would make Theorem 1 a tautology.
The proof needs a finite-dimensional minimax theorem (Mathlib's Sion.minimax, or the platform's BanditAlgorithm.exists_pointwise_le_of_compact_convex_weighted_le), compactness of convex hulls of compact sets in finite dimensions, and the barycenter-in-convex-hull lemma. These pieces are reusable beyond this mission. Contributions to any milestone, and to the measure-theoretic barycenter lemma in particular, are welcome.
A trade agent buys a product from a seller and resells it to a buyer whose demand is fixed by contract. Agricultural produce, surplus inventory and commodities are often traded this way: the agent owns no warehouse, so units it buys beyond the demand must be disposed of, and demand it cannot serve incurs a contractual penalty. The agent's only lever is the bid, the unit price it offers for the seller's lot of units.
Two uncertainties meet in this decision. The bid may be rejected: the seller accepts only bids at or above an unknown ask price . And when the bid wins, only a random fraction of the lot may be usable (yield uncertainty). The classical random-yield newsvendor literature (e.g. Yano and Lee, 1995) fixes the unit cost and optimizes a quantity; here the quantity is fixed by the seller and the unit cost is the decision. Çakıcı and Karaesmen (SSRN 4409114, 2023; later published in Manufacturing & Service Operations Management, 2024, doi:10.1287/msom.2023.0190) formulate this trade agent's newsvendor problem and characterize the optimal bid in closed form. This mission formalizes their main single-seller result, Theorem 1, from the October 14, 2023 working-paper version.
On a probability space let (the ask price) and (the yield fraction) be independent real random variables.
If the bid wins, the agent pays , receives usable units, ships , and earns
If the bid loses, it earns . The expected profit (Lean: expProfit) is the expectation of this profit. The constants
are the paper's (rho) and its expected benefit of bidding (expBenefit). The expected sales-to-supply ratio is (salesSupplyRatio). Assumption 1 (Assumption1) requires to be strictly increasing on . An optimal bid maximizes over (optimalBids).
Let . Then:
Under and Assumption 1: the equation has a unique root (32)–(33), and the expected profit is strictly increasing on , strictly decreasing on , with unique maximizer (34)–(35). Lemma 2: for a continuous in with , for every . Finally, implies and , the first and the outer inequality of (37).
Theorem 1 separates the agent's decision into two parts. Whether to bid depends only on the yield distribution and the costs, through the comparison of the expected sales-to-supply ratio with the threshold , which mirrors the critical fractile of the classical newsvendor with overage cost and underage cost . How much to bid depends on the ask-price distribution only through the first-order condition (6). The comparative statics of the paper (Theorems 2, 3 and 5, monotonicity of in costs, in the ask-price distribution and in the variability of the yield) are read off this characterization, and its multi-seller model (Theorem 6) builds on the single-seller analysis.
The result is proved on paper; no machine-checked proof is known. A formal proof needs the reduction (4) of a two-stage stochastic profit to a deterministic objective, which uses the independence of the bid outcome and the yield, and an optimization argument on a non-concave objective. The mission also records a gap in the printed proof: the middle inequality of display (37) invokes Lemma 2, which needs a continuous yield, while Theorem 1 allows any yield in . For a Bernoulli yield that inequality is an equality. The milestone states the first inequality and the outer inequality, both of which hold for every admissible yield, and drops the second one.
The expected profit is not concave in unless is linear, which is impossible on all of . So the first-order condition does not certify a maximum by itself, and global optimality has to come from the sign pattern of the derivative. The printed argument also asserts that the first-order condition has a solution because is strictly increasing. Strict monotonicity gives uniqueness only. Assumption 1 does not make continuous, so existence of the root has to be argued without assuming a continuous density. Finally, part (iv) cannot be obtained by appealing to Lemma 2, as explained above.
All quantities are real numbers. The ask price and the yield are measurable functions on one probability space, independent (IndepFun Z U P). The expected profit is the Bochner integral of the primitive profit of displays (2)–(3), not the closed form (4), which is a milestone. The density is a separate function w' with HasDerivWithinAt (winProb P Z) (w' b) (Set.Ici 0) b and 0 < w' b for . A two-sided derivative at is impossible for a nonnegative ask price with . Optimality, monotonicity and unimodality are all on (Set.Ici 0). Over all of every negative bid would tie with , since vanishes there.
Display (3) as printed attaches to and to . The formalization follows the definitions of and on p.8, the only assignment consistent with display (4). "Decreasing" in part (i) and "unimodal" in part (ii) are read in the strict sense the proof establishes. Every denominator (, , , ) is positive under the hypotheses, so no junk value of real division enters. No assumption on the law of is made beyond and . In particular continuity of and are hypotheses of Lemma 2 only, not of the goal.
The development needs Mathlib's independence and integration API (IndepFun, integrals of products of independent variables), Darboux's theorem for derivatives within an interval, and the monotonicity-from-derivative lemmas on convex sets. The definitions (win probability, expected profit, expected benefit of bidding, optimal-bid set, unimodality on ) are reusable for other bidding-newsvendor models. Proofs of the milestones in any order, and alternative arguments for Lemma 2 (its printed proof via concavity is roundabout), are welcome.
Online marketplaces such as Amazon, Walmart and Alibaba let sellers pay to have their products shown in sponsored slots. The platform decides which assortment of sellers to display to an arriving consumer, and the consumer then chooses among the displayed products. Unlike a standard ad auction, a seller's value from being shown depends on who else is shown: a consumer who sees many attractive substitutes is less likely to buy any particular one. The quantity that drives this substitution, a product's attractiveness to the current consumer, is estimated by the sellers from their own models and is not known to the platform.
Balseiro and Désir (SSRN 3821382, 2022; published in Management Science, doi:10.1287/mnsc.2022.4603) ask how much welfare a platform must give up to run a truthful mechanism in this setting. Without private information, the problem is classical assortment optimization under the multinomial logit model, solved by revenue-ordered assortments (Talluri and van Ryzin, 2004). With private attractiveness the first-best assortment is not incentive compatible, and the paper quantifies the loss with competitive ratios against first best. Its main finding is that the worst-case cost of truthfulness grows with the number of sellers.
There are sellers. Seller earns a public revenue if the consumer buys its product, and . Its product has an attractiveness , private to seller ; a profile is . If the assortment is displayed, the consumer buys from seller with the MNL choice probability
The welfare of is , and the first-best welfare is .
A deterministic mechanism maps reports to an assortment and payments . Seller , reporting when the true profile is , gets
so the assortment depends on the report but the purchase probability on the true attractiveness. A mechanism is ex-post incentive compatible (IC) if for all , and individually rational (IR) if . Let be the set of IC and IR deterministic mechanisms. The prior-independent competitive ratio is
For a partition of , the partition mechanism displays a part of highest welfare and charges a displayed seller the revenue of its threshold type; is the partition mechanism of the singletons .
If for all , then
and is IC, IR and attains it: its worst-case ratio over priors equals . The printed statement gives and "achieved by "; with the bound proved on p.28 this is the equality.
In proof order: the taxation property (Lemma 2.3) and its menu form (1); Claim G.1 on the difference of two choice probabilities; the forced-display interval of Corollary 5.1; truthfulness of nested partition mechanisms (Corollary 5.3); the lower bound for (p.28); the reduction of priors to point masses (Prior independent); and the three steps of Appendix G.3 at the profile : a singleton gets of first best, an assortment with two sellers forces a profile with ratio , and so every IC mechanism has .
The result shows that the cost of ex-post truthfulness is not a constant factor: no truthful deterministic mechanism can guarantee more than a fraction of first-best welfare uniformly over priors, and the trivial mechanism that displays only the best single seller already guarantees . Under the separation condition , displaying several sellers buys nothing in the worst case. It contrasts with the case without substitution, where VCG implements first best, and with the prior-dependent ratio, which the paper shows to be ; the two-seller case contains Proposition 4.3.
The result is proved in the paper; no machine-checked proof is known. A formalization would check a proof that, as printed, has gaps: Corollary 5.1 needs the extra conditions and no ties in , Corollary 5.3 holds for the nested partitions but not for every partition, the payment rule (3) violates IR at ties, the last display of Appendix G.3 inverts , and its opening claim holds only up to . The milestones state the corrected versions, each with a counterexample to the printed one.
The lower bound is a pointwise inequality. The upper bound must hold for every IC mechanism, and IC mechanisms in this model are not characterized: the interdependence through makes a seller's preference over assortments depend on its own attractiveness non-monotonically. The obvious approach, evaluating a mechanism at the single profile where first best displays everyone, fails: a mechanism that displays two or more sellers there achieves a good ratio at . A bad profile for such a mechanism exists, but it lies far from , and its existence rests on what IC forbids the mechanism to do along the way, which the paper describes only partially (Corollary 5.1). That partial characterization is delicate at ties between assortments with the same , and the separation condition is what keeps such ties away from the profiles that matter.
Sellers are Fin n (0-based: Lean's seller is the paper's ) with [NeZero n]; attractiveness profiles are Fin n → ℝ≥0; assortments are Finset (Fin n). Payments are real-valued and mechanisms carry no measurability condition. Expectations are lower Lebesgue integrals ∫⁻ of ENNReal.ofReal of the welfare, and ratios, infima and suprema live in ℝ≥0∞. The prior is excluded from the infimum (and from the pointwise infimum): there both expectations vanish and the ratio is , which in ℝ≥0∞ would evaluate to and make trivially. The ratio condition is written . Ties in are not resolved by the paper, so is formalized for every welfare-maximizing selector, and partitions are Finpartitions.
The definitions (MNL choice, welfare, mechanisms, IC/IR, support, , partition mechanisms, nested partitions) are self-contained and reusable for other results of the paper, including the prior-dependent ratio of §5.4. Proofs of any milestone are welcome, as are alternative arguments for the upper bound.
Governments and firms often buy development work through contests: suppliers race through milestones, and the first to finish gets a prize. Such contests stall when a supplier learns that it has fallen behind and stops working, so the organizer's control over what suppliers learn is a design lever alongside the prize. Khorasani, Körpeoğlu and Krishnan study this lever in Dynamic Development Contests (Operations Research, 2024). This mission follows the authors' manuscript with its Online Appendix.
The question belongs to the literature on information in dynamic contests. Halac, Kartik and Liu (2017) and Bimpikis, Ehsani and Mostagir (2019) compare disclosure rules in experimentation contests, Ely (2017) characterizes optimal dynamic persuasion when the state evolves exogenously, and Ely, Georgiadis, Khorasani and Rayo (2022) treat optimal feedback in a contest. Here the state is created by the agents' own unobserved effort, so disclosure and effort feed back into each other.
Two risk-neutral agents race through two stages. Time is continuous, the horizon is infinite, and there is no discounting. Agent chooses an effort at flow cost . Effort is private, and a stage is completed at a Poisson arrival with instantaneous probability . A completed stage is a success. It is seen only by the agent concerned and the principal. The first agent with two successes ends the contest at the date and receives the fixed reward , and the reward is budget-constrained:
Before the contest the principal commits to a disclosure policy: a rule, possibly random, private and asymmetric, that turns the record of first successes into messages. Agents then play a Nash equilibrium of the resulting game.
The policy PCSD works as follows. Write for the two beliefs defined by (10) and by the theorem, and let . Before the principal says nothing. A first success arriving at is disclosed at that instant with probability , and is otherwise never disclosed. An agent with no success works until her first success, or the end of the contest, or the disclosure of her rival's progress. An agent with one success works until the end.
For every and every in the range above, the stated strategies are a Nash equilibrium under PCSD; the belief path satisfies ,
and it is the unique solution of this initial value problem; and for every disclosure policy and every Nash equilibrium under ,
In proof order: the law of motion of the belief (9) and its Bayes derivation; the properties of the belief path; full effort after one success; the first-stage incentive constraint (EC.39)–(EC.40); the continuation values (EC.41); the value in phase 2 and incentive compatibility in phase 1; the equilibrium; the value-duration identity (EC.42); the bound above ; and the time to the first success.
The theorem identifies the optimal information design for a principal who cannot afford to keep both agents working by reward alone. Disclosure is delayed at first, then used at exactly the rate that holds the value of a first success at the minimum needed for effort. The result separates what information can achieve from what requires money: at this budget a rule of disclosure alone gives the best lead time.
No part of this result has a machine-checked proof, as far as a search of the platform shows. The mission contributes a complete model of the contest over all disclosure policies, together with the verified optimality theorem. The model is at a generality that the paper states only in words, and its statements on continuation payoffs are stated as expectations over clocks rather than as formal manipulations of a Bellman equation.
The statement here corrects the paper in one respect. As printed, Theorem 2 has a finite date with and after it. But (12) reads , so is a rest point, and no solution starting below it reaches it in finite time. With and , a solution with would be constant, against . Hence , at every date, and . The printed figure's is a numerical tolerance.
The equilibrium half is a verification, but in a game of incomplete information in continuous time: a deviation changes the distribution of the record and the agent's posterior beliefs along it.
The optimality half is the hard one. The printed proof shows that PCSD minimizes the continuation payoff at each belief , and concludes that it minimizes the time after the first success. This compares policies at equal beliefs, but a policy controls the distribution of beliefs, and at equal dates the comparison fails. The published route also ignores equilibria with reduced first-stage effort. Numerical checks support the statement, and a repaired route exists. In it, let be the probability that both agents reach the second stage. The time spent in each state gives ; the identity prices ; and the deviation of never working gives . For this already matches the value of PCSD. For the same step must be applied to the deviation that stops at when still in the first stage, and this case is only a sketch. It needs a bound on the chance that a laggard who catches up wins, and control of slower first-stage efforts.
Agents are Fin 2 and time is ℝ≥0. A record is Fin 2 → ℝ≥0∞, with ⊤ for "no success yet". Arrivals come from four independent unit-exponential clocks, one for each agent and stage: a stage ends when reaches its clock. play computes the realized record, end date and winner from the clocks, state by state.
A Policy U M has a probability space U, any message type M, and a signal to each agent that depends on the record only as it stands at that date. A strategy is admissible when it is jointly measurable, has values in , and depends only on the agent's own first success and her signals. An agent never reads her rival's success directly, which is the content of the model. The lead time is a lintegral in ℝ≥0∞, which is when a contest may fail to end. Payoffs are EReal, so an infinite cost is .
Competitors are not restricted: IsNash does not ask for symmetry or for any behaviour of a leader. A class such as time-dependent , public signals or symmetric equilibria would be a special case, and optimality against such a class is not the goal. A hypothesis that reintroduces a finite is not acceptable either.
A complete development needs the Poisson clock calculus (exponential races, memorylessness, the identity above), conditional laws of the record, and a verification theorem for (EC.39). The clock calculus and the verification theorem are reusable beyond this mission. Sketches for the case are especially welcome.
Approximate linear programming computes a value function approximation (VFA) for a discounted-cost Markov decision process by maximizing a weighted average of the VFA subject to the Bellman inequalities (De Farias and Van Roy, 2003). The method needs a set of basis functions, and the choice of those functions is a recurring difficulty in operations research applications. Pakiman, Nadarajah, Soheili and Lin replace hand-engineered bases by random basis functions, whose parameters are drawn from a known density, in the spirit of random features (Rahimi and Recht, 2008). Their self-guided scheme samples further bases at each iteration and links consecutive VFAs by constraints (arXiv:2001.02798v2). This mission formalizes the paper's error bound for that scheme.
Let be a nonempty compact state space, a nonempty compact action set, an immediate cost, a transition distribution on , and a discount factor. The value function is the continuous solution of
A class of random basis functions consists of , a sampling density on , and , with . Weighting functions live in the Hilbert space with inner product and norm . Assumption 2 requires with , universality of the class, a finite second moment of , a Lipschitz constant of , and .
Given bases , the sampled VFA is . FALP maximizes its -average subject to the constraints (8):
Self-guided FALP adds the guiding constraints (9), for all , where is the previous iterate.
With the space attached to by Definition EC.2, is the component of orthogonal to its closure. Put , with .
If on , then for all and , with probability at least over fresh samples there is with (i) feasible to (8), (ii) for all , and (iii) , where
In proof order: Lemma EC.1 (continuous functions feasible to the Bellman inequalities lie below ); Proposition 1 (an optimal solution of the feature-based exact linear program represents ); Proposition 4 (monotonicity of Algorithm 2's VFAs, bounded by ); Proposition EC.1 (sup-norm approximation of by random bases); Proposition EC.2 (orthogonal decomposition of ); Proposition EC.3 (replacement of the first component); Proposition EC.4 (approximation by further bases).
The result. Theorem 2 quantifies what a further batch of bases buys given the current VFA, at the dimension-free rate . The earlier sampling bound for FALP does not apply to the self-guided sequence, because consecutive VFAs are coupled by (9). The monotonicity of Proposition 4 gives a sequence that does not worsen state by state.
The formalization. The paper's statements are proved on paper only. Nothing on approximate linear programs or random-feature value functions is on the platform, and no machine-checked proof of these results is known here. The mission records two corrections that a formal statement forces, and exposes one open point in the printed proof. Its reusable products are a continuous-state discounted MDP layer and a sup-norm random-feature bound.
The central difficulty is Proposition EC.1. The natural Monte Carlo estimator of has weights , and these are only square-integrable under , not bounded, so the classical bounded-weight concentration argument of Rahimi and Recht does not apply directly. A plain truncation of the weights does not recover the rate . The printed proof of Proposition EC.1 has a gap: in (EC.7) the kernel smoothing lacks the normalization by the volume of the ball, and inserting it breaks the bound (EC.8). No counterexample to the corrected statement is known, and it is trivially true when ; its truth for large is not settled by the paper. The goal and Proposition EC.4 rest on it. A proof or a refutation of Proposition EC.1 is the most valuable contribution to this mission.
Conventions. and are subsets of EuclideanSpace ℝ (Fin d) and EuclideanSpace ℝ (Fin m); finite action sets are compact sets. is a hypothesis: a function continuous on solving the Bellman optimality equation, so Assumption EC.1 and the existence of an optimal policy are not assumed. Integrals are Lebesgue integrals on , which excludes sampling laws without a Lebesgue density. is Lp ℝ 2 of . Sup-norm bounds are stated pointwise on . "With probability at least " means a measurable event of mass at least inside the set where the property holds, and all coefficients are chosen after sampling. The first samples are fixed; the probability is over the new ones. "-feasible" means (9) relaxed by .
Correction 1. Page 9 prints as , without a square root. Bounds in that quantity are quadratic in while the error is linear, so they fail under scaling. All bounds here use the square root.
Correction 2. Page 19 defines as a subset of the class . With on a bounded , every element of is entire and tends to a constant at infinity, so a finite combination of sines in is constant, and the theorem fails. The goal's ranges over all of .
Risk. Definition EC.2 uses indicators of single points inside a Lebesgue space, so , , and does not depend on , contrary to the paper's narrative on p.19. The mission formalizes the printed definition; the verification file proves the degeneracy. The statement is not vacuous: the joint satisfiability of the goal's hypotheses is proved there too.
The representation is universally quantified and must not be replaced by a free function: is pinned down by the Bellman hypothesis. Contributions welcome: proofs of the milestones; Proposition EC.1 or a counterexample; a continuous-state MDP library.
A set function is submodular when its marginal gains shrink as the set grows. Submodular minimization over all subsets is solvable in polynomial time, and Edmonds' greedy description of the polymatroid gives the convex hull of the epigraph of a submodular set function through one linear inequality per permutation of . Many models in integer programming, facility location, sensor placement and image segmentation do not use only decisions. They have general integer and continuous variables, bounds, and precedence constraints of the form .
Q. Yu and S. Küçükyavuz (arXiv:2211.07726v2, 2023; later in Mathematics of Operations Research, 2025) extend the polyhedral picture to DR-submodular functions of mixed-integer variables under box and monotonicity constraints. They describe the convex hull of the epigraph completely, and it turns out to be a polyhedron.
Let be a finite index set of variables, the integer ones, and a directed rooted forest (every vertex has at most one parent, no directed cycle). and are the descendants and the ascendants of , both containing . Upper bounds satisfy , for , and on every arc. The feasible set is
and the epigraph is . A function is DR-submodular on if whenever and (Definition 1.1). The paper also assumes .
Fractional bounds above integer variables create the set . Assumption 1 (no two elements of on one directed path, children of integer) and Property 4.2 (each has a single integer child with ) are standing from §4. Assumption 2 asks below every with . The polyhedron consists of the box and monotonicity constraints together with one mixed-integer rounding (MIR) inequality per (6a–6c). Its extreme points are explicit points , (eq. (9)). A valid permutation of (Definition 5.2) yields linear coefficients (eqs. (27)–(29)) and the DR inequality
Under the standing conditions, Assumptions 1, 2 and Property 4.2, for every with that is DR-submodular and concave along each coordinate on :
The theorem turns the mixed-integer nonlinear problem into a linear program over an explicit polyhedron. With the exact separation algorithm of §7 (not part of this mission), this gives the paper's polynomial-time solvability claim. In the case with no arcs, it recovers Edmonds' description of the epigraph of a submodular set function through its greedy extreme points. The MIR description of (Theorem 4.21) is a polyhedral result for forest-ordered mixed-integer sets in its own right.
The paper's result is proved on paper but has no machine-checked proof. The printed statement needs a correction. A -linear function with and satisfies the paper's hypotheses on one continuous variable with , yet violates the DR inequality . The proof of Lemma 3.2 passes from midpoint concavity to concavity without regularity. The mission adds exactly the property that proof claims, namely concavity of along each coordinate on . Every continuous DR-submodular function has it. Formalizing the paper settles whether this one correction suffices.
The obvious approach writes a point of as some convex combination of extreme points and applies the DR inequality term by term. This fails. The DR inequality is not implied by concavity, since is in general neither convex nor concave. The bound holds only for the particular chain selected greedily by Algorithm 2 (Lemma 6.3). Showing that the greedy chain exists, is valid and gives non-negative weights needs a careful case analysis of the MIR vertices (Lemmas 5.17–5.21). The extreme-point description of rests on explicit primal–dual optimal pairs of a linear program on trees (§4.1–4.2). Validity at the points in case (3) needs Assumption 2 and a telescoping argument across the subtree of each (Lemmas 6.15–6.18).
Coordinates are a finite type V with N : Set V, arcs a relation A : V → V → Prop, and u : V → ℝ. The upper bounds are finite, by the paper's own reduction on p.5. Permutations are Fin |V| ≃ V, with the paper's 1-based index kept in , and . The index "0" of is none. is a chosen child, unique under Property 4.2, which every statement assumes. is constrained only on the real box (DR-submodular, coordinate-concave, ). Algorithm 2 is a relation covering every tie-break, so statements about "the output" hold for every output. The convex hull is Mathlib's convexHull, not its closure.
The DR family ranges over valid permutations only, and contains the MIR rows. Dropping either changes the right-hand set, and a verification file checks that the MIR row cuts off a point and that validity excludes some permutations. The goal's hypotheses are satisfiable ( on one variable meets all of them), so the statement is not vacuous.
A complete development needs elementary facts about finite forests (ascendant chains, uniqueness of the deepest ascendant), convex hulls and extreme points of polyhedra in , and one-variable concave functions. The forest and convex-hull lemmas are reusable beyond this mission. Contributions are welcome on any milestone; §4 and §5 do not involve and can be attacked independently of §6.
A decision maker with limited capacity (a college admitting students, a lender approving loans) treats only the fraction of applicants with the highest score . The applicants know the rule and invest effort to change their covariates , so the score distribution, and hence the admission threshold, depends on the rule itself. When the rule is used over many periods, each cohort reacts to the previous threshold and the threshold moves. Whether it settles, and where, decides the value of the policy.
Sahoo and Wager, Policy Learning with Competing Agents (arXiv:2204.01884v5), model this as a capacity-constrained treatment rule facing strategic agents. They take the quantile rule of Bhattacharya and Dupas (2012) and add agent best responses in the spirit of strategic classification (Hardt et al., 2016). They show that the threshold converges to a mean-field equilibrium threshold , and then learn by gradient ascent on the equilibrium policy value. This mission formalizes the convergence result for a finite number of agents, Theorem 4, together with the chain of agent-level, mean-field and finite-sample results that leads to it.
Covariates live in a convex compact set , and the selection criterion is a unit vector . There are finitely many agent types , with probabilities (Assumption 2). Type has raw covariates and a cost that is , -strongly convex and minimized at (Assumption 1). Write .
An agent who reports against the previous threshold has expected utility
where is the distribution function. The noise perturbs the report. The best response maximizes this expected utility over , and Assumption 3 requires it to be interior. The expected score is .
The score of an agent is , with distribution function , and denotes the lower -th quantile at the capacity level . The mean-field iteration is , and an equilibrium threshold is a fixed point .
In the finite model, a fresh i.i.d. cohort of agents responds at each step to the realized previous threshold, and is the empirical distribution function of their scores:
Suppose . Let be a Lipschitz constant of , , and , and let be the margin (4.2). Then
The goal also asserts that exists and is unique and that some exists, so the bound is not vacuous.
Theorem 4 justifies treating the mean-field equilibrium as the object of policy learning. A finite system run long enough with large enough cohorts has thresholds close to , so the equilibrium value is what a decision maker actually obtains, and its gradient is what the estimators of §5 target. The bound is explicit. Since is linear in and is linear in small , the sample size scales with .
The formalization adds three things. First, a Lean model of strategic response under a capacity constraint, reusable for other threshold and quantile rules. Second, a machine-checked chain from Gaussian smoothing to contraction of the population quantile. Third, a corrected finite-sample argument: Lemmas 33 and 34 are false as printed (counterexamples in their statements). The milestones state what the proof of Theorem 4 actually uses, namely a one-step bound at the random threshold and a pathwise recursion, and Theorem 4 itself survives unchanged. None of these results has a machine-checked proof on the platform.
Every noise threshold in the paper comes from the sharp bound on the slope of the Gaussian density, set against the strong convexity . A cruder bound does not reach the stated noise levels. The finite iteration is not a contraction: each step adds fresh sampling noise, so Banach's theorem does not apply. The one-step concentration must hold at a random threshold that depends on all earlier cohorts, so it has to be uniform in . That is why is an infimum over all of . Proving then needs control of the quantile as , which is the content of Lemmas 29 and 32. The natural route of stochastic domination by a fixed random variable, taken in the printed Lemmas 33–34, fails because is bounded by and cannot grow linearly in .
Covariates are EuclideanSpace ℝ (Fin d), and is assumed to lie on the unit sphere in every statement. Agent types form a finite type ι with positive weights summing to . The class of costs and the outcomes are not modelled, since no statement here uses them. Formula (2.2) is the definition of the expected utility; a verification file proves that it is the expectation over the noise for unit . Quantiles are lower quantiles . The noise law is multivariateGaussian 0 (σ² • 1), and Mathlib's gaussianReal takes the variance . StrongConvexOn univ α has the paper's modulus.
The process takes fresh cohorts that are independent over all , each of law . The initial threshold is a real number. The goal holds for every Lipschitz constant , and it also asserts that the fixed point and some such exist, which rules out a vacuous reading in which no or satisfies the hypotheses.
A complete development needs the implicit function theorem on the sphere, Hoeffding's inequality for indicators, the Gaussian distribution function's smoothness and strict monotonicity, and the law of a linear functional of a multivariate Gaussian. The quantile-concentration bound (Theorem 17) and the Gaussian facts are reusable beyond this mission. Contributions toward any milestone are welcome.
In cognitive radio networks, several radios share a set of frequency channels. Each radio picks a channel in every time slot. The quality of a channel is random and unknown, and two radios that pick the same channel interfere and transmit nothing. This is the multiplayer multi-armed bandit problem: players repeatedly choose among arms, an arm pays a random reward, and a collision (two or more players on the same arm) pays zero to everyone involved. The players do not communicate and run the same algorithm.
The distributed problem was introduced by Liu and Zhao (2010), who gave regret with depending on the instance and proved an lower bound; the dependence of on the parameters was improved by Anandkumar et al. (2011), Rosenski, Shamir, Szlak (2016), who introduced the "musical chairs" subroutine, and Besson, Kaufmann (2018). These works let a player observe whether she collided. Lugosi and Mehrabian (arXiv:1808.08416v2, to appear in Mathematics of Operations Research) study the harder weak feedback model, in which a player only sees her own reward. A zero reward then does not tell her whether the arm paid nothing or another player was on it. Their Theorem 1 is the first regret guarantee for this model.
Let players and arms play for rounds. On a probability space, is the reward of arm in round ; the reward vectors are i.i.d. over rounds, with means . Sort the means as and let
be the gap between the -th and the -th best arm.
In round player pulls arm . The collision indicator is if two distinct players pull arm , and the player receives
A policy is a single rule that every player runs: in round it maps the player's own history (her arms and rewards in earlier rounds) and a private uniform random seed to an arm. It may use , , , but not the collision indicators, other players' actions, the means, or the player's index. The regret is
the gap between the best assignment of players to arms and the means actually collected.
The paper's algorithm (Algorithm 1) has four phases per player, with : explore uniformly and estimate each mean by the average reward divided by the no-collision probability until the estimated -th and -th means differ by ; explore uniformly for more rounds; pull uniformly random arms among the estimated best until a positive reward ("musical chairs"); then stay on that arm.
There is an absolute constant such that for all , , some policy satisfies, for every reward model,
The paper writes ; at that bound is , which no symmetric policy attains, so is replaced by , which changes nothing for .
Theorem 1 shows that collision information is not needed for logarithmic regret: the players can learn the best arms and share them using only their own rewards, at a cost of . Its dependence on matches the lower bound of Liu and Zhao, and it is at least as good as the bound of Rosenski et al., which uses collision information and knowledge of (p.6). The same paper uses the ideas for gap-free bounds (Theorem 2) and for reaching approximate Nash equilibria of stochastic anti-coordination games (Theorem 3).
The theorem is proved in the paper; nothing in this mission is open mathematics. As far as is known, no part of it has a machine-checked proof. The mission produces a formal model of decentralized play in which the information available to each player is enforced by types, a formal multiplayer bandit regret, and checked versions of the concentration arguments behind explore-then-commit strategies under collisions.
The obvious argument treats each player as running a single-player explore-then-commit algorithm. It fails because the other players change the collision probability: an estimate is unbiased only while all other players explore uniformly, and the phases of different players are not synchronized. Lemma 6 needs a coupling argument showing that, on the good event, every player finishes Phase 1 while every other player is still in Phase 1 or 2. Lemma 5 needs Hoeffding's inequality conditional on a random number of pulls of an arm, and Lemma 7 a geometric bound for a process in which the set of free arms shrinks over time. In Lean, the play itself is a recursion over rounds in which each player's action depends on her past rewards, which depend on everybody's past actions; measurability of the resulting regret has to be established before its expectation means anything.
Rounds are 0-based (paper round is Lean round ), arms are Fin K, players Fin m. The reward model (GameModel) asks for measurable rewards in , reward vectors i.i.d. over rounds (arms may be dependent within a round), seeds i.i.d. uniform on , and rewards independent of seeds. A policy (Policy K) is a measurable map from (own history, own seed) to an arm, shared by all players; Algorithm 1 is the rule algorithm1. The means are never assumed sorted: and the benchmark come from Tuple.sort. The bound is multiplied by , so gives the paper's vacuous case rather than Lean's . Lemmas 6 and 7 are stated in the -round game: may be (Phase 1 not finished by ), and the round counts are capped at .
The goal cannot be met trivially: the constant is chosen before , the policy before the reward model, the policy class excludes collision feedback and player indices, and for every policy in the class the regret is a bounded random variable, so its expectation is not a junk value.
Needed infrastructure: Hoeffding and multiplicative Chernoff bounds in the strict form, the measurability of algorithm1, a conditioning argument for averages over a random number of pulls, and union bounds over players, arms and rounds. The concentration statements are reusable for other bandit missions. Proofs of the milestones, of measurability of Algorithm 1, and alternative arguments with better constants are welcome.
Online publishers sell display-ad impressions in two ways: by real-time auction, and by preferred deals, contracts that give a buyer first look at impressions at a fixed price. Google's Preferred Deals service (Google Ad Exchange) is the model: a buyer who joins a deal may buy an impression at the agreed price before it reaches the open auction, and is excluded from the auction. Kim, Mirrokni and Nazerzadeh (SSRN 2693037; Operations Research 2021, doi:10.1287/opre.2020.2087) study how a seller should design a sequence of such deals for several buyers. They show that finding the optimal sequence is NP-hard, and they give a greedy algorithm, Auction-Adjusted Greedy (AAG), with a constant-factor revenue guarantee and prices that decrease along the sequence, which matches how the platform allocates impressions (the highest fixed price first).
A preliminary version (Mirrokni and Nazerzadeh, Proceedings of WWW '17, pp.7–14, cited on p.5 of the paper) designed deal sequences without the price monotonicity; the algorithm formalized here is the paper's new one, built to have it.
There are buyers. Each impression carries a valuation vector , drawn independently for each impression, with
where is a common value component and is buyer 's private signal, with a density vanishing outside . The components are nonnegative and jointly independent. Valuations are independent when and correlated otherwise.
A preferred deal offers a buyer first look at the impressions in at price per impression, with the obligation to buy at least a fraction of them, in expectation. A buyer who accepts buys every impression he values at least , and, if that is not enough, his highest-value impressions until the fraction is reached; he accepts when his expected utility is nonnegative. In a priority sequence of deals, buyer sees every impression, buyer sees those did not buy, and so on. The seller's revenue is the expected price paid per impression; is its supremum over all sequences of deals.
On a stream with buyer set , AAG puts aside the buyers who never have the highest valuation and gives them the empty deal. For each remaining buyer it takes the smallest threshold with , and the deal , . It serves a buyer of largest price first and recurses on the impressions with and the buyers . If one buyer remains, it sells him everything at his mean value.
Every run of AAG on the whole stream, with output , satisfies
and the prices along are non-increasing. A run exists. The statement covers every tie-break in the choice of .
In proof order: the cherry-picking inequality (3); the revenue of an AAG deal under the buyer behaviour; the benchmark ; the decomposition (9); the identity (10); ; Lemma 4, (and if ); the induction turning a per-level factor into the guarantee ; Lemma 6 (first-order stochastic dominance); Lemma 7; Claim 1, ; and Lemma 5, prices fall from one iteration to the next.
The result. Optimal deal design is NP-hard (Theorem 1 of the paper), and the natural recursion for the optimum takes exponential time. AAG runs in polynomial time with a constant fraction of the optimum, and its revenue is compared with , the welfare of efficient allocation and "the trivial upper bound on the optimal revenue" (p.12). Monotone prices are what makes a deal sequence implementable by "highest fixed price wins" allocation. The guarantee for general deals with a second-price auction (Theorem 3) uses Theorem 2 as a building block.
Formalizing it. The theorem is proved in the paper; nothing is machine-checked. The mission produces a model of priority-ordered contracts with best-responding buyers, where revenue is computed from the buyers' behaviour, not from the algorithm's own bookkeeping. It also produces a checked version of a proof that conditions repeatedly on events of a common value component. The formalization fixes two points of the printed text: Lemma 7 fails on an arbitrary set of impressions and is stated on the streams the algorithm visits, and a dropped factor in the p.25 induction chain is avoided.
The induction runs over the streams the algorithm creates: the original law conditioned on events in and in the signals of buyers already served. The step needs (10) and Lemma 7, which hold only because the signals of the remaining buyers are independent of those events. An induction over arbitrary impression sets fails: Lemma 7 has a counterexample there. Price monotonicity is a separate argument: conditioning on lowers the law of in stochastic dominance (Lemma 7, via Lemma 6), which lowers each remaining buyer's threshold (Claim 1) and price (Lemma 5). The comparison with needs the benchmark bound for arbitrary deals, including those whose purchase requirement binds.
Buyers are Fin n; the impressions are a probability space and a stream is a measurable set . Per-impression quantities on are set integrals and measures; most milestones are stated unnormalized, which is the paper's statement multiplied by a positive mass. The common value may have any law on ; the signals keep bounded positive densities. . The threshold is an infimum, and its attainment is a conclusion, not a definition. AAG is an inductive run relation covering every maximizer in (2). The revenue of a sequence is computed from boughtSet, the buyer's behaviour of §2 (purchase threshold with the top- quantile, acceptance at nonnegative expected utility). is the supremum over all admissible priority sequences.
A trivializing formalization would define the algorithm's revenue as along the recursion, or as . Neither is done here: both are computed from buyer behaviour, and the milestones bridge them.
The development needs conditional expectations on events, independence of the signals from residual events, the decomposition of by the maximizer, Chebyshev's association inequality, and first-order stochastic dominance (Lemma 6, reusable on its own). Proofs of any milestone, and of reusable lemmas about the deal semantics, are welcome.
Mediation is a dispute resolution method in which a neutral third party helps disputants reach a voluntary agreement short of litigation. Courts in all US states offer some form of it, and online platforms use automated mechanisms to resolve large numbers of small disputes (Kesten and Özyurt, 2018, p.2). A mediator who proposes an outcome from the parties' reports faces an incentive problem: each party knows privately where its walk-away point lies, and a rule that rewards exaggeration will not recover that information.
The classical cardinal treatment of bargaining starts from Myerson and Satterthwaite (1983), which shows that efficiency and incentive compatibility conflict in bilateral trade with private values, even in the Bayesian sense. Kesten and Özyurt take the ordinal route used in matching and assignment. The mediator elicits rankings only, and the question is which rules are strategy-proof in dominant strategies. This mission formalizes their characterization theorem.
Two negotiators settle two issues. The outcome sets are and with , where are the outside options. On each issue the negotiators' rankings of the alternatives are public and exactly opposed: negotiator 1 prefers smaller indices and negotiator 2 larger ones. The option is worst for both. The position of is private and is the negotiator's type. Row is the type of negotiator 1 that accepts , and column is the type of negotiator 2 that accepts .
A bundle is a pair . The logrolling bundles are
Preferences over bundles are not determined by a type. Each type has a set of consistent orderings: complete and transitive relations satisfying monotonicity in both issues, the deal-breakers condition (an unacceptable alternative in is never preferred to an acceptable one or to , for ), and logrolling (among acceptable alternatives, the worse one on with its partner on is ranked at least as high).
A mediation rule is a matrix of bundles. It is strategy-proof if truthful reporting is a best response at every ordering of , individually rational if it is weakly better than at every such ordering, and efficient if no bundle is unanimously at least as good at all orderings and strictly better for someone at some ordering.
For every , the rule is efficient, individually rational and strategy-proof if and only if there are one and one strict total order on with
and, for , with
The 'if' direction: richness of the consistent orderings, individual rationality and efficiency of adjacent rules, the value regions of Lemma 1, and strategy-proofness. The 'only if' direction: Parts i and ii, Lemma 2 (the row order on the diagonals), Lemma 3 (adjacency), Lemmas 4 and 6 on the constructed relation , Lemma 5 (where a beaten bundle can appear), and the extension of to a strict total order satisfying clause (iii).
The result describes every dominant-strategy mediation rule in this model: such a rule is a fixed priority over the logrolling bundles, applied to the mutually acceptable ones. It is what makes the paper's next results possible, since Theorem 2 (p.19) selects the rank-variance minimizer inside this class. It also shows that the impossibility of the single-issue case (pp.8–9) disappears with a second issue whose outside option is public.
Theorem 1 is a published result with a paper proof, and no machine-checked proof is known to exist. The platform has Gibbard–Satterthwaite and Myerson–Satterthwaite, both negative results, but no positive characterization of this type. A formal proof adds three things: a corrected statement, repaired gaps in the proof, and a reusable treatment of preferences given as a set of admissible orderings. Clause (i) as printed is false in the 'if' direction, and the mission states the form the proof establishes.
Efficiency and strategy-proofness quantify over all consistent orderings, so every excluded deviation needs a fact about the whole set : what holds at every ordering, and what fails at some ordering. The obvious argument compares bundles componentwise, and that step fails: the unanimous order has three kinds of edges, and comparisons that pass through logrolling chains are not componentwise. The second obstacle is global. Local comparisons on neighbouring cells define a relation on , but excluding 2-cycles and 3-cycles does not produce a linear order. Acyclicity must be shown for every .
Representation. Issues are Option (Fin m) with none the outside option, and a Fin m value is the paper's index minus one. Types are Fin m, so the type that accepts nothing is omitted, as on p.15. A rule is Fin m → Fin m → Bundle m, row first. The order is a relation on the subtype of .
Conventions. is the set of all consistent orderings, and a definition rather than a parameter: Theorem 1 is false for smaller maps, and the proof uses the full set. The logrolling map is the fixed for both negotiators. The value of clause (i) and the order are each quantified once, outside the cells.
Trivialization excluded. If were empty, every rule would be strategy-proof. It is non-empty and not a singleton for every , and the local verification file proves this, exhibits an adjacent rule, and exhibits rules that are not efficient or not strategy-proof.
Needed. The definitions layer is small and local. Solvers need the description of what holds at all consistent orderings (the richness milestone) and a linear extension step, which Mathlib's extend_partialOrder provides. The richness milestone and the handling of admissible sets of orderings are reusable beyond this mission. Direct proofs of milestones, and alternative routes to the acyclicity step, are welcome.
An online retailer choosing which low-demand products to display, and to stock in its urban warehouses, faces an unusual learning problem. Thousands of products must be chosen at once, the selection can change only a few times per season, and sales data arrive only for the products that were offered. Jin, Simchi-Levi, Wang, Wang and Yang (arXiv:1903.07844v2) model this as a stochastic linear semi-bandit in which the number of selections per period is large and the number of periods is small. Their study uses data from Alibaba Tmall.
The problem belongs to a line of work on linear bandits. Abbasi-Yadkori, Pál and Szepesvári (2011) gave the OFUL algorithm and its confidence ellipsoids for one action per period. Chu, Li, Reyzin and Schapire (2011) bounded the sum of confidence widths used in the analysis. Qin, Chen and Zhu (2014) and Wen, Kveton and Ashkan (2015) studied richer semi-bandit models, but their bounds carry terms such as , which are of little use when is large and is small.
There are products, each with a known feature vector , and an unknown parameter with , . Product has positive sales with probability . In each period the retailer offers a set of products and observes binary outcomes for , which are independent across products and periods. The regret against an optimal -set is
ConsUCB keeps the matrices and vectors of regularized least squares, with and , and the estimate . Within a period it selects products one at a time. The -th selection maximizes, over the products not yet selected, the score
where and for the selected product . The second radical shrinks after each selection, using features only: no outcome of the period is seen until all products are chosen.
For , , , , every instance, every optimal set and every tie-break depending on the observed history, ConsUCB with satisfies, with probability at least ,
This is the explicit bound printed at the end of the proof; it implies the theorem's .
In the order of the proof: the confidence event (4), the monotonicity of the widths, the inequalities (5)–(6), Proposition 1, the regret decomposition, the first line of the final display, the boundary terms, Lemma 2 with the correction , and the rewriting of the bound in form.
Theorem 3 splits the regret into a fixed cost , independent of , and a variable cost . The same paper shows that the standard upper confidence bound algorithm has fixed cost and at least . ConsUCB therefore improves the fixed cost by a factor of , which is what matters when is small, since the total reward over the season is of order . Since an regret in the first period cannot be avoided, the fixed cost is optimal up to a factor .
The result is proved in the paper; no machine-checked proof is known. The formalization adds a checked account of the within-period selection argument and a statement that makes the constants, the tie-breaking and the failure event explicit. It also records one defect: Lemma 2 as printed fails at , a gap in the proof of Theorem 3 that closes with one line, since there .
Within a period, selections must be made before any outcome of that period is seen. The obvious argument treats the period as one optimistic choice of products, all scored with . It then has to compare the width of a selected product under with its width after the earlier selections of the same period, and that comparison is what produces the fixed cost , which the paper's lower bound shows is not an artefact of a loose analysis in alone. Any improvement must change the algorithm, and the new score no longer equals the upper confidence bound: for it can fall below it, so the usual optimism step does not apply.
The probabilistic step has its own care: the confidence event must hold for a run in which the design vectors of a period are chosen sequentially, at horizon , including .
All declarations are in the namespace ShrinkingUCB, over Mathlib; the conventions below are binding.
Fin d → ℝ, norms are written , and Matrix.inv is the inverse (every dominates , so it is genuine). Logarithms are natural.Bool variables, with the algorithm reading only the offered entries. A tie-break is a deterministic function of the observed history, the selections so far in the period and the tied set. It cannot read an unobserved outcome; a rule that could would make the goal false, and restricting to one fixed rule would weaken it.A complete development needs a self-normalized bound along the observation sequence ordered within periods, a bound on the sum of unsquared widths, and the bookkeeping that the selections are distinct. Published tools such as ImprovedLinBandits.OFUL.confidence_ellipsoid and BanditAlgorithm.elliptical_potential_lemma are relevant but are not stated in this form. Contributions of the linear algebra of rank-one updates are reusable beyond this mission and welcome.
Charging every customer segment its own optimal prices is the most a seller can extract with a posted price per segment, and solving each segment's problem is often easy. Finding one optimal non-personalized price vector is harder, because aggregate demand may be much more complex than the segments' demands, so single-factor heuristics are used instead. A natural question is how much is lost.
For one product, Bergemann, Castro and Weintraub bound the ratio of personalized to uniform profit by two when each type's profit is concave and demand is positive on a common compact set; Malueg and Snyder bound it by the number of types under milder conditions; and Elmachtoub, Gupta and Hamilton give bounds in terms of summary statistics of the demand distribution. For several products, Berbeglia and Joret analyse uniform pricing in the special case of envy-free pricing. Gallego and Berbeglia state the first tight bound of this kind for general multi-product demand, against the personalized optimum rather than the non-personalized one.
A firm sells a finite nonempty set of products to customer types , distributed according to a probability measure . In the paper is finite with weights ; its remark on p.5 extends the result to continuous types. Write for the demand of type for product at the price vector . The type profit is and the aggregate profit is .
Let be an optimal price vector of type (Assumption A0: optimal prices exist and are positive and finite). The personalized profit is . Pricing along a positive vector earns ; is uniform pricing. For , the filtered demand is the -weighted demand at the personalized optima, keeping the pairs with , and . Assumption A1 is for all . Finally, and are the infimum and supremum of the ratios .
for every finite nonempty product set, every probability space of types, every positive and every selection of optimal prices, under A0 and A1, with and integrable demands.
For every there is an instance with one product, , , , and
For every and there is an instance with one product, , finitely many types, , , and .
All three are clauses of the goal theorem, SingleFactorPricing.LogBound.theorem_1. The milestones are the displayed steps of the paper's proof (the integral forms of the profits, the split at , the identity , the pointwise bound on ) and its tight instance.
Since , where is the optimal non-personalized profit, one inequality yields a guarantee for single-factor heuristics against non-personalized pricing and a bound on the value of personalization. The constant depends only on the spread of the optimal prices measured against , not on the number of products or types. For example, gives . The paper also gives sufficient conditions for A1 that hold in linear, multinomial logit and envy-free models, and uses the bound to compare linear with non-linear pricing.
The result is proved in the paper. This mission adds a machine-checked version: the bound over a general type space, where the paper only remarks that the proof carries over; both meanings of tightness, of which the paper states neither separately; and an explicit probability law for the instance. No formalization of this bound for general demand is known. The platform has narrower statements of the same shape: RevenueOrdered.UDPmin.uniform_pricing_log_ratio_bound for envy-free pricing and ValuePersPricing.Deviation.theorem_2 for one product.
The obvious comparison fails. Personalized optimal prices need not lie on a single ray , so no single can be compared with them, and A1 compares two sums at the same rather than two profits. The bound therefore has no term-by-term proof, and the factor is not visible from any one type.
Three points need care in Lean. Over a general type space, involves an exchange of integrals for functions that are only assumed integrable in the type. The second line of the printed chain contains , and nothing makes measurable. And "tight" cannot mean equality with finitely many types: when and , is a step function and equality is impossible, so the exact statement and the finite statement are independent, and the instance for each needs its own computation.
The type space is T with a probability measure μ, and demand is d : T → (N → ℝ) → N → ℝ with N a nonempty Fintype. Non-negativity and optimality are required for only. KallMayerSLP.ICC.discreteLaw θ id, a published finite law, recovers the paper's finite model, and regularity is then automatic. , and are fixed by IsGLB, IsLUB and IsLUB, so a real ⨆ is not used; need not be attained. The filter uses the paper's non-strict inequality. The optimality of stays in AssumptionA0 although the bound does not use it, so that is the personalized optimum and not the profit of arbitrary prices. There is no cost vector (footnote 1 of the paper).
Trivial tightness is excluded: the clauses assert , and LogBoundInstance fixes and as the true infimum and supremum of the ratios, not bounds on them.
A complete development needs integrals over the product of the type space and , the logarithmic integral, the moments and tail of the truncated law tailLaw, and an explicit family of finite instances for the last clause. The definitions are general enough to reuse for the other results of the paper. Proofs of the milestones and of the goal are welcome, as are the omitted results (Corollary 1, Proposition 1, Theorem 2), which would be separate statements.