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?
In contextual stochastic optimization a decision is chosen after observing features , and the ideal policy solves, for each feature value,
for a cost and an uncertain outcome (inventory demand, asset returns). Kallus and Mao (arXiv:2008.07473, Management Science 2023, doi:10.1287/mnsc.2022.4458) estimate such policies with stochastic optimization forests: random forests whose trees are grown to minimize the downstream decision cost rather than the prediction error of .
The bottleneck is choosing a split. The natural rule, the oracle criterion, re-solves an optimization problem for every candidate split of every node, which is too expensive inside a forest. The paper replaces it by an approximate risk criterion that needs only a gradient per child and one Hessian per parent, and justifies the replacement by a second-order perturbation analysis. This mission formalizes that justification.
Let be the law of on and let be the regression cost. For a region with write
A node of a tree is a region ; a candidate split is a partition into disjoint measurable pieces. Abbreviate , for ; note . Let be the unique minimizer of , the gradient and the Hessian in , and the diameter of .
The oracle criterion (eq. (8)) is the optimal cost after the split,
and the approximate risk criterion (eq. (13)) is
For the norm (70) is , and .
Assume is for every ; , , are -Lipschitz in uniformly in ; and at an anchor point the function has a unique, nondegenerate, level-bounded minimizer. Then for every there is such that every split of a region satisfying the paper's conditions 1–3 for obeys
Since does not depend on the split, the two criteria rank splits of a small node alike.
Theorem 2 is the guarantee behind the paper's algorithm: the criterion that is cheap to evaluate agrees with the expensive oracle criterion to second order in the node size, so a forest grown with it splits nodes the way a forest grown with the oracle would, while inverting only one Hessian per node. The same perturbation analysis drives the approximate solution criterion (Theorem 3) and, with constraints, Theorems 4 and 6; the unconstrained milestones here (Corollary 1, Theorem 9) are the reusable core.
The result is proved in the paper; nothing here is open. No part of it has a machine-checked proof. The mission produces a formal model of region-averaged costs, a quantitative second-order perturbation theory for unconstrained minimization (Corollary 1 and Theorem 9, which are standard in the Bonnans–Shapiro theory but absent from Mathlib), and a version of Theorem 2 with its limit, uniformity and error scale made explicit.
The expansions are about global minima, and Taylor's theorem only controls local behaviour. The obvious argument expands around and minimizes the quadratic model; it fails when the perturbation creates a competing minimum far from , which a small does not rule out when is flat at infinity. Theorem 9 is true only because the minimizer is unique along the whole path , , which keeps it from jumping.
The second obstacle is uniformity. Theorem 9 is stated for a fixed , but in Theorem 2 the base function is the average over and moves as shrinks. The little- must hold uniformly over base functions near the limit ; Milestone 7 isolates this step.
Finally, a literal reading of the printed bound is weak: both and are , so the printed bound holds without any second-order cancellation whenever . The content is the factor .
Features are EuclideanSpace ℝ (Fin p), decisions EuclideanSpace ℝ (Fin d) (unconstrained, §2). The law is a probability measure. The regression cost is the primitive; and enter only through it (tower property). Gradients are Mathlib's gradient; the Hessian is the derivative of the gradient, and the inverse Hessian is ContinuousLinearMap.inverse, always paired with a positive-definiteness hypothesis so that it is a true inverse. Minima are real infima, and every statement assumes or derives attainment. Little- claims are – statements; "" bounds the value, the gradient and the Hessian pointwise, with the Hessian in operator norm (weaker than the paper's Frobenius norm, so the statements are stronger).
Choices made where the page is silent or misprinted, all disclosed in the items:
The bound without the factor , a reading of condition 3 that forces at the optimum, a sup-norm defined by a supremum that is for unbounded functions, and a radius chosen after the regions would each make the goal trivial; the statements exclude all four.
Infrastructure needed: differentiation of set integrals with integrands (Mathlib's dominated-derivative lemmas suffice), consistency of minimizers under uniform perturbation, local strong convexity from a positive definite Hessian, and the second-order Taylor bound with remainder. The perturbation results (Milestones 4–7) are reusable for any unconstrained parametric minimization. Proofs of any milestone, and of the goal from Milestones 1, 3 and 7, are welcome.
Online marketplaces decide which products to show first. A promotion puts a seller's product in front of consumers who will not search further, so it changes both the seller's sales and the surplus of the consumers who see it. A seller who is uncertain about the market sets prices from the sales they observe, and the platform's promotion decisions shape what those sales reveal. Gur, Macnamara, Morgenstern and Saban (arXiv:1911.09256, Management Science 2023) study how a platform that maximizes consumer surplus should combine an initial disclosure of information with a dynamic promotion policy when the seller learns and prices myopically.
The question joins two literatures. Bayesian persuasion (Kamenica and Gentzkow 2011) describes the value of a one-shot signal by the concave envelope of a value function. Learning-and-earning in dynamic pricing (Harrison, Keskin and Zeevi 2012) studies how a seller's beliefs converge when sales are informative. The paper's central result says what the platform can achieve in the long run when it controls both the starting point and the drift of the seller's belief.
A fraction of consumers is impatient, with ; the platform observes and the seller holds the prior . The seller sets prices in a compact interval containing . In each period one consumer arrives. A patient consumer buys with probability . An impatient consumer buys with probability if the seller is promoted and with probability otherwise. Consumer surplus is , or in the three cases. The purchase probabilities are decreasing and Lipschitz, the revenues and are strictly concave, , and are decreasing and Lipschitz.
Before the first period the platform commits to a signaling mechanism , a distribution over signals for each value of , and to a promotion policy , where is the probability of promoting the seller at price after the history of the signal, past prices and past sales. The seller updates a belief about by Bayes' rule and follows a myopic Bayesian pricing policy : in each period they choose a price that maximizes the current expected revenue, breaking ties in favour of the current consumer surplus. The platform's payoff is the expected total consumer surplus .
A promotion policy is confounding if it keeps the seller's belief constant, which requires the probability of a sale to be the same under and at the price the seller sets. Let be the largest one-period expected consumer surplus of a confounding policy at belief , and let be its concavification, the smallest concave function above on .
For every prior ,
and for every some signal and confounding policy achieve average surplus exactly . The goal is stated as a uniform upper bound for large together with exact attainment at every .
The theorem identifies the long-run value of the platform's joint design problem with a static object. The platform's levers act on the belief process: the signal sets its starting point and the promotion policy its drift. The theorem says that, in the long run, the best use of the second lever is to stop the drift. Information is then disclosed only once, as in a persuasion problem with value function . A consequence is that a policy maximizing the current surplus in every period, which lets the seller learn , is generally not long-run optimal. The paper quantifies the gap on its uniform-willingness-to-pay example. The characterization is also the basis of the paper's later results on approximately optimal policies without signals and on equilibria with a forward-looking seller.
The result is proved in the paper; no part of it has been machine-checked. The formalization produces a finite, measure-free encoding of a dynamic Bayesian game with history-dependent policies, reusable for other learning-and-earning models, and makes the uniformity of every constant explicit.
The obvious argument treats each period separately: the surplus of a period is at most , and by Jensen's inequality the average is at most . This bound is too weak, because exceeds at interior beliefs. The proof must show that periods whose surplus exceeds by cannot recur often. This requires two quantitative statements that hold uniformly over all beliefs, policies and signals: each such period reveals information about by a fixed amount, and beliefs then concentrate exponentially fast. The surplus gained before concentration must also be controlled near the degenerate beliefs. The myopic tie-break makes the one-period problems discontinuous in the policy, so the compactness arguments behind need care.
The game is encoded without measure theory. The state is a Boolean, the signal set is Fin n for an arbitrary , pricing policies are deterministic, and the expectation is a finite sum over the state, the signal and the sale outcomes, with path probabilities given by products of the sale probabilities. Beliefs follow Bayes' rule, and a probability-zero observation leaves the belief unchanged. Definitions 1–3 quantify over histories whose recorded prices lie in . The tie-break of Definition 1 uses the current expected surplus under the seller's belief. and are real suprema over one-period rules and myopic responses. is the supremum over the convex hull of the hypograph restricted to and is used only on . The standing assumptions add and , since these are probabilities. Only policies admitting a myopic response are considered, as the paper presumes. Constants in Lemmas 2 and 3 and in the finite-horizon bound are chosen before the horizon, the signal and the policies.
is the one-period version of (10) under myopic pricing with the tie-break, not the static program (11). The goal quantifies over all history-dependent promotion policies, all finite signals and all myopic pricing policies, so it cannot be trivialized by restricting the policy class or stating only the upper bound. The attainment conjunct requires a confounding policy with a myopic response at every history.
The paper asserts that is attained for every . Under the tie-break the supremum defining can fail to be attained, so the corresponding milestone states only the repetition step. Proposition 1 is stated with the prior fixed before the policies are chosen.
A complete development needs Bayesian updating on finite trees, the martingale property and Jensen's inequality for finite mixtures, concave envelopes on an interval and their attainment by two-point splits, Berge-type continuity of constrained one-period optima, and exponential concentration of posteriors under separated likelihoods. The last three are reusable beyond this mission. Contributions to any milestone, and to general lemmas on concave envelopes and posterior concentration, are welcome.
Retail inventory records are often wrong. A store's system may report units on the shelf that are not there (phantom inventory), so the replenishment system never reorders and the product silently stops selling. Audits fix such errors but are expensive, so a retailer wants to decide which store–SKU pairs to audit from sales data alone. The classical way, studying each pair's sales history over a long period, needs time-homogeneous data that rarely exists.
Farias, Li and Peng (arXiv:2006.13126v3, Manufacturing & Service Operations Management, 2024) instead use a single cross-sectional snapshot of sales across stores and SKUs. Expected demand is modelled as a low-rank matrix, anomalies corrupt a random subset of entries, and only some entries are observed. The paper proposes the entrywise (EW) algorithm and proves that its expected decision cost approaches that of an oracle knowing the model, at rate . A matching lower bound (Proposition 1) is also proved. The paper evaluates the method on synthetic data and on real data from a consumer goods retailer.
An instance has an expected-demand matrix with , rank and SVD with singular values and . It also has an anomaly model , which is a family of laws on indexed by a parameter and a mean level . The remaining data are a true parameter , an anomaly probability , an observation probability , and costs (flagging a normal entry) and (missing an anomaly). Independently for every entry:
Assumptions (§2):
The oracle knows and . It computes the posterior , where and . It flags iff . The EW algorithm runs four steps:
The cost of decisions is
The constants and and the sparsity constant depend only on , , and the regularity constant . The statement asserts the paper's rate with polynomial dependence on the model parameters. It does not fix the polynomial, so a sharper analysis still proves it.
Theorem 1 says that the value of cross-sectional data grows with the number of stores and SKUs. A retailer that can only see one snapshot does nearly as well as one that knows the demand matrix and the anomaly law exactly. With Proposition 1, the rate is optimal up to the logarithmic factor. Theorem 2 is, per the authors, the first entrywise guarantee for matrix completion under Poisson (more generally sub-exponential) noise, and it is reusable outside inventory problems.
The results are proved on paper: Theorem 1 by a proof sketch in §5.1 plus Appendix B, and Theorem 2 in Appendix A, which builds on a cited entrywise eigenvector perturbation theorem of Abbe et al. None of this is formalized. A machine-checked proof would also settle the constants and conventions that the paper leaves implicit. These include the dimension restriction in Lemma 17, the unspecified constant in Lemma 3, the form of the sparsity assumption used in the proof of Theorem 2, and the closed range of in .
The obvious argument plugs consistent estimates of and into the Bayes rule. It breaks at the first step: a Frobenius-norm bound for , which is what standard matrix completion gives, does not control any single . An entrywise bound is needed, under heavy-tailed (sub-exponential, not sub-Gaussian) noise, and with the anomalies corrupting the mean by the unknown factor . The second step inverts the moment map . Closeness of moments yields closeness of parameters only through a quantitative inverse-function argument, which needs the regularity conditions of Lemma 1. A third subtlety is that is a ratio whose denominator can be tiny. The error bound of Lemma 3 therefore degrades on rare sales values, and Theorem 1 averages this over the law of .
One definitions module, InventoryAnomaly.EW.Model, holds the instance, the product sampling law over observedanomalous per entry, the estimators, the costs and four predicates:
Model: §2's assumptions;SparsityMax: the sparsity condition as read in the proof of Theorem 2, p. 41;Regular: Lemma 1's conditions;CostBound: costs in .The sub-exponential norm is the published HighDimProb.Concentration.subexponentialNorm.
Conventions:
The algorithm's selections are universally quantified together with their defining properties. Neither may be replaced by unconstrained functions. The cost of must use , not . The goal must keep the explicit rate and the full probability model, without assuming Theorem 2's event.
Not formalized: Proposition 1 (the lower bound), Appendix E (the TPR/FPR-constrained variant), the cited Lemmas 6–7, and the internal Lemmas 9–13 and Propositions 2–3 of Appendix A.
Useful infrastructure includes entrywise singular-subspace perturbation bounds, Bernstein's inequality for bounded independent sums, and Orlicz-norm bounds for Poisson variables. All three are reusable beyond this mission. Proofs of individual milestones are welcome, especially Lemmas 8, 14, 17 and 19 and Step 4, which are self-contained.
Several problems in machine learning and game theory are optimization problems over probability measures. Training a wide two-layer neural network can be viewed as minimizing a functional of the distribution of the network's parameters (Mei, Montanari, Nguyen, PNAS 2018; Hu, Ren, Šiška, Szpruch, arXiv:1905.07769). Adding a relative-entropy penalty makes the problem strictly convex in the density and connects its minimizers to the invariant measures of Langevin-type diffusions, the mean-field Langevin dynamics. The first-order condition for the unconstrained problem is Hu et al., Proposition 2.4.
Conforti, Kazeykina and Ren (arXiv:2004.02457v2) add a random environment: a variable with a fixed law that every player observes, such as the time index in a dynamic game or a shared signal. The strategies are then probability measures on whose -marginal is prescribed. Their Theorem 3.1 extends the first-order condition to this constrained problem. The introduction names it "one of our main contributions": it gives the necessary condition for Nash equilibria of games on a random environment (Corollary 3.3), and it identifies the invariant measure of the mean-field Langevin system studied in the rest of the paper.
Let be a Polish space with a probability measure , and let . Write and . The strategy set is
the probability measures on with finite -th moment and -marginal . By disintegration, .
A function has a linear functional derivative if for all
Assumption 2.1 asks that have such a derivative, that and be continuous for the -Wasserstein distance , that be continuously differentiable in , and that .
The regularizer is the relative entropy with respect to : if has density with respect to , then , and otherwise. For the objective is
If , then has a density which, for -a.e. , is positive with differentiable and
Conversely, if is also convex on , every satisfying (3.1) minimizes over . The goal states both directions, as printed.
Theorem 3.1 says that each fibre of an entropy-regularized minimizer is a Gibbs measure, . In the paper this yields the Nash-equilibrium condition (3.2) for -player games on a random environment, the uniqueness of equilibria under a monotonicity condition (Corollary 3.4), and the identification of the stationary measures of the mean-field Langevin system (2.2) with these equilibria, the basis of the convergence results (Theorems 3.8–3.12). For a one-player problem it is the optimality condition behind gradient-descent training of mean-field neural networks with an environment variable.
The result is proved in the paper; it is not formalized anywhere known. The mission produces the first machine-checked first-order condition for optimization over probability measures, with or without a marginal constraint, and the supporting objects: the strategy set , the linear functional derivative, and relative entropy with respect to the infinite reference measure . The unconstrained case ( a point) is a special case.
The sufficiency direction is two convexity inequalities and a cancellation of the -dependent constants, which uses the common marginal . The necessity direction is harder. The first variation of at gives only an inequality (5.1) in the directions with , and the entropy's difference quotient is not dominated where is small, so the limit requires a one-sided Fatou argument. The inequality (5.1) is not yet a pointwise equation. Converting it into " is constant" needs admissible competitors with bounded density relative to , built fibre by fibre in , and these only reach the support of . Ruling out zeros of (Step 3) needs a separate competitor that charges a set where vanishes. Finally (3.1) concerns a smooth version of the density, which has to be produced from an almost-everywhere identity. The obvious idea of differentiating along for a signed perturbation fails: such perturbations leave unless they preserve positivity and the -marginal.
is EuclideanSpace ℝ (Fin d) with Lebesgue measure; is a complete separable metric space with its Borel -algebra (a Polish space with a fixed compatible metric, needed to state moments and ); carries the max product metric, and in the growth bound is the distance to a base point , with and fixed once for all . is the coupling infimum over this metric, valued in , and continuity is the – notion on . and are functions on all measures of which only the values on matter; is part of the data and the theorem holds for every derivative satisfying (2.1). The definition of the derivative makes explicit what (2.1) presupposes: joint measurability in and integrability in . Mixtures are for , and convexity of is along these mixtures. and take values in , with off absolute continuity. (3.1) is required of some measurable version of the density, for -a.e. and every , together with positivity and differentiability of .
The Lean logarithm satisfies , a non-integrable Bochner integral is , and the gradient of a non-differentiable function is . These would trivialize the statements, so (3.1) demands differentiability, and the milestones that integrate assert integrability and that does not charge , which is what the paper's convention encodes.
A complete development needs: mixtures and moments of measures in ; -convergence of mixtures; dominated convergence along mixtures; the entropy of a mixture and its one-sided derivative; disintegration with respect to the -marginal; and the passage from an a.e. identity to a smooth version of the density. The mixture, moment and entropy lemmas are reusable for any mean-field optimization problem. Contributions of any of these intermediate results, and of proofs of the milestones in any order, are welcome.
Large online marketplaces are hybrid platforms: they host third-party sellers and also sell their own products. Running the marketplace gives the platform access to sellers' sales data, and it can use that data to identify successful products and launch imitations of its own. The practice is colloquially called "Sherlocking". It has drawn regulatory attention: the European Commission's case against Amazon over the use of non-public seller data, and proposals to ban platforms from using such data or from competing with their own sellers at all.
Choi, Kim and Mukherjee (CESifo WP 10769 / SSRN 4643950, 2023; Management Science, 2025, doi:10.1287/mnsc.2024.05215) study the problem as a tension between the platform's fee, its entry decision and its information policy. The threat of imitation discourages sellers from joining, so a platform would like to commit not to imitate too aggressively. Commitment to an entry policy is rarely credible, but commitment to a data policy (what the product division is allowed to learn about a seller) is something a platform can build into its organization. The paper asks when the second kind of commitment is as good as the first.
A seller decides whether to join a marketplace run by a platform. Time has two periods of lengths and . The platform posts a referral fee , a share of the seller's profit. The seller's type , his profit per unit time as a monopolist, is uniform on and known only to him; entry costs him . Assumption 1 is .
If the seller enters, the platform collects in the first period. At the start of the second period it may imitate at cost , taking the whole second-period profit ; otherwise it collects . If the platform enters with probability , the entering seller's expected payoff is . Two cutoffs organize the analysis:
The seller enters against a platform that never imitates iff ; the platform gains from imitating type iff .
Full commitment. If the platform could commit to an entry probability for each type, its optimal policy is to stay out on and to enter on with the largest probability that keeps the seller willing to enter,
Its value is , and denotes a fee maximizing on . The resulting entry pattern is the full commitment outcome.
Information policy. Without commitment, the platform chooses an information policy: a set of realizations and a signal , a probability distribution on for each type. Its product division sees only the realization and then decides whether to imitate, in its own interest. The seller anticipates this. The solution concept is weak perfect Bayesian equilibrium. The full commitment outcome is implementable by an information policy if some signal has an equilibrium in which exactly the types in enter and the platform imitates type with probability on and below.
Under the binary signal (3), which reports with probability for and otherwise, the platform obeys the recommendation "stay out" iff
For a maximizer of on , the full commitment outcome at is implementable by an information policy if and only if (OC0) holds at , which is equivalent to
Proposition 3 gives a checkable condition under which information design substitutes for commitment to entry. When (4) holds, the platform obtains its full-commitment profit by restricting what its product division learns, and the seller faces the same entry threat as under full commitment. When (4) fails, the paper's Proposition 4 shows the platform must distort the outcome by excluding an interval of types. The comparison underlies the paper's policy conclusions about bans on data use and on imitation.
The result is proved in the paper; nothing in this mission is open mathematically. What the mission adds is a machine-checked development of a small information-design model: a formal revelation principle for this game (Lemma 1), with an equilibrium notion that handles a continuum of signal realizations, and a formal check that the integral conditions are equivalent. No part of the paper has been formalized before, to our knowledge.
The sufficiency direction is a computation with signal (3). The necessity direction is not: implementability quantifies over every signal space and every equilibrium, so (OC0), which is a property of one specific binary signal, has to be derived from an arbitrary equilibrium. The naive route of conditioning on each realization fails for a continuum of realizations, where conditional expectations are defined only almost everywhere and off-path behaviour is unconstrained. Separately, the goal is stated at the maximizer , and nothing in the hypotheses says directly that lies in the non-degenerate range , where some type enters.
Everything is real-valued, in the namespace Sherlocking.InfoPolicy, with a single definitions module.
X : Type with a σ-algebra. Platform strategies are measurable maps , the probability of imitating after each realization.Implementability is never defined through (OC0) or through signal (3). It quantifies over all realization spaces, signals, strategies and entry sets, under the full equilibrium predicate; a definition that fixed the signal would make the necessity direction trivial.
A complete development needs interval and set integrals of bounded functions, measurability of kernels and parametric integrals, and the Giry monad on Bool, all available in Mathlib. The binary revelation argument is reusable for other sender–receiver models with a binary action. Proofs of any milestone are welcome, as are alternative proofs of Lemma 1.
Many decision problems in operations research end in a linear optimization over a finite set of alternatives whose objective coefficients are random: the longest path in a project network with random activity durations, a maximum-weight assignment or spanning tree with random weights, the best item in a ranking with random utilities. The quantity of interest is the expected optimal value , where . In practice the one-dimensional distributions of the coefficients can be estimated, while their dependence structure usually cannot. The marginal distribution model therefore asks for the largest expected optimal value over all joint distributions consistent with the given marginals, a distributionally robust bound that does not assume independence.
Chen, Ma, Natarajan, Simchi-Levi and Yan (Operations Research, 2022) study this bound for an arbitrary finite feasible set and arbitrary marginals.
Timeline. Meilijson and Nádas (1979) gave a convex formulation of the tight upper bound on the expected completion time of a PERT network when only the marginal distributions of the activity times are known. Bertsimas, Natarajan and Teo (2004) studied the analogous bound for 0–1 problems under marginal moment information. Natarajan, Song and Teo (Management Science 55(3), 2009) gave a concave maximization formula for the marginal distribution model when consists of integer points and the marginals are absolutely continuous. The paper of this mission removes both restrictions: is any finite point set, the marginals are arbitrary (discrete marginals allowed), and the bound is cast in Lagrangian primal and dual forms.
Fix , a nonempty finite set , and probability measures on . Write for the coordinate projections of .
The value to be computed is
The Lean development names these objects proj, Z, frechetClass, couplings, margMeasure (), conj (the inner maximum of ), lagrangian, quantile and quantileForm (the objective of (8)), all in MarginalDRO.Lagrange.
For marginals with finite variance and a nonempty finite , with every optimum attained,
The result. Theorem 2 turns an optimization over joint distributions on , an infinite-dimensional problem, into a saddle problem over probability vectors on and univariate functions on the finite sets . The dual form gives upper bounds on from any choice of prices , and the primal form gives a worst-case joint distribution. The paper builds on it a compact reformulation (its §4) whenever has a tractable description, and applications to appointment scheduling, robust maximum flow, ranking and project scheduling. Theorem 3 makes the primal side explicit as a concave program in the quantile functions, which holds for discrete marginals as well as continuous ones.
Formalizing it. The results are proved in the paper; none of them has a machine-checked proof. The development needs pieces that are of independent use: Kantorovich duality for a signed, unbounded cost that is linear in one variable, the monotone (comonotone) coupling lemma, gluing of couplings along a common marginal, measurable selection of maximizers over a finite set, and a minimax exchange for a Lagrangian that is affine on a simplex and convex in an infinite family of functions. The ≥ step of the printed proof uses a product of couplings that does not give the inequality in general; a formal proof has to replace it by a gluing argument.
The obvious route to the first equality bounds from both sides by a joint law of . From above this needs a measurable optimal selection; from below it needs a joint law under which is a point of and each pair has a prescribed coupling. Independent products of the couplings fail here, because their -coordinates no longer form a point of . The Lagrangian equalities need duality for a cost that is neither bounded nor of one sign, with supported on all of , and attainment of the dual infimum over an unbounded family of potentials, which is invariant under the shifts by arbitrary constants and so has no compactness for free.
Finset (Fin n → ℝ); is its coordinate projection; is stdSimplex ℝ 𝒳, whose topology for finite is the weak-* one.Measure ℝ with IsProbabilityMeasure. Finite variance is MemLp id 2. Lemma 1 and Theorem 3, which print no moment condition, assume a finite mean (Integrable id) so that every expectation is finite.IsGreatest, IsLeast); inner inf/sup are IsGLB/IsLUB. The quantile is a real infimum that takes the value outside , a null set for the integrals.The following formalizations would trivialize the goal and are excluded: as a maximum over or ; a class that fixes only some marginals; couplings without the second marginal ; a conjugate taken over instead of ; equalities decided by the default value of a real sSup/sInf; an empty .
Welcome contributions: the monotone coupling lemma for general supermodular costs, Kantorovich duality on for finite , gluing of couplings, and proofs of any milestone.
A firm that sells several products must decide, before demand is known, how much capacity to build. It can build dedicated capacity, one resource per product, or a single flexible resource that can serve any product but costs more per unit. The classical argument for flexibility is risk pooling: one pooled resource absorbs the fluctuations of several demands, as studied by Fine and Freund (1990) and Van Mieghem (1998).
Chod, Markakis and Trichakis (SSRN 3212177, published in Management Science, 2021) identify a second, independent benefit. A firm usually observes its sales, not its demand: when a product stocks out, the firm learns only that demand exceeded capacity. This is demand censoring. Because flexible capacity can be shifted to whichever product is in demand, it stocks out less often for each product, and so the firm learns more about demand from a flexible system than from a dedicated one. When demand is correlated over time, that information is worth money in later periods. The paper calls this the learning benefits of flexibility and asks when they are positive.
To separate learning from pooling, the paper compares the two systems at the break-even cost of flexibility, the unit cost of flexible capacity at which both systems earn the same profit in a single period. Any difference that remains in a two-period model is then due to learning alone (Eq. (14) of the paper).
There are two products with a common unit price . Dedicated capacity costs per unit and flexible capacity costs per unit, with . The first-period demands are independent and each uniform on , with and . The profit margin is .
Static model. With dedicated capacities , product sells , and the expected profit is . With flexible capacity , product 1 is served first: it sells and product 2 sells ; the expected profit is . The optimal static profits are
and is a break-even cost when .
Learning. A product that had units available and demand reveals exactly if ; otherwise the firm learns only that and conditions its prior on that event. The firm's belief after period 1 is the product of the two products' posteriors. In period 2 demand repeats (), and both systems build dedicated capacity against the posterior belief , earning
The two-period optimal profits are
Take . There is a threshold such that for all with , , and ,
The goal fixes no numerical value of ; the paper reports .
Proposition 1 says that learning favours flexibility when margins are low or moderate and favours dedicated capacity when margins are high. Combined with the risk-pooling analysis, it shows that the value of flexibility in a dynamic setting is not captured by static pooling models: a firm choosing a technology by comparing single-period profits misjudges it in both directions, depending on the margin. The comparison at the break-even cost is the cleanest available measurement of the information value of a capacity structure under censored demand.
The paper proves Proposition 1 by computing closed forms of all the value functions and then certifying a polynomial inequality over a semialgebraic parameter set with sum-of-squares methods (p. A8). No machine-checked proof exists. A formalization would replace a computer-algebra certificate whose details are not printed with a checked argument, and would fix the value-function closed forms (milestones 2–6), which the paper derives in a few lines each. The milestones are of independent use: Lemma 3 and the censored-sales posterior are standard in inventory learning models.
The value functions and are suprema of first-period profit plus the expectation of a second-period value under a posterior that depends on whether each product stocked out. In the flexible system the capacity left for product 2 depends on product 1's realized demand, so the posterior of product 2 depends on product 1's demand, and the objective splits into regimes with different formulas; it is not concave in general (the paper notes "optimization of non-concave functions", p. 12). The break-even cost is defined implicitly by an equation involving square roots, so the final comparison is between two functions of along an implicit curve; the obvious approach of comparing closed forms branch by branch needs a sign certificate for a polynomial system rather than a one-line inequality.
Everything is real-valued. The uniform prior is times Lebesgue measure on ; the joint prior is the product measure. The stock-out posterior is Mathlib's conditional measure cond of the prior on , an exact observation is a Dirac measure, and a demand is observed exactly iff it is strictly below the available capacity (p. 9). The joint posterior is the product of the per-product posteriors, which is exact because the observation is a product event given product 1's demand. All optima are real suprema of images over nonnegative capacities, never closed forms. The symmetric case of §3 is built in (, common , i.i.d. uniform demands), as is (second-period demand equals first-period demand); at the paper's noise is zero for every , so the goal loses nothing. Added hypotheses, disclosed in each statement: , , , and in the goal .
The values must not be defined by their closed forms or by the paper's case split ; that would make the goal a statement about polynomials rather than about the Bellman problems.
A complete development needs: integrals of piecewise-linear functions against uniform laws and their products, conditional uniform laws, measurability of the posterior-dependent second-period value, and a sign certificate for the final polynomial comparison. The newsvendor and censored-posterior lemmas are reusable in other inventory-learning models. Contributions are welcome on any milestone, on alternative proofs of the final comparison, and on the regime of the flexible objective, which the milestones do not cover.
Temporal-difference (TD) learning estimates the value of a policy in a Markov decision process from sampled transitions, by repeatedly moving a parametrized value function towards a one-step bootstrapped target (Sutton, 1988). With a linear parametrization its behaviour is well understood: TD converges to the fixed point of the projected Bellman equation (Tsitsiklis and Van Roy, 1997), with finite-sample rates for projected and stochastic variants (Bhandari, Russo and Singal, 2018). With a nonlinear parametrization the same update can diverge: Tsitsiklis and Van Roy (1997) give an example, and the TD direction is not the gradient of any objective. Deep reinforcement learning nonetheless runs TD with neural networks as a matter of course.
Cai, Yang, Lee and Wang (arXiv:1905.10027v2, Mathematics of Operations Research, 2024) prove that TD with an overparametrized two-layer ReLU network, projected onto a ball around its random initialization, converges at rate to the global optimum of the mean-squared projected Bellman error (MSPBE) over a function class that becomes richer as the width grows. This mission formalizes that theorem for the stochastic-semigradient algorithm (Theorem 4.6 of the paper).
Transitions are tuples drawn i.i.d. from a sampling law : are feature vectors of the current and next state–action pair, with , the reward satisfies , and and have the same distribution (they are drawn from the stationary distribution of the policy). The discount factor is and .
The value function is the two-layer network
of width , with hidden weights and output weights . At initialization and , all independent; only is trained. The training set is the ball .
Algorithm 1 (neural TD) samples a tuple at each step , forms the Bellman residual , takes the semigradient step , projects it onto , and outputs with .
The linearization of the network at initialization is
a linear function of with random features. Writing for the Bellman residual of , an approximate stationary point is a with
The function solves the projected Bellman equation over the class . The regularity condition (Assumption 4.3) asks for with for every unit vector and every .
With and under Assumption 4.3, there is a constant such that for all , , and every approximate stationary point ,
where and the expectation is over the initialization, the samples of the run and a fresh .
The theorem gives a non-asymptotic guarantee for TD with a nonlinear function class, a setting in which the algorithm can diverge without further structure. The limit object is a projected Bellman fixed point over a class that, as , approaches a ball in the reproducing kernel Hilbert space of the neural tangent kernel; the paper uses this to bound the distance to the true value function (Proposition 4.7) and to analyze neural Q-learning and policy gradient methods (Section 6). The argument is an instance of the "lazy training" or neural-tangent-kernel regime, in which an overparametrized network trained from a random initialization stays close to its linearization.
The result is proved in the paper and, to our knowledge, has no machine-checked proof. A formalization would also produce reusable components: Gaussian anti-concentration of random ReLU activation patterns (Lemmas H.1–H.2), the linearization error of wide two-layer networks (Lemma 5.1), and a projected stochastic-approximation template with averaged iterates. The appendix proofs are short and pass over several measure-theoretic steps (conditioning on the current iterate, independence of the samples from the initialization, Jensen for the averaged iterate), which a formal proof has to supply.
The TD update is not a gradient, so the convergence proof cannot be a descent argument on an objective. The paper's route is to compare the update with that of the linear TD problem defined by , whose population semigradient is monotone, and to control the difference by overparametrization. The obvious first approach, linearizing the network in a deterministic neighbourhood of , fails: the ReLU activation pattern can change for some units whatever is. The comparison holds only in expectation over the random initialization and a fresh input, through Assumption 4.3 and the finiteness of for , which is where enters. The iterates and depend on the initialization, so these bounds are needed for random parameters that are correlated with but independent of the evaluation point.
Lean represents points as EuclideanSpace ℝ (Fin d) and parameters as PiLp 2 over Fin m, so all norms on are . The MDP, the policy and the feature map are not modelled; the statements see only the sampling law on tuples with the properties listed above. The run's samples form an -indexed i.i.d. sequence (product measure) independent of the initialization, and the evaluation tuple is a fresh draw. Expectations of nonnegative quantities are lower Lebesgue integrals, so non-integrability cannot make a bound hold vacuously. The ReLU semigradient uses the strict convention and keeps the factor of (3.2).
Conventions and readings fixed by the formalization, all disclosed in the item statements:
A formalization in which the comparison point may lie outside , the expectation is a Bochner integral of a possibly non-integrable function, or the constant may depend on , or , would not express the theorem and is excluded. Approximate stationary points are compared through , never through .
A complete development needs Gaussian measures on with the integrability of for , product and infinite-product probability measures with conditioning on the past of a sequence, existence of solutions to variational inequalities on compact convex sets, and nonexpansiveness of Euclidean projection onto a ball. Proofs of individual milestones are welcome independently; Lemmas H.1, 5.1 and (C.16) are self-contained.
Liquid democracy lets each voter either vote directly or delegate the vote to another voter, who may delegate it further. It has been used in practice, for example by the German Pirate Party on the LiquidFeedback platform and in the Google Votes experiment, and has been studied in computational social choice as a way to give more weight to better-informed voters. A natural worry is that delegation concentrates power: if too many votes flow to a few voters, the outcome rests on those few judgements and the "wisdom of the crowd" of independent votes is lost. Kahng, Mackenzie and Procaccia (Journal of Artificial Intelligence Research, 2021) showed that no local delegation mechanism can guarantee, for every instance, that liquid democracy is never worse than direct voting and sometimes strictly better.
Berinsky, Halpern, Halpern, Jadbabaie, Mossel, Procaccia and Revel (arXiv:2107.11868v3; Management Science, 2025) replace the worst-case requirement by a probabilistic one: competencies and delegations are random, and the comparison is made with high probability as the number of voters grows. Their first main result, Theorem 1, concerns the simplest model in which delegation goes only upward in competence. It is the goal of this mission.
There are voters deciding a binary question with a correct answer. Voter has a competence , the probability that its own vote is correct; given , the votes are independent, with law .
A delegation graph is a directed graph on in which every voter has at most one outgoing edge, the voter it delegates to. A voter who votes directly has weight (the number of voters whose delegation chain ends at ); a delegating voter has weight ; voters on a delegation cycle, or delegating into one, are not counted. is the largest weight. Direct democracy gets correct votes and liquid democracy . The gain of the instance is
A model consists of and . Competencies are drawn i.i.d. from a distribution supported in ; then each voter independently keeps its vote with probability and otherwise delegates to some with probability proportional to (and keeps its vote if all these weights vanish). This defines the law of the random instance.
The Upward Delegation Model has and : each voter delegates with probability , to a strictly more competent voter chosen uniformly. is the class of continuous distributions on .
The proof runs through the infinite Pólya urn with attachment probability : at time there is one ball in one bin; each new ball opens a new bin with probability and otherwise joins an existing bin with probability proportional to its size. is the largest bin size at time .
For every ,
The milestones are the statements the paper's proof uses, in attack order:
then satisfies probabilistic do no harm. If moreover some satisfies with probability , it satisfies probabilistic positive gain.
Theorem 1 shows that the impossibility result of Kahng et al. is an artefact of worst-case analysis: under a simple and natural random model, liquid democracy is asymptotically no worse than majority vote for every continuous competence distribution, and strictly better for some. Lemma 1 is the paper's general tool: it reduces both properties to two checkable conditions, a sub-linear largest weight and a linear increase of the expected number of correct votes, and is reused for the paper's two other models (Theorems 2 and 3). Lemma 2, a sub-linear bound on the largest bin of the infinite Pólya urn (the Simon–Yule preferential-attachment process), is of independent interest in random-structure theory.
The results are proved in the paper. None of them is formalized; Prove2Me has no liquid-democracy, delegation-graph or infinite-urn item. A formal development adds a checked version of the core lemma for arbitrary models, and a formal treatment of the urn that the later models' arguments can be compared with. Several steps of the paper are terse (the late-bin bound rests on a cited convergence rate; the arithmetic of Appendix B.3 is loose), so a checked proof adds more than a transcription.
The obvious argument — liquid democracy moves votes to better voters, so it should do at least as well — fails because concentration is lost when weights become large: if one voter carries a constant fraction of the votes, no longer concentrates, and the majority can be wrong with constant probability even though the expected number of correct votes rises. The heart of Theorem 1 is therefore Lemma 2, a bound with on the largest bin of an infinite Pólya urn. A first-moment bound on each bin handles the bins born before time , but the union bound over the remaining bins needs each to exceed with probability , which first moments do not give. The coupling between the urn and needs the competencies to be distinct, which is where continuity of enters.
All declarations live in the namespace LiquidDemocracy.Upward, in two definition files (Setting, Urn) and one file per theorem, against the platform's default Mathlib.
Fin n; a delegation graph is a map g : Fin n → Fin n with g i = i meaning "votes directly". A voter's weight counts the voters whose chain, followed steps, ends at it; chains running into a cycle reach no direct voter, which implements the cycle convention.Measure.bind; bins are numbered from , time means balls, and the step into time divides by .=o[atTop]; Definitions 1–2 keep the paper's form. In Lemma 1 the model is assumed typed as on p. 10 and measurable.A trivializing formalization is excluded: the instance law is a probability measure for and is nonempty (the uniform distribution on belongs to it), both checked sorry-free, so neither property holds vacuously or fails for a degenerate reason.
A complete development needs Hoeffding's and Chebyshev's inequalities (in Mathlib), Gautschi's inequality for Gamma ratios, a coupling argument for stochastic domination of Markov chains, and the conditional-independence structure of the instance law. The urn results and Lemma 1 are reusable beyond this mission. Contributions to any milestone are welcome, including alternative proofs of the late-bin bound (for instance by second-moment recursions instead of the cited Beta-limit rate).
Ride-hailing platforms change prices by location in real time, and drivers respond by moving. A price increase at one location changes where drivers go, how congested each location becomes, and therefore what every driver earns everywhere else. Besbes, Castro and Lobel, Surge Pricing and its Spatial Supply Response (SSRN 3124571, version of May 17, 2019; later published in Management Science, DOI 10.1287/mnsc.2020.3622), model this as a platform choosing prices over a continuous two-dimensional city, with non-atomic drivers who then relocate in equilibrium. Earlier work on ride-hailing pricing took space into account only in reduced form (e.g. Castillo, Knoepfle and Weyl, EC 2017) or on a finite network (Bimpikis, Candogan and Saban, Operations Research 2019). The platform's problem in this model is an infinite-dimensional optimization problem with equilibrium constraints. The paper's main result, the goal of this mission, characterizes optimal prices and supply locally, inside the regions drivers move into.
This mission formalizes that result from the SSRN preprint of May 17, 2019. Its online appendix contains the proofs, and every page and label cited here refers to it.
The city is convex and compact. It carries a finite city measure , a finite potential demand measure and a finite initial supply measure , all concentrated on , with . The demand density is , which is positive -a.e. At location the riders' willingness to pay has CDF , strictly increasing on its support , with and a continuous, unimodal revenue curve . The driver receives a fraction of each fare.
The platform chooses a measurable price mapping . Drivers relocate according to a flow , a measure on with first marginal and second marginal . The post-relocation supply is . A driver who ends at is matched with probability (with conventions at zero supply), earns , and pays travel cost when coming from . The best utility available from is the -essential supremum
is a supply equilibrium if almost every driver goes to a destination attaining this value. Problem (P2) maximizes , with , over price–equilibrium pairs; the paper shows (P2) is equivalent to maximizing platform revenue.
A single location run as a capacitated monopoly with supply has revenue and optimal price . The congestion function , with , is the utility per driver at that location. The indifference region of is . The attraction region of is . The point is a sink if and for every . Along each ray from , is the last point of .
For every feasible of (P2) and every sink , there are a feasible with at least the same (P2) value, points and numbers , such that on
where .
In order: Lemma 1 (p. 13, is 1-Lipschitz); Lemma A-1 (bounds on ; on the support of ); Lemma A-2 (equilibrium utilities); Lemma A-3 ( strictly decreasing); Proposition 2 (p. 15, the congestion bound -a.e.); Lemma B-2 (indifference propagates along segments); Lemma B-1 (attraction regions are closed unions of segments ); Lemma B-3 (positive flow contains an indifferent pair); Proposition B-1 (flow separation at the endpoints and at the sink); Proposition B-2 (pasting a local equilibrium into an attraction region).
Theorem 1 shows that, within any attraction region, an optimal solution has a simple structure. Supply is filled ray by ray outward from the sink up to the congestion bound, and each location is priced as a local monopolist given its supply. It reduces the platform's infinite-dimensional problem with equilibrium constraints to a choice of one cutoff point per ray. In the paper it is an ingredient of the explicit global solution of the one-dimensional demand-shock family of §8 (Theorem 3).
The result is proved in the paper (Appendix C). None of it has been formalized. A formal proof would check a long measure-theoretic argument (Appendix C, about nine pages) that works with densities, essential suprema and a.e. statements throughout. The milestones are smaller results with short proofs, and are self-contained targets.
The goal is an existence statement over flows, so the new equilibrium must be constructed and its equilibrium property checked. Changing supply inside changes utilities at every location whose drivers could move there. The supply and prices therefore cannot be optimized pointwise and pasted back without controlling flows that cross the boundary of the region. Matching the drivers available in to the congestion bound along each ray must work for an arbitrary finite , which may have atoms or be concentrated on curves. Every density identity holds only -a.e., and the region boundaries or can carry positive measure.
The plane is EuclideanSpace ℝ (Fin 2). The paper says "a norm", but the ray geometry of Appendix B needs a strictly convex one. Measures are measures on concentrated on , and flows are measures on . Densities are Radon–Nikodym derivatives converted to reals, so every pointwise claim about , or prices built from them is stated -a.e. is the Mathlib essSup with respect to ; it is finite under the standing assumptions, so no boundedness hypothesis is added. Rays are indexed by unit vectors.
The standing assumptions of §3.1 are one hypothesis, Market.Standing, of every theorem. It contains: convex compact city; finite measures concentrated on it, with ; ; ; a CDF supported on and strictly increasing there; continuous, unimodal revenue; -a.e.; joint measurability of . The last assumption and the CDF properties are implicit in the paper and are added openly. A sanity file shows that these assumptions hold for a one-point city.
In Theorem 1, is written as . The supply cases are read in the printed order at the sink. Prices come from (5), so . In Proposition B-1, the printed is read as the half-open used in its proof. Proposition B-2 adds , the precondition of Definition 3.
Two formalizations would make the goal trivial, and both are excluded. Dropping the equilibrium condition from feasibility would let any flow "dominate". Taking as a pointwise supremum or as a free function would decouple the objective from the flow. Feasibility includes Definition 1, is an essential supremum, and is the density of the flow.
Contributions welcome: proofs of the milestones, general lemmas on essential suprema of Lipschitz families, and general measure-theoretic results about finite planar measures and rays from a point, which can be reused outside this mission.
Housemates who share a house must decide who gets which room and how the total rent is split. A solution pairs an assignment of rooms to agents with a rent for each room, and it is envy-free if no agent prefers another room at that room's rent. Envy-free rent division is the textbook example of fair division with money and is the mathematical core of two-sided matching markets with transfers, where an envy-free solution is a competitive equilibrium.
For quasilinear utilities (a room's value minus its rent) envy-free solutions are computed by an assignment problem and a linear program (Aragones, 1995), and this method is in practical use. Real preferences are often not quasilinear: an agent may have a budget, or be less sensitive to rent at low prices. Existence of envy-free solutions for general continuous, decreasing utilities was established by Svensson (1983) and by Alkan, Demange and Gale (1991), whose perturbation lemma lowers the rents of an envy-free solution while keeping it envy-free. Alkan (1989) gave an algorithm that finds an equilibrium in finite time, with no polynomial bound. Arunachaleswaran, Barman and Rathi (arXiv:1807.04163; Mathematics of Operations Research, 2022) give the first fully polynomial-time approximation scheme for continuous, decreasing piecewise-linear utilities. They also show that the exact problem lies in PPAD ∩ PLS.
There are agents and rooms. Agent 's utility for room at rent is , given by a base value (of either sign), break points and slope magnitudes , so that is continuous, strictly decreasing and linear with slope on (the last piece is unbounded). The total number of pieces is , and bounds over all slopes. A solution is a bijection from agents to rooms and a rent vector . It is envy-free if for all . For it is -EF (Definition 2) if every agent with nonnegative utility satisfies for all , and every agent with negative utility satisfies for all .
Algorithm 1 works on a modified instance : above a threshold with for all , every utility is continued with slope (equation (1)). It starts from any envy-free solution of with all rents at least . While all rents are positive it (i) takes a maximum-weight perfect matching of the first-choice graph at , with the weight of edge equal to of the current slope of ; (ii) sets to a minimum-total-rent solution of the linear program that keeps envy-free, keeps the rents nonnegative, and keeps them inside the current linear domain (the box of rents between consecutive slope changes, Definition 1).
The approximation scheme rounds every slope up to a power of , . Each piece is replaced by two pieces of slopes and that meet the original function at the piece's end points, after the zero of each utility has been made a break point. The resulting instance is .
There is a constant such that for every instance with , every and every admissible threshold for , Algorithm 1 run on
iterations, whatever Step 2 solution, matchings and LP optima are chosen; 3. outputs rents such that is an -EF solution of the original instance.
The polynomial is left unspecified; the paper's proof gives a small explicit one, and any polynomial establishes the scheme.
The proof has two halves. Theorem 1 (p. 9, proof pp. 13–14) is the same statement with "envy-free" in place of "-EF" for any instance whose slopes are already powers of . It rests on Lemma 16 (quasilinear envy-free allocations are the maximum-weight matchings), Lemma 18 (its multiplicative form), the perturbation Lemma 2, the run invariants Lemmas 3–5 and the per-domain count (3), . Lemma 9 (p. 17) states that every envy-free solution of with nonnegative rents is -EF for the original instance, through Lemmas 6–8 on the rounded functions.
Theorem 2 gives an efficient algorithm for approximately fair rent division under general piecewise-linear utilities: budgets, rent-sensitive valuations and concave utilities. Exact envy-free solutions for this class are only known to lie in PPAD ∩ PLS. Because envy-free solutions are equilibria of unit-demand markets with money, the theorem also yields approximate equilibria for such markets with non-quasilinear utilities. Theorem 1 gives an exact polynomial algorithm whenever slopes are powers of .
The result is proved in the paper. None of it has been machine-checked: there is no formal model of envy-free rent division, of the perturbation lemma, or of a price-descent algorithm of this kind in Mathlib or on the platform. A complete development would give a checked proof that a fair-division algorithm terminates within a polynomial number of iterations with a fairness guarantee.
Envy-freeness of the output is not the hard part: every iterate of Algorithm 1 is envy-free for by construction, and the rounding lemmas are elementary inequalities on single pieces. The difficulty is termination with a polynomial bound. Lowering rents by the perturbation lemma alone need not stop: Alkan gives an instance in which the perturbations do not converge. A bound has to control how many iterations the algorithm spends inside one linear domain and how many domains it visits. The first count fails for arbitrary slopes, where up to matchings of distinct weight can occur in one domain; the power-of- structure is what the rounding provides. The perturbation lemma is also needed in the form of Lemma 2, for every maximum-weight matching of the weighted first-choice graph, not only for one matching it produces. A formal proof must further show that each step can be carried out: the matching exists and each linear program attains its minimum.
Standing requires first start , strictly increasing starts and positive slopes. Agents and rooms are Fin n, allocations are Equiv.Perm (Fin n), rents are real. is the natural logarithm. bounds and stands in for the bit complexity of the slopes. Base values may be negative.A chance constraint asks that a random inequality system hold with at least a prescribed probability . Such constraints appear throughout engineering and energy optimization: reservoir and power-system management, network design, and any decision that must stay feasible against uncertain demand or inflow with high reliability. The function is called a probability function. It is in general neither convex nor smooth, even when the underlying random inequality is convex in the random vector, and this is what makes chance-constrained problems hard to solve with standard nonlinear-programming methods.
One remedy is to replace the probability function by a regular approximation and to solve a sequence of approximate problems. van Ackooij, Pérez-Aros, Soto and Vilches (arXiv:2301.09803, Mathematics of Operations Research, 2024) propose an inner regularization built from the Moreau envelope of a scalarized constraint function, for conic constraints in infinite-dimensional decision spaces. The approximate feasible sets contain the original one, and the approximate problems have smooth data. A regularization is useful only if solving the approximate problems recovers the original problem in the limit. This mission formalizes that consistency statement, Theorem 5.4 of the paper.
Let be a separable real Hilbert space (the decision space), a real Banach space with dual , and a random vector on a probability space whose law has a density with respect to Lebesgue measure. A continuous map and a nonempty closed convex cone define the probability function
The conic constraint is scalarized by a convex, weak-compact set whose generated cone has weak closure equal to the positive polar cone . A convex, continuously differentiable is assumed to make every scalarization , , jointly convex. The supremum function is .
For and , the Moreau envelope is . The inner regularization of is
the envelope being taken on with the Hilbert norm. For put and . Given a proper, convex, lower semicontinuous objective , problem (P) minimizes over and the regularized problem (Pλ) minimizes over , with optimal values and .
If is moreover coercive and , then
and for and optimal solutions of with , the point is optimal for (P). If moreover and is Fréchet differentiable on , then in norm.
Theorem 5.4 justifies the regularization as a solution method: optimal values converge, and weak limits of regularized optimal solutions solve the original problem, with strong convergence under a smoothness condition on . Combined with the paper's differentiability results for (§4, not part of this mission), it reduces a nonsmooth chance-constrained problem to a sequence of problems with smooth data whose solutions approximate the true ones. The intermediate results (monotone convergence of , the limsup estimate, convergence of feasible sets) are reusable for any analysis of envelope-based approximations of probability functions.
All statements are proved in the paper. None of them, and none of the general facts used (monotone and lower epi-convergence of Moreau envelopes in Hilbert space, Painlevé–Kuratowski and Mosco convergence), has a machine-checked proof on the platform at the time of writing. The mission produces a formal account of the conic scalarization, of the inner regularization, and of the consistency argument.
The obvious approach, "the regularized feasible sets converge, the regularized objectives converge, hence the minima converge", fails in two places. First, the decision space is infinite-dimensional, so bounded minimizing sequences only converge weakly, and the probability function must be controlled along weakly convergent sequences. This requires weak upper semicontinuity of and a limsup estimate for along weakly convergent , which do not follow from continuity of . Second, convergence of values needs a liminf inequality for along weakly convergent sequences together with Mosco, not merely Painlevé–Kuratowski, convergence of the feasible sets. The probability function is not convex, so the usual convex-analytic route to Mosco convergence is unavailable.
The Lean development uses H with [InnerProductSpace ℝ H] [CompleteSpace H] [SeparableSpace H], Y a real Banach space with dual StrongDual ℝ Y, and weak notions through WeakDual ℝ Y. Extended-valued functions (, , , , , ) are EReal-valued, and infima and suprema are taken there, so no default value enters. Probabilities are ℝ≥0∞-valued. The product carries the ℓ² norm (WithLp 2), as the paper requires. Weak convergence is defined through inner products. The limit is the filter of right neighbourhoods of for values and positive sequences for solutions and feasible sets.
The definitions file contains , , coercivity, conjugate, subdifferential, Fréchet differentiability of an extended-valued function, weak convergence, sequential weak continuity, Painlevé–Kuratowski and Mosco convergence, the conic setting (9)–(10), , , , , , , and optimality for (P) and (Pλ).
Two hypotheses are added to the printed statements, each used by the paper's own proofs: is closed (the bipolar step of Proposition 2.6), and is sequentially weakly continuous in Theorem 3.1 d) and throughout Theorem 5.4. The second is automatic when is finite-dimensional. Both are disclosed in the statements.
Trivializing readings are excluded: the feasible set meets ; is proper; the envelope uses the Hilbert, not the sup, norm on the product; is an extended-real supremum over a nonempty set, not a real supremum with a default value; every is positive. Item b) of the goal is vacuous only when some regularized problem has no optimal solution, exactly as in the paper.
Contributions welcome: Moreau-envelope convergence in Hilbert space, the bipolar theorem for closed convex cones in Banach spaces, measure-theoretic continuity arguments for , and the existence argument for optimal solutions of (P).
Nonlinear conic programming covers nonlinear programming (NLP), nonlinear semidefinite programming (NLSDP) and nonlinear second-order cone programming (NSOCP) in one model: minimize a smooth objective subject to the requirement that a smooth map takes values in a closed convex cone. The classical first-order necessary condition, the Karush–Kuhn–Tucker (KKT) condition, holds at a local minimizer only under a constraint qualification such as Robinson's, and for conic constraints such qualifications are restrictive and hard to check.
Sequential optimality conditions avoid this. They require only that approximate KKT points exist along a sequence converging to the candidate, and they hold at every local minimizer with no constraint qualification. They are also what practical algorithms actually produce, since an algorithm only ever stops at an approximate point. For NLP, AGP was introduced by Martínez and Svaiter (2003) and CAKKT by Andreani, Martínez and Svaiter (2010); Andreani, Haeser and Martínez (2011) compare the sequential conditions. R. Andreani, W. Gómez, G. Haeser, L. M. Mito and A. Ramos (Mathematics of Operations Research, 2022) extend AGP and CAKKT to general conic programs, by means of projections onto the cone and its polar. They then show that a safeguarded augmented Lagrangian method generates sequences satisfying them. This mission formalizes that convergence theory (Section 4 of the paper).
Let and be continuously differentiable, where is a finite-dimensional real inner product space. Let be a nonempty closed convex cone, and consider
A point is feasible if . The polar cone is . For a closed convex set , denotes the orthogonal projection of onto (its nearest point). is the adjoint of the derivative of at .
A feasible satisfies AGP (Approximate Gradient Projection) if there are sequences and with
It satisfies CAKKT (Complementary Approximate KKT) if moreover, on the same sequences, .
The augmented Lagrangian is for . Algorithm 1 takes positive tolerances , a nonempty convex compact safeguarding set , and constants , , . At step it:
A point and a function satisfy the generalized Łojasiewicz inequality if, for some and some continuous on with as ,
If is a feasible limit point of a sequence generated by Algorithm 1, and satisfies (28) for , then
Theorem 4.1 shows that the augmented Lagrangian method, with no constraint qualification at all, produces AGP points. AGP was previously the condition behind inexact restoration methods, so this puts the two method families on a common footing. Theorem 4.2 adds the complementarity limit (18) under the generalized Łojasiewicz inequality. Every analytic function satisfies that inequality. For NLSDP the theorem refines the earlier guarantee that such methods generate TAKKT sequences. Combined with the paper's result that every local minimizer is a CAKKT point, it says the algorithm's limit points pass a necessary optimality test that is sharper than AGP. The theory allows cones with empty interior or without self-duality, such as the cone of Euclidean distance matrices.
The results are proved on paper. No machine-checked version is known. Formalizing them needs a working theory of projections onto closed convex cones in finite-dimensional inner product spaces: existence, nonexpansiveness, Moreau's decomposition, and the differentiability of the squared distance. It also needs derivative calculus for the augmented Lagrangian. These are reusable well beyond this paper, by any later formalization of conic optimization algorithms.
The algorithm is stated with free choices at every step, so nothing about it can be computed. Everything has to come from the inequalities that define a run. The main obstacle is the case of an unbounded penalty parameter in Theorem 4.2. In that case the multipliers may diverge, and it is not clear why should vanish. Without (28) it need not: the paper points to a counterexample in which the method produces sequences that are not CAKKT. The bounded case needs instead the observation that the Step 4 test forces once the penalty stops growing. The calculus milestones depend on the differentiability of , which is not in Mathlib in this form.
EuclideanSpace ℝ (Fin n), and is any finite-dimensional real inner product space.ContDiff ℝ 1.MoreauProx.Decomposition.Cones. The polar uses the sign .fderiv ℝ G x, and is Mathlib's gradient.IsALRun on the produced sequences . Every free choice of the page stays free. The convention is encoded as . The initial point plays no role and is omitted.MapClusterPt). In (28), is the open ball and is the operator norm of the derivative.Contributions are welcome on the convex-projection layer: existence and uniqueness of , nonexpansiveness, Moreau's decomposition (posed separately on the platform as MoreauProx.Decomposition.cone_decomposition), and the gradient of the squared distance. They are also welcome on the two case analyses of the convergence proofs.
We establish several upper bounds on the energy-constrained quantum and private capacities of all single-mode phase-insensitive bosonic Gaussian channels. The first upper bound, which we call the "data-processing bound," is the simplest and is obtained by decomposing a phase-insensitive channel as a pure-loss channel followed by a quantum-limited amplifier channel. We prove that the data-processing bound can be at most 1.45 bits larger than a known lower bound on these capacities of the phase-insensitive Gaussian channel. We discuss another data-processing upper bound as well. Two other upper bounds, which we call the "-degradable bound" and the "-close-degradable bound," are established using the notion of approximate degradability along with energy constraints. We find a strong limitation on any potential superadditivity of the coherent information of any phase-insensitive Gaussian channel in the low-noise regime, as the data-processing bound is very near to a known lower bound in such cases. We also find improved achievable rates of private communication through bosonic thermal channels, by employing coding schemes that make use of displaced thermal states. We end by proving that an optimal Gaussian input state for the energy-constrained, generalized channel divergence of two particular Gaussian channels is the two-mode squeezed vacuum state that saturates the energy constraint. What remains open for several interesting channel divergences, such as the diamond norm or the Renyi channel divergence, is to determine whether, among all input states, a Gaussian state is optimal.
This mission is the statement-level formalization of Bounding the energy-constrained quantum and private capacities of phase-insensitive bosonic Gaussian channels (arXiv:1708.07257v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 26: thermal gap bound (Theorem 26, PDF p. 34). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
51 results of the paper are not stated yet, because the library lacks an interface they need:
We derive a simple relation between a quantum channel's capacity to convey coherent (quantum) information and its usefulness for quantum cryptography.
This mission is the statement-level formalization of Quantum privacy and quantum coherence (arXiv:quant-ph/9709058v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Fixed-strategy guaranteed privacy is bounded below by Bob information minus environment Holevo information (Equation (8): fixed-strategy guaranteed privacy lower bound, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
3 results of the paper are not stated yet, because the library lacks an interface they need:
We establish the classical capacity of optical quantum channels as a sharp transition between two regimes---one which is an error-free regime for communication rates below the capacity, and the other in which the probability of correctly decoding a classical message converges exponentially fast to zero if the communication rate exceeds the classical capacity. This result is obtained by proving a strong converse theorem for the classical capacity of all phase-insensitive bosonic Gaussian channels, a well-established model of optical quantum communication channels, such as lossy optical fibers, amplifier and free-space communication. The theorem holds under a particular photon-number occupation constraint, which we describe in detail in the paper. Our result bolsters the understanding of the classical capacity of these channels and opens the path to applications, such as proving the security of noisy quantum storage models of cryptography with optical links.
This mission is the statement-level formalization of Strong converse for the classical capacity of optical quantum communication channels (arXiv:1401.4161v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Operational strong converse above the optical classical-capacity threshold (Introduction and Corollary 1, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
A longstanding open problem in quantum information theory is to find the classical capacity of an optical communication link, modeled as a Gaussian bosonic channel. It has been conjectured that this capacity is achieved by a random coding of coherent states using an isotropic Gaussian distribution in phase space. We show that proving a Gaussian minimum entropy conjecture for a quantum-limited amplifier is actually sufficient to confirm this capacity conjecture, and we provide a strong argument towards this proof by exploiting a connection between quantum entanglement and majorization theory.
This mission is the statement-level formalization of Majorization theory approach to the Gaussian channel minimum entropy conjecture (arXiv:1111.1986v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Single-use reduction: C1 iff C2 iff C3; C4 is sufficient (C1–C4; Appendix 1, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
The long-standing conjectures of the optimality of Gaussian inputs for Gaussian channel and Gaussian additivity are solved for a broad class of covariant or contravariant Bosonic Gaussian channels (which includes in particular thermal, additive classical noise, and amplifier channels) restricting to the class of states with finite second moments. We show that the vacuum is the input state which minimizes the entropy at the output of such channels. This allows us to show also that the classical capacity of these channels (under the input energy constraint) is additive and is achieved by Gaussian encodings.
This mission is the statement-level formalization of A solution of the Gaussian optimizer conjecture (arXiv:1312.2251v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Main result: vacuum optimizer and unconditional Gaussian minimum-output additivity (Main result: vacuum optimizer and unconditional Gaussian minimum-output additivity, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need:
Optical channels, such as fibers or free-space links, are ubiquitous in today's telecommunication networks. They rely on the electromagnetic field associated with photons to carry information from one point to another in space. As a result, a complete physical model of these channels must necessarily take quantum effects into account in order to determine their ultimate performances. Specifically, Gaussian photonic (or bosonic) quantum channels have been extensively studied over the past decades given their importance for practical purposes. In spite of this, a longstanding conjecture on the optimality of Gaussian encodings has yet prevented finding their communication capacity. Here, this conjecture is solved by proving that the vacuum state achieves the minimum output entropy of a generic Gaussian bosonic channel. This establishes the ultimate achievable bit rate under an energy constraint, as well as the long awaited proof that the single-letter classical capacity of these channels is additive. Beyond capacities, it also has broad consequences in quantum information sciences.
This mission is the statement-level formalization of Ultimate communication capacity of quantum optical channels by solving the Gaussian minimum-entropy conjecture (arXiv:1312.6225v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-energy Gaussian minimum output entropy (Eq. (2), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
Online marketplaces (ride-sharing, delivery, freelance labour) set payments for their suppliers and want to know how a change in payment would change the platform's utility. The standard tool, a randomized A/B test, is biased in a marketplace: treated and control suppliers compete for the same demand, so a payment increase given to the treatment group draws business away from the control group. This interference violates the no-interference assumption of classical causal inference (Hudgens and Halloran, 2008), and it was documented on a large platform by Blake and Coey (2014). Global experimentation, changing the payment for everyone and comparing days, avoids interference but is slow and costly.
Wager and Xu (2021) propose local experimentation: give every supplier a small, symmetric, random payment perturbation, measure how participation responds to one's own perturbation, and correct for the equilibrium feedback using a model of how demand is matched to suppliers. The perturbations are symmetric, so they do not move the market equilibrium at first order. The paper shows that in a large market this recovers the gradient of the platform's equilibrium utility. This mission formalizes that result, Theorem 6 of the paper, together with the lemmas on which its proof rests.
Everything is conditional on a global state (weather, holidays), which is dropped from the notation. In the -th system there are potential suppliers and a random demand on with , and .
Matching. If suppliers are active and demand is , each active supplier serves on average units. is non-decreasing in , non-increasing in , and , where the error is bounded and , and is a regular allocation function: is smooth, concave, non-decreasing, , , .
Choice. Supplier has a private feature and is paid per unit served. Given its expected revenue , it becomes active () with probability , where each choice function is -valued, non-decreasing and twice differentiable with uniformly bounded second derivative.
Equilibrium. With independent of , let . Under a payment law , the equilibrium supply fraction solves the balance equation
At a fixed payment , . The mean-field supply solves , and the mean-field platform utility is
with the limiting revenue per unit of supply. The marginal response is , and is its pre-limit analogue.
The experiment. Payments are with independent signs . From , and the regression slope
form and
For with (), and perturbation sizes with ,
A platform can thus learn the payment sensitivity of its equilibrium utility from one period of data, with perturbations that vanish as the market grows. The gradient estimate is the input to the first-order payment-optimization scheme of §4.2 of the paper, and the decomposition of Lemma 4 separates the measurable marginal response from an interference correction that depends only on the matching function .
None of these results has been machine-checked. A complete formalization gives a verified mean-field limit for a fixed-point equilibrium with binomial supply, a binomial Stein-type identity (Proposition 10), and a consistency proof for a regression estimator under vanishing perturbations. The mission also records two corrections. The claim for in (A.7) is too strong as printed. Lemma 15 (Appendix B.3), used in Proposition 10's proof, omits a factor; Proposition 10 itself is not affected.
The obvious argument says that is a regression slope, so it converges by the law of large numbers. It does not apply directly, for two reasons. First, the are not sampled at the unperturbed equilibrium: the perturbation itself moves the equilibrium, and the experiment runs at . Showing that this shift is uniformly in (Proposition 11) needs the implicit-function structure of the balance equation and the symmetry of the perturbation. Second, the noise in has standard deviation of order , while its bias is of order . The rate restriction balances the two. Finally, the limit of is a derivative of an expectation over a binomial law in which the error term is multiplied by ; controlling it needs a Stein-type identity, not term-by-term convergence.
All objects live in the namespace EquilibriumExperiment.Gradient. A Market B holds the primitives for one global state; Market.Standing bundles Definition 5, Assumptions 1–2, the part of Assumption 3 that concerns , and the demand conditions (3.1)–(3.2). Conventions:
eLpNorm … 2 → 0.Ruled out: independent of the perturbation, an arbitrary random variable rather than the solution of (A.2), hypotheses on all of , or as a deriv of a non-differentiable function (Proposition 12 proves differentiability).
Not in this mission. Theorem 7 (the regret of the first-order method) is false as printed: with , , , , utilities and in two periods and , the left side of (4.6) at , equals ; step (A.10) drops a factor 2. Corollary 8, which rests on it, Theorem 9, Lemma 3 and (3.15), which concern the pre-limit utility, are also excluded. Lemma 15 is false as printed and is not an item.
Contributions are welcome at every milestone; the binomial Stein identity, the implicit-function argument for monotone fixed points and the triangular-array law of large numbers for the slope are reusable.
School districts, public housing authorities and refugee resettlement agencies allocate scarce items (school seats, apartments, slots) without prices. Most such systems are priority-based: each applicant receives a priority, possibly depending on observable characteristics such as neighborhood or sibling status, and a mechanism such as deferred acceptance (DA), serial dictatorship or top trading cycles turns priorities and reported preferences into an assignment. The planner's design question is which priorities and quotas to choose. Shi (SSRN 3425348; Management Science 2022, doi:10.1287/mnsc.2020.3925) reduces this question, in a large-market model, to a linear program over budget set probabilities: the probability that an applicant of each segment can choose from each menu of items. That reduction is only useful if the optimal menus can actually be produced by a familiar mechanism. Theorem 1 a) of the paper says that, under a mild regularity condition, DA can produce any feasible menu distribution, and DA with a single tie-breaker (DA-STB) can produce exactly the nested ones.
The continuum approach to DA follows Azevedo and Leshno (JPE 2016), who describe stable matchings in large markets by cutoff vectors, and Abdulkadiroğlu, Che and Yasuda (AEJ: Micro 2015) on expanding choice in school choice.
There are items and an outside option , with . A market has segments of agents with masses , capacities for the real items (the outside option is unlimited), and for each segment a probability distribution of utility vectors with pairwise distinct components (strict preferences). The choice probability is
A budget set probability matrix lists the probability that a segment- agent faces menu . The feasible set consists of those with , , when , and the capacity constraint for every .
In DA, each agent of segment draws a priority vector from a law , independently of his utilities. Given a cutoff vector , his budget set is and he receives his favourite item in it. The demand is . For quotas , the DA operator raises each just enough to bring down to , and the DA cutoff is its least fixed point in . A mechanism implements if for all and . In DA-STB, for a deterministic boost matrix and one tie-breaker per agent.
The market is regular if implies for all : adding items to a menu strictly lowers the chance that the outside option is chosen. A matrix is nested within segment if any two menus used with positive probability by the same segment are ordered by inclusion.
If is regular, then
The milestones are the steps of the paper's own proof, in attack order:
Theorem 1 a) is what makes the paper's optimization approach operational. Once a planner solves the linear program over , part i) guarantees a DA mechanism with explicit priorities and quotas that realizes the solution, so for regular markets nothing is lost by restricting attention to DA. Part ii) characterizes the DA-STB-implementable matrices, which is what lets the paper compare single tie-breaking with DA and identify when the simpler mechanism suffices. The remaining results of the paper (optimal assortments under multinomial and nested logit, the Boston school choice application) are built on this reduction.
The theorem is proved in the paper; nothing here is open. To the best of the drafting search, none of it is formalized: Prove2Me has finite two-sided matching and Gale–Shapley items, but no continuum matching market, no DA cutoff, and no budget set implementation result. Formalizing it provides a machine-checked large-market DA model (demand, cutoff operator, least fixed point) that other market design papers using the Azevedo–Leshno framework can reuse.
The obvious argument shows that the all-ones cutoff vector reproduces and is a fixed point of the DA operator. That does not finish the proof: the DA mechanism uses the least fixed point, and in general there are smaller ones. Example H.1 of the paper (p. 50) gives a non-regular market with a feasible, nested matrix that no DA mechanism implements under any priorities or quotas, so regularity cannot simply be dropped. The work is in showing that, under regularity, no fixed point strictly below can change the menu probabilities. This mixes order theory (Knaster–Tarski on a box), measure theory (product measures of utilities and priorities, continuity of the demand under an atomless tie-breaker) and a strict comparison of outside-option masses.
Items are Option (Fin n), with none the outside option; priorities and cutoffs are Fin n → ℝ; menus are Finset (Option (Fin n)), and sums over menus run over the whole power set of . The utility laws are probability measures on Option (Fin n) → ℝ, concentrated on injective vectors (strict preferences). Capacities are assumed nonnegative. Probabilities are real numbers obtained as toReal of finite measures. The demand is computed under the product measure , which encodes independence of priorities and preferences.
The DA operator merges the two branches of Algorithm 2 into a single infimum over , with added to the set so the operator maps to itself, as the paper asserts. The DA cutoff is characterized as the least element of the fixed points in . DA-implementability quantifies over a priority box with , probability laws supported in it, quotas , and the DA cutoff. DA-STB-implementability quantifies over boosts with , so priorities stay in the box.
Implementability is never stated as quantification over menus directly: that would be the random assortment mechanism, which implements every by definition and would make part i) trivial. The cutoff is never "some fixed point": the all-ones vector is a fixed point by construction, and only the least fixed point carries the content of the theorem.
Theorem 1 b) (TTC and serial dictatorship) is not part of this mission: the TTC cutoffs are imported from Leshno and Lo as a black box. Contributions are welcome on the measure-theoretic lemmas (continuity of the demand, the menu law under (H.1) and under single tie-breaking) and on the Knaster–Tarski step, which can use Mathlib's OrderHom.lfp on a complete lattice of boxes.
Machine-learned models of molecular energies and properties are trained on the output of quantum-chemistry calculations, and a common way to make them data-efficient is to build the physical symmetries of the problem into the architecture. When the input is not a point cloud but a set of matrices expressed in an atomic-orbital basis (Fock, density, overlap and Hamiltonian matrices from a cheap mean-field calculation), the relevant symmetry is the freedom to rotate the orbital basis of each atom independently: a rotation of the molecule, or any other unitary change of the local frames, changes every matrix element but not the physics.
Qiao, Christensen, Welborn, Manby, Anandkumar and Miller (arXiv:2105.14655v4, published in PNAS 2022) introduce UNiTE (Unitary N-body Tensor Equivariant network), the architecture behind OrbNet-Equi. They state as eq. (4), p. 3, that the network must satisfy for every isometric basis rotation , and prove this property in Appendix S2.6 (pp. 26–28) for a generalized version of the network: tensors of any order , complex scalars, and an arbitrary unitary change of basis on each atom. The empirical results of the paper (QM9, MD17, GMTKN55) rest on this design principle, but the mathematical content of the paper is the equivariance proof.
There are atoms . Atom carries a finite basis , and the concatenated basis is the set of pairs . An N-body tensor of order is a function of concatenated indices; its sub-tensor at collects the entries whose -th index lies in atom .
A group (the paper's ; in the experiments) acts through unitary representations , and each atom has a subgroup . An element with acts on tensors by the local action (S26):
The network's hidden features assign to each label of a unitary representation and each channel a vector ; acts by . Matching matrices relate the atomic basis to a basis adapted to the decomposition .
The UNiTE network (Methods 1.1; Appendix S2.5) consists of:
Under the hypotheses the paper's proof uses — compatibility (S35) of the matching matrices, the Clebsch–Gordan property (S33) of , equivariance (S32) of the diagonal reduction, invariance of the attention weights, and positivity of the EvNorm constants — for every , tensor and atom ,
The proof in S2.6 rests on three results of S2.4 and four labelled sub-proofs:
The theorem is what justifies feeding UNiTE features in arbitrary local frames: the predicted invariant quantities (energies) do not depend on the choice of atomic-orbital phases or orientations. The vector-valued outputs, such as dipole moments, then transform correctly. Without it, the model would have to learn the symmetry from data or from augmentation. The same argument applies to other architectures acting on matrices in local bases, for example models of Hamiltonian or density matrices.
The result is proved in the paper, with a proof written at the level of index manipulations. To our knowledge it has no machine-checked proof. Formalizing it pins down exactly which hypotheses each layer needs: (S35) on the matching matrices, the complex conjugate in (S36), the intertwining form of (S33), and invariance of the attention weights. It also yields a reusable library of statements about tensor-product and block-diagonal actions of unitary representations. Theorem S1 for an arbitrary group with a complete catalogue of irreducibles is a statement of independent interest: finite-dimensional unitary representations are completely reducible, which Mathlib does not yet provide outside finite groups.
No single step is deep; the difficulty is bookkeeping across dependent index types. The local action is block-diagonal over atoms, so cross-atom terms must be shown to vanish. Sub-tensor indices are dependent on the atom sequence . The block convolution's cancellation uses unitarity and the conjugate. The reverse matching layer needs the adjoint form of (S35), which uses that is a subgroup (closed under inverses). The point-wise block reindexes a double sum through a Kronecker product. The full network is a two-phase recursion whose attention weights depend on the current features, so the induction must carry the equivariance of every intermediate feature. Theorem S1 needs complete reducibility of a finite-dimensional unitary representation of an arbitrary group, together with the identification of each irreducible summand with a catalogue member.
A tempting shortcut, assuming each layer equivariant and composing, proves nothing about UNiTE: the content is that these specific layers are equivariant under these specific hypotheses.
All scalars are complex; the paper's real (orthogonal) case is the special case of real unitary matrices. is replaced by an abstract group ([Group K]), representations are homomorphisms K →* Matrix.unitaryGroup ι ℂ, and the catalogue of irreducibles of is a family with the hypothesis CatalogComplete (every irreducible unitary representation is equivalent to some ), the formal reading of the paper's "we have abstracted the labelling details … into the index L". The subgroups are S u : Subgroup K, and every hypothesis is assumed only for .
Committed conventions:
Σ u, ι u;Trivializing formalizations are ruled out. The layers are defined concretely, not replaced by maps assumed equivariant. The action is local, one unitary per atom, not one global unitary. The complex conjugate in (S36) is kept. Irreducibility of the catalogue and its completeness are both stated in Theorem S1 and the corollaries.
The development needs one definitions module (OrbNetEqui.Equivariance.Basic) and Mathlib's matrices, unitary groups, block-diagonal and Kronecker matrices. Contributions are welcome on every milestone; the building-block lemmas (block-diagonal and Kronecker actions of unitary matrices, unitary invariance of the regularized norm) and complete reducibility of finite-dimensional unitary representations are reusable beyond this mission.
A company that is about to launch a product often has several candidate versions of it (designs, packagings, feature bundles) and wants to know which one consumers like best. A common way to find out is to ask: show an arriving consumer a few versions and record which one they pick. Each such query costs time and money, and consumer answers are noisy, so the question is how to choose what to show, and when to stop asking, so that the most preferred version is found with a prescribed reliability using as few consumers as possible.
Y. Feng, R. Caldentey and C. T. Ryan, Robust Learning of Consumer Preferences (SSRN 3215614; Operations Research, doi:10.1287/opre.2021.2157), treat this as a sequential hypothesis test in the style of best-arm identification (Garivier and Kaufmann, 2016; Kaufmann, Cappé and Garivier, 2016). The difference from a bandit is in the feedback: an action is a set of versions, and an observation is a choice from that set drawn from an unknown choice model. The paper asks for a policy that is good not for one choice model but uniformly over a large nonparametric class of them, and shows that a simple likelihood-based policy achieves this.
There are versions, . A display set is a subset with ; is the collection of display sets. A preference gives, for each and , the probability that a consumer shown picks . A ranking is a permutation of , rank being the top.
For , the class of -separable preferences (Definition 1) consists of the with exactly for , , and a ranking such that within every display set, iff (for ), and moreover whenever . The goal is to identify the top-ranked version .
An admissible policy chooses, after each history , a distribution over display sets for the next consumer; it stops at a stopping time and selects . It is -accurate if for every it stops almost surely and ; a family is accurate if each is -accurate (Definition 2).
With and , Chernoff's information is
where is the set of preferences in with a different top-ranked version. The ordinal attraction (OA) preferences are , where is the rank of within .
The Myopic Tracking Policy (MTP, Algorithm 1) with threshold fits the OA ranking of maximum likelihood to the votes so far, stops when the generalized log-likelihood ratio against every OA ranking with a different top reaches , and otherwise shows the top- versions of the fitted ranking with probability , an explicit distribution given in (7).
There is a threshold such that
that is, for every choice of the initial display set the family is accurate and its worst-case rate is at most that of every accurate family. The goal states the shape of the result and does not fix the optimal value.
The theorem says that one fixed, computable policy is optimal against the hardest consumer population in a nonparametric class, without knowing the population. Its display rule is static and sparse: only the nested sets of top-ranked versions are ever shown. The value gives a closed-form benchmark for the number of consumers any reliable test must survey, and Proposition 2 shows it barely depends on . The lower bound (Theorem 1) is a change-of-measure argument that applies beyond this model, for example to identifying the top- versions or the full ranking.
The results are proved in the paper; none is formalized. A formalization would produce a reusable discrete framework for sequential testing with set-valued actions and categorical feedback (finite-history laws, stopping times, expected stopping times in ), a formal treatment of Chernoff-type max-min information over a choice-model class, and a machine-checked LP duality certificate for the optimal display distribution. It would also pin down the exact hypotheses: two printed statements need correction (see Formalization scope).
The class is infinite and nonparametric, so the usual best-arm identification arguments, which track an estimate of the true instance, do not apply directly: MTP only ever estimates within the OA family, even when the truth is not OA. The upper bound must show that the drift of MTP's log-likelihood process under an arbitrary is at least , which rests on the dominance structure of Lemmas 4–5 and on the optimality of the fixed distribution . The accuracy proof must control the error probability uniformly over with a threshold independent of and . Computing on OA preferences reduces to a linear program over all rankings with a different top, whose explicit primal and dual solutions require the identities of Lemmas 6–9.
Everything is finite or discrete and no measure theory is used. Versions are Fin K and rankings are Equiv.Perm (Fin K) with 0-based ranks (rank 0 is the top); the restricted rank stays 1-based. A preference is a function DS K → Fin K → ℝ. A policy is given by its display rule (a function of the history into ℝ≥0∞), a stopping predicate on histories, and a selection function; the law of a history is the explicit product , in , and , and all rates are in . Limits as are along 𝓝[>] 0. MTP's uniform tie-break enters as a mixture in the display rule; for stopping and selection do not depend on it.
Added hypotheses and readings, each disclosed in the items: (A-3) is required for only (as printed it is unsatisfiable at ); and ; ; (Algorithm 1's input); the initial display set is arbitrary. Theorem 1's first inequality is stated for , since it fails for close to . Theorem 6's final sentence (equality for OA preferences) is not formalized, since it fails for bounded thresholds. The constants of Lemma 10 and Theorem 7 are quantified after and before .
Trivializing formalizations are ruled out: Definition 1 is non-vacuous (an OA preference is shown to lie in ), the alternative sets require membership in , top-rankedness is tied to the (A-3) ranking, and the goal includes the accuracy of MTP. Without it, a tiny threshold would stop after one vote.
Not in scope: Theorem 2 (a different policy for finite classes), Propositions 1 and 3–7, Corollaries 2–3, and the numerical study. Contributions to any milestone are welcome. The finite-history probability layer and the lower-bound argument are reusable for other sequential identification problems.
Data marketplaces buy personal data from many individuals to estimate population statistics. Two features set such pricing apart from an ordinary procurement auction. First, each data owner has a private cost of sharing, so the buyer must design a menu of payments that elicits these costs truthfully. Second, data are correlated across people: an individual who refuses to share still loses privacy when similar people share. Liao, Su, Ziani, Wierman and Huang call the consequence the privacy paradox: privacy-conscious people may join a platform because abstaining does not protect them (arXiv:2105.14262, §1; published in Mathematics of Operations Research, 2024).
The paper asks how an analyst with a fixed budget should design such a mechanism when the goal is statistical: to estimate a population mean while trading off the bias caused by non-participants against the variance caused by sampling only some participants. The answer extends the optimal-auction framework of Myerson (Math. Oper. Res. 1981) and the data-procurement mechanisms of Roth and Schoenebeck (EC 2012) and Chen, Immorlica, Lucier, Syrgkanis and Ziani (EC 2018) to a setting with participation externalities and an adversarial correlation between data and costs.
Agents are split into groups . An agent in group has a cost drawn from a density on the support , with distribution function . At a fixed desired participation profile the privacy cost of a participant is with , a non-participant suffers , the gap is strictly increasing, and participants receive a benefit .
The analyst posts a menu: a selection probability and a payment for a reported cost . A participant with true cost who reports has expected utility
The menu is truthful if reporting maximizes this utility. An agent joins if some report gives utility at least , and the menu induces if the fraction of joining agents of group is for a threshold . The virtual cost is
For the statistical problem, Appendix C of the paper discretizes the costs and sorts all virtual costs of participants as , with cell probabilities summing to . Given agents, a budget , a constant collecting the participation terms, and a weight on the variance, the analyst chooses and an adversary chooses the data probabilities in the min-max program
subject to the budget , under the standing condition .
There are constants , , and a feasible, non-increasing allocation
such that for every feasible . The constants are left existential, as in the printed theorem; the case analysis that identifies them belongs to the milestones.
Theorem 1 is a participation-aware version of Myerson's characterization: it shows that the analyst loses nothing by restricting to monotone allocation rules with one explicit payment, and it pins down the payment that realizes a target participation rate. Theorem 2 then solves the analyst's worst-case bias–variance problem: the optimal selection probability is flat for cheap agents and decays like the inverse square root of the virtual cost for expensive ones. This shape explains when the mechanism can be strictly truthful (a strictly decreasing rule, Corollary 2, in the low-budget regime) and when only weak truthfulness is possible (a flat region, larger budgets).
The paper proves Theorem 2 for discrete costs and passes to continuous costs by letting the number of cells grow without bound, a step it asserts without proof. The mission formalizes the discrete theorem that Appendix C actually proves, together with both directions of Theorem 1. None of these results has a machine-checked proof yet.
The goal is a min-max statement about a program that is convex in the allocation and concave in the adversary's choice, with a coupled budget constraint. The natural first idea, to solve each player's first-order conditions and plug them into each other, does not by itself produce a solution: the analyst's best response clips at 1, the adversary's best response may be interior on some cells and at the boundary on others, and which cells are which depends on the budget. The paper resolves this by a case analysis on the ratio against the values of , with thresholds obtained from intermediate-value arguments, and each case requires its own multiplier and its own adversary strategy.
For Theorem 1 the obstacle is that the paper's envelope argument differentiates the allocation rule, while the theorem quantifies over all monotone rules, which need not be differentiable. The "only if" direction must be recovered from the convexity of the maximal utility as a function of the true cost.
All statements live in the namespace PrivacyParadox.Alloc and use one definitions file. The group layer fixes one desired profile, so , , and are functions of the cost or numbers; their dependence on participation rates and correlation strengths plays no role in Theorems 1–2. The discrete layer indexes cells by as the paper does, with real-valued data and Real.sqrt.
The formalization commits to the following conventions, each disclosed in the item it affects:
Two trivializing readings are excluded: the goal compares with every feasible allocation, so it is not the best-response property of Lemma 3, and it asserts the existence of rather than assuming an optimizer of the stated form.
A complete development needs elementary real analysis (interval integrals of monotone functions, Fubini on a triangle, the intermediate value theorem) and finite-dimensional convex optimization (first-order optimality for a concave quadratic on a box and for a separable convex program with one linear constraint). The latter two are reusable well beyond this mission. Proofs of milestones are welcome in any order. The continuous form of Theorem 2, Lemma 1 (the derivation of the objective from the Horvitz–Thompson estimator), Propositions 1–2 and Properties 1–4 are not part of the mission.
Many estimation problems in statistics, signal processing and machine learning ask for a low-rank positive semidefinite matrix: phase retrieval, matrix sensing, PCA-type problems and the Burer–Monteiro approach to semidefinite programs. A standard formulation is
and Riemannian optimization solves it by treating the feasible set as a smooth manifold. Two geometries are in common use. In the embedded geometry the set of rank- PSD matrices is a submanifold of with the Euclidean metric. In the quotient geometry one writes with a full-column-rank factor and optimizes over equivalence classes . Algorithms built on the two geometries behave similarly in experiments, and landscape results (absence of spurious local minima, strict saddles) have been proved separately for each. Luo, Li and Zhang (arXiv:2110.12121, Mathematics of Operations Research 2024) explain this by an explicit dictionary between the Riemannian gradients and Hessians of the two geometries. This mission formalizes their first main result, Theorem 3, for the full-rank factorization of PSD matrices.
Matrices carry the Frobenius inner product . The objective is twice continuously differentiable and symmetric, (the paper's standing assumptions); and are its Euclidean gradient and Hessian.
Embedded geometry. , viewed as . Its tangent space is the span of the tangent cone. The Riemannian gradient is the orthogonal projection of onto , and the Riemannian Hessian quadratic form is the derivative at along any curve in with , .
Quotient geometry. The total space is , the matrices of full column rank, with the objective (18a). A weight , smooth and symmetric positive definite, defines the metric . The vertical space is tangent to the orbit , and the horizontal space is its -orthogonal complement. Tangent vectors of the quotient are represented by horizontal vectors: is the horizontal part of the total-space gradient , and for horizontal , where is the Levi-Civita connection of (Koszul formula).
Comparison data. ; spans the top eigenspace of , , . For a quadratic form on a -dimensional space with inner product , is its -th largest eigenvalue relative to (). are the extreme singular values of an matrix.
If in addition for all orthogonal , then for every and ,
and if is a Riemannian first-order stationary point of (18a),
both Hessians have eigenvalues, and lies between and .
Theorem 3 says that at stationary points the two geometries see the same second-order landscape: the Hessians are congruent through , so their eigenvalues have the same signs and comparable magnitudes, with explicit factors depending on and the spectrum of . The paper derives from it (Corollary 1) that first-order stationary points, second-order stationary points and strict saddles correspond between the embedded and quotient formulations, so a landscape result proved in one geometry transfers to the other. The choice of weight (flat , right-invariant , or ) changes the comparison constants, which is how the paper relates the conditioning of the two approaches.
The result is proved in the paper; it is not formalized anywhere. A formal development adds machine-checked Riemannian gradients and Hessians on a concrete embedded submanifold and on a concrete quotient, a checked horizontal-space computation, and a reusable abstract sandwich theorem for max–min eigenvalues. Corollary 1 and the parallel results for the polar factorization and for general rank- matrices (Theorems 4–7) are natural follow-up missions on the same definitions.
The identities (19), (20) and (34) are matrix calculus once the geometric objects are pinned down; the difficulty is that the definitions are intrinsic. The embedded Hessian requires differentiating the tangent projection along the manifold, which produces the curvature term ; the obvious computation that ignores the moving tangent space gives the wrong Hessian. The quotient Hessian involves the derivative of the weight and needs the horizontal-space description of Lemma 4 to see that the projection in (5) can be dropped. Identifying of the tangent cone with the block form (14) needs an explicit chart of the rank- PSD set. The final sandwich requires a max–min (Courant–Fischer) argument relative to two different inner products, and the order of the bounds flips for negative eigenvalues.
EuclideanSpace ℝ (Fin a × Fin b) (Frobenius inner product) with matrix views toMat/ofMat. The weight takes values in in the same form so that is defined.ProjLikeRetr.Retractor.tangentSpace (span of the tangent cone) and ZORiem.RGD.rgrad (projected Euclidean gradient); "smooth embedded submanifold of dimension " is the published coordinate-slice predicate ProjLikeRetr.Retractor.IsSubmanifold k d, for every .Useful contributions include Mathlib-level lemmas on the tangent cone of the rank- PSD set, Courant–Fischer for a form relative to a non-standard inner product, and matrix-calculus lemmas for .