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?
Online platforms run randomized experiments on users who interact with each other. When the treatment of one user affects the outcome of another, comparing treated and control users is biased. A standard remedy is cluster-based randomization: users are grouped into clusters with few edges between them, and whole clusters are assigned to treatment or control (Ugander et al., KDD 2013). The price is variance: there are far fewer clusters than users, and clusters differ in size, so the Horvitz–Thompson estimator of the treatment effect can be very noisy.
Candogan, Chen and Niazadeh (SSRN 3852100; Management Science, 2024) observe that the experimenter controls more than the marginal treatment probability of each cluster: it also controls the correlation between the assignments of different clusters. Correlating assignments negatively, for example by treating exactly a fixed number of clusters, can reduce the variance. Since the potential outcomes are unknown, the paper designs the correlation against the worst case. This mission formalizes the paper's main asymptotic result: a simple family of designs, independent block randomization (IBR), is asymptotically as good as the best possible design whenever no single cluster dominates.
There are clusters. Cluster is assigned ( = treatment), and every cluster is treated with the same known probability . An experiment is a joint law of with for every ; the set of experiments is . Its correlation matrix is .
Each cluster has a size . Nature chooses a vector in the box , and the worst-case variance of a matrix is . Under the paper's Assumption 2.1, the variance of the Horvitz–Thompson estimator reduces to this quantity (Lemma 2.1). The robust correlation-design problem (1) is
Relaxing to an arbitrary correlation matrix (positive semidefinite, unit diagonal) gives the lower bound of (5).
An IBR experiment sorts the clusters by decreasing size, , cuts the sorted list into consecutive blocks, and on each block of clusters independently treats a uniformly random set of clusters with probability , and of clusters otherwise. The best IBR experiment is found by a dynamic program, the Bellman equation (4). Its worst-case variance is . For an integer , the -partition IBR experiment first groups the clusters into consecutive groups of and partitions each group optimally; its worst-case variance is . Finally, denotes for clusters of size one.
For every there is a constant such that for all sorted sizes with ,
and along every sequence of instances with , both this quotient tends to and . The constant is not fixed: only its dependence on alone is asserted, so an improved constant does not invalidate the goal.
In attack order:
The result. Problem (1) optimizes over all joint laws of binary variables, an exponentially large polytope, and its optimal design is unknown in general. Theorem 4.8 says that nothing is lost asymptotically by restricting to IBR designs, which are computable in polynomial time and easy to implement and explain. The rate quantifies the loss through a single statistic of the cluster sizes. Example 4.1 of the paper shows that the no-dominating-cluster condition cannot be dropped. Theorem 4.5 adds a finite- guarantee: for instance, a -approximation at , against a factor for independent assignment.
Formalizing it. The result is proved in the paper; none of it is machine-checked. A formal proof requires: the second-moment calculus of exchangeable Bernoulli laws behind Proposition 3.1; the identification of for equal sizes; the lower bound of Lemma 4.2, obtained through a randomized outcome vector; and the analysis chain of §4. The development also checks the paper's informal steps, such as "the worst case of a group grows with its sizes" in the proof of (13), and the proof of Lemma 4.7, whose displayed equality in Appendix B.7 holds only as an inequality (the lemma is unaffected).
The obvious argument compares with directly. It fails because has no closed form beyond equal sizes, so the comparison has to go through the relaxation , and the lower bound on must hold for every correlation matrix at once. A second obstacle is that the IBR worst case is a maximum of a quadratic over a box, and maxima do not add in general; additivity holds only because the blocks are independent. Finally, the asymptotic statement needs Proposition 3.1 with all its constants: the linear growth is what makes the bound vanish, and that growth needs the exact optimal value for equal clusters, not just a bound.
All objects are finite and real-valued; no measure theory is used. Clusters are Fin n, 0-based ( is w ⟨0, _⟩). Assignments are Fin n → Bool. A law is a nonnegative real weight function on assignments with total mass one and marginals . The worst case is a real sSup over the whole box (not only its vertices). and are real sInfs of nonempty sets bounded below by . Partitions into consecutive blocks are Mathlib's Composition n, and is the minimum over them. is the minimum over the compositions refining the -grouping, which equals the paper's construction because the IBR worst case is additive. is of unit clusters, not a closed formula. Every statement assumes and . The §4 statements also assume sizes sorted decreasingly (Remark 4.1) and , which excludes only the all-zero instance where every ratio is . Proposition 3.1 assumes , and wherever appears.
The statements rule out the trivializing formalizations. The constant is chosen after and before and , never per instance. ranges over consecutive blocks of the sorted clusters, not over arbitrary partitions. It is defined from the actual IBR law and its correlation matrix, not from a hand-written block matrix.
All definitions live in one file, CorrClusterExp.IBR.Setting. Reusable beyond this mission: the robust correlation-design problem, the exchangeable block law, and the IBR construction. Proofs of any milestone are welcome, as are Lemma 3.3 (the worst case of a block) and the high-multiplicity and logarithmic-partition results (Theorems 4.9, 4.10), which are not part of this mission.
In a generalized Nash equilibrium problem (GNEP) each player's feasible set depends on the strategies of the other players. Such coupled constraints arise wherever players share a resource: transmission capacity in electricity and telecommunication markets, emission caps in environmental games, track time in railway pricing, road capacity in transportation equilibria. The coupling is what makes GNEPs harder than ordinary Nash equilibrium problems (NEPs): an equilibrium solves a quasi-variational inequality rather than a variational inequality (Harker 1991; Pang–Fukushima 2005), and most existence theory and algorithms for NEPs do not apply directly.
Exact penalization removes the coupling. Each player's coupled constraints are moved into the objective as a residual function multiplied by a penalty parameter , leaving a NEP in which each player faces only a private strategy set. The question is when one finite , the same for all players, suffices for every equilibrium of the penalized NEP to be an equilibrium of the GNEP.
Timeline. Facchinei and Pang (2006) introduced exact penalty functions for GNEPs. Facchinei and Kanzow (SIAM J. Optim. 2010) and Facchinei and Lampariello (J. Global Optim. 2011) proved penalty results for inequality-constrained GNEPs under the extended Mangasarian–Fromovitz constraint qualification (EMFCQ), in full and partial penalization forms; Fukushima (2011) and Kanzow and Steck (2016) followed with related penalty and augmented Lagrangian schemes. All of these treat inequality constraints only. Ba and Pang (arXiv:1811.10674, Operations Research 2022) gave a theory covering shared and non-shared coupled constraints, including equality constraints, under a Slater-type condition instead of EMFCQ.
There are players. Player chooses from a private set , and denotes the rivals' strategies. Player minimizes a cost subject to and the coupled constraint . A profile lies in the graph of if for every . An equilibrium of the GNEP is a profile such that, for every , is feasible and minimizes over .
In the non-shared finitely representable case (16),
with convex and differentiable and affine. For the residual of player is
which vanishes exactly on the coupled set. The penalized NEP has player minimize over alone; its equilibria are profiles in from which no player can lower this penalized cost unilaterally.
Let each be compact and convex, each convex and Lipschitz on with a common constant , and . Suppose there is such that every outside the graph of admits and an infeasible player along whose block every violated constraint decreases at rate at least :
Then
The threshold is existential; no formula for is fixed.
The theorem converts a GNEP with non-shared coupled inequality and equality constraints into a standard NEP with one penalty parameter for all players. NEPs with private convex constraints admit the classical existence theory and the solution methods for variational inequalities, so the result transfers both to this class of GNEPs once feasibility of penalized equilibria is guaranteed. The hypothesis is required only at infeasible points of ; the paper's Proposition 12 shows that the commonly used EMFCQ implies it, so the theorem extends the EMFCQ-based penalty results while also allowing equality constraints.
The result is proved in the paper (pp. 17–18). As far as a search of the Prove2Me library shows, no part of it, of the residual calculus, or of GNEP penalization is formalized. A formal development would supply a reusable layer for GNEPs (equilibria with coupled constraints, residual functions, penalized NEPs) and the differential calculus of residuals, which also underlies exact penalty theory for single optimization problems.
The obvious argument penalizes each player's problem separately: for fixed rivals, a classical exact penalty theorem gives a threshold above which the penalized best response is feasible. That threshold depends on the rivals' strategies, and can degenerate when is empty for some rivals' profiles, which is allowed here; then no uniform follows. What is needed is control of the penalty terms that is uniform over all infeasible profiles in , which is exactly what the Slater-type hypothesis is about. Formally, the statement also involves the gradient of a nonsmooth-looking norm of positive parts and absolute values, valid only off the constraint set, and the comparison of and sums for , where the latter is not a norm.
Player 's space is EuclideanSpace ℝ (Fin (n ν)); a profile is a dependent function, and is Function.update x ν y. Strategy spaces, profiles and NEP equilibria are the published definition LeiBR.Sync.NashGame. The coupled multifunction is a family X ν x read as ; the GNEP equilibrium includes feasibility. The residual is written as an explicit sum of real powers, partial gradients applied to a direction are Fréchet derivatives in one player's block, and is Real.sign with . "For all " quantifies over profiles whose rival blocks lie in their private sets. The numbers of constraints may be zero.
The following formalizations would trivialize or change the goal and are excluded: penalized players also constrained by ; a GNEP equilibrium without feasibility; a chosen after the equilibrium; an that may depend on ; the hypothesis required at feasible points as well; an residual with the wrong exponent.
Objects defined: the GNEP and its equilibria, the graph of , -residual functions, the finitely representable sets (16), the residual (4)/(17), and the Slater-type condition of Theorem 11 (b). A complete development needs one-variable calculus of and , chain rules through Function.update, monotonicity of sums in , and directional derivatives of convex Lipschitz functions along segments; the last three are reusable well beyond this mission. Theorem 11 (a), existence of penalized equilibria, is not part of the mission. Proofs of any milestone, and alternative proofs of the goal, are welcome.
A seller who knows the distribution of a buyer's value can post the revenue-maximizing price. In practice the seller rarely knows ; often it has only a handful of past observations. Pricing with samples asks how much revenue such data can guarantee: the seller sees independent draws from , posts a price that depends on them, and is judged by the worst-case ratio of its expected revenue to the revenue of an oracle that knows . The question connects prior-independent mechanism design in computer science (Dhangwatnotai, Roughgarden and Yan, 2015; Huang, Mansour and Roughgarden, 2018) with data-driven pricing in operations research.
Without restrictions on no mechanism has a positive guarantee (Cole and Roughgarden, 2014), so the literature works with shape classes. Two are central: regular distributions, whose virtual value is non-decreasing, and monotone hazard rate (mhr) distributions, whose hazard rate is non-decreasing.
Timeline for one sample against mhr distributions.
A seller has one good and faces one buyer with value drawn from a distribution on . Write for the complementary cdf; posting price sells with probability and earns in expectation. The oracle revenue is
and an oracle price is a maximizer. The class contains every with ; then .
For , is -strongly regular if it has a density and its virtual value satisfies for in the support. With the -strongly regular members of , is the regular class and the mhr class. The generalized Pareto tails () and are the extreme members of .
With one sample , independent of , the mechanism posts the price . Its expected revenue is
For every ,
This is the mhr row of Table 3 (p. 27) and Table 4 (p. 29) of the paper; the abstract rounds it to "64%". It fixes the mechanism the paper reports and leaves the distribution arbitrary in .
The milestones are the lemmas of the paper's reduction that can be stated without its dynamic-programming objects:
The result pins down the value of a single sample against mhr demand: together with the paper's upper bound it places the best one-sample guarantee in . A deterministic deflation of the sample is near optimal, so randomization is worth at most 0.4 points against this class. The lower bound improves the previous 58.9% guarantee, and the same method extends to any and to several samples.
No part of the chain is machine-checked at present. A formalization would add to the platform a reusable model of α-strong regularity and of generalized Pareto tails, which also appear in auction and prophet-inequality work. It would also give the first machine-checked guarantee for sample-based pricing. The milestones are general facts about α-strongly regular laws that hold independently of the numerical goal.
The direct approach is a worst case over all mhr distributions. That is an infinite-dimensional problem, and it is not convex: a mixture of mhr laws need not be mhr. The paper reduces it to finitely many quantiles of (Lemmas 1–2, Propositions 2–4, Theorem 1). It then evaluates the remaining low-dimensional program numerically, with value iteration on a grid of step , iteration error below and adaptive quadrature at relative tolerance (Theorem D-11, App. D.6). The 64.4% figure is the output of that computation. A complete formal proof of the goal therefore needs either a certified evaluation of the finite program, for instance by interval arithmetic, or a different argument. Checking the inequality on a few families, such as exponentials or the paper's near-worst two-piece tails, does not prove it.
All declarations live in PricingSamples.OneSampleMHR.
The constant is the tables' 64.4%, reported as a provable bound for . A numerical search over two- and three-piece exponential-hazard laws finds a worst ratio of about 0.6472, consistent with the paper's bracket .
Not posed. The following are left out because their printed statements cannot be formalized without choosing between conflicting readings:
Contributions are welcome on any milestone. Lemma 2 and Lemma G-1 are general facts about log-concave and α-concave tails. Lemma 1 is a change of variables to quantile space. The App. A.1 bound is a classical mhr inequality. Each is reusable beyond this mission.
Online advertising platforms sell impressions through repeated auctions, and advertisers typically buy them under a budget: a cap on what they spend over a campaign. Because the advertisers cannot re-optimize their bids in every auction, the platform usually manages their budgets for them, adjusting how each advertiser participates so that spending tracks the budget. Platforms implement this in different ways, such as pacing bids down, raising personalized reserve prices, or entering a buyer only when his value clears a threshold, and the choice affects the platform's revenue, the advertisers' surplus and welfare.
Balseiro, Kim, Mahdian and Mirrokni (Budget Management Strategies in Repeated Auctions, Operations Research 2021; SSRN working paper 2858261, version of July 8, 2020) put these practices in one model and compare them at equilibrium. The comparison of the seller's profit is the paper's main theoretical result (§1.1). Among the strategies it covers, three are compared in this mission:
Bid shading is the strategy behind the multiplicative pacing equilibria of Conitzer et al. (2018 working paper; Operations Research 2022). The learning strategies of Balseiro and Gur (2019), which converge to a system equilibrium, are similar to it in spirit.
A seller has items to sell, one per round, to buyers, at an opportunity cost per item. In each round the buyers' values are drawn, independently across rounds, from a joint law with a continuous density that is positive on the box and zero outside it (, ), with . In the symmetric correlated setting is exchangeable (invariant under permuting the buyers) and all buyers have the same budget .
A budget management mechanism has one parameter per buyer. Its allocation rule and payment rule are given in Table 1 of the paper, with competing bid :
| mechanism | parameter | buyer wins if | and pays |
|---|---|---|---|
| bid shading (S) | |||
| reserve pricing (R) | |||
| thresholding (T) |
Buyer 's expected expenditure and utility over the horizon are and . The expected number of items sold is , and the seller's profit is
A profile is a system equilibrium (Definition 2.1) if every buyer's parameter maximizes his own utility over his parameter space, the others' parameters fixed, subject to his budget . For reserve pricing the parameter space is restricted by a lower bound , defined through the generalized failure rate , and the notion is a restricted system equilibrium (Definition A.1). Assumption 1 asks that be jointly continuous and that be strictly increasing in . A symmetric equilibrium is one of the form .
For every symmetric correlated instance, and with the symmetric (restricted) system equilibria of thresholding, bid shading and reserve pricing,
This is the paper's "Reserve Pricing Thresholding Bid Shading". Proposition 4.1 shows that each of these equilibria exists and is unique, so the comparison is well defined. The statement is quantified over every admissible choice of the parameter spaces' upper ends.
The theorem ranks three budget-management strategies a platform can deploy by the profit they yield, uniformly over all exchangeable value distributions (with the failure-rate condition for the reserve-pricing comparison). Reserve pricing extracts the most from a binding budget while selling the fewest items, which matters when items are costly. Bid shading comes last. The comparison holds at equilibrium, where each buyer's parameter is a best response under his budget. A mechanism-by-mechanism simulation cannot establish such a uniform ranking.
The result is proved in the paper, with the proofs in its electronic companion. No part of it has been formalized. A Lean development would provide a reusable model of budget-constrained repeated auctions with correlated values and of system equilibria. It would also give machine-checked proofs of the equilibrium characterization (Proposition 4.1) and of the dominance chain, whose proofs in the paper differentiate under the integral and rest on several unstated regularity conventions.
The comparison is between equilibria, not between mechanisms at a fixed parameter. The obvious idea is to compare the profit functions pointwise, but that fails: at the same parameter, thresholding and reserve pricing sell the same items at different prices, while bid shading's parameter lives on a different scale. What can be compared is how expenditure trades off against items sold along each mechanism's one-parameter family. That requires the equilibria to be characterized by a one-variable complementarity condition, which in turn needs strict monotonicity of the expenditure function in the common parameter, continuity, and the intermediate value theorem.
For reserve pricing the expenditure is not monotone on all of : it increases while the conditional generalized failure rate is below one. The parameter space is therefore a non-rectangular region cut out by . The case where reserve pricing's lower end exceeds needs an extrapolation argument rather than the sufficient condition used for the other pairs. With correlated values, every monotonicity statement goes through conditional laws of one buyer given the others.
Values live in Fin n → ℝ with the Lebesgue measure weighted by the density ; expectations are Bochner integrals. The instance (SymInstance) bundles:
Further conventions:
0;The generalized failure rate is written as , and reserve pricing's constraint as , as on p. ec 9. The lower ends of the parameter spaces are Table 1's (, , ). The upper ends are not fixed: every statement quantifies over all upper ends satisfying the conditions the paper's existence proof imposes (inside the support, budget met at the upper end). Bounded conditional expectations, which the paper uses only to construct such upper ends, are not assumed.
Two trivializations are ruled out:
Needed infrastructure:
The model and the monotonicity lemmas can be reused for the paper's utility and welfare comparisons (Theorems 4.3, 4.4). Contributions to any milestone are welcome; Proposition 4.1 and Lemmas B.2–B.3 can be attacked independently.
Firms that sell configurable products — computers, cable and phone packages, meal combos — decide not only how much to stock but also which bundles of components to offer and at what prices. Bundling decisions interact with inventory: offering a bundle draws on several items at once, and an overstocked item is a reason to push the bundles that use it. Song and Xue (SSRN 3168907, forthcoming in Operations Research, doi:10.1287/opre.2020.2062) build a multi-period model that optimizes procurement, assembly, bundle selection and pricing jointly. Its key modelling device is to use the market-share vector as the decision instead of prices: offering no bundle means , and prices are recovered from the shares. Under standard discrete-choice models the expected revenue is then concave in the shares, which makes the dynamic program tractable.
The single-item analogue, joint pricing and inventory control with an order-up-to (base-stock) list-price policy, goes back to Federgruen and Heching (1999) and Chen and Simchi-Levi (2004). With several items assembled into bundles the policy is no longer a plain base-stock policy, and the paper's main result describes what replaces it.
There are periods , items , potential bundles , a nonnegative bill of materials and a discount rate . In period the firm chooses a market-share vector , where is compact and convex. Bundle demand is
with the expected number of customers and a random vector with zero mean and finite variance, possibly correlated across bundles. The expected revenue is , and the revenue rate is concave on (Property-CV, Assumption 1).
Costs are row vectors: procurement , assembly , backorder and holding , with the postponement savings , and , and it is assumed that and .
Under bundle-to-stock (BTS) the firm, with net item inventory , orders items up to , schedules bundle production with , and sets , all before demand is observed. After a change of variables the problem is the dynamic program (9): and
with profit rate and expected inventory cost .
For a no-order set with complement , problem (14) maximizes over , , , .
For every period and inventory : (a) is jointly concave and non-increasing; (b) is jointly concave in and (14) with has a maximizer ; (c) if , ordering up to and producing is optimal, and otherwise there is a nonempty no-order set such that the solution of (14) for is optimal in (9):
Theorem 2 says that bundling, pricing and replenishment decisions are still governed by order-up-to levels, with one correction: items that are already overstocked form a no-order set, and once that set is known all remaining decisions, including which bundles to offer (), solve the single concave program (14). This is what makes the paper's branching algorithm for (Algorithm 1), its myopic policy and its numerical study of bundling under inventory pressure possible.
The paper omits the proof ("similar to that of Theorem 2 in Song and Xue (2007)", an unpublished working paper). A machine-checked proof therefore supplies an argument that is not in the published record. No part of the model is formalized elsewhere: there is no multi-item joint pricing–inventory dynamic program on the platform and none in Mathlib.
The concavity part is the classical backward induction, but every step needs analytic bookkeeping that the paper does not do: the value function must be shown finite (the supremum of over an unbounded feasible set), of linear growth, and therefore integrable against the demand distribution; the partial maximization of a jointly concave function over a jointly convex set must be shown concave. The no-order-set clause is the hard part. A first idea is to set ; this is wrong, because once some items are frozen at the optimal assembly plan, market shares and hence the remaining order-up-to levels change, and items can enter or leave the set. The no-order set depends on the whole optimal decision, not on and alone, and (14) drops the constraints on , so its maximizers are not obviously feasible in (9). The existence of maximizers requires coercivity of in the production vector , which in turn needs a bound on from above.
Items and bundles are finite types, vectors are real-valued functions with the coordinatewise order, and is the matrix–vector product. The randomness of period is a probability measure on , the law of , under which each coordinate is integrable with mean zero and square integrable. The value function is defined by backward recursion with for , and is the real supremum of over the feasible set of (9); proving that this supremum is finite is part of the work. The program (9) is the paper's transformed program (P), stated directly; the change of variables from the original model is not formalized.
Hypotheses added relative to the page, all implicit in the model: , , , , and . For the existence of maximizers and the no-order-set clause only, the goal also assumes coercivity: continuous on , and , where and (the fill rate of §5.2 lies in ). Problem (14) keeps the constraint , which the printed (14) omits but the text after Lemma 2 requires. Maximizers need not be unique, so "otherwise" in Theorem 2(c) means that no maximizer of (14) with covers .
The value function is the supremum over (9), not the value of (14) or a closed form, and the no-order set must come with the maximality in (14), the optimality in (9) and the attainment of ; a bare existence of some would be trivial.
A complete development needs: concavity of partial maximization over a convex constraint set, concavity and continuity of expectations of concave functions of affine maps of a random vector, and coercivity arguments for existence of maximizers on unbounded domains. These lemmas are reusable for any convex stochastic dynamic program, and contributions of them as separate theorems are welcome.
A monopolist selling to a large market of unit-demand consumers with a known demand curve cannot do better than posting a single price (Myerson 1981; Bulow and Roberts 1989). When the demand curve itself is uncertain, consumers' valuations are correlated through the aggregate state, and the picture changes. Crémer and McLean (1985, 1988) showed that with Bayesian incentive compatibility and only interim participation constraints, the seller can extract the entire surplus through side bets whose payments may far exceed a consumer's valuation. Such payments are not enforceable when a consumer can walk away from a deal that charges more than the good is worth to them.
Segal (2003) imposed ex post individual rationality together with ex post (dominant-strategy) incentive compatibility, and showed that as the number of buyers grows the optimal mechanism converges to state-by-state monopoly pricing: post, in each demand state, the monopoly price of that state's demand curve. Dominant-strategy incentive compatibility rules out most price discrimination. Peck and Rampal (2021) ask whether Segal's answer survives when incentive compatibility is weakened to the Bayesian (interim) notion, which leaves room for discrimination. Their Proposition 1 claims that it does, under four conditions on demand and beliefs. An earlier note by the same authors (Peck and Rampal 2019) shows that it fails when a single-crossing condition on beliefs (Condition 2 below) is dropped.
There are two demand states, low (state 1, probability ) and high (state 2, probability ). Valuations lie in with . In state the mass of consumers with valuation above is , so , and the demand density is . A consumer who knows their valuation updates their belief about the state in proportion to . The density ratio is . The firm has zero marginal cost and learns the state by aggregating reports.
A deterministic direct mechanism assigns to each state and report an allocation and a payment . It is anonymous: it depends only on the inferred state and the consumer's own report. It is ex post individually rational (EIR) if for all and both states, and Bayesian incentive compatible (BIC) if for all
The firm's profit is .
The conditions are: (1) each is with on ; (2) on ; (3) on ; and (4) either (i) on , or (ii) on . Under (4)(ii), every type assigns the low state the higher posterior probability. A monopoly price maximizes over . SBSMP sells in state to every at price .
Under Conditions 1, 2, 3 and 4(ii), SBSMP is BIC and EIR, and for every deterministic BIC and EIR mechanism ,
The goal does not claim uniqueness of the optimal mechanism, which the paper neither states precisely nor proves.
The milestones are the paper's own steps:
The goal is a BIC–DIC equivalence for an environment with correlated types and ex post participation. The paper describes it as the first such result: earlier equivalence results either assume independent types or rely on interim participation and large payments. When the conditions hold, a monopolist facing aggregate demand uncertainty gains nothing from the extra room for discrimination that Bayesian incentive compatibility allows, so Segal's ex post optimal mechanism remains optimal.
Formalizing the result adds three things. It checks a proof that is incomplete in print (see below). It separates the branch of the proposition that is true from the branch that is false. And it provides a reusable layer for mechanism design with a continuum of consumers and an aggregate state: demand curves and densities, deterministic anonymous mechanisms, EIR, posterior-weighted BIC, profit as an integral, and state-contingent posted prices. No part of the paper has been machine-checked before.
Status. The proposition is stated in the paper with Condition 4 as the disjunction of (i) and (ii). The Condition 4(i) branch is false, so this mission does not pose it. Take , , and , which satisfy Conditions 1–3 and 4(i). Consider the mechanism that
It is EIR, and BIC because every type is exactly indifferent between its two purchase options. Its profit is , which exceeds SBSMP's . The printed argument breaks where it treats a lower bound on the state-1 price of as a BIC constraint (§A.5.2(iv), Claim 3(iv)).
The Condition 4(ii) branch held in every exact computation on discretized instances: SBSMP was optimal among all BIC and EIR mechanisms in 34 of 34 random instances. Its printed proof has a gap. In Claim 5, the bound of (A.46) sets the state-1 price of the lowest type of equal to . Under 4(ii), BIC allows that price to be strictly larger, so is not an upper bound. A solver must supply a correct argument for excluding mechanisms in which only and are nonempty.
The class of competitors is large: , and can be arbitrary sets, and payments on arbitrary functions. The natural first step proves an interval structure and then optimizes over a few thresholds. That step does not go through in general. BIC alone does not force the interval property when all three sets are nonempty, and the paper instead compares against bounding mechanisms that need not be BIC. Statements that "the optimal mechanism" has a given set nonempty are fragile, because moving a single indifferent type changes them without changing profit. Excluding under 4(ii) is exactly the step where the printed bound fails. Reading SBSMP's optimality off the ex post (DIC) problem is also not enough: BIC permits strictly more mechanisms, and the 4(i) counterexample shows that the extra mechanisms can win.
Fin 2: index 0 is the paper's state 1 (low), index 1 is state 2 (high). The economy is a structure with vlo vhi α₁ : ℝ and D : Fin 2 → ℝ → ℝ. Valid records , and . These are added explicitly: EIR is unsatisfiable at negative types, and is the model's meaning of .Bool, which is "deterministic". EIR and BIC quantify over all . SBSMP charges to non-buyers.sSup, or by asserting only that SBSMP is feasible. Each of these would change the theorem.Warnings about health, financial or environmental risks are among the most common policy instruments: cigarette packs carry risk statements, doctors tell patients which risk group they belong to, and retirement planners report survival probabilities. Standard decision theory says that more accurate information can only help a decision maker. That conclusion fails when the decision maker has present bias, a stronger preference for immediate gratification than his own later selves would endorse (Phelps and Pollak, 1968; Laibson, 1997). For such a decision maker, learning that a harmful habit is only moderately risky can trap him into consuming even though, from an earlier perspective, he would rather abstain.
Mariotti, Schweizer, Szech and von Wangenheim ask how information about an individual risk should then be disclosed. They combine the quasi-hyperbolic model of self-control of Carrillo and Mariotti (2000) with the Bayesian-persuasion framework of Kamenica and Gentzkow (2011), and characterize the information structure that maximizes the decision maker's own long-run welfare, an information nudge. This mission formalizes that characterization.
A decision maker lives at dates 0, 1, 2, 3. At dates he chooses (consume or abstain). Consumption yields utility 1 immediately and, with probability , a cost two periods later. With a present-bias parameter and a discount factor , his date-0 and date-1 utilities are
with . The risk type is unknown; the prior is any probability distribution on , discrete, continuous or mixed, with distribution function . Two cutoffs organize the analysis:
Given a mean belief , both of the decision maker's selves consume if and abstain otherwise (Lemma 1); the date-0 self would prefer to abstain whenever .
A persuasion mechanism is a measurable , the probability that a type- decision maker receives the recommendation "consume". It is incentive-compatible if both recommendations are followed:
each constraint being void when its denominator vanishes. The designer maximizes the date-0 welfare, which up to a positive constant is . A cutoff mechanism recommends consuming with probability to the lowest types: with ,
The paper's Assumption 1 is and .
Under Assumption 1:
Optimality is over all incentive-compatible mechanisms. Uniqueness of is among .
The result shows that the welfare-maximizing disclosure policy for a present-biased agent is coarse and has a simple shape. It never reveals the type fully. It tells the lowest-risk types to consume and the highest-risk types to abstain, with randomization at most at one type. When harmful consumption cannot be avoided, the warning to abstain is pooled so that the abstaining group's mean risk is exactly , just alarming enough to be credible. The paper's comparative statics in the present bias, the alternative objectives of §5 and the traffic-light nudges of §6 are all built on this characterization.
The result is proved in the paper; to our knowledge it has not been machine-checked. A formalization adds a fully explicit treatment of priors with atoms, where the cutoff mechanism randomizes and the conventions , matter, and of the degenerate cases in which a recommendation is never sent. It also produces a reusable "bathtub" lemma (Lemma 2) and a monotonicity result for upper-tail conditional means for general distributions on the line, neither of which is in Mathlib.
The design problem is an infinite-dimensional linear program with a strict inequality constraint, so existence of an optimum is not automatic: a strict constraint can make the supremum unattained (the paper's §5 lobbyist problem has exactly this defect). The reduction to cutoff mechanisms requires the minimization in Lemma 2 for arbitrary distributions, including atoms at the quantile, and uniqueness up to null sets. The second half of Proposition 2 depends on how the upper-tail conditional mean behaves as a function of the mass of the tail: continuity across atoms, the limit at the top of the support, and monotonicity that becomes non-strict when there is an atom at . A naive argument that treats as continuous and invertible covers none of these cases.
The goal is not trivialized: optimality ranges over all incentive-compatible measurable mechanisms, not only cutoff mechanisms; (6) is not weakened to ; and is asserted to exist, not assumed.
A complete development needs the theory of the quantile function and of left limits of distribution functions for general measures on , the bathtub principle, and continuity of . These parts are reusable beyond this mission. Proofs of any milestone, and of auxiliary facts about distribution functions and quantiles, are welcome.
Minimizing a nonsmooth, nonconvex Lipschitz function is intractable in general, so nonsmooth optimization asks for a weaker certificate: a point near which a small convex combination of nearby subgradients exists. Such a vector is a Goldstein subgradient, a notion going back to Goldstein in the 1970s. Zhang, Lin, Jegelka, Sra and Jadbabaie (2020) gave the first dimension-free complexity analysis for finding a small Goldstein subgradient, using a directional subgradient oracle and a randomized line search. Concurrent work by Jordan, Lin and Zampetakis and by Kornowski and Shamir (2022) proved negative results for the general dimension-independent question with deterministic methods.
Kong and Lewis show that the obstruction disappears once the nonconvexity of the objective is measured. A simple deterministic bisection replaces the random line search, and the number of oracle calls is bounded explicitly in terms of a nonconvexity modulus . For difference-of-convex objectives (piecewise linear functions among them, which are not weakly convex) this gives an deterministic method, and in the weakly convex case (arXiv:2210.00652, abstract).
is a real inner product space with norm , possibly infinite-dimensional and not complete. is convex and is a real function on , bounded below.
Started at with and with any , if , Algorithm 4.1 stops at a point with , , within
oracle calls. The paper prints the first factor as . That expression is at a minimizer, and the bound fails there: a run started with a large subgradient needs at least one call. The page's own proof gives the corrected count.
The milestones follow the paper's proof:
The theorem gives a deterministic, dimension-independent oracle complexity for Goldstein stationarity, with the dependence on nonconvexity isolated in one scalar, . The paper bounds for weakly convex functions (Proposition 6.2), for difference-of-convex functions (Proposition 6.3, Corollaries 6.4–6.5) and for semi-linear functions, so explicit rates follow for each class. The univariate result, Corollary 5.6, is a complexity bound for a bisection line search in its own right, and Example 5.9 shows it is optimal among line searches.
The result is proved in the paper; no machine-checked version is known. The mission produces a formal model of the oracle, the Goldstein set, the concave deviation and the full run of Algorithm 4.1, with every oracle call counted. It also states the corrected constant. Formalizing the proof checks that the bound survives a stricter accounting than the paper's, which counts only line-search evaluations, not trial points or re-initializations.
Two counting arguments are glued together, and each has a gap that the prose skips.
First, the bisection bound needs the convex perturbation of the concave deviation to control the bisection through Theorem 5.2. The induction there restarts the method on a half-interval, and its sub-run re-evaluates an endpoint that the outer run evaluated already. Aligning the counts takes care.
Second, the global bound multiplies the number of phases by the number of line searches per phase and the cost per line search. The phases are separated by reductions, and a line search may stop at its first evaluation. The algorithm's iterates must also be shown to stay where the hypotheses apply: in , below , with segments of length inside .
The tempting shortcut is to take the printed bound and the paper's count of line-search evaluations at face value. Both are off at the edges.
[NormedAddCommGroup X] [InnerProductSpace ℝ X], with no completeness and no finite dimension.X → ℝ constrained only on . The oracle identity is required only at points of , along directions that stay in for small steps.sInf (f '' C) with BddBelow (f '' C).ℝ≥0∞. "Finite " is ≠ ⊤, and the bound uses its real value.HasDerivWithinAt on closed intervals. Their finiteness is an added hypothesis.Nat.floor/Nat.ceil.A trivializing formalization is ruled out: the goal is a bound fixed before the run, on the actual run that bisects with the rule and updates by shortest vectors. Mere existence of a point with a small Goldstein subgradient, or termination without a bound, are weaker statements and are not the goal.
Infrastructure needed: one-sided derivatives of convex functions on intervals, monotonicity of their difference quotients, and a counting argument over a state machine. Proofs of the univariate milestones (Lemma 5.1, Theorem 5.2, Corollary 5.6) are reusable for other line-search analyses. Contributions of any milestone are welcome. Not formalized here: Propositions 2.4, 3.2, 5.5, 6.2, 6.3, Theorem 4.3 (termination under semismoothness), Theorem 5.7 and the appendix on distributional second derivatives.
Ranking from pairwise comparisons is used in sports ratings, recommendation systems, crowdsourcing and web search. The most widely used parametric model is the Bradley–Terry–Luce (BTL) model (Bradley and Terry 1952; Luce 1959), in which item carries a score and item beats item with probability . The scores are identified only up to a common shift, so estimation is carried out under a constraint such as . Point estimation in this model is well understood: the regularized maximum likelihood estimator attains optimal rates (Chen, Fan, Ma and Wang 2019). Uncertainty quantification, such as confidence intervals for a score or tests of whether one item is preferred to another, requires more: an estimator whose individual coordinates are asymptotically normal with an estimable variance.
Liu, Fang and Lu build such estimators through a Lagrangian debiasing step. Debiasing a regularized estimator by one Newton-type correction is standard in high-dimensional regression (Zhang and Zhang 2014; Javanmard and Montanari 2014; Ning and Liu 2017). Under an equality constraint, the Hessian alone is the wrong object: the correction has to respect the constraint, which leads to the bordered Hessian of the Lagrangian. Theorem 3.1 of the paper states asymptotic normality of the resulting estimator in a general framework, not tied to the BTL model; the BTL case is a separate result (Theorem 3.2) with its own proof.
A parameter is estimated by minimizing a random loss subject to one smooth equality constraint . Write , for the true parameter and for an initial estimator. Norms: , , and for a matrix .
The bordered Hessian at is
In high dimensions need not be invertible, so its inverse is estimated by a block formula. Let be an estimator of the inverse of (the paper uses CLIME, Cai, Liu and Luo 2011), and . The block-inverse estimator is
and the Lagrangian debiased estimator is
The population counterpart is the same formula applied to , where is the target of . Let and define the variances
Assumptions 3.1–3.4 of the paper control the initial estimator (), the score and Hessian of the loss (, Hessian Lipschitz with constant along the segment from to ), the constraint gradient (bounded by , Lipschitz with constant ), and the inverse-Hessian estimator (, , , , ). Assumption 3.5 is a central limit theorem for the score , studentized by and , under a lower bound on these variances.
If and
then
The rates are left abstract, so the goal covers every model in which the five assumptions can be verified.
The theorem gives asymptotically valid confidence intervals for a single score and for a score difference under a general equality constraint, from an initial estimator that may be biased and a Hessian that may be singular. Pairwise differences are the basic building block of the paper's ranking inference (comparisons of two items and, through the bootstrap of §3.2, tests of top- membership). The general form makes the debiasing step reusable for other constrained M-estimation problems: any model with a smooth equality constraint for which Assumptions 3.1–3.5 can be checked inherits the conclusion.
The result is proved in the paper; it has not been machine-checked. The mission formalizes the general framework of §3.1.1 with explicit, dimension-uniform constants, which makes precise several points the printed statements leave implicit: which norm is meant on , which blocks of and the proof actually controls, and where the constraint enters.
The deterministic core is a perturbation argument for the rank-one corrected matrix , together with an integral-form Taylor remainder for and under a Hessian-Lipschitz condition, all with constants that must not grow with . The obvious approach of bounding the inverse of directly fails: may be singular, and the estimator never inverts it. The bounds have to be carried block by block, with the correct pairing of norms: the matrix row-sum norm against the vector sup norm, and the norm on the constraint gradient. A careless choice (the max-entry norm on ) makes Corollary 3.2 false as . Passing from the remainder bounds to convergence in distribution requires the variance lower bound in Assumption 3.5: without it the remainder, divided by , need not vanish.
Parameters live in Fin d → ℝ with the sup norm; matrices are Matrix (Fin d) (Fin d) ℝ; bordered matrices are indexed by Fin d ⊕ Unit via Matrix.fromBlocks. Gradients and Hessians are defined from fderiv; the loss is and the constraint . All random objects live on one probability space; the sample size is , and the dimension and the coordinates are sequences. Convergence in distribution is TendstoInDistribution to the law gaussianReal 0 1, and is TendstoInMeasure.
Conventions committed to:
A formalization that takes as an arbitrary matrix satisfying the conclusion of Corollary 3.1, or that drops the variance lower bound (so that a zero variance makes both sides by Lean's division convention), would be a different and weaker theorem and is ruled out.
A complete development needs: dimension-uniform perturbation bounds for rank-one updates in the row-sum norm; the fundamental theorem of calculus for along a segment; and Mathlib's Slutsky lemma (tendstoInDistribution_of_tendstoInMeasure_sub). The perturbation and Taylor lemmas are reusable for any constrained or debiased M-estimator. Proofs of any milestone, and alternative routes to the goal, are welcome.
CoVaR is the measure of systemic risk proposed by Adrian and Brunnermeier (AER 2016): the β-quantile of one institution's loss given that another loss (a bank, a market index) sits exactly at its own α-quantile, its value-at-risk. Regulators and risk managers compute it from simulation models of portfolios, where the joint law of is available only through samples. The difficulty is that the conditioning event has probability zero, so no sample ever lands on it, and the ordinary sample quantile cannot be applied.
Huang, Lin and Hong (arXiv:2210.06148v1, 2022; Operations Research, 2024) propose a batching estimator that circumvents this and establish its consistency, asymptotic normality and rate of convergence. This mission formalizes the asymptotic normality and the rate (their Theorem 3), together with the lemmas its proof rests on.
Let have a joint density on , with marginal density and marginal distribution function . The conditional distribution function is (Equation (3) of the paper)
and the conditional density is . For , and are the reals with
Assumption 1 asks for open neighbourhoods and on which (on ) and (on ) are continuously differentiable and positive, and that be twice differentiable on for each .
The batching estimator. An i.i.d. sample of size is split into batches of pairs . In batch , sort the 's, take the -th smallest, , and let be the paired with it (its concomitant; not the -th smallest ). Then
the -th smallest of . Write for the empirical distribution function of the batch values and .
A sequence is if for every there is with for all .
Suppose Assumption 1 holds, there is with for and for , and . Then
Both regimes are part of the goal.
In the order of the paper's argument:
Theorem 3 separates the two sources of error in the estimator: the bias of order from replacing by the event of being the -th order statistic, and the sampling noise of order across batches. Balancing them gives the optimal rate , slower than the of an ordinary quantile estimator; that gap is the price of conditioning on a null event. In the regime the limit law is the one obtained as if were known, which is what justifies the distribution-free confidence interval the paper builds from two order statistics.
The result is proved in the paper, with an appendix proof. It has no machine-checked proof. Formalizing it requires the first Lean development of concomitants of order statistics as estimators, a quantitative bias bound for a smooth functional of a sample quantile, and a Berry–Esseen step specialized to Bernoulli summands, all on top of Mathlib's convergence in distribution. The milestones are each usable on their own: Equation (6) and Lemma 3 apply to any batching or nearest-neighbour conditional estimator, and the p. 8 identity is a general fact about empirical quantiles.
The batch values are i.i.d., but their common law is not the target conditional law ; it depends on and drifts towards the target only at rate . A standard quantile central limit theorem therefore does not apply to : the triangular array changes law with , and the bias has to be controlled uniformly in near CoVaR, at the moving points , where and is the scale of the limit law. Controlling that bias requires the law of a single order statistic of (Lemma 3) without any moment assumption on . The paper's printed proof cites moment bounds on the order statistic that need not hold for heavy-tailed , and Assumption 1 says nothing about tails. The normal approximation is needed with an explicit rate (Lemma 4), not merely in the limit, because it is evaluated along the moving points .
All statements live in the namespace CoVaRMC.Batching, built on Mathlib and on the published order-statistic definitions ImpactInvesting.Portfolio.orderStat / inducedOrderStat (Mathlib's Tuple.sort, ties broken by index; ties have probability zero under a density).
TendstoInDistribution to gaussianReal 0 σ² with .The goal is not any of the following weaker statements, each of which would trivialize it: consistency of (the paper's Theorem 2); a fixed batch size ; batch values drawn directly from , which skips the concomitant; one regime only; or an whose constant may depend on .
Contributions welcome: proofs of any milestone, a general Berry–Esseen theorem in Mathlib form (from which Lemma 4 follows), and the measurability of order statistics and concomitants as random variables.
Panels of professional forecasters — the European Central Bank's Survey of Professional Forecasters, the Federal Reserve's surveys, election and sports forecasters — increasingly report probabilistic forecasts: a whole predictive distribution rather than a single number. Aggregating such panels presumes that each forecast reflects the forecaster's own information. Forecasters, however, are also judged against each other, and an expert who strays far from the consensus risks being wrong alone. This tendency to move toward the crowd is called herding.
For point forecasts, herding has a standard model: the beauty-contest game of Morris and Shin (2002), in which each agent trades off accuracy against closeness to the average action, and whose unique linear equilibrium overweights public information. Jia, Keppo and Satopää (SSRN 3674961) extend this game from point forecasts to normal probabilistic forecasts, scoring accuracy with the logarithmic score and deviation with the Kullback–Leibler divergence. Their Theorem 1 gives the equilibrium in closed form; it drives their analysis of information disclosure and their structural estimation of the herding level from survey data.
A state is unknown, with the improper flat prior . There are experts. Expert observes a public signal and a private signal , with independent noises and , precisions . Expert 's posterior of given is the normalized likelihood; its mean and variance are
Given , another expert's private signal follows the predictive law, the posterior convolved with .
Each expert reports a forecast , , standing for , as a function of ; such an assignment for all experts is a strategy profile . The negative log score of at is
and the KL deviation of from is
With herding level , expert chooses to minimize
A (Bayesian Nash) equilibrium is a profile in which every expert's forecast minimizes (9) at every signal pair, given the others' strategies.
For , let
The goal asserts three things: the profile is an equilibrium; every equilibrium reports the means ; and every equilibrium whose variances grow at most polynomially in the private signal is this profile.
The theorem says that herding acts on a probabilistic forecast in two separate ways. The mean shifts toward the public signal exactly as in Morris and Shin (2002), independently of the variance. The variance is inflated above the Bayesian posterior variance by a term quadratic in , so experts whose private information disagrees with the public signal report more uncertainty. Neither the mean nor the variance depends on . The paper's comparative statics, its analysis of public information disclosure (Theorem 2), and the structural estimator of (Theorem 3) all start from this closed form.
The result is proved in the paper's electronic companion by a first-order-condition argument and a reference to Morris and Shin's uniqueness argument. As printed the uniqueness claim is false (see Formalization scope), so the mission states what is true. No part of it is formalized anywhere known: the work is the Gaussian posterior under an improper prior, the best-response computation with an explicit unequal-variance KL term, and a uniqueness argument for a linear fixed-point equation driven by a Gaussian Markov kernel.
The best response is not a convex problem: the objective is not jointly convex in , though it has a unique minimizer, and the minimizer must be found against arbitrary measurable, possibly asymmetric opponents. The main obstacle is uniqueness. The mean equation (EC.11) is a fixed point of an averaged predictive-expectation operator . The obvious argument iterates and uses , but is not a contraction on unbounded functions: with and , maps to for a specific . At this produces non-closed-form solutions. The means are still pinned down, but only through the variance equation (EC.12); the variances need an extra growth condition.
Everything lives in the namespace HerdingForecast.Equilibrium, in one definitions file and six theorem files. Signals, states, means and variances are real numbers; experts are Fin K; a profile is a function Fin K → ℝ → ℝ → ℝ × ℝ. The improper prior gives no joint probability measure, so "" is integration against two explicit laws, the normalized likelihood (posterior) and its convolution with (predictive). The deviation is the paper's explicit KL formula, not Mathlib's klDiv. Logarithms are natural.
The following hypotheses and conventions are not printed in the paper and are disclosed in each statement:
Two formalizations would trivialize the goal and are ruled out. The equilibrium is not defined by the first-order conditions: it is defined by minimization of (9), so the best-response milestone carries content. Uniqueness is not restricted to linear, symmetric or continuous profiles: it ranges over all admissible profiles. The paper restricts attention to symmetric equilibria (§2.2, p. 10); uniqueness over all admissible profiles contains that case.
A complete development needs Gaussian integrals of polynomials and of of a quadratic, the convolution of Gaussians (in Mathlib), the posterior computation for a product of Gaussian densities, and an iteration argument for with Jensen's inequality and Tonelli. The posterior and predictive laws, and the Gaussian Markov-kernel argument, apply to other Gaussian beauty-contest games beyond this mission. Proofs of the milestones in any order are welcome, as is a proof of the variance-uniqueness clause under a weaker growth condition than polynomial.
Envy-free cake cutting asks for a division of a divisible resource, modelled as the interval , among agents with individual preferences so that no agent prefers another agent's share to its own. For a single cake and contiguous pieces, the existence of envy-free divisions goes back to Stromquist (1980) and to Su's Sperner-lemma proof (1999).
Multi-layered cake cutting, introduced by Hosseini, Igarashi and Searns (2020), models resources made of several parallel copies of a time line: meeting rooms booked over a day, or a facility with several machines shared in time slots. A bundle receives a piece of every layer, and it is feasible only if its pieces in different layers do not overlap in time, since one group cannot use two rooms at once. Igarashi and Meunier (arXiv:2106.02262v4, Mathematics of Operations Research, 2025) prove that envy-free feasible divisions exist when the number of bundles is a prime power, and they divide the agents into groups of almost equal size, each group sharing one bundle.
Timeline:
A piece is a finite union of pairwise disjoint closed subintervals of . An -layered cake has layers , each a copy of . A layered piece has one piece per layer; it is non-overlapping if is empty or finite whenever . A multi-division is a -tuple of layered pieces covering every layer, with entries meeting in at most finitely many points of each layer. It is contiguous if each is an interval, feasible if each is non-overlapping, and obtained with long knives if there are positions , the same in every layer, such that every is one of the intervals .
Each agent has a choice function that returns, for a multi-division , the set of preferred layered pieces. It is invariant under permuting the entries of , and it prefers at least one entry of . Layered pieces are compared by the pseudo-metric , where is Lebesgue measure. An agent has closed preferences if, whenever multi-divisions converge entrywise to a multi-division and for all , also . One agent is the birthday agent : the division is computed without its preferences, and it may pick any bundle afterwards.
Let with a prime power, and let all agents have closed preferences. Then there is a feasible, contiguous multi-division into layered pieces, obtained with long knives, such that for every there is an assignment with
The multi-division is fixed before the birthday agent chooses. The group sizes count the birthday agent.
For and , Theorem 1 is the Avvakumov–Karasev theorem: an envy-free division exists even when agents may prefer empty pieces, provided the number of agents is a prime power. For general it gives envy-free divisions among groups, and for a feasible schedule of parallel resources. The paper derives from it the existence of proportional feasible multi-divisions for every with (Theorem 5).
None of these results has been machine-checked. A formalization would add, beyond Theorem 1 itself, a Lean model of multi-layered cake cutting with choice-function preferences, the chessboard complex with its free group action, and an integral rounding lemma for bipartite assignments with a reserved slot. No statement of Volovikov's theorem or of its consequences exists on the platform yet; Lemma 1 would be the first.
The classical route encodes divisions by points of a simplex and applies Sperner's lemma. In the layered setting the induced coloring need not satisfy Sperner's boundary condition, even for monotone preferences (p. 6), and without hungriness it fails already for one layer. The proof therefore relies on Volovikov's Borsuk–Ulam-type theorem for -actions and on the -connectivity of the chessboard complex ; Mathlib has neither. The prime-power hypothesis is essential: for one layer and not a prime power, Avvakumov and Karasev show that envy-free divisions need not exist without hungriness, and Lemma 1 itself fails already for . Passing from triangulations to the limit needs closedness of preferences and the continuity of the encoding (Lemma 3), whose proof must handle several simplices of the configuration space accumulating at the same limit point.
Layered pieces are Fin m → Set ℝ, multi-divisions Fin q → Fin m → Set ℝ, choice functions maps from multi-divisions to sets of layered pieces. "Disjoint interiors" and "non-overlapping" are encoded as finiteness of intersections, which is equivalent for finite unions of closed intervals. The pseudo-metric sums (volume (symmDiff …)).toReal over the layers. The birthday agent is an arbitrary b : Fin n; "prime power" is IsPrimePow q; group sizes are cardinalities of fibres over all of Fin n.
Three readings are disclosed:
The chessboard complex is realized concretely in , with columns indexed by , so the bijection of the page is the identity.
Trivializing formalizations are ruled out. Without the covering clause the empty multi-division would satisfy everything. An agent preferring nothing would make the goal false. Choosing the multi-division after the birthday agent's choice () is a weaker theorem. The goal states .
A complete development needs:
These pieces, and the cake model, are reusable beyond this mission. Contributions are welcome on any milestone.
Large projects such as buildings, infrastructure and software systems are routinely outsourced. The client who owns the project pays a subcontractor to execute it, and the subcontractor privately chooses how hard to work. Faster work costs him more, while the benefit of early completion goes mainly to the client. The paper notes that the fixed-price and cost-plus contracts are the two most widely used contract forms in practice, and that their terms are typically negotiated rather than dictated by one side.
Hou, Lu, Deng and Shen ask which contract forms align the subcontractor's choice of work rate with the system optimum once the terms are set by bilateral bargaining, and how the answer depends on the two firms' bargaining powers. Most earlier project-contracting models (Bayiz and Corbett, 2005; Kwon, Lippman and Tang, 2010; Chen, Klastorin and Wagner, 2015) let one party make a take-it-or-leave-it (Stackelberg) offer; Lippman, McCardle and Tang (2013) is a bargaining exception. That is the extreme case of a Nash bargaining framework with all the power on one side. This mission formalizes the single-task part of the paper (Section 3), whose main result is Proposition 1.
A client receives a one-time reward when the project is completed. The subcontractor chooses a constant work rate . Let be a random variable with a density, cdf and mean ; at work rate the task duration is . Both firms discount at rate . The subcontractor's realized total discounted cost is , with expectation . The standing assumptions are:
The system profit is
and denotes its maximizer, with .
A contract form specifies a payment , valued at completion, as a function of a term , of and of the realized cost :
| form | payment | parameter |
|---|---|---|
| fixed-price FP | — | |
| two-part fixed-price TF+, TF | (TF+), (TF) | |
| time-based incentive TB | ||
| cost-sharing CS | ||
| cost-plus C+ | — |
In the two-part contract, is a down payment made at the start of the task. The subcontractor's profit is his expected discounted payment minus , and the client's profit is the expected discounted reward minus the payment. Given a term , the subcontractor chooses a rate maximizing . When his profit is flat in , he chooses the system-optimal rate (footnote 1 of the paper).
The term is fixed by Problem B, the generalized Nash bargaining problem with disagreement points :
where is the subcontractor's bargaining power. Form coordinates the system at if Problem B has a solution and every solution induces . The set of such is . Finally,
is the subcontractor's profit under the TB term with parameter that induces .
and every bargaining solution at has the negotiated terms
with and . The goal also states that the TB set equals the printed interval when the minimum of is attained, and that for FP, TF+ and TB no bargaining solution outside induces .
Proposition 1 separates the contract forms by how much bargaining power they tolerate. The fixed-price and cost-plus contracts, the two forms most used in practice, coordinate the project only when one party holds all the power. The two-part fixed-price contract and the cost-sharing contract coordinate for every , at the price of a participation fee or of cost verification. The time-based incentive contract coordinates above a threshold. This classification is the base case for the paper's multi-task results (parallel and serial tasks, Propositions 2–4), which show that coordination degrades further when several subcontractors bargain separately. It also explains a common practical observation: commonplace contracts leave efficiency on the table whenever power is shared.
The proofs are in the paper's online appendix and have not been machine-checked. A formal proof would check the "only if" directions, which rest on an argument (following Horn and Wolinsky, 1988, and Feng and Lu, 2013b) that the upper frontier of the feasible set is that of a convex set. It would also settle the boundary of the TB set (see below) and produce a reusable Lean layer for Nash bargaining over contract terms with an induced best response.
The bargaining is over a contract term, and the payoffs depend on the subcontractor's induced work rate. The feasible set of profit pairs is therefore not convex in general, and Nash's theorem cannot be applied to it directly. Showing that the Nash product is maximized exactly at the coordinating terms needs global control of the best-response map : its existence, uniqueness and continuity, and the envelope behaviour of both profits along it. The naive argument "coordinating terms put the total profit at , so they must be optimal" fails twice. Under FP and TB the coordinating terms cannot reach every split of . Under C+ with every feasible outcome gives the subcontractor zero profit, so maximizing the Nash product selects nothing. The expectations involve a general scale family, so no closed forms are available. Concavity in has to come from Assumption 1 through the integration-by-parts identity of milestone 1.
The model is a structure holding , , the law of as a measure on , the realized cost and the expected cost , together with a validity predicate for the standing assumptions. Contract terms are pairs . For FP the dummy is pinned to , and for C+ to . Expectations are Bochner integrals. Conventions and added hypotheses:
Real.rpow on nonnegative profits, so makes it at and at .Weaker readings do not discharge the goal. Exhibiting one at which a form coordinates, showing that the printed terms are a Nash solution, or defining coordination as "some solution induces " all fall short: the goal fixes each exactly and asserts the terms of every solution.
The development needs concavity of Laplace-type integrals in the scale parameter, differentiation under the integral sign, and existence and continuity of maximizers of strictly concave functions on . The Nash-bargaining-over-terms layer is reusable beyond this paper. Contributions are welcome on each contract form separately: the four Proposition 1 milestones share no argument beyond milestones 1–3.
Dynamic traffic assignment predicts how travellers choose routes and departure times when travel times depend on the traffic itself. Its central solution concept, the dynamic user equilibrium, asks that no particle of flow can lower its cost by switching to another route or departure time. Existence of such equilibria in continuous time is classical: Friesz et al. (Oper. Res. 1993) gave the variational-inequality formulation, and Zhu and Marcotte (Transp. Sci. 2000) proved existence from Lions' theorem on variational inequalities.
Real networks also carry side constraints: hard limits on how much traffic an edge may hold (road volume caps, parking, the battery and charging limits of electric vehicles). In static models, side-constrained equilibria go back to Larsson and Patriksson (Transp. Res. B 1999) and to Marcotte, Nguyen and Schoeb (Oper. Res. 2004). For the dynamic model, Zhong et al. (Transp. Res. B 2011) claimed existence through a variational inequality over the constrained flow set. Graf and Harks (arXiv:2211.03194, Operations Research 2024) show that this claim fails: with volume constraints the feasible set need not be convex. They replace the variational inequality by a behavioural definition of equilibrium and prove the first existence theorem for the non-convex volume-constrained case. That theorem is the goal of this mission.
There are finitely many commodities and finitely many walks ; each walk belongs to one commodity, denotes the walks of commodity , and a walk is the list of its edges . Time runs over a horizon . A walk inflow gives the rate at which flow enters walk at time . With departure time choice, the feasible inflows are
where is the volume of commodity and bounds the inflow rate of walk .
The traffic model supplies four functions of the inflow: the effective walk delay , the cost of entering walk at time ; the arrival times at which a particle entering at time enters the -th edge of ; the edge loads ; and the capacities . The capacity-feasible inflows are .
A -deviation from walk removes a small inflow from and adds it to , delayed by : . A correspondence lists the admissible deviations, and is an admissible alternative to at time , written , if arbitrarily small admissible deviations concentrated arbitrarily close to exist. A flow is a side-constrained dynamic equilibrium (SCDE) if
Two choices of matter here. In a strong dynamic Larsson–Patriksson equilibrium (strong LPDE) a deviation onto is admissible if every edge of has strict slack, , at the time the deviating particle would enter it. In a strong dynamic Marcotte–Nguyen–Schoeb equilibrium (strong MNSDE) slack is not required on a common prefix of and when .
Under the paper's assumptions (A2), (A3), (A5), (A9)–(A19) and continuity of the capacities (A22),
The assumptions are qualitative (continuity, uniform convergence along weakly convergent inflows, causation, an outside option, bounded delays on ); no constants are fixed.
The result. Theorem 7.6 is an existence theorem for a model whose feasible set is not convex, where the standard route through variational inequalities is closed: the paper's counterexample (§4) shows that the variational-inequality approach of Zhong et al. does not give existence. The paper argues that the Vickrey point-queue model and the linear edge-delay model satisfy its assumptions (Lemma 7.10, whose proof defers to earlier work, and Corollary 7.11), and the equilibrium notions it produces (strong LPDE, strong MNSDE) are the dynamic counterparts of the established static side-constrained equilibria.
Formalizing it. The result is proved in the paper but nowhere formalized. A formalization adds a reusable layer for continuous-time traffic equilibria: walk inflows, weak convergence in , deviation operators, admissible deviations and SCDE, and Lions' existence theorem in , which does not exist on the platform or in Mathlib. A related item on the platform, FrieszDUE.PIE.theorem_2_pie_vip, characterizes route-departure equilibria by a variational inequality in a model without rate bounds; it is not the statement of Theorem 3.3 here.
The obvious approach is to solve the variational inequality over the constrained set . It fails twice: need not be convex, so Lions' theorem does not apply, and even a solution need not be an SCDE because small deviations from a feasible flow can leave . The paper therefore penalizes capacity violations in the cost, , and passes to the limit . The hard steps are the limit arguments: showing that the weak limit of penalized equilibria is feasible, and that an improving admissible deviation for the limit would produce an improving deviation for some penalized equilibrium. Both combine weak convergence of inflows with uniform convergence of loads, arrival times and delays; the second also needs strict slack to survive the passage to the limit.
Inflows, deviations and test functions are real functions on (representatives), not classes. The bounds defining hold almost everywhere, and inflows vanish outside ; the support and size conditions on hold pointwise on the chosen representative, as the paper prescribes on p. 33. Weak convergence is convergence of for every with square-integrable components. The deviation (17) is read additively, also when . Arrival times use a 0-based node index: Lean's tau h p j t is the paper's . Delays are real-valued. The condition , which §7 adds implicitly to every deviation set, is written out.
Every SCDE statement includes , and the admissible alternatives are built from genuine deviations: a measurable with , supported in , with . A formalization in which is always empty, or in which the SCDE predicate omits feasibility, would make the goal trivial and is ruled out; a sorry-free sanity file exhibits a feasible flow with a non-empty that is not an SCDE, and a model satisfying every hypothesis of the goal.
Three choices differ from the printed theorem. (A22) continuity of every capacity on is added: Theorem 7.6 assumes only that capacities are non-negative and non-decreasing, but two steps of its proof (that satisfies (A4), and the transfer of strict slack in Claim 7) need continuity, and the paper itself assumes (A22) in Theorem 7.9. (A17) is posed for all rather than , because the proof applies it to infeasible flows. Measurability of the arrival times is a standing convention. Only the model with departure time choice is posed; the half of Theorem 7.6 with fixed inflow rates is not.
A complete development needs: weak sequential compactness of in ; Lions' theorem in (Brouwer is available as AGT.brouwer_fixed_point); the bathtub argument behind Theorem 3.3; and the limit arguments of Claims 5–7. Lions' theorem and the weak-compactness facts are reusable beyond this mission. Proofs of individual milestones, in any order, are welcome.
Minimizing a separable convex function over the integral points of a polyhedron is a recurring problem in combinatorial optimization: resource allocation, minimum-cost flows with convex costs, and the "fair" or "decreasingly minimal" integral elements studied by Frank and Murota all have this form. When the polyhedron is described by a totally unimodular matrix, or is an integral base polyhedron (an M-convex set), discrete convex analysis supplies min-max theorems that certify optimality by a dual object. Frank and Murota (arXiv:2007.03507v3, Mathematics of Operations Research 2022) observe that the role of M-convexity in those theorems is only that M-convex sets are discrete box-TDI sets, and prove one min-max formula for every box-TDI polyhedron.
Timeline. Edmonds and Giles (1977, 1984) introduced total dual integrality and box-total dual integrality of linear systems. Cook (1986) and Cook, Fonlupt and Schrijver (1986) gave basic properties, including sparse integral dual optima. Murota's discrete Fenchel-type duality (2003) gives min-max formulas for M-convex functions. Frank and Murota (2020–2022) proved min-max theorems for separable discrete convex functions on M-convex and M₂-convex sets using that duality; the present paper derives them, and a general version, from box-TDI-ness alone.
Let be a finite ground set and a finite set of rows. For an integral matrix and an integral vector let and let be its integral points.
A rational system is totally dual integral (TDI) if, for every integral cost for which the maximum in
is finite, that maximum has an integral optimal solution . It is box-TDI if is TDI for all rational vectors .
A function is discrete convex if for every in its effective domain, and that domain is the set of integers of an interval. Given such for each , the separable discrete convex function is . Write . A pair of an integral and an integral row vector is -compatible with respect to if
with finite: is a subgradient of at .
Assume is box-TDI, , and is finite on . Then is bounded from below on if and only if some and some integral form a -compatible pair; in that case
both sides are attained, and the maximum is attained by a with at most positive components.
The proof runs through weak duality and a main tool on box-TDI systems:
The theorem gives an optimality certificate for separable discrete convex minimization over every box-TDI polyhedron: a minimizer is certified by an integral with and a subgradient of at . For linear it is integral linear programming duality for box-TDI systems. Specializations recover the min-max theorems for M-convex and M₂-convex sets, square-sum minimization over integral flows, and the paper's application to inverse combinatorial optimization.
The result is proved in the paper, which relies on two external theorems: Edmonds–Giles (a TDI system with integral right-hand side defines an integral polyhedron) and Cook–Fonlupt–Schrijver (sparse integral dual optima). No part of the theory of TDI or box-TDI systems is formalized in Mathlib, and the platform has no item on it. A complete development formalizes box-TDI-ness and its closure properties, both external theorems, and the main tool, all reusable for other integral-polyhedra results.
Weak duality is a coordinatewise subgradient inequality. The strong direction is the hard one: integrality of the dual is not a consequence of convexity. A natural first idea is to take the Lagrangian dual and invoke LP duality for the subgradient constraints; this gives a real , not an integral one. Total dual integrality of alone does not suffice: by Cook's counterexample (Remark 2.1) it is not inherited by the auxiliary system of Proposition 2.10, in which appears twice with one-sided bounds. The sparsity clause is a further integrality statement about dual optima, not a consequence of the min-max equality.
All definitions are in BoxTDIMinMax.Separable (one definitions file). Conventions:
WithTop ℤ, with ; is the finite sum. Discrete convexity is (1.2) on the domain together with an interval domain, as the page states; the identically function is allowed.EReal-valued and defined by cases; the sums in (2.9) never mix and .The goal is not weakened: without attainment, the inequality alone, the boundedness equivalence alone, or the formula without the clause are each a different, weaker theorem and do not close the mission. Box-TDI-ness cannot be replaced by TDI.
Contributions welcome: the TDI/box-TDI closure lemmas, LP-duality glue between the dual-feasible-set formulation and Mathlib, Edmonds–Giles integrality, and Cook–Fonlupt–Schrijver sparsity.
In a Markov decision process a controller chooses actions over time to influence a random system. A basic question for every such model is whether the controller loses anything by ignoring the past: whether, for every policy that uses the full history, some Markov policy (one that looks only at the current state and time) performs equally well. For discrete-time models the answer goes back to Derman and Strauch (1966): the Markov policy that randomizes according to the conditional distribution of the action given the current state has the same state-action marginals as the original policy, and therefore the same expected costs for any criterion that depends on these marginals.
In continuous-time jump Markov decision processes (CTJMDPs) with unbounded transition rates the question is harder, because the process may explode: infinitely many jumps can accumulate in finite time, after which the process leaves the state space. Earlier sufficiency results assumed bounded rates or nonexplosive processes (Kitaev 1985; Kitaev and Rykov 1995; Guo and Song 2011; Piunovskiy and Zhang 2014). Feinberg, Mandava and Shiryaev (arXiv:2003.01342) proved the continuous-time analogue of Derman and Strauch's result with no such assumption: the induced Markov policy has state-action marginals no larger than those of the original policy, and equal ones as long as it does not explode.
A CTJMDP is given by a state space and an action space , both standard Borel spaces; nonempty sets of actions available at each state , whose graph is measurable and contains the graph of a measurable selector; and transition rates , where is a finite measure, measurable in . The jump intensity is , and Assumption 2.1 requires for every . A probability measure on acts through and .
A trajectory is , with jump epochs and post-jump states ; the process is for and leaves at . A policy chooses, between the th and st jump, the action distribution , concentrated on . A Markov policy is a transition probability from to with . An initial distribution and a policy define the law of the process: from the next jump occurs at hazard rate and lands in with intensity .
The state marginal and the state-action marginal are
for , , . A Markov policy satisfies (16) for if
that is, is the conditional distribution of the action given under . The process under is nonexplosive when for all .
If is a Markov policy satisfying (16) for , then
with equality for whenever , and equality for all when the process under is nonexplosive.
The milestones follow the paper's proof: existence and uniqueness of (§2); the compensator identities (8) and Lemma 3; the forward identity (37) for -bounded sets (Lemma 4); Feller's minimal solution of Kolmogorov's forward equation (Theorem 3), its identification with the marginal of a Markov policy ((31), Corollary 5); the occupation identities (49)–(50); the state-marginal comparison (Lemma 2) and Theorem 1 for one initial state (Lemma 5); the characterization (19) of (16) (Corollary 1); the scaling identity (58)–(59) and the claim (19) for the extended model (p. 16); and the existence of (Lemma 1).
Theorem 1 with Lemma 1 shows that Markov policies are sufficient in CTJMDPs with unbounded rates. Every cost criterion that is a monotone functional of state-action marginals with nonnegative costs (expected total discounted costs, finite-horizon costs, average costs per unit time, and the corresponding constrained problems) is no larger under the Markov policy, which is the content of §6 of the paper. Equality holds whenever the Markov policy does not explode, for example when the rates are bounded (Corollary 2), and two Markov policies satisfying (16) have the same law (Corollary 3). The intermediate results, in particular Lemma 4 (the forward identity for possibly explosive processes) and Feller's minimal-solution theorem, are tools in their own right for continuous-time Markov chains on general state spaces.
The result is proved in the paper; nothing here is open mathematically. No part of it is formalized: Mathlib has no jump processes, compensators of point processes, Kolmogorov forward equations on general state spaces, or Feller's construction of minimal transition functions. The mission produces a machine-checked account of these foundations and of the sufficiency theorem built on them, with every measure-theoretic step (the law of the process, the disintegration, the minimality argument) made explicit.
The direct argument for discrete time compares the two marginals step by step through the one-step transition law. In continuous time there is no first step, and the natural replacement, comparing the forward equations satisfied by the two marginals, breaks down twice. First, with unbounded rates the integrals in the forward equation (37) can be infinite, so the equation is not even well defined for all sets, and the standard derivations assume nonexplosiveness. Second, forward equations need not have unique solutions when the process can explode, so showing that both marginals solve the same equation does not make them equal. The paper handles the first point with the class of -bounded sets and the second with Feller's minimal solution, which yields only an inequality in general; equality needs the probability-one condition. Passing from an initial state to an initial distribution is a further step: the forward equation is stated for a point initial condition, and the reduction goes through an extended model with an added state.
All quantities take values in . Rates are given by off-diagonal finite jump measures, with off . A trajectory is an element of X × (ℕ → ℝ≥0∞ × X); the cemetery point is not a separate state, and is ignored once . A policy is a family that depends only on the history up to the th jump. Marginals read the process at , which equals almost surely at each fixed .
The law is a hypothesis of each statement: any probability measure on trajectories with initial law whose one-step conditional laws are the explicit sojourn/jump kernel (the Ionescu-Tulcea construction (75)–(76) of the paper) is admitted, and a milestone states that exactly one such measure exists. The paper characterizes the same measure through Jacod's compensator theorem. The compensator properties (8) and Lemma 3 are stated as (8) for every stopping time of the natural filtration . Kolmogorov's forward equations are written additively, with the subtracted integral finite, which is equivalent to the real equation. In the extended model of the proof the added state and actions are Sum.inr points of X ⊕ Unit and A ⊕ Bool; the policy (55) is evaluated on the observed part of the path and chooses the absorbing action off the set , which is a null set.
A formalization in which the law is never shown to exist, or in which (16) cannot be satisfied, would make Theorem 1 vacuous; the existence-and-uniqueness milestone and Lemma 1 rule this out.
A complete development needs the Ionescu-Tulcea construction of the law, compensators of multivariate point processes, the forward equation and Feller's series on a standard Borel space, and disintegration of measures. The first three are reusable for any continuous-time Markov chain or CTJMDP on a general state space, and contributions to them are welcome on their own.
Minimizing a convex Lipschitz function over the unit ball of to accuracy takes first-order queries when is small compared with , and cutting-plane methods such as the center-of-mass method attain this rate (Nemirovski–Yudin 1983). They do so by storing their whole cutting history, about bits. Gradient descent stores one vector, bits, but needs queries. Woodworth and Srebro asked at COLT 2019 whether a method with bits can keep the near-optimal query count (Woodworth–Srebro 2019).
Timeline.
An -bit memory-constrained deterministic algorithm (Definition 3) has a query map , an update map and a stopping rule. Starting from , at iteration it queries , receives and stores . Here is convex and -Lipschitz, and is any subgradient selection: for all . The algorithm stops at some iteration ; its output is .
It solves convex optimization to accuracy with queries if on every pair it stops at some with for every . In Lean these are MemAlg d M, IsCOInstance f g, memAt and SolvesCO alg Q ε.
The proof introduces further objects: a sign matrix with ; the uniform law (sphereLaw) and its restriction to slabs (slabLaw); a partition of the sphere into equal-measure cells with representatives (SphereDisc); the parameters , , and of Eq. (3); the Orthogonal Vector Game with Hints (Game 2, Player, winProb); and the adaptive hard functions built by Procedure 1 (procRun).
For every there are , and such that for every and every -bit algorithm with that solves convex optimization to accuracy with queries,
The constants depend on , and none of them is fixed numerically.
The result. Cutting-plane methods are Pareto-optimal for deterministic algorithms up to logarithmic factors: between and bits, any saving in memory costs queries polynomially. Proposition 14 is a memory-sample trade-off for a game with adaptive side information, reusable for other learning problems with hints. The paper also proves a feasibility-problem version (Theorem 2) by the same method.
Formalizing it. The theorem is proved on paper but has no machine-checked proof. A formalization has to make several steps exact that the paper leaves informal: finite-precision hints, the joint law of adaptively sampled slabs, the information-theoretic chain rule of Proposition 14, and the case analysis of Procedure 1. Several statements needed small repairs to be true as written (see below), so writing them precisely is part of the work.
The obvious route is to let the hard function hide its structure in the kernel of and argue that each query reveals little about it. It breaks on information leakage. The vectors built in earlier periods depend on the algorithm's queries, which depend on . So the subgradients returned later can carry information about that the -bit memory never had to store, and a lower bound that ignores this leakage cannot reflect the memory constraint. The central difficulty is to bound this leakage by bits while the adaptively built function stays convex and indistinguishable, for the algorithm, from a fixed function queried through an ordinary first-order oracle (Proposition 8).
Conventions committed to:
EuclideanSpace ℝ (Fin d).Fin M → Bool, and stopping is a map on memory, read after each update.Hints are represented by their cells, so every probability of Game 2 and Procedure 1 is a finite sum. Disclosed repairs:
The reduction step carries the hypotheses and , which the paper's proof uses silently.
SolvesCO is not vacuous. An algorithm without memory cannot satisfy it at accuracy below (proved in a sanity file), while a subgradient method with rounded iterates and an iteration counter can satisfy it with bits. A formalization in which the output is not the query at the stopping time, or in which stopping may happen at time , would make the goal trivial; the definitions rule this out.
Needed infrastructure: the uniform sphere law and its conditioning on slabs; Beta-type laws of projections of uniform vectors; equal-measure partitions of the sphere; entropy and mutual information on finite spaces; singular values of rectangular matrices (Lemma 22). The sphere and information-theoretic lemmas are reusable beyond this mission. Proofs of any milestone are welcome, and so are proofs of the cited Lemmas 5 and 12.
Not formalized: Theorem 2 and the feasibility procedure (§4), and Remark 4.
A mechanism is strategyproof when truth-telling is a dominant strategy for every agent. Experimental and theoretical work has found that this guarantee is fragile in practice: agents faced with a sealed-bid second-price auction often misreport, while the same agents bid truthfully in the strategically equivalent ascending clock auction. Li (Obviously strategy-proof mechanisms, American Economic Review, 2017) explained the gap with obvious strategyproofness (OSP): a mechanism is OSP when, every time an agent is asked to act, the worst outcome of acting truthfully is at least as good as the best outcome of any deviation, given only what the agent has observed so far. OSP mechanisms are exactly those whose incentives can be checked by an agent with limited contingent reasoning.
This makes OSP a design constraint, and a natural question for algorithmic mechanism design is how much it costs in solution quality. Ferraioli, Meier, Penna and Ventre (arXiv:1805.04190v2, published as New Constructions of Obviously Strategyproof Mechanisms, Mathematics of Operations Research, 2023) give a characterization of OSP by cycle monotonicity and use it to measure this cost for makespan minimization on related machines, one of the standard testbeds of the field since Archer and Tardos (FOCS 2001). Without the OSP constraint, truthful mechanisms for this problem can be optimal. With it, the paper shows a gap of order as soon as each agent has three possible types.
There are agents. Agent has a private type in a finite domain , and is the set of type profiles. An extensive-form mechanism is given by an implementation tree : each internal vertex is labelled by an agent , who takes there an action depending only on her own presumed type; the action selects the child of at which execution continues. Each leaf carries an outcome, and is the outcome at the leaf reached by the profile . A profile is compatible with if its execution passes through ; two profiles diverge at if both are compatible with and leave it through different children.
The mechanism also pays each agent , and agent of type has quasi-linear utility , where is her cost of outcome . The mechanism is OSP if for every vertex with and all profiles , of that are compatible with and diverge there,
The OSP-graph has the profiles of as nodes, and an edge from to whenever the two diverge at some vertex labelled , of weight .
In machine scheduling on related machines, identical jobs are assigned to machines; agent owns machine and is its processing time per job. An outcome is a load vector with , agent 's cost is , and the makespan is . is the least makespan over all load vectors, and a mechanism is -approximate if its makespan is at most on every profile.
Let , (so ), and with , and . For every implementation tree whose outcomes on schedule all jobs, and every payment function making it OSP on ,
Equivalently, no OSP mechanism is -approximate for any . The statement fixes no approximation constant below ; it is the paper's lower bound in the instance family its proof uses.
The theorem shows that the restriction to obviously strategyproof mechanisms has a price that grows with the number of agents, even when every agent has only three types. It contrasts with two results in the same paper: an optimal OSP mechanism exists for two-value domains (Proposition 11), and for three-value domains there are OSP mechanisms that are -approximate when (Corollary 16) and -approximate when (Proposition 19), so is the right order. The cycle-monotonicity characterization (Theorem 3) is the tool behind both the lower and the upper bounds, and it reduces OSP to the absence of negative cycles in a finite graph, which is the form in which later work designs OSP mechanisms.
The results are proved in the paper; none is machine-checked. Formalizing them produces a reusable Lean model of extensive-form mechanisms (implementation trees, compatibility, divergence, OSP) that does not exist in Mathlib or on the platform, where incentive compatibility is formalized only for direct mechanisms. It also checks the proof of Theorem 12 where the paper is informal (agents that never diverge).
The obvious route to a lower bound for a truthful mechanism is a monotonicity argument on a single pair of profiles. For OSP this is not enough: OSP constrains only pairs of profiles that diverge at a vertex of the tree, and the mechanism designer chooses the order in which agents are queried and what each query separates. The lower bound must therefore hold for every query order and every partition of types at every vertex, including trees that query some agents late or never. The paper's argument identifies agents by the order in which they first diverge; agents that never diverge, and the integrality of job loads in the final counting step, are treated informally there and must be handled explicitly in Lean.
All declarations live in the namespace OSPMech.SqrtLB. An implementation tree is an inductive type whose internal vertices carry an agent i : Fin n and an action map ℝ → ℕ to child indices; positions are lists of child indices. The paper's four conditions on edge labels hold by construction. Types are reals, domains are Finset ℝ, outcomes for scheduling are load vectors Fin n → ℕ, and the cost of agent is . Payments are a function of the declared profile (p. 6), not a label of the leaves; for the impossibility results this admits more mechanisms and so strengthens them. The OSP-graph weight is the one of Observation 1 and of the proof of Theorem 3 (p. 24); Definition 2 prints the opponents' profiles swapped. The makespan is a supremum over the finite set of machines, an infimum over feasible load vectors.
The goal is stated for with , , , , exactly the instance family of the paper's proof, with written as ; the hypothesis reads the paper's non-negative costs with . Lemma 13 is stated for agents that really diverge on the all- path, with the paper's 1-based index written as rank .
The statement cannot be trivialized: the goal requires the mechanism's outcomes to schedule all jobs on every profile of (without this, "assign nothing" would be OSP with makespan ), OSP compares only pairs that are compatible with and diverge at a vertex of the deviating agent (so one-query trees satisfy it), the conclusion is an existential over profiles rather than a fixed approximation constant, and is excluded.
Contributions welcome: proofs of Observation 1 and Theorem 3 (the latter needs shortest-path potentials on a finite graph without negative cycles), proofs of the two parts of Lemma 13 from the 2-cycle case of Theorem 3, and the counting argument closing Theorem 12.
Bilevel optimization chooses an upper-level variable to minimize an objective that depends on the solution of a lower-level problem. Hyperparameter tuning and meta-learning are the standard examples (Franceschi et al. 2018; Ghadimi and Wang 2018). In the decentralized version the data are split among agents. Each agent sees only its own upper- and lower-level functions and , and it can talk only to its neighbours in a communication network. The paper's example is hospitals tuning a regularization weight of a logistic-regression model. No hospital may share its patients' data, but the hyperparameter has to be good for the pooled data.
Decentralized bilevel algorithms before this paper converged only under a heterogeneity assumption, a bound on how much the agents' functions may differ. DSBO (Chen, Huang and Ma 2024) assumes i.i.d. local data, MA-DSBO (Chen et al. 2023) a uniform bound on , and SLAM (Lu et al. 2022) Lipschitz-type closeness of the local Hessians. Such assumptions fail exactly when the agents' data differ, which is the case that motivates decentralization in the first place. Dong, Ma, Yang and Yin propose SLDBO, a single-loop method that needs no such assumption, and prove an rate for it.
There are agents. Agent holds . Write and . Problem (6) is
Assumption 2.1 gives constants and . Each is -strongly convex. is -Lipschitz with an -Lipschitz gradient. is twice differentiable with an -Lipschitz gradient and an -Lipschitz Hessian. Under these conditions is well defined and is differentiable, with the hypergradient (7)
Here are the partial gradients, is the Hessian of in , and is the Jacobian of in .
Assumption 2.2. The agents communicate through a nonnegative, symmetric, doubly stochastic mixing matrix , and bounds the contraction of away from consensus.
SLDBO (Algorithm 1) keeps three local iterates per agent. Agent computes the local directions , and at . It feeds them into gradient-tracking variables , which estimate the network averages of the directions. It then takes one mixed step on each iterate with constant step sizes . The step on is followed by the projection onto the ball of radius , which contains every . All agents start from common points with (BOX 1). Bars denote averages over agents, e.g. .
The step sizes have thresholds depending only on : first , then given , then given . Below these thresholds, every instance with bounded below has a constant such that for all
The goal fixes no explicit step sizes and no explicit constant ; it asserts the rate.
These are the paper's own statements, in attack order:
The theorem shows that a single-loop decentralized method reaches the stationarity rate known for centralized single-loop bilevel methods (Ji et al. 2022; Dagréou et al. 2022). Each iteration needs communication rounds and one Hessian- and one Jacobian-vector product, with no heterogeneity bound. The consensus clauses add that the agents agree at the same rate.
The result is proved in the paper; nothing about it is formalized. The mission adds three things. First, a machine-checked statement with explicit conventions. Second, a check of the constants. The printed in (8) has a term that is not homogeneous in the scale of , and the explicit step-size bounds (62) do not make the Lyapunov coefficient nonnegative (checked numerically). The goal is therefore stated in a form the argument supports. Third, reusable lemmas for gradient-tracking analyses: the mixing-matrix contraction, the projected-consensus inequality, the tracking identity and the hypergradient formula.
The obvious analysis of a decentralized SOBA-type method bounds the change of the directions and between iterations by the change of the iterates. Those directions contain . Without control of , their variation is bounded only by assuming the local Hessians are close, which is the heterogeneity assumption. The projection removes the need for it. The price is that no longer follows the averaged direction, so the consensus and error recursions for have to be derived separately. All of these recursions are then combined into one Lyapunov function (15) whose coefficients must be balanced against three coupled step sizes. Most of the work, and the published constants' main failure, is in that balancing.
Vectors live in EuclideanSpace ℝ (Fin d). Lipschitz conditions in use , never Lean's sup norm on a product. The model and the added hypotheses:
ContinuousLinearMap.inverse, and is the formula (7). A milestone proves that (7) is the gradient of .run. Its state at index holds .The goal would become trivial if the thresholds were chosen after the instance or after , and false without bounded below; the statement rules both out. All hypotheses are satisfiable: a two-agent instance with and is checked in Lean.
A complete development needs the implicit-function theorem for , the descent lemma, strong-convexity inequalities for gradient steps, and the gradient-tracking bookkeeping. The mixing-matrix and tracking lemmas are reusable for other gradient-tracking methods. Proofs of any milestone, and repaired explicit step-size conditions, are welcome.
A learner who minimizes a regularized population risk
usually has access to only through an i.i.d. sample , and so works with the empirical risk instead. The question this mission formalizes is how well the first-order behaviour of reflects that of when the loss is neither smooth nor convex. This matters because the algorithms used in practice for such problems (stochastic subgradient, proximal point and Gauss–Newton methods) find only approximately stationary points, and a uniform estimate of the gap between empirical and population stationarity tells one when further optimization of the empirical problem stops improving the population one.
For convex losses with strongly convex regularization, Shalev-Shwartz, Shamir, Srebro and Sridharan (COLT 2009) showed that the regularized empirical minimizer is stable and generalizes at a dimension-free rate. For smooth nonconvex losses, Mei, Bai and Montanari (Ann. Statist. 2018) and Foster, Sekhari and Sridharan (NeurIPS 2018) proved uniform convergence of gradients. For nonsmooth nonconvex losses, pointwise convergence of the stationarity measure was known, but uniform results were asymptotic and needed extra structure, because is highly discontinuous. Davis and Drusvyatskiy (arXiv:1810.07590, Mathematics of Operations Research 2022) replace it by a smoothed measure, the gradient of a Moreau-type envelope, and prove finite-sample uniform bounds for it. The losses covered are the weakly convex ones: phase retrieval, blind deconvolution, robust PCA, censored block models, conditional value-at-risk and sparse dictionary learning all fit (Table 1 of the paper).
Fix a finite-dimensional real normed space with norm and dual norm . Extended-valued functions are described by their domain and their values there.
A Legendre function is proper, closed and strictly convex, differentiable on the nonempty interior of its domain, and its gradient norm blows up at the boundary of the domain. It induces the Bregman divergence
and its symmetrization . For , . A function is -weakly convex relative to if is convex, and compatible with if . For the Φ-proximal map and Φ-envelope are
The standing assumptions are: (A1) is Legendre, compatible with , and on ; (A2) for a.e. , is -weakly convex relative to and bounded below; (A3) with and . Finally for an independent Rademacher sign , and is its Fenchel conjugate.
For every , , and , with probability at least ,
where is the covering number of in the metric . If is twice differentiable, the same probability bounds the event in the local dual norm.
The result gives a sample size beyond which approximate stationarity of the empirical problem certifies approximate stationarity of the population problem, uniformly over a region, with an explicit dependence on the sample size and on the covering number of the region. Because the graph of the proximal map is linearly isomorphic to the graph of the subdifferential, it also bounds the Hausdorff distance between and (Theorem 4.5 of the paper, not part of this mission). The Bregman setting covers non-Euclidean geometries (an -setup) and losses that are only locally Lipschitz with polynomial growth. Theorem 4.2 is reusable on its own: it is a McDiarmid inequality for unbounded, light-tailed differences.
The paper's proofs are complete; nothing here is open. None of the statements has been formalized before. Mathlib has the Fréchet derivative, product measures, cumulant generating functions and convexity, but no Legendre functions, Bregman proximal maps or envelopes, and no McDiarmid inequality with data-dependent differences; the platform has McDiarmid only with constant differences.
The naive route, McDiarmid's inequality applied to , needs a bounded difference constant, and the stability estimate (4.1) gives only , which is unbounded unless the data are. The concentration step therefore needs a version of McDiarmid's inequality whose differences are random. A second obstacle is that the empirical objects are random sets: proving that the proximal points are single-valued, interior, and measurable in the sample is a step the paper takes for granted. Third, uniformity over comes through Lemma 4.3 in the mirror metric , not in the norm of .
The space is a finite-dimensional real normed space ; gradients are Fréchet derivatives, the dual norm is the operator norm, and is the second Fréchet derivative, a map . Extended-valued functions are pairs (domain, real values), so no extended-real arithmetic occurs. Proximal maps are sets of minimizers; envelopes are real infima, used only where Theorem 3.1 guarantees attainment. "With probability " is an outer-measure bound on the failure set under . The covering number is replaced by the size of an arbitrary finite -net fixed before the sample, and by for an arbitrary with integrable; both replacements are equivalent to the page. Hypotheses the paper uses without stating are explicit: , , nonempty and convex, measurable and integrable, closedness of and of , bounded below; the second display of the goal assumes and an invertible Hessian on . Theorem 4.1 is read, as its proof is, with and the proximal points at .
A pointwise version (fixed ), a version where the net may depend on the sample, a bound for one fixed , or the Euclidean case alone would each be a strictly weaker theorem and does not close the goal.
A complete development needs: Legendre-function theory (coercivity of , interiority of Bregman proximal points), Danskin-type differentiation of the envelope, measurability of argmin maps, the extended McDiarmid inequality, and a covering/union bound. The McDiarmid extension and the Bregman proximal-point lemmas are reusable well beyond this paper. Proofs of the milestones, sanity instances of (A1)–(A3), and intermediate lemmas from the paper's proofs are all welcome.
The state of a finite-dimensional quantum system is a density: a positive semidefinite matrix of trace one. Under coherent (Hamiltonian) control the evolution is unitary, , and preserves the eigenvalues of . Even with full unitary control, a state can therefore only be moved within its unitary orbit. A mixed state cannot be purified, and a pure state cannot be made mixed. Dissipation, modelled by Lindblad generators (Gorini–Kossakowski–Sudarshan 1976, Lindblad 1976), is what breaks these spectral invariants. Engineered dissipation is a standard tool for state preparation (Verstraete–Wolf–Cirac 2009).
This raises a basic control question: how much dissipation must be added to full unitary control before every state can be steered to every other state? Cai, Govindarajan and Junge (arXiv:2504.04883v2) answer it for qubits. One amplitude-damping jump and one dephasing operator, both acting on a single qubit, suffice.
Timeline.
Let be the space of qubits, with computational basis , . A superoperator is a linear map on -qubit matrices. Densities form the set .
For an operator , the Lindblad generator with rate is
For every , is a quantum channel.
Fix a resource set of operators with . The closed class is the smallest closed set of superoperators with three properties:
generates a Hörmander system if the real Lie algebra generated by the anti-Hermitian part of contains , the traceless anti-Hermitian matrices. A set of superoperators is transitive if for all some satisfies . The range of is .
On one qubit, , is the amplitude-damping jump, and keeps the diagonal of a matrix and deletes the rest. The replacer channel is , and .
If generates a Hörmander system on and
then
The goal asserts reachability only. It places no bound on time or on the number of compositions.
The result. Full unitary control alone cannot change the spectrum of a state. Theorem 2.12 shows that two dissipative resources acting on one qubit already remove every obstruction. This is close to optimal: Proposition 2.7 of the paper shows that self-adjoint jumps alone produce only unital channels, which fix the maximally mixed state, so at least one non-self-adjoint resource is necessary. The result also needs no convexity. The class contains genuine Markovian semigroups, their compositions and their limits, but no mixtures. The surrounding statements are reusable on their own:
Formalizing it. The paper's proof is short, but several steps are stated without detail: "by assumption", "using the conjugation trick and products", and Chow's theorem cited for a semigroup rather than a group. A formal proof fixes exactly what the closure (CL) contributes. It supplies the negative-time unitaries (milestone 1) and the conditional expectations and (milestones 4–6), none of which is of the form . No machine-checked proof of these statements is known (a search of the Prove2Me library in October 2026 found none). Mathlib has the matrix exponential, the operator norm on superoperators and Lie subalgebras. It has neither Chow's theorem nor the correspondence between Lie subalgebras and connected subgroups of .
The one hard step is milestone 1. (UN) supplies only the forward flows , , of the directions in the span of . The Hörmander condition is a statement about the Lie algebra they generate, while the class is a semigroup closed under limits. The naive argument applies the Lie-algebra/Lie-group correspondence directly, but that correspondence speaks about the group generated by the flows , . The class contains only nonnegative times and their compositions and limits, so the step from the generated group to the closed semigroup is exactly what has to be supplied.
The remaining milestones are explicit matrix analysis: exponentials of explicit superoperators on one qubit and their limits as , and register swaps. Milestone 7 has two halves. The inclusion is the construction. The inclusion requires every element of the closed class, limits included, to be positive and trace-preserving.
Carrier. The basis of is indexed by bit strings Fin k → Bool, with false . Operators are complex matrices on this index set. Superoperators are continuous -linear maps with the operator norm over the -operator norm on matrices. In finite dimension every norm gives the same topology, so closedness and limits do not depend on this choice. Exponentials are NormedSpace.exp on matrices and on superoperators. Milestones 3 and 4 are stated on matrices indexed by Fin 2, with basis order .
The class. is the intersection of all closed sets with (UN), (JU) and (CO). A formalization in which some class with these properties is merely assumed to exist would make the goal trivial (take all superoperators), and is ruled out. Likewise, the Hörmander hypothesis is containment of in the generated real Lie algebra, not in the span of .
Conventions committed to.
Infrastructure needed.
The first two are reusable well beyond this mission. Proofs of individual milestones, and of general lemmas on Lindblad semigroups, are welcome.
Product development is often organized as a search over prototypes: several candidate designs exist, each must be built or tested at a cost before its quality is known, and the firm wants to end up launching the best one without spending too much on testing. When each test reveals the true quality of a prototype, this is Pandora's box problem, solved by Weitzman (Weitzman 1979): attach to every box an index, its reservation price, open boxes in decreasing order of the index, and stop as soon as the best value found exceeds every remaining index.
In practice, tests are rarely perfect. Simulations, virtual prototypes, consumer panels and outsourced test platforms return a noisy measurement of a prototype's value, not the value itself. Bhaskaran and Erat (Bhaskaran and Erat 2025) ask what the optimal sequential testing policy is when each evaluation only yields a signal correlated with the true value. Extensions of Weitzman's model are known to be fragile: with learning across alternatives (Erat and Kavadias 2008) or with the option to select an alternative without inspecting it (Doval 2018), index policies stop being optimal. Theorem 1 of the paper shows that measurement noise is not such a perturbation: an index policy remains optimal once the indices are computed from the right distributions.
There are prototypes, . Prototype has a true value and, when evaluated, yields a measurement . The pair has a joint density on with , and different prototypes are independent. Evaluating prototype costs , paid once.
The firm sees only measurements. It evaluates prototypes one at a time, in any order and adaptively; it may stop at any time, including before any evaluation. On stopping it launches one of the evaluated prototypes, receiving its true value, or launches nothing and receives the outside option . Its net payoff is the value received minus the evaluation costs paid, and a policy is judged by its expected net payoff.
The paper's objects are:
the expected true value of prototype given the measurement ;
In the Lean development these are Model, Policy, run, netPayoff, Admissible, value, Q, g, V, B and fidelityPolicy in the namespace NoisyPrototyping.ReservationPolicy.
The fidelity-adjusted reservation price policy evaluates the prototypes in the order and, after the -th evaluation (), stops and accepts if (always at ), and otherwise evaluates prototype . The goal states that is admissible and that, for every admissible adaptive policy ,
Theorem 1 says that the qualitative structure of Weitzman's solution survives imperfect evaluation. The evaluation order is fixed in advance, by indices that depend only on each prototype's cost and on the joint law of its value and measurement; the stopping rule is a threshold rule applied to a monotone transform of the measurements. Everything the paper does afterwards rests on it: the Gaussian closed form of Theorem 2, the comparative statics of Propositions 1–3 in the fidelity of the test, the choice of fidelity in Propositions 4–6, and the pricing of an outside test platform in Propositions 7–8.
The result is proved on paper by reduction to Weitzman's theorem. Weitzman's theorem itself is neither proved nor posed on the platform (searched October 2026), so the formalization produces two things: a formal proof of optimality of Pandora's rule, in the version with recall, any order, free stopping and an outside option; and a formal account of the reduction from noisy to perfect evaluation, which the paper presents as two short claims.
The natural first idea is to declare that "the firm only cares about " and apply Weitzman directly. Two steps of that argument need work. First, the policies of the noisy problem see the measurements , which may carry more information than when is not injective, so the class of policies in is richer than in ; showing that this extra information is useless requires the independence of prototypes and a conditioning argument for adaptive, history-dependent stopping. Second, the replacement of by in the payoff must be justified for an adaptive launching decision, not for a fixed prototype. Weitzman's theorem itself is not in Mathlib, and its optimality claim ranges over every adaptive policy, so it cannot be checked by comparing finitely many candidate rules.
Prototypes are indexed by Fin N from ; the paper's reordering is a bijection σ : Fin N ≃ Fin N along which the prices are non-increasing (ties in any order), and the paper's is R (σ n). The law of is a probability measure on ; the outcome of all prototypes has the product law, which encodes independence. The goal and Claims 1–2 assume this law has a measurable density . A history records evaluated prototypes and their measurements only; a policy maps histories to evaluate , launch or stop with nothing; each prototype is evaluated at most once, and illegal decisions end the run with nothing. A policy is admissible when the evaluation order and the final decision are measurable events and the net payoff is integrable; values are Bochner integrals of the net payoff.
Disclosed readings: independence across prototypes; ; ; formula (1) with in the denominator (the page prints , which would not give a conditional expectation); as the law of (formula (2) as printed lacks a Jacobian factor). The proof's simplifying assumption that is increasing onto is not made.
The statement admits trivializing encodings, and they are excluded: policies cannot see true values (that would make the problem full-information, where is not optimal); is the explicit formula (1), not a conditional expectation by definition; enters as the hypothesis that it is the least root, never through a choice function; and competitors are compared only when admissible, while the admissibility of is part of the conclusion.
A complete development needs: the conditional expectation of a coordinate under a joint density; conditioning arguments for adaptive policies on a product space; and Weitzman's theorem. The last two are reusable beyond this mission, for any search or bandit model with independent alternatives. Proofs of the milestones in any order are welcome, and a proof of the Weitzman milestone is the most reusable contribution.
An agent who maximizes an expected sum of rewards over time is time-inconsistent when the plan that is optimal today stops being optimal tomorrow. This happens as soon as discounting is not exponential: with hyperbolic or quasi-hyperbolic discounting, a reward far in the future is weighed differently at time 0 and at time 1, and the agent's future selves want to revise today's plan. Strotz (Strotz 1955) proposed to treat the problem as a game between the current self and all future selves and to look for a strategy that no self wants to deviate from: an equilibrium. Non-exponential discounting is documented in experimental economics (Laibson 1997), and equilibrium controls are the standard solution concept for such problems in mathematical finance and stochastic control (Björk, Khapko, Murgoci 2017).
The basic question is whether an equilibrium exists. For a Markov decision process on a finite state space with a general action set, Huang and Zhou proved existence when the actions available in each state form a closed convex set and the reward is concave in the action. Without convexity there need not be an equilibrium among deterministic feedback controls. Bayraktar, Huang, Wang and Zhou show that existence is restored for relaxed (randomized) controls, under only Lipschitz continuity and a geometric condition on the action space. This mission formalizes their discrete-time result.
The action space is a compact set with positive Lebesgue measure , and the state space is . Each action has a transition matrix , with -th row . A reward function depends on the time difference , the state and the action.
A relaxed feedback control is a map : in state the agent samples an action from the probability measure . The set of relaxed controls is . The chain then moves with the averaged matrix , and the value is
For , the concatenation uses at time and afterwards. A control is a relaxed equilibrium if
The paper also uses an entropy-regularized problem. A control is regular () if each has a density on whose differential entropy is finite. For and a discount function , the regularized value adds to the reward at time . A regular control is a regular relaxed equilibrium if no regular deviation improves . The Gibbs density
defines the map , where is the continuation value from time .
The assumptions are the following.
Under Assumptions 2.1–2.3, there exists with
The statement fixes no constants and assumes no convexity.
The result. Theorem 2.2 removes the convexity and concavity assumptions of the earlier existence theorem for discrete-time time-inconsistent MDPs. Its price is randomization. The action space may be a finite union of polytopes, for example, and the reward need not be concave in the action. Theorem 2.1 is of independent interest for reinforcement learning, where entropy-regularized objectives are the standard way to encourage exploration (Ziebart et al. 2008). With non-exponential discounting, the theorem guarantees a randomized policy that all future selves uphold. The regularized equilibria are fixed points of a single-valued map, and the paper (Remark 2.6) points to them as a computational route to relaxed equilibria.
The formalization. The results are proved in the paper. None of them has a machine-checked proof, and this mission produces the first. Along the way it requires a formal treatment of relaxed controls as measure-valued maps, of the differential entropy of densities on a subset of , and of Gibbs variational principles for such densities.
The obvious route to existence is a fixed-point theorem for the best-response correspondence on deterministic controls. It needs convex values, hence a convex action set and a concave reward, and both are absent here. Relaxing to measures restores convexity of each best-response set. However, the unregularized best response is set-valued on an infinite-dimensional space, and the value depends nonlinearly on through the whole future of the chain. The regularized problem has a single-valued best response, but a fixed point needs a uniform bound on entropies of Gibbs densities. That bound must grow only logarithmically in (otherwise no ball is invariant) and stay controlled as . The geometric Assumption 2.3 enters exactly there, and again in the limit, where Gibbs measures must concentrate on maximizers that a cusp or isolated point of would otherwise hide.
Actions are points of EuclideanSpace ℝ (Fin ℓ) with . The state space is Fin d, value vectors are Fin d → ℝ, and every norm on (and ) is Euclidean. A control is a family of measures on :
Expected values are infinite sums through products of the averaged transition matrices (Remark 2.1), and the concatenation is the control sequence . The p. 6 decomposition is therefore a theorem, not a definition. Weak convergence is tested against bounded continuous functions on . Constants that the paper says depend on are quantified before , , , and .
Disclosed conventions:
A trivializing formalization is ruled out. Equilibria quantify over all relaxed deviations, Dirac controls included. is computed from the process, not from the one-step formula. The hypotheses of the goal are satisfiable: a verified instance with and exists in the development.
Needed infrastructure, reusable beyond this mission:
Proofs of any milestone and of reusable lemmas are welcome.
Firms disclose information to capital markets, but the same disclosures are read by other parties with a stake in the firm's cash flows. Labor unions are a leading example: anticipated good performance is associated with more aggressive union demands (evidence cited in Arya and Ramanan, p. 11: Bova 2013; Chung et al. 2016; Aobdia and Cheng 2018). A firm's choice of information system, that is, whether to gather information at all, whether to commit to publishing it, or whether to keep discretion over what to release, therefore trades off stock-market valuation against the union's bargaining posture.
Arya and Ramanan (Endogenizing Discretion in Disclosures, Management Science; authors' manuscript SSRN 3935991) make this choice endogenous. The ex post discretionary branch builds on the single-threshold disclosure equilibrium of Dye (1985); the ex ante branch relates to information design in the sense of Kamenica and Gentzkow (2011). The paper's main result says which information system the firm's CEO installs as a function of the union's strength.
A firm's cash flow is uniform on . The CEO sells her shares at an interim date and maximizes the stock price . A union observes every public signal; bargaining costs it and, if undertaken, transfers an expected fraction of the cash flow (in the paper , a success probability times a share).
The CEO first chooses an information system :
The union bargains if , does not if , and mixes with any probability at equality (Lemma 1); the price is (Lemma 2). Throughout, .
Under , write for the value of silence and for the union's bargaining probability after silence. The price of a disclosed is for and for , and the silence price is . A -subgame equilibrium is a pair such that is a Lemma 1 best response to , and is the Bayes posterior mean of given silence when the informed CEO withholds exactly the with below the silence price. The CEO's ex ante objective is the expected price , written , , and .
With :
Concretely: (a) for , and at every -subgame equilibrium; (b) for , some equilibrium has , and every equilibrium does when ; (c) for , , some equilibrium has , and every equilibrium with does.
The result says that discretion over disclosure, usually viewed as costly because the market discounts silence, can be the optimal design when a third party reacts to disclosures. The mechanism is that the CEO's ex post wish to inflate valuation lowers the value of silence, and a value of silence below the bargaining threshold disciplines the union. Against a weak union no information is best; against a strong one, committed public disclosure is best because it reveals all low cash flows that deter bargaining.
The result is proved in the paper by explicit computation. To our knowledge none of it is machine-checked. Formalizing it requires solving the Bayes fixed-point equations (1)–(4) for each regime, evaluating the expected prices, and comparing them across the parameter space; it also makes precise a point the paper passes over, namely that the -subgame equilibrium is not unique near .
The value of silence is defined by a fixed point: the nondisclosure set depends on the silence price, which depends on the value of silence, which depends on the nondisclosure set. The set is a union of two intervals whose endpoints move with , and the regime changes at four cutoffs, with a mixed-strategy regime in which the union's indifference pins and the fixed point is solved for instead. Each regime yields a quadratic whose relevant root must be shown to satisfy the regime's inequalities, with square roots whose radicands must be shown nonnegative.
The comparison in Proposition 9 then compares piecewise closed forms across these regimes. The first idea, that discretion is optimal exactly when the paper's selected equilibrium has , does not settle the statement for every equilibrium: just below there are mixed equilibria at which discretion beats public disclosure, and at there is a pure equilibrium at which it does not.
ℝ. The uniform prior is encoded by Lebesgue integrals over subsets of divided by ; no probability space is introduced. The parameter enters only as . The standing assumptions , , , are a single predicate Standing carried by every statement. Under it, the weak-union part (a) is vacuous for , as in the paper.Digital-goods platforms (video, music, e-books, software) sell access in two ways at once: subscriptions, which give unlimited use of a set of items for a period, and rentals, which charge per use. A platform with a large catalogue could offer many subscription sets at different fees, but most platforms offer a single all-inclusive subscription. Alaei, Makhdoumi and Malekian (Optimal Subscription Planning for Digital Goods, Operations Research 2023; working paper SSRN 3476296) ask when that practice is revenue-optimal. Users differ not only in how they value items but in how often they consume (their usage rate), and it is this second dimension that makes the question nontrivial: a frequent user values unlimited access more, even with the same per-use tastes.
The paper's first main result, Theorem 2, gives a condition on the value distributions under which a single grand subscription (all items, one fee), together with the rental prices, earns as much as any menu of subscription sets, whatever the masses and usage rates of the user types.
There are user types and item types . On a probability space, is the value of one watch of item to a user of type and is the value of an outside option. Type has mass with , and watches at usage rate over a period of length .
A subscription planning (Definition 1) is a pair : a fee for each subscription set , and a rental price for each item. A user subscribed to gets utility from an item , from an item , and from the outside option, and takes the best of these on each watch. Two per-watch quantities summarise this choice:
By Proposition 2, for fixed the platform chooses fees and an assignment to maximise the revenue
subject to the incentive constraints for all and . Such with is a feasible planning. In the grand subscription only is offered, at a fee , and each type subscribes or not according to its incentive.
Condition 2 (p. 12) requires, for every and ,
The first part says the grand set has the best trade-off between subscription gain and lost rentals; the second says all types rank sets by the same relative gain.
If satisfies Condition 2, then for all and there are a fee and incentive-compatible subscription decisions such that
Since the grand subscription is itself feasible, it achieves the optimal revenue.
In attack order:
The result separates what a menu of subscription sets can do from what the grand subscription does. Under Condition 2, which holds for instance for values with item-dependent Gumbel distributions (Example 2 of the paper), a platform loses nothing by offering a single subscription at a single fee, whatever the distribution of usage rates. The optimal fee is then one of candidates, , so the platform's problem collapses from a menu over sets to a one-dimensional choice.
The theorem has a published proof; this mission formalizes it. No part of it is machine-checked yet. A formal development would also settle the boundary cases the printed argument passes over: ties in the per-watch choice, ties among usage-weighted gains, and types with zero subscription gain.
The obvious argument is the single-type one: with one user type, Lemma 2 shows the grand set dominates. With several types, a menu can screen them by usage rate: frequent users buy large sets at high fees, infrequent users buy small sets or rent. The grand subscription cannot screen, and any single grand fee either excludes infrequent users (losing their fees) or undercharges frequent ones. So no single grand fee can be compared with a screening menu type by type. Any comparison has to cover rental revenue as well as fees: a menu that sells small sets keeps collecting rentals from the types it screens, while the grand subscription collects rentals only from non-subscribers. The menu's structure is also not explicit: the sets chosen by different types need not be nested, and without a common ranking of sets across types (part 2 of Condition 2) the menu's revenue does not decompose along the order of usage rates at all.
All statements live in the namespace SubscriptionPlanning.GrandOptimal. User types are Fin n, item types Fin m, sets Finset (Fin m), and the values are real random variables on a probability space , measurable and integrable. The model bundles , , and (the paper's standing assumptions, p. 4). The values may have any joint law; the paper draws them independently, and nothing in Theorem 2 uses independence.
Committed conventions, each disclosed in the item statements:
Trivializing readings. The goal is not "some grand fee beats some planning"; it is not stated with feasibility lacking any incentive constraint; and it does not fix all types to subscribe or let ignore incentives. The goal quantifies the fee before every feasible planning, and must respect each type's incentive.
Not posed. Theorem 2 opens with "if and only if", but only the first bullet (sufficiency) is posed. The second bullet (necessity) is false as printed. With a single user type the grand subscription is always optimal by Lemmas 2 and 5, yet part 1 of Condition 2 can fail. Theorem 3, Propositions 1–3 and Lemma 6 are also out of scope.
Infrastructure and contributions. A complete development needs expectations of maxima of finitely many integrable random variables, measurability of the first-maximizer choice, and finite telescoping sums; the per-watch choice lemmas (Lemmas 2 and 5) are reusable for any model of menus with per-use prices. Proofs of the milestones, alternative arguments for the goal, and sanity examples (e.g. Gumbel values) are welcome.