Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A longstanding open problem in quantum information theory is to find the classical capacity of an optical communication link, modeled as a Gaussian bosonic channel. It has been conjectured that this capacity is achieved by a random coding of coherent states using an isotropic Gaussian distribution in phase space. We show that proving a Gaussian minimum entropy conjecture for a quantum-limited amplifier is actually sufficient to confirm this capacity conjecture, and we provide a strong argument towards this proof by exploiting a connection between quantum entanglement and majorization theory.
This mission is the statement-level formalization of Majorization theory approach to the Gaussian channel minimum entropy conjecture (arXiv:1111.1986v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Single-use reduction: C1 iff C2 iff C3; C4 is sufficient (C1–C4; Appendix 1, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
The long-standing conjectures of the optimality of Gaussian inputs for Gaussian channel and Gaussian additivity are solved for a broad class of covariant or contravariant Bosonic Gaussian channels (which includes in particular thermal, additive classical noise, and amplifier channels) restricting to the class of states with finite second moments. We show that the vacuum is the input state which minimizes the entropy at the output of such channels. This allows us to show also that the classical capacity of these channels (under the input energy constraint) is additive and is achieved by Gaussian encodings.
This mission is the statement-level formalization of A solution of the Gaussian optimizer conjecture (arXiv:1312.2251v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Main result: vacuum optimizer and unconditional Gaussian minimum-output additivity (Main result: vacuum optimizer and unconditional Gaussian minimum-output additivity, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need:
Optical channels, such as fibers or free-space links, are ubiquitous in today's telecommunication networks. They rely on the electromagnetic field associated with photons to carry information from one point to another in space. As a result, a complete physical model of these channels must necessarily take quantum effects into account in order to determine their ultimate performances. Specifically, Gaussian photonic (or bosonic) quantum channels have been extensively studied over the past decades given their importance for practical purposes. In spite of this, a longstanding conjecture on the optimality of Gaussian encodings has yet prevented finding their communication capacity. Here, this conjecture is solved by proving that the vacuum state achieves the minimum output entropy of a generic Gaussian bosonic channel. This establishes the ultimate achievable bit rate under an energy constraint, as well as the long awaited proof that the single-letter classical capacity of these channels is additive. Beyond capacities, it also has broad consequences in quantum information sciences.
This mission is the statement-level formalization of Ultimate communication capacity of quantum optical channels by solving the Gaussian minimum-entropy conjecture (arXiv:1312.6225v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-energy Gaussian minimum output entropy (Eq. (2), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Online marketplaces (ride-sharing, delivery, freelance labour) set payments for their suppliers and want to know how a change in payment would change the platform's utility. The standard tool, a randomized A/B test, is biased in a marketplace: treated and control suppliers compete for the same demand, so a payment increase given to the treatment group draws business away from the control group. This interference violates the no-interference assumption of classical causal inference (Hudgens and Halloran, 2008), and it was documented on a large platform by Blake and Coey (2014). Global experimentation, changing the payment for everyone and comparing days, avoids interference but is slow and costly.
Wager and Xu (2021) propose local experimentation: give every supplier a small, symmetric, random payment perturbation, measure how participation responds to one's own perturbation, and correct for the equilibrium feedback using a model of how demand is matched to suppliers. The perturbations are symmetric, so they do not move the market equilibrium at first order. The paper shows that in a large market this recovers the gradient of the platform's equilibrium utility. This mission formalizes that result, Theorem 6 of the paper, together with the lemmas on which its proof rests.
Everything is conditional on a global state (weather, holidays), which is dropped from the notation. In the -th system there are potential suppliers and a random demand on with , and .
Matching. If suppliers are active and demand is , each active supplier serves on average units. is non-decreasing in , non-increasing in , and , where the error is bounded and , and is a regular allocation function: is smooth, concave, non-decreasing, , , .
Choice. Supplier has a private feature and is paid per unit served. Given its expected revenue , it becomes active () with probability , where each choice function is -valued, non-decreasing and twice differentiable with uniformly bounded second derivative.
Equilibrium. With independent of , let . Under a payment law , the equilibrium supply fraction solves the balance equation
At a fixed payment , . The mean-field supply solves , and the mean-field platform utility is
with the limiting revenue per unit of supply. The marginal response is , and is its pre-limit analogue.
The experiment. Payments are with independent signs . From , and the regression slope
form and
For with (), and perturbation sizes with ,
A platform can thus learn the payment sensitivity of its equilibrium utility from one period of data, with perturbations that vanish as the market grows. The gradient estimate is the input to the first-order payment-optimization scheme of §4.2 of the paper, and the decomposition of Lemma 4 separates the measurable marginal response from an interference correction that depends only on the matching function .
None of these results has been machine-checked. A complete formalization gives a verified mean-field limit for a fixed-point equilibrium with binomial supply, a binomial Stein-type identity (Proposition 10), and a consistency proof for a regression estimator under vanishing perturbations. The mission also records two corrections. The claim for in (A.7) is too strong as printed. Lemma 15 (Appendix B.3), used in Proposition 10's proof, omits a factor; Proposition 10 itself is not affected.
The obvious argument says that is a regression slope, so it converges by the law of large numbers. It does not apply directly, for two reasons. First, the are not sampled at the unperturbed equilibrium: the perturbation itself moves the equilibrium, and the experiment runs at . Showing that this shift is uniformly in (Proposition 11) needs the implicit-function structure of the balance equation and the symmetry of the perturbation. Second, the noise in has standard deviation of order , while its bias is of order . The rate restriction balances the two. Finally, the limit of is a derivative of an expectation over a binomial law in which the error term is multiplied by ; controlling it needs a Stein-type identity, not term-by-term convergence.
All objects live in the namespace EquilibriumExperiment.Gradient. A Market B holds the primitives for one global state; Market.Standing bundles Definition 5, Assumptions 1–2, the part of Assumption 3 that concerns , and the demand conditions (3.1)–(3.2). Conventions:
eLpNorm … 2 → 0.Ruled out: independent of the perturbation, an arbitrary random variable rather than the solution of (A.2), hypotheses on all of , or as a deriv of a non-differentiable function (Proposition 12 proves differentiability).
Not in this mission. Theorem 7 (the regret of the first-order method) is false as printed: with , , , , utilities and in two periods and , the left side of (4.6) at , equals ; step (A.10) drops a factor 2. Corollary 8, which rests on it, Theorem 9, Lemma 3 and (3.15), which concern the pre-limit utility, are also excluded. Lemma 15 is false as printed and is not an item.
Contributions are welcome at every milestone; the binomial Stein identity, the implicit-function argument for monotone fixed points and the triangular-array law of large numbers for the slope are reusable.
School districts, public housing authorities and refugee resettlement agencies allocate scarce items (school seats, apartments, slots) without prices. Most such systems are priority-based: each applicant receives a priority, possibly depending on observable characteristics such as neighborhood or sibling status, and a mechanism such as deferred acceptance (DA), serial dictatorship or top trading cycles turns priorities and reported preferences into an assignment. The planner's design question is which priorities and quotas to choose. Shi (SSRN 3425348; Management Science 2022, doi:10.1287/mnsc.2020.3925) reduces this question, in a large-market model, to a linear program over budget set probabilities: the probability that an applicant of each segment can choose from each menu of items. That reduction is only useful if the optimal menus can actually be produced by a familiar mechanism. Theorem 1 a) of the paper says that, under a mild regularity condition, DA can produce any feasible menu distribution, and DA with a single tie-breaker (DA-STB) can produce exactly the nested ones.
The continuum approach to DA follows Azevedo and Leshno (JPE 2016), who describe stable matchings in large markets by cutoff vectors, and Abdulkadiroğlu, Che and Yasuda (AEJ: Micro 2015) on expanding choice in school choice.
There are items and an outside option , with . A market has segments of agents with masses , capacities for the real items (the outside option is unlimited), and for each segment a probability distribution of utility vectors with pairwise distinct components (strict preferences). The choice probability is
A budget set probability matrix lists the probability that a segment- agent faces menu . The feasible set consists of those with , , when , and the capacity constraint for every .
In DA, each agent of segment draws a priority vector from a law , independently of his utilities. Given a cutoff vector , his budget set is and he receives his favourite item in it. The demand is . For quotas , the DA operator raises each just enough to bring down to , and the DA cutoff is its least fixed point in . A mechanism implements if for all and . In DA-STB, for a deterministic boost matrix and one tie-breaker per agent.
The market is regular if implies for all : adding items to a menu strictly lowers the chance that the outside option is chosen. A matrix is nested within segment if any two menus used with positive probability by the same segment are ordered by inclusion.
If is regular, then
The milestones are the steps of the paper's own proof, in attack order:
Theorem 1 a) is what makes the paper's optimization approach operational. Once a planner solves the linear program over , part i) guarantees a DA mechanism with explicit priorities and quotas that realizes the solution, so for regular markets nothing is lost by restricting attention to DA. Part ii) characterizes the DA-STB-implementable matrices, which is what lets the paper compare single tie-breaking with DA and identify when the simpler mechanism suffices. The remaining results of the paper (optimal assortments under multinomial and nested logit, the Boston school choice application) are built on this reduction.
The theorem is proved in the paper; nothing here is open. To the best of the drafting search, none of it is formalized: Prove2Me has finite two-sided matching and Gale–Shapley items, but no continuum matching market, no DA cutoff, and no budget set implementation result. Formalizing it provides a machine-checked large-market DA model (demand, cutoff operator, least fixed point) that other market design papers using the Azevedo–Leshno framework can reuse.
The obvious argument shows that the all-ones cutoff vector reproduces and is a fixed point of the DA operator. That does not finish the proof: the DA mechanism uses the least fixed point, and in general there are smaller ones. Example H.1 of the paper (p. 50) gives a non-regular market with a feasible, nested matrix that no DA mechanism implements under any priorities or quotas, so regularity cannot simply be dropped. The work is in showing that, under regularity, no fixed point strictly below can change the menu probabilities. This mixes order theory (Knaster–Tarski on a box), measure theory (product measures of utilities and priorities, continuity of the demand under an atomless tie-breaker) and a strict comparison of outside-option masses.
Items are Option (Fin n), with none the outside option; priorities and cutoffs are Fin n → ℝ; menus are Finset (Option (Fin n)), and sums over menus run over the whole power set of . The utility laws are probability measures on Option (Fin n) → ℝ, concentrated on injective vectors (strict preferences). Capacities are assumed nonnegative. Probabilities are real numbers obtained as toReal of finite measures. The demand is computed under the product measure , which encodes independence of priorities and preferences.
The DA operator merges the two branches of Algorithm 2 into a single infimum over , with added to the set so the operator maps to itself, as the paper asserts. The DA cutoff is characterized as the least element of the fixed points in . DA-implementability quantifies over a priority box with , probability laws supported in it, quotas , and the DA cutoff. DA-STB-implementability quantifies over boosts with , so priorities stay in the box.
Implementability is never stated as quantification over menus directly: that would be the random assortment mechanism, which implements every by definition and would make part i) trivial. The cutoff is never "some fixed point": the all-ones vector is a fixed point by construction, and only the least fixed point carries the content of the theorem.
Theorem 1 b) (TTC and serial dictatorship) is not part of this mission: the TTC cutoffs are imported from Leshno and Lo as a black box. Contributions are welcome on the measure-theoretic lemmas (continuity of the demand, the menu law under (H.1) and under single tie-breaking) and on the Knaster–Tarski step, which can use Mathlib's OrderHom.lfp on a complete lattice of boxes.
Machine-learned models of molecular energies and properties are trained on the output of quantum-chemistry calculations, and a common way to make them data-efficient is to build the physical symmetries of the problem into the architecture. When the input is not a point cloud but a set of matrices expressed in an atomic-orbital basis (Fock, density, overlap and Hamiltonian matrices from a cheap mean-field calculation), the relevant symmetry is the freedom to rotate the orbital basis of each atom independently: a rotation of the molecule, or any other unitary change of the local frames, changes every matrix element but not the physics.
Qiao, Christensen, Welborn, Manby, Anandkumar and Miller (arXiv:2105.14655v4, published in PNAS 2022) introduce UNiTE (Unitary N-body Tensor Equivariant network), the architecture behind OrbNet-Equi. They state as eq. (4), p. 3, that the network must satisfy for every isometric basis rotation , and prove this property in Appendix S2.6 (pp. 26–28) for a generalized version of the network: tensors of any order , complex scalars, and an arbitrary unitary change of basis on each atom. The empirical results of the paper (QM9, MD17, GMTKN55) rest on this design principle, but the mathematical content of the paper is the equivariance proof.
There are atoms . Atom carries a finite basis , and the concatenated basis is the set of pairs . An N-body tensor of order is a function of concatenated indices; its sub-tensor at collects the entries whose -th index lies in atom .
A group (the paper's ; in the experiments) acts through unitary representations , and each atom has a subgroup . An element with acts on tensors by the local action (S26):
The network's hidden features assign to each label of a unitary representation and each channel a vector ; acts by . Matching matrices relate the atomic basis to a basis adapted to the decomposition .
The UNiTE network (Methods 1.1; Appendix S2.5) consists of:
Under the hypotheses the paper's proof uses — compatibility (S35) of the matching matrices, the Clebsch–Gordan property (S33) of , equivariance (S32) of the diagonal reduction, invariance of the attention weights, and positivity of the EvNorm constants — for every , tensor and atom ,
The proof in S2.6 rests on three results of S2.4 and four labelled sub-proofs:
The theorem is what justifies feeding UNiTE features in arbitrary local frames: the predicted invariant quantities (energies) do not depend on the choice of atomic-orbital phases or orientations. The vector-valued outputs, such as dipole moments, then transform correctly. Without it, the model would have to learn the symmetry from data or from augmentation. The same argument applies to other architectures acting on matrices in local bases, for example models of Hamiltonian or density matrices.
The result is proved in the paper, with a proof written at the level of index manipulations. To our knowledge it has no machine-checked proof. Formalizing it pins down exactly which hypotheses each layer needs: (S35) on the matching matrices, the complex conjugate in (S36), the intertwining form of (S33), and invariance of the attention weights. It also yields a reusable library of statements about tensor-product and block-diagonal actions of unitary representations. Theorem S1 for an arbitrary group with a complete catalogue of irreducibles is a statement of independent interest: finite-dimensional unitary representations are completely reducible, which Mathlib does not yet provide outside finite groups.
No single step is deep; the difficulty is bookkeeping across dependent index types. The local action is block-diagonal over atoms, so cross-atom terms must be shown to vanish. Sub-tensor indices are dependent on the atom sequence . The block convolution's cancellation uses unitarity and the conjugate. The reverse matching layer needs the adjoint form of (S35), which uses that is a subgroup (closed under inverses). The point-wise block reindexes a double sum through a Kronecker product. The full network is a two-phase recursion whose attention weights depend on the current features, so the induction must carry the equivariance of every intermediate feature. Theorem S1 needs complete reducibility of a finite-dimensional unitary representation of an arbitrary group, together with the identification of each irreducible summand with a catalogue member.
A tempting shortcut, assuming each layer equivariant and composing, proves nothing about UNiTE: the content is that these specific layers are equivariant under these specific hypotheses.
All scalars are complex; the paper's real (orthogonal) case is the special case of real unitary matrices. is replaced by an abstract group ([Group K]), representations are homomorphisms K →* Matrix.unitaryGroup ι ℂ, and the catalogue of irreducibles of is a family with the hypothesis CatalogComplete (every irreducible unitary representation is equivalent to some ), the formal reading of the paper's "we have abstracted the labelling details … into the index L". The subgroups are S u : Subgroup K, and every hypothesis is assumed only for .
Committed conventions:
Σ u, ι u;Trivializing formalizations are ruled out. The layers are defined concretely, not replaced by maps assumed equivariant. The action is local, one unitary per atom, not one global unitary. The complex conjugate in (S36) is kept. Irreducibility of the catalogue and its completeness are both stated in Theorem S1 and the corollaries.
The development needs one definitions module (OrbNetEqui.Equivariance.Basic) and Mathlib's matrices, unitary groups, block-diagonal and Kronecker matrices. Contributions are welcome on every milestone; the building-block lemmas (block-diagonal and Kronecker actions of unitary matrices, unitary invariance of the regularized norm) and complete reducibility of finite-dimensional unitary representations are reusable beyond this mission.
A company that is about to launch a product often has several candidate versions of it (designs, packagings, feature bundles) and wants to know which one consumers like best. A common way to find out is to ask: show an arriving consumer a few versions and record which one they pick. Each such query costs time and money, and consumer answers are noisy, so the question is how to choose what to show, and when to stop asking, so that the most preferred version is found with a prescribed reliability using as few consumers as possible.
Y. Feng, R. Caldentey and C. T. Ryan, Robust Learning of Consumer Preferences (SSRN 3215614; Operations Research, doi:10.1287/opre.2021.2157), treat this as a sequential hypothesis test in the style of best-arm identification (Garivier and Kaufmann, 2016; Kaufmann, Cappé and Garivier, 2016). The difference from a bandit is in the feedback: an action is a set of versions, and an observation is a choice from that set drawn from an unknown choice model. The paper asks for a policy that is good not for one choice model but uniformly over a large nonparametric class of them, and shows that a simple likelihood-based policy achieves this.
There are versions, . A display set is a subset with ; is the collection of display sets. A preference gives, for each and , the probability that a consumer shown picks . A ranking is a permutation of , rank being the top.
For , the class of -separable preferences (Definition 1) consists of the with exactly for , , and a ranking such that within every display set, iff (for ), and moreover whenever . The goal is to identify the top-ranked version .
An admissible policy chooses, after each history , a distribution over display sets for the next consumer; it stops at a stopping time and selects . It is -accurate if for every it stops almost surely and ; a family is accurate if each is -accurate (Definition 2).
With and , Chernoff's information is
where is the set of preferences in with a different top-ranked version. The ordinal attraction (OA) preferences are , where is the rank of within .
The Myopic Tracking Policy (MTP, Algorithm 1) with threshold fits the OA ranking of maximum likelihood to the votes so far, stops when the generalized log-likelihood ratio against every OA ranking with a different top reaches , and otherwise shows the top- versions of the fitted ranking with probability , an explicit distribution given in (7).
There is a threshold such that
that is, for every choice of the initial display set the family is accurate and its worst-case rate is at most that of every accurate family. The goal states the shape of the result and does not fix the optimal value.
The theorem says that one fixed, computable policy is optimal against the hardest consumer population in a nonparametric class, without knowing the population. Its display rule is static and sparse: only the nested sets of top-ranked versions are ever shown. The value gives a closed-form benchmark for the number of consumers any reliable test must survey, and Proposition 2 shows it barely depends on . The lower bound (Theorem 1) is a change-of-measure argument that applies beyond this model, for example to identifying the top- versions or the full ranking.
The results are proved in the paper; none is formalized. A formalization would produce a reusable discrete framework for sequential testing with set-valued actions and categorical feedback (finite-history laws, stopping times, expected stopping times in ), a formal treatment of Chernoff-type max-min information over a choice-model class, and a machine-checked LP duality certificate for the optimal display distribution. It would also pin down the exact hypotheses: two printed statements need correction (see Formalization scope).
The class is infinite and nonparametric, so the usual best-arm identification arguments, which track an estimate of the true instance, do not apply directly: MTP only ever estimates within the OA family, even when the truth is not OA. The upper bound must show that the drift of MTP's log-likelihood process under an arbitrary is at least , which rests on the dominance structure of Lemmas 4–5 and on the optimality of the fixed distribution . The accuracy proof must control the error probability uniformly over with a threshold independent of and . Computing on OA preferences reduces to a linear program over all rankings with a different top, whose explicit primal and dual solutions require the identities of Lemmas 6–9.
Everything is finite or discrete and no measure theory is used. Versions are Fin K and rankings are Equiv.Perm (Fin K) with 0-based ranks (rank 0 is the top); the restricted rank stays 1-based. A preference is a function DS K → Fin K → ℝ. A policy is given by its display rule (a function of the history into ℝ≥0∞), a stopping predicate on histories, and a selection function; the law of a history is the explicit product , in , and , and all rates are in . Limits as are along 𝓝[>] 0. MTP's uniform tie-break enters as a mixture in the display rule; for stopping and selection do not depend on it.
Added hypotheses and readings, each disclosed in the items: (A-3) is required for only (as printed it is unsatisfiable at ); and ; ; (Algorithm 1's input); the initial display set is arbitrary. Theorem 1's first inequality is stated for , since it fails for close to . Theorem 6's final sentence (equality for OA preferences) is not formalized, since it fails for bounded thresholds. The constants of Lemma 10 and Theorem 7 are quantified after and before .
Trivializing formalizations are ruled out: Definition 1 is non-vacuous (an OA preference is shown to lie in ), the alternative sets require membership in , top-rankedness is tied to the (A-3) ranking, and the goal includes the accuracy of MTP. Without it, a tiny threshold would stop after one vote.
Not in scope: Theorem 2 (a different policy for finite classes), Propositions 1 and 3–7, Corollaries 2–3, and the numerical study. Contributions to any milestone are welcome. The finite-history probability layer and the lower-bound argument are reusable for other sequential identification problems.
Data marketplaces buy personal data from many individuals to estimate population statistics. Two features set such pricing apart from an ordinary procurement auction. First, each data owner has a private cost of sharing, so the buyer must design a menu of payments that elicits these costs truthfully. Second, data are correlated across people: an individual who refuses to share still loses privacy when similar people share. Liao, Su, Ziani, Wierman and Huang call the consequence the privacy paradox: privacy-conscious people may join a platform because abstaining does not protect them (arXiv:2105.14262, §1; published in Mathematics of Operations Research, 2024).
The paper asks how an analyst with a fixed budget should design such a mechanism when the goal is statistical: to estimate a population mean while trading off the bias caused by non-participants against the variance caused by sampling only some participants. The answer extends the optimal-auction framework of Myerson (Math. Oper. Res. 1981) and the data-procurement mechanisms of Roth and Schoenebeck (EC 2012) and Chen, Immorlica, Lucier, Syrgkanis and Ziani (EC 2018) to a setting with participation externalities and an adversarial correlation between data and costs.
Agents are split into groups . An agent in group has a cost drawn from a density on the support , with distribution function . At a fixed desired participation profile the privacy cost of a participant is with , a non-participant suffers , the gap is strictly increasing, and participants receive a benefit .
The analyst posts a menu: a selection probability and a payment for a reported cost . A participant with true cost who reports has expected utility
The menu is truthful if reporting maximizes this utility. An agent joins if some report gives utility at least , and the menu induces if the fraction of joining agents of group is for a threshold . The virtual cost is
For the statistical problem, Appendix C of the paper discretizes the costs and sorts all virtual costs of participants as , with cell probabilities summing to . Given agents, a budget , a constant collecting the participation terms, and a weight on the variance, the analyst chooses and an adversary chooses the data probabilities in the min-max program
subject to the budget , under the standing condition .
There are constants , , and a feasible, non-increasing allocation
such that for every feasible . The constants are left existential, as in the printed theorem; the case analysis that identifies them belongs to the milestones.
Theorem 1 is a participation-aware version of Myerson's characterization: it shows that the analyst loses nothing by restricting to monotone allocation rules with one explicit payment, and it pins down the payment that realizes a target participation rate. Theorem 2 then solves the analyst's worst-case bias–variance problem: the optimal selection probability is flat for cheap agents and decays like the inverse square root of the virtual cost for expensive ones. This shape explains when the mechanism can be strictly truthful (a strictly decreasing rule, Corollary 2, in the low-budget regime) and when only weak truthfulness is possible (a flat region, larger budgets).
The paper proves Theorem 2 for discrete costs and passes to continuous costs by letting the number of cells grow without bound, a step it asserts without proof. The mission formalizes the discrete theorem that Appendix C actually proves, together with both directions of Theorem 1. None of these results has a machine-checked proof yet.
The goal is a min-max statement about a program that is convex in the allocation and concave in the adversary's choice, with a coupled budget constraint. The natural first idea, to solve each player's first-order conditions and plug them into each other, does not by itself produce a solution: the analyst's best response clips at 1, the adversary's best response may be interior on some cells and at the boundary on others, and which cells are which depends on the budget. The paper resolves this by a case analysis on the ratio against the values of , with thresholds obtained from intermediate-value arguments, and each case requires its own multiplier and its own adversary strategy.
For Theorem 1 the obstacle is that the paper's envelope argument differentiates the allocation rule, while the theorem quantifies over all monotone rules, which need not be differentiable. The "only if" direction must be recovered from the convexity of the maximal utility as a function of the true cost.
All statements live in the namespace PrivacyParadox.Alloc and use one definitions file. The group layer fixes one desired profile, so , , and are functions of the cost or numbers; their dependence on participation rates and correlation strengths plays no role in Theorems 1–2. The discrete layer indexes cells by as the paper does, with real-valued data and Real.sqrt.
The formalization commits to the following conventions, each disclosed in the item it affects:
Two trivializing readings are excluded: the goal compares with every feasible allocation, so it is not the best-response property of Lemma 3, and it asserts the existence of rather than assuming an optimizer of the stated form.
A complete development needs elementary real analysis (interval integrals of monotone functions, Fubini on a triangle, the intermediate value theorem) and finite-dimensional convex optimization (first-order optimality for a concave quadratic on a box and for a separable convex program with one linear constraint). The latter two are reusable well beyond this mission. Proofs of milestones are welcome in any order. The continuous form of Theorem 2, Lemma 1 (the derivation of the objective from the Horvitz–Thompson estimator), Propositions 1–2 and Properties 1–4 are not part of the mission.
Many estimation problems in statistics, signal processing and machine learning ask for a low-rank positive semidefinite matrix: phase retrieval, matrix sensing, PCA-type problems and the Burer–Monteiro approach to semidefinite programs. A standard formulation is
and Riemannian optimization solves it by treating the feasible set as a smooth manifold. Two geometries are in common use. In the embedded geometry the set of rank- PSD matrices is a submanifold of with the Euclidean metric. In the quotient geometry one writes with a full-column-rank factor and optimizes over equivalence classes . Algorithms built on the two geometries behave similarly in experiments, and landscape results (absence of spurious local minima, strict saddles) have been proved separately for each. Luo, Li and Zhang (arXiv:2110.12121, Mathematics of Operations Research 2024) explain this by an explicit dictionary between the Riemannian gradients and Hessians of the two geometries. This mission formalizes their first main result, Theorem 3, for the full-rank factorization of PSD matrices.
Matrices carry the Frobenius inner product . The objective is twice continuously differentiable and symmetric, (the paper's standing assumptions); and are its Euclidean gradient and Hessian.
Embedded geometry. , viewed as . Its tangent space is the span of the tangent cone. The Riemannian gradient is the orthogonal projection of onto , and the Riemannian Hessian quadratic form is the derivative at along any curve in with , .
Quotient geometry. The total space is , the matrices of full column rank, with the objective (18a). A weight , smooth and symmetric positive definite, defines the metric . The vertical space is tangent to the orbit , and the horizontal space is its -orthogonal complement. Tangent vectors of the quotient are represented by horizontal vectors: is the horizontal part of the total-space gradient , and for horizontal , where is the Levi-Civita connection of (Koszul formula).
Comparison data. ; spans the top eigenspace of , , . For a quadratic form on a -dimensional space with inner product , is its -th largest eigenvalue relative to (). are the extreme singular values of an matrix.
If in addition for all orthogonal , then for every and ,
and if is a Riemannian first-order stationary point of (18a),
both Hessians have eigenvalues, and lies between and .
Theorem 3 says that at stationary points the two geometries see the same second-order landscape: the Hessians are congruent through , so their eigenvalues have the same signs and comparable magnitudes, with explicit factors depending on and the spectrum of . The paper derives from it (Corollary 1) that first-order stationary points, second-order stationary points and strict saddles correspond between the embedded and quotient formulations, so a landscape result proved in one geometry transfers to the other. The choice of weight (flat , right-invariant , or ) changes the comparison constants, which is how the paper relates the conditioning of the two approaches.
The result is proved in the paper; it is not formalized anywhere. A formal development adds machine-checked Riemannian gradients and Hessians on a concrete embedded submanifold and on a concrete quotient, a checked horizontal-space computation, and a reusable abstract sandwich theorem for max–min eigenvalues. Corollary 1 and the parallel results for the polar factorization and for general rank- matrices (Theorems 4–7) are natural follow-up missions on the same definitions.
The identities (19), (20) and (34) are matrix calculus once the geometric objects are pinned down; the difficulty is that the definitions are intrinsic. The embedded Hessian requires differentiating the tangent projection along the manifold, which produces the curvature term ; the obvious computation that ignores the moving tangent space gives the wrong Hessian. The quotient Hessian involves the derivative of the weight and needs the horizontal-space description of Lemma 4 to see that the projection in (5) can be dropped. Identifying of the tangent cone with the block form (14) needs an explicit chart of the rank- PSD set. The final sandwich requires a max–min (Courant–Fischer) argument relative to two different inner products, and the order of the bounds flips for negative eigenvalues.
EuclideanSpace ℝ (Fin a × Fin b) (Frobenius inner product) with matrix views toMat/ofMat. The weight takes values in in the same form so that is defined.ProjLikeRetr.Retractor.tangentSpace (span of the tangent cone) and ZORiem.RGD.rgrad (projected Euclidean gradient); "smooth embedded submanifold of dimension " is the published coordinate-slice predicate ProjLikeRetr.Retractor.IsSubmanifold k d, for every .Useful contributions include Mathlib-level lemmas on the tangent cone of the rank- PSD set, Courant–Fischer for a form relative to a non-standard inner product, and matrix-calculus lemmas for .
In bundle size pricing (BSP) a seller of many products offers a menu of bundles in which the price of a bundle depends only on its size, the number of items in it. Customers choose which items to put in a bundle and which size to buy. Season tickets for theatres and sports teams, cable-TV channel packages and streaming plans priced by the number of simultaneous devices are priced this way, and BSP is known to recover much of the profit of full mixed bundling with only a handful of prices (Chu, Leslie and Sorensen 2011).
Choosing the optimal size prices is hard. For given prices, the customer's value for the best bundle of size is a maximal partial sum of order statistics of the item valuations, and the seller's expected profit depends on the joint law of these sums across sizes. Even when that law is known, it is not known whether the resulting pricing problem is tractable.
Li, Sun and Teo (2021) replace the exact choice model by the cross moment model (CMM) of Mishra, Natarajan, Tao and Teo (2012): only the mean vector and the covariance matrix of the bundle valuations are specified, and choice probabilities are those of the extremal distribution, among all laws with these two moments, that maximizes the customer's expected surplus. Their main result (Theorem 2) is that the seller's profit, written as a function of the choice probabilities, is concave, so the pricing problem becomes a concave maximization over a simplex. This mission formalizes that result.
Let be the number of bundle sizes. Let be the mean valuation vector, the vector of bundle costs, and the covariance matrix of the bundle valuations (the outside option, with value , is excluded). Write for the all-ones vector. The simplex and its interior are
A point is a vector of choice probabilities: is the probability that the size- bundle is bought, and the probability of buying nothing.
For a positive semidefinite matrix , denotes its unique positive semidefinite square root, and means that is positive semidefinite. Define
where is the diagonal matrix with diagonal , and below is the vector of diagonal entries of . In the paper, Theorem 1 and Lemmas 1–2 show that for every is the CMM demand at exactly one price vector, namely with
Substituting this price into the profit gives the BSP-CMM profit of Problem (6):
The statement is uniform in , , and in the positive definite ; it fixes no constant.
Concavity of turns bundle size pricing under the cross moment model into a concave program over the simplex: a local maximizer is global, and the problem can be passed to a conic solver through the semidefinite representation of milestone 5. The paper uses this to price bundles directly from two moments of the valuation distribution, and notes that the same reduction approximately solves other bundle pricing problems once they are written as multidimensional pricing problems. Before this result it was known that CMM choice probabilities are computable by convex optimization (Ahipaşaoğlu, Li and Natarajan 2018), but not whether pricing under CMM is tractable.
The result is proved in the paper; it has no machine-checked proof. The mission produces a formal statement of Theorem 2 against the explicit function (6), and the chain of the paper's proof as separately provable milestones. Several of these are reusable beyond the paper: Loewner concavity of , Loewner concavity of the square root composed with it, and the Schur-complement description of a bordered linear matrix inequality over the reals.
The function is not a composition of standard concave functions: it contains the inverse square root of a matrix that depends quadratically on , inside both a diagonal extraction and a quadratic form. The scalar composition rules for concavity do not apply to matrix-valued maps, and the second derivative of has no usable closed form. What is needed is the operator monotonicity and operator concavity of the matrix square root on positive semidefinite matrices (Horn and Johnson 1990). Mathlib has the corresponding results only for elements of C⋆-algebras, through the continuous functional calculus; real symmetric matrices with the Loewner order are a separate instance whose square root, monotonicity and concavity must be connected to that theory or proved directly.
Everything is stated inside BSPConvex.CMM. Vectors are Fin m → ℝ and matrices Matrix (Fin m) (Fin m) ℝ; is named Sig. The objects , , , , , , (defined by the displayed formula), (written literally as (6)), and the bordered matrix are definitions in one file. is CFC.sqrt under open scoped MatrixOrder, and is (A - B).PosSemidef throughout. is (CFC.sqrt (T q))⁻¹, the matrix inverse.
The formalization departs from the page in three disclosed ways:
A formalization that defines through or so that concavity is definitional, or that states the theorem on a set where it is vacuous, does not count: is the literal expression (6), and is nonempty for every (it contains ).
Contributions welcome beyond the milestones: a real-matrix version of operator monotonicity and concavity of the square root, the Schur complement criterion for real block matrices with a positive definite block, and differentiability of on positive definite matrices.
A seller who offers products and sets one price vector for all customers must price for a heterogeneous population. The finite-mixture logit (FML) model describes such a population with a small number of segments. Each segment follows its own multinomial logit (MNL) demand, so this is the simplest heterogeneous extension of the MNL model. It is widely used in empirical demand estimation (Train, 2009). Pricing under it is harder than under a single MNL. The single-segment MNL revenue is not concave in prices (Hanson and Martin, 1996), but it becomes concave once it is written in market shares (Li and Huh, 2011). With two or more segments that change of variables fails, and the revenue can be multimodal (Li et al., 2019). Local search then gives no quality guarantee.
van de Geer and den Boer give an algorithm with a guarantee: for every it returns prices whose revenue is at least times the optimum. This mission formalizes that guarantee, Theorem 1 of the paper (published in Management Science, doi:10.1287/mnsc.2021.4272).
There are segments with shares , , and products . Segment values product at . The price sensitivity depends on the product but not on the segment. At prices , a segment- customer buys product , or nothing, with probability
and the expected revenue is .
All maximizers of lie in a box , where and adds to the largest single-segment revenue. The no-purchase vector is , and is the set of attainable no-purchase vectors. Fix and substitute . The best revenue among prices with is then the value of a concave program with linear constraints , where .
Algorithm 1, , searches the -dimensional set by branch and bound over boxes of sup-norm radius around centers , clipped to . It keeps a lower bound , an upper bound , and an incumbent . In each pass and for each box that meets , it solves a linear program . A map turns the solution into an attainable point in the box. The pass then evaluates , compares an upper bound with , and keeps or discards the box. Kept boxes are split into boxes of half the radius. The loop runs while .
For every , terminates after finitely many passes, and every maximizer of gives prices with
The goal is posed for every bounding rule with two properties, for some constant and all , :
It is also posed for every choice of LP solution and every visiting order of the boxes.
Theorem 1 is an approximation scheme for a non-concave revenue function. The search space has dimension , the number of segments, rather than , the number of products. The reduction behind it (Lemma 1, Equation (5) and Proposition 2) applies to any search over no-purchase probabilities, not only to branch and bound. Proposition 7 and Corollary 1 give an exact LP test for whether a box of no-purchase probabilities contains an attainable point.
The results are proved on paper. None of them has a machine-checked proof, and the platform has no FML model, no no-purchase reparameterization and no pricing branch and bound. A formal proof would also settle two printed defects found in planning. First, Proposition 4 (a Lipschitz bound used inside the paper's bounding rule ) is false as printed: it pairs a sup-norm gradient bound with a sup-norm displacement. Second, the printed constraints (15)–(16) of make Proposition 7 false for centers outside , and Algorithm 1 creates such centers. The mission states the corrected versions.
The obvious argument is the one in the paper: boxes that may contain a maximizer are never discarded, and the gap between the bounds shrinks with the radius. Writing it out runs into two problems.
Proposition 1 is the heaviest analytic milestone. It needs coercivity of in every direction, including negative prices, and a first-order argument for the box.
Segments and products are Fin m and Fin n, and vectors are functions on them. The norm on Fin m → ℝ is the sup norm, as on p. 17. The standing assumptions are , with (the page writes ), and . , and are real suprema, read only where their sets are nonempty and bounded. is an extended real, so line 2 sets it to , line 6 to , and follows extended-real arithmetic.
Algorithm 1 is a definition, not a hypothesis. One pass is a left fold over an enumeration of the finite set of centers. The run is an iterate of the pass, and the state after the first failed loop test is the output. The departures from the page are these:
The counterexample to Proposition 4 has : , , , and . The point then has , which exceeds . Propositions 3, 4, 5 and 8, Theorem 2 (running time) and the competition extension of §5 are not posed.
(U1) and (U2) together say exactly that is -Lipschitz on , and then satisfies both. The goal is therefore not vacuous. It cannot be trivialized either: it concerns the defined algorithm, with every line except the bounding rule kept, and its conclusion compares with a global maximum of over all of .
A complete development needs elementary analysis of logit probabilities, concavity of , compactness on boxes, finite LP attainment, and an invariant proof for an iterated fold. The no-purchase reparameterization (Lemma 1, Equation (5), Proposition 2) is reusable for other FML pricing results. Proofs of the milestones, a Lean proof that is Lipschitz on (which makes (U2) concrete), and a corrected Proposition 4 are all welcome.
Schools, universities and public employers that run affirmative action decide whom to admit from a set of applicants who are ranked by a priority ordering (exam scores, lottery numbers, seniority) and who belong to a minority or a majority group. The procedures used in practice, such as the reserve and quota systems of Boston, Chicago and New York school choice, or the reservation system of India's public sector, are choice rules: functions from the set of applicants, their types and their priorities to the set of admitted students. Market design needs these rules to be substitutable (a chosen student stays chosen when other applicants withdraw), because substitutability is the condition under which centralized clearinghouses produce stable matchings (Hatfield and Milgrom, 2005; Hatfield and Kojima, 2008).
B. Doğan and K. Yıldız, Choice with Affirmative Action (SSRN 3626941; Management Science, doi:10.1287/mnsc.2022.4447), ask which affirmative action rules are substitutable and also respond monotonically to the minority students they are meant to help. Their Theorem 1 says that such rules are exactly reserve rules whose reserve number changes by at most one in response to a type or priority change. This mission formalizes the direction of Theorem 1 that the paper proves correctly: every such rule is a bounded reserve rule.
Fix a nonempty finite set of students and a capacity . A problem is a set of applicants, a type function ( minority, majority) and a strict priority ordering on . The rank of is one plus the number of students with higher priority. The top tier is the set of students of rank at most , the students a pure priority rule would admit; the bottom tier is . Superscripts and select minority and majority students: , , , .
A choice rule picks a subset of at most students. is the set of chosen minorities and the minorities chosen via affirmative action. The axioms are:
An affirmative action rule satisfies these three. Substitutability requires whenever and . MPI (monotonicity in priority improvements) requires that improving the priority of a chosen minority student does not reject any chosen minority student. MTC (monotonicity in type changes) requires that turning a chosen minority student into a majority student does not reject any other chosen minority student.
A reserve function gives each problem a number that depends only on the types of the students of ranks . admits a reserve representation via if chooses all of , then the highest-priority students of (all of them if fewer), then the highest-priority majority students until the seats are filled. The representation is bounded if satisfies Condition B: changing the type of a top-tier minority, improving a top-tier minority's rank, or worsening a top-tier majority's rank changes by or , and worsening the rank of a top-tier majority leaves unchanged when is among the lowest-ranked top-tier majorities.
Milestones 2 and 3 together give the goal, with .
The result describes every substitutable, monotone affirmative action rule by one integer per top-tier type configuration, constrained by local bounds. A designer who wants substitutability, so that the rule can be plugged into a deferred-acceptance clearinghouse, and wants monotonicity in the minority students' favour, therefore only has to choose a reserve schedule. The paper's lexicographic and stepwise-adjusted–reserves rules (§5) are built on this description.
Formalizing it has a second purpose. Theorem 1 is printed as an equivalence, but its (⇐) half is false. Take and the reserve when the top tier has at most one minority, otherwise. This satisfies B1–B3. With priorities and minorities , the rule chooses from but from , so removing the rejected student rejects , and substitutability fails. The same failure occurs in the paper's Example 1 (), and the error sits in Case 3 of the (⇐) proof on p. 23. The mission therefore poses only the (⇒) half, which planning checked by exhaustive search for every capacity and every universe of up to seven students. A machine-checked proof would settle that half for every and every universe. No formalization of this result, or of affirmative action choice rules in this model, exists on the platform or in Mathlib.
The reserve that represents has to be defined from alone. The obvious candidate, the number of affirmative-action admissions at the problem itself, is not a reserve function: it depends on how many minorities happen to sit in the bottom tier, while a reserve function may depend only on the top tier. Showing that a well-defined reserve exists already uses neutrality, substitutability and capacity-filling together (Lemma 1). The bounds of Condition B then compare reserves at problems whose top tiers differ. The monotonicity axioms give only the lower half of each bound, "the reserve does not fall"; the upper half, "the reserve rises by at most one", and the equality of B3 (ii) are not consequences of MPI or MTC and need substitutability. Small universes are a further obstacle: the paper's argument works with problems containing minority students and more than students, which a small does not contain, while the goal makes no assumption on .
Everything lives in the namespace AffirmativeChoice.Reserve, in one definitions file and seven theorems.
Problem holds S : Finset 𝒮, τ : 𝒮 → Bool (true = minority) and pri : 𝒮 → ℕ with s ≻ s' ↔ pri s < pri s', injective on S. Only values on S matter; restriction keeps τ and pri.rank ≤ q; the type of the k-th ranked student is an Option Bool, none beyond |S|.ChoiceRule 𝒮 q carries only C P ⊆ P.S, |C P| ≤ q and nonemptiness for nonempty S; the axioms are separate predicates.reserveChoice, with the majority cap .canonicalReserve, an sSup on ℕ over problems with the same top-tier type configuration. It agrees with the paper's whenever the paper's witness problem exists.Ruled out: problems encoded as type words, which quotients away neutrality; reserve functions defined only on type words; axioms built into the choice-rule structure; an existential that is not required to be a reserve function; or a reserve procedure that may admit bottom-tier majority students. Each of these would make the goal different from, or weaker than, the paper's. The (⇐) half and the full equivalence are not stated in any item.
Contributions welcome: the finite-order combinatorics of ranks, tiers and improvements, which is reusable for other priority-based choice models (reserves, quotas, slot-specific priorities); proofs of the milestones in any order; and a formal proof of the counterexample to the (⇐) half.
Sponsored-search platforms sell ad impressions through auctions in which advertisers submit both per-impression bids and a budget that caps their total spend. The platform then decides which auctions to run, subject to everybody's budget. Most auction theory treats budgets as exogenous constraints. In practice an advertiser chooses the budget, and committing capital has a cost, so budgets and bids are chosen together, strategically.
Ciocan and Iyer (SSRN 3240995; published in Operations Research, doi:10.1287/opre.2020.2052) study this joint choice. Exact equilibria of the resulting game are intractable: when budgets bind, the platform's allocation is the solution of a linear program, and an advertiser's best response depends on everybody else's budget in a complicated way. The paper shows that in large markets a simple, explicit strategy profile is an approximate equilibrium. This mission formalizes that result.
There are bidders and items . Bidder has private valuations , all independent, with . Committing a budget costs her , with . The platform earns an outside value per unit of an unallocated item.
A strategy maps to a budget and bids . Given bids , the price of item to bidder is the next lower bid,
The platform picks an allocation that is optimal for the linear program
Bidder 's spend is , her payoff is , and her modified profit is , the payoff she would get with a budget equal to her spend.
Write and , and assume . Let , let be the second highest on item , and let . The profile has bidder bid with budget
where averages over the other bidders' valuations. A profile is an -equilibrium if no bidder can raise her expected payoff above by a unilateral deviation.
There is a constant such that if and , then for every bidder and every deviation ,
so is an -equilibrium with .
The paper's own lemmas, in the order of its proof: the pathwise slack bound (Lemma 2), the dual-multiplier comparison (Lemma 4), greediness of the equilibrium allocation (Lemma 6), the key no-profitable-deviation lemma on a typical event (Lemma 3, corrected, see below), an order-statistic bound (Lemma 18), the probability of the typical event (Lemma 7), and the expected bounds on modified profit and spend (Lemmas 17, 15, 5, 16).
The theorem shows that a strategy which needs only each bidder's own distribution is an approximate equilibrium: shade each valuation by and declare a budget slightly above the expected unbudgeted spend. The error vanishes as the number of bidders grows, and Theorem 2 of the paper adds that the platform's optimal allocation under is then a per-item second-price auction with high probability. Together these justify analysing budgeted ad markets through a simple, decoupled model.
The result is proved in the paper but not machine-checked. Formalizing it means building an LP-based allocation model with measurable selections, order statistics of independent exponentials, and concentration bounds for sums over items. The formalization also records a correction: Lemma 3 as printed is false (see Formalization scope), and the corrected statement still yields Theorem 1.
The obvious route fails because a deviating bidder can change the allocation of every other bidder. If bidder overbids on an item that bidder would win, she raises 's price, and can run out of budget and leave other items for to buy cheaply. Underbidding creates a similar effect. So the deviation's effect on the market is not small, and mean-field arguments do not apply. The budgets have to absorb these effects on a typical event, while the expected cost of the unspent budget, , has to stay small next to the bidder's profit. Both requirements must hold uniformly over all deviations, including ones whose budget constraint binds, where the optimal allocation is not greedy.
The model is one Lean structure Market (sizes, rates , , the interval , ) with the standing assumptions of p. 18 in Market.Standing. Valuations are a function Fin m → Fin n → ℝ with the product law of independent exponentials. The conventions are:
No allocation rule is fixed by fiat, and none may ignore budgets: the rule must be LP-optimal for all nonnegative budgets, and the sanity check exhibits a market satisfying the standing assumptions, so the goal is neither vacuous nor provable by choosing a convenient allocation.
A complete development needs measurable selections of LP optima, LP duality and complementary slackness (both available on the platform as general theorems), order statistics of independent exponential variables, and a Bernstein-type concentration bound (available as HighDimProb.Concentration.bernstein_unweighted). The order-statistic and concentration layers are reusable beyond this mission. Contributions of the appendix lemmas (Lemmas 9, 23–26) as intermediate results are welcome.
A retail store manager does two kinds of work that the firm cannot observe directly: operational effort, which keeps shelves stocked, and marketing effort, which draws customers. The firm sees only the outcomes, namely how much inventory was available and how much was sold. Sales are the smaller of inventory and demand, so whenever the shelf runs empty the true demand is hidden. This is demand censoring, and it links the two tasks: a sales figure equal to the inventory level says little about how hard the manager worked on marketing.
T. Dai, R. Ke and C. T. Ryan (SSRN 3235866; Management Science, doi:10.1287/mnsc.2020.3651) study the principal–agent problem this creates, with a risk-neutral, limited-liability manager whose pay lies between and a cap . With the bang-bang approach of their §4, they show that an optimal plan pays either nothing or the full bonus , according to whether a weighted likelihood-ratio statistic of the observed pair (inventory, sales) clears a trigger . In the two-effort-level case, the bonus region has a distinctive mast-and-sail shape. Their §6 asks whether such a plan is monotone, meaning that more inventory or more sales never lowers the pay. A non-monotone plan invites ex post moral hazard: the manager would gain by discarding stock. The goal of this mission is the paper's answer, Proposition 5.
Inventory takes values in and demand in , with . Under low and high operational effort, inventory has densities and ; under low and high marketing effort, demand has densities and , with distribution function . Inventory and demand are independent. Each density is continuous, strictly positive on its closed support, and integrates to there. The monotone likelihood ratio property (MLRP) holds: is nonincreasing in , and is nonincreasing in .
Sales are . A compensation plan is defined on the domain . Points with are no-stockout (NSO) outcomes and points with are stockout (SO) outcomes. The firm wants both efforts high. For nonnegative weights summing to , one for each deviation, define
The plan (11) pays on the sail and on the mast , and pays elsewhere. The critical inventories are , the least with , and , the least with ; each equals when no such exists. The sail boundary is the least with .
A plan is monotone in (in ) if raising inventory (sales) within never lowers pay. It is jointly monotone if whenever both points lie in , and .
For every plan of the form (11) with :
By Proposition 3, part (ii) and part (iii) of the goal together cover every plan.
Proposition 5 shows that a mast-and-sail plan fails to be monotone in inventory exactly when the mast starts strictly below the sail. In that case a manager whose sales fall just short of the inventory level would gain by discarding the unsold units. The outcome then becomes a stockout on the mast, which earns the bonus, instead of a no-stockout point below the sail, which earns nothing. This ex post moral hazard is the paper's motivation for studying the cost of imposing monotonicity in its later sections. Propositions 1–3 describe the optimal plan's bonus region completely, and Lemma OA3 records the stochastic-order facts the analysis rests on: MLRP implies a hazard-rate ordering of the demand distributions.
The results are proved in the paper and its online appendix. No machine-checked version of any of them is known. The mission states them under the standing assumptions made explicit, about canonical thresholds rather than existential witnesses, and for every plan of the form (11) rather than only optimal ones. Under this reading Propositions 3 and 5 are slightly stronger than printed. Two printed claims need an added hypothesis to be true, and the mission states these honestly: the continuity of in Proposition 1, and the strict survival-versus-density inequality.
The goal's statement is elementary, but every step depends on joint properties of the two ratio functions on the whole domain. These are monotonicity of in both arguments, monotonicity of , continuity, and the comparison . The last of these is a hazard-rate statement about integrated tails, not a pointwise MLRP fact. The thresholds are infima of level sets, so each part of the goal requires showing that the infimum is attained, and handling the empty cases (an empty sail, an empty mast) where the thresholds default to . Joint monotonicity is strict in both coordinates, so it does not follow from the product order on .
All objects live in MastSail.Monotone. A model bundles , and the four densities as real functions, which are read only on or . Distribution functions are interval integrals from . Pairs are ordered (inventory, sales). The standing assumptions add two things to the printed model: strict positivity of the densities on the closed supports (from §4, p. 9) and (the paper has ). These ensure that every ratio has a positive denominator, so no ratio defaults to division by zero. The paper's "" is read as the least point with . The weights range over the three deviations from the target. Optimality of the plan is never assumed. Proposition 1 additionally takes strict MLRP of and ; Proposition 2 takes . The goal takes only .
The plan and the thresholds are the model's own definitions. A Proposition 5 stated for abstract regions shaped like a mast and a sail, or for thresholds supplied as hypotheses, would be set geometry and does not count. A complete development needs interval integrals, monotone level sets of continuous functions, and product measures with densities (for Lemma 1). The likelihood-ratio-to-hazard-rate comparison for densities on an interval can be reused well beyond this mission. Proofs of any milestone are welcome, as are proofs of the strict variants under weaker hypotheses.
Many sequential decision problems in operations research are learned online while the environment changes: demand responds to prices differently from week to week, click-through rates drift, and the value of an action in a recommendation or auto-loan pricing system decays as conditions move. The stochastic linear bandit is the standard model for such problems when actions are described by feature vectors. The classical algorithms for it (OFUL of Abbasi-Yadkori, Pál and Szepesvári, 2011) assume the unknown parameter is fixed, and they can incur linear regret when it drifts.
Besbes, Gur and Zeevi (2014, 2015) introduced the variation budget , a bound on the total movement of the environment over the horizon, and showed that the right benchmark is then the dynamic regret: the loss against the sequence of per-round optimal actions. Cheung, Simchi-Levi and Zhu, Hedging the Drift: Learning to Optimize under Non-Stationarity (arXiv:1903.01461v4, 2021; Management Science, doi:10.1287/mnsc.2021.4024), study the drifting linear bandit. Their SW-UCB algorithm attains the minimax rate when is known. Their Bandit-over-Bandit (BOB) algorithm needs no knowledge of : it hedges over window sizes with an adversarial bandit learner. This mission formalizes BOB's dynamic regret bound, Theorem 4 of the paper, together with the chain of results that leads to it.
A drifting linear bandit instance consists of a horizon , finite nonempty decision sets , and unknown parameters for , all fixed in advance. In round the learner picks and observes . The noises are i.i.d., centred and -sub-Gaussian: . The constants bound and , and . Assumption 1 asks that every action be a multiple of one vector of a fixed orthonormal basis. The variation constraint is
and the dynamic regret of a policy is with .
SW-UCB with window size and regularisation estimates by ridge regression on the last rounds only:
and plays with .
BOB cuts the horizon into blocks of rounds. Before each block an EXP3 learner draws an index , , and BOB restarts SW-UCB with window . The block's total reward, divided by and shifted by , is EXP3's feedback.
read as: for fixed there are such that the expected regret is at most times the bracket, for every , , , instance and noise.
Theorem 4 shows that a learner ignorant of how fast the environment drifts can still be no-regret against the moving optimum. When it matches, up to logarithmic factors, the rate of SW-UCB tuned with knowledge of , which matches the paper's minimax lower bound (Theorem 1) up to logarithmic factors. The bandit-over-bandit template, in which an adversarial bandit chooses among configurations of a base algorithm run on restarted blocks, is applied in the same paper to generalized linear and combinatorial semi-bandits, and by the same authors to non-stationary reinforcement learning.
The result is proved in the paper; nothing in this chain is machine-checked. The platform has an Exp3 regret bound and an elliptical-potential lemma, but no non-stationary bandit, no sliding-window estimator and no bandit-over-bandit result. A complete development would give a checked proof of the decomposition, of the per-block reduction to SW-UCB, and of the interaction between EXP3 and the high-probability normalisation, which the printed proof treats briefly.
The obvious argument for SW-UCB is to copy OFUL's analysis. It fails at the elliptical-potential step, because the sliding-window Gram matrices are not monotone in (old observations leave the window). Lemma 5 replaces it, and the drift bias of the estimator (Lemma 3) needs Assumption 1. Lemma 3 is false for actions in general position.
For BOB, the obvious idea is to treat each window size as an expert with bounded rewards. Block rewards are not bounded, though: they carry sub-Gaussian noise, and the normalised reward lies in only on a high-probability event (Lemma 1). EXP3's guarantee must be combined with that event. The restarts are also essential: without them a block's reward would depend on earlier EXP3 choices, and EXP3's adversary would no longer be oblivious.
Fin d → ℝ, matrices are Matrix (Fin d) (Fin d) ℝ, and rounds are numbered . The window of round for a run started at round is .A complete development needs:
The self-normalized bound, matrix-inverse monotonicity and the EXP3 bound are reusable well beyond this mission. Contributions to any milestone, and to these general lemmas, are welcome.
Retailers and platforms increasingly set prices and choose which products to display per customer, using observed customer attributes (location, device, purchase history). The decision rule is usually built in two steps: fit a choice model to historical transactions, then optimize prices and assortments as if the fitted model were the truth. Chen, Owen, Pixton and Simchi-Levi (Management Science, 2021; author manuscript SSRN 2579462) ask how much revenue this "estimate, then optimize" procedure loses, as a function of the amount and richness of the historical data. Their answer is a non-asymptotic, high-probability bound on the revenue gap for a feature-dependent multinomial logit model that covers personalized pricing and personalized assortment in one framework.
The estimation side builds on the econometrics of the conditional logit model (McFadden, 1974), whose classical theory is asymptotic. The finite-sample tools come from high-dimensional statistics: concentration of sample covariance matrices of sub-Gaussian vectors (Vershynin, 2012) and strong-convexity arguments for M-estimators.
There are products and a no-purchase option . A customer arrives with a feature vector , scaled so that . The seller offers an assortment and sets a price for each product, ; the price box is . For product the feature–price vector is .
The parameter is . The mean utility of product is . Under the multinomial logit (MNL) model the customer buys with probability
and buys nothing with probability . The expected revenue is .
The data are past transactions , where is the observed choice. The negative log-likelihood is . Given a radius with , the constrained MLE minimizes over .
Two assumptions govern the data. Assumption 1: the outcomes are conditionally independent given features and prices and follow the MNL model at the true parameter , and for each the vectors are independent across (not necessarily identically distributed) and sub-Gaussian with norm at most . Assumption 2: every product was offered in at least transactions, and the averaged second-moment matrix over the transactions offering has smallest eigenvalue at least .
Given a family of feasible assortments, maximizes over (the oracle decision) and maximizes .
For every there is , and for every a constant , such that whenever , with probability at least , for every feature vector ,
The constants are unspecified, as on the page; only their dependence is fixed.
The result. The theorem quantifies the value of historical data for personalized revenue management. The loss shrinks as and degrades with (products rarely offered in the past) and (features and prices that are nearly collinear in the data). This makes precise two practical warnings of the paper: price experimentation must not be correlated with customer features, and every product must have been explored. The bound is uniform over customers, so it is an out-of-sample guarantee. It specializes to customized pricing (Corollary 1) and to personalized assortment with fixed prices (Corollary 2), and the parameter rate of Theorem 1 matches the Cramér–Rao rate up to logarithmic factors.
Formalizing it. The paper's results are proved but none has been machine-checked. A formal development would produce a verified finite-sample theory of the constrained logit MLE: the softmax Hessian bound, strong convexity of the log-likelihood with high probability, the gradient concentration, and the transfer to revenue. Two printed statements need care, and the mission states the corrected forms: Lemma 2 needs an additional sample-size condition (see Formalization scope), and the printed (5) loses a factor relative to what Theorem 1 uses.
The deterministic parts (Lemma EC.1, the constant , the Lipschitz bound, the step (4)–(5)) are finite-dimensional calculus. The main obstacle is Lemma 2. Its proof needs the empirical second-moment matrices to be within of their expectations in operator norm, for independent but non-identically distributed sub-Gaussian vectors, with a sample size depending on only through a constant. The standard references state this for identically distributed vectors. Mathlib has no matrix concentration of this kind, and an -net argument with a Bernstein-type bound must be built. A second obstacle is the randomness of the decision itself: the optimal decisions are argmax selections, so the bad event is controlled through Theorem 1's event and not through measurability of the decision.
A first attempt often tries to bound the gap by the parameter error directly through the optimization problem. That fails: the argmax is not Lipschitz in . The paper's route compares revenues of fixed decisions, which needs the bound of Proposition 1 uniformly over all decisions.
The model is one definitions file in the namespace PersonalizedRM.RevenueGap. The parameter is EuclideanSpace ℝ (Fin J × Fin (d+1)), so ‖θ‖ is the Euclidean norm; is an explicit sum and is a bound on every fderiv partial derivative. Outcomes are Option (Fin J) (none is no purchase). Historical assortments are deterministic. The conventions committed to are:
Theorem 1, Proposition 1 and Theorem 2 are stated exactly as printed.
Constant order. The constants are quantified in the order , before , , , , and the data. A constant chosen after the data could be made large enough that the right-hand side exceeds the trivial bounds (revenue gap , parameter error ), and the statements would be empty.
Infrastructure. A complete development needs:
The concentration bound and the softmax Hessian bound are reusable beyond this mission. Contributions to any milestone are welcome, as are proofs of the generic lemmas as separate theorems.
Not formalized: Corollaries 1–2 (specializations of the goal), Proposition 2 (the mixing-data rate, stated only up to ), and the numerical study of §5.
In a contextual bandit, a decision maker repeatedly observes the features of an individual (a patient, a customer, a user), chooses one of several actions, and sees the reward of the chosen action only. Applications include personalized medicine, dynamic pricing and ad placement. The standard algorithms (upper-confidence-bound and Thompson-sampling methods, or forced-sampling schemes such as the OLS Bandit of Goldenshluger and Zeevi, 2013) deliberately explore: they sometimes take actions that look suboptimal in order to learn. In many of these applications exploration is costly or ethically constrained, and practitioners often run the greedy policy instead, which always takes the action that looks best under current estimates.
Bastani, Bayati and Khosravi (arXiv:1704.09011, Management Science 2021) ask when the greedy policy is nonetheless rate optimal. Their answer is a condition on the context distribution, covariate diversity, under which the natural randomness of the contexts does the exploring. For two arms they prove that the greedy algorithm then has logarithmic cumulative regret, which matches the lower bound of Goldenshluger and Zeevi (2013) for this problem.
There are two arms with unknown parameters . At times a context arrives; the contexts are i.i.d. with law . Pulling arm yields the reward , with independent mean-zero noise satisfying for all real (-sub-Gaussian).
The Greedy Bandit (Algorithm 1) keeps, for each arm, the set of times at which it was pulled, the sample covariance and the ordinary least squares estimate (and while is singular). At time it pulls , breaking ties with a fair coin . Its instantaneous expected regret and cumulative expected regret are
The assumptions are:
With and , for and every ,
The theorem shows that, under covariate diversity, exploration is unnecessary for the two-armed linear contextual bandit: the greedy policy achieves the optimal rate. It explains the good empirical performance of greedy policies reported in practice, and it underlies the paper's Greedy-First algorithm, which runs greedily and switches to exploration only when the data show that covariate diversity fails. The two concentration tools (Lemmas 8 and 9) are standard and reusable well beyond this paper; Lemma 5 is a reusable least-squares bound for adaptively collected data.
The result is proved in the paper. As far as is known, none of it is formalized: the mission produces a machine-checked proof of the regret bound with explicit constants, and of the adapted matrix Chernoff inequality, which is not in Mathlib. Note that the printed display (3) multiplies the constant term by , a factor the proof does not produce; the goal states the bound the proof establishes.
The samples of each arm are chosen by the algorithm from its own past estimates, so they are neither independent nor identically distributed, and classical least-squares consistency results do not apply. The obvious argument, "each arm is chosen with positive probability, hence is sampled linearly often, hence its estimate converges", fails at the second step: being sampled often does not make the sample covariance well conditioned, because the chosen contexts all lie in the half-space where that arm currently looks best. Covariate diversity is exactly what makes the conditional covariance of such a half-space well conditioned, and transferring this to the sample covariance requires a matrix concentration inequality for martingales. The regret bound then needs a peeling argument against the margin condition, with the constants tracked explicitly.
Fin d → ℝ; every norm is the Euclidean norm (Lean's default norm on this type is the sup norm and is not used). and are the infimum and supremum of over unit vectors.Fin 2; times start at . Contexts, noises and tie-breaking coins live on one probability space and are mutually independent; the context law is any probability measure (the paper's Lebesgue density is not used by the proof). Noise sub-Gaussianity is two-sided (Mathlib's HasSubgaussianMGF): the paper's one-sided Definition 1 does not force mean zero, and the theorem would be false without it.A buyer with a fixed budget wants to hire a team from a pool of sellers, each of whom knows privately what participating would cost them. The buyer values teams through a set function and pays each hired seller. The sellers are strategic: they report whatever cost serves them best. A budget-feasible mechanism decides whom to hire and what to pay so that reporting the true cost is optimal for every seller, nobody is paid less than their reported cost, and the total payment never exceeds the budget. The model was introduced by Singer (FOCS 2010). It describes crowdsourcing marketplaces that recruit workers under a fixed task budget, and influence-maximization campaigns that recruit seed users of a social network.
Budget feasibility is what separates the model from classical mechanism design. The truthful VCG mechanism pays far more than any fixed budget. The question is how much value is lost when the payment rule must be truthful and stay within the budget.
Timeline (as surveyed in arXiv:1905.00848v2, pp. 2–5):
For general non-monotone submodular valuations no budget-feasible -approximation mechanism was known before Amanatidis, Kleer and Schäfer (arXiv 2019; Mathematics of Operations Research, 2022). Their offline result is the subject of this mission. The obstacle is that the payments of Singer-style greedy mechanisms can be unbounded once is not monotone.
There is a finite set of agents. Agent has a private cost , where is the budget. The valuation is normalized (), non-negative and submodular: . It need not be monotone. The marginal value of with respect to is . The benchmark is
A deterministic mechanism consists of an outcome rule , which maps declared costs to a set of winners, and a payment rule. Throughout, payments are threshold payments: a winner is paid the largest bid with which it would still win, and a loser is paid nothing. A mechanism is truthful if declaring maximizes each agent's utility (payment minus cost if it wins, otherwise) whatever the others declare. It is individually rational if winners are paid at least their bids, and budget-feasible if the payments sum to at most . A randomized mechanism is universally truthful if it is a probability distribution over deterministic mechanisms that are all truthful.
Simultaneous Greedy grows two candidate solutions with separate budgets . It repeatedly takes the agent–solution pair of largest positive marginal value and offers the take-it-or-leave-it price . If accepts and the price fits into , it joins ; either way it is removed from the pool. The output is the best of and two unconstrained 2-approximate improvements . Sample-then-Greedy splits uniformly at random into , estimates with an -approximation for the knapsack problem on , and runs Simultaneous Greedy on with . GenSm-Main hires the single most valuable agent with probability and runs Sample-then-Greedy otherwise.
GenSm-Main is universally truthful, individually rational and budget-feasible, and for every cost vector the returned set satisfies
The goal is the paper's headline, stated about the mechanism as constructed. Every algorithmic ingredient (the greedy run, the posted prices, the sampling, the threshold payments, the expectation) is defined explicitly. The subroutines , and the tie-breaking rule are left general and enter only through the guarantees the paper uses.
In attack order: Definition 2.1 (three equivalent forms of submodularity); Lemma 2.4 (Myerson: monotone rules with threshold payments are truthful and individually rational); Lemma 3.3 (Simultaneous Greedy is monotone); Lemma 3.4 (Simultaneous Greedy is budget-feasible); Corollary 3.5 (the incentive half of the goal); Lemma 3.6 ( when no agent is worth ); Lemma 3.7 (a random halving keeps a fraction on both sides with probability ); Lemma 3.8 (Sample-then-Greedy's guarantee with probability ); Corollary 3.9 (the approximation half of the goal).
The result. Theorem 3.1 gave the first polynomial-time, constant-factor, budget-feasible mechanism for non-monotone submodular objectives. The posted-price structure of Simultaneous Greedy reduces budget feasibility to a bookkeeping argument and is reused in the paper's online mechanism (Section 4, the secretary model) and its extension to -system constraints (Section 5). Before it, constant-factor guarantees for non-monotone objectives were limited to special classes (cut functions, symmetric submodular functions).
Formalizing it. The result is proved on paper; nothing in it has been machine-checked. The mission produces a checked model of single-parameter procurement mechanisms with threshold payments, a checked form of Myerson's lemma in the procurement convention, and a checked analysis of a greedy algorithm whose two candidate solutions interact through a shared pool. The random-partition lemma (Lemma 3.7), which the paper cites without proof, has to be proved from scratch. The constant 505 is tight to the paper's own arithmetic: with and the chain of bounds gives .
Two steps resist the obvious argument. First, the threshold payment of a winner in Simultaneous Greedy has to be identified with the posted price it accepted. This requires showing that raising one's bid up to that price, or lowering it, changes nothing else in a run whose order of examination depends on marginal values only. Second, the approximation analysis of the case in which some agent is rejected for lack of budget (Lemma 3.6, Case 1) and the case in which every rejection is for price (Case 2) uses three different forms of submodularity together with the non-monotonicity of : adding agents can lower the value, so the usual greedy charging argument fails, and both candidate solutions are needed. Lemma 3.7 is a concentration statement for submodular functions under a uniform random split, cited from earlier work, and must be proved for non-monotone .
Agents form a finite type with decidable equality, sets are Finsets, and values and costs are real numbers (the paper uses ). Submodularity is the published lattice definition NonmonotoneSubmod.Shared.Submodular. The model commits to the following conventions:
Three hypotheses make the paper's implicit assumptions explicit. is deterministic, as in the printed proof (footnote 3 and Remark 3.10 explain that a randomized gives ). is cost-local: it reads only the costs of . The tie-breaking rule sees only the pool and the two partial solutions (Remark 2.6). Exact optimizers satisfy all three, so none is vacuous. The polynomial running time is not formalized.
A trivializing formalization is ruled out by the statement: the goal is about genSmMain as defined, with payments computed from its outcome rule, truthfulness against every misreport in , and the expectation over the explicit randomness. It is not the existence of some mechanism, and not truthfulness against a fixed bid.
Contributions welcome: proofs of Myerson's lemma and Lemma 3.7 are reusable beyond this mission, as is any general library of threshold-payment mechanisms. The online mechanism (Theorem 4.1), the -system result (Theorem 5.2) and the lower bounds of Section 6 are not part of this mission.
Retailers, online travel agencies and search engines display products in an ordered list or on a physical layout, and customers inspect only a prefix of it. Display optimization asks how to assign products to positions so as to maximize expected revenue when each customer considers only the products shown in the first positions, with random. Aouad and Segev (SSRN 2709652; Management Science 67(6), 2021) study this problem with vertically differentiated locations (every customer who sees position also sees positions ) and multinomial logit (MNL) choice within the consideration set. The model covers assortment planning over time and product framing on web pages, and it was calibrated on Expedia hotel-search data in the paper's case study.
The paper's headline claim (Theorem 1.1) is a polynomial-time approximation scheme, obtained by a dynamic program over approximate assortments followed by a rounding of its actions into an assignment. The rounding analysis, Section 5.2, contains a self-contained chain of combinatorial inequalities about the rounded assignment. That chain is the subject of this mission.
There are items. Item has a price and an MNL preference weight ; write and, for an assortment ,
the expected revenue of offering to an MNL customer with a no-purchase option of weight . An assignment is a bijection from positions to items; is the set of items in positions , , and with position weights the objective is
The algorithm fixes an accuracy and a guessed position . A sequence of dynamic-programming actions consists of events and pairs of item sets (a sub-assortment and a super-assortment), starting from , and ending at , . Consecutive actions must satisfy seven constraints, (8)–(14) of the paper: nestedness , the accuracy bounds and the same for , a cardinality constraint linking sets to events, and three growth conditions on the proxies
depending on the position of relative to . With the last index whose event is at most , the actions are rounded into blocks of new items (from before , from after), and the rounded assignment lists the blocks in order, each by non-increasing price. The block boundaries are , and are the position intervals between consecutive boundaries, split at .
For every , every feasible action sequence and every rounded assignment ,
with . This is inequality (15) of the paper combined with (16), in the proof of Lemma 5.4.
The goal is the step that converts the dynamic program's value into a revenue guarantee for an actual assignment: whatever action sequence the dynamic program returns, the assignment built from it earns at least times the interval-weighted minima of the program's proxies. Any repaired analysis of the scheme has to pass through a statement of this form, since the rounding of §4.4 is the only link between the program's actions and a display.
The remaining half of the paper's argument is not true as printed. Lemma 5.4, , and with it the approximation clause of Theorem 1.1, fail for the paper's own algorithm: with , , , and , no feasible action sequence can place item 2 first, and every rounded assignment earns at most against an optimum of . A formal proof of the true half isolates precisely where the published argument stops working. No part of this chain has a machine-checked proof.
The rounding discards items. Before , block keeps only the part of the sub-assortment that is new with respect to , so the prefix of can carry less -mass than . A loss bounded by the per-step accuracy would accumulate over up to steps; Lemma 5.2's constant is independent of , and holds only because the growth constraint forces to grow geometrically, which the obvious step-by-step bound does not use. The second obstacle is that the revenue between two block boundaries is not monotone; bounding it by the boundary values requires the unimodality of Claim 5.5, which depends on the price order inside each block and on the MNL convex-combination structure, not on the dynamic program.
Items are Fin n; positions and DP indices are 1-based natural numbers as on the page, and an assignment is an equivalence Fin n ≃ Fin n from the 0-based position to the item at position . A DP sequence stores events and set pairs as functions on ℕ, read through accessors implementing the root convention , and . Feasibility is exactly the boundary and root conditions plus (8)–(14), with (11) written without natural-number truncation and (14) in the lower-bound form printed on p. 19. The rounded assignment is a predicate: block contents fixed by , non-increasing prices within a block, ties in any order.
Conventions and additions relative to the page:
Feasibility and rounding are the page's constructions; neither predicate builds in Lemma 5.2, Lemma 5.3 or any revenue property, so the goal cannot be obtained by unfolding a hypothesis. A sorry-free sanity check exhibits an instance (, ) satisfying all hypotheses at once.
The development needs only finite sums over Finset, real arithmetic and induction over the block index. Contributions of all milestones are welcome; the identity and Claim 5.5 are reusable for any MNL ranking or display model.
Random utility models are the standard way to turn utilities into demand in operations management, marketing and economics. A consumer facing products assigns each a random utility and buys the one with the highest realization; the choice probabilities are the market shares that pricing and assortment models optimize. The multinomial logit, built on i.i.d. Gumbel errors, has closed-form choice probabilities, but its errors have the same variance for every product, and this forces the independence-of-irrelevant-alternatives property.
Alptekinoğlu and Semple (SSRN 3232788, forthcoming in Operations Research) replace the Gumbel errors by exponential errors with a product-specific rate. Uncertainty about a product's value can then differ across products, for example between a familiar brand and a new entrant. Their earlier exponomial choice model (Alptekinoğlu & Semple, Operations Research 64(1), 2016) is the special case of equal rates. The paper's first result is that this heteroscedastic model still has choice probabilities in closed form, a finite combination of exponentials of linear functions of the utilities. Its pricing analysis rests on that formula.
There are choices, . Choice gives the random utility
where is the ideal utility of choice and is an exponential random variable with error rate , with density and distribution function for (both for ). The errors are independent, and they are not identically distributed. Since , the ideal utility is the largest utility choice can ever deliver.
The choice probability of choice is
Write and for the choices that are better and strictly better than , and for the strictly worse ones. Let and . The exponomial term of choice is
The proof also uses the distinct values of , and the sets .
For every ,
The statement holds for arbitrary real utilities, ties included, and arbitrary positive rates.
The result. Theorem 1 makes the HEC model usable. Every later result of the paper starts from (3): the continuity and the partial derivatives of (Theorem 2), the expected consumer surplus (Theorem 3), log-concavity (Theorem 5), and the monopoly and oligopoly pricing results. Unlike the multinomial logit, the closed form shows how the rate of each worse product enters through , so substitution patterns are not proportional. With equal utilities it reduces to , and with equal rates it gives the exponomial model of 2016.
Formalizing it. The theorem is proved in the paper. The proof in Appendix C is short and leaves the integration steps to the reader. No machine-checked proof of the theorem or of any step of its proof is known. The mission asks for a complete Lean proof that starts from the probability itself, a product of exponential laws, so that the integral representation (1) is part of what is proved and not assumed. It also produces general facts about the maximum of independent shifted exponential variables, which have uses beyond this paper.
The obvious argument has two steps, and both hide work. Step one conditions on and integrates the product of survival functions. In Lean this is a computation of a product measure of a non-rectangular set, a Fubini argument over with the marginal of one coordinate split off. Step two integrates a function whose exponent is piecewise linear with breakpoints at the gaps . The breakpoints coincide when utilities tie, and the formula is stated through the distinct levels precisely to handle that. Regrouping the telescoping display (16) by level, and identifying each regrouped term with the strictly worse choices at that level, is bookkeeping over a sorted enumeration of a finite set. It is easy on paper and has to be done with care in Lean.
Choices are Fin n. The errors are the coordinates of a point of Fin n → ℝ under Measure.pi (fun j => expMeasure (lam j)), Mathlib's product of exponential laws. is the real value of this measure on the closed event , with the weak inequality as printed. All values are real. Every statement assumes and , the standing assumptions of p. 4. Integrals are Bochner integrals over . is defined for every , with value at a choice of maximal utility, where the paper leaves it undefined; the theorems use it only for , where it is at least . The levels are the increasing enumeration of the set of values of , indexed from in Lean.
is defined as a probability. It is neither the integral (1) nor the closed form (3), either of which would make the goal a computation or a tautology.
A complete development needs the product-measure computation behind (1) and the exponential integral . It also needs facts about sorted enumerations of finite sets of reals. The first two are reusable for any model with independent exponential errors. Proofs of the milestones in any order are welcome, as are alternative proofs of Theorem 1 that bypass them.
Not in scope: Corollary 1, Theorems 2–14 and the pricing results, which build on Theorem 1.
Large-scale learning problems, such as empirical risk minimization over millions of samples, are solved in practice by stochastic gradient descent (SGD) run on many processors at once. In a master–worker system, or in a multi-processor system with shared memory, a worker reads the current parameter, computes a stochastic gradient and writes its update back. Other workers update the parameter in the meantime, so by the time a gradient is applied it is stale: it was evaluated at an older iterate. In heterogeneous clusters these delays are not bounded in any useful sense, and they can grow with the run.
The classical analyses of asynchronous gradient methods (Bertsekas and Tsitsiklis, Parallel and Distributed Computation, Prentice Hall 1989, reprinted by Athena Scientific 1997) and of asynchronous SGD for machine learning (Agarwal and Duchi, NeurIPS 2011; Recht et al., Hogwild!, NeurIPS 2011; Lian et al., NeurIPS 2015) assume bounded delays. Zhou, Mertikopoulos, Bambos, Glynn and Ye (arXiv:2107.02919, Mathematics of Operations Research, 2022) show that the delays may grow without bound, polynomially in the iteration count, as long as the step size shrinks to match. This mission formalizes their first main result, Theorem 1, on general nonconvex objectives.
Let be a probability space and a random function. The objective is
to be minimized over . Write for the gradient of in .
Assumption 1 asks that be differentiable for -almost every , that the stochastic gradient have bounded second moment, , and that its mean be -Lipschitz.
Distributed asynchronous SGD (DASGD, Algorithm 3 of the paper) starts at and updates
where are step sizes, is an i.i.d. sequence with law , and is the iteration at which the gradient applied at step was requested. Its delay is .
Assumption 2 couples delays and step sizes. It requires one of four regimes:
If Assumptions 1 and 2 hold and , then
The goal covers all four regimes at once, through the disjunction in Assumption 2. It fixes no constant: , and the regime's parameters are arbitrary.
The result. For a general nonconvex smooth objective, convergence to a minimizer cannot be expected. The standard guarantee is that the gradient vanishes, and Theorem 1 gives it in mean square, which also implies convergence in probability of to zero. The theorem shows that asynchronous SGD stays stable under delays that grow without bound, and it identifies the price: each step up in delay growth costs a logarithmic factor in the step size. A step size of order is, up to a factor, sufficient for every polynomial delay process. The guarantee does not depend on whether the architecture is master–worker or shared-memory, since only enters.
Formalizing it. The paper proves the result, but no machine-checked version of any asynchronous or delayed SGD guarantee exists on Prove2Me or in Mathlib. A formal proof would check the step most prone to error in such analyses: the conditioning that makes a stale stochastic gradient unbiased given the past. The page's own chain before (B.5) has a constant slip ( where belongs), which the printed (B.5) absorbs. The delay-sum estimates (B.8)–(B.10) are asymptotic computations with logarithms, and the paper states them with "". The reusable parts are the differentiation-under-the-integral lemma (Remark 1) and the series lemma A.4.
Without delays, the descent inequality telescopes directly: the cross term has zero conditional mean. With delays, the gradient is unbiased for , not for . The discrepancy has to be paid for out of the step sizes accumulated over the delay window. When the window grows polynomially, it is a sum over polynomially many past steps, and finiteness of the total penalty depends on the precise step-size law. A cruder bound that ignores the logarithmic factors fails in regimes 3 and 4.
A second obstacle is that a finite weighted sum gives only a . The paper's own counterexamples (p. 10) show that it does not imply convergence. The increment bound of Lemma 2 is what closes the gap.
EuclideanSpace ℝ (Fin d), and is Mathlib's gradient. gradient returns at points of non-differentiability, so the goal also asserts that is differentiable.A Lean integral of a non-integrable function is , and gradient is where is not differentiable. Those conjuncts are there so that the goal cannot be proved through either junk value. The goal is also stated for all four regimes, with the delay inside the recursion, so it is not the classical bounded-delay theorem.
A complete development needs:
Contributions of the real-analysis milestones (Lemma A.4, the delay sums) are welcome independently of the probabilistic ones.
Many decision problems in operations research and machine learning ask to minimize an expected cost subject to constraints that also hold only in expectation: a portfolio with a bound on expected shortfall, a resource allocation whose expected load must stay below capacity, a classifier with an expected fairness constraint. The expectations are integrals over a distribution that can only be sampled, so the problem cannot be solved by evaluating it exactly. Stochastic approximation methods process one sample at a time and are judged by how fast their cumulative cost and cumulative constraint violation grow with the number of samples.
For constraints in expectation, the approach that has been analysed most is the primal–dual subgradient method with a drift-plus-penalty multiplier update (Yu, Neely and Wei, NeurIPS 2017, arXiv:1708.03741), which gives expected regret and constraint violation. Zhang, Zhang and Wu (arXiv:1907.12226v3, 2020) replace the gradient step by a proximal method of multipliers in the sense of Rockafellar (Math. Oper. Res. 1976): each iteration minimizes a sampled augmented Lagrangian plus a proximal term over the feasible set. They show that this method, PMMSopt, attains the same rates.
Let be a measurable space, a nonempty closed convex set and an open bounded convex set. Let and be jointly measurable, with and each continuous and convex on . For the law of a random sample , set and . The expectation-constrained problem (1.1) is
with feasible set .
The assumptions are as follows.
Write for the componentwise positive part of . The augmented Lagrangian at the sample is
PMMSopt starts from and . For it sets
The iterates depend only on .
Take and , with and . Then for every and every feasible ,
The constants are and , where is built from the explicit of (3.1). These are the two bounds of the paper's contribution (1). Each half is also a milestone on its own.
The milestones follow the paper's proof chain.
Pathwise lemmas. These hold on every sample path.
Probabilistic lemmas.
The bounds say that, with samples and step parameters tuned to , PMMSopt has average constraint violation and average objective regret against every feasible point, under assumptions that only bound the data and its subgradients. The constraint bound needs Slater's condition; the regret bound does not. The same chain of lemmas feeds the paper's high-probability results in §4, which this mission does not cover.
The paper proves these results; none of them had a machine-checked proof. Formalizing them also fixes several slips in the printed constants. As printed, Lemma 2.4's bound (2.7) is false: a one-step counterexample is recorded on the item. Corollary 2.1 inherits that error. The constant of Theorem 3.1 is not what its proof gives, both because of the inherited factor and because can exceed . The mission states the corrected versions under which the printed proofs go through. The drift lemma (Lemma 2.7) is quoted by the paper without proof, so formalizing it is self-contained new work. It applies to drift analysis well beyond this algorithm.
The pathwise lemmas are convex-analysis inequalities. Their main obstacle is that is not differentiable: the paper's proof of Lemma 2.3 writes , so the three-point inequality has to be derived from convexity and strong convexity alone.
The core difficulty is the expected multiplier bound. An obvious argument would iterate Lemma 2.1 and take expectations. That gives growing linearly in , hence a constraint bound of order rather than . The uniform bound on comes only from the negative drift in Lemma 2.6 combined with the drift lemma, which is an exponential-supermartingale argument in the style of Hajek. Lemma 2.6 itself needs conditional expectations with respect to the sample history, together with the independence of from . An off-by-one in the history σ-algebra breaks it.
and are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin p), so norms and inner products are Euclidean. The factors depend on this. is a general measurable space, and and are assumed jointly measurable. Samples are indexed from , and the history is hist ξ t, so the paper's is hist ξ (k+1). Expectations of sums are integrals of the sums.
The run is a predicate IsRun that carries the exact argmin over of Step 1, the exact multiplier update, and the measurability of in the history (asserted on p. 4). It is not a chosen argmin, and it is not an abstraction of the run by its drift properties: a hypothesis of that kind would make Theorem 3.1 a restatement of Lemma 2.7.
The formalization makes the following changes to the paper's statements, each disclosed on its item:
Every hypothesis set is satisfiable: a sorry-free check exhibits a one-dimensional instance with a PMMSopt run. Every statement requires , so the coefficient is never the junk value. The standing hypotheses make every integrand integrable, so no bound holds because an integral defaulted to .
The development needs conditional expectation, independence and filtrations from Mathlib, plus convex-analysis facts about proximal steps. The drift lemma and the three-point inequality are reusable beyond this mission. Contributions to any milestone are welcome, in any order.
A large language model serving a multi-turn conversation re-reads the whole conversation history at every turn. The intermediate attention state of that history, the KV cache, can be stored in GPU memory and reused, so that only the uncached part of the prompt must be recomputed before the first output token appears. GPU memory is scarce, so a server must decide, after every turn, which blocks of which conversations to keep. Production systems such as vLLM (Kwon et al., 2023) use least-recently-used (LRU) eviction for this (vLLM prefix caching).
Service-level objectives for LLM inference are written in terms of tail latency: the fraction of requests whose time-to-first-token exceeds a threshold. Zhang, Li, Moallemi and Peng (arXiv:2510.15152v1, 2025) measure this by the Tail Excess Latency (TEL) of a request: the number of uncached blocks above a threshold. They propose a variant of LRU aimed at the tail and prove that its expected version is optimal in a stochastic model of conversation arrivals. This mission formalizes that optimality theorem, Theorem 2 of the paper, together with the steps of its proof.
The cache holds blocks. A request of conversation whose history has length , whose new prompt has length and of which blocks are cached pays the Tail Excess Latency
where is the latency threshold expressed in blocks.
Conversations are born at rate and die at rate . While active, conversation sends requests as a Poisson process of rate . Each prompt length is drawn from a known, possibly conversation-specific law; each response length from an arbitrary law. Caches are not shared between conversations.
Deaths are never observed, so the decision-maker keeps a belief turn-arrival rate for each conversation. The belief state is : belief rates, conversation lengths and cached blocks of the conversations that have arrived so far. Between arrivals every is multiplied by the decay factor , where is the inter-arrival time. The next request comes from conversation with probability , or from a new conversation with probability . After serving conversation with prompt and response , its rate resets to , its length grows by , and the server chooses a new cache vector subject to
The belief update is the paper's: it decays the return rate with elapsed time and does not otherwise condition on the observed silence.
Expected-Tail-Optimized LRU (ET-LRU, Definition 1) chooses
the cache that minimizes the expected TEL of the next turn under the current beliefs.
For every ET-LRU policy (any tie-break), every policy whose decisions always satisfy (9), (10) and the capacity constraint, every number of requests and every well-formed belief state ,
Milestones 2 and 6 together give the goal.
ET-LRU is myopic: it looks one turn ahead. Theorem 2 says that in this model nothing is lost by myopia over any horizon. Setting with homogeneous rates turns (8) into "keep the blocks of the most recently active conversations", so the theorem yields an optimality statement for LRU for average latency. With deterministic prompt lengths it yields the optimality of the paper's Tail-Optimized LRU. With zero prompt and response lengths after the first turn it reduces to unit-page caching (p. 9), the setting in which Belady (1966) characterized the offline optimum. The paper reports that no such optimality result for LRU under stochastic arrivals had been established before.
The result is proved in the paper; nothing in it is machine-checked. A formalization adds a checked statement of the model (arrival law, belief dynamics, constraints and objective), whose conventions are easy to get wrong in prose, and a checked version of an exchange argument that the paper gives in compressed form. The greedy implementation (Lemma 1) is an instance of separable convex resource allocation and is reusable on its own.
The obvious argument compares ET-LRU's decision with another feasible decision and charges the difference to the next turn alone. That fails: a cache choice changes the state from which every later decision is made, and a cheaper next turn could in principle leave a worse state. The proof must show that the ranking of conversations by is consistent with the optimal cost-to-go at every later stage, under every possible next arrival, including arrivals that refill a conversation's cache and arrivals of new conversations. Ties in the ranking require care: two evictions of equal current score can have different future costs.
The invariant (a belief rate never exceeds the rate a conversation resets to) holds on every reachable state and is needed: exact dynamic-programming computations find states with from which ET-LRU is not optimal.
Everything lives in the namespace TailOptCaching.ETLRU, in one definitions file and eight theorem files.
ℝ≥0∞; is ENNReal.ofReal z; expectations over prompt and response lengths (laws PMF ℕ) are tsums, and the expectation over the decay factor is a lintegral. If a prompt-length law has infinite mean, every value is ; that is the correct reading, not a loophole.The goal must not be trivialized: the horizon is arbitrary (with the claim is the definition of ET-LRU), the competing policy is any admissible policy, not one of index type, the decay factor is not fixed to , and the Bellman optimum is defined independently of ET-LRU.
Not formalized here: Theorem 1 (the hindsight-optimal policy, App. A), the forced-caching variant (App. C) and the experiments. Contributions of proofs of any milestone are welcome. The finite-horizon Bellman machinery and the greedy allocation lemma are the parts most likely to be reused.
Many repeated interactions charge a player not only for what is played at each stage but also for changing what is played: a firm that reconfigures production, a defender that relocates patrols, a server that migrates jobs. Switching costs model this. In a zero-sum repeated game with switching costs, player 2 pays player 1 a stage payoff that depends on the current actions, plus a penalty proportional to a weight whenever player 2 changes action. A natural question is how the value of the game depends on : whether small changes in the cost weight can change the value or the optimal behavior abruptly, and whether an optimal strategy computed for one remains optimal for nearby .
Tsodikovich, Venel and Zseleva (MOR 2022) answer this for the undiscounted average payoff. Earlier work on such games (Liuzzi et al., Rass and Rainer, Schoenmakers et al.) studied static strategies, which repeat one mixed action forever; this mission concerns the value achieved by stationary strategies, which depend on the previous action of player 2.
Let be a real matrix, , and let be a real matrix with nonnegative entries and for every . Fix . At each stage player 1 (the maximizer) chooses a row and player 2 (the minimizer) chooses a column , and player 2 pays player 1
with . Both players observe the whole past history, in particular .
A behavior strategy assigns a mixed action to every finite history. Under a pair of behavior strategies the payoff is the lower limit of the expected average,
A stationary strategy (Definition 1) chooses its mixed action as a function of only, so it is a vector of mixed actions. The game has value in stationary strategies if there are stationary with for all behavior strategies . The game is a stochastic game whose state is the previous column; only player 2 controls the transitions.
The proof of the main theorem also uses a parametric one-shot game: for nonnegative and , is the one-shot zero-sum game with payoff matrix , and is its value.
For every the game has a value in stationary strategies. The function is continuous, increasing, concave, piecewise linear and eventually constant on , and if is linear on then player 2 has one strategy that is optimal for every in that interval:
As an illustration only (a numerical computation, not part of the mission), for and one finds , with a single breakpoint at .
The result. Theorem 1 describes the complete shape of the value as a function of the cost weight: no jumps, diminishing marginal effect of switching costs, finitely many regimes, and saturation at a level below the pure minimax of . The robustness clause says that, inside each linear regime, player 2 can play optimally without knowing exactly, and that optimal strategies need to change only at the finitely many breakpoints. The paper contrasts this with the value in static strategies (its Theorem 2), which is concave and increasing but in general only semialgebraic.
Formalizing it. The result is proved in the paper, but the proof leans on two cited theorems about single-controller stochastic games (Filar's existence theorem for the limiting-average criterion and the Filar–Raghavan matrix-game reduction). A formalization produces machine-checked versions of these classical results for the undiscounted, liminf-average criterion against arbitrary behavior strategies, and a general statement about parametric matrix games (Lemma 1) that is reusable outside this model. None of the statements has a machine-checked proof at present.
The obvious argument writes as a min-max of payoffs that are affine in and concludes concavity and piecewise linearity. This works for the one-shot game on pure stationary strategies, but transferring it to the repeated game is the hard step: the opponent may use any history-dependent behavior strategy, and the payoff is a lower limit of averages that need not converge. Showing that stationary strategies suffice against all behavior strategies, and that the value of the repeated game coincides with the value of the finite one-shot game, is the content of the single-controller theory. A second difficulty is the limiting behavior of the Markov chain induced by a stationary strategy of player 2, which need not be irreducible or aperiodic: its Cesàro averages converge, but the occupation frequencies depend on the initial column. Simply restricting both players to stationary strategies does not prove the theorem.
All objects are defined in SwitchCostGames.Stationary. Rows are Fin m, columns Fin n, with [NeZero m] [NeZero n]; the paper's is column 0. Stages are -based in Lean (stage s : Fin T is the paper's ). Strategies are behavior strategies on finite histories Fin t → Fin m × Fin n; the expectation over the first stages is a finite sum over histories, so no measure theory is needed. The payoff is Filter.liminf of the expected -stage average, which is a bounded sequence, so the liminf is a genuine limit inferior. The structure Game carries and ; the weight is a separate real argument and every statement assumes . Mixed actions and one-shot saddle values use the published finite zero-sum game BlottoLP.Flow.ZeroSum. "Increasing" is nondecreasing (MonotoneOn); "piecewise linear" means affine between finitely many breakpoints.
The value is a property of the repeated game: optimality is against all behavior strategies, not only stationary ones. Defining as the value of the one-shot game on pure stationary strategies, or restricting deviations to stationary strategies, would make the goal a corollary of Lemma 1 and is ruled out. The robust strategy in Theorem 1 is required to be stationary, which the paper's proof provides.
A complete development needs: von Neumann's minimax theorem for finite types, the theory of finite Markov chains (Cesàro limits of transition matrices), the reduction of a fixed-strategy problem to a one-player average-cost decision problem, and Filar's and Filar–Raghavan's single-controller theorems. The Markov-chain and single-controller layers are reusable for other average-payoff stochastic games. Contributions are welcome at every level, including proofs of Lemma 1 alone, which is independent of the repeated game.
The small-step subgradient method is the basic algorithm for minimizing a nonsmooth, nonconvex, locally Lipschitz function . It is also the scheme behind stochastic gradient training of neural networks with nonsmooth activations. From a starting point it iterates
with step sizes and . The basic question is whether a bounded run converges. For smooth , and for continuous-time subgradient flows, convergence follows from a Kurdyka–Łojasiewicz (KŁ) inequality together with tame geometry such as Whitney stratifiability (Bolte, Daniilidis, Lewis, Shiota 2007; Absil, Mahony, Andrews 2005). Whether the same hypotheses suffice for the discrete nonsmooth method was open.
R. Ríos-Zertuche (arXiv:2007.11699, published in Math. Oper. Res. 2022) is a companion to the work of Bolte, Pauwels and Ríos-Zertuche on the long-term dynamics of the subgradient method for path-differentiable functions (arXiv:2006.00098). That work proves positive results, such as slowdown near limit points and convergence of the values under the weak Sard condition. The examples paper shows that these results cannot be improved to convergence of the iterates. Its first example (Section 2) lives on and is the subject of this mission.
For a locally Lipschitz , the Clarke subdifferential is the convex envelope of all limits along sequences of points where is differentiable. The critical set is .
A subgradient sequence (Definition 1) is a sequence obeying the recursion above with positive steps , . The function is path-differentiable (Definition 2) if for every Lipschitz curve and almost every , for all . It satisfies the weak Sard condition (Definition 3) if it is constant on each connected component of . It is Whitney -stratifiable (Definition 5) if its graph in is a locally finite union of disjoint connected submanifolds. These pieces must satisfy the frontier condition and Whitney's condition A: limits of tangent spaces of a stratum contain the tangent spaces of the strata in its boundary.
The example works on . For let
and . Let be the distance to the unit circle . Let be a smooth radial bump with values in , equal to on , vanishing for and non-increasing along rays. Set and . For ,
There are , steps and a sequence such that is a bounded, non-convergent subgradient sequence of , and has all of the following properties:
This is the paper's negative answer to its question Q9, combined with its remarks in Q1 and Q12. The witness is left existential.
The milestones are the properties of the explicit witness (4):
The example is a counterexample: the standard toolbox of tame geometry plus a KŁ inequality does not give convergence of the discrete small-step subgradient method, even with a uniform gradient lower bound away from the critical set and the weak Sard condition. In continuous time the same hypotheses give convergence. The gap therefore comes from discretization. Any convergence proof for nonsmooth subgradient methods needs further structure, such as definability in an o-minimal structure or a stronger KŁ inequality near the critical set. Q12 adds that requiring the iterates to stay in the full-measure set of differentiability points does not help.
The result is proved in the paper; to our knowledge none of it is formalized. Formalizing it gives the first machine-checked Clarke-subdifferential, path-differentiability and Whitney-stratification counterexample. It also gives reusable estimates for an explicit sequence spiralling onto a circle.
Most of the steps are explicit estimates, but three of them are delicate.
Everything lives in EuclideanSpace ℝ (Fin n). The definitions follow these conventions:
ShorNonsmooth.AlmostDiff.almostGradients, which uses cluster points of the gradients rather than limits; the two sets are the same.ProjLikeRetr.Retractor.IsSubmanifold) for every . Tangent spaces are spans of tangent cones, and Grassmannian convergence is convergence of the subspace gap to .BumpProfile with exactly the properties listed on p. 6, and the series in (4) are tsums. The indices , where and in Lean, are never used.Four statements are adjusted, and each adjustment is disclosed in its item:
gradient is at non-differentiable points.The goal cannot be met trivially. Boundedness of the sequence and the conditions , are part of it, and they rule out an affine . Every regularity property is a separate conjunct. Contributions that develop the geometry of Whitney stratifications and path differentiability in Lean are reusable well beyond this example.