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?
Policy evaluation asks for the value of a fixed decision rule in a Markov decision process whose transition probabilities are unknown. It is the inner loop of policy iteration, the subroutine behind actor-critic methods, and the question an operator faces before deploying a policy in an inventory, queueing or routing system that can only be simulated. The simplest estimator is the plug-in (model-based) one: sample transitions from a simulator, build the empirical transition kernel, and compute the value of the policy in the resulting empirical MDP.
How many samples this estimator needs has a short history. Azar, Munos and Kappen (Machine Learning, 2013) introduced the total-variance argument that yields the dependence for planning with a generative model. Agarwal, Kakade and Yang (COLT 2020) proved minimax-optimal guarantees for model-based planning, but only when the sample size per state-action pair exceeds roughly . Pananjady and Wainwright (IEEE Trans. Inf. Theory, 2021) gave instance-dependent policy-evaluation bounds and a minimax lower bound, again under a sample-size requirement of order . Li, Wei, Chi and Chen (arXiv:2005.12900v8; Operations Research, 2024) removed this barrier: their Theorem 3 shows that the plug-in estimate is accurate across the whole accuracy range once the sample size exceeds up to logarithmic factors. This mission formalizes that theorem and the lemmas its proof rests on.
A discounted Markov decision process consists of a finite state set , a finite action set , a transition kernel (for each pair , is a probability vector over ), a reward and a discount factor . A deterministic policy is a map . Its value function is
Write for the state transition matrix of and for its reward vector, so that . For a vector , is the one-step variance of under the chain.
The generative model returns, for every pair , independent next states . The empirical kernel is , and for a policy chosen independently of the data the plug-in estimate is the value function of in the empirical MDP , that is, . Norms are maxima of absolute entries; and is natural.
There is a universal constant such that for every MDP as above, every fixed policy , every and every ,
The constant is not specified, so the goal survives any later improvement of the constants.
In attack order: Lemma 10 (elementary facts on , p. 23); the matrix form (27) of (p. 12); Lemma 11, for with (p. 24); the total-variance bound (70) of Azar et al. (p. 24); the deterministic instance-dependent bound (80) under a Bernstein-type condition (pp. 25–26); Lemma 2, the worst-case bound under the same condition (p. 15); the high-probability Bernstein bound (82) for a fixed policy (p. 27); and Lemma 1, the explicit-constant version of the goal with an instance-dependent refinement (p. 13):
with and .
The theorem says that the plug-in estimate of a fixed policy's value beats a random guess as soon as exceeds up to logarithmic factors, and that its sample size matches the minimax lower bound of Pananjady and Wainwright (2019, Theorem 2(b)) up to a factor over the full range . Lemma 2, which does not require the policy to be independent of the data, is the step the paper reuses to analyze the data-dependent optimal policy of the empirical MDP (Theorems 1 and 2, posed in sibling missions of this series).
The result is proved in the paper; none of it is formalized. The mission produces a machine-checked account of the variance-aware analysis of tabular MDPs: the resolvent calculus of Lemma 10, the total-variance bounds (70) and Lemma 11, which recur across the reinforcement-learning sample-complexity literature, and a high-order expansion argument that turns a Bernstein-type condition into an error bound. A formal proof of (70), which the paper quotes without proof, would itself be a reusable result.
The obvious argument writes and bounds the two factors separately. The resolvent of the empirical chain is correlated with the deviation , and bounding crudely by its row sums loses a factor that forces ; this is exactly the barrier in earlier work. Removing it requires controlling a whole sequence of auxiliary vectors , each defined through the variance of the previous one, up to a logarithmic depth, and showing that their norms do not blow up (Lemma 11). The Bernstein step must also use the variance, not the range, of ; a Hoeffding bound gives the wrong power of .
States and actions are finite types; the kernel is P : S → A → S → ℝ with P s a s' , a probability vector for each (s, a) (the published IsTransitionKernel). The standing setting is the predicate IsDiscountedMDP P r γ: a kernel, , , and nonempty state and action sets (, , p. 5). Policies are deterministic maps S → A; the value function is the published series PolicyValue of the induced point-mass policy. Vector norms are Mathlib's sup norm on finite function types, matching ; vector inequalities and square roots are entrywise.
The data set is the finite type of arrays of next states per pair, its law is the product of the kernel probabilities, and of an event is a finite sum. "With probability at least , " is stated as . The goal assumes , the standing assumption of the empirical kernel (3), which is implied by the sample-size condition since is nonempty. Index ranges "" range over the integers in that interval. The deterministic milestones (80) and Lemma 2 are stated for an arbitrary transition kernel , which is what their proofs use.
Three formalizations would trivialize the goal and are ruled out: computing from the true kernel instead of the empirical one; letting be chosen after the data are seen; and letting depend on , , , , or (the existential over precedes all of them).
A complete development needs: the matrix form of the value function, Neumann series and nonnegativity of ; variance identities for finite distributions; a Bernstein inequality for i.i.d. bounded categorical samples with a union bound over states and indices; and the algebra of the recursive expansion. The resolvent and total-variance lemmas are reusable for any tabular discounted MDP. Proofs of individual milestones are welcome independently; (70) is a standalone classical result.
Online matching platforms for dating, freelancing or ride sharing do not match agents themselves. They decide whom each agent gets to see and how often, and the agents then accept or reject. Immorlica, Lucier, Manshadi and Wei (arXiv:2102.09017, Management Science 2023) model this as directed search. The platform designs assortments, which are rates at which types of agents meet, and the agents play an equilibrium of the induced search game. The platform's design problem only makes sense if every choice of assortments leads to a single, well-defined equilibrium outcome. Otherwise "the welfare of an assortment" is not a function of the assortment. This is not automatic: even for simple asymmetric preferences under random meetings, multiple stationary equilibria can arise (Burdett and Coles 1997).
This mission formalizes that well-posedness result, Proposition 3.1(1) of the paper, together with the fixed-point and iteration lemmas of Appendix A.3 and Appendix B.3 on which its proof rests. It is the companion of the mission on the paper's quarter-approximation theorem (Theorem 4.1), which uses the same model.
The source is the arXiv v2 preprint (18 Aug 2021). The Management Science version may number results differently.
There are finitely many agent types on each side of the market, a set and a set , with . Agents of every type leave the market unmatched at a life-event rate , and type arrives at rate . When an agent of type meets an agent of type , the pair draws one utility . Valuations are symmetric: both agents receive if they match, and . Each is a probability law on with no atoms (a "continuous distribution").
An assortment for type is a family of rates at which type- agents meet type- agents on the opposite side. Under a threshold strategy with threshold , a type- agent accepts a meeting if and only if . A meeting turns into a match when both agents accept, i.e. when . If every type plays a threshold strategy, the expected utility of a type- agent is (equation (5))
A type's own threshold enters its own utility through .
One type's equation. Fix the thresholds of the opposite types. Write for the right-hand side of (5) with replaced by . Lemma A.3 states that has exactly one solution. The best-response map of Appendix A.3 sends a profile to the profile in which each type's new threshold is that solution, computed against the opposite side's thresholds in . A best-response sequence starts at the all-zero profile and applies this map repeatedly.
For any fixed assortments there is exactly one threshold profile with
Uniqueness ranges over all real profiles.
Proposition 3.1 is what makes the platform's problem OptimalDirectedSearch well defined. Assortments determine a unique threshold profile. That profile determines the matching rates (Lemma 3.2) and, through stationarity, the population masses. Welfare is then a function of the assortments, and the program (6) used for Theorem 4.1 encodes exactly this fixed point as its incentive constraint (6e). The constructive proof also yields an algorithm: iterate best responses from zero, and the iteration stops after rounds.
Formalizing it adds three things beyond the paper. First, a checked version of an argument the paper gives informally, including the odd/even sandwich of the iteration, which the paper proves in a few lines. Second, a reusable fixed-point and unimodality lemma for ratios of tail integrals, , which recurs in reservation-value arguments in search theory. Third, an exact accounting of the hypotheses: integrable utilities and the reading of the best-response map. To our knowledge none of these results has been machine-checked.
The obvious route to uniqueness, a contraction argument for the map , fails. That map is neither monotone nor contractive in general, since raising a type's own threshold can raise or lower its utility. Existence by Brouwer's fixed-point theorem gives no uniqueness and no algorithm. The best-response iteration does not converge monotonically either: its odd and even iterates move in opposite directions, so convergence in finitely many rounds is a combinatorial statement about the order of the thresholds, not a limit argument. A formal proof also needs continuity and monotonicity of tail integrals of atomless laws, which Mathlib provides only in pieces.
The two sides are separate finite types M and W. A threshold profile is a pair of functions (M → ℝ) × (W → ℝ), ordered componentwise. A market records , and the laws F m w : Measure ℝ. The standing assumptions are:
NullSingletonClass);Tails are and . Capacity (2), flow balance (3) and stationarity (1) are not hypotheses, because Proposition 3.1 holds for any fixed assortments.
The best-response map is encoded as a relation: each new threshold solves its own equation against the opposite side's input thresholds. This is the paper's reading ("This map is a best response by Lemma A.3"). Evaluating (5) at the old profile, own old threshold included, would be a different map. Under that reading finite convergence and the p. 37 claims are false: with one type per side, , and uniform on , its iterates are rational and converge only in the limit to .
Two formalizations would trivialize the goal, and both are ruled out. Uniqueness is over all real profiles, not only nonnegative ones or those reached by the iteration. The tail integrals are not allowed to vanish by default for non-integrable laws, because integrability is a hypothesis. is encoded with a constant chosen before the market.
Not formalized: the agents' Markov decision process of Appendix A.1. Consequently "this strategy profile is a Nash equilibrium", item 2 of Proposition 3.1, Lemmas A.1–A.2 and the best-response sentences of Lemma A.3 and Proposition A.4 are out of scope.
Contributions welcome: continuity and monotonicity lemmas for and for atomless integrable laws, which are reusable well beyond this mission, and proofs of the milestones in any order.
In many auctions a bidder's value for what she wins depends on information held by others. The value of an oil lease, a spectrum licence or a piece of art to one bidder depends on survey data, market forecasts or expert opinions that other bidders hold privately. The model of interdependent values (Milgrom and Weber, 1982) captures this: each agent holds a private signal , and every agent's value is a publicly known function of the whole signal profile .
With interdependent values, maximizing welfare in ex-post equilibrium is impossible unless the valuations satisfy the single-crossing condition (Maskin, 1992; Dasgupta and Maskin, 2000), and even single crossing does not suffice beyond single-item auctions with single-dimensional signals. Without any condition, there are valuations for which no deterministic mechanism achieves a bounded approximation ratio and no randomized mechanism does better than a factor (Eden, Feldman, Fiat and Goldner, ACM EC 2018; Examples 1.2–1.3 of the source). Eden, Feldman, Fiat, Goldner and Karlin (arXiv:1903.08384v2, 2019) introduce submodularity over signals (SOS): raising one signal increases a value by less when the other signals are higher. They show that SOS valuations admit constant-factor, or signal-space-dependent, approximations in settings where single crossing fails, including combinatorial auctions. This mission formalizes their Theorem 6.1, the case of combinatorial auctions with single-dimensional signals taking values.
Timeline. Milgrom–Weber (1982) introduce the interdependent values model. Maskin (1992) and Dasgupta–Maskin (2000) show that single crossing makes efficient auctions truthful. Jehiel–Moldovanu (2001) show that efficient implementation fails generically with multidimensional signals. Eden–Feldman–Fiat–Goldner (2018) give approximations under a relaxed, -single-crossing condition, with ratios depending on and . Eden–Feldman–Fiat–Goldner–Karlin (2019; Mathematics of Operations Research, 2024) introduce SOS and prove Theorems 4.1, 5.1, 6.1 and 6.5.
There are agents and items, and signal values. Each agent has a signal , and is the grid. Agent 's value for a bundle at the profile is ; the empty bundle is worth , and for nonempty , is weakly increasing in every signal and strictly increasing in . We write for the profile with agent 's signal replaced by , and for the profile that keeps the signals of the agents in and sets those in to .
A function of the profile is SOS if for every coordinate , all with , and grid profiles with coordinatewise,
The setting is SOS when every is.
A feasible allocation gives disjoint bundles ; its welfare at is . A deterministic mechanism maps reported profiles to an allocation and payments. Agent 's utility is her value, at the true profile, for the bundle she receives at the reported profile, minus her payment. The mechanism is ex-post IC if truthful reporting maximizes each agent's utility whenever the others report truthfully, and ex-post IR if that utility is nonnegative. A randomized mechanism is universally ex-post IC-IR if every deterministic mechanism in its support is.
The mechanism k-HL runs, with probability , Random Threshold: choose uniformly in , call the high agents, allocate to them a feasible allocation maximizing , and charge agent receiving the price . Otherwise it runs Random Sampling: split the agents uniformly at random into and , allocate to a feasible allocation maximizing , and charge nothing. In the Lean development (namespace InterdepSOS.KHL) these are rtAlloc, rtPay, rsAlloc and khlWelfare.
For SOS valuations with signal values, every Random Threshold component and every Random Sampling component is ex-post IC and IR, and for every grid profile and every feasible allocation ,
where the expectation is over , over and over the coin choosing between the two mechanisms, and welfare is measured with true values at the truthful profile.
Theorem 6.1 is the paper's answer for general combinatorial auctions with single-dimensional signals and arbitrary bundle valuations, a setting where single crossing gives nothing and where the random-sampling technique of the single-parameter case (Theorem 4.1) is not enough on its own: Random Sampling alone covers only the contribution of the other agents' signals. The ratio depends on the size of the signal space but not on the number of agents or items. The same decomposition, with Random Threshold replaced by a bucketing mechanism, yields the -approximation for strong-SOS valuations (Theorem 6.5), so milestones 1 and 5 are shared by both results.
The result is proved in the paper; no machine-checked version is known to exist. A formalization fixes the incentive argument precisely (which data the allocation may depend on, how ties are broken) and makes the uniform averages over thresholds and partitions explicit. The development reuses the Key Lemma 3.1 of the paper, which is posed in a sibling mission of this series.
Two points resist a direct argument. First, incentive compatibility of Random Threshold requires that a high agent who changes her report within leaves the allocation unchanged, and this is true only if the argmax rule sees the reports through the proxy data alone: an argmax rule that breaks ties using the full report profile can make a high agent's bundle, and hence her utility, depend on her report. The formalization must therefore state precisely what the allocation rule may depend on. Second, the welfare bound for Random Sampling rests on the Key Lemma 3.1 (zeroing a uniformly random half of the other signals keeps, in expectation, half of an SOS value), which here has to hold on the discrete grid , with SOS assumed only there; the expectations over partitions and thresholds are finite averages whose bookkeeping (agents in receive nothing, agents outside receive nothing) must match the mechanism exactly.
Agents are Fin n, items Fin m, bundles Finset (Fin m), signals natural numbers with the grid condition InGrid k s. All hypotheses on valuations (nonnegativity, monotonicity, strict monotonicity in the own signal, SOS) are imposed on grid profiles only, with the shifted coordinate staying below ; a condition on all of would be stronger than the paper's. The empty bundle is worth and the monotonicity clauses concern nonempty bundles. Allocations are maps Fin n → Finset (Fin m) with pairwise disjoint values; agents outside the eligible set receive .
The argmax allocations are produced by arbitrary selectors, functions of the threshold (or of ) and of the proxy profile, required to return a feasible maximizer of the proxy welfare; the theorems quantify over all such selectors. Expectations are finite uniform averages, and , never an existential or universal quantifier over or . The ratio is stated against every feasible allocation, with welfare at true values, never with proxy values and never through a supremum. IC and IR are stated for every component of the mixture, with the paper's explicit payments. Random Sampling zeroes the signals of all of , the agent's own included (the page's "" is read as ). For , and the threshold average is the empty sum.
Lemmas 6.2 and 6.3 and displays (6)–(7) are stated for every feasible allocation (every assignment, for (6)–(7)), which is stronger than the paper's statements for a welfare-maximizing .
Needed infrastructure: the Key Lemma 3.1 on the discrete grid, finite averages over subsets, and a lemma that a maximizer over a subfamily of allocations dominates any restriction of a feasible allocation. Contributions of proofs of the milestones in any order are welcome; the IC-IR milestones are independent of the welfare milestones.
The source is the arXiv preprint arXiv:1903.08384v2; the Mathematics of Operations Research (2024) version is not the cited source, and its numbering may differ.
Many allocation problems distribute chores: tasks, shifts, teaching duties or cleaning rotas that every recipient would rather avoid. Agents often have unequal obligations, for example a full-time and a part-time worker, and a fair division should respect these entitlements. When the tasks can be split (time shares, probabilities), the competitive rule of Bogomolnaia, Moulin, Sandomirskiy and Yanovskaya (Econometrica 2017) is the standard answer: chores are priced, each agent must "earn" a prescribed amount by taking on chores, and each takes the least unpleasant bundle that earns it. The resulting allocation is efficient and envy-free with respect to the entitlements.
Most chores cannot be split. Then exact envy-freeness or proportionality may be impossible (for instance with fewer chores than agents), and the literature asks for relaxations "up to one chore". For goods, Barman and Krishnamurthy (AAAI 2019) showed how to round a competitive allocation into an indivisible one that is Pareto efficient and approximately fair. Brânzei and Sandomirskiy (arXiv:1907.01766v2, §7; Mathematics of Operations Research, 2024) transfer this rounding to chores with arbitrary weights. This mission formalizes that result, Theorem 34 of the paper.
There are agents and chores. A bundle is a vector ; an allocation is a matrix , agent receiving the bundle ; it is feasible if for every chore . Values form a matrix , and agent 's utility is additive, . The utility profile of is , and is the set of utility profiles of feasible allocations.
At prices a bundle costs . Given budgets , a feasible allocation is competitive at (Definition 3) if every agent's bundle satisfies and maximizes among all bundles with . It is Pareto optimal (Definition 5) if no feasible allocation makes every agent weakly and some agent strictly better off; the Pareto frontier is the set of their utility profiles. The Nash social welfare of is .
An allocation is indivisible if every ; then is identified with a set of chores, and . Fix weights .
For every and there is an indivisible allocation with
Pareto optimality is in the divisible problem: is compared with all fractional allocations.
The proof also uses two results of the paper that are formalized in the companion mission Algorithms for Competitive Division of Chores 1: the First welfare theorem (Theorem 9, item 1, p. 14) and the characterization of competitive allocations by minimum pain-per-buck chores (Lemma 36, p. 50). They will be linked as reference milestones once published.
Theorem 34 says that weighted envy-freeness up to one chore, weighted proportionality up to one chore and Pareto efficiency are compatible for indivisible chores with arbitrary entitlements. Envy-freeness alone can be achieved by simple procedures, but those allocations are typically inefficient; the theorem shows that efficiency need not be given up. Its proof produces the allocation from a divisible competitive allocation, which makes the competitive rule a single source for both divisible and indivisible fair division of chores. The paper also gives a strongly polynomial algorithm when or is fixed; that part is not in scope here.
The result is proved in the paper, partly by reference to Barman and Krishnamurthy for goods and to Bogomolnaia et al. for existence. No machine-checked version of it, of the competitive rule for chores, or of the rounding procedure is known to exist. The formalization would make all three available, and would make the deduction of Theorem 34 from Theorem 35 precise: as written, that deduction needs a chore outside agent 's bundle, which the statement of Theorem 35 does not provide.
The main obstacle is existence. For goods, competitive allocations maximize the Nash social welfare over the whole feasible set, a convex program. For chores the set of competitive allocations can be disconnected; their utility profiles lie on the Pareto frontier and are critical points of Nash welfare on the feasible utility set. Maximizing the Nash welfare over the feasible set does not characterize all of them, and the frontier itself has to be handled as a polyhedral surface.
The rounding is combinatorial: it needs an acyclic consumption graph, a forest of agents and chores, which is traversed from roots to leaves. The bounds (12) and (13) come from an invariant of that traversal, not from a local exchange argument.
Agents are Fin n and chores Fin m, both 0-based. Values v : Fin n → Fin m → ℝ and budgets b : Fin n → ℝ carry the sign hypotheses v i j < 0, b i < 0 in each theorem, not in the definitions, because Theorem 35 applies Definition 3 to budgets . Competitiveness at prices requires , the budget constraint and optimality among all bundles in within the budget. An indivisible feasible allocation is a map σ : Fin m → Fin n, its 0/1 matrix is indicator σ, and bundles are Finsets. Graphs are edge sets Finset (Fin n × Fin m); acyclic means no simple cycle with at least two agents. Weights are arbitrary positive reals, never normalized.
Added hypotheses: in the goal (with no agents and chores no allocation exists), and , in the existence milestone (with no bundle meets a negative budget). The running-time statements of Theorems 34 and 35 are not formalized.
The trivializing readings are excluded: competitiveness always includes the budget constraint; values and budgets are strictly negative, not non-negative; Pareto optimality of the goal is with respect to all fractional allocations, not only indivisible ones; and (10) ranges over all ordered pairs of agents and all chores .
A complete development needs the existence theorem for chores (via the critical-point characterization of Theorem 7 or a fixed-point argument), the minimum pain-per-buck characterization of competitive allocations, cycle elimination in consumption graphs, and the forest traversal of Algorithm 3. The definitions of competitive allocations, Pareto frontier and weighted EF¹₁/Prop1 are shared with the companion mission and reusable for other fair-division results. Proofs of any milestone, and alternative proofs of the existence theorem, are welcome.
Dividing indivisible goods among agents with different preferences is a central problem of fair division, with applications from inheritance and course allocation to the assignment of compute or shared resources. The standard fairness notion for indivisible goods is envy-freeness up to one good (EF1), introduced by Budish (2011): no agent prefers another agent's bundle once a single good is removed from it. EF1 allocations always exist for additive valuations, and the simplest algorithm that finds one is Round-Robin: the agents take turns in a fixed order, and each picks her favourite remaining good.
That guarantee assumes the algorithm knows the agents' true values. A mechanism only sees what the agents report, and Round-Robin is not truthful: an agent can gain by claiming that a good she likes moderately is her favourite, because she knows nobody else will take the good she likes most. Amanatidis, Birmpas, Christodoulou and Markakis (EC 2017) showed that already for two agents no truthful mechanism without payments can always produce EF1 allocations once there are more than four goods. Amanatidis, Birmpas, Fusco, Lazos, Leonardi and Reiffenhäuser (WINE 2021; Mathematics of Operations Research, 2024) therefore ask a different question: if agents bid strategically and reach a pure Nash equilibrium, is the resulting allocation still fair with respect to their true valuations? For Round-Robin the answer is yes, and this is the paper's main technical result.
Timeline:
There are agents and goods . Agent has a non-negative value for every good, and her value for a bundle is the sum . Values may tie and may be zero.
Each agent reports a bid vector . Round-Robin (Mechanism 1) processes the agents in the order ; the active agent receives the available good with the highest bid in , ties broken in favour of the good with the lower index, until no good is left. So it runs rounds and the last one may be incomplete. It returns an allocation .
The bid is a best response to the others' bids if no other bid vector gives agent a bundle of larger true value . A profile is a pure Nash equilibrium (PNE) if every bid is a best response. An allocation is EF1 if for all with there is with , and EF from 's perspective if for all .
For every instance and every PNE of Round-Robin,
The milestones follow the paper's argument:
The two-agent case, Theorem 3.2, has its own short proof and is included as a companion statement.
The result. Theorem 3.3 shows that a simple, non-truthful mechanism keeps its fairness guarantee under strategic play. Every stable outcome of the bidding game is EF1 for preferences the mechanism never sees. Round-Robin has a PNE in every instance (Theorem A.3, a separate mission of this series), so the guarantee is never vacuous. Theorem 3.4, the statement about the first mover, is of independent interest: it is the strategic analogue of the classical fact that the first agent in Round-Robin envies nobody. The run-comparison Lemma 3.7 is a general tool for sequential allocation mechanisms.
The formalization. The theorem is proved in the paper; it has no machine-checked proof. Formalizing it requires a precise model of Round-Robin with lexicographic tie-breaking, best responses over the continuum of bid vectors, and a careful treatment of ties in valuations. The paper's appendix handles ties with a perturbation argument whose published construction has a gap, so a formal proof also settles that step.
The obvious approach does not work for . With two agents, envy-freeness and proportionality coincide: a non-EF1 allocation leaves an agent with less than half her value, and deviating to her truthful bid would guarantee half (Lemma 3.1). With three or more agents, an agent who envies another agent's bundle may still hold her proportional share, so no single deviation is obviously profitable. One would like to argue that a best response is "at least as good as truth-telling", but the best-response bundle and the truthful bundle are not comparable good by good.
The paper instead replaces a best-responding first mover by an imaginary truthful agent with the same view of the same allocation (Lemma 3.5). The construction is recursive, round by round, and requires controlling how a run of Round-Robin changes when one agent's ranking changes. That is the content of Lemma 3.7, whose induction needs Claim 3.8 to exclude the one bad configuration. Ties in valuations need a further perturbation argument (Lemma A.1).
Agents are Fin n with [NeZero n], goods are Fin m, both 0-based; agent 1 is 0 and picks first. Valuations and bids are real functions Fin n → Fin m → ℝ, with non-negativity stated as hypotheses; bundle values are finite sums, so additivity holds by construction. Round-Robin is defined step by step. At each step, the agent whose turn it is takes the first available good in the stable sort of the goods by non-increasing bid, which is the lexicographic tie-breaking of Mechanism 1. The definition is generalized to a start agent and a good set (rrFrom s G), so that Mechanism 1 is rrFrom 0 univ and the Round-Robin of p. 10 is rrFrom ℓ (M \ H), wrapping around after agent . Lemmas 3.1, 3.5, 3.7, A.1, Claim 3.8 and Theorem 3.4 are stated in that generality, with agent in the role of agent 1; the page states the instance , . The goal is stated for Mechanism 1 only.
Deviations in the best-response predicate range over every non-negative bid vector, not over rankings, truthful bids or a finite menu. Restricting them would weaken the PNE hypothesis and change the theorem. EF1 is measured with the true valuations, never with the bids. Ties are broken lexicographically; an "any tie-breaking" Round-Robin would be a different, nondeterministic mechanism. The goal assumes no strict values, no positive values, no distinct bids and no divisibility .
Lemma A.1 is posed in the reading its proof supports: the profile is fixed before the perturbed valuation is chosen. Read with one valuation for all profiles, the lemma is false.
The development needs only finite sums and finite sets from Mathlib. Contributions to the general run-comparison machinery (how pick and allocBefore behave under a change of one agent's ranking or of the start agent) are reusable for the companion mission on existence of equilibria and for other sequential mechanisms.
Linear programming and two-player zero-sum matrix games are two faces of one theory. Von Neumann's minimax theorem is a statement of LP duality, and conversely, since Dantzig's 1951 note, every linear program can be rewritten as a zero-sum game. The equivalence matters in practice whenever an algorithm is much better at one of the two problems. Game solvers based on multiplicative weights and sampling, such as the randomized algorithm of Grigoriadis and Khachiyan (GK95), approximate the value of an game in time sublinear in the size of the matrix. Carmon, Duchi, Sidford and Tian (arXiv:1903.02675) and van Apeldoorn and Gilyén (arXiv:1904.03180) use such game solvers, classical or quantum, as linear-programming solvers. For that to work, the reduction from a linear program to a game must be explicit, with the exact error budget that the game solver has to meet.
This mission formalizes that reduction as it is stated in §4 of van Apeldoorn and Gilyén (2019), Lemma 12 (p. 14). The paper uses it to turn its quantum zero-sum game solvers into quantum LP solvers with cubic dependence on (Theorem 13, p. 15).
The linear program. Let , and . The primal LP (4) and its dual (5) are
The paper's standing assumptions (p. 12) are:
The game. In a zero-sum game with payoff matrix , the column player picks a mixed strategy in the standard simplex , and the row player picks the row with the largest payoff. The value of the game (LP (1), p. 2) is
The reduction. Fix a threshold . With the all-ones vector of length , the game matrix (6) acts on the variables (the original variables, one slack variable and one homogenizing variable):
Write for its value, and set the error level .
For every , every threshold with , and every estimate with ,
This is the paper's "finding the optimal value of the game (6) up to additive error suffices to correctly conclude either or ", with the decision rule its proof uses.
The goal splits into the two exact implications of the proof:
The milestones follow the printed proof, all on p. 14:
The result. Lemma 12 is the bridge that makes any approximate zero-sum game solver an approximate LP solver. It turns the question "is ?" into a single approximate value computation, and binary search over (p. 12) then locates to additive error . The constant is the price of the reduction. It fixes how accurately the game must be solved, and therefore the and factors of Theorem 13. The same reduction appears, in other forms, in classical sublinear LP solvers.
Formalizing it. The lemma is proved in the paper; this mission produces a machine-checked version with every constant explicit. That is not a formality here. As printed, the second row of (6) is , and with that row the lemma is false: for , , , , , and , one has but . The derivation on p. 13 gives , which the mission uses. Step (7) of the proof is written for and needs in general. The mission states the lemma with both repairs, so that later LP-solver formalizations can cite an exact statement. To our knowledge no machine-checked version of this reduction exists.
Each step is elementary, and the difficulty is bookkeeping. The game value is an infimum over the simplex, and the second case needs a strategy that actually attains it, or an approximation argument with slack. The homogenizing variable is pinned only approximately: an approximately optimal strategy satisfies only up to . That error is multiplied by and , whose signs are arbitrary, so the inequalities that look natural for nonnegative data fail for negative or . The relaxed constraints then pass through weak duality, where the dual bound enters, and the errors have to add up to exactly . A reading with would cover only half of the binary search.
Data. is Matrix (Fin n) (Fin m) ℝ, is Fin m → ℝ and is Fin n → ℝ: constraints are indexed by Fin n and variables by Fin m, as in (4). The paper's index letters in §4 vary.
Standing assumptions. A structure LPStanding A b c R r OPT collects them:
The last item is the paper's assumption of strong duality, in the form its proof uses. It is a hypothesis, not a theorem to derive.
The game. The matrix (6) has rows Fin 2 ⊕ (Unit ⊕ Fin n) and columns Fin m ⊕ Fin 2 (with = inr 0 and = inr 1), and its second row is the corrected .
The value. The value is sInf of the image of stdSimplex under . It is not an infimum over a membership proposition, which in Lean would return and make the first case vacuous. LP (1)'s side constraint is omitted because it is inactive for entries in .
Constants. exactly, with .
Added hypothesis. is the one hypothesis not written in the lemma. §4 supplies it through the binary search range, and through the requirement that (6) be a game with entries in .
Trivializing formalizations are ruled out. LPStanding is satisfiable, the second row forces , the value is not junk on a positive game, and the goal is stated for every estimate within rather than only at . A sanity file checks the first three on small instances.
Infrastructure. Everything is built from Mathlib's stdSimplex, Matrix.mulVec and dotProduct. The attainment of the value of a finite matrix game (milestone exists_strategy_le) and weak duality with relaxed constraints are reusable beyond this mission. Proofs of any milestone are welcome, and so are alternative proofs of the second case that avoid attainment by a slack argument.
In large data centres, an incoming task often cannot run on every server: its data, software or licences sit on only some of the machines. Such strict compatibility constraints are modelled by a bipartite graph between task types (dispatchers) and servers. For the fully flexible system, in which every task can go to every server, the JSQ() policy (sample servers at random and join the shortest queue) is described in the large-system limit by the mean-field ODE of Vvedenskaya, Dobrushin and Karpelevich (1996) and Mitzenmacher (1996). Rutten and Mukherjee (arXiv:2008.07562, Math. Oper. Res. 2023) identify two graph conditions, proportional sparsity and subcriticality, under which JSQ() on a sparse compatibility graph has the same mean-field limit and the same steady state as the fully flexible system (their Theorem 3.4).
The two conditions are useful in system design only if there are natural graph families that satisfy them. A storage designer controls the server degree: the number of task types a server can process is roughly proportional to the data it must store. Theorem 3.5 of the paper answers this design question for random graphs. If every server stores data for task types chosen uniformly at random, then together with a mild density condition suffices, even when is negligible compared with the number of task types. This mission formalizes Theorem 3.5's graph-theoretic content and the chain of lemmas in Appendix A that proves it.
A system with servers and dispatchers has a compatibility graph with . The neighbourhood of a dispatcher is ; that of a server is .
Proportional sparsity (Definition 3.1): for every ,
In words, for every set of servers, all but a vanishing fraction of the dispatchers see in roughly the proportion .
Subcriticality (Definition 3.3) with sample size : there are probability distributions on the sets such that
Think of a static policy that routes a task arriving at to a server in a sampled set according to . The condition says that no server receives more than its fair share of load. Its uniform-weight special case is condition (A.19):
The random graph. Let . For each , each server independently chooses its neighbourhood uniformly among the -subsets of , so every server has degree exactly . All graphs live on one probability space, but only the law of each is prescribed; the joint law across different is arbitrary.
If and , then almost surely
The result. Theorem 3.5 shows that the performance of the fully flexible JSQ() system, in the mean-field limit and in steady state, can be achieved with a server degree that grows arbitrarily slowly. The only requirement is that each dispatcher's mean degree grow faster than . Each server then needs to store data for only task types, a vanishing fraction of the types. The threshold matches the scale below which some dispatchers have too few neighbours to share the load evenly.
Formalizing it. The result is proved in the paper, and no part of it has been machine-checked. The mission produces reusable statements about random bipartite graphs with fixed left degree: hypergeometric concentration over all large dispatcher sets, the degree lower tail, and a Borel–Cantelli argument without independence across . It also produces a deterministic reduction from subcriticality to (A.19). That reduction is shared with Theorem 3.6 of the same paper (inhomogeneous random graphs). The printed proof of Lemma A.5 has a gap: (A.23) bounds the probability that some dispatcher has low degree by , but the union over dispatchers gives . This is not summable when grows faster than every polynomial, which the hypotheses allow. A complete formal proof must close this gap or show that low-degree dispatchers contribute too little to matter.
Every statement is almost sure along the whole sequence, but the graphs for different may be coupled arbitrarily, so no strong law over is available. Each a.s. claim needs a failure probability that is summable in , followed by the first Borel–Cantelli lemma. Proportional sparsity quantifies over all server sets , and Lemma A.2 over all dispatcher sets . The obvious argument would concentrate each separately and take a union bound. It fails because is only of order , which may be far smaller than and , so per-dispatcher tails cannot absorb an or union. Uniform control over all large sets (Lemma A.2) is therefore the crux. For subcriticality, the difficulty is that the maximum over runs over servers while the minimum degree runs over dispatchers.
Fin N, dispatchers Fin (M N); a graph is a Finset (Fin N × Fin (M N)), and a random graph is a measurable random adjacency matrix Fin N → Fin (M N) → Bool (the space of p. 13).Tendsto … atTop atTop). is Real.log, so the ratio is at , which does not affect a limit.Finset.powersetCard, and Borel–Cantelli for eventually-uniform statements over families of finite sets.On reward-based crowdfunding platforms such as Kickstarter, a project creator fixes two numbers before launch: the pledge level , the amount a backer commits, and the campaign duration . Both are set once and cannot be revised. A higher pledge earns more per backer but turns away backers whose valuation falls short, and a longer campaign reaches more backers but makes them wait longer for a project they value less the further away its delivery is. Zhang, Savin and Veeraraghavan (Revenue Management in Crowdfunding, Manufacturing & Service Operations Management, 2022; manuscript SSRN 3065267) model this trade-off with two kinds of backers. Independent backers decide on their own valuation. Herding backers arrive in proportion to the pledges already collected, so early success attracts more pledges. The paper asks when the creator should exploit herding and when it should ignore it.
This mission formalizes the paper's answer in the simplest setting it treats: every independent backer values the project at the same , and every herding backer at the same .
A campaign has a population of independent backers, who arrive at rate times the number still to come. Every backer discounts the project's value at rate : a backer arriving at time with valuation pledges if and only if . Herding backers arrive at time at rate times the number of pledges so far, where is an arrival rate and a propensity to pledge, and they pledge under the same discounted-value rule. Valuations lie in and enter only through the survival functions and of the two valuation laws.
The paper solves the pledging dynamics in closed form (its Propositions 1 and 2). The numbers of pledging independent and herding backers at time are
The total number of pledges is , and the creator's problem (18) is
With identical valuations, for and for , and likewise with , where . Proposition 6 adds the constraint , under which every independent backer pledges from the start.
Let , , and set , , and
If and , then on Proposition 6's feasible set the unique maximizer of is
Proposition 6 separates two regimes. When herding backers value the project at least as much as independent ones, the optimal campaign is short, , and its pledge is at least . When herding is weak () and independent backers value the project enough more than herding ones, the creator's best response is to price herding backers out entirely and run the campaign that would be optimal if no herding backer existed. The threshold (33) quantifies "enough more". Together with Proposition 3(b), which fixes the duration and finds that the optimal pledge sits exactly at the highest level that keeps every independent backer in from the start, these results give a creator explicit rules rather than a numerical optimization.
The paper states that the proofs of Propositions 3 to 7 are in an online Technical Appendix, which is not part of the manuscript this mission cites; the manuscript's own Appendix proves only Propositions 1 and 2 and Corollaries 1 and 2. None of the results has a machine-checked proof. Formalizing Proposition 6(ii) would supply a verified proof of a result whose published proof is not in the source held here, and would check the threshold (33), whose grouping of terms is read off the typeset page.
The objective is defined through nested integrals of step functions, so it is not differentiable everywhere: the jumps of and put kinks in where and where or , at which a backer type starts or stops pledging during the campaign. Setting a gradient to zero does not identify the optimum. The obvious argument for the goal, that herding backers do not pledge at and so the no-herding optimum is optimal, compares only campaigns that exclude herding backers; it says nothing about the campaigns with a lower pledge level that do attract them. Those campaigns gain a herding term growing exponentially in times the time during which herding backers pledge, and the comparison must hold uniformly over the whole feasible region, which is what the threshold (33) is for. Uniqueness, not only optimality, must also be shown.
All objects live in the namespace CrowdfundRM.Identical. Parameters form a structure Campaign with fields Ihat, k, r, Lh (for ), q, vbar, Fbi, Fbh. The standing assumptions, implicit in the paper, are , , and that each survival function is nonincreasing, takes values in , equals below and from on. Identical valuations set , to the step functions above with .
Conventions: real numbers throughout; the pledge counts are the closed forms (5) and (11); the feasible set of (18) adds , which requires; "the optimal" is the unique maximizer over the stated feasible set, and Proposition 6(i), which does not claim uniqueness, asserts that a maximizer exists and bounds every maximizer; "sufficiently long" in Proposition 3(b) is an unspecified threshold ; is added in Proposition 6(ii) because and divide by . The paper's has an undefined and is read as . In (33) the factors and multiply only the first bracket.
The following formalizations would trivialize the targets and are ruled out: defining by the explicit formulas (14)–(15) or by the paper's single formula (17) instead of (5) and (11); stating optimality through sSup or a first-order condition; stating Proposition 6(i) for maximizers without asserting that one exists; and stating Proposition 3(b) with a chosen threshold or with Proposition 6's narrower feasible set. The pledging differential equations themselves and their solution (Propositions 1–2) are formalized in the companion mission on triangular valuations; this mission works from their closed forms.
Infrastructure needed: interval integrals of monotone step functions, the exponential, logarithm and real power from Mathlib. Explicit evaluation of the nested integrals under step laws (Corollary 1) is reusable for any proof in this model. Contributions are welcome on each milestone and on lemmas such as continuity of on the feasible set and the closed form of in each region of .
In hiring, admissions and procurement, candidates are often judged by scores that are known to be biased: two candidates from different groups, schools or evaluation pipelines cannot be compared by their observed scores, while two candidates from the same pipeline can. Salem and Gupta (SSRN 3444283, published in Management Science, 2023) model this situation as a poset secretary problem. The decision maker sees only a partial order between candidates, namely the comparisons that are trustworthy, and must still make irrevocable online selections.
The classical secretary problem and its -selection variant (Kleinberg, 2005) assume a total order. With only partial comparisons, the natural question is how much the missing comparisons cost. Salem and Gupta answer it in terms of the width of the poset. This mission formalizes their lower bound: no algorithm can do better than a factor of the width.
A finite set of candidates carries a partial order . Each candidate has a true score . The scores are nonnegative and pairwise distinct, and they are consistent with the order: implies . The pair is an instance. Candidates arrive in uniformly random order. An algorithm knows and a capacity , observes the comparisons of among the candidates that have arrived, and selects at most candidates, irrevocably. It never observes the scores.
The offline optimum is
An algorithm is -competitive if on every instance (Definition 3.4).
The width of is the largest number of pairwise incomparable candidates (an antichain).
Because an algorithm sees only the poset and the arrival order, on a fixed poset its randomness (arrival order and internal coins) induces a probability distribution on the selected set, supported on sets of at most elements, and does not depend on the scores. Such a is called a selection rule with capacity . Its expected score is . The selection probability of is .
The instance of the lower bound is : disjoint chains of elements each, with elements in different chains incomparable (Figure 8 of the paper, with ).
For every and there is a poset of width such that for every selection rule with capacity and every there is a consistent scoring with and
Equivalently, for every algorithm, , the supremum taken over the scorings of .
The result shows that the width of the poset is a genuine barrier: whatever the algorithm, an adversary choosing scores after seeing how the algorithm spreads its selections can force a ratio arbitrarily close to . The paper's ProxyLabel algorithm has competitive ratio at most when the width is known (Corollary 5.1, p. 15). Together the two results show that the best achievable competitive ratio in the poset secretary problem is of order , which the paper calls order-optimal. The lower bound also covers the group-bias model of the paper: groups whose members are compared only within their group form exactly the instance used here.
On the formal side, the result is proved in the paper but has no machine-checked proof. The mission produces a formal model of score-independent randomized selection on a finite poset, a formal offline optimum with selections, and the width of a disjoint union of chains. These can be reused for other lower bounds in online selection.
The argument is short, and the work lies in getting the quantifiers and the encoding right. The printed statement places "there is an instance" before "for any algorithm". Read literally this is false for : on a fixed instance, the algorithm that always selects the highest-scoring elements achieves ratio . The proof establishes the other order: the poset is fixed, then the algorithm, then the scoring. A formalization must keep the scoring chosen after the algorithm while preventing the algorithm from depending on the scores.
The printed chain of inequalities also needs care. Its middle step drops the term , which the stated constraints on the perturbation do not make nonpositive. The bound therefore holds for perturbations chosen small enough, not for every perturbation satisfying the printed constraints. The existence of distinct, order-consistent scores meeting all the constraints at once has to be shown, and so does the identification of the optimum with the heavy chain.
Elements form a finite type with a partial order. A consistent scoring is a function to that is nonnegative, injective and strictly monotone (). These are the standing assumptions of the model (§3.1, p. 7), not additions. is a finite maximum over subsets of at most elements. Width is the published definition AppliedComb.Posets.width, the size of a largest antichain, not a minimum number of chains, so the width milestone is a real claim. Algorithms are represented by selection rules: nonnegative weights on subsets summing to and vanishing on subsets of more than elements. This class contains the selected-set law of every online algorithm, so a lower bound for it is a lower bound for online algorithms. Expectations and probabilities are finite sums. Competitiveness is stated as together with , with no division by an expectation that may vanish. The hypotheses and are standing: with the poset is empty, and with every ratio is . The instance is the sigma type with Mathlib's disjoint order.
Trivializing formalizations are ruled out explicitly. A selection rule must have total mass , so the zero rule does not make the expected score vanish. It must respect the capacity, so the rule selecting everything is excluded. The scoring is quantified after the selection rule, never before it and never as an input to it. is part of the conclusion.
The development needs finite sums over subsets, the order on sigma types, and antichains. Contributions are welcome on any milestone. The width of a disjoint union of chains and the pigeonhole bound on selection probabilities are reusable beyond this mission.
Many outpatient clinics offer two ways in: an appointment booked online, and walk-in hours on the day. Some patients have no choice (acute cases arrive as walk-ins), but many can pick either channel, and they pick the one that costs them less: a long appointment delay pushes them into the walk-in room, a crowded walk-in room pushes them to book or to give up. A clinic deciding how to split its daily capacity between the two channels therefore faces a game, not a forecasting problem.
Liu, van Jaarsveld, Wang and Xiao (SSRN 3558209; Management Science 2023, doi:10.1287/mnsc.2023.4676) model this game and compare three operational levers: the capacity split, how much delay information the booking system reveals, and triage, that is, reserving walk-in hours for acute patients only (as some practices do, e.g. Centre Pediatrics 2021). This mission formalizes the triage comparison, Proposition 6 of the paper: closing walk-in hours to patients who could book pays off exactly when lost demand is cheap relative to overtime.
Patients. Exogenous walk-ins arrive at rate and are always served on the day, possibly in overtime. Strategic patients arrive as a Poisson process of rate . A served patient gains .
Capacity. The clinic has total capacity per day, split into appointment hours and walk-in hours , with .
The appointment queue. Appointments form a single-server queue with deterministic service time . In the observable setting a patient sees the queue: with patients waiting, the delay is , uniform on . A patient schedules when this delay is at most a threshold , and scheduling at delay is worth . The fraction of strategic patients who do not schedule is the blocking probability of this M/D/1/K−1+p queue, where and . With it has the closed form , where is built from the Poisson weights by the Brun–Garcia recursion (Online Appendix C, (26)–(27), Corollary C.1). With no appointment hours, .
Walking in and balking. A patient who does not schedule walks in with probability proportional to or balks with probability proportional to . Walking in is worth , with convex, strictly increasing and ; balking is worth . An observable equilibrium is a solution of conditions (6)–(10): the threshold makes scheduling at least as good as the walk-in/balk mixture up to and worse beyond it, , and patients walk in (balk) only if walking in is worth at least (at most) zero.
Costs. The provider pays per balking patient and for overtime, with convex and strictly increasing. In the strategic model patients choose freely, and the cost at allocation and equilibrium is
In the triage model strategic patients may only schedule or balk, so they behave with threshold and
Let solve (15): below these walk-in hours the exogenous walk-ins alone make walking in worthless.
Suppose and set
Then
where the infima are over allocations and, on the strategic side, over the equilibria at each allocation. The Lean statement says this without infima: every strategic configuration is matched by a triage allocation that costs no more, and every triage allocation is matched by a strategic allocation at which an equilibrium exists and every equilibrium costs no more.
Proposition 6 turns a qualitative trade-off into two explicit thresholds on the ratio of the lost-demand cost to the overtime cost. Free choice reduces balking but lets strategic patients crowd the walk-in hours; triage removes that crowding at the price of more balking. The thresholds and depend only on the overtime function, the capacity and the blocking probability, so a clinic can evaluate them from its own data. The paper also shows (Remark 4, Appendix D.8) that the same insight holds in the unobservable setting, with capacity playing an additional role; that variant is not part of this mission.
The result is proved in the paper (Online Appendix E.3, pp. 35–37) and has no machine-checked proof. The formalization adds three things. It fixes the equilibrium concept precisely, including the mixture weights and the endpoint conventions. It states the comparison of optimal costs without presupposing that the optima are attained; the paper's proof begins "denote the optimal capacity allocations" without proving existence. And it ties the blocking probability to the paper's closed form, so the monotonicity in that the proof invokes becomes a statement about an explicit function rather than about a queue described in words.
The comparison itself is a chain of convexity inequalities at a single allocation. The hard part is the blocking probability. The paper proves that decreases in by a sample-path argument on the queue, but a formal development has only the closed form, in which jumps at every where is an integer, jumps from to there, and moves continuously. Monotonicity and continuity must be shown across these seams, through alternating sums whose terms cancel heavily. The obvious route, differentiating the closed form for fixed , does not give the sign without a further structural argument on the coefficients .
Existence of an equilibrium (milestone 2) is an intermediate-value argument in , which in turn needs continuity of in and positivity of .
Everything lives in the namespace OutpatientWalkIn.Triage. The definition Queue contains the closed-form blocking probability blockProb lam δ μS; the definition Setting contains the model, the standing assumptions, the utilities, the equilibrium IsObsEq, the costs obsCost and triageCost, and the thresholds alphaLow, alphaHigh.
Conventions:
A formalization that compares the two models at one fixed allocation only, that lets the prover choose a cheap equilibrium when several might exist, or that replaces by an arbitrary decreasing function, is not the paper's theorem; the statements here rule these out.
Contributions welcome: properties of the closed-form (positivity, , monotonicity and continuity in both arguments), the existence of equilibria, and the convexity estimates of the final comparison. The queue file is reusable for any M/D/1/K model with partial joining.
A generative model lets a planner request independent next-state samples for any state-action pair. This is a useful idealization for studying how many simulator calls are needed before a policy computed from an estimated model performs well in the true environment. Li, Wei, Chi, and Chen show that a small independent perturbation of the rewards lets a model-based planner meet a sample-size bound with cubic dependence on the effective horizon , while providing guarantees for both values and action values (Li et al., 2024). This mission isolates their perturbed-planning result and the source lemmas that support it.
A finite discounted Markov decision process consists of a state set , an action set , a transition probability , an immediate reward , and a discount factor . A deterministic policy chooses an action at each state. Its value is the expected sum of rewards, discounted by , from state . Its action value takes action first and follows thereafter. The optimal values and are those of an optimal deterministic policy; equivalently, .
For each , draw independent next states from , independently across pairs. The empirical kernel is their frequency table. Independently draw one reward perturbation per pair and set . The planner returns an optimal deterministic policy for the empirical MDP . The performance claim evaluates this policy under the original and , so the perturbation changes policy selection but not the evaluation target.
Theorem 1 of Li et al. asserts that absolute constants can be chosen before , , , , , , and . For , , and , the sample-size condition is
With probability at least over both the samples and the perturbation, every optimal policy of the perturbed empirical MDP simultaneously satisfies
The milestone list follows the paper's numbered statements: fixed-policy and Bernstein-condition value bounds (Lemmas 1–2), calibrated state-action absorbing models and their finite reward grid (Lemma 3, (88), Lemma 4), planning under a separated optimum (Lemma 5), separation induced by random rewards (Lemma 6), and the reward-change bound before (49). The paper's additional claim about iteration counts for empirical QVI and PI is outside this target.
The theorem gives a policy guarantee from a finite number of calls to a generative model. It bounds the true value of the selected policy at every state and its true action value at every state-action pair, rather than only the empirical objective used to select the policy. Its is the number of samples per pair; the total number of transitions observed is . The statement is a theorem proved in the cited paper, not an open mathematical conjecture (Li et al., Theorem 1).
The formalization work is to turn the paper's probability experiment, policy choice, and linked inequalities into machine-checked statements and eventually machine-checked proofs. The published FoundationsML transition kernel and policy-value definitions provide reusable base objects. This mission adds a finite generative-sample law, the reward-perturbation law, and an absorbing-MDP interface. Those objects can support later formalizations of empirical planning and policy evaluation beyond this theorem. The goal and milestone proofs remain open in the present draft.
A fixed policy can be evaluated against an empirical transition kernel using concentration at that policy. The planner's policy depends on the same sampled kernel, so a fixed-policy bound cannot simply be applied to it. Small changes in transition frequencies may also switch the chosen optimal action when actions have nearly equal values. The paper's intermediate results specify the needed value-control and separation properties; a Lean proof must track their constants and their probability events without silently assuming that the data-dependent policy was fixed before sampling (Li et al., §§6.2–6.3).
The Lean state and action types are finite, and both are nonempty where cardinalities occur in denominators. A transition kernel is a probability vector at each state-action pair. Policies are deterministic functions , embedded as point-mass stochastic policies for the published value definitions. is the maximum over the finite set of deterministic policies; is . Function norms are supremum norms. The empirical kernel is the frequency table of a finite array of samples, with in the goal because its formula divides by . The independent perturbation is the uniform measure on the cube .
Probability claims bound the failure event. The data law is a finite product, and the auxiliary continuous draw is measured section by section. This formulation allows an outer measure for a section whose measurability is not already known; it does not let a nonmeasurable success event satisfy the result for free. The main theorem quantifies over every optimal policy of the empirical perturbed model, and its universal constants do not depend on the instance. These choices rule out treating the selected policy as arbitrary, fixing the perturbation in advance, or choosing constants after seeing the MDP.
The absorbing-MDP construction changes one transition row and one reward. The reward at that row may leave , so the underlying value function accepts arbitrary real rewards even though the main MDP has normalized rewards. Lemma 5 is stated with normalized rewards as printed. Reusable contributions include basic properties of the sampling law, optimal-policy existence, the absorbing construction, and quantitative value stability; the milestone statements themselves are the intended proof targets.
Many optimization problems in statistics and machine learning constrain the variable to a smooth manifold: orthonormal frames in sparse PCA and dictionary learning (the Stiefel manifold), unit vectors in phase retrieval (the sphere), fixed-rank matrices in matrix completion. Riemannian optimization handles these problems directly on the manifold. A step is taken in the tangent space and mapped back to the manifold by a retraction.
In several applications the objective can be evaluated but not differentiated: black-box adversarial attacks, simulation-based models, and hyperparameter or policy tuning. Zeroth-order (derivative-free) methods replace the gradient by an estimator built from function values. In Euclidean space the standard construction is Gaussian smoothing, analysed by Nesterov and Spokoiny (2017) and Ghadimi and Lan (2013). Li, Balasubramanian and Ma (arXiv:2003.11238; Mathematics of Operations Research, 2023) carry the construction over to embedded submanifolds. They sample a Gaussian vector, project it onto the tangent space, and use the retraction in place of the straight line . This mission formalizes their first optimization guarantee: the convergence rate of zeroth-order Riemannian gradient descent (ZO-RGD).
Let be a finite-dimensional real inner product space (the ambient ). Let be a embedded submanifold of dimension . At each the tangent space is a -dimensional linear subspace of ; let denote the orthogonal projection onto it. carries the metric induced by the inner product of .
A retraction is a map such that, for every , is smooth on , maps into , satisfies , and has the identity as its differential at . In this mission is defined on all of .
For a differentiable the Riemannian gradient is . Assumption 2.1 (retraction smoothness) asks for a constant such that
Given and a standard Gaussian vector of , set . The zeroth-order Riemannian gradient estimator is
ZO-RGD (Algorithm 1) starts at , draws independent Gaussian vectors , and sets , where uses . The step size is . Let be a minimizer of over .
For every ,
where and
These are the paper's own intermediate results (§2.2, p. 8):
Theorem 3.1 shows that ZO-RGD reaches an -stationary point in expectation using function evaluations, provided the smoothing parameter is of order . The dimension that enters is the intrinsic dimension of the manifold, not the ambient dimension . For the Stiefel manifold of orthonormal frames this is the difference between and , and for the sphere between and . More importantly, the estimator never explores normal directions. The three estimates of Proposition 2.1 are the toolkit that the paper reuses for its stochastic (ZO-RSGD), proximal (ZO-ManPG) and second-order variants.
The paper proves these results on paper; none of them has a machine-checked proof. The mission adds three things. It gives a precise model of a random iterate sequence on a submanifold, driven by the infinite product of Gaussian draws. It formalizes the projected-Gaussian identities, which are reusable for any method that samples in tangent spaces. And it pins down the constants. In checking the constants, the printed Proposition 2.1(b) turned out to be false for large (its proof yields , not ), and the middle term of the printed inherits that slip. The statements here carry the constants the proofs actually give.
In Euclidean space, is exactly the gradient of the Gaussian-smoothed function , and the analysis runs on . Once a retraction replaces , no smoothed function has as its gradient. The bias must be estimated directly from Assumption 2.1, which controls only along the tangent space. The moment bounds must then be taken for a Gaussian projected onto a subspace that changes with .
In the descent argument, the direction is sampled in , which depends on all earlier draws. The expectation of step is therefore conditional on the past. Summing the one-step inequality requires conditional expectations on the product space, together with measurability of the iterate map. Finiteness of is not given and must be handled as well.
stdGaussian E, so becomes integration against it.ProjLikeRetr.Retractor.IsSubmanifold 1 d M, which ties to . The tangent space is the published ProjLikeRetr.Retractor.tangentSpace M x, the span of Mathlib's tangent cone. Neither nor the tangent spaces are free parameters.Several trivializing formalizations are ruled out. A Bochner integral of a non-integrable function is , so every expectation in a conclusion is either a lower Lebesgue integral compared with a finite bound or paired with an integrability conjunct. The dimension comes from the manifold, not from a free natural number. The projection is onto 's own tangent space, never onto an arbitrary subspace field.
A complete development needs the following infrastructure:
The projected-Gaussian lemmas and the iterate model are reusable for the stochastic variant (ZO-RSGD) in the companion mission. Contributions of proofs for any milestone, and of general lemmas about Gaussian measures restricted to subspaces, are welcome.
The minimum bisection problem partitions an even-sized graph into two equally large groups while cutting as few edges as possible. In community detection, a graph may have been generated around an unknown, balanced pair of groups. The statistical question is whether an optimizer can identify that planted partition from the edges. Before studying random graph models or relaxations, it is useful to know which properties of a single observed graph suffice for recovery and whether those properties can be weakened.
Del Pia, Khajavirad and Kunisky express a deterministic sufficient condition through two vertex-degree parameters. Their Theorem 1 says that minimum bisection recovers the planted partition when the smallest within-community degree exceeds the largest cross-community degree by more than . Theorem 2 supplies graphs at or below that boundary where recovery fails. Thus the degree difference has a sharp worst-case boundary within the theorem's stated size and degree ranges. This mission formalizes that second, tightness result.
Let be a simple undirected graph with vertices. A bisection is a partition of with . Its cut cost is the number of edges with one endpoint in each side. The planted bisection is a designated partition regarded as the answer the optimizer should recover. Since exchanging and leaves the partition unchanged, uniqueness is always understood up to this exchange.
For each vertex , count its neighbors on its own side of the planted bisection and its neighbors on the opposite side. Write and for these counts. The two parameters of the planted graph are
Minimum bisection recovers the planted partition if every bisection with cost at most that of the planted one is the planted partition, up to swapping its sides. This formulation requires both optimality and uniqueness. If the planted bisection costs more than a competitor, recovery fails; it also fails when a distinct bisection ties it. These definitions follow §2 of the pinned preprint.
Lemma 1 supplies two finite-graph existence statements. For positive even , a simple -regular bipartite graph exists on vertices with vertices per side whenever . For the same , a simple -regular graph exists whenever . The bipartite part includes the edgeless graph at and the complete bipartite graph at . The second part includes the edgeless and complete graphs at its own endpoints.
The mission's goal is Theorem 2. For every positive multiple of eight and every pair of nonnegative integers satisfying
there exist a graph on vertices and a planted bisection with those exact parameters for which minimum bisection does not recover the planted partition. The inequalities delimit the claimed family; the goal does not assert failure for every graph with those degrees. The word “exact” matters because a construction with merely smaller within-side degrees or larger cross-side degrees would not establish tightness for the requested parameter pair.
Together with the paper's Theorem 1, the goal locates the worst-case threshold for recovery by minimum bisection: a strictly larger degree difference guarantees recovery, while every admissible parameter pair at or below the boundary occurs in a counterexample. This separates a guarantee about all graphs with given degree extrema from a claim about a particular graph. It also gives a deterministic baseline for comparing the behavior of the paper's linear programming relaxation and stochastic block model, whose recovery guarantees concern different optimization procedures and graph distributions.
The theorem is proved in the cited paper; the task here is to state its graph model, parameter extrema, and recovery conclusion in Lean with the same quantifiers and boundary cases, then obtain a machine-checked proof. The regular-graph existence lemma is independently reusable for other finite graph constructions. The definition layer can also support later exact-recovery statements for the same paper after the series' graph conventions are consolidated.
A strict threshold being sufficient does not itself show that it is necessary. At equality, an inequality used in a recovery guarantee no longer forces a unique optimum, but that leaves open whether a graph with the prescribed degree extrema actually has a competing bisection. Every requested pair must be realized by a genuine simple graph, including the degree endpoints, and the competing partition must be balanced and distinct even after sides are exchanged. The proof therefore needs graph existence and degree bookkeeping as well as a comparison of cut costs. The page states one numbered supporting lemma, Lemma 1; its two clauses are the mission's milestone.
Vertices are represented by Fin n, indexed from zero rather than the paper's . A side of a bisection is a Finset; its complement represents the other side. Graphs are Mathlib SimpleGraph values, and cut cost counts each undirected crossing edge once by ordering its endpoints. The within and across degrees are filtered neighbor counts. Their minimum and maximum range over all vertices, matching the paper. An empty vertex type receives a conventional zero degree extremum, while Theorem 2 requires .
The bounds involving and are compared in the reals, so natural-number subtraction cannot truncate a negative difference. The hypothesis makes an integer in the theorem's actual domain. Lemma 1 uses positive even , with Mathlib's regular-degree predicate and a bisection set witnessing equal bipartition sizes. Its bound is safe in natural numbers because .
The formal goal requires a witness graph whose minimum within-side degree equals the requested and whose maximum across-side degree equals the requested . It also requires an actual planted bisection and failure of uniqueness up to complement. Replacing either equality with a loose degree bound, or allowing a non-bisection witness, would make the claim easier and lose the paper's result. Contributions toward finite regular graph constructions, exact degree calculations, and cut-cost comparisons are within scope.
Value iteration (VI) is the standard method for computing the optimal value function of a discounted Markov decision process (MDP). It applies the Bellman operator repeatedly, and because that operator is a -contraction in the sup norm, the error after steps is at most times the initial error. When the discount factor is close to , as in long-horizon planning, this rate is slow.
Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) read value iteration as a gradient-type method and transfer momentum schemes from convex optimization (Nesterov acceleration, heavy-ball momentum) to the Bellman operator. On reversible policy chains these accelerated schemes provably converge faster than VI. On general MDPs, however, the accelerated iterates need not converge at all: the paper exhibits instances on which Accelerated Value Iteration (A-VI) oscillates or diverges. Section 7 of the paper resolves this tension with Safe Accelerated Value Iteration (S-AVI, Algorithm 1), which tries an accelerated step at every period and keeps it only when it makes enough progress on the Bellman equation . This mission formalizes the convergence guarantee of S-AVI, Theorem 7.1.
Let be a finite set of states and a nonempty finite set of actions. A discounted MDP is given by a transition kernel , with the probability of moving from state to state under action and ; a reward for each state-action pair; and a discount factor . The Bellman operator is
The sup norm is . The optimal value function is the unique fixed point of . For a vector , the quantity is its Bellman residual.
S-AVI (Algorithm 1) takes a scalar , step sizes and any starting vector . It sets , and at each period forms
If , the accelerated candidate is accepted, ; otherwise the algorithm takes a value-iteration step, . In the Lean development the MDP is AccelVI.SafeAVI.MDP with validity predicate MDP.Valid, the operator is bellman M, and the iterates are savi M lam' α γ v0 : ℕ → (S → ℝ).
For a valid MDP, any , any and any , the S-AVI iterates converge to , and
that is, there is a constant with for every . The constant is left unspecified, as in the paper.
The result. Theorem 7.1 says that the safeguard costs nothing in the worst case: S-AVI converges on every MDP at rate , and with it matches the rate of value iteration, which Theorem 6.3 of the same paper shows cannot be beaten by any first-order method uniformly over MDPs. At the same time it accepts accelerated steps whenever they reduce the residual fast enough, so it keeps the empirical speed-ups of A-VI. Remark 7.2 of the paper describes the role of : values closer to admit more accelerated steps. The guarantee also gives a computable stopping rule, since the residual bounds the distance to .
Formalizing it. The result is proved in the paper; to our knowledge it has not been machine-checked. This mission produces a Lean statement of the finite discounted MDP layer, the Bellman operator and Algorithm 1 itself (including its two-step recursion and its data-dependent branch), and a formal proof that the safeguarded iteration converges. The contraction property of and the residual-to-error bound are reusable for any later value-iteration development on the platform. Three sibling missions of this series pose the paper's other main results: the rate of Accelerated Value Computation on reversible chains (Theorem 5.1), the rate of Momentum Value Computation (Theorem 5.5), and the first-order lower bound (Theorem 6.3).
The accelerated candidate is built from two past iterates through a momentum step, and on a general MDP nothing controls it: A-VI is not a descent method, and its iterates may diverge. The natural first attempt, proving that A-VI steps contract the error, therefore fails. The difficulty in the formal setting lies elsewhere: the iterates are defined by a two-step recursion with a branch on a real inequality, so any argument must handle both branches at every period and keep the paper's indexing straight (the threshold at period is and it compares with the residual of , not of ). Existence and uniqueness of and the contraction property of a max of affine maps also need to be established for the specific operator, from the stochasticity of .
States and actions are finite types, [Fintype S], [Fintype A], and [Nonempty A] so that the maximum in exists. Vectors are functions S → ℝ with Mathlib's sup norm, which is . Rewards are arbitrary reals. The discount factor is M.lam with inside MDP.Valid; the initial distribution of the paper's tuple is omitted because no statement uses it. The optimal value function enters each statement as a vector vstar with bellman M vstar = vstar; this is not vacuous, since a valid MDP has exactly one such vector. The scalar ranges over the closed interval , and as in Algorithm 1, although the convergence argument does not need the step sizes to be positive. The sequence savi is indexed as the paper's : its recursive case s + 2 is the paper's period , with threshold lam' ^ (s + 2). " for all " is encoded as a single constant valid for every , which is stronger than an eventual big-O.
A formalization that replaced the test by the per-step condition (7.2) of Remark 7.3, used the residual of instead of , fell back to , or allowed would be a different theorem; none of these is posed. Remark 7.4's extension to arbitrary contractions is not posed either.
The development needs the contraction property of , the Banach fixed-point bound relating error and residual, and an induction over the iterates. Proofs of the milestones as separate lemmas are welcome, as are general statements about safeguarded fixed-point iterations for -contractions that specialize to this one.
When a contract breach propagates along a supply chain, one failure triggers the next: a supplier delivers late, the manufacturer misses its own delivery, the distributor misses its, and so on. Each link suffers a loss caused by its predecessor, and the question is who should be liable for what. Gudmundsson, Hougaard and Ko (Management Science 70(3), 2024) study this as an axiomatic cost-sharing problem, with the aim of rules simple enough to be executed automatically by a smart contract.
Their first main result characterizes a one-parameter family, the fixed-fraction rules , , by four axioms. The axioms do not single out a member of the family. Section 4 of the paper gives two normative arguments for the midpoint . This mission formalizes the first of them, Theorem 2: for loss chains with equal losses, is the allocation at equal Euclidean distance from every agent's "ideal" allocation. The construction follows the tradition of ideal points in bankruptcy, taxation and bargaining (Yu 1973; Chun 1988), with one ideal allocation per agent instead of a single ideal point.
There are agents in a chain. Agent causes a loss to agent ; a loss problem is , with total loss .
An allocation of is a vector of liabilities with , with for (no initial segment of the chain pays less than the losses it caused), and with . The set of allocations is , and the ordered allocations are .
The fixed-fraction rule with parameter (Definition 1) is
Each agent pays the fraction of the loss it caused directly, and the initiator also pays the residual .
For the ideal allocation charges the first agents equally and the rest nothing:
When , is the allocation agent 2 would prefer among the ordered allocations, is the one agent would prefer, and is agent 1's. Distances are Euclidean: .
For every and with ,
Theorem 2 is one of the two arguments the paper gives for recommending among the fixed-fraction rules; the other is that is the Shapley value and the nucleolus of the associated liability game (Theorem 3, a separate mission of this series). The uniqueness companion turns the theorem into a selection principle: equalizing distances to ideal allocations determines the allocation completely. The paper also remarks that the same principle, applied to the elementary problems with unit-vector ideal allocations, selects the serial rule, which shows that the choice of ideal allocations drives the result.
The result is proved in the paper; to the best of our knowledge it has no machine-checked proof. The mission produces a formal model of loss chains, allocations and fixed-fraction rules on which the other missions of the series also build, and a checked version of the paper's computation, including the boundary cases (, ) that the printed proof passes over.
The theorem is a computation, and the obstacles are the ones a careful formalization has to face rather than conceptual ones. The squared distance to splits into a part common to all and a part linear in the prefix sum , and the printed argument passes between the two forms by dividing by , which is not allowed for the zero problem. The uniqueness statement must also hold at , where every ideal allocation is the zero vector and the prefix characterization breaks down. Prefix sums over must be matched exactly with the nonzero coordinates of ; an off-by-one in either produces a different family of points. Finally, the equal-loss hypothesis cannot be dropped: for , , at distance from and from .
Agents are indexed in Lean (the paper's agent is index ), vectors are functions Fin n → ℝ, and nonnegativity of a loss vector is the predicate IsLoss. The fixed-fraction rule is a function of , and ; is named lam. The ideal allocation ideal ℓ k is defined for every natural but is used only for ; every statement quantifies over exactly that range, because ideal ℓ 0 is the zero vector in Lean and is not one of the paper's points. Distances are Mathlib's distance on EuclideanSpace ℝ (Fin n); the sup distance on Fin n → ℝ is not used, and would not even be detected by the Figure 1 example, where the sup distances to are also all equal.
Disclosed additions and corrections:
A formalization that states the conclusion with the sup metric, that ranges over or , or that drops the equal-loss hypothesis does not formalize Theorem 2. Contributions of proofs of any item are welcome; milestone 1 is a finite-sum computation reusable for any distance-to-ideal-point argument in this setting.
Value iteration (VI) is the basic algorithm for computing the optimal value function of a discounted Markov decision process (MDP). Its error contracts by the discount factor per step, so it needs on the order of iterations, which is slow when is close to , the regime of interest in long-horizon planning and reinforcement learning. Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) read VI as gradient descent on the residual map and import Nesterov's acceleration and heavy-ball momentum from convex optimization. In convex optimization the corresponding lower bounds of Nesterov (2004/2013) show that acceleration is optimal among first-order methods. The question this mission formalizes is the MDP counterpart: can any method that only combines past iterates and their Bellman images beat the rate of plain VI on every MDP? Theorem 6.3 of the paper answers no.
A finite MDP consists of a state set with , a finite nonempty action set , transition probabilities with , rewards , and a discount factor . Its Bellman operator is
a -contraction for the sup norm . Its unique fixed point is the optimal value function.
A sequence in is a first-order sequence for if
VI from () and relaxed VI () from produce such sequences.
The chain MDP of Figure 1 has states and a single action. State is absorbing with reward ; every state moves deterministically to and earns nothing. In Lean (namespace AccelVI.LowerBound) the MDP is MDP, validity is MDP.Valid, is bellman, the chain is chainMDP n lam, and the first-order condition is IsFirstOrder T v.
For every , every , the fixed point of the Bellman operator of the -state chain, every first-order sequence for , and every ,
The result. Theorem 6.3 shows that, measured by the number of Bellman evaluations, no first-order method improves on the worst-case rate of value iteration uniformly over MDPs, as long as the number of steps is below the number of states. In convex optimization the analogous class admits acceleration from to ; with , , the analogue for MDPs would be a rate of about , and this theorem rules it out. It is the reason the paper's accelerated schemes are analysed under extra structure, such as reversible policy-evaluation chains, or are safeguarded.
Formalizing it. The result is proved in the paper; no machine-checked version exists. The mission produces a checked lower bound for fixed-point iterations of Bellman operators, the contraction inequalities (3.5)–(3.6) for a general finite MDP, and an explicit value function for a hard instance. The paper's other main results, Theorems 5.1, 5.5 and 7.1, are posed as the sibling missions 1, 2 and 4.
The obvious argument that the error is at least the contribution of states never reached fails without control of the span: the first-order class allows arbitrary real coefficients, including ones that change with and depend on all past iterates, so one has to show that no such combination puts mass on states beyond index . The support claim has to be carried through the nonlinear max in , which is benign here only because the chain has a single action. The second ingredient converts a bound on a few coordinates of into a bound in sup norm with the exact constant , which requires the two-sided inequalities (3.5)–(3.6) for and the explicit value .
Fin n and are 0-based: the paper's state is index , so is lam ^ k / (1 - lam) at index and "" is . The action set of the chain is Unit.Fin n → ℝ. "span" is the real linear span Submodule.span ℝ, with both lists running to index inclusive.FoundationsML_ReinforcementLearning_BellmanOperator and FoundationsML_ReinforcementLearning_IsTransitionKernel.Contributions welcome: proofs of the contraction inequalities for general finite MDPs (reusable by every Bellman-operator mission), of the support recursion, and of the final chain of inequalities.
The Quantum Approximate Optimization Algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028) is a family of shallow quantum circuits for combinatorial optimization. At its lowest level, , the circuit has two real parameters, and its output is a random bit string. The question is how many constraints that string satisfies, compared with the best classical algorithms.
Max E3LIN2 is a natural test problem. Each constraint is a linear equation modulo on exactly three bits, and the task is to satisfy as many of the equations as possible. A uniformly random string satisfies in expectation, and for general instances no efficient algorithm does better than unless P = NP (Håstad 2001). The interesting regime is bounded occurrence: every bit lies in at most equations.
Timeline, as recorded on p. 3 of the paper:
An instance on bits consists of equations. Equation is
on a triple of distinct bits , with right-hand side , and no triple carries two equations. The instance has occurrence bound if every bit appears in at most equations.
Let be the number of equations satisfied by the string , viewed as a diagonal operator on the -dimensional space spanned by the basis states . Let be the sum of the Pauli operators, and the uniform superposition of all basis states. For real angles the level-one QAOA state is
Measuring it in the computational basis returns with probability . The expected satisfied count is
The paper writes the objective as , with for the equation on . The analysis is phrased through the shifted quantity .
The angles used are and, for an odd integer ,
There is a threshold such that for every there is an odd with , such that on every instance with occurrence bound some grid angle satisfies
and depend on only, never on the instance. Equivalently, in the paper's form (44), .
The milestones are the displayed claims of Section II, in the order the argument uses them:
The theorem shows that a single layer of the QAOA, with fixed and predetermined angles, beats random guessing by on every bounded-occurrence instance. Up to the factor this matches the threshold that Trevisan's hardness result places on efficient algorithms.
Two ingredients are reusable well beyond this paper. The hypercontractive inequality (29) bounds all moments of a degree-2 polynomial in uniform variables, at every exponent . The Chebyshev-node inequality (39) bounds from below the maximum of a polynomial with unit linear coefficient over the points . Neither is in Mathlib or on the platform in this generality.
The result is proved on paper, with explicit constants, but none of it has been machine-checked. A complete formalization would also pin down two places where the printed argument is loose (see Formalization scope).
The obvious approach is to expand the expected count as a power series in and keep the linear term . That fails because the higher-order terms are not small: each clause interacts with up to others, so the coefficient of can grow like , and their signs are uncontrolled. Uniform small-angle estimates therefore lose the linear gain unless . Even there, the polynomial part of degree up to can cancel the linear term at any single angle. The step that needs a genuinely new input is showing that some angle of a short fixed grid avoids this cancellation for every instance at once. The remaining difficulty is bookkeeping: the threshold where the explicit constants start to work is enormous ( of order several hundred), so it has to be existential.
Qubits n = Fin n → Bool, with true the bit . An instance is tri : Fin m → Fin n × Fin n × Fin n (strictly increasing coordinates, injective) and rhs : Fin m → Bool. Bounded occurrence counts, for each bit, the equations whose triple contains it.QAlgorithms definitions supply act, prob, uniformState, problemHamiltonian, qaoaMixer and qaoaUnitary.In many auctions a bidder's value for what is sold depends on information held by other bidders: the value of an oil-drilling lease depends on every bidder's geological survey, the value of a piece of art on what other experts know about its provenance. This is the interdependent values model of Milgrom and Weber (1982). With interdependent values the standard private-value tools fail: the Vickrey–Clarke–Groves (VCG) mechanism is no longer incentive compatible, exact efficiency in ex-post equilibrium requires a single-crossing condition, and with multidimensional signals maximizing welfare is generically impossible even in Bayes–Nash equilibrium (Jehiel and Moldovanu 2001). Without some structural condition on how values respond to others' information, even a single-item auction can force every truthful randomized mechanism to lose a factor of order (Example 1.3, after Eden et al. 2018), when values treat the signals as complements.
Eden, Feldman, Fiat, Goldner and Karlin (arXiv:1903.08384, Mathematics of Operations Research 2024) identify such a condition, submodularity over signals (SOS), and show that under SOS simple randomized mechanisms recover a constant fraction of the optimal welfare in rich settings. This mission formalizes their result for combinatorial auctions with multidimensional signals and separable SOS valuations, where the mechanism is a random-sampling variant of VCG with explicit payments.
Timeline of the line of work:
There are agents and items; a bundle is a set . Each agent privately holds a signal for every bundle , and collects all agents' signals for . Agent 's value for bundle is , a known function of , weakly increasing in every signal and strictly increasing in ; the empty bundle is worth .
A function of the signal vector is SOS when raising a single coordinate helps at least as much at a coordinatewise lower profile of the other coordinates: for every coordinate , and profiles off ,
The valuations are separable SOS when
with (depending only on the other agents' signals for ) and weakly increasing and SOS.
An allocation gives agent the bundle , with the bundles pairwise disjoint. A deterministic mechanism maps reported signals to an allocation and payments. It is ex-post incentive compatible (IC) if, whatever the true signals, no agent gains by misreporting when the others report truthfully, where the agent's utility is her value at the true signals for the bundle she receives minus her payment; it is ex-post individually rational (IR) if the truthful utility is nonnegative. A randomized mechanism is universally ex-post IC-IR when every deterministic mechanism in its support is.
Random-Sampling VCG (RS-VCG) partitions the agents uniformly at random into and . For it sets the proxy weight
the value with the bundle- signals of the other members of replaced by . It allocates to a feasible allocation maximising , and a winner pays
where is the maximum proxy welfare of an allocation to .
For separable SOS valuations, RS-VCG is ex-post IC and IR for every partition, and for every true profile and every feasible allocation ,
The theorem shows that VCG-style reasoning survives interdependence when the dependence on other agents' information enters additively and submodularly: separability makes the payment absorb the effect of the others' signals, so that each agent of faces the proxy welfare as its objective. It gives a constant-factor welfare guarantee in ex-post equilibrium for combinatorial auctions with multidimensional interdependent signals, a setting in which exact efficiency is generically out of reach. The construction is the template for the paper's single-dimensional results in §6.
The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it produces a reusable Lean model of interdependent-value combinatorial auctions (multidimensional signals, ex-post IC/IR, universal truthfulness of random mixtures) and of the SOS condition, and a checked account of the VCG accounting identity in this setting.
The approximation part rests on the Key Lemma 3.1: a uniformly random half of the other agents' signals set to zero keeps, in expectation, half of an SOS value. The obvious argument — monotonicity alone — gives no constant: with values depending on many signals, zeroing half of them can destroy almost all of the value, and the SOS condition is exactly what rules this out. The incentive part is where the obvious transfer of VCG fails: the proxy weight of agent is not its value, and the true value depends on signals that the proxy zeroes. Without separability, the payment of a VCG-style rule would itself depend on the agent's report (the paper's remark at the start of §5), and alignment of the agent's utility with the proxy objective breaks. Ties in the argmax and agents receiving the empty bundle must be handled for every tie-breaking rule.
Agents are Fin n and items Fin m, with arbitrary; bundles are Finset (Fin m). Signals are NNReal, one per (agent, bundle), and is a function of the bundle- signal vector. The empty bundle is worth ; monotonicity, strict own-signal monotonicity and the separable decomposition are assumed for nonempty bundles. The function is written on the whole vector with the hypothesis that it ignores coordinate . The decomposition is data of the mechanism, since the payments use .
The allocation is produced by an arbitrary selector returning a feasible maximiser of the proxy welfare for every partition and report; all statements hold for every such selector. is a maximum over the finite set of feasible allocations to . Agents of , and agents of that receive the empty bundle, pay (the paper defines payments for winners only). The expectation over the partition is the uniform average , never an existential or universal over ; the approximation is stated for every feasible comparator allocation, with welfare at true values under truthful reports, never for proxy welfare or through a supremum. IC and IR are stated for each partition with the paper's explicit payments, not with existentially chosen payments.
A complete development needs finite averages over subsets, the Key Lemma 3.1 for SOS functions (posed in the companion mission on RS-V and not restated here), and finite argmax reasoning; the SOS layer and the combinatorial mechanism model are reusable for the other missions of this series. Proofs of the milestones, and of the d-SOS variant mentioned after the proof (a -approximation, not posed here), are welcome.
The source is the arXiv preprint arXiv:1903.08384v2 (2 June 2019); all page and display numbers refer to it, not to the journal version in Mathematics of Operations Research (2024).
Bitcoin and other proof-of-work cryptocurrencies rely on miners, who spend computing power ("hash rate") to win the right to append a block and collect a reward. The security argument for such systems assumes that no single miner, or small coalition, controls a large share of the total hash rate. Whether the economics of mining push the system towards or away from that decentralized state is therefore a basic question for anyone designing or regulating these protocols.
A. Capponi, S. Ólafsson and H. Alsabah, in Proof-of-Work Cryptocurrencies: Does Mining Technology Undermine Decentralization? (arXiv:2106.09783v1, 2021), model mining as a contest in which miners differ in their cost per hash and face a common capacity constraint. Their §4.3 asks how equilibrium hash rates respond to the model's parameters. This mission formalizes the answer for two of them: the capacity parameter , which measures how quickly a miner's operating cost grows with its scale, and the mining reward . The finding is that increasing either parameter shifts hash rate share from large miners to small ones. This is the third mission of a four-part series on the paper; the first poses the existence and structure of the mining equilibrium, the second its sensitivity to mining costs.
There are active miners, indexed , with costs per hash (sorted, without loss of generality), a reward and a capacity parameter . Miner choosing hash rate earns , where is the aggregate hash rate (the paper's (3.4)). The cumulative cost is .
In the paper's Proposition 4.1, the equilibrium aggregate hash rate is the positive root of , and the equilibrium hash rates are given in closed form. The paper's appendix (B.3) writes them as functions of the active miners' data:
with and . Miner is active exactly when . The hash rate share of miner is .
The paper's sensitivities are derivatives of these maps at a state where small parameter changes leave the set of active miners unchanged (pp. 15–16). For , (B.4) splits the derivative of into a direct part, with held fixed, and an indirect part through the aggregate, .
For every active miner ,
and the derivatives of with respect to and to are increasing in , for .
The result. Proposition 4.8 says that a tighter capacity constraint and a larger reward both favour small miners. The direct effect of a larger lowers every miner's hash rate. The indirect effect raises the hash rate of every miner with less than half of the total, because the aggregate falls and the marginal gain of hashing rises. For the reward, every miner's hash rate rises, but the share derivatives are increasing in the miner's index, i.e. in its cost: costlier, smaller miners gain share. Table 1 of the paper (p. 16) lists the signs; this proposition supplies the and columns. The paper uses it to argue that rising block rewards or tighter hardware constraints work against concentration (§4.3.3), in contrast to cost reductions from new hardware (§5).
Formalizing it. The result is proved in the paper by explicit differentiation (Appendix B). No machine-checked version exists. The mission produces checked closed forms of every derivative in (B.2), (B.4) and (B.6) for the and directions, the sign analysis, and the monotonicity in . The proof text on p. 43 says "decreasing in " where the proposition says "increasing"; a formal proof settles which is right (the displayed expressions give increasing, which is what is posed).
Each derivative is an exercise; the difficulty lies in keeping the algebra correct over several layers. The aggregate is the root of a quadratic, so its derivatives involve the square root, and every simplification of (B.4) and (B.6) uses the root identity , i.e. , and the first-order identity . The sign of the indirect parts is not visible from the raw derivative: it requires rewriting so that the threshold appears. The positivity of needs a separate bound, since its indirect part can be negative. The monotonicity in is the most delicate part: it is not true term by term in (B.6) as first displayed, and only becomes visible after the p. 43 rewrite, which separates the dependence on (decreasing in ) from that on (increasing in ), with coefficients whose signs again come from the root identity. Without the sorting of the costs, the monotonicity claim is false.
Everything lives in the namespace PoWMining.CapacityStatics. Miners are Fin n, 0-based: Lean miner i is the paper's miner , so "increasing in " is Monotone on Fin n, and "increasing" is weak, as in the paper's footnote 12. The definition ClosedForms provides cumCost (), gH ((4.1)/(B.3), with both branches of (4.1)), fH ( with the aggregate as a free argument), hstar, share, and the standing assumptions Standing: , , , , costs sorted, and for every (all miners active). The condition is the paper's: (B.3) defines only for . The definition Sensitivities defines the four 's as derivatives (Lean deriv) of the (B.3) maps, never by their closed forms; derivative claims in theorems are stated with HasDerivAt, so a junk value of deriv at a non-differentiable point cannot make a statement true.
The mission takes the active miners' costs as its data, which is the paper's own meaning of a sensitivity at a fixed active set. That and are the equilibrium of the mining game is Proposition 4.1, posed in mission 1 of this series; the cost derivatives, (B.5) and are posed in mission 2. This mission uses those identities but does not pose them.
Trivializing formalizations are ruled out: the 's are derivatives, not formulas whose signs can be read off; the standing assumptions are satisfiable (two miners with , , give , ); and the monotonicity is stated for derivatives asserted to exist.
Needed infrastructure: one-variable calculus in Mathlib (HasDerivAt for square roots, quotients and compositions) and finite sums. A reusable lemma library for (the root identity, positivity, ) serves all three of missions 1–3 and is welcome, as are proofs of the milestones in any order.
Many allocation problems divide work, not goods: shifts among employees, teaching loads among faculty, cleaning duties among housemates, maintenance tasks among the owners of a shared resource. For divisible goods the standard fair and efficient solution is the competitive rule (competitive equilibrium from budgets): give every agent a budget, find prices at which every agent demands what she receives, and the outcome is Pareto optimal and envy-free (weighted by budgets). For goods with additive utilities this rule is single-valued and is the solution of the Eisenberg–Gale convex program, which yields polynomial-time algorithms.
For chores (bads) the competitive rule keeps its fairness and efficiency guarantees but loses the convex structure: Bogomolnaia, Moulin, Sandomirskiy and Yanovskaya (BMSY17) showed it is generally multi-valued, with competitive allocations corresponding to critical points, not maximizers, of the Nash social welfare on the Pareto frontier. Brânzei and Sandomirskiy (arXiv:1907.01766v2, Mathematics of Operations Research, 2024) enumerate all competitive utility profiles in strongly polynomial time when the number of agents or the number of chores is fixed. Their counting result is the target of this mission.
There are agents and divisible chores, one unit of each. Agent 's value for one unit of chore is , and her budget is . A feasible allocation is with for every chore ; agent 's utility is , the utility profile is , and is the set of utility profiles of feasible allocations.
A feasible allocation is competitive for budgets if there are prices such that for every agent the bundle costs and maximizes among all bundles with . A competitive utility profile is for a competitive .
is Pareto optimal if no feasible allocation makes every agent weakly better off and some agent strictly better off; the Pareto frontier consists of their utility profiles. For weights the face of the Pareto frontier is the set of maximizers of over .
The proof runs through graphs. The consumption graph links agent and chore when . The maximal weighted welfare (MWW) graph links and when for every agent . A family of graphs is rich if every Pareto optimal profile in is for a feasible whose consumption graph is in the family. Along a path the product of disutilities is .
For , and ,
The result. Corollary 25 says that the competitive rule for chores, although multi-valued and non-convex, has at most polynomially many outcomes when or is fixed, and that the Pareto frontier has polynomially many faces meeting the negative orthant. It is the exact mathematical content of the paper's algorithmic Theorem 17: an enumeration that tries every graph of a rich family and recovers at most one candidate profile from each cannot miss a competitive profile and cannot produce more than of them. For the bound is attained in Example 1 of the paper by the face count.
Formalizing it. The result is proved in the paper; nothing is known to be machine-checked. The mission builds a reusable layer for linear Fisher-type economies with bads: the competitive rule with negative prices and budgets, welfare theorems, the trading-cycle and weighted-welfare criteria of Pareto optimality, and the graph-theoretic description of the faces of a polytope of feasible utilities. Lemma 14 and Lemma 18 are of independent use for any linear allocation model.
The obvious argument for goods, uniqueness of the equilibrium utility profile via a strictly concave program, fails: for chores there may be several competitive profiles, even on a single closed face (in Example 1 of the paper, both competitive profiles lie on one edge of the frontier). The count must therefore pass through combinatorics. Two steps carry the weight. First, the faces of the Pareto frontier, a continuous object, must be put in bijection with a finite set of graphs, and the graphs must be chosen so that each competitive profile is realized by an allocation whose consumption graph is exactly an MWW graph, not merely contained in one. Second, the size bound cannot come from counting bipartite graphs, which gives only ; it has to exploit the structure of MWW graphs, and its second term, polynomial in for fixed , requires the agent–chore symmetry of Lemma 22, whose natural route goes through the second welfare theorem.
Agents are Fin n, chores Fin m (0-based); values, budgets and prices are real functions; graphs are Finset (Fin n × Fin m) of edges; a path is a record of its length , agents and chores. Faces are the sets of maximizers of over for , the dual representation of p. 16. Counts are Set.encard in and the bound is computed in . Added relative to the paper: and (the paper's sets of agents and chores are non-empty) where a statement needs them. Not formalized: the running-time claims (Theorem 17, the second bullet of Lemma 23), item 4 of Lemma 38 (critical points of the Nash social welfare), and the sentence on p. 27 that each face carries at most one competitive profile, which is false for closed faces.
The following formalizations would trivialize the goal and are ruled out: a competitive allocation without the budget constraint ; non-negative values, budgets or prices; faces exposed by or by of arbitrary sign; counts over sets assumed finite; Pareto optimality restricted to a subclass of allocations.
All definitions live in CompetitiveChores.RichFamily; Mathlib supplies only finite sums and products, Finset, and Set.encard. Contributions welcome: proofs of the appendix lemmas (pure linear algebra on finite sums), of Lemma 14 (the cycle-cancelling argument of Appendix B), and of the two-agent splits-and-cuts count inside Lemma 23.
Classical mechanism design assumes that agents optimize exactly: a buyer facing a menu of lotteries picks the one that maximizes expected utility, and an incentive compatible (IC) mechanism makes truth-telling optimal. Buyers that are only approximately rational, or that face small costs of computing or reporting, need only be made to prefer the truth up to a slack . Approximate incentive compatibility (-IC) is the corresponding relaxation of the IC constraints. It is also used in computer science as a robustness notion and in learning settings where a mechanism is only approximately optimal for the buyer.
Balseiro, Besbes and Castro (arXiv:2103.03403) ask how much revenue a seller of one item can gain from such a relaxation. For a single buyer, Myerson's theory gives the IC optimum as a posted price. With -IC the feasible set grows, and the paper determines the order of the additional revenue as .
Timeline. The rounding argument attributed to Noam Nisan, first used by Balcan, Blum, Hartline and Mansour (FOCS 2005), turns an -IC mechanism into an IC one with a small revenue loss; for a single buyer it bounds the gain by for every distribution (Proposition 1 of the paper). Balseiro, Besbes and Castro (2021; v2 2022; Operations Research 2024) prove an upper bound (Theorem 1) under a curvature condition on the revenue curve, show that deterministic mechanisms gain only (Theorem 2), and give a matching lower bound by an explicit randomized construction (Theorem 3). This mission formalizes the lower bound.
A seller sells one item to one buyer. The buyer's value has a cumulative distribution function with density supported on , . Assumption 1 requires to have bounded variation on . Write , the revenue curve (the revenue of a posted price ), and .
A direct mechanism gives a buyer who reports the item with probability and charges . It is individually rational (IR) if for all , and -incentive compatible (IC) if
is the set of IR and IC mechanisms, the expected revenue, and . A best reporting mapping for picks, for each value , a report in .
Local -power envelopes (Definition 1): has a unique maximizer on , interior, and there are , and with and
The parameter measures how flat is at its peak; is the generic smooth case.
Perturbed delayed mechanisms (§5.1). For the buyer is steered to report , equal to below , to on , and to above. With its generalized inverse, the allocation solves on the ordinary and delay differential equations
is above , and the payment is given explicitly in terms of and .
Under Assumption 1 and local -power envelopes there are and such that for all some satisfies
The constants may depend on the distribution, but not on .
The result. Theorem 3 shows that the upper bound of Theorem 1 is tight up to the logarithm. Since for , the revenue gain from approximate incentive compatibility is supralinear in : a seller who exploits -optimizing buyers gains strictly more than the order- gain available to deterministic mechanisms (Theorem 2). Randomization is therefore what makes the relaxation valuable, and the curvature of the revenue curve at the optimal price determines the exponent, which ranges from (as ) to (as ), the latter matching Nisan's universal bound.
Formalizing it. The result is proved in the paper's online appendix; none of it is formalized. A formal development would supply a machine-checked revenue lower bound for an explicit class of -IC mechanisms, a formal treatment of a linear delay differential equation with a piecewise history (method of steps, closed-form solution), and the two-sided bound on , which the paper derives from the renewal function of uniform interarrival times.
The obvious approach, perturbing the optimal posted price or a hard/soft floor mechanism, gains only order (Theorem 2). To gain more, the mechanism must make the buyer misreport downward in a coordinated way, and the allocation that sustains a prescribed misreporting strategy is the solution of a delay differential equation. Three steps are delicate: showing that this solution exists, is unique and is monotone (the delay term couples to ); choosing the delay so that the allocation reaches exactly at , which requires the sharp two-sided bound on and an intermediate value argument; and verifying global -IC, since a best-response argument must rule out every deviation, not only local ones. The final bound balances the gain against losses of order , with of order .
Values are reals, every function is a total function whose values matter only on , and the density is integrable on with total mass . Mechanisms are required to be measurable, which the expectation presumes. is a supremum (sSup); the goal is stated with an explicit witness , which is equivalent because the revenue image is nonempty and bounded above by . is defined as , not as a derivative. The constants are quantified after the distribution and before .
The derivatives in (ODE)-(DDE) are one-sided at the endpoints of their closed intervals. At the two right-hand sides differ, so a two-sided derivative would make the system unsolvable and every statement about its solutions vacuous; this encoding rules out that trivialization. The goal does not mention perturbed delayed mechanisms: any witness is acceptable.
Disclosed additions relative to the page: in the §5.1 statements (presumed by the paper's definition of ); Propositions 3–6 and Lemma 5 are stated for any price with and , since their proofs never use optimality of ; in Proposition 6 the integrand is written in product form because divides by .
A complete development needs: absolutely continuous distribution functions and integration by parts on intervals; existence and uniqueness for linear ODEs and for a delay equation by the method of steps; Irwin–Hall distributions or a direct analytic bound for Lemma 6; and the intermediate value theorem. The delay-equation and results are reusable outside mechanism design. Contributions to any milestone, and alternative proofs of Lemma 6, are welcome.
Fair division asks how to split a divisible resource among agents whose preferences differ. In the non-atomic ("cake-cutting") model the resource is a region of Euclidean space and an agent values each measurable piece. Bogomolnaia and Moulin (arXiv:1911.10009, Mathematics of Operations Research, 2023) study fair guarantees: utility levels that a division rule lets every agent secure for herself, whatever the other agents' preferences and behaviour. Two numbers bracket every such guarantee. Maxmin is an upper bound on any fair guarantee, and minMax is what Kuhn's Divide & Choose rule secures for arbitrary continuous preferences (Theorem 1 of the paper; a companion mission formalizes it).
For utilities that are monotone in the share (the manna is unanimously good), the authors ask whether rules of a different shape improve on minMax. They consider the classical Moving Knife rules, where a knife sweeps the manna and agents shout "stop", and introduce Bid & Choose rules, where a clock runs and the agent who stops it picks any share of a prescribed size. Each rule comes with a computable guarantee, for the knife and for Bid & Choose. The question this mission formalizes is where these guarantees sit relative to the two benchmarks.
The manna is a bounded measurable subset of , , with Lebesgue measure and . A share is a measurable . Shares are compared by the pseudo-metric . A utility is a bounded, -continuous function on shares with ; it lies in if implies .
An -partition of is a tuple of shares with union and pairwise null overlaps; it is an equipartition for if all are equal. The benchmarks are
over all -partitions .
A moving knife is a -continuous path of shares on from to with whenever . A benchmark measure is a probability measure on , mutually absolutely continuous with Lebesgue measure on . Write for the sequences , and
For the guarantees are
For , , every moving knife and every benchmark measure :
The paper also claims . That inequality is false and is not posed. Take , Lebesgue measure and . There is an increasing continuous , built from dyadic "spike" sets, for which while every 2-partition has a share worth about .
A further item records what the page's left-hand argument for does prove: for every .
The goal shows that, for a good manna, a Moving Knife rule is never worse than Divide & Choose by the minMax measure and never promises more than the Maxmin ceiling. Bid & Choose likewise never exceeds Maxmin. Since Maxmin profiles need not be feasible (the paper's Leontief example, p. 16), these inequalities locate the new guarantees inside the only interval where fair guarantees can live.
The mission also corrects the record. The paper is published, but its Lemma 4 and Theorem 2 iii) as printed in the arXiv v3 preprint are not right for . Lemma 4 i) asserts continuity of and Lemma 4 ii) the existence of an equalising -sequence, and both fail for some . The left-hand θ-inequality fails as well. The mission states only true claims and leaves precise statements on record. As far as we know none of these results has been machine-checked. The platform has no prior cake-cutting, moving-knife or equipartition development, so the definitions here are new.
The knife sandwich hinges on an equalising sequence. One must show that is jointly continuous and run an -step intermediate value argument whose optimality proof needs the two-sided monotonicity of . Proposition 1 ii) needs the trimming step. A share must be continuously shrunk inside while its utility is tracked, and then iterated across shares while all trimmed shares are kept equal. This is the longest argument in the mission.
For , the natural first idea is to copy the knife argument: prove continuous, then equalise. It fails, because is an inf–sup over the non-compact space of shares and can jump. The right-hand inequality has to hold for every without any attainment, and any argument for it requires shares of every prescribed -size, i.e. a non-atomicity (Sierpiński-type) argument for .
Space: EuclideanSpace ℝ (Fin d) with volume, and is assumed in every theorem, because in Lebesgue measure is a point mass, which the paper's non-atomic model excludes. Utilities are functions on all subsets, constrained on shares only. Partitions are Fin n-indexed, with union exactly and null pairwise overlaps (not disjointness). Every min/max of the paper is an inf/sup (sInf, sSup), as the paper itself says on p. 9. Each defining set is nonempty and bounded for , which every theorem assumes. Knife continuity is – continuity for on . is mutually absolutely continuous with volume.restrict Ω, with . quantifies over shares , with exact disjointness and exact -sizes. Only is treated, as Theorem 2 states.
Ruled out: as a supremum over a possibly empty set, an inner supremum in over arbitrary sets, the sandwich without monotonicity of , a single rule in place of both, and replaced by its value at one particular . None of these is the paper's statement, and some are trivially true.
Needed infrastructure: δ-continuity of set-valued paths, existence of measurable subsets of prescribed measure for non-atomic measures on , and intermediate-value arguments in several variables. The model definitions are reusable for any non-atomic fair-division development. Proofs of any item are welcome, as are formal versions of the counterexamples to the θ claims.
In large server farms and cloud platforms, not every server can process every task. Data locality, licences, hardware and security rules restrict each task type to a subset of servers. Such compatibility constraints are modelled by a bipartite compatibility graph between task types (dispatchers) and servers. Classical mean-field results for load balancing, such as Mitzenmacher's analysis of the power of choices (Mitzenmacher 2001) and Vvedenskaya, Dobrushin and Karpelevich's supermarket model (1996), assume full flexibility: every task may join every server. Rutten and Mukherjee (arXiv:2008.07562, Math. Oper. Res. 2023) identify graph conditions under which JSQ() on a sparse compatibility graph behaves, in the large-system limit, exactly like the fully flexible system. This holds both on finite time intervals and in steady state.
Related work includes Budhiraja, Mukherjee and Wu (2019), on the supermarket model on graphs whose vertices are servers; Mukherjee, Borst, van Leeuwaarden and Whiting (2018), on the universality of power-of- schemes; and Bramson (2011) and Cardinaels, Borst and van Leeuwaarden (2019), on the stability of JSQ-type policies under compatibility constraints.
There are servers and dispatchers , with an edge set . Dispatcher can only send tasks to its neighbourhood .
The state is the vector of queue lengths. Two statistics of a state are used:
Occupancies live in .
The sequence is proportionally sparse if for every
Put . The sequence is subcritical if there are probability distributions on the sampled sets with
This bounds the load that a static randomised routing would put on any server.
The fully flexible mean-field limit is the system of ODEs
whose fixed point is .
Let be proportionally sparse and connected, and suppose with . Then, for every and ,
If moreover is subcritical, then for all large the chain has a unique stationary distribution , and .
The result. The theorem separates two graph properties.
Together they justify using the fully flexible ODE (3.3) and its fixed point for the stationary performance of a constrained system. Companion results (Theorems 3.5 and 3.6, formalized in missions 2 and 3 of this series) show that random graphs with degrees growing only slightly faster than logarithmically satisfy both conditions, so the flexibility needed for full mean-field performance is far smaller than complete flexibility.
Formalizing it. The result is proved on paper but has no machine-checked proof. A formalization would produce the following.
The global stability of (3.3) relies on Mitzenmacher's weighted-potential theorem, which is posed separately on the platform (PowerTwoChoices.Limit.theorem_3) and is open.
The obvious argument couples the system on with the fully flexible system server by server. This fails because a task arriving at can only join , so the two systems cannot place it at the same server. The paper instead couples the queue lengths chosen and counts mismatches. That bound is only useful if almost every dispatcher sees a local queue-length distribution close to the global one at all times. The set of good dispatchers changes with the state, and controlling it requires a uniform bound over all subsets of servers.
A second gap concerns the goal itself. Theorem 4.3 covers policies that depend only on the local empirical distribution. JSQ() without replacement also depends on when neighbourhoods are small, so deducing the goal from Theorem 4.3 needs an approximation step that the paper does not spell out.
For the steady state, subcriticality bounds a only, so stability holds for large and not for every . Tightness in a fixed -ball does not suffice: the limit is identified through a stability result that holds in a weighted norm with geometrically growing weights. The tightness has to be proved in that norm, through moment bounds on stationary tails.
Fin N, dispatchers Fin (M N) with , and edges a Finset. Connectivity is a separate hypothesis (Definition 3.1 and §2). Proportional sparsity is the limit condition (3.1). In subcriticality the normaliser is , and the distributions are constrained only for nonempty . Both choices agree with the paper whenever .lbKernel, run at the epochs of an independent Poisson clock of rate . Statements quantify over every realisation on every probability space, for . JSQ() samples without replacement; with replacement, Theorem 4.8 is false under Definition 3.3.l1dist in . "Converges weakly" to a deterministic limit is rendered as convergence in probability. Ergodicity is rendered as existence and uniqueness of a stationary distribution.PowerTwoChoices.Limit.SupermarketSystem (the ODE, fixed point and potential) and PowerOfDUniversality.Fluid.FluidSpace (l1dist, supDistL1).CountableChain: stationarity, -step kernels, petite sets and uniformisation.Contributions to any milestone are welcome. Lemma 4.2, Proposition 4.7 and Lemma H.4 are self-contained.
Ride hailing, online advertising and kidney exchange share a decision problem: resources that are present from the start must be matched, irrevocably and one at a time, to requests that arrive at random. When the arrival probabilities are known in advance, the natural benchmark for an online algorithm is not the offline optimum (the "prophet", who sees every arrival in advance) but the optimal online algorithm: the best expected profit any algorithm can earn when it must decide without seeing the future. That benchmark is well defined and computable in exponential time, so the question becomes one of approximation algorithms: how much of it can a polynomial-time algorithm guarantee?
Papadimitriou, Pollner, Saberi and Wajc (arXiv:2102.10261, Math. Oper. Res. 2024) answer both halves of that question for online Bayesian bipartite matching. They show that approximating the optimal online algorithm within some constant is PSPACE-hard (Theorem 1.1, not part of this mission), and they give a polynomial-time algorithm that earns a fraction of it (Theorem 1.2). The number matters because is the best possible ratio against the prophet, already for a single bin, so shows that comparing with the online optimum genuinely permits better guarantees.
Timeline:
A RideHail instance has a finite set of bins (taxis) and balls (passengers) , revealed in this fixed order. Ball arrives with probability , independently of every other ball. If it arrives it may be matched, irrevocably and before ball is revealed, to an unmatched bin , earning . A deterministic online policy chooses the bin for ball as a function of the arrivals of balls only. Its expected profit is the average, over the arrival patterns, of the total weight of the matching it builds, and is the largest expected profit over all such policies.
LP-Match is the linear program in variables , read as "the probability that the algorithm matches to ":
Its optimal value is . The third family of constraints, (11), holds for online algorithms only.
Algorithm 1 (Rounding LP-Match Online), with , takes an optimal solution of LP-Match, adds a weight-zero dummy bin for each ball so that , and then processes the balls in order. When ball arrives it picks a bin with probability . If is vacant, is matched with probability
If is still unmatched, it picks again from the same distribution, and is matched to the new pick when that bin is vacant and . Edges added by the first pick form , those added by the second pick form , and .
For every instance and every optimal solution of LP-Match,
where is the output of Algorithm 1 run on .
The milestones follow the paper's proof. LP-Match is a relaxation of the online problem (Lemma 4.1). Algorithm 1 matches every edge with probability at least (Theorem 4.2), which rests on two bounds:
Lemma 4.8 comes from the negative association of early-occupancy indicators: Lemma 4.9 and Corollary 4.10, resting on Definition 2.5 and Propositions 2.6–2.8.
The result. Theorem 1.2 is the first polynomial-time algorithm for online stochastic matching with a ratio above against the optimal online algorithm. It separates the online benchmark from the prophet benchmark in an algorithmic sense, and its main technical step, bounding positive correlation between bins' matched statuses through negative association, has been reused for online edge colouring.
Formalizing it. The result is proved on paper and is not machine-checked anywhere. The mission produces:
The negative-association layer (Definition 2.5, Propositions 2.6–2.8) is general probability, absent from Mathlib, and reusable well beyond this mission.
The obvious argument fails at the second pick. Once ball has been rejected by its first pick, the events "bin is vacant" and "the first pick was rejected" are dependent, for two reasons:
Either effect alone can make the second pick useless. The first is controlled by Constraint (11) (Lemma 4.7). The second needs a quantitative bound on the covariance of vacancy indicators (Lemma 4.8), proved by splitting occupancy into early and late parts and showing that the early parts are negatively associated, through a coupling of the algorithm's randomness with independent pick and coin variables. Lemma 4.1 is also not routine to formalize: it requires turning an arbitrary history-dependent online policy into a feasible LP solution, using the independence of arrivals from past decisions.
Conventions committed to in Lean (namespace OnlineMaxWeightMatch.Approx):
ι; balls are Fin n in arrival order (paper ball is index ). Weights and probabilities are real numbers with and ; missing edges have weight .Option-valued: "no bin" carries the leftover mass . When , is in Lean and the ball never arrives.ι ⊕ Fin n with weight . A dummy first pick is accepted with probability and consumes the ball's turn, as in the paper. A dummy is never matched as a second pick.ProbabilityTheory.cond, which is on null events. Equation (20) and Lemma 4.7 therefore carry positivity hypotheses (, ) that make the conditioning event non-null.ProbabilityTheory.covariance."Polynomial time" is not formalized. Because "some online algorithm earns " is trivially true of the optimal online algorithm itself, the goal names Algorithm 1 run on an arbitrary optimal LP-Match solution. That solution exists, so the goal is not vacuous. Replacing by an offline benchmark, dropping Constraint (11), restricting to non-adaptive policies, or treating the dummy pick as "pick nothing" would each change the theorem.
Infrastructure a complete development needs: negative association with its closure properties, finite product probability spaces, conditioning on events, covariance of indicators, and linear-programming feasibility arguments for online policies. Contributions to any milestone are welcome; the probability layer (Propositions 2.6–2.8) is independent of the rest.
Community detection asks for a partition of the vertices of a graph into groups that are densely connected inside and sparsely connected across. In its simplest form there are two communities of equal size, and the natural combinatorial formulation is the minimum bisection problem: among all ways of splitting the vertex set into two halves, find one that cuts the fewest edges. The problem is NP-hard in general, yet on graphs that genuinely contain two well-separated communities one expects it to return exactly those communities. For the two-community stochastic block model, minimum bisection is the maximum a posteriori estimator, so understanding when it returns the hidden partition is the baseline against which convex relaxations are compared.
Del Pia, Khajavirad and Kunisky (arXiv:2006.03213v2, Mathematics of Operations Research 2023) study this question deterministically, without a random graph model, in terms of two worst-case degree parameters. Their Theorem 1 gives a sufficient condition for the minimum bisection problem to recover the hidden partition, and Theorem 2 shows the condition cannot be weakened. The rest of the paper compares this with the metric linear programming relaxation of minimum bisection. This mission formalizes Theorem 1.
Let be a simple graph on . A bisection of is a partition of into two sets of equal cardinality ; it exists only for even . Its cost is the number of edges with one end in each set. The minimum bisection problem asks for a bisection of minimum cost.
A fixed bisection , unknown to the solver, is the planted bisection. Write and for the subgraphs induced on the two sides and for the bipartite graph of edges between them. Two parameters measure how well the planted bisection separates the graph:
An optimization problem recovers the planted bisection if its unique optimal solution corresponds to the planted bisection. For minimum bisection a solution is an unordered partition, so this means: every bisection whose cost is at most that of is the partition itself.
The hypothesis is the only one; no connectivity, regularity or lower bound on is assumed.
Fix a second bisection and set , , , , . Let be the edges between and or between and , the edges between and or between and . The paper's proof combines
The last two hold for every pair of bisections.
Theorem 1 is a purely combinatorial certificate of exact recovery: it applies to any graph, random or not, and its two parameters are computable in linear time. Together with Theorem 2 of the same paper, which shows that for every divisible by eight and every admissible with some graph is not recovered, it determines exactly which degree pairs guarantee recovery. The paper then shows that the metric LP relaxation recovers under the nearly identical condition with an additional regularity assumption, so the LP loses almost nothing against the NP-hard problem in this deterministic regime.
The theorem and its proof are published, and the proof is elementary. To our knowledge no machine-checked version exists. Formalizing it fixes a reusable Lean vocabulary for planted bisections (bisections as Finsets, intra- and inter-community degrees, cut cost, recovery up to swapping the sides). The later missions of this series, on the LP relaxation and on the stochastic block model, use the same vocabulary.
The argument is short, and the work lies in the bookkeeping. The obvious contrapositive step, "an optimal bisection different from the planted one cuts at most as many edges", only compares two totals. The proof has to split those totals into the six edge classes between the four sets , and it relies on the identity , valid for any two bisections. The lower bound on needs a double-counting step: the degrees inside of the vertices of sum to at least , and edges inside account for at most of that sum. In Lean the edge classes are filters over ordered pairs , so each identity between them is a statement about disjoint unions of finite sets. The quantity can be negative, so the integer arithmetic must not truncate.
Fin n (0-based, the paper's ), graphs are SimpleGraph (Fin n), and a bisection is a Finset V1 with 2 * V1.card = n, the other side being V1ᶜ. The second bisection of the proof is a Finset W, with = Wᶜ.dIn is the minimum over all vertices of the number of same-side neighbours (defined as when ), and dOut is the maximum over all vertices of the number of other-side neighbours. They are the paper's parameters, not free integers.∀ S, IsBisection n S → cutCost G S ≤ cutCost G V1 → S = V1 ∨ S = V1ᶜ. Requiring S = V1 alone would make the theorem false, since has the same cost.The definitions are finite and decidable in principle and need nothing beyond Mathlib's SimpleGraph and Finset. Contributions of proofs of the three milestones and of the goal are welcome. Lemmas expressing the cut cost of as and that of as are useful intermediate results.