Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Online advertising sells billions of impressions a day through auctions, and most advertisers do not bid by hand: they hand a budget to the platform, which paces their bids so that spending over a campaign matches the budget. Over the last decade the major ad exchanges moved from second price to first price auctions. An advertiser who has tuned a pacing policy for one format wants to know whether it still works after the switch, and a platform wants to know whether its revenue changes.
Classical revenue equivalence (Myerson 1981; Riley and Samuelson 1981) says that, with independent private values, risk-neutral buyers and no budgets, every standard auction yields the same expected revenue. Che and Gale (1998) showed that this fails when budgets are hard: first price auctions then raise more revenue than second price auctions. Balseiro, Kroer and Kumar (2023) study budgets that bind in expectation over many auctions, with values driven by item features, and show that equivalence is restored. This mission formalizes that result, their Theorem 2.
An item has a context drawn from a law with a density. Each of buyers has a type drawn independently from a law with a density on . Here are feature weights and is a budget. The buyer's value for the item is , and is the supremum of all values. The seller discloses , then runs an auction with reserve price . A buyer must keep its expected payment, over contexts and competitors' types, at most .
A pacing function shades every value to the paced value . Let be the law of the paced value when , and the c.d.f. of the highest of independent paced values. In first price auctions the paper's candidate strategy is , where is the first-price equilibrium bid against paced competitors.
The buyer's dual function is the supremum over bid functions of the Lagrangian , with competitors bidding . The set collects pacing functions with values in and total variation at most . The correspondence is the set of minimizers over of . A fixed point is an equilibrium pacing function for first price auctions.
An anonymous standard auction gives the item to the highest bid at or above the reserve. Its payment for a bid against competing bids does not depend on the buyers' identities. An oracle returns, for each atomless value law on , a single-auction equilibrium bid that is nondecreasing, meets the reserve exactly for values above it, gives a zero-value bidder zero payoff, and has an atomless bid law. The candidate strategy is
For every family of anonymous standard auctions with such an oracle and every with :
Theorem 2 says that pacing is portable: an equilibrium pacing function computed for first price auctions is an equilibrium pacing function for second price auctions, all-pay auctions, or any context-dependent mixture of standard formats. Each buyer's expected spend is the same in all of them, so the seller's expected revenue is too. This explains why budget-management systems built for second price auctions keep working after a move to first price. It also separates in-expectation budgets, where equivalence holds, from the hard budgets of Che and Gale, where it fails. Theorem 3 of the same paper, a liquid-welfare price of anarchy of , uses Theorem 2 to argue in the second price auction.
The paper's proofs are in its online appendix, which is not part of the source this mission cites. To our knowledge no part of the argument has been machine-checked. Classical revenue equivalence for incentive-compatible direct mechanisms without budgets exists on the platform as other items, but none has pacing, budgets or contexts. The mission asks for a machine-checked proof of Theorem 2 and of the two steps the authors name.
The classical argument pins payments by the allocation rule and the envelope formula, value by value. Here a buyer's decision is a whole bid function of the context, coupled across contexts by one budget constraint, and the budget-constrained problem is not convex. So the envelope argument cannot be applied to the constrained problem directly. The obvious move, Lagrangian relaxation, needs strong duality for a non-convex problem, and it needs the dual of each standard auction to agree with the first-price dual for every multiplier, not only at the optimum. The paced value laws need not have densities, so the textbook single-auction results, which assume a positive density, do not apply verbatim. Finally, the fixed-point hypothesis ties all buyer types together, and optimality must be recovered almost surely in the type.
Everything is defined in the namespace ContextualAuctions.RevEquiv. Contexts are Fin d → ℝ, types are (Fin d → ℝ) × ℝ, and is an explicit sum. The joint law of the context and the competitor types is F.prod (Measure.pi fun _ => G). Ties win, as in the paper's tie-breaking rule. The standing assumptions are , and probability measures with densities concentrated on and , in the open positive orthant, and measurable. Disclosed additions, implicit in the paper:
The dual function is the supremum over admissible bids, which are measurable with integrable payment. Its closed form is a milestone and never its definition. Total variation (Definition 3) is extended-real valued and uses the Euclidean norm of the test field. In oracle property 1, expected payments are taken in , so a bid with infinite expected payment can never look free. The payment identity of Theorem 2 is stated in , so it also asserts that the left side is finite. This rules out the trivializing readings: a closed-form definition of that makes the first milestone hold by definition, Bochner junk zeros for non-integrable payments, and a vacuous variation bound.
A complete development needs single-auction revenue equivalence for i.i.d. atomless value laws without densities. It also needs the measure-theoretic interchange of a supremum over bid functions with the expectation over contexts, and strong duality for the budget-constrained problem. These pieces, notably the single-auction equivalence for general atomless laws, are reusable beyond this mission. Contributions toward any of them are welcome.
Many optimization problems are posed over a manifold rather than a vector space: orthogonality constraints (the Stiefel manifold), unit-norm constraints (the sphere), fixed-rank matrices. In some of them the objective can only be evaluated, not differentiated. Black-box adversarial attacks on a neural network with a norm-constrained perturbation, hyperparameter tuning and simulation-based objectives are examples, and in all of them each function value is also noisy. Zeroth-order (derivative-free) methods replace the gradient by a random finite-difference estimate built from function values alone.
In Euclidean space the analysis of such methods is well developed. Nesterov and Spokoiny (2017) analysed Gaussian-smoothing estimators for deterministic objectives, and Ghadimi and Lan (2013) gave the first non-asymptotic stationarity rates for stochastic nonconvex objectives (the RSGF method). Li, Balasubramanian and Ma (arXiv:2003.11238, published in Mathematics of Operations Research, 2023) carried this programme to embedded submanifolds. They estimate the Riemannian gradient by projecting a Gaussian vector onto the tangent space and moving along a retraction, and they prove convergence rates for the resulting methods. This mission formalizes their rate for the stochastic method, ZO-RSGD (Theorem 3.2).
Let be a finite-dimensional real inner product space (the paper's ), and let be a embedded submanifold of dimension . The tangent space at is the linear span of the tangent cone of at . For a submanifold this is the set of velocities of curves in through , and it is a subspace of dimension . carries the metric induced by the inner product of , and denotes the orthogonal projection of onto .
A retraction is a map , . For every it sends all of into and is smooth on , with and differential the identity at . The Riemannian gradient of a differentiable is .
The objective is stochastic, , with noise distributed according to a probability measure . Two assumptions are imposed:
Given a smoothing parameter and a batch size , draw independent pairs , each with independent of , and put . The mini-batch zeroth-order Riemannian gradient is
ZO-RSGD (Algorithm 2) starts at and iterates with step and a fresh batch at every step. denotes a minimizer of over .
If , then for every
The constants are the paper's own. The goal states the rate for every , and . It does not state the parameter choices , , that follow from it.
Theorem 3.2 is the basic complexity result for derivative-free stochastic optimization on manifolds. With the parameter choices of (3.10) it gives an -stationary point in expectation after noisy function evaluations. The dependence is on the manifold dimension , not on the ambient dimension . This matches the Euclidean rate of Ghadimi and Lan with replaced by , and it is what makes projected-Gaussian estimators attractive when (for example, low-dimensional Stiefel manifolds embedded in large matrix spaces).
The results are proved in the paper (main text, p. 17, and Appendix C) but, to our knowledge, none of them has been machine-checked. The Euclidean Gaussian moment bound (Lemma 2.2) is formalized on the platform. The Euclidean RSGF results of Ghadimi and Lan are stated on the platform, and they are different statements: they use instead of a retraction, the full space instead of a tangent space, and a random output index. A complete formalization would also produce reusable infrastructure: Gaussian identities for orthogonal projections, the projected-Gaussian moment bound, and a template for proving stationarity rates of random iterates on a product probability space.
The Euclidean argument relies on a smoothed function whose gradient is exactly the mean of the estimator. That identity has no Riemannian analogue: is not a translate, so is not the gradient of any smoothed function. The bias in Proposition 2.1(a) has to be bounded directly from Assumption 2.1, and this is why the estimator is only approximately unbiased.
The convergence proof needs a one-step descent inequality conditioned on the past. The direction at step is projected onto , which depends on all earlier draws, so the conditional bound of Lemma 3.1 must be integrated against the product law of the batches. A naive reading that samples every direction from one fixed subspace, or that treats the iterates as deterministic, does not describe the algorithm. A further subtlety is that the gradient term of Lemma 3.1 must be absorbed by the descent of one step. This requires the batch to be large compared with the dimension, .
stdGaussian E.ProjLikeRetr.Retractor.IsSubmanifold 1 d M (a coordinate-slice submanifold), so is tied to and is never a free number. is the published ProjLikeRetr.Retractor.tangentSpace M x, never an arbitrary subspace.ENNReal.ofReal of the bound. Every vector-valued expectation comes with an integrability conclusion, and Assumption 2.3 carries the integrability of and . So no statement can hold because a Bochner integral defaulted to .stdGaussian under an orthogonal projection.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.
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.
Decoded quantum interferometry (DQI) is a quantum algorithm, introduced by Jordan, Shutty, Wootters, Zalcman, Schmidhuber, King, Isakov, Khattar and Babbush (arXiv:2408.08292), that turns an approximate optimization problem over a finite field into a decoding problem for a linear code. It applies to max-LINSAT: given linear constraints over , satisfy as many of them as possible. For structured instances such as optimal polynomial intersection the authors find DQI reaching approximation ratios that no known polynomial-time classical algorithm reaches, which makes it one of the few concrete candidates for a quantum advantage in optimization.
Whether DQI is useful on an instance depends on one number: the expected fraction of constraints satisfied by the string it outputs. Theorem 4.1 of the paper computes this number, in the limit of many constraints, for the best DQI state of a given degree. Every comparison of DQI with classical algorithms in the paper (simulated annealing, Prange's algorithm, the OPI and max-XORSAT benchmarks) is a comparison against this formula, and the follow-up analysis of imperfect decoders (Theorem 10.1) is a perturbation of it.
Fix a prime . A max-LINSAT instance is a matrix with rows and subsets ; constraint asks that (Definition 2.1). Throughout, and every has the same size . Put if and otherwise, and
For a real polynomial of degree at most , the DQI state is , normalized so that . Measuring it in the computational basis returns with probability , so the expected number of satisfied constraints is
and is its supremum over all such .
The dual code is and is the least Hamming weight of a nonzero codeword. The condition says that syndromes of errors of weight up to (and a little more) determine the error.
The analysis passes through rescaled constraint functions with Fourier transforms , the elementary symmetric polynomials evaluated at the , and the symmetric tridiagonal matrix with diagonal and off-diagonal entries , at .
Fix , and . For any sequence of instances with , and , writing ,
For the curve is , a semicircle, which gives the theorem its name.
The result. Theorem 4.1 makes DQI's performance a closed-form function of two numbers, and , and moves every question about an instance into coding theory: how large a the instance's dual code has, and whether it can be decoded efficiently up to errors. The OPI advantage claim of the paper, the comparison with Prange's algorithm on max-XORSAT, and the imperfect-decoding bound of Theorem 10.1 all start from this formula. The finite-size identity (131) is also useful on its own: it gives the exact optimum for any instance, not only in the limit.
Formalizing it. The theorem is proved in the paper; to our knowledge no part of it has been machine-checked. A formalization would check the Fourier bookkeeping of §8.2.1 and §9 (normalizations , character sums over ), the claim that every degree- DQI state is a combination of the and conversely, and the eigenvalue asymptotics of the tridiagonal matrix. Two points of the printed text need care and are stated correctly here: Lemma 9.2 writes its decomposition in the where the normalization requires the rescaled , and the "otherwise " branch of Theorem 4.1 is argued only briefly on p. 34.
The algebraic steps are finite but long, and every one carries a normalization that a careless formalization gets wrong. The asymptotic step is the main obstacle. Lemma 9.3 needs a lower bound on from a test vector of growing width and a matching upper bound from Gershgorin's theorem, and the upper bound holds only under , which is exactly the regime . In the other regime that hypothesis fails and the Gershgorin bound overshoots, so the limit needs a separate argument; the observation that "increases in ", printed on p. 34, does not give it at fixed and . A second difficulty is that is a supremum over polynomials, while Lemma 9.2 is a statement about weight vectors ; identifying the two needs both directions of Lemma A.1's correspondence and the normalization of Lemma 9.1.
All objects live in the namespace DQI.Semicircle and one definitions file. is ZMod p with [Fact p.Prime]; vectors are Fin n → ZMod p; constraints are indexed by Fin m from . is computed from the representative of in . Polynomials are real with natDegree ≤ ℓ; weight vectors are real. The optimum is the real supremum over exactly the normalized polynomials of degree at most evaluated at ; its set is nonempty (constant polynomials) and bounded by . The dual-distance condition is "every nonzero with has weight "; is never an infimum, and (the paper's standing assumption) guarantees a nonzero codeword, so the condition forces . is the supremum of the real spectrum. The limit " with fixed" is any sequence of instances with and , with and fixed along it. Convergence of the ratio includes irrational with integer sizes.
Added hypotheses, all disclosed in the items: Lemma 9.2 decomposes in the rather than the printed ; (129) assumes to avoid dividing by ; Lemma 9.3 imposes its hypothesis on only when ; (114) is stated as a with an explicit .
A formalization that replaces by a supremum over all states (which gives ), drops "nonzero" from the distance condition (which makes it unsatisfiable), or states the goal at a single is not this theorem and is ruled out by the definitions above.
Needed infrastructure: Fourier analysis on (character orthogonality, Parseval), elementary symmetric polynomials and their reduction modulo a quadratic, Rayleigh quotients and Gershgorin discs for real symmetric matrices, and elementary limits. The tridiagonal-matrix bounds and the quadratic-reduction lemma are reusable beyond DQI. Proofs of any milestone, alternative arguments for the "otherwise" branch, and sharper finite- bounds on are welcome.
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.Two-player zero-sum matrix games are the simplest model of strict competition, and computing their value is equivalent to linear programming. Many algorithms in optimization and learning (boosting, online learning with experts, approximate LP and SDP solvers) are, at their core, procedures that approximately solve such a game. For large games the cost of reading the whole payoff matrix dominates, so algorithms that look at only a small part of it are of direct interest.
Grigoriadis and Khachiyan (Operations Research Letters 18(2), 1995) gave a randomized algorithm that finds a pair of -optimal strategies for an game with entries in after iterations, each of which touches only one row and one column of the matrix. They also showed that every deterministic algorithm must read entries. Van Apeldoorn and Gilyén (arXiv:1904.03180v1, 2019) re-prove the correctness of this algorithm directly for non-symmetric games (Lemma 1, p. 3) and then speed up its sampling step on a quantum computer. Lemma 1 is the classical guarantee that their quantum algorithms (Theorems 9 and 11) inherit.
A matrix game is a matrix with entries , . Alice chooses a row and receives ; Bob chooses a column and receives . Mixed strategies are probability vectors and . The value of the game is
Bob's strategy is -optimal if for every , and Alice's is -optimal if for every .
The Gibbs distribution of a vector is (Definition 5, p. 7).
Algorithm 1 (p. 3) keeps cumulative vectors and , both starting at . In iteration it uses a step , samples independently
and updates and . Each player thus plays a smoothed best response to the other's empirical play, which connects the method to fictitious play. After iterations the candidate strategies are the normalized vectors and . In the fixed accuracy-goal version the step is .
For and , Algorithm 1 run with satisfies, for every ,
The goal is the fixed-step statement because it is the form invoked by the paper's later results and it carries the paper's explicit constant . The anytime statement is stronger in one respect (a single event for all ) and is posed as a further target.
Lemma 1 says that the sampled dynamics converge to an -equilibrium in rounds, each of which reads one row and one column of . That gives sublinear-time approximation of the game value, and it is the classical skeleton of the paper's quantum algorithms: Theorems 9 and 11 run exactly this iteration, replacing the classical Gibbs sampler by a quantum one. Through the reduction of §4 (Lemma 12), the same iteration also yields the paper's LP solvers.
The result is proved in the paper and in [GK95]. As far as is known it has no machine-checked proof. Formalizing it fixes a precise probability law for a sequential randomized algorithm whose sampling distribution depends on the whole history, and it records exactly where each constant (, , ) comes from. The milestones (a potential identity, a one-step expectation bound, Markov's inequality on a finite path space) are pieces of the multiplicative-weights analysis that recur throughout online learning.
Each step is elementary, but the statement concerns a randomized process, not a deterministic one. The iterates are random, and the distribution of each draw depends on all previous draws. The obvious approach of bounding the potential pathwise fails: on unfavourable paths can grow like , so a high-probability statement is unavoidable. Making that rigorous needs the conditional expectation of the next potential given the past, iterated over the path law, followed by Markov's inequality and a union of pointwise consequences. The bookkeeping also needs care: the step index, the fact that , and the requirement under which the quadratic bound on applies.
A : Matrix (Fin n) (Fin m) ℝ with |A i j| ≤ 1 and 0 < n, 0 < m. The value is the infimum of over the image of stdSimplex ℝ (Fin m). It is not written as ⨅ y ∈ stdSimplex …, which over ℝ evaluates to , and ε-optimality is measured against this value. LP (1)'s constraint is inactive and not encoded.stdSimplex, Matrix.mulVec, Real.exp/Real.log and finite sums. The finite path-law calculus (a tower property over the last draw, Markov's inequality for a finite weighted sum) is reusable for other sequential sampling algorithms. Contributions of proofs of any milestone are welcome. A PMF-based restatement proved equivalent to the finite-sum law would also be useful.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.
Many optimization models in statistics, signal processing and machine learning minimize a smooth loss plus a nonsmooth regularizer, . When is quadratic this is the quadratic composite problem, which also appears as the subproblem of sequential quadratic programming and of proximal Newton methods. First-order splitting methods (proximal gradient, forward-backward) handle such problems with only the proximal mapping of , but converge at best linearly. Newton-type methods converge superlinearly but classically need either smoothness or convexity of , or strong regularity (uniqueness and Lipschitz stability) of the solution.
Khanh, Mordukhovich and Phat (arXiv:2009.10551v2, 2022; Mathematics of Operations Research 2023) designed a Newton-type method for the stationarity inclusion of a nonconvex composite cost whose steps use only the proximal mapping and the second-order subdifferential (generalized Hessian) of , and proved local superlinear convergence under metric regularity rather than strong metric regularity. This mission formalizes that result, Theorem 7.8 of the paper, together with the chain of propositions through which it is proved.
Work in with the Euclidean inner product. A function is proper if it is finite somewhere, and prox-bounded if it is bounded below by a quadratic . The limiting subdifferential collects limits of Fréchet subgradients at nearby points with nearby values.
For a set-valued map the limiting coderivative is the set of with a limiting normal to at ; the second-order subdifferential is . is metrically regular around if near , and semismooth* at if for every in the directional coderivative .
is prox-regular at for with modulus if it is lower semicontinuous near and, for some ,
for within of , and within of ; continuously prox-regular if in addition along subgradient pairs .
The cost is with , symmetric. The proximal mapping is the argmin set of , and the forward-backward envelope (FBE) is
Algorithm 7.6 with parameter : if stop; otherwise set , pick , choose with
and set .
Let be proper, prox-bounded and continuously prox-regular at a stationary point () for with modulus , and let satisfy at : (H1) solvability of near , (H2) metric regularity, (H3) semismoothness*. Then
and every run from converges Q-superlinearly to .
The result gives a locally superlinear method for nonconvex composite problems that uses only first- and second-order information of the regularizer, and it replaces strong metric regularity, which forces isolated solutions, by metric regularity. The FBE reduction (Propositions 7.2–7.5) is reusable on its own: it identifies the stationary points, the generalized Hessian, and the regularity of a nonsmooth composite cost with those of a smooth function.
Formalizing it builds the first machine-checked library of coderivative calculus on Prove2Me: normal cones to graphs, limiting and directional coderivatives, second-order subdifferentials, metric regularity and semismoothness*. As far as the platform record shows, none of the paper's results has a machine-checked proof. The paper's proofs lean on second-order sum and chain rules from Mordukhovich's monograph and on Poliquin–Rockafellar's analysis of Moreau envelopes of prox-regular functions; those external results are part of the work.
The FBE of a nonconvex is not globally smooth; its smoothness near comes from the local single-valuedness of , which prox-regularity provides only for small and only near . The printed parameter range is too large: a far-away deep well of can capture the proximal point (see the correction below). Transferring (H1)–(H3) from to requires exact second-order calculus (sum and chain rules for coderivatives), not inclusions, and metric regularity is not preserved by the obvious estimates: the paper uses a coderivative characterization. Finally, Theorem 5.7 itself requires an inexact Newton analysis in which the Newton inclusion is solved by an arbitrary element of a coderivative, not by a matrix.
EuclideanSpace ℝ (Fin n); products carry the sup norm, which does not change any normal cone. A symmetric is a self-adjoint continuous linear operator.EReal; is assumed proper. The envelopes are EReal-valued infima; wherever is differentiated, finiteness on a neighbourhood is asserted and the real-valued function is differentiated. is the derivative of gradient f.NonconvexSplitting.Shared.LimitingSubdiff. It agrees with the paper's geometric definition (2.9) for functions lower semicontinuous around the point, which covers every function the statements apply it to.Impact investing selects securities by a non-financial characteristic: an ESG rating, a carbon-intensity metric, a "sin stock" flag. A recurring question in finance is whether such a selection costs or earns the investor anything, and by how much. Lo and Zhang (SSRN 3944367; Management Science, doi:10.1287/mnsc.2022.01168) give a closed-form answer in a stylised model: the excess return of a portfolio formed by ranking securities on an impact factor is governed by the correlation between that factor and the securities' unobserved excess returns. The mathematical tool is the theory of induced order statistics (concomitants), introduced by Bhattacharya (1974) and David (1973) and surveyed in David and Nagaraja, Order Statistics (2004), §6.8. The same tools were used by Lo and MacKinlay (1990) to quantify data-snooping biases in asset-pricing tests.
There are securities. Security has an observable impact factor and an unobservable excess return (the part of its return not explained by priced factors). Under Assumption (A1) the pairs , , are independent and identically distributed bivariate normal with means , variances and correlation . As the paper does before its Proposition 2, the mission takes , and .
An investor ranks the securities by . Let be the permutation sorting increasingly. The order statistics are , and the induced order statistics are
the excess return of the security whose impact factor has rank (display (6) of the paper). The vector is not sorted by its own values; its order is induced by .
An impact portfolio holds the securities of a set of ranks with weights summing to one; its excess return is
The paper prints the last line with where is needed. The two agree only when or . For , and , the true variance is and the printed expression gives . The goal states the corrected identity.
The result. Proposition 6 reduces the first two moments of any rank-based impact portfolio to three parameters (, , the weights) and to moments of standard normal order statistics, which are tabulated. The sign of alone decides whether a portfolio of top-ranked securities has positive, zero or negative expected excess return. That is the paper's quantitative answer to whether impact investing helps or hurts returns. The variance formula is what the paper's later results build on: Sharpe and information ratios of impact portfolios, Treynor–Black weighting (Proposition 7) and combination with a passive index (Proposition 8).
Formalizing it. The proposition is proved in the paper; the mission is a machine-checked version of it. The proof needs a reusable, currently absent piece of probability in Lean: moments of induced order statistics of Gaussian pairs, including the behavior of residuals carried along by a sort keyed on an independent sample. No order-statistic or concomitant result of this kind is on the platform or in Mathlib. The mission also records a corrected form of (31), whose printed version is false whenever .
The algebra from Proposition 2 to Proposition 6 is the bilinearity of variance and covariance. The substance is in Proposition 2, and specifically in the step from (A.21) to (A.22). The permutation that sorts is random, so is a residual read at a random index. The tempting argument treats as "an ", which would give mean zero and variance immediately. That argument is incomplete: it needs the joint law of conditional on , which requires that is a function of only, that is independent of , and that the law of is invariant under permutations. None of this is written out on the page, and none of it is in Mathlib; integrability and measurability of the order statistics must also be established, since the Lean moments are defined without them.
All declarations live in the namespace ImpactInvesting.Portfolio. Order statistics use Mathlib's Tuple.sort: orderStat x i = x (Tuple.sort x i) and inducedOrderStat x a i = a (Tuple.sort x i). Ranks are 0-based: i : Fin N is the paper's rank . Ties are broken by index; they have probability zero under (A1), and no no-ties hypothesis is added.
Assumption (A1) is the predicate IsA1 P X α σα ρ. Each pair (X i, α i) has a Gaussian law (HasGaussianLaw), the pairs are mutually independent (iIndepFun), and the moments are fixed: , , , , . Identical distribution follows, because a bivariate Gaussian law is determined by these moments. The normalisations , , are hypotheses, not a without-loss-of-generality step; (8) is false without . The ranges and are explicit hypotheses. Moments are the Bochner integral P[·], Var[·; P] and cov[·, ·; P]. No integrability hypotheses are added: order statistics of Gaussian samples are in every , and proving this is part of the work. The portfolio is a Finset (Fin N) of ranks with weights w : Fin N → ℝ summing to one on it; is taken in the order of Fin N.
A formalization in which the "order statistics" are not sorted, or the induced statistics are sorted by itself, would make the statements trivial or false; the definitions sort by and read at the same permutation. The printed second line of (31) is not stated anywhere, because it is false.
Out of scope: the multi-factor return model (1)–(2) beyond the role of , Treynor–Black weights (Proposition 7), combined portfolios (Proposition 8), the asymptotic expansions and limits (Propositions 3, A.1, A.2), and the omitted-factor model (Proposition 5, a separate mission). Contributions welcome: integrability and measurability of order statistics, the permutation-invariance lemma for residuals carried by a sort, and Gaussian regression decompositions; all of these are reusable beyond this mission.
Display advertising on the open web runs through ad exchanges, intermediaries that sell ad impressions on third-party publisher sites to advertisers. A large share of these ads is retargeting: an advertiser shows ads to consumers who recently visited its own website and so revealed purchase intent. Retargeting needs tracking data (a cookie or pixel placed by the exchange on the advertiser's site), and the advertiser decides which exchange receives it. An exchange that held such data could in principle also let a rival advertiser reach those same high-intent consumers, which is called cross-targeting. In practice exchanges do not offer it.
J. P. Johnson, T. Jungbauer and M. Preuss (SSRN 3898798, version of November 2, 2022; published in Management Science, 2024, doi:10.1287/mnsc.2022.03385) explain this with a small game. Advertisers hold the data property rights and can take their data to a rival exchange that never cross-targets, so an exchange may keep cross-targeting closed to secure their data, even where cross-targeting would raise total surplus. This bears on policy debates about third-party tracking, consumer opt-out rights, and category-based tracking schemes such as Google's Topics. This mission formalizes the base model and its main equilibrium characterization, Proposition 1.
There are two advertisers and two exchanges . A unit mass of consumers has shown purchase intent: a mass has visited only 's website, a mass only 's, and both, so each advertiser has visitors. An ad costs . An advertiser earns the monopoly profit from a consumer who sees only its ad and the competition profit from one who sees both, with . Each exchange keeps a fraction of the price of every ad it places. alone can also identify look-alike consumers: of them if one advertiser shares data with it and if both do, and both advertisers can target them.
The game has three stages.
The resulting payoffs include for full cross-targeting (both on an open ), display (2); for leaving to and sniping, display (3); and for leaving without sniping, display (4). The two conditions of the paper are
Equilibrium is subgame-perfect in pure strategies. Assumption 1 removes, within each stage-2 subgame, any equilibrium that is strictly Pareto dominated in the advertisers' payoffs by another equilibrium. then chooses open or closed to maximize its revenue.
In every equilibrium,
in which case both advertisers cross-target. In addition, both advertisers always share data with , retarget their exclusive visitors, and target the look-alike audience of size . The goal also asserts that an equilibrium exists. The "if" direction is stated off the knife edge where one of the two conditions holds with equality (see Formalization scope).
Proposition 1 has two parts. First, always secures both advertisers' data, because only it offers look-alike audiences, which grow with the data it holds. Second, it opens cross-targeting only when neither advertiser would then leave for , and these are two explicit inequalities in the primitives. When they fail, cross-targeting is absent even in cases where advertisers would jointly prefer it, which is the inefficiency the paper studies. The later results of the paper (consumer control over tracking, Proposition 3; Topics-style tracking, Proposition 5) are comparisons against this base equilibrium.
The results are proved in the paper by case analysis. None of them is machine-checked. The mission produces a precise, checkable equilibrium model with stage-3 rationality, a Pareto selection and a leader's choice, together with complete statements of each step. Formalizing it exposed a knife-edge gap in the published argument (below), which the formal statements correct and disclose.
Each payoff comparison is linear arithmetic. The difficulty is equilibrium bookkeeping. Lemma 5's existence argument splits on whether sniping pays, against , and on whether being sniped is preferable to escaping to , and each branch needs a different candidate profile. Lemma 3 must rule out asymmetric equilibria using the rival's optimal stage-3 response after a deviation, so the snipe decision has to be rational off the path. The naive reading, in which full cross-targeting being an equilibrium immediately makes open, fails: the open subgame can have several equilibria, and 's revenue depends on which one Assumption 1 leaves.
All quantities are real numbers in a structure Params. Params.Standing encodes , , , . The bound is a disclosed addition. The paper uses it throughout but does not state it in §1: footnote 3 (p. 5) and p. 21 ("We maintain the assumption that it is profitable to target all customers interested in the product category") rely on it, and without it look-alike consumers have no value. The bound is kept although no statement here uses it.
An advertiser's plan (Plan) is an exchange and a snipe decision. Every other stage-3 action is fixed, since quitting it is strictly unprofitable (pp. 7–8). IsSPE requires the snipe decision to be optimal in its subgame for every rival plan, and no profitable change of exchange; deviations use weak inequalities. ParetoDominates means both advertisers are strictly better off. IsSelected applies Assumption 1 within the subgame. IsEquilibrium combines selected continuations after both stage-1 choices with a revenue-maximizing choice of (weak optimality). Statements about who contracts where are about exchange profiles: snipe decisions of advertisers on do not affect payoffs.
The knife edge. When the binding one of (No Leave) and (No Leave & Snipe) holds with equality, the profile with one advertiser on each exchange is also an equilibrium, with exactly the payoffs of full cross-targeting. The paper's proof of Lemma 3 treats a break-even deviation as profitable. At such points Lemmas 3 and 4 and the "if" half of Proposition 1 fail as printed. They are posed with a disclosed hypothesis NoKnifeEdge (neither condition holds with equality). Everything else, including the "only if" half and the path claims of Proposition 1, is stated without it.
The following would trivialize the mission and are excluded: defining " allows cross-targeting" as the two conditions instead of quantifying over equilibria; not requiring snipe decisions to be optimal off the path; dropping ; and hard-coding the selected continuation.
Contributions are welcome on any milestone. The finite case analyses (16 plan profiles) are good targets for decide-style automation over Bool and Exchange combined with linarith.
In a linear exchange market every agent owns one divisible good and has linear utilities over all goods; an equilibrium is a price vector at which every agent can spend its budget on goods that maximize utility per unit of money, and all goods are sold. Computing such an equilibrium in strongly polynomial time, with a number of arithmetic operations bounded by a polynomial in the number of agents alone, was an open question until Garg and Végh (arXiv:1809.06266; Operations Research, 2023). Their algorithm alternates two kinds of phases. One identifies "revealed" edges that appear in every equilibrium (the subject of mission I of this series). The other computes good starting prices for the current set of revealed edges by solving a linear program whose constraint matrix has a special sign structure.
No strongly polynomial algorithm is known for that linear program. Systems in which every inequality has at most one positive and at most one negative coefficient, by contrast, are strongly polynomially solvable (Megiddo, 1983; Hochbaum and Naor, 1994). The paper bridges the gap with Theorem 6.4: a polyhedron given by a -matrix is sandwiched between a monotone two-variable-per-inequality polyhedron and its scaling by an explicit factor . This mission formalizes that theorem and the lemmas of §7 that prove it. It is a statement about matrices and polyhedra only; no market notions enter.
Matrices are rational. For integers a matrix is a -matrix, written , if every off-diagonal entry is nonpositive and every column sum is nonnegative:
For a non-square matrix the diagonal entries are the with . Square -matrices are exactly the transposes of weighted Laplacians of directed graphs, or such transposes with one row and column deleted.
is the set of rational matrices with at most one positive and at most one negative entry in every row. A system with is a monotone two-variable-per-inequality system (M2VPI).
For and with , the polyhedron of interest is
Write for the number of nonzero entries of , for , and
In §7 the right-hand side is called instead of , and .
The proof works with a square with positive diagonal. Its digraph has an arc whenever . is the set of vertices reachable from (including ), and is the submatrix of the rows , . The vertices split into (at most one outgoing arc), (at least two arcs and ) and (at least two arcs and ).
For with and nonzero entries, and with , there are , and with
Theorem 6.4 turns an LP over a constraint matrix, for which no strongly polynomial algorithm is known, into an M2VPI system that is strongly polynomially solvable, at the price of a factor . In the exchange-market algorithm , so the starting prices of each phase come within a factor of optimal (the proof of Theorem 3.7, p. 15). That bound is what lets the potential argument advance in a polynomial number of phases. The construction is not specific to markets: any LP of the form over with a -matrix, which includes LPs over transposed weighted Laplacians of directed graphs, inherits the same approximation.
The result is proved in the paper; to our knowledge none of it has been machine-checked. A formalization produces a checked proof of the sandwich. It also produces reusable facts about Gaussian elimination on -matrices (Lemma 7.2), which hold for any matrix whose off-diagonal entries are nonpositive and whose column sums are nonnegative.
The obvious approach, deleting all but two variables from each inequality of , fails: the dropped negative terms make the resulting system either too weak or invalid. The paper instead derives one new constraint per arc of , as a nonnegative combination of the inequalities . Finding it requires an ordering of in which every vertex but has an in-neighbour placed after it, and an elimination on the permuted submatrix whose penultimate row has exactly two nonzero entries. The reverse containment is the hard direction. It splits by whether the rows on are linearly independent () or not (), and the case needs the extra constraint and the comparison of entries of the elimination multipliers in Claim 7.5. Every step relies on a sign invariant of the elimination that Lemma 7.2 proves by induction.
Indices are 0-based (Fin k, Fin t); the paper's . Matrices , and right-hand sides , , are rational (ℚ), as on p. 15, and act on real vectors through the cast. A diagonal entry of a rectangular matrix is one whose two indices agree as natural numbers. is the image . is defined for only, and every statement using it assumes (resp. ).
Not formalized: the running time and the polynomial bound on the encoding size of , in Theorem 6.4. The goal is the existence statement that the construction (13) witnesses. The standing assumptions of §7 (; positive diagonal after the reduction) appear as hypotheses of the milestones that live in that setting.
Lemma 7.2 is stated about the specific elimination of the proof (p. 17), defined explicitly; an existential "there is " form would be nearly trivial, since satisfies all but one clause. In the goal, must have at most one positive and at most one negative entry per row, and . Dropping either requirement makes the goal weaker than the paper's theorem.
, defined in (12) through the elimination for an arbitrarily chosen arc, is restated intrinsically as the -th entry of , a number the paper shows equal (proof of Lemma 7.4(iii)). It is used only for , where that block is invertible. Claim 7.3(i)–(ii) and Lemma 7.4(ii), which concern the elimination output for a particular arc, are not milestones.
A complete development needs the elimination and its invariants, reachability in a finite digraph, ranks of row submatrices, and the construction (13). The elimination lemmas are reusable for any -matrix. Contributions are welcome on any milestone, on the reduction from rectangular to the square positive-diagonal case, and on the two containments of the reduced case.
Classical mechanism design assumes that agents optimize exactly: a buyer facing a menu picks the option that maximizes his utility, however small the advantage over the next-best option. In many settings this is implausible. Agents may face cognitive or computational costs, or the designer may only be able to certify incentives approximately, as in algorithmic mechanism design where exact incentive compatibility is replaced by ε-incentive compatibility: no deviation gains more than .
Balseiro, Besbes and Castro (arXiv:2103.03403v2; Operations Research, 2024) ask how much a revenue-maximizing seller can gain when the buyer is only an -optimizer, in the most basic setting: one seller, one item, one buyer. Without the relaxation the answer is classical: by Myerson (1981) and Riley–Zeckhauser (1983) the optimal mechanism is a posted price. The rounding argument usually attributed to Nisan shows that the gain from the relaxation is for every distribution. This mission formalizes the paper's first main theorem, which shows that for regular instances the gain is much smaller and is determined by the local curvature of the revenue curve at the optimal price.
The buyer's value has a density on , with , , off and . Assumption 1 requires in addition that has bounded variation on . Write , , the revenue function (the revenue of a posted price ), and .
A mechanism assigns to every report an allocation probability and a payment . It is individually rational (IR) if for all , and ε-incentive compatible (IC) if
is the set of such mechanisms, the expected revenue, and .
Definition 1 (local α-power envelopes). has a unique maximizer on , and there are , and a neighborhood with
For the uniform distribution on , and .
Under Assumption 1, local -power envelopes at and ,
where allows a factor and the constants depend on the instance but not on .
The paper's argument passes through the following stated results, in attack order:
Theorem 1 is an instance-dependent impossibility result: no -IC mechanism can extract more than beyond the optimal posted price. Since for every , it strictly improves the universal bound for these distributions; for (a revenue curve with nonzero second derivative at ) the rate is . Together with Theorem 3 of the same paper, a matching lower bound by a randomized mechanism, it identifies the exact rate up to the logarithm. The authors conjecture that the logarithmic factor can be removed.
The result is proved in the paper; no machine-checked proof of it or of any of its lemmas exists. A formalization would check an appendix argument of several pages of explicit estimates, and would produce reusable components: a weak duality theorem for a mechanism-design program over a path of incentive constraints, an explicit solution of the functional equation by iterates of , and estimates of iterated piecewise-linear maps.
The obvious approach is to bound the gain by perturbing the optimal posted price, which yields only the rate of the rounding argument. Getting the exponent requires an upper bound that is tight to first order, i.e. a nearly optimal dual certificate for an infinite-dimensional program. The dual depends on the choice of path: the paper's analysis shows that a parallel shift cannot beat , so the path must approach the diagonal near while keeping the number of steps controlled. The estimates for in milestones 7–8 require tracking through iterations of , with a bounded-variation (possibly discontinuous) density. Measure-theoretic details absent from the paper also have to be supplied: changes of variables along a Lipschitz path, almost-everywhere differentiability of iterated compositions, and integrability of the dual variable.
The Lean development lives in namespace ApproxIC.UpperBound. Every function of the value is a total function ℝ → ℝ and every condition quantifies over only. Committed conventions:
sSup of the revenue image, which is nonempty and bounded above by .LocalPowerEnvelope.deriv w.The goal imports only the model file; paths, the dual and eq. (9) appear only in the milestones. A formalization in which 's constants are chosen after , is replaced by a constant, or the revenue integral is allowed to vanish on non-measurable mechanisms is not this theorem and is ruled out by the statement.
A complete development needs interval integrals and the fundamental theorem of calculus for absolutely continuous functions, change of variables along monotone Lipschitz maps, BoundedVariationOn, real powers and logarithms, and iterates Nat.iterate. The duality lemma and the functional-equation solution are reusable for other single-agent screening problems with relaxed incentive constraints. Contributions to any milestone, and alternative proofs of the goal that bypass the path construction, are welcome.
In a proof-of-work cryptocurrency such as Bitcoin, miners spend computing power (hash rate) to win the right to add the next block and collect a reward. Whether this competition stays decentralized depends on how individual hash rates react to differences in mining costs: if a cost advantage translates into an ever larger share of the total hash rate, mining concentrates in a few hands. Capponi, Ólafsson and Alsabah (arXiv:2106.09783v1, 2021) model mining as a game among miners with heterogeneous costs and limited capacity, and derive its equilibrium in closed form. Their Section 4.3 then asks how equilibrium hash rates and hash rate shares respond to a change in one miner's cost. This mission formalizes the answer, Proposition 4.6 of that preprint.
Fix active miners. Miner has cost-per-hash , and every miner bears the capacity cost with capacity parameter (a larger means smaller capacity). The miners compete for a reward , which miner wins in proportion to its hash rate over the aggregate hash rate . Write for the cumulative cost.
When exactly these miners are active, the paper's equilibrium (Proposition 4.1, posed in mission 1 of this series) is explicit. The aggregate hash rate is the positive root of :
and the individual equilibrium hash rates are with
All miners being active means for every . The hash rate share of miner is .
A change in moves in two ways. The direct sensitivity holds the aggregate fixed. The indirect sensitivity acts through the change of the aggregate. For shares, the paper's decomposition on p. 42 gives and .
For active miners , and are differentiable in and , and
The proposition separates the effect of a cost change into a direct part, always negative, and an indirect part through the aggregate, whose sign is set by the hash rate share alone. A miner with less than half the total hash rate partly offsets a cost increase, because rivals' responses lower the aggregate; a dominant miner amplifies it. The same indirect term is exactly the response of to a competitor's cost. For shares the answer is unconditional: a miner's share falls with its own cost and rises with a rival's. These signs (Table 1 of the paper) are what the paper's later discussion of cost advantages and concentration rests on.
The result is proved in the paper by direct calculation. It has not been machine-checked anywhere known to this series, and no comparative statics of a contest or mining game exists on the platform. Formalizing it checks the differentiation of the closed forms, including the case , and fixes the definition of , which the paper uses without defining.
Each step is elementary calculus, but the steps do not close by naive differentiation. The derivative of in , computed from the explicit formula, is a rational function of , and the square root in . Its sign is not visible until the square root is eliminated through and the first-order condition of the miner is used to rewrite . The equivalence (4.5) depends on the activity condition ; without it can be negative and the sign claims fail. The case uses the second branch of , which has no square root, so the paper's middle expression in (B.2) does not apply there.
Miners are indexed by Fin n, 0-based. Costs are a vector c : Fin n → ℝ. The objects cumCost, gH (both branches of (4.1)), fH (with the aggregate as a free argument G), hstar, share and the four sensitivities are defined in PoWMining.CostStatics.Setting. The standing assumptions , , , and for all are bundled in Standing. The last of these is the paper's "for active miners", read at a state where small changes do not alter the set of active miners (pp. 15–16). Costs need not be sorted.
Partial derivatives are one-variable derivatives along Function.update c i, and every derivative claim is a HasDerivAt statement. The sensitivities are defined by deriv, never by their closed forms. A definition would make "" a positivity check and turn the goal into milestone 4; this is ruled out. Sign claims about a deriv-defined quantity are always paired with the corresponding HasDerivAt claim, so a non-differentiable junk value of cannot satisfy them. is allowed throughout.
The sensitivities are derivatives of the closed forms (B.3) of the active miners, as in the paper's proof. That these closed forms are the equilibrium of the game is Proposition 4.1, and the first-order condition behind milestone 5 is Proposition 4.2; both are posed in mission 1 of this series and are not restated here. Printed slip: the middle term of (B.5) has a sign error ( for ); only the outer equality, which the proof uses, is stated.
Proofs need only real arithmetic, Real.sqrt and one-variable derivative rules. Contributions of any milestone are welcome; a lemma computing the derivative of gH along a single cost coordinate is reused by several of them and by the companion mission on capacity and reward.
Classical mechanism design assumes that agents best-respond exactly: a buyer who gains even an infinitesimal amount by misreporting will misreport. In practice agents face cognitive and computational costs, and a buyer may ignore a deviation that gains less than some small amount . A seller facing such a buyer only needs to satisfy the incentive constraints up to , and the natural question is how much revenue this relaxation is worth.
Balseiro, Besbes and Castro (arXiv:2103.03403v2, 2022; Operations Research, 2024) study this question in the simplest setting, one seller and one buyer with a single item. Their answer separates deterministic and randomized mechanisms. This mission formalizes the deterministic half: Theorem 2, which identifies the optimal deterministic -incentive-compatible mechanism and shows that its revenue gain over the classical optimum is exactly linear in .
The buyer's value for the item is drawn from a distribution with a density supported in , , with . Assumption 1 adds that has bounded variation on . Write , , and for the revenue of a posted price .
A direct mechanism assigns to each reported value an allocation probability and a payment . It is individually rational (IR) if for all , and -incentive compatible (IC) if
denotes the feasible mechanisms, and the deterministic ones. The revenue is and . At the optimum is attained by a posted price at any maximizer of on .
The hard/soft floor mechanism , , allocates the item to every report ; a report in pays its own value and a report pays :
Under Assumption 1:
that is, there are with for all .
Theorem 2 settles what deterministic mechanisms can do against an -optimizing buyer: the gain is linear in , no more and no less. The lower half shows that any optimal approximately incentive compatible mechanism gains at least order ; the upper half shows that a seller who wants more must randomize. Together with the paper's Theorems 1 and 3 (other missions of this series), which give the rate for randomized mechanisms under a curvature condition on , it locates the full spectrum of achievable gains between and . The hard/soft floor form is also a practical design: a posted price followed by a pay-your-bid band of width .
The result is proved in the paper's online appendix. To the best of our knowledge it has no machine-checked proof; the classical posted-price optimality has a formalization on Prove2Me under the stronger assumption of a strictly positive density, and this mission needs it for densities that may vanish.
The obvious argument for "an optimal deterministic mechanism is a hard/soft floor" starts from an optimal mechanism, which need not exist a priori, and takes its allocation right-continuous "without loss of generality". Neither step is available for an arbitrary measurable mechanism: the allocation set may have no least element, and changing on a null set can break IC at individual points. The domination milestone is therefore stated for every deterministic mechanism. The revenue identity needs integration by parts for an absolutely continuous whose density may vanish or be discontinuous, and the comparison with needs the classical posted-price optimality without positivity of . The lower bound needs the optimal price to sit strictly inside and to stay bounded away from zero just above it.
Values are reals and every function is a total function ; only its values on matter. Mechanisms are required to be measurable (implicit in ); IR and IC then make bounded on , so revenue integrals are genuine. is a supremum (sSup) of a nonempty set of revenues bounded above by . The goal's is the conjunction of the paper's and (p. 13), with constants depending on the distribution but chosen before , written as "some deterministic mechanism earns at least , every one earns at most "; stays a supremum and is not replaced by . The payment region of is as in the proof (the theorem prints , which double-counts at ). The hard floor ranges over , so the soft floor may exceed .
The domination statement quantifies over all of , not over monotone or right-continuous mechanisms, and the constants may not depend on ; either restriction would trivialize the result.
The development needs interval integrals, integration by parts for absolutely continuous functions, and continuity of . The posted-price optimality milestone is reusable for every single-buyer revenue question and is welcome as a stand-alone contribution.
Many proof-of-stake blockchains do not let every participant produce blocks. Instead, token holders elect a small committee of block producers, and the committee runs a Byzantine agreement protocol among itself. EOS, for example, elects 21 producers by approval voting: each token holder approves a set of candidates, and the 21 candidates with the most approvals form the committee. Byzantine agreement protocols are safe only while a large enough fraction of the committee is honest, typically more than two thirds, so the security of the whole chain rests on a question of social choice: does approval voting, with voters who see only noisy information about the candidates, elect a committee with enough honest members?
Benhaim, Falk and Tsoukalas (arXiv:2110.08673v2, Management Science 2023) model this election and analyse it. Their main result, Theorem 3, shows that whatever strategies the voters use, as long as the honest candidates are approved with probability at least a fixed margin above the dishonest ones, the probability of electing an honest committee converges to one exponentially fast in the number of voters. This mission formalizes that result.
There are voters and candidates (block producers), and a committee of size is to be elected. Each voter submits an approval ballot , a subset of the candidates. The score of candidate is the number of voters approving it,
The elected committee consists of candidates with the highest scores. When several candidates tie at the lowest elected score, or when fewer than candidates have a non-zero score, the paper resolves the choice adversarially. Formally, a set of candidates is an admissible committee if and for every and .
Each candidate is honest or dishonest. Let denote the set of dishonest candidates. For a tolerance (for instance ), the committee is honest, written , if it has at least honest members. Because ties and filling are adversarial, means that every admissible committee has at least members outside .
The ballots are random: they are drawn on a probability space, independently across voters, while the approvals inside a single ballot may depend on each other in any way. The vote probability is the probability that voter approves candidate . The candidates' types are fixed throughout, and all randomness is in the ballots.
Suppose there are a set of honest candidates with and a with . Then
The theorem is the paper's answer to its title question. Its bound holds for every voting behaviour, including the threshold and cardinal strategies the paper studies and strategies with arbitrary correlation inside a ballot. So the security guarantee does not depend on voters coordinating or on knowing the signal model. All it needs is that signals are informative by a margin . The bound also shows the trade-off quantitatively: the failure probability grows quadratically in the number of candidates and decays exponentially in the number of voters . This is the basis of the paper's Corollaries 1 and 2 on the threshold and cardinal strategies.
The paper proves the result on paper (Appendix B.2, p. 48), using a Chernoff–Hoeffding bound it cites from Dubhashi and Panconesi. As far as the platform's index shows, no machine-checked version of the result or of its committee model exists. The mission contributes the first formal model of -winner approval voting with adversarial tie-breaking on Prove2Me, a formal statement of the Poisson-binomial law of approval counts, and the one-sided Hoeffding bound for sums of independent Bernoulli variables in the form. The formalization also records three places where the printed text needs correcting (see Formalization scope).
There are two difficulties. The first is the committee predicate. Ties and under-filled committees are resolved by an adversary, so is a statement about every admissible committee, not about one top- list. The reduction from honesty to the score-separation event has to handle both the case where all of is elected and the case where some member of is left out, so that every elected candidate outscores it.
The second is the concentration step. The vote counts of different candidates are not independent, because each voter's ballot ties the approvals together, so no argument that treats the counts as independent variables applies. The paper's own step from the gap to (82), the split (80)/(81), uses strict inequalities and is false when the two thresholds coincide at an attained integer value; the printed Hoeffding bound (Theorem 6) is strict as well, so the printed chain does not close as written at that boundary.
Fin n and candidates Fin m, both 0-based. A random ballot is a measurable map Ω → (Fin m → Bool) on a probability space (Ω, P). The ballots are mutually independent (iIndepFun), and each voter's ballot law is otherwise arbitrary. This generalises the paper's Gaussian signal model and its strategy classes, which are not formalized, and the paper's per-type probabilities become per-candidate . The cap of Definition 2 is not imposed. The printed statements are special cases.Measure.real, sub-Gaussian concentration for bounded independent variables, and Finset.powersetCard. The committee definitions and the Poisson-binomial law can be reused by later missions on voting and on the companion single-voter result. Proofs of any milestone are welcome, and so are alternative routes to the goal.Classical mechanism design assumes that agents are perfect optimizers: a mechanism is incentive compatible if no buyer gains anything, however small, by misreporting. In practice buyers face cognitive and computational costs, and a buyer may not bother to deviate for a gain below some threshold . Balseiro, Besbes and Castro, Mechanism Design under Approximate Incentive Compatibility (arXiv:2103.03403v2, 2022; Operations Research, 2024), ask how much additional revenue a seller can extract when the incentive constraints only need to hold up to .
A known benchmark answers this at order . It comes from a rounding argument attributed to Noam Nisan, used in mechanism design to transform an approximately incentive compatible mechanism into an exactly incentive compatible one (see e.g. Balcan, Blum, Hartline and Mansour, FOCS 2005). The paper states this benchmark as its Proposition 1 and proves it in its online appendix "for completeness". This mission formalizes that benchmark; the paper's sharper, instance-dependent rates are the subject of the other missions of this series.
A seller sells a single item to one buyer. The buyer's value is drawn from a distribution with a density supported in , , with .
A direct mechanism assigns to each reported value an allocation probability and a payment (payments may be negative). Given , the mechanism is
denotes the set of mechanisms satisfying IR and IC (problem of the paper). For this is the classical feasible set, and . The revenue of is , and the optimal revenue under -IC is
The quantity of interest is the revenue gain .
In the Lean development the model is ApproxIC.Rounding.Model (fields vbar, f) with the predicate Model.Standing; mechanisms are Mech (fields x, t); the sets and values are Mset M ε, revenue M m and optRev M ε.
in the paper's notation (p. 13): there are and , which may depend on the distribution, such that for every and every ,
Fix and , and let .
The result. Proposition 1 gives a distribution-free shape for the value of relaxing incentive compatibility: an -optimizing buyer can be exploited for at most order extra revenue. It is the starting point against which the paper measures its main contributions: an instance-dependent upper bound of order (Theorem 1) and a matching lower bound (Theorem 3) for distributions whose revenue curve has local -power envelopes around the optimal price, and the rate for deterministic mechanisms (Theorem 2). Since for every , these show that the benchmark is not tight for such distributions. The rounding step itself (milestone 1) is the standard device for converting approximately incentive compatible mechanisms into exactly incentive compatible ones, and is reused across mechanism design.
Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a formal single-buyer model with -IC mechanisms that the other missions of the series share, and a formal version of Nisan's rounding argument for a continuum of types.
The paper's proof is short, but it is written for an argmax that is attained and a rounded mechanism that is tacitly measurable. In a formal treatment, the selection must be chosen so that is measurable and its expected payment is defined. Exact incentive compatibility forces to be nondecreasing on , and that monotonicity has to be established and then turned into measurability. The revenue comparison needs the integrability of , which comes from IR and IC bounding on , not from an assumption. The milestone-3 bound carries no attainment hypothesis, so a proof must also handle the case in which the maximum over is not attained. Finally, is a supremum, and its nonnegativity (used in ) and its finiteness must be derived from the feasible set.
sSup) of the revenue image of , which is nonempty (the zero mechanism) and bounded above by ; the goal and milestone 3 are stated for every , which is equivalent to the bound on the supremum. is never replaced by the posted-price revenue.Real.sqrt ε. The constants and are quantified after the distribution and before ; quantifying them after would make the goal trivial.vs with values in attaining the maximum, as the page assumes. The rounded mechanism is set to off ; its measurability is part of the conclusion, not a hypothesis.Needed infrastructure: monotone functions are measurable, interval integrals of bounded measurable functions against an integrable density, and suprema of bounded real sets, all in Mathlib. Contributions of the rounding lemma in reusable form (for general type sets) are welcome.
Centralized markets such as kidney exchanges, ride-sharing platforms and online labor markets match agents who arrive over time. Kerimov, Ashlagi and Gurvich (SSRN 3824407; Management Science, 2023, doi:10.1287/mnsc.2021.01215) study such a market with agent types and feasible multi-way matches. Their main result is that, when a fluid linear program called the static-planning problem (SPP) has a unique non-degenerate solution, a periodic resolving policy keeps the regret against the hindsight optimum bounded by a constant of order at all times, where the general position gap is the smallest positive basic variable of (SPP).
The constant is only informative if one can say what is. Section 5 of the paper does this for a class of networks it calls (SPP)-acyclic: there the optimal solution of (SPP) is an explicit signed sum of arrival rates, so is an imbalance between sums of arrival probabilities. This mission formalizes that structural result and the lemmas it rests on. It needs no probability: only the combinatorics of the network and linear programming.
A matching network has agent types and matches . Match uses one agent of each type in a set with , every type belongs to some match, and the matching matrix has iff . Arrival probabilities satisfy , , and match values satisfy .
The matching network graph is the bipartite graph whose vertices are the types and the matches, with an edge between type and match iff .
For a right-hand side , the static-planning problem is
and (SPP) is the case . For a solution write (active matches), (redundant matches), and .
The network satisfies the general position condition (GP) if (SPP) has a unique optimal solution and it is non-degenerate: . The optimal basis matrix is formed by the columns of indexed by and the unit vectors , .
The (SPP)-residual graph is with the redundant matches removed, and the network is (SPP)-acyclic if it satisfies GP and its (SPP)-residual graph has no cycle.
Assume GP and (SPP)-acyclicity. Then there are vectors , , with
and every right-hand side with for all has, as its unique optimal solution, on , on , and zero elsewhere.
A further theorem item, Lemma 5.1 (p. 24), states that under GP a network with only two-way matches, in which every cycle contains an even number of matches, is (SPP)-acyclic.
Theorem 5.1 turns the regret constant of the paper's main theorem into a quantity one can read off the data: every positive basic variable, and therefore , is with coefficients in . Its second sentence describes the whole region of right-hand sides on which the same basis stays optimal, an open polyhedral cone cut out by the inequalities , which is how the paper relates GP to the arrival rates in §5.1.
On the formal side, the mission builds a reusable model of the matching network, its bipartite incidence graph and the static-planning linear program with a variable right-hand side. Prove2Me does not yet contain the structural theory of optimal bases of such programs. Theorem 5.1 and its milestones are proved in the paper (Appendix C and §4.2); none of them is machine-checked yet.
The representation holds for every network in general position, so the content of the theorem lies in two places.
Types are Fin n, matches Fin d, both 0-based. The topology is the structure MatchingNetwork with the fields and "every type is in a match"; and are separate vectors with the standing predicates , and , which are hypotheses of every theorem. The optimal solution is an argument together with the GP hypothesis, never a default or a choice. The graph is a SimpleGraph on Fin n ⊕ Fin d; the residual graph keeps redundant matches as isolated vertices, which affects neither acyclicity nor the degrees of type vertices. The column index type of is , and the inverse is a two-sided inverse over these index types, not Matrix.inv, which is on singular matrices.
Conventions the statements commit to:
The paper's own text says "all entries of are either , , or " (p. 25); this is read as , or , as in the theorem's statement.
A formalization that keeps only the first sentence of Theorem 5.1, or that lets the vectors be unrelated to the basis, is trivially satisfiable and is not the theorem.
Needed infrastructure: optimality conditions for linear programs in equality form (reduced costs, uniqueness of a non-degenerate optimum), Mathlib's acyclic graphs and trees (SimpleGraph.IsAcyclic, IsTree.card_edgeFinset), and degree counting on bipartite graphs. The paper proves Theorem 5.1 in Appendix C by an explicit construction along paths of the residual graph; any correct argument is welcome. Lemmas on the inverse of a basis matrix whose bipartite row–column graph is a forest would be reusable well beyond this mission.
Many problems in optimization reduce to a subgradient inclusion : for a smooth this is the gradient equation , and for an extended-real-valued (a smooth loss plus an indicator or a nonsmooth regularizer) it is the first-order optimality condition of a composite problem. Newton's method is the classical way to solve such equations with a superlinear rate, but its textbook form needs and a nonsingular Hessian. Khanh, Mordukhovich and Phat (arXiv:2009.10551v2, 2022; Mathematics of Operations Research, 2023) design a Newton-type method in which the Hessian is replaced by Mordukhovich's second-order subdifferential , and prove local superlinear convergence under two assumptions that are weaker than the usual ones: metric regularity (instead of strong metric regularity or tilt stability) and the semismooth* property of Gfrerer and Outrata.
Timeline of the ingredients:
Let be proper. Its limiting subdifferential collects the limits of Fréchet subgradients at points with . For a set , the regular normal cone contains the vectors with for ; the limiting normal cone contains the limits of regular normals at nearby points. For a set-valued , the coderivative is , and the second-order subdifferential is .
The function is prox-regular at for with modulus if it is l.s.c. around and, for some , whenever lie within of , and lies within of . It is continuously prox-regular if, in addition, along every with . It is prox-bounded if it is bounded below by a quadratic function.
For , the Moreau envelope and proximal mapping are
Algorithm 6.2 starts at . While it sets , picks any with , and moves to .
The standing assumptions at a solution are:
If is proper, prox-bounded, continuously prox-regular at for with constants , and (H1)–(H3) hold, then
The result gives a Newton method for nonsmooth, nonconvex subgradient inclusions whose convergence does not require strong metric regularity. Example 5.2 of the paper exhibits a function whose gradient is metrically regular and semismooth* but not strongly metrically regular, so the theorem covers solutions that earlier generalized Newton theories exclude. Through the Moreau envelope, the method reduces to a gradient equation; the same reduction, with the forward–backward envelope, drives the paper's composite algorithm (the companion mission) and its applications to Lasso-type problems.
The paper's results are proved on paper; none of them, nor the underlying theory of coderivatives, second-order subdifferentials or semismooth* maps, is formalized in Mathlib. This mission produces a machine-checked development of that layer and of the convergence theorem. It also fixes a defect: as printed, Lemma 6.3 and Theorem 6.6 claim their conclusions for every , which is false (see Formalization scope); the formal statements are the corrected ones.
The obvious argument says "Algorithm 6.2 is Algorithm 5.3 for , so apply Theorem 5.7". Each step of that sentence carries the difficulty. Transferring (H1)–(H3) from to requires the coderivative of the inverse , which needs a local graphical calculus for limiting normals that Mathlib does not have. The property of the envelope and single-valuedness of the proximal map hold only for small and near : prox-regularity is local while minimizes globally, so a far-away deep well can capture the proximal point. Theorem 5.7 itself rests on a uniform coderivative bound from metric regularity (Lemma 5.4, a pointwise-to-uniform form of the Mordukhovich coderivative criterion) and on the semismooth* estimate (Lemma 5.5), which combines directional normal cones with the symmetry of generalized Hessians.
EuclideanSpace ℝ (Fin n); definitions are stated on real inner product spaces, and carries the sup norm (the cones are norm-independent).NonconvexSplitting.Shared.LimitingSubdiff. It agrees with the paper's geometric (2.9) for functions l.s.c. around the point, which covers every function is applied to here.EReal and is assumed proper; the envelope is EReal-valued, and finiteness is asserted wherever it is differentiated.Classical.choose; and is not specialized (no convexity, which would make ; no ; no strong metric regularity; no assumption that is a minimizer).Rank-order competitions — sports tournaments, poker final tables, golf tours, crowdsourcing contests, sales leagues — end with a ranking of the participants and a pot of prize money that has to be split according to that ranking. Organisers publish prize tables that change with the number of entrants and with the size of the purse, and these tables are usually justified only by tradition. Dietzenbacher and Kondratev (arXiv:2008.08985v2, published in Management Science 2023, doi:10.1287/mnsc.2022.4520) take the axiomatic approach of fair-division theory and ask which prize allocation rules are characterised by natural requirements of fairness and coherence across competitions of different sizes.
Consistency — invariance of a rule under "re-running the allocation" for a subgroup with the money it collectively received — has a long history in axiomatic allocation: bankruptcy problems (Aumann and Maschler 1985), taxation (Young 1987), bargaining (Lensberg 1987, 1988) and cooperative games (Peleg 1986; Hart and Mas-Colell 1989). The paper applies it to competitions. Full consistency together with order preservation and endowment monotonicity yields the interval rules (Theorem 1); weakening consistency to local consistency yields the single-parametric rules (Theorem 2). This mission concerns the weakest version, top consistency, which only constrains the top segment of the ranking and describes real prize schemes such as the golf tournament of Table 1(b) of the paper. It is the third mission of a series on this paper; the first two treat Theorems 1 and 2.
Fix a countable set of at least three potential competitors. A competition consists of a finite nonempty set , a ranking (a bijection; competitor is ranked above when ), and a prize endowment . For the subranking orders as does.
A prize allocation rule assigns to each competition a vector with . The axioms are:
A rule is parametric if there are continuous non-decreasing with and such that , where solves . The winner gets and position gets . Equal Division () and Winner-Takes-All ( for ) are parametric.
Both directions are part of the goal.
Lemma 1 of the paper (endowment monotonicity implies endowment continuity, p. 10) is used in the proof; it is formalized in the first mission of this series and will be referenced from there.
Replacing winner strict endowment monotonicity by endowment additivity (equivalently scale invariance) characterises the proportional rules with and .
Theorem 3 says that the four axioms leave exactly one degree of freedom per position: a monotone function of the winner's prize. This gives organisers a complete menu of prize schemes that are fair in the anonymous, order-preserving sense and that keep the top of the table unchanged when lower-ranked entrants leave — the property that matters when competitors are eliminated one at a time and paid at the moment of elimination. It contains the single-parametric rules of Theorem 2, the Winner-Takes-Surplus rules, the geometric rules and the proportional rules (Corollary 8) as special cases, and the paper shows in a Remark (p. 33) that the four axioms are logically independent.
The theorem is proved in the paper; to our knowledge no part of it has been machine-checked. The formalization adds a reusable layer for variable-population allocation problems — rankings of finite subsets of a fixed universe, subrankings, and consistency axioms restricted to families of subsets — that is not in Mathlib. Formal proofs of both directions, of the milestones, and of Corollary 8 are all welcome.
The "if" direction is a computation, but it requires showing that the parameter is well defined and moves monotonically with , which uses and the intermediate value theorem. The "only if" direction must construct the functions from an abstract rule. The natural first idea — define as the prize of position when the winner receives — needs the winner's prize to be invertible as a function of , which uses continuity (supplied by Lemma 1, not assumed), strict monotonicity only for the winner, and unboundedness, which comes from order preservation together with exhaustion of the endowment. Top consistency then has to transfer the representation from competitions of size to size , and anonymity has to transfer it from one ranked set to every other one of the same size; the induction over the number of competitors must keep all smaller sizes, since top consistency reduces to every top segment.
List U, best competitor first; is the 1-based index pos l i, and is the sublist of entries in . is an arbitrary type with decidable equality; the paper's standing assumptions (countable, at least three elements) are hypotheses of the goal and of Corollary 8, and are omitted from milestones that do not use them.φ : List U → ℝ → U → ℝ; it is required to be a prize allocation rule (nonnegative prizes summing to ) on rankings and , and every axiom quantifies only over that domain. Endowments are reals with .f : ℕ → ℝ → ℝ, indexed from 1 as on the page ( unused); continuity, monotonicity, nonnegativity and are required on . The parameter is given existentially; it is unique, so this is the page's "where is such that".Trivializing formalizations are ruled out: rules act on every finite ranked subset of , not on a fixed competitor set; top consistency quantifies over exactly the top segments (full or local consistency would change the theorem — the rule of Example 6 is parametric but not locally consistent); the goal is a biconditional; the parametric family includes , the decreasing chain , and continuity of every .
Corollary 7 of the paper is not included: its "only if" parts ("for each ") fail as written when is finite, since for is not determined by the rule.
Quantum state tomography reconstructs an unknown -dimensional quantum state from measurements on many copies of it. For qubits, , so the number of copies a tomography procedure needs grows exponentially in , and lower bounds on that number decide how far experiments can scale. In many experiments the only measurements available are Pauli measurements: each qubit is measured in the eigenbasis of one of .
Flammia and Liu, Direct fidelity estimation from few Pauli measurements (arXiv:1104.4695, Phys. Rev. Lett. 106, 230501, 2011), show that the fidelity of an experimental state with a target pure state can be estimated with far fewer copies than full tomography needs. To make the comparison meaningful they also prove that full tomography of a pure state with Pauli measurements requires copies. That lower bound has two steps. The first builds a large family of nearly orthogonal pure states whose Pauli expectation values are all small, so that Pauli measurements extract little information about which state is present. Its engine is Lemma 1 of the paper (p. 7), the subject of this mission. The second step, an information-theoretic argument over a noisy classical channel, is not in scope.
Fix qubits and put . States are unit vectors , ; the overlap is conjugate-linear in .
The single-qubit Pauli matrices are , , , . A Pauli label determines the -qubit Pauli operator (with ). There are labels; the all-zero label gives . Every is Hermitian and unitary, so the Pauli expectation is a real number in .
A Haar-random state is a vector drawn from the uniform (rotation-invariant) probability measure on the unit sphere of , a real sphere of dimension . The constants of the lemma are
with the natural logarithm and a parameter.
Let be states with . Then there is a state with
These are (31) and (32) of the paper. The goal is an existence statement with no measure in it.
Every constant is the paper's; none is replaced by an unspecified absolute constant.
The result. Lemma 1 is a packing statement: applied repeatedly, it yields states that are pairwise almost orthogonal and whose non-identity Pauli expectations are all . Such states are hard to tell apart with Pauli measurements, since each measurement outcome is nearly unbiased. The paper converts this into the copy lower bound for full tomography with Pauli measurements (pp. 3, 7–8). Since direct fidelity estimation of an arbitrary pure state uses copies (for fixed accuracy and failure probability), the lower bound is what shows that the scheme beats tomography followed by a fidelity computation by a factor of about .
Formalizing it. The lemma and its proof are published, but none of it is machine-checked: Mathlib has no Pauli operators, no concentration of measure on spheres with explicit constants, and no Levy lemma. A formal proof needs a concentration inequality on the complex unit sphere with the explicit constant (or any sharper one), the vanishing of the means by symmetry, and the union bounds. Each milestone is a reusable fact about Haar-random states.
The two union bounds (35) and (38) and the Lipschitz estimates (33) and (36) are elementary. The central difficulty is the tail bounds (34) and (37). The paper obtains them from Levy's lemma, which it cites (P. Lévy, 1951) and does not prove; Levy's lemma rests on the isoperimetric inequality on the sphere, which Mathlib does not have, and (37) concerns a quadratic form of rather than a linear one. Both tail bounds also need a working theory of the uniform measure on the complex unit sphere (rotation invariance, the distribution of a coordinate), little of which exists in Lean today.
A second difficulty is that the printed proof does not cover every parameter. The union bound produces a good only when . For small , or small with few given states, the goal is still true, but a complete proof must handle those cases separately; they are not in the paper.
Q n = Fin n → Fin 2, Pauli labels P n = Fin n → Fin 4, states live in EuclideanSpace ℂ (Q n), and is the entrywise product of single-qubit Pauli matrices (the Kronecker product). is the real number ; is Real.log; ⟨φ|ψ⟩ is Mathlib's inner ℂ φ ψ.Measure.toSphere of an additive Haar measure on (as a real vector space), normalised to total mass one. The paper's "Haar-random vector in " is read as this measure on the unit sphere of .The Quantum Approximate Optimization Algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028, 2014) is a family of shallow quantum circuits for combinatorial optimization, indexed by a depth and real angles. It has become one of the standard candidate algorithms for near-term quantum hardware, and its MaxCut instance is the usual benchmark on which it is analysed.
The algorithm is run by preparing a quantum state, measuring it in the computational basis to obtain a bit string , and evaluating the classical objective . Its analysis in the paper bounds the mean of . A mean alone does not say what a single run returns. Section III of the paper supplies the missing piece for MaxCut on bounded-degree graphs: the variance of grows at most linearly in the number of edges, so the measured cut values are concentrated around and a modest number of repetitions reproduces the mean. This mission formalizes that variance bound, equation (30) of the paper, together with the locality and counting facts it rests on.
Let be a simple graph on vertices with edge set of size , each edge listed once. Vertices are qubits; a computational basis state is a bit string .
In Lean these are edgeCut, cutValue, qaoaState, expectCut and edgeTerm in the shared FarhiQAOA.Cubic setting, and edgePairs, cutVariance, edgePairTerm, edgeCov and lightCone in FarhiQAOA.Concentration, all built on the published QAlgorithms definitions of qubit registers, measurement probabilities, the uniform superposition, the problem Hamiltonian and the QAOA unitary.
For a -regular graph with , every depth and all real angles,
The constant is the paper's, as printed.
Companions, printed in the paper for : and at most meeting edges.
The result. For fixed and the bound makes the standard deviation of the cut value , while the mean is of order . The algorithm's output is therefore concentrated: a single measurement already returns a cut close to in relative terms, and the paper uses this to argue that the sample mean of polynomially many runs estimates within . The same locality structure, that each edge term depends only on a bounded neighbourhood, is what makes classically computable for fixed and underlies later analyses of QAOA on bounded-degree and random regular graphs.
Formalizing it. The bound is proved in the paper in a few lines; none of it is machine-checked. A formal proof has to make the paper's operator locality argument precise (the conjugated clause operator is supported on the light cone, and the initial state is a product state), connect it to the computational-basis probabilities, and carry out the graph counting with explicit constants. The resulting locality lemma for QAOA circuits on graphs is reusable for any statement about QAOA at fixed depth.
The algebra of (28) and the bound by are routine. The substance is in two places.
The vanishing of a covariance requires showing that , for the full depth- QAOA unitary , acts only on the qubits of , and that for two operators acting on disjoint sets of qubits the expectation in the product state factorizes. Both are statements about operators on , whereas the objects in the statement are probabilities of computational basis states; the formal proof must pass between the two. Matrix exponentials of commuting sums have to be split into commuting factors, which in Lean means working with NormedSpace.exp on matrices indexed by bit strings.
The counting (26) and (29) is a ball-growth bound in a graph of bounded degree. The paper's count, via (26) with replaced by , bounds vertices, while (29) counts edges; the passage between the two, and the extended graph distance on disconnected graphs, must be made exact with the printed constant.
Fin n, bit strings are Fin n → Bool with true the bit , and states live in EuclideanSpace ℂ (Fin n → Bool).SimpleGraph.edist ( between components).A variance defined with two different states, or a probability vector that is not normalised, would make the goal vacuous or false; the definitions use the single state throughout.
Out of scope: the standard-deviation reading and the sampling claim after (30), which carry no explicit constant; the measurement-and-repetition procedure, running time, circuit depth and the classical search for the angles.
Welcome contributions: a general light-cone lemma for conjugation by products of exponentials of local Hamiltonians on qubits; factorization of product-state expectations over disjoint qubit sets; ball-size bounds in graphs of bounded degree.
Firms that outsource work to an agent whose effort they cannot observe often punish poor performance by suspending the relationship for a while, even though restarting costs money: a new set-up, re-training, re-mobilisation. Cao, Sun and Tian (Management Science, 2024) study this trade-off in a continuous-time principal–agent model with Poisson arrivals and a fixed switching cost paid every time work (re)starts. They characterise the optimal dynamic contract in three regimes: never hire the agent, hire and keep the agent working forever, or a control-band contract with suspension episodes of fixed length. The model extends the Poisson-arrival contracting framework of Sun and Tian (2018) by adding the switching cost.
The proof follows a guess-and-verify pattern. A stochastic verification theorem (Theorem 1 of the paper) turns any pair of functions satisfying a system of quasi-variational inequalities into an upper bound on the principal's value. Propositions 2–7 then supply such a pair in each parameter region. This mission covers one region: the agent is much more impatient than the principal (Condition 2) and the switching cost is high.
A principal earns revenue per arrival of a Poisson process. Without the agent's effort the arrival rate is ; with effort it is , and effort costs the agent per unit of time. While the agent works, the principal's total cost rate is . Each time work starts or restarts, the principal pays a switching cost . The principal discounts at rate and the agent at rate , with . Write . Assumption 1 is .
The derived constants are
The variable is the agent's promised utility. The revenue threshold is
Condition 2 is: and .
For a function on with left derivative , the working-state operator and the suspension-state operator are
The first is a delay-differential operator: it evaluates at . A pair satisfies the optimality condition (20)–(22) if
Under Condition 2, let be the line from at to at , and let be constant beyond (display (31)). Then
where in the second case is the line from to on , constant beyond (display (32)).
Through the paper's verification theorem, Proposition 4 yields the "not hiring" half of the main Theorem 2 in the Condition 2 regime. If , the principal's value is at most , so it is optimal never to engage the agent (Theorem 3). The threshold is the switching cost above which the value of hiring, net of the set-up cost and of the agent's promised rent, falls below the outside value. Together with the companion missions of this series (Condition 1 with high cost, Condition 2 with medium cost, and the low-cost control-band regime), this result completes the partition of the parameter space behind Theorem 2.
The result is proved in the paper and has no machine-checked proof yet. This mission states the analytic certificate of the guess-and-verify argument, not the contract-optimality theorem. The contribution it asks for is a formal proof that these explicit functions satisfy the quasi-variational inequalities, including the left-derivative behaviour at the kink and the algebra that links Condition 2 to the sign of .
The functions are piecewise linear, so the difficulty is not analytic depth but bookkeeping that is easy to get wrong:
The naive check, that vanishes or is positive because is "close to" a solution of the delay equation, does not work: is not a solution of (25), and the inequality is strict in general.
All parameters are real numbers in one structure Params. Its predicate Standing collects the paper's standing assumptions: , , , and . Two of these are added to the page and disclosed: , since it is an arrival rate, and , since (31)–(32) divide by .
Functions are ℝ → ℝ, and every condition is quantified over only. The derivative in and is the left derivative derivWithin f (Set.Iic w) w, as the paper prescribes on p. 15. Inequality (20) is required for : on the left derivative at does not exist. Inequalities (21) and (22) are required exactly as printed. "Satisfy the optimality condition (20)–(22)" means exactly these three conditions; the paper's Theorem 1 additionally asks for monotonicity and concavity, but Proposition 4 does not claim them and they are not added.
The threshold is the printed formula. Its denominator is positive under Condition 2, so Lean's convention never applies there.
None of the conditions is weakened: (21) keeps both bounds, (22) is kept, and the operators are not pre-simplified with the closed form of . A formal proof therefore has to carry out the sign computation itself. The stochastic contract model (Poisson point processes, promise keeping, incentive compatibility), the verification Theorem 1 and the optimality Theorems 2–3 are not formalized.
Two hat symbols elsewhere in the paper are distinct objects from those used here: of Lemma 3 and the bold of Proposition 6. Neither appears in this mission. Proofs of the milestones, and proofs of the goal that use them, are welcome.