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?
Since 2017, billions of dollars have been raised through the issuance of crypto-assets, many of them tokens: digital claims on a future product or service, issued before the product exists. Malinova and Park, Tokenomics: When Tokens Beat Equity (SSRN 3286825; Management Science, 2023, doi:10.1287/mnsc.2023.4882), ask when such a pre-sale is a better way to finance a venture than the two classical instruments, equity and debt. To answer, they first work out how equity and debt perform in a simple monopoly model in which demand is uncertain when the money is raised. This mission formalizes the debt half of that benchmark (Proposition 2), together with the equity half (Proposition 1). The other three missions of the series treat the optimal token contract (Proposition 3), its comparative statics (Proposition 4) and financing under moral hazard (Proposition 8); all of them compare against the benchmark proved here.
An entrepreneur must pay a set-up cost before she learns demand. Afterwards she is a monopolist with constant marginal cost , facing the linear inverse demand
where the demand intercept is uniformly distributed on , with . Investors require a zero expected return. For a payoff of the demand realization write
At demand the monopolist produces and earns the monopoly profit
that is if and otherwise. The project's net present value is .
Under equity, investors receive a fraction of profits; break-even is (5). Under debt with promised repayment , investors receive : the full when the venture is solvent (), the whole monopoly profit under the debtor-in-possession arrangement when , and nothing when . The entrepreneur keeps . The repayment breaks even when
In Lean these are expect, pim, npv, equityShare, debtInv and debtEnt in the namespace TokenFinance.Debt.
If , then
and every such satisfies
Uniqueness is asserted among all nonnegative repayments, which implies the paper's uniqueness in .
Propositions 1 and 2 establish that, absent agency problems, equity and debt finance exactly the positive-NPV projects and leave the entrepreneur the entire surplus. This is the benchmark of the paper: Proposition 3 shows that a carefully designed token pre-sale matches it, while naive token contracts (revenue sharing, plain output pre-sales) distort output and fail to finance some profitable projects. Corollary 1 of the paper is the conjunction of Propositions 1–3. The debt repayment characterized here also reappears in the moral-hazard analysis (§IV), where the ranking of debt, tokens and equity depends on the size of relative to the low-demand state.
On the formal side, the results are proved in the paper with short calculus arguments, and nothing about them is machine-checked. The mission produces a checked model of uniform-demand monopoly financing in which expectations are genuine integrals of realized payoffs, the cubic reduction of the break-even condition, and the uniqueness argument for the repayment. These are the pieces the token missions of the series build on.
The central step is the passage from (7) to the cubic (33). The investors' payoff changes form at and at the solvency threshold , so the expectation must be split at points that depend on and may fall outside for large ; only for does the threshold stay inside the demand range. Uniqueness over all also needs the regime , where the investors receive the whole profit and the break-even condition reduces to . A naive argument that solves the cubic in and stops gives uniqueness only inside .
All objects are plain functions of real parameters; there is no probability space. Demand enters only through , the expectation under (open or closed endpoints make no difference). Case distinctions of the paper are encoded with and , so the break-even condition (7) is a single integral of the realized repayment rather than the paper's split integral with limits; the split form is a theorem (milestones 2 and 5). The standing assumptions are and ; is the paper's "positive marginal cost" (p. 22) and is kept throughout the series although Proposition 2 itself needs only . "All positive NPV projects" is the hypothesis on the integral-defined NPV.
A trivializing formalization is ruled out: the NPV, the investors' break-even condition and the entrepreneur's payoff are expectations of realized payoffs, never their closed forms, so neither (3) nor the reduction to (33) is true by definition.
The definitions file also declares the token objects of Proposition 3 (the revenue share , the realized token payoffs and condition (16)), identical across the four missions of this series so that they can be merged later; they are not used here. Out of scope: the secondary token market, bankruptcy costs, consumer welfare and the institutional discussion of the paper. Useful infrastructure includes lemmas for integrals of piecewise polynomials on intervals and a reusable "strictly increasing continuous function with a sign change has a unique root" argument.
Grocery chains and restaurants that promise delivery within an hour or less must decide, at each dispatch epoch, which drivers to send out and along which routes. Liu and Luo (arXiv:2107.13058v3; Manufacturing & Service Operations Management, 2023) model this as a finite-horizon dynamic program and solve its per-period approximation with a logic-based Benders decomposition: a master problem chooses how many drivers to commit to future periods, and a routing subproblem then picks the routes that serve the current orders.
The routing subproblem is a set-partitioning integer program over an exponentially large route set. The paper solves it with a route enumeration algorithm, which generates only the routes that can still appear in an optimal solution. The pruning rule that makes this work is Lemma 2 (p. 19): a route whose LP reduced cost exceeds the gap between an upper bound and the LP bound cannot appear in any optimal solution. Rules of this kind, reduced-cost fixing for set-partitioning formulations, are a standard component of exact vehicle-routing algorithms (see, e.g., Baldacci, Christofides, Mingozzi 2008). This mission formalizes Lemma 2 for the paper's own subproblem.
Fix a period and a solution of the master problem. The data are:
Write , the number of drivers the master solution allows to remain occupied in period .
The routing subproblem SF1 (pp. 16–17) is
Its LP relaxation RF1 replaces by and the partitioning rows by covering rows ; denotes its optimal cost. The dual variables are for the occupancy rows, for the fleet row and for the covering rows. The reduced cost of a route with respect to a dual solution is
An upper bound of SF1 is a number at least as large as the optimal cost of SF1.
Let be an upper bound of SF1, the optimal cost of RF1, a dual optimal solution of RF1, and . If
then in every optimal solution of SF1.
For a route , let , let be the routes that cover only locations in , and let SF1 be SF1 on and with right-hand sides and ; RF1 (75)–(79) is its LP relaxation, and its optimal cost.
The result. Lemma 2 turns one LP solve into an elimination test for every route at once. The route enumeration algorithm of §5.3 generates only routes whose reduced cost is at most a gap , raises until it reaches , and at that point the enumerated route set is guaranteed to contain every optimal solution of SF1. Without the lemma the algorithm would not certify optimality. The same algorithm also solves the single-period problems in the offline estimation stage of the paper's policy, so its correctness underlies all the computational results.
Formalizing it. The lemma is proved in the paper's Online Appendix (Appendix G, p. 42) in a few lines that rest on unstated conventions: the signs of the dual variables, the right-hand sides of SF1, and the equality of with the dual objective of a dual optimal solution, which is LP strong duality. The formalization pins each of these down. The strong-duality step is available on the platform as LinearOptimization.lp_strong_duality (proved, for general-form LPs indexed by Fin), included as a reference item. No part of this mission is formalized elsewhere.
The elimination test (74) and the dual bound are short combinatorial and weak-duality arguments. The step that does not go through by algebra alone is (80) ⇔ (81): it requires that the dual objective of the dual optimal solution equals . Treating this equality as a hypothesis would make the step trivial and is excluded; the hypothesis is only that the dual solution maximizes the dual objective over the dual feasible set. Deriving the equality means applying LP strong duality to RF1, whose data are indexed by arbitrary finite types rather than by Fin, so a transport to the platform's general-form LP is needed. A second point is the passage from SF1 to SF1: removing a route from an optimal solution must yield a feasible point of SF1, which depends on the reduced right-hand sides and on the partitioning rows of SF1 forcing the other routes to avoid 's customers.
All statements live in the namespace OnDemandDelivery.RouteElim. Routes, locations and future periods are arbitrary Fintypes; route vectors are functions to ℝ; and are natural numbers and is computed in ℝ. The standing assumptions are , and (pp. 15–16, (17), (21)).
Conventions committed to:
IsLeast), not an arbitrary real.EReal, when SF1 is infeasible, and (74) is stated in EReal.Trivializing formalizations are ruled out: is not a free real, the dual solution is optimal and not merely feasible, no hypothesis states equals the dual objective, and the conclusion concerns optimal solutions of SF1.
Needed infrastructure: weak duality for the two LPs (elementary), and a bridge from RF1 to LinearOptimization.GeneralFormLP for strong duality, which is reusable for any LP stated over finite index types. Contributions of such a transport lemma are welcome.
Establish the separation exponent for total Boolean functions, improving on the depth-20 specialization of OpenAI's construction.
Precisely, for every and every integer , construct a function with and .
A finite certificate is sufficient: supply a function and an input with , , , and , then apply the shared certificate theorem. Sharper estimates, improved parameters, and different constructions are all eligible; direct family proofs are also welcome.
This is an open research target. The preceding benchmarks are classically and approximately from the depth-20 seed. Numerical searches guide discovery but do not replace certified bounds. Intermediate improvements are welcome as separate campaign entries.
The RangeDivisor problem asks whether an integer has a divisor in a specified short interval. It is the decision problem connecting number theory to the two item periodic joint replenishment model studied by Schulz and Telha. Their Appendix starts with Partition, the problem of splitting a list of positive integers into two groups of equal sum, and constructs a RangeDivisor instance from primes chosen near carefully scaled powers of two. The equivalence between the two yes instances is the mathematical target here. Schulz and Telha, Appendix, pp. 16–17
The route has a history. Karp included Partition among classical combinatorial decision problems in 1972. Shor discussed an NP complete variant of factoring in 2011, and Schulz and Telha adapted that connection to their joint replenishment setting. The paper cites a 2016 conditional short interval result of Dudek, Grenié, and Molteni to obtain primes that can be sampled near the requested powers. That prime existence claim motivates the reduction, while this mission starts with primes satisfying the specified windows. Karp, 1972 Shor, 2011 Schulz and Telha, p. 16
A Partition input is an indexed list of natural numbers. It is a yes instance if some index set has . Indices matter: equal entries may occur more than once and can be assigned separately. For this reduction, , , and each entry lies in . The total is assumed even. Write , so is then an integer even though its Lean definition is real valued. Schulz and Telha, Appendix, p. 16
Set and . The input also includes a real constant and a prime for each index. Every prime lies in the open interval
and the paper's quantitative small window condition holds for every . Define , , and . The RangeDivisor instance uses the integer endpoints and . A valid instance has and ; it is a yes instance if some divisor of belongs to . These conditions are part of the target, not conventions left to the reader. Schulz and Telha, pp. 12, 15–17
The goal states the full correctness of the rounded numerical construction. Under the prime windows above and the paper's condition , the triple is a valid RangeDivisor instance and
The milestones follow the Appendix's stated intermediate claims: the elementary power estimate, the chain of prime windows, the equivalence for a subset sum and its subproduct, the unrounded divisor equivalence, the numerical interval condition, and the paper's rounding assertion. The unrounded equivalence is a separate milestone because it isolates the number theoretic claim from the integer endpoint convention. Schulz and Telha, pp. 15–17
The result turns equal sum partitions into divisors in a controlled interval of a product of primes. This is the first mathematical half of the paper's route from Partition to the periodic joint replenishment decision problem; Lemma 3 supplies the second half. The present theorem identifies exactly which numerical statements that route needs, including validity of the rounded interval. Without the equivalence, the constructed integer might have a divisor in the interval for reasons unrelated to the original Partition input. Schulz and Telha, §3 and Appendix
The paper proves its reduction on paper. This mission asks for machine checked proofs of the reduction's arithmetic assertions, not a new complexity result. The reusable pieces are finite product bounds for real powers, the description of divisors of a finite prime product as subproducts, and a rounding result for the RangeDivisor side condition. Such pieces can support other reductions that encode additive choices by products of nearby primes.
The prime bounds are stated one index at a time, while a divisor of may combine any number of factors. Controlling the product through a strict interval must account for every subset size, including the empty subset and repeated primes. The converse has an additional discrete issue: a product close to the target power should correspond to the exact integer half sum, not merely to a nearby real value. After that, changing real endpoints to integer endpoints must preserve both the divisor question and the numerical promise required by RangeDivisor. A statement only about divisors in the unrounded interval leaves the eventual decision instance incomplete.
Lean represents inputs as functions Fin n → ℕ, index subsets as finite sets, primes with Nat.Prime, and exponents and interval endpoints in the real numbers. The real powers use real exponentiation; uses real division, not truncated natural division. The general Partition and RangeDivisor predicates are separate definitions. The Appendix's , , , and are derived definitions of the particular input, so a theorem cannot choose convenient values for them. Strict window inequalities remain strict, and the goal retains the printed sampling window rather than assuming only the later multiplicative bound. It explicitly asserts the rounded instance condition as well as the yes instance equivalence.
The printed converse needs an even total: if the total is odd, is half integral and a subset one half unit away can produce a product inside without being a Partition solution. A computational reduction can send an odd total to a fixed no instance; this theorem covers the nontrivial even branch. The prose condition that is sufficiently large is replaced by the paper's displayed inequality , and the printed endpoint condition is stated directly. The proof must not gain a vacuous equivalence by allowing zero indices, by selecting the primes existentially to fit the answer, or by dropping the sampled prime windows.
This mission formalizes the correctness of the reduction behind Theorem 2; polynomial running time, randomized prime sampling, the conditional prime count, the padding of arbitrary Partition inputs to a fixed bit range, and the NP hardness assertion are outside its Lean statement. The Riemann hypothesis is needed by the paper to justify finding suitable primes efficiently, not as an assumption of the arithmetic equivalence once those primes are given. Contributions that establish the product, divisor, or rounding milestones are welcome. Schulz and Telha, pp. 15–17
Fair division of indivisible goods asks how to split a set of items among agents with different tastes so that nobody has a strong reason to complain. Fairness notions such as envy-freeness up to any good (EFX) and the maximin share (MMS) have been studied extensively as algorithmic targets: given the agents' valuations, compute an allocation satisfying the notion. In practice the valuations are private, and an agent may misreport them to obtain a better bundle. Truthful mechanisms are too weak for this setting: for two agents, no truthful mechanism without payments produces EFX (or even EF1) allocations when there are more than four goods (Amanatidis, Birmpas, Christodoulou, Markakis, EC 2017).
Amanatidis, Birmpas, Fusco, Lazos, Leonardi and Reiffenhäuser (arXiv:2109.08644, Mathematics of Operations Research 2024) take a different route. They let agents bid strategically and ask how fair the pure Nash equilibria of a non-truthful mechanism are with respect to the agents' true valuations. For two agents they study a modified version of the classical cut-and-choose protocol, due in this form to Plaut and Roughgarden (SIAM J. Discrete Math. 2020). They show that it always has equilibria and that all of them are MMS, and hence EFX. As an algorithm run on truthful values, the same mechanism guarantees no more than a fraction of the maximin share.
There are two agents and a set of indivisible goods. Agent has a non-negative value for each good and values a bundle additively, . There is no free disposal, so an allocation is a partition of .
Mod-Cut&Choose (Mechanism 2) works as follows:
In the Lean development these objects are val, IsBestResponse, IsPNE and rank (namespace StrategicAlloc.RRFair, shared with the sibling missions) and IsEFX, mu, IsApproxMMS, cut and modCutChoose (namespace StrategicAlloc.CutChoose).
For every instance with two agents and non-negative additive valuations,
Both halves are part of the goal. Existence alone, or fairness of equilibria alone, is a weaker statement.
LittleCharity.MMS.mms_le_average, used here as a reference.The theorem identifies a simple mechanism whose strategic outcomes are as fair as the best allocations that exist for two agents: every MMS allocation is EFX, and an MMS allocation always exists for two agents. The mechanism achieves this without any truthfulness requirement. It is the positive counterpart to the impossibility results for truthful mechanisms. It is also the starting point of §4.2 of the same paper, which asks how much of this guarantee survives for every mechanism whose equilibria are always EFX (Theorems 4.5 and 4.7).
The result is proved in the paper. As far as the platform's catalogue shows, none of it is formalized. This mission produces:
The fairness half is short once its ingredients are available. The weight lies in Lemma 4.1: the cut phase is a greedy procedure over a bid-sorted order, and showing that every partition of can be produced requires explicit bids and an invariant along the greedy loop. The case where both sets have at least two goods needs carefully calibrated values. The tie-breaking rules (lexicographic sorting, ties to in both phases) enter the argument, and the formalization fixes them exactly.
A natural shortcut is to restrict agent 1's strategies to orderings of the goods, or to assume that any cut is reachable. Either one turns Lemma 4.1 into an assumption. The existence half needs no compactness argument: the set of possible cuts is finite, so a best cut for agent 1 exists, but this has to be connected with deviations over the continuum of real bid vectors.
Fin 2 (agent 1 is 0) and goods are Fin m, indexed in the order that lexicographic tie-breaking refers to.Fin 2 → Fin m → ℝ. Non-negativity of is a hypothesis of every theorem, and every bid in a profile or deviation is required to be non-negative.mu v i reuses the published LittleCharity.MMS.mms with two bundles and .LittleCharity.MMS.IsEFX is not used.The statements rule out the trivializing formalizations. Deviations are not restricted to a subset of bids (rankings, truthful bids, a finite menu). MMS and EFX are measured with the true valuations, never with the bids. The mechanism's tie-breaking is fixed rather than arbitrary.
A complete development needs basic finite-sum and finite-supremum facts and a proof that the greedy cut covers with disjoint bundles. The model layer (val, IsEFX, IsPNE over all non-negative bids) is shared with the four sibling missions on Round-Robin and on mechanisms with EFX equilibria. Proofs of any milestone, and of mms_le_average, are welcome.
The joint replenishment problem (JRP) is the multi-item extension of the economic order quantity (EOQ) model. Each item is reordered periodically and pays its own ordering and holding costs, and a joint ordering cost is shared by items ordered at the same time. Before this work no hardness result was known for the periodic JRP (p. 10), even though no exact polynomial-time algorithm was known either (Schulz and Telha, arXiv:2007.09045; Operations Research, 2024, as Integer Factorization: Why Two-Item Joint Replenishment Is Hard).
The paper explains this through number theory. In the periodic JRP the joint cost is incurred every periods, so the objective contains a greatest common divisor of the decision variables. The paper's Theorem 2 states that, assuming the Riemann hypothesis, the two-item periodic JRP is NP-hard under randomized reductions. The proof composes two reductions:
This mission formalizes Lemma 3. Mission 4 of this series formalizes the Partition half; missions 1 and 2 formalize the integer-factorization reductions behind Theorem 1.
A period is a positive integer . An item with ordering cost and holding cost costs
per unit time. The two-item periodic JRP (objective (3), p. 10) minimizes, over ,
As a decision problem (p. 13), it asks whether some has cost at most a threshold .
An instance of RangeDivisor (p. 12) is a triple of integers satisfying
it is a yes-instance when has a divisor with .
Given such a triple, the instance sets
and the threshold is , where . Once item 2 is fixed at , item 1 solves problem (5):
In Lean these objects are JRPHard.Aperiodic.eoq, JRPHard.Periodic.periodicCost, JRPHard.Periodic.coefK2, JRPHard.Periodic.coefH2 (shared with missions 1 and 2), and IsRangeDivisorInstance, HasDivisorIn, coefK0, rangeCost, threshold, obj5 and fConv in the namespace JRPHard.RangeDiv.
For every RangeDivisor instance ,
Lemma 3 is the step that carries hardness from number theory to inventory theory. With Shor's result it shows that, under the Riemann hypothesis, no polynomial-time exact algorithm for the two-item periodic JRP exists unless NP problems can be solved in randomized polynomial time. The paper concludes (p. 15) that no algorithm for the two-item problem may be simultaneously exact and polynomial on all inputs, so some concession, such as heuristics, must be made.
The result is proved in the paper; it has not been machine-checked. The mission produces a checked statement of the reduction's correctness with every coefficient explicit, and it corrects two imprecisions in the printed lemma (the threshold and the unspecified "sufficiently large" coefficients of item 2; see below). The objects (eoq, periodicCost) are the same ones used in mission 2 of this series.
Each step is elementary, but the statement mixes integer and real reasoning. The objective of (5) is not monotone or convex in : its value jumps between at divisors of and at least elsewhere. The argument must show that the gap between these two curves exceeds the window around , and this is exactly what RangeDivisor's condition provides. Without that condition a non-divisor can be cheaper than (for , , , the period has objective ). The pinning of also has to beat the slack against , which is where is used.
This mission formalizes the correctness of the reduction behind Theorem 2 (its JRP half, Lemma 3); polynomial running time is not formalized. Theorem 2 itself, Shor's NP-completeness of RangeDivisor under randomized reductions, and "one can construct in polynomial time" are not stated. What remains of the polynomial-time claim is the explicit coefficients and the bound (bit length at most ).
Conventions:
Real.sqrt exactly as printed;Two disclosed departures from the printed lemma:
A formalization that drops the positivity of periods, states the threshold as on the full two-item cost, or leaves existential does not capture Lemma 3 and is ruled out.
No library beyond Mathlib (Nat.gcd, Real.sqrt) is needed. Proofs of the milestones, and alternative proofs of the goal, are welcome.
Reinforcement learning with a generative model (a simulator that returns an independent next state for any queried state–action pair) is the standard setting for measuring how many samples are needed to plan in an unknown Markov decision process. The simplest algorithm is model-based planning: query each pair times, build the empirical transition kernel, and plan in the resulting empirical MDP. Azar, Munos and Kappen (2013) showed that total samples suffice and are necessary, but only for . Agarwal, Kakade and Yang (2020) extended the range to . A sample size barrier remained: for larger , no algorithm was known to be minimax optimal with fewer than samples.
Li, Wei, Chi and Chen (arXiv:2005.12900v8, Operations Research, 2024) remove the barrier: the sample size is minimax optimal over the full range . They give two planners. The first (Theorem 1) perturbs the rewards slightly at random. The second, the subject of this mission, leaves the rewards unchanged and instead chooses among near-optimal actions by a randomized but structured rule.
Timeline:
A finite discounted MDP has states , actions , a transition kernel , rewards and a discount factor . A deterministic policy has value , the expected discounted sum of rewards from , and Q-function . The optimal value is and .
The data are independent next states for every pair, and the empirical kernel is . The empirical MDP has optimal functions and .
The conservative planner (Algorithm 2) draws a threshold independently of the data and plays
the smallest-indexed action whose empirical Q-value is within of optimal.
There are universal constants such that, for every MDP as above, every and , with and
with probability at least over the data and ,
The constants are left unspecified, as in the paper.
The paper's own steps, in the order of §6.4:
Theorem 2 shows that the minimax sample size is reachable over the whole range of without altering the reward function: a planner can keep the model it estimated and only change how it breaks near-ties. The guarantee covers both value and Q-function suboptimality, and with a sample size proportional to rather than in the large- regime it allows a coarse but correct policy to be computed from very few samples.
None of these results is formalized. The mission produces a machine-checked account of the decoupling argument for data-dependent policies (absorbing MDPs, nets, stability of the tie-breaking rule), which the companion missions on Theorems 1 and 3 share. The paper omits the last step of the proof of Theorem 2 ("follows from an identical argument as in the proof of Theorem 1"); a formal proof has to supply it, including the analogue of Lemma 5 for , which the paper does not state.
The policy depends on all the data, so the standard concentration argument for a fixed policy (Lemma 1) does not apply to . A union bound over all deterministic policies costs a factor in the sample size, which is exactly the barrier. The leave-one-out construction removes the samples of one pair from the policy; it works only if the policy is stable under the small change of that this causes. The greedy policy is not stable when two actions nearly tie. The conservative rule is stable with high probability over (Lemma 8), but only because it takes the smallest near-optimal action: the set is stable, and a rule that picked an arbitrary member of it would not be.
All declarations live in the namespace BreakingSample.Conservative. The MDP layer reuses the platform's FoundationsML.ReinforcementLearning definitions (IsTransitionKernel, PolicyValue, QFunction); deterministic policies enter as point-mass stochastic policies, and is the maximum over the finite set of maps . Norms are sup norms on finite function types. The order on is an arbitrary linear order on a finite type.
Probability: a data set is a map with the product law, so probabilities of data events are finite sums. The threshold has the uniform law on ; joint probabilities are , with the outer measure for non-measurable sections. "With probability at least " is stated as an upper bound on the probability of the failure event. Because the policy defined by (10) is a predicate on policies, the conclusion is stated for every policy satisfying (10). The universal constants are quantified before all types and parameters. The goal adds , the standing assumption of (3); "the same assumptions of Theorem 1" is formalized with the goal's own constants .
A trivializing formalization is ruled out: is the smallest-index rule of (10), not an arbitrary policy within of optimal, and is random, not fixed.
Infrastructure that a complete development needs and that is reusable: Bellman optimality for finite MDPs with deterministic policies and real rewards, the resolvent identities, Bernstein's inequality for the empirical kernel, the absorbing-MDP construction, and the analogue of Lemma 5 for the conservative policy. Proofs of any milestone, and of the policy-evaluation lemmas, are welcome.
A blockchain such as Bitcoin settles a limited number of transactions per unit of time, and every on-chain transaction pays a fee that rises with congestion. The Lightning Network moves payments off the chain. Two parties lock funds in a payment channel with one on-chain transaction, and they can then pay each other any number of times by updating the channel balance privately. A new on-chain transaction is needed only when one side of the channel runs out of funds and the channel must be reset.
Guasoni, Huberman and Shikhelman (Management Science, 2023) model a channel between two nodes that pay each other at Poisson rates. They compute its cost and its optimal size, and in §3.3 they quantify how much a channel relieves the chain. The relief is the long-run number of channel transactions carried per on-chain transaction (Proposition 2). A related quantity is the probability that the payee side of the channel, not the payer side, is exhausted first (Proposition 1). This mission formalizes both results, which are statements about two finite random walks.
Node 1 commits units to the channel and node 2 commits units. Node 1 pays node 2 one unit at the jumps of a Poisson process with rate , and node 2 pays node 1 at rate , independently. Write . The balance starts at . It moves up by one when node 2 pays and down by one when node 1 pays. Node 2 has exhausted its side when , and node 1 when .
Only the sequence of payments matters here, not their timing or discounting. Observed at its jumps, the balance is a random walk that steps up with probability and down with probability . Two versions of this walk appear.
The transactions that trigger an on-chain reset are the up-moves from and the down-moves from . Their stationary fraction is
and the long-term ratio of channel to on-chain transactions is .
For with and , the reset walk has a stationary distribution, and every stationary distribution satisfies
Proposition 2 measures how much a channel relieves the chain. A unidirectional channel of size carries payments per on-chain transaction. A symmetric bidirectional channel carries , which grows with the product of the two sizes rather than their sum. For a fixed total commitment, the relief is therefore largest when the flows are balanced. This is the paper's quantitative case that bidirectional channels reduce congestion far more than one-way ones. The probabilities of Proposition 1 tell each node how likely it is to be the one whose funds run out.
Both results are proved in the paper by elementary difference-equation arguments. Neither has a machine-checked proof. Formalizing them gives a verified closed form for the stationary law of a biased walk with resets at both ends. It also gives a biased gambler's-ruin probability on top of the platform's Markov chain library, which so far has only the fair case. The formalization also corrects case (b) of Proposition 1, which as printed claims for every ; the paper's own proof gives .
The reset walk is not a birth–death chain: the balance receives the reset flow from both ends, so the walk is in general not reversible, and the detailed-balance shortcut that gives the stationary law of a reflected walk in one line fails. The balance equation (27) holds only away from and from the two reset points. In Lean, the abstract equation on Fin (l₁ + l₂ - 1) must be related to recurrences indexed by integer balances, and the edge cases and , where the bottom or top balance is itself, have to be handled. For Proposition 1, the hitting probability is defined as an infinite series of first-passage probabilities over trajectories, and the closed form is a statement about the value of that series.
MarkovMixing vocabulary (mm_basic, mm_path). Stationarity is MarkovMixing.IsStationary (nonnegative, sums to one, ), and hitting probabilities are MarkovMixing.hitBeforeProb, a series that sums to when it is not summable. The absorbed walk is absorbed almost surely, so this convention is never triggered.Fin (l₁ + l₂ + 1), with index for the balance . The reset walk has states Fin (l₁ + l₂ - 1), with index for the balance . massAt reads at an integer balance and returns outside the interior, which is the paper's convention .MarkovMixing.exists_stationary_pos and MarkovMixing.stationary_unique for irreducible chains, and the fair gambler's ruin. Lemmas on stationary laws of chains with resets, and biased gambler's-ruin results on the MarkovMixing chains, would be reusable beyond this mission and are welcome.Video-game consoles, streaming services and messaging apps share two features: users value a platform more when more people use it (network effects), and some users buy access to more than one platform (multihoming). In the standard Hotelling model where every consumer buys exactly one good, network effects intensify competition: a stronger network effect makes demand more price-sensitive, and the equilibrium price and profit fall in (the paper's single-homing benchmark, §3.1). Foros, Kind and Stähler (SNF Working Paper 16/21, NHH Bergen, 2021; published in Management Science, 2025, doi:10.1287/mnsc.2022.00613) show that this intuition reverses when consumers can multihome: firms then price the incremental value of their good (Kim and Serfes, 2006; Anderson, Foros and Kind, 2017), and the network benefit of the rival's users feeds back into that incremental value.
This mission formalizes the paper's Proposition 3, which describes how the symmetric multihoming equilibrium price and profit respond to the strength of network effects over the whole admissible range. It is the third of three missions on the paper; the first treats weak network effects with asymmetric firms (Proposition 1) and the second the comparison with the no-network-effect benchmark (Proposition 2).
Two firms sit at the ends of a Hotelling line of unit length, populated by a unit mass of consumers, uniformly distributed. A consumer at distance from firm pays a mismatch cost with . Each good carries exclusive features (the same number for both firms in this mission) plus features common to both goods, which cancel from every object below. Buying good gives a network benefit , where is the network-effect strength and the expected number of users of good ; the paper assumes (Assumption 1(i)).
A consumer buys a second good when its incremental value exceeds its price. Under fulfilled expectations (), the multihoming demand for good at prices is (14)
Maximizing gives the reaction function (15), , whose symmetric fixed point yields the price and profit (26)
In the Lean development these are demandM t μ e pi pj, reactM t μ e pj, pM t μ e and piM t μ e in the namespace Multihoming.Hump. Partial multihoming means that some consumers buy one good and some buy both.
Assume partial multihoming. Then and are hump-shaped in on : there are peaks with
The goal leaves the peaks unnamed; that is the paper's statement.
The result. Proposition 3 says that firms benefit from weak network effects and are harmed by strong ones. As the goods become as if undifferentiated, competition for consumers becomes Bertrand-like, and ; combined with this means firms would prefer a market without network effects once these are strong enough. This non-monotone response is the paper's main qualitative message on pricing under multihoming, and the comparison of Proposition 2 (where the profit curve crosses its level) depends on the same shape.
Formalizing it. The result is proved in the paper by sign analysis of explicit derivatives; it has no machine-checked proof. A formal proof certifies the two derivative factorizations, the location of each peak strictly inside , and the passage from derivative signs to strict monotonicity on closed intervals that the appendix states in one sentence. It also makes explicit the parameter range on which the statement holds, which the printed proposition leaves to the phrase "partial multihoming".
The derivatives of and are rational functions whose numerators are quadratics in with square-root roots; showing that exactly one root lies in requires inequalities between square roots and polynomials in that hold only under . The appendix asserts "it is straightforward" and "it can be shown" at these steps. A second obstacle is the passage from "the derivative vanishes at one point, is positive at and negative at " to strict monotonicity on each closed piece: this needs the sign of the derivative on the whole open subinterval, not only at the endpoints. Showing only that a maximizer exists on is trivial for any continuous function and is not the claim.
HasDerivAt; all functions are smooth near under the hypotheses, and every denominator (, , , ) is positive where it is used, so no statement relies on Lean's convention or for .HasDerivAt, strictMonoOn_of_deriv_pos) and real-closed-field arithmetic are needed. Contributions of any milestone, alternative proofs of the hump via the derivative factorizations, and proofs that identify the price peak explicitly are welcome.Fake accounts (purchased followers, likes and engagement) are a large part of influencer marketing on social media, and platforms say they invest in detecting and removing them. Huang and Liu (Management Science 71(10), 2025) model this market as a signaling game. An influencer of unknown quality buys fake followers to look popular, consumers decide whether to follow, an advertiser pays for the real followers it expects, and the platform, which takes a share of the advertising revenue, chooses how much antifake effort to spend. A practical question for regulators and platform designers follows: does a platform that maximizes profit have any reason to fight fake accounts? This mission formalizes the paper's answer for the purely profit-driven platform: it does not.
The model draws on the signaling literature, in particular the undefeated equilibrium refinement of Mailath, Okuno-Fujiwara and Postlewaite (1993), and is close to the welfare analysis of social-learning manipulation in Chen and Papanastasiou (Management Science 67(11), 2021).
An influencer is of type (probability ) or , with content quality , and . A fraction of consumers (social media literacy) are informed and know the type. The platform picks an effort . With technology level and base price , a fake account costs (1), and following costs a consumer (2), with .
Informed followers of a -type number (8). Uninformed consumers see the early follower count and follow in number (9). The real followers are (10). An uninformed advertiser expects (11). From the -type's side, the advertiser pays for real followers (12). Under a pooling equilibrium both types show the same count and the posterior is . Under a separating equilibrium (costly or natural) the posterior is at the -type's count and at the -type's.
With advertising revenue per real consumer and platform share , the platform's profit under equilibrium type is (6)
where averages (12) over the type. Two thresholds, (13) and (16), with and , select the equilibrium (Proposition 1). If and the equilibrium is pooling. Otherwise it is costly separating for and naturally separating beyond. The equilibrium profit is .
A purely profit-driven platform ( in the objective of (3)) optimally chooses zero antifake effort, and zero is the unique optimum.
Proposition 4(a) separates two motives for antifake effort. Effort harms a profit-maximizing platform twice: it raises the consumers' following cost, which lowers participation and revenue, and it costs . Pooling, in which low-quality influencers successfully mimic high-quality ones, also earns more revenue than separation, because uninformed consumers follow an average influencer more readily than the average of the two types. So any antifake effort a platform makes must come from its concern for consumer welfare (Proposition 4(b)), not from advertising profit. That is the paper's argument for external pressure or regulation.
The result is proved in the paper's Online Appendix. This mission formalizes the main-text claims behind it: the threshold ordering, Lemma 7, the concavity argument and Lemma 8, together with the goal. To our knowledge none of these has a machine-checked proof. The definitions of the follower and profit model are reusable for the companion mission on the influencer's defensive purchasing (Proposition 3).
The obvious argument is "effort only costs, so choose zero". It is incomplete, because effort changes which equilibrium is played, and the equilibrium profit is discontinuous at and . Comparing profits across regimes needs two facts. First, pooling revenue dominates separating revenue at the same effort, a strict-convexity (Jensen) inequality for applied to the uninformed followers through (11)–(12). Second, the thresholds are ordered, , which uses the explicit . The bookkeeping of (10)–(12), where the advertiser's expectation is nested inside the type-average, has to be unfolded exactly. The boundary case falls under Proposition 1(a), so zero effort then induces costly separation, not pooling.
Parameters form a Lean structure with ASCII field names (mu, lamI, lamP, rho, l, qH, qL, c0, c1, tau, p0, gamma). A Standing predicate records the ranges: ; with ; ; ; ; ; . is unconstrained, and Assumption 3 () is a separate hypothesis, used only in Lemma 8(a). The model's expectations are the closed forms (8)–(12); no probability space is built. Follower formulas are untruncated, as in the paper. Assumptions 1–2 depend on , are never stated for a range of , and are not needed, so they are not imposed.
The equilibrium regime map is Proposition 1 taken as a definition: the belief systems, the undefeated refinement and the proofs of Lemmas 1–4 are in the Online Appendix, which this mission does not use. The regime test is " and " for pooling, which matches Proposition 1(a) at . Lemma 7 is stated on all of , a superset of each regime's range. The two separating profits are the same function, because real followers depend only on the information revealed. The concavity milestone assumes , without which both sides are equal.
The goal is about the equilibrium profit computed from (6) and (8)–(12). It is not about abstract regime profits with Lemmas 7–8 as hypotheses, and pooling revenue is not defined by substituting into a single-type formula, which would hide the Jensen step. Consumer welfare is not formalized: its formula is not in the main text, so Proposition 4(b) and Table 3 are out of scope. Contributions welcome: proofs of the milestones and the goal, and a formalization of the signaling game behind Proposition 1.
Video-game consoles, streaming services, ride-hailing apps and payment systems are sold in markets where the value of a product grows with the number of people who use it. In the classical analysis of such markets every consumer buys exactly one of the competing products (singlehoming). Under that assumption, a stronger network effect intensifies price competition in Hotelling models of incompatible products, so equilibrium prices fall (Farrell and Saloner, 1992; Shy, 2001); Katz and Shapiro (1985) find the same under Cournot competition. In practice many consumers own both a PlayStation and an Xbox, or subscribe to several streaming services (multihoming).
Foros, Kind and Stähler (Management Science, 2025; SNF Working Paper 16/21, 2021) let consumers choose endogenously whether to buy one good or both. Their Proposition 1 shows that the classical conclusion reverses once some consumers multihome: near the point without network effects, a stronger network effect raises each firm's demand, price and profit, even when the firms differ in size. This mission formalizes that proposition together with the computations on which the paper rests it.
Two firms are located at the ends of a Hotelling line of unit length, along which a unit mass of consumers is uniformly distributed. A consumer at distance from firm pays a mismatch cost , with . Good has exclusive features worth and shared features worth ; buying good also yields a network benefit , where is the strength of the network effect and is the expected number of buyers of good . Throughout, (Assumption 1 (i) of the paper), and denotes the rival of .
When some consumers buy both goods and expectations are fulfilled (), the paper derives the demand for good at prices :
Maximizing the profit (marginal costs are zero) gives the reaction function
and solving the two reaction functions gives the candidate prices
At these prices the output of good is , the number of singlehomers of good (consumers who buy only ) is , the number of multihomers is , and firm 's profit is . All of these are functions of for fixed . In Lean they are demandM, reactM, priceM, outM, singleM, multiM and profitM in the namespace Multihoming.Local, each taking its parameters in the order .
Partial multihoming means that some consumers buy both goods and some buy only one of each: , , . At this is exactly , and .
Assume and , , . Then there is such that, for each ,
The goal fixes no constant and no size of the neighbourhood: it asserts the direction of every effect near , for asymmetric firms.
The result separates two regimes that the classical theory does not distinguish. Under singlehoming, network effects are a force for competition and lower prices; under partial multihoming, a small network effect makes prices strategic complements (each firm's reaction function slopes upward in the rival's price) and raises the prices, outputs and profits of both firms. This is the paper's explanation for why firms facing multihoming consumers may welcome network effects, and it is the starting point of the paper's later analysis of symmetric firms, of the thresholds on exclusive content, and of mergers.
The proposition is proved in the paper by a short computation: differentiating closed forms at . To our knowledge none of it has been machine-checked. A formal proof would confirm the closed forms (16), (19), (20), the derivative signs (22) and footnote 15, and would upgrade the paper's derivative-at-a-point argument to monotonicity on an explicit interval. The formalization also records a printed slip: the second constant of (22) is printed as , while the value implied by (16) and (17) is . The sign, and so Proposition 1, is unaffected.
Each identity is a rational-function computation with up to quartic denominators, which is tedious but routine once the denominators are known to be nonzero. The substantive step is from a derivative at one point to monotonicity on an interval. The paper computes one-sided derivatives at . To conclude strict monotonicity on , one needs the derivatives to keep their sign on a neighbourhood, which requires continuity of the derivative of each of eight functions (four quantities for each of two firms) and a common . The price claim has no printed derivative at all. A further subtlety is that the profit derivative at is positive only because , which is not a hypothesis but follows from .
HasDerivAt, StrictMonoOn). Lemmas turning a positive continuous derivative on an interval into strict monotonicity are reusable. Proofs of the milestones and of the goal are welcome, as are proofs that derive the goal from the milestones.Demand, prices and click-through rates often follow seasonal cycles: weekly, monthly, yearly. A decision maker who repeatedly chooses among options whose expected payoffs repeat in time faces a non-stationary multi-armed bandit. Chen, Wang and Wang (arXiv:2005.08088v4, Operations Research, 2025) study the model in which each arm's mean reward is periodic with its own unknown period. They give a two-stage policy whose regret is , and a lower bound showing that no policy, even one told the periods, does better than . This mission formalizes that lower bound, Theorem 3 of the paper. A companion mission of the same series covers the upper bound.
Lower bounds of this kind fix what is achievable. For the stationary -armed bandit, the minimax regret is of order (Auer, Cesa-Bianchi, Freund and Schapire, 2002; Lattimore and Szepesvári, Bandit Algorithms, 2020, Ch. 15). In the periodic model a learner effectively faces "effective arms" (arm at each phase of its cycle), which suggests the rate . The paper proves the weaker but general bound , which matches the upper bound up to a factor and logarithms.
There are arms and epochs . An instance is a family of mean rewards . If arm is pulled at epoch , the reward is drawn from the Gaussian law , independently of the past given the arm.
A sequence has minimum period if for all and no smaller positive integer has this property.
A policy chooses the arm at epoch at random, from a distribution that depends on the previous arms and rewards. Its expected regret on is display (1) of the paper:
Three classes of instances appear, all with unit-variance Gaussian rewards and means in (Assumption 1):
The proof compares instances through the metric (B-48),
The periods satisfy Assumption 3 with the parameters (7): with and , , and for every .
For every policy there is with
Theorem 3 shows that knowing the periods does not remove the cost of learning them phase by phase: the regret must grow like , not like . Together with the paper's upper bound and the inequality , it shows the two-stage policy is near-optimal when is fixed. The intermediate results are reusable: Lemma 12 is a clean two-point Gaussian lower bound, Lemma 13 is a phase-decomposition argument that applies to any bandit model with known cyclic structure, and facts 1 and 2 give a continuity framework for the regret as a function of the instance.
The result has a published proof. As far as the platform's records show, none of it has been machine-checked. The stationary minimax lower bound of Lattimore and Szepesvári (a different family and constant) exists on the platform, together with the Bretagnolle–Huber inequality, the Gaussian KL divergence and the divergence decomposition, which this mission lists as tools.
The two-point argument of Lemma 12 is standard, but its constant needs , so small horizons must be handled separately. Lemma 13 decomposes the problem into phase problems; making this rigorous means showing that a policy on the periodic problem induces, on each phase, a policy on a stationary problem of horizon , with a history law that factorizes accordingly. The phase-wise instances produced by the decomposition need not have minimum period exactly (all phases may coincide), so a perturbation is needed to land in ; the constant has slack for it. Fact 2 asks for continuity of an integral against the law of a -round adaptive process, uniformly over all policies, which needs a domination argument that does not depend on the policy's kernels.
Fin K, 0-based: the paper's first arm is index . Epochs are 1-based natural numbers; history coordinate is epoch . Values of the means at are ignored.BanditAlgorithm.BanditPolicy K: one Markov kernel per round from the history to the next arm. The history law periodicMeasure reuses the platform's step kernel with the Gaussian bandit of the current epoch's means; with constant means it is BanditAlgorithm.banditMeasure of BanditAlgorithm.gaussianBandit. Lemma 12 is stated with the platform's banditRegret, , which equals (1) for Gaussian arms; the other statements use (1) directly.Welcome contributions: the bridge between periodicMeasure with constant means and banditMeasure, the phase decomposition of the history law, and the uniform continuity of the regret in the means.
Short selling is never free. To sell a share short, an investor borrows it from a holder and pays that holder a lending fee, and the size of these fees has been documented empirically for decades (D'Avolio 2002; Duffie, Gârleanu and Pedersen 2002). Most equilibrium models of asset pricing either forbid short sales or take the fee as exogenous. Evgeniou, Hugonnier and Prieto build a continuous-time general-equilibrium economy where the fee is determined jointly with prices: investors disagree about expected dividend growth, the pessimist wants to short, the optimist owns the shares, and the cost of shorting clears the securities lending market. The paper uses the model to explain how a positive shorting cost can coexist with apparent mispricing, as in the 3Com/Palm spin-off.
In the special case of a single risky asset (the market portfolio), the equilibrium reduces to a pair of algebraic equations for the shorting cost and the lending yield at each state, and the paper solves them in closed form (Proposition 3). This mission formalizes that closed form and its comparative statics in the belief gap.
At a fixed state of the economy, three numbers describe the environment:
Short selling is active only when the optimist holds a large enough share of consumption, namely on the shorting region , where
Two unknowns are determined in equilibrium: the shorting cost , the flow rate a short seller pays per unit of position, and the lending yield , the flow rate a lender receives per unit of shares held. The paper shows (p. 27) that with one risky asset they satisfy
The proof of Proposition 3 works with the per-volatility yield and the quadratic
In Lean these objects are costOne σ δ s, yieldOne σ δ s, IsOneAssetSystem σ δ s Φ Γ and gQuad σ Δ s γ, all in the namespace CostlyShort.OneAsset.
For and : for every and every , the pair solves (29)–(30) if and only if
and both (31) and (32), as functions of , are non-decreasing and convex on and strictly increasing for .
A companion statement, not a milestone, formalizes the limits on p. 29: as , and .
Proposition 3 is the only fully explicit equilibrium of the paper. It gives the level of the shorting cost and of the lending yield as functions of disagreement and of the wealth distribution, and its monotonicity in is the model's prediction that short interest and lending fees rise with the dispersion of beliefs, which the paper checks against analysts' forecast dispersion (Table 1). Convexity says the effect accelerates with disagreement. The two-asset case of §4.2 has no closed form and is solved numerically; the one-asset formulas are its benchmark.
The result is proved in the paper, but the proof of the comparative statics is omitted ("We omit the details", p. 50), and the selection of the positive root is asserted ("it is clear"). A formal development supplies the omitted differentiation argument, including convexity across the kink at the boundary of the shorting region, and checks the paper's algebra. No part of this paper has a machine-checked proof.
The algebra of milestones 1, 4 and 5 is mechanical but involves a square root and several divisions, whose signs must be tracked throughout. The substantive step is the comparative statics. Monotonicity and convexity of in need the derivative of a square-root expression on the open region, and then a separate argument at the kink: both functions vanish identically for , so convexity on requires the one-sided derivative at to be non-negative, which is a computation rather than a consequence of convexity on each piece. For the paper's route is indirect: with , and composition of a non-decreasing convex with a non-decreasing convex . Differentiating (32) directly is possible but heavier.
Everything is pointwise in real numbers. The continuous-time economy of §2 (Brownian dividends, portfolio choice, the derivation of (29)–(30) from the equilibrium conditions (16), (20), (21)) is the paper's motivation and is not formalized; Proposition 3 is stated relative to (29)–(30), which is exactly where the paper's proof begins. Conventions committed to:
A trivializing formalization is ruled out: stating only that (31)–(32) satisfy (29)–(30), or convexity only on the open shorting region, would be strictly weaker than the paper and is not the goal.
Needed infrastructure is Mathlib's real analysis: Real.sqrt, deriv, MonotoneOn, ConvexOn, and convexity of compositions. Proofs of any milestone are welcome independently. Facts about convexity of a function that vanishes up to a point and is convex beyond it are reusable outside this mission.
A life assurance pays a contingent lump sum under a policy-defined event, rather than a sequence of survivor-contingent instalments. A benefit paid at the end of the policy year of death has a different value from one paid immediately on death. A pure endowment pays instead when the insured survives to maturity, while an endowment assurance combines cover for death before maturity with a maturity payment to survivors. For these products, the event partition, contractual recipient and payment instant must be explicit before an expected present value is calculated.
Promislow (2015, Chapter 5, sections 5.1–5.8) derives a general annual insurance–annuity relationship from benefit vectors. Dickson, Hardy and Waters (2020, Chapter 4) develops the corresponding conventional life insurance factors. The mission makes the death, survival and maturity events visible as actual random cashflows, then derives the classical identities without taking the desired identities as assumptions.
Let the lifetime-state variable take values . For , state represents death during the policy year whose start is anniversary and whose end is anniversary . State represents survival at the model's right-censoring anniversary. Nonnegative probabilities satisfy . The anniversary survival probability is , for . The annual discount factor satisfies , and all values are expressed at policy commencement, time zero.
For an amount schedule in money per death claim, the random present value of a death benefit payable at the end of the death year is
A temporary assurance of duration includes deaths in policy years . A deferred term assurance adds a waiting period and covers deaths in years . A pure endowment is triggered by and pays at time . The term and maturity components are disjoint for . The specific settlement recipient can be identified contractually; if recipient survival or eligibility changes the payment event, that condition requires an additional model variable.
The foundational result is a reconciliation between the expectation of the realised random present value and a separate valuation made from the probability of death in each covered policy year. For a unit sum assured, both routes must produce an actuarial value from exactly the same state law. The analogous pure-endowment reconciliation averages realised survivor payments and independently discounts the survival tail.
The next result establishes the endowment decomposition from disjoint actual payment events, including the zero-term boundary and a terminal survivor who must not receive a fictitious death claim. The year-end-of-death benefit and the maturity benefit are valued separately. Their combination is then reconciled with a survival-contingent annuity paid in advance at anniversaries .
Writing for the annual effective discount rate, the central finite relationship for unit death and maturity benefits is
Here includes deaths before maturity and settlement at the following policy-year end. The maturity mass captures those alive at . The formula is derived by telescoping discounted survival decrements. When the horizon is right-censored, a whole-horizon death-only assurance omits terminal survivors and requires a residual term. A familiar whole-life identity without that term needs certain death by the terminal horizon or an expressly defined terminal benefit.
The source also defines arithmetic increasing and decreasing insured amounts, geometric escalation and minimum-benefit floors. It constructs the second moment of the actual claim present value by squaring its realised value and compares it to a separate squared-benefit death-mass sum. Distinct death years are mutually exclusive, so mixed claim terms vanish. A variance is meaningful only with a normalised, nonnegative probability law. Additional families cover insurance-term extensions, the split of a deferred term, exact commutation recursions and benefit or discount ordering.
The principal capstone starts with a single finite lifetime law and one annual discount basis. It simultaneously derives the death-claim expectation, the pure-endowment expectation, the disjoint endowment decomposition, the finite insurance–annuity conservation identity and the independent second-moment formula. The conservation equation is the substantive conclusion rather than a restated hypothesis. Each item remains an open theorem statement until a valid Prove2Me proof is separately accepted.
The additional model uses an actual real future lifetime T with a specified probability measure μ supported on nonnegative times. It does not infer a continuous death-time distribution from annual mortality probabilities. At nonnegative maturity n, death in 0≤T<n triggers an immediately paid claim. Death at T=n instead belongs to the pure-endowment event T≥n, even if the probability law has an atom there.
At constant force of interest δ, put U=min(T,n). A continuously paid unit annuity has realised present value Y=(1−exp(−δU))/δ when δ≠0, and Y=U when δ=0. An immediate death benefit or maturity benefit pays exp(−δU) under exactly one of the two events. Therefore its pathwise conservation law is
Taking expectations under the same μ produces the distinct continuous insurance–annuity identity
Fractional-time results specify m>0 annual instalment periods, each ending at (r+1)/m. A death in [r/m,(r+1)/m) is payable at the following subperiod end, without ambiguity at exact grid instants. At nonnegative force, immediate payment is at least as valuable as m-thly payment, which is at least as valuable as year-end payment. Supporting results cover cashflow moments, settlement lag, escalation and UDD-versus-constant-force survival. The annual–continuous bridge equates year-end claim values under matched policy-year death masses.
This event-level basis, grounded in the insurance benefit conventions of Dickson, Hardy and Waters (2020, Chapter 4), supports analyses of death-in-service benefits, death-in-deferment cover, pension-scheme lump sums, term life protection and survival maturity benefits. It also makes transparent why the expected value of a lump-sum death claim can be represented using an annuity schedule only after the schedules and discounting are related mathematically. The annuity correspondence reflects an exact payment-mass identity, and a denominator used for recurring premiums needs strict positivity before division.
These reusable cashflow models can support future dependent-beneficiary and pension-scheme guarantees, but true survivor entitlement requires an additional joint-life state.
Careful classification at anniversaries is essential. In the annual model, a death allocated to the policy year following maturity cannot generate both the pre-maturity death benefit and the maturity benefit. Terminal censoring distinguishes survival observed at the end of a finite table from guaranteed eventual death. The conservation identity should remain valid at zero interest and zero term; when no covered deaths occur, its insurance component must vanish. Later death-year payments also make valuation sensitive to the chosen discount factor.
Death-claim second moments require exclusive event indicators, not independence. The capstones derive values from cashflows rather than commutation-table definitions. These constraints exclude vacuous premises and cosmetic equalities.
The private formal development contains two distinct models: a finite annual right-censored K-model with discount factor v and an actual real-lifetime T-model with exponential discounting at force δ. The annual root remains the main theorem, while the continuous insurance–annuity result is a separate supporting capstone. Targeted Mathlib imports encode a probability measure, real claim instants, fractional settlement and cashflow moments.
The classical actuarial identities are already established in the literature. The Draft contains 119 open theorem statements, including seven explicitly formulated reusable root-support lemmas, with no accepted mission proofs. Pinned-revision private Lean checks have verified 85 distinct theorem statements, including the complete 12-conjunct finite annual root, distribution-level insurance–annuity conservation and the annual–continuous settlement bridge. These are private compiler diagnostics, not accepted proofs of published mission targets.
Annual discount d=1−v differs from continuous force δ. The fractional branch models UDD and finite constant-force survival and bridges half-year survival to the payment grid. General-duration inequalities, death-time density valuation, select tables, dependent-survivor eligibility and infinite-horizon convergence remain open. A time-dependent recipient multiplier does not establish joint-life entitlement.
Flatly Foliated Relativity (FFR) is a theory of gravity introduced by Bray, Hamm, Hirsch, Wheeler and Zhang (arXiv:1911.00967, 2019) that sits between special and general relativity. It keeps the Einstein–Hilbert action of general relativity (GR) but restricts it to spacetimes that are foliated by flat Euclidean spaces (Assumption 1 of the paper): "matter curves spacetime, but not space". The authors motivate this by the observed spatial flatness of the local universe. Since gravitational waves are excluded, FFR is proposed as an approximation of GR whose metric equations are much more tractable. It still contains the big bang (FLRW spacetimes with ), accelerated expansion and the exterior Schwarzschild spacetime.
One headline feature of the theory is how a positive cosmological constant (Assumption 2) shapes it. For the paper shows that the FFR metric equations are elliptic on every slice, that the mean curvature of the foliation gives a geometric arrow of time, and that there is exactly one vacuum solution among solutions that are spherically symmetric at infinity. For uniqueness fails, and for existence fails. This mission formalizes Sections 3.2–5 of the paper, which contain these statements.
All FFR equations live on a single flat slice , with no time derivatives, so the formalization works on with coordinates . The spacetime metric is
where is the lapse and is a one-form on , identified with a vector field through the flat metric. Matter enters through the energy density and the momentum density . Writing , and for the flat Laplacian (summation over repeated indices), the FFR equations (34)–(35) are
Substituting with gives the elliptic form (39)–(41), with unknowns . Here :
together with the requirement at infinity. Vacuum means and . When , the paper fixes the time orientation by the arrow-of-time convention (Convention 1). A pair is spherically symmetric at infinity if it is spherically symmetric on for some . Two vacuum solutions count as the same if they differ by an overall positive constant factor, which corresponds to rescaling .
For , the pair , is a smooth vacuum solution that is spherically symmetric at infinity. Every smooth vacuum solution with and that is spherically symmetric at infinity has the form
Theorem 2 (equivalence with the elliptic form), Theorem 3 (arrow of time), Theorem 4 (ellipticity inequality), Lemma 1 (symmetrization), identity (82)–(83), Theorem 5 (uniqueness for the elliptic form under approximate spherical symmetry), Lemma 2 (: many vacua) and Lemma 3 (: no vacuum).
Corollary 2 is the fourth claim of the paper's main result (Theorem 1). It is the precise sense in which FFR with is rigid, in contrast to GR, which has many vacuum solutions that are spherically symmetric at infinity (gravitational waves). Together with Lemmas 2 and 3, it singles out the sign of as the parameter that controls existence and uniqueness. The intermediate results are of independent use. Theorem 2 lets the elliptic system replace the original one, Theorem 4 is the ellipticity statement behind the existence question posed in the paper (Question 1), and Lemma 1 is a symmetrization inequality for the -Hessian operator .
These are paper proofs. No machine-checked version of any of them is known to the proposer. The mission asks for a complete formal proof of the goal and the milestones in Lean 4 with Mathlib.
The algebra is elementary. The difficulty is analytic. The uniqueness arguments rest on maximum principles for the elliptic equations (41) and (45) on all of under conditions at infinity, on Liouville-type arguments for harmonic functions, and on a Newtonian-potential representation (convolution with the Green's function of ) used to show . Lemma 1 needs averaging over rotations (spherical symmetrization), Jensen's inequality and a characterization of its equality case. Theorem 5 then needs a divergence-theorem argument on large balls that is controlled only by the approximate symmetry hypothesis. Mathlib provides the divergence theorem on boxes and some harmonic-function theory, but no ready-made maximum principle for second-order elliptic operators with variable coefficients on .
EuclideanSpace ℝ (Fin 3). One-forms are vector fields , and the paper's is written w in Lean. Partial derivatives are fderiv applied to the standard basis vectors. Because fderiv returns at non-differentiable points, every statement assumes smoothness (ContDiff ℝ ∞) of all fields, as the paper does.volume.toSphere. "Approximately spherically symmetric at " is read as: is bounded and uniformly as , using operator norms.The Riemann zeta function governs the distribution of prime numbers, and the size of on the critical line controls error terms throughout analytic number theory. In 1908 Ernst Lindelöf asked how fast can grow as and conjectured that it grows more slowly than every positive power of . This Lindelöf hypothesis is a consequence of the Riemann hypothesis but is strictly weaker in its formulation, and it is open. It has equivalent forms in terms of zeros of (Backlund) and in terms of moments of on the critical line, and it implies bounds for gaps between consecutive primes (Ingham) and the zero-density hypothesis.
Timeline (as recorded in the source, Wikipedia: Lindelöf hypothesis):
is the analytic continuation to of (). The Lindelöf hypothesis states that for every ,
For real the growth exponent is
taken in the extended reals. The source records that for , that (functional equation), and that is convex (Phragmén–Lindelöf). The Lindelöf hypothesis is the statement .
Zeros of are counted with multiplicity (order of vanishing). denotes the number of zeros with and . is the -th prime and .
This is the existing platform theorem lindelof_hypothesis, referenced as the goal. It is equivalent to the big- form above, which is the published definition RiemannVonMangoldt.LindelofHypothesis used by the milestones.
A proof would give, among the consequences listed in the source, prime gaps , the density hypothesis, and bounds for all moments of on the critical line. Each improvement of the exponent feeds into error terms for divisor problems and primes in short intervals.
On the formal side, Mathlib provides , its functional equation and the Phragmén–Lindelöf principle, which are the starting point for the milestones. The unconditional milestones (properties of , the convexity bound, the zero count in unit windows, the second moment) are classical theorems whose proofs can be formalized now; the bounds of Hardy–Littlewood and Bourgain and the density estimates are proved results with long proofs; the goal itself is open.
The convexity argument interpolates between the bound on and its reflection through the functional equation, and it cannot give better than . Every improvement requires cancellation in exponential sums of length about , and current methods (Weyl, van der Corput, Bombieri–Iwaniec, decoupling) save only a fixed power. The hypothesis demands square-root cancellation up to , which is far beyond these methods. Backlund's reformulation shows it is only "slightly" stronger than the known zero count in unit windows, yet that gap has not been closed.
is Mathlib's riemannZeta; the Riemann hypothesis is Mathlib's RiemannHypothesis. The definition file LindelofHypothesis_GrowthAndZeroCounts introduces as an infimum in EReal (so degenerate cases are , never a junk ), zero counts as ℕ∞-valued sums of analyticOrderAt riemannZeta over the zero set (so an infinite count is and upper bounds cannot hold vacuously), and with primes indexed from . Asymptotics are along atTop, with ; by this covers . Where the source writes the base is read as , and density bounds are stated with an implied constant. " is convex" is stated as: is finite and agrees with a convex real function. The source gives no -range for Huxley's estimate; the range of Huxley's theorem is used.
Contributions welcome: the basic theory of , Phragmén–Lindelöf for vertical strips specialized to , Jensen-type zero counting, mean-value theorems for Dirichlet polynomials, and exponential-sum estimates.
Counting solutions of polynomial equations over finite fields is one of the oldest themes of number theory, going back to Gauss's count of points on modulo a prime. In 1949 André Weil proposed a precise description of how these counts behave when the field is enlarged: for a smooth projective variety over , the generating function of its point counts — the zeta function — should be a rational function with integer polynomial factors, satisfy a functional equation, and have its zeros on prescribed "critical lines", in exact analogy with the Riemann hypothesis. These Weil conjectures organized several decades of work in algebraic geometry and directly motivated the construction of étale cohomology.
Timeline (as recorded in the source article, Wikipedia: Weil conjectures):
Let be a finite field with elements and characteristic . Let be a smooth projective variety of dimension over : a scheme with a structure morphism that is smooth of relative dimension , geometrically irreducible, and admits a closed immersion into some projective space over .
For let be the extension of of degree , and let
be the number of -morphisms . The zeta function of is the formal power series
so that .
There exist integer polynomials and multisets of nonzero complex numbers such that
with , , and over for . 2. Functional equation.
where is the Euler characteristic; moreover as multisets. 3. Riemann hypothesis. for all and all .
The historical partial results (Weil's theorem for curves; Dwork's rationality; Grothendieck's rationality and functional equation; Deligne's Riemann hypothesis) and the worked examples of the source (projective line, projective space, elliptic curves, the genus-2 curve over and the Weil polynomials of its Jacobian).
The Weil conjectures give sharp estimates for point counts, and through them bounds on exponential sums (Kloosterman sums, character sums), the Ramanujan–Petersson conjecture for holomorphic modular forms (Deligne 1971), and the hard Lefschetz theorem over finite fields. They are a standard input in analytic number theory, coding theory and cryptography.
All four statements have been proved since 1974. None of them has a machine-checked proof in Lean/Mathlib at present; Mathlib does not yet contain étale cohomology, Jacobians of curves, or the Hasse bound for elliptic curves over finite fields. This mission records faithful, compiling statements so that partial formalizations — the elementary examples, Hasse's theorem, Weil's theorem for curves via Riemann–Roch or Stepanov–Bombieri, Dwork's -adic rationality proof, and eventually the cohomological proofs — can be attached to a common target.
The examples with a cell decomposition (projective spaces, Grassmannians) reduce to counting points in affine spaces. Beyond them, even rationality is a theorem of substance: there is no elementary formula for , and the counts must be shown to satisfy a linear recurrence. The functional equation and the precise shape of the require a cohomology theory with Poincaré duality and a Lefschetz trace formula; the Riemann hypothesis requires, in addition, control of the absolute values of Frobenius eigenvalues, which in Deligne's proof uses Lefschetz pencils, monodromy and the "tensor power trick". For curves, Riemann–Roch and the Hasse–Weil bound (or Stepanov–Bombieri) suffice, but these too are absent from Mathlib.
k : Type with [Field k] [Finite k] [CharP k p], p prime; q = Nat.card k. Schemes live in Scheme.{0}.Proj of graded by total degree; "projective" means a closed immersion into some commuting with the structure maps. "Non-singular of dimension " is SmoothOfRelativeDimension n f; "variety" is GeometricallyIrreducible f.FiniteField.Extension k p m; is PowerSeries.subst of into PowerSeries.exp ℚ.Contributions welcome: the zeta function of projective space, Hasse's theorem, point counts and Weil polynomials for the examples, rationality for curves, and general infrastructure (Riemann–Roch for curves, Jacobians, étale cohomology).
Mass–energy equivalence is the relationship between mass and energy in a system's rest frame: the two differ only by the constant factor , the square of the speed of light,
It was proposed as a general principle by Albert Einstein in 1905 ("Does the inertia of a body depend upon its energy-content?") as a consequence of special relativity, and it underlies nuclear and particle physics: the mass defect of a nucleus measures its binding energy, and the energy released in fission or annihilation is accounted for by the change in rest mass.
Timeline. Electromagnetic-mass relations of the form were considered in the late 1800s and by Poincaré (1900) and Hasenöhrl (1904). Einstein (1905) derived the relativistic kinetic energy and stated that a body emitting energy as radiation loses mass . Planck, Stark, Lewis–Tolman and Lorentz (1907–1914) rewrote the relation in its modern forms, and von Laue (1911) gave a proof from the stress–energy tensor. This mission follows the Wikipedia article Mass–energy equivalence.
Velocities and momenta are vectors in with Euclidean norm . Fix a speed of light . A body of rest mass moving with velocity , , has
For a finite system of free particles the invariant mass is , the total energy over in the centre-of-momentum frame (zero total momentum). A Lorentz boost with speed along the first axis sends to , .
It contains as the case .
The energy–momentum relation is the kinematic identity behind relativistic energy bookkeeping: rest energy, kinetic energy, invariant-mass reconstruction and the frame independence of rest mass all follow from it. The low-speed expansion makes precise in what sense Newtonian mechanics is the limit of relativity. The composite-system statements formalize why, in relativity, mass is neither additive nor separately conserved while energy and momentum are conserved.
All results are classical and established in the physics literature. The mission produces machine-checked versions of these kinematic facts in a reusable -vector setting with an explicit speed of light.
Most single-particle statements are algebraic once the square roots are controlled; the work lies in handling the square-root and division conventions of a total formal language. The power-series milestone requires the binomial series of , and the asymptotic milestones require Taylor-type bounds near . The non-additivity milestone is a reverse triangle inequality for future-pointing timelike four-vectors, including its equality case, which does not reduce to a one-line computation.
Lean uses EuclideanSpace ℝ (Fin 3) for , with explicit (no natural units). All definitions are total functions: for and , so every theorem assumes and ; rest masses are assumed non-negative. Massless particles cannot be described by velocity-based quantities ( is undefined at ), so milestone 3 is phrased directly in terms of an energy–momentum pair. Only boosts along the first axis are formalized. Systems are finite and free (no interaction potential). Historical derivations (Einstein 1905, Rohrlich 1990) and the nuclear-physics applications are not formalized.
Many service systems must route work to servers whose quality is not known in advance: crowdsourcing platforms matching job types to worker types, wireless schedulers assigning users to channels, call centers routing request classes to agent pools. Learning the unknown service rates is a multi-armed bandit problem, but the cost of a bad decision is not a lost reward. It is a longer queue, and a queue can recover from past mistakes when it empties. Krishnasamy, Sen, Johari and Shakkottai (arXiv:1604.06377v4, Operations Research 2021, doi:10.1287/opre.2020.1995) measure the cost of learning by the queue-regret, the expected excess queue length relative to a genie that knows the rates. Their analysis shows two regimes. Early on the regret grows like a bandit regret. After the system has learned enough to stabilize, queues regenerate and the regret decays. This mission formalizes their lower bound for the second regime: no reasonable learning policy can make the late-stage queue-regret decay faster than .
The lower bound adapts the classical consistency-based bandit lower bounds of Lai and Robbins (1985) and their non-asymptotic, hypothesis-testing form (Bubeck, Perchet and Rigollet 2013) to queue dynamics. The step from counts of suboptimal schedules to queue lengths is specific to queues.
A switch has queues and servers. Time is slotted, . In slot queue receives an arrival , and the link between queue and server offers a service . All of these are independent, and i.i.d. over slots. A problem instance is the pair , with every entry in .
In every slot the scheduler picks a matching : queue is assigned server , and distinct queues get distinct servers. The scheduler knows neither nor . Its decision in slot may use the past schedules, the services observed on the scheduled links in slots , and its own randomness. Queue receives and evolves as
Assumption 1 (unique optimal matching) says that each queue has a unique best server , and that implies . The genie always schedules . Its queues start from the same and see the same arrivals and offered services, with . The queue-regret of queue is .
Write , , , , , . With the Bernoulli divergence , display (2) of the paper defines
Let . For , a policy is -consistent (Definition 2) if for every instance with a unique optimal matching there is a constant with for all and all . Consistency rules out policies tuned to one instance, such as "always schedule a fixed matching", which would have zero regret on that instance and linear regret elsewhere.
For every instance with a unique optimal matching, every law of the initial queue lengths, every and every -consistent policy:
A companion item, Lemma 1 (p. 10), states : queue-regret never exceeds the bandit regret.
Theorem 3 shows that the paper's Q-UCB algorithm, whose late-stage queue-regret is (Theorem 5), is optimal in its dependence on up to polylogarithmic factors. It also separates queue-regret from bandit regret. The bandit regret of a consistent policy grows like , while the queue-regret decays to zero. The cost of learning in a queue is transient, but it cannot vanish faster than . The theorem holds for every initial law of the queues, so it does not depend on the system starting in steady state.
The proof is complete in the source (§9.1, pp. 37–42). As far as we know none of it is machine-checked. A formal development would also give the first formal bandit lower bound in which the consistency class must contain the alternative instances of a change-of-measure argument, here instances with two optimal servers swapped, together with a reusable model of a learning scheduler on a switch.
The obvious route is to bound the regret of each slot by the probability of a suboptimal schedule (Lemma 21), and to bound the number of suboptimal schedules from below by a Lai–Robbins argument. Both steps resist direct proof.
For the first step, and share arrivals and services but are not ordered pathwise, because the policy's services are independent across links. A comparison exists only in distribution.
For the second step, the alternative instance must again satisfy Assumption 1, so a single service rate cannot simply be raised. When server is the best server of another queue , the best servers of and must be swapped, and the divergence decomposition then involves two links.
The final step goes from a cumulative bound to an "infinitely often" bound, and only from a logarithmic lower bound on partial sums. A lower bound on cumulative regret does not give a bound for every large .
Queues and servers are Fin U and Fin K (0-based), with . The hypothesis is added: for the policy and the genie coincide and both sides are zero, and the minimum defining would range over an empty set. Slots are 1-based.
The probability space is canonical: with law . A seed holds one uniform per arrival, one per link and one for the scheduler, and , . A policy maps the history of past schedules and observed services, together with a private uniform seed, to a matching. The only constraint is measurability in the seed, so every randomized history-dependent policy is covered. The law of is arbitrary, as the paper notes after Theorem 3, so Assumption 3 is not used. Assumption 2 (stability under the optimal matching, for every ), which the paper assumes whenever queue-regret is evaluated (p. 8), is a hypothesis of Theorem 3 and of Lemmas 1 and 21. Lemma 19 and Corollary 20 concern schedule counts, which do not depend on the arrival rates.
is a Bochner integral of , which is bounded by . Expected counts are integrals under the seed law, since the schedule never observes arrivals or . and are set to when , where the divergence is . Corollary 20(c)'s becomes the sum over servers outside the range of . Fact 1 is stated for every real sequence: the printed "bounded" is not needed and does not hold in the application. "For infinitely many " is ∃ᶠ t in atTop.
-consistency quantifies over every service matrix in satisfying Assumption 1, and its constant is chosen after the instance. Requiring consistency on the given instance only would make Theorem 3 false, because the genie's own policy has . A constant chosen before the instance would make the hypothesis unsatisfiable.
A complete development needs the canonical seed space and its measurability, a chain rule for the KL divergence of the history laws, the Bretagnolle–Huber inequality (available), and an elementary harmonic-sum estimate. The switch model and the consistency class are reusable for the paper's early-stage lower bound and its upper bound. Proofs of any milestone, and alternative proofs of Lemma 21 that avoid the coupling, are welcome.
The source is the arXiv v4 preprint; the paper's proofs are in its §§8–9.
An indistinguishability obfuscator (iO) is a compiler that scrambles a program so that any two programs computing the same function become computationally indistinguishable after compilation. Garg, Gentry, Halevi, Raykova, Sahai and Waters gave the first candidate construction for all circuits (SIAM J. Comput. 45(3), 2016; conference version FOCS 2013). The candidate later became the starting point of a large body of work on iO, functional encryption and their applications (Sahai–Waters, STOC 2014).
The security of the candidate rests on a new assumption about garbled branching programs (the paper's Assumption 1, "Equivalent Program Indistinguishability"). Appendix C of the paper gives evidence for it: in an idealised generic colored matrix model, where an attacker can only add, scale and multiply the published matrices in an order that respects their colours, the assumption holds unconditionally. That unconditional statement is Theorem 6, and it is the target of this mission. It is an information-theoretic counting statement over finite fields; it involves no machines, no running times and no negligible functions.
Timeline. Barrington (1986) showed that width-5 permutation branching programs compute NC¹. Kilian (1988) randomised such programs by conjugating consecutive matrices with random invertible matrices. Garg, Gentry and Halevi (2013) proposed approximate multilinear maps. The present paper (2013) combined the three, adding a dummy program, bookend vectors and bundling scalars, and analysed the result in the generic colored matrix model. Later work (Barak et al. 2014; Brakerski–Rothblum 2014) proved security in a generic multilinear-map model for modified constructions.
A branching program of length on input bits consists of a map and, for every step and bit , a permutation matrix . On input it outputs iff . A partial assignment fixes the input bits in ; two partial assignments , are functionally equivalent if the program computes the same function of the remaining bits under both.
Fix a prime , and . The randomized program consists of the matrices and , together with bookend vectors , and their primed versions. Here the are uniform invertible matrices over ; is block diagonal with random diagonal entries and the block ; has the block (the "dummy program"). The vector is zero on its first entries and on its next , and their last five entries (and ) are random subject to . The bundling scalars are products of random 's arranged so that their products over each block agree.
In the generic colored matrix model each matrix carries a left and a right colour (: ; : ; : ; : ). A representation oracle holds the database : the bookends, one matrix per step and program for the fixed steps (bit ), and both for the free steps. An adversary sees only handles. It may ask to add two matrices of the same colours, scale one, or multiply two whose colours match. The oracle answers with the handle of an existing record whenever the result equals a stored matrix mod , so equality of matrices is all the adversary learns.
For every prime , branching program , functionally equivalent and adversary receiving at most handles,
for an absolute constant . No value of is fixed, as the paper gives none.
Theorem 6 says that the candidate cannot be broken by any attack that stays within linear algebra over the published matrices in the intended order: partial evaluations, mixing the primal and dummy programs, and mixing inputs that are inconsistent within a block are all detected or harmless. The proof explains the purpose of each design element: the bookend zero patterns kill the random diagonals, and the dummy program and bundling scalars defeat mixed-input attacks.
The theorem has a pen-and-paper proof in the paper and, as far as is known, no machine-checked proof. A formalization would pin down the model exactly: how ⊥ replies, handle reuse and adaptivity behave, and which distribution the bundling scalars follow. These are points the paper leaves informal, and the formal statement records them. The milestones are reusable on their own: the bookend identity and Lemma 2 are pure algebra, and the partial-evaluation bound is a Schwartz–Zippel application to block-diagonal matrix products.
The obvious argument says each new handle is a "new polynomial", and Schwartz–Zippel makes a collision unlikely. That argument fails for bookend products. There, a primal and a dummy evaluation on an accepting input are equal as field elements but different as formal expressions, so a simulator must identify them using only . No other cancellation may survive, including those between products that mix the two values of an input bit within a block, and those on rejected inputs, where the 5-vectors are correlated through . The bundling scalars are products of two uniform field elements, so they vanish with probability about , and the counting has to absorb such degenerate events. Finally, the adversary is adaptive: its later queries depend on earlier equality patterns, so the comparison of the two executions must go through a simulator that does not depend on .
Everything is over ZMod p with [Fact p.Prime]. Probabilities are counting fractions over finite product types; no measure theory is used. Steps, handles and -indices are 0-based. Branching programs output iff the ordered product of permutation matrices is the identity; this is the convention of §3, §4.2 and App. C, not the outputs of Definition 9. The bundling scalars follow the -procedure of p. 42. §4.1 instead says "random subject to the constraint", and over the two distributions differ; the proof analyses the -procedure. A malformed query (unknown handle, mismatched dimensions or colours) is answered ⊥ and leaves the database unchanged. Adversaries have coins uniform on Fin K, make adaptive queries and output a bit. The statistical distance between the views is expressed as the largest acceptance gap over all adversaries; this is equivalent, since every distinguisher of the views is an adversary's final decision. is taken to be , the number of handles a -query adversary receives. The page's in the partial-evaluation case is read as .
Trivializing formalizations are excluded. The constant comes before , so the bound cannot absorb the trivial distance . The oracle compares matrices mod together with dimensions and colours, never formal expressions, and it respects colours. The sampler keeps every random component of §4.1.
The development needs only Mathlib (matrices, GL, MvPolynomial, Schwartz–Zippel). Proofs of the milestones are welcome independently. A formal treatment of the paper's simulator (non-commutative formal polynomials, canonical forms) would be a reusable contribution for other generic-model arguments. The paper's PPT security reductions (Theorems 2–4) are out of scope; the mission formalizes the paper's evidence for Assumption 1, not the obfuscator's security.
In contextual dynamic pricing a seller posts a price for each arriving customer, observes only whether the customer buys, and must learn the demand from these binary responses while selling. The problem arises in e-commerce, insurance and consumer lending, where every customer comes with features (product attributes, customer characteristics) that shift the willingness to pay. Most regret analyses assume either that the noise distribution of the valuation is known up to a parameter, or that it belongs to a parametric family. Luo, Sun and Liu (arXiv:2109.07340, Mathematics of Operations Research, 2024) drop that assumption: the valuation is linear in the features plus a noise with an unknown distribution, and they give a policy, DIP, whose regret is bounded without parametric knowledge of the noise.
This mission formalizes the paper's main upper bound, Theorem 1, together with the chain of lemmas and propositions of its proof. The source is the arXiv v2 preprint (6 March 2023); all proofs are in its Appendix A.
At each period a customer arrives with a covariate , where on . The customer's valuation is , with an unknown parameter , for a known , and market noises drawn i.i.d. from an unknown CDF . The seller posts a price and observes ; the revenue is . The expected revenue of price at linear value is
The clairvoyant price maximizes over and is assumed to lie in . The regret of period is , and .
Two assumptions are made on . Assumption 1: is -Lipschitz. Assumption 2: there is a constant with for all , and .
The DIP policy (Algorithm 4) splits time into episodes of lengths and , , for . In episode it takes an estimate computed from episode (Inner Algorithm A), cuts into equal pieces with midpoints , and runs a UCB rule (Inner Algorithm B) over the candidate prices . The UCB step is analysed as a perturbed linear bandit (PLB): rewards whose parameters satisfy . The algorithm M-LinUCB (Algorithm 5) is optimistic linear UCB with forced exploration of new coordinates.
For every model satisfying the standing assumptions and Assumptions 1–2, every DIP configuration with and , there is such that every run of DIP satisfies, for all ,
where is the number of episodes. The printed statement reads ; the single logarithm is what the proof gives.
In the order of the proof: Lemma 1 (the pricing problem of one episode is a PLB with perturbation ); Lemma 2 (M-LinUCB on that PLB is Inner Algorithm B); Lemmas S1–S5 (weighted averages, the elliptical potential lemma, the shadow parameter, the self-normalized bound, a confidence ellipsoid); Lemma 3 (M-LinUCB on a PLB has regret with high probability); Proposition 4 (the discrete-part regret of one episode); Lemma S6 (the confidence term in form); Proposition 3 (the total regret of one episode, ). Lemmas S2 and S4 are already proved on the platform and are referenced.
The bound separates the cost of learning the unknown noise distribution, up to a logarithm, from the cost of estimating , which enters only through the estimation errors. Any estimator with a known error rate therefore gives an explicit regret rate for DIP: if with , the regret is (p. 19). The rate of the paper's logistic-regression estimator on adaptively collected data is not established; the authors study it by simulation. Lemma 3 is a regret bound for linear bandits with bounded parameter drift that is linear in the drift and otherwise, which the authors note is of independent interest.
The results are proved in the paper, not formalized. The two textbook lemmas the paper quotes, the elliptical potential lemma (S2) and the self-normalized bound (S4), are already proved on the platform; the paper's own results (Lemma 3, the PLB reduction, the episode analysis and Theorem 1) have no machine-checked proof. Faithfulness checks during drafting found printed slips that the formal statements correct and disclose: the unsquared norm in Lemma S2, the finite UCB of an unpulled arm in display (2), and a missing nonemptiness condition for the candidate price sets.
The obvious argument treats each episode as a linear bandit around the central parameter and invokes the standard optimistic regret bound. That fails because the parameter moves with the covariate through the estimation error ; the ridge estimate then tracks no fixed vector, and a general misspecified-bandit bound pays an extra factor in the drift term (Remark 5, p. 21), which destroys the rate once grows with the horizon. A second difficulty is bookkeeping: the per-episode bound must hold uniformly over the random estimate , over the growing discretization , and over the truncated last episode, before the episodes are summed.
Periods are 1-based; arm indices are Fin d, 0-based. Norms are written out: , coordinatewise. The probability space carries a filtration ; covariates and prices are -measurable (adaptive or adversarial covariates and randomized prices are allowed), and has CDF and is independent of . Conditional sub-Gaussianity is Mathlib's HasCondSubgaussianMGF, which needs a standard Borel sample space. Expectations are lower Lebesgue integrals of nonnegative regrets. "With probability at least " means a measurable event of probability at least on which the bound holds.
The standing assumptions are , , on , and maximizing the revenue over . Hypotheses added to the printed statements: (resp. ), which makes every candidate price set nonempty; in Proposition 3; in Lemma 3; finite action sets; a nonempty index set in Lemma S1. Algorithm 3 is read with forced exploration of unpulled arms, as Lemma 2 fixes. Inner Algorithm A is any measurable estimator of the previous episode's data with values in ; the paper's logistic regression with projection is one instance. Algorithms are run predicates that hold for every tie-breaking rule. The constants of Theorem 1, Proposition 3 and Lemma S6 are chosen before the processes, the estimate, and the horizon.
The formalization cannot be satisfied trivially: expectations are integrals of nonnegative quantities, so no non-integrability default applies; the run predicates are satisfiable (a sorry-free check accompanies the drafts); LinUCB is a closed form whose maximality over the confidence ellipsoid is itself a milestone, not a real supremum; and the noise CDF is pinned by .
A complete development needs the PLB analysis (Lemmas S3, S5, 3), which is reusable for any linear bandit with one-sparse actions, and the conditional Hoeffding step for Lemma 1, for which a platform theorem exists. Proofs of any milestone, and reusable lemmas on ridge estimates with diagonal designs, are welcome.
Robust control repeatedly meets linear matrix inequalities that must hold for every value of an unknown, norm-bounded matrix. A typical instance is
where collects model uncertainty or noise. Such a condition quantifies over infinitely many matrices and cannot be checked directly. Petersen's lemma (Petersen and Hollot, Automatica 1986; Petersen, Systems & Control Letters 1987) replaces it by a single inequality in one scalar multiplier . The lemma is a standard tool in the design of quadratically stabilizing controllers for uncertain systems, and it was recently used for controller design from noisy data (Bisoffi, De Persis and Tesi, arXiv:2109.12175).
H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman (arXiv:2203.12959v3, 2023; SIAM J. Control Optim.) develop a theory of quadratic matrix inequalities (QMIs) and prove matrix versions of the S-lemma. In §4.5.3 they show that both the strict and the non-strict Petersen lemma follow from their matrix S-lemmas (Theorems 4.10 and 4.7) by a suitable choice of the two quadratic forms. This mission formalizes that derivation.
Timeline. Petersen and Hollot (1986) and Petersen (1987) state the lemma for stabilization of uncertain linear systems. Bisoffi, De Persis and Tesi (arXiv 2021) use strict and non-strict versions for data-driven stabilization. van Waarde, Camlibel, Eising and Trentelman (2023, Proposition 4.16) recover both versions from matrix S-lemmas.
All matrices are real. For a symmetric matrix , () means positive semidefinite (definite), and means ; the notation includes symmetry. is the Moore–Penrose pseudo-inverse and the positive semidefinite square root of .
Quadratic matrix inequalities. A symmetric is partitioned into blocks (), , , (). Its solution sets are
and is defined in the same way with . The generalized Schur complement is , and the class consists of the with , and .
Petersen's data. Fix symmetric, , with , and . The uncertainty set is . Display (4.17) defines
In this proposition the letters of the QMI section become , so .
(a) The robust strict inequality holds if and only if a single multiplier exists:
(b) If , and , the same equivalence holds with in place of on both sides.
The result itself. Petersen's lemma converts a semi-infinite family of matrix inequalities into one inequality that is jointly an LMI after a Schur complement. In controller synthesis this makes robust quadratic stabilization against norm-bounded uncertainty a convex feasibility problem. The derivation in this paper places the lemma inside a general theory: Petersen's lemma becomes the special case of the matrix S-lemmas for the pair of (4.17), and the hypotheses , , of the non-strict version become exactly the Slater condition of Theorem 4.7.
Formalizing it. All results here are proved in the paper. None of them, and no matrix S-lemma, has a machine-checked proof on this platform. The mission produces formal statements and proofs of Petersen's lemma in both forms, of the contraction factorization Lemma A.1, and of the strict and non-strict matrix S-lemmas, which are reused by the data-driven stabilization results of the same paper (Theorems 5.1 and 5.3).
The "if" directions are routine: a multiplier certificate yields the robust inequality by completing a square. The difficulty is the converse, which needs a lossless S-lemma for matrix-valued quadratic forms. The scalar S-lemma rests on the convexity of the joint range of two quadratic forms (Dines' theorem). It does not apply directly to matrix inequalities, and the reduction of Section 4.2 from the matrix case to the vector case is the main obstacle. A second, smaller obstacle is the non-strict case: an equivalence with is false without a Slater-type condition, and the formal statement has to carry , and exactly where the paper does. Petersen's lemma does not follow from a pointwise choice of . The quantifier over must first become a QMI in , which is what Lemma A.1 provides.
Matrices are Mathlib Matrix over ℝ. In the goal the sizes are Fin n, Fin p, Fin q. In the S-lemmas the two block index types are arbitrary finite types, and a partitioned matrix is a matrix over the sum type. is (−X).PosDef and is (−X).PosSemidef; both include symmetry, as the paper's notation does. is (F̄ − FᵀF).PosSemidef. The multiplier is required positive, so is the true inverse. The pseudo-inverse is the unique matrix satisfying the four Penrose conditions, selected by Hilbert's ε, and the square root is Mathlib's CFC.sqrt under the scoped matrix order. "At least one positive eigenvalue" refers to the eigenvalues of the symmetric matrix . "Full column rank" is B.rank = q.
Two choices differ from a literal transcription, and both are disclosed in the items. The strict "Moreover" of Lemma A.1 carries no rank hypothesis, because already forces full column rank. The Schur step includes its non-strict analogue, which the paper uses implicitly ("the proof of statement (b) is analogous").
A trivializing formalization is excluded. The quantifier in the goal ranges over every with , not over a fixed or over . Part (b)'s extra hypotheses are not added to part (a), and the sanity instance , , satisfies every hypothesis and both multiplier conditions at .
A complete development needs: Loewner-order calculus and Schur complements for block matrices; Moore–Penrose pseudo-inverse identities; positive semidefinite square roots; the scalar S-lemma (Dines' theorem); and the reduction from matrix to vector QMIs. The S-lemmas and Lemma A.1 are reusable well beyond this mission. Proofs of any milestone, and of the auxiliary results of §4.1–4.2 (Lemmas 4.1–4.5, Theorem 4.6) as supporting theorems, are welcome.
Quadratic matrix inequalities (QMIs) describe sets of matrices rather than sets of vectors. They appear whenever an unknown matrix is constrained by a quadratic bound: in robust control, where an uncertain block of a system is only known to lie in a norm ball or a sector, and in data-driven control, where the system matrices of a linear system are unknown and the measured data, corrupted by noise satisfying a quadratic bound, only pin them down to a set defined by a QMI.
H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman (arXiv:2203.12959, SIAM J. Control Optim. 2023) develop a systematic theory of such sets, culminating in matrix versions of the S-lemma and of Finsler's lemma and in data-based stabilization tests. Before any of that can be used, one has to know when the set of matrices satisfying a QMI is nonempty, convex, bounded, has interior points, or contains strict and boundary solutions. Section 3.1 of the paper answers these questions in terms of the blocks of the matrix defining the QMI. This mission formalizes that section, Theorem 3.2, together with the Schur complement identities (3.2)–(3.4) on which it rests.
All matrices are real. Fix integers . For a matrix , the Moore–Penrose pseudo-inverse is the unique matrix with
is the set of symmetric matrices; for , and mean positive semidefinite and positive definite, , the negative versions, and means (the Loewner order).
A matrix is always partitioned as
For the QMI is
with solution set . Replacing by or gives the sets of strict solutions and of solutions of the quadratic matrix equation. The generalized Schur complement is
and the class (equation (3.5) of the paper) consists of the with
In Lean these are pinv, qmiForm, ZSet, ZPlus, ZZero, schur and InPi in the namespace QuadMatIneq.Basic.
For :
For with and :
Theorem 3.2 turns geometric questions about a set of matrices into finite checks on the blocks of : semidefiniteness, definiteness, vanishing and a rank comparison. In the data-driven setting of the paper, (after transposition) is the set of noise samples, and hence of systems, consistent with the data; part (b) decides when that set is compact, part (c) when it has interior, and (a) guarantees convexity, which is what allows linear matrix inequalities to be used over it. The identities (3.2)–(3.4) are used throughout the rest of the paper, in the matrix S-lemma, the matrix Finsler lemma and the parametrization of solution sets.
The result and its proof appear in the paper; this mission produces machine-checked versions. Mathlib has the Schur complement for invertible blocks and positive semidefiniteness, but no Moore–Penrose pseudo-inverse for matrices and nothing on QMI solution sets. To the knowledge of this mission no formalization of these statements exists.
The obvious argument is the classical Schur complement, which requires to be invertible. Here is only negative semidefinite, and the singular case is exactly where the interesting behaviour lives: the solution set is unbounded precisely when has a kernel, and gives the whole space. Working with the pseudo-inverse requires the range and kernel identities of for a symmetric matrix and the kernel inclusion at every step. Part (c) needs a topological argument about the interior in , and part (e) needs a factorization of one positive semidefinite matrix through another of possibly different size, which is a rank argument rather than an identity.
toBlocks₁₁, …, toBlocks₂₂. Nothing assumes except part (b).Classical.epsilon over the four Penrose conditions. Since a solution exists and is unique, this is the pseudo-inverse and not a default value; the total inverse A⁻¹, which is on singular matrices, is not used anywhere.PosSemidef and PosDef, which include symmetry, matching the paper's convention that definiteness is only asserted for symmetric matrices. is IsHermitian.Infrastructure needed and reusable beyond this mission: the existence and uniqueness of the matrix pseudo-inverse with its basic identities (, is the orthogonal projector onto the range), and the generalized Schur complement identities. Contributions of these as separate lemmas are welcome.
Learning dynamics in games describe how players who repeatedly interact adjust their strategies from observed payoffs. A central question is whether such dynamics lead to Nash equilibrium. For the replicator dynamics, the canonical model of evolutionary game theory, the answer is negative in general: in Matching Pennies and in generic zero-sum games with a unique interior equilibrium, replicator trajectories cycle forever. A classical positive result survives: if a replicator trajectory of a 2-player game stays a bounded distance away from the boundary of the strategy space, its time average converges to the Nash set (Hofbauer and Sigmund, 1998, Ch. 7).
Mertikopoulos and Sandholm (arXiv:1407.6267v2; Math. Oper. Res. 41(4), 2016) study a broad family of continuous-time learning dynamics, regularized reinforcement learning: each player aggregates payoffs into scores and plays the mixed strategy that maximizes score minus a strongly convex penalty function. The family contains the replicator dynamics (entropic penalty) and the projection dynamics (quadratic penalty). For non-steep penalties, trajectories can enter and leave the boundary of the strategy space infinitely often, so the classical "stay away from the boundary" criterion is no longer natural. Section 6 of the paper replaces it with a condition on scores and derives convergence of time averages in zero-sum games with an interior equilibrium.
A 2-player finite game has players , finite pure strategy sets , and payoff functions on pure profiles. A mixed strategy is a probability vector on ; is the set of mixed profiles and the expected payoff (2.1). The payoff vector of player is , the payoff of the pure strategy against the opponent's mixed strategy (2.2). A profile is a Nash equilibrium if no player gains by a unilateral deviation to another mixed strategy; it is interior if for every and . The game is zero-sum if .
On the simplex of a finite set, a penalty function (Definition 2.1) is continuous on , smooth on the relative interior of every face, and -strongly convex for some :
No steepness is required. The choice map is (Definition 2.2), the convex conjugate is (C.1), and the Fenchel coupling is (C.10).
Each player has its own penalty function . An orbit of (RL) is a pair of trajectories , , of score vectors and mixed profiles with
The time average of the orbit is .
If is a 2-player zero-sum game with an interior Nash equilibrium, then for every orbit of (RL),
The statement fixes no rate and no particular penalty function: it holds for every choice of .
The result. Proposition 6.2 shows that the time-average convergence known for the replicator dynamics in zero-sum games is a property of the whole class of regularized reinforcement learning schemes, including those whose trajectories hit the boundary of the strategy space infinitely often, such as the projection dynamics. Time-averaged play of no-regret-type dynamics in zero-sum games is the continuous-time counterpart of the standard argument that averaged learning computes minimax strategies. Theorem 6.1 isolates the mechanism for general 2-player games: bounded score differences suffice, with no zero-sum assumption.
Formalizing it. The results are proved in the paper; none has a machine-checked proof. A complete formalization produces reusable components: differentiability of the conjugate of a strongly convex function on the simplex (a Danskin-type statement), the Fenchel-coupling identity along the dynamics, and a conservation law for zero-sum games. These are the building blocks of many analyses of mirror-descent and follow-the-regularized-leader dynamics.
The first idea, comparing itself with the equilibrium, fails: need not converge, and for non-steep penalties it does not stay in the interior, so the Kullback–Leibler argument used for the replicator dynamics is unavailable. The conserved quantity is a function of the scores , not of , and turning its boundedness into control of score differences requires the asymptotic behaviour of the choice map when some scores diverge. The second difficulty is analytic: is not differentiable at the boundary of , yet must be differentiable everywhere on the score space, with derivative , for the chain rule along (RL) to apply. Finally, the passage from score differences to the time average uses that is linear in the single opponent's strategy, which is specific to two players.
Fin 2, strategy types A k are finite, payoffs are real functions on pure profiles; mixed profiles, expected payoffs and mixed Nash equilibria come from the published agt_games vocabulary (AGT.IsMixedNash). Zero-sum is for every pure profile; interiority is .IsPenalty h K is Definition 2.1 with strong convexity in the Euclidean norm; since is existential the class does not depend on the norm. Steepness is not assumed. Each player has its own .IsChoice h y x (maximizer of over ), never a chosen argmax. An orbit is IsRLOrbit u h y x: for , and , a right derivative at . This differential form is equivalent to the integral form (RL) because is continuous along an orbit.Metric.infDist in the sup metric on profiles. For Theorem 6.1, which has no equilibrium among its hypotheses, the conclusion also asserts that the Nash set is nonempty, because the distance to the empty set is in Lean.Contributions are welcome on any milestone; Proposition C.1 and Proposition A.1(iii) are self-contained convex-analysis statements about a single penalty function.
A variational inequality asks for a point of a convex set at which a vector field points "inward" against every feasible direction. It is the common form of convex minimization (with a gradient), of saddle-point problems (with the monotone operator of a convex–concave function), of Nash equilibria of convex games, of complementarity problems and of traffic and economic equilibria. Iterative methods that use only evaluations of and projections onto the feasible set are the methods of choice when the problem is large, because each step is cheap.
The classical such method, the projected gradient iteration , does not converge for merely monotone . Korpelevich's extragradient method (1976) does, at the price of two projections and two evaluations of per step, and it is known to converge R-linearly under strong monotonicity (Tseng 1995, reference [19] of the paper). Popov (1980), Tseng (2000) and Censor–Gibali–Reich (2011) reduced the number of projections or evaluations. Yu. Malitsky's projected reflected gradient method (arXiv:1502.04968, SIAM J. Optim. 25(1), 2015, doi:10.1137/14097238X) uses one projection and one evaluation of per step, evaluating at the reflected point instead of at . This mission formalizes the paper's second main result: under strong monotonicity the method keeps the R-linear rate of the extragradient method.
Let be a real Hilbert space with inner product and norm , let be closed and convex, and let . The metric projection is the unique point of nearest to . The variational inequality (1.1) is
with solution set . The paper's standing assumptions for this result are
Algorithm 3.1 chooses and a step and iterates
The Lean development names these objects proj, solSet, IsStronglyMonotoneMap, IsLipschitzMap and IsPRGRun in the namespace ProjReflGrad.Linear.
Under (C1), (C2*), (C3) and , every run of Algorithm 3.1 converges to the solution of (1.1) at least R-linearly:
The goal fixes neither nor ; the proof produces them from , and , but the theorem asserts only the shape of the rate.
In attack order:
The result. Theorem 3.3 shows that halving the per-step cost of the extragradient method does not cost the linear rate under strong monotonicity. For strongly monotone problems (strongly convex minimization, strongly convex–strongly concave saddle points, strictly monotone games with a quadratic margin) the method therefore reaches accuracy in iterations with one projection each, which matters when projecting onto dominates the cost. The two-step recursion (3.9) and Lemma 2.8 are also a reusable template: the same mechanism gives linear rates for other methods with a memory of one past iterate.
Formalizing it. The theorem is proved in the paper; nothing here is open. No machine-checked proof of it, or of its lemmas, is on the platform. A formal proof needs the projection inequality in a general real Hilbert space, a careful account of the reflected iterate, and a rigorous version of Lemma 2.8, whose printed proof leaves the range of and the positivity of implicit. The deliverable is a checked R-linear rate for a one-projection method in infinite dimension.
The natural first attempt, a contraction (Q-linear convergence), is not what the paper proves and is not available: the reflected point depends on , so the error at step is controlled only by the errors at steps and , together with auxiliary terms and . Strong monotonicity is applied at , not at , and can be smaller than ; the lower bound may even be negative. The step range is exactly what keeps the coefficients of the Lipschitz error terms below the gain from the projection inequality, and the resulting two-step recursion needs Lemma 2.8, with its choice of and , to yield a geometric bound.
[CompleteSpace H]); it is never specialized to .LipschitzWith, whose constant admits ). (C1) stays in the goal: it is the paper's assumption and its only source of .VectorSpaceOpt.min_distance_convex_set, included as a reference. Contributions welcome: proofs of the milestones in any order; Lemma 2.8 and the identity of milestone 2 are self-contained.