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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
The Shannon information function measures the average information gained when one samples a discrete probability distribution . Its use as a measure of distinguishability (the mutual information of Chapter 2 of C. A. Fuchs's thesis, arXiv:quant-ph/9601020) is only as convincing as the reasons for the formula itself. Section 2.4.1 of the thesis derives the formula from two requirements on an information function: it depends only on the probabilities and not on how outcomes are labelled (symmetry), and the expected information gained does not depend on the order in which an observer asks about the outcome (objectivity). The derivation follows Z. Daróczy (Information and Control 16, 1970), who embeds the problem in a one-parameter family of functional equations whose solutions are explicit, and recovers Shannon's formula as the limit .
Characterizations of this kind go back to Shannon (1948), Khinchin (1953) and Faddeev (1956), who used continuity or monotonicity assumptions. Daróczy's route needs no regularity hypothesis on at all: symmetry and the recursion of type already force a closed form, and the regularity enters only through the limit in . This mission formalizes that derivation as Fuchs presents it (Theorem 2.7, printed pp.32–35).
For let
be the -point probability distributions and . In Lean, IsDist p says that p : Fin n → ℝ lies in .
A function is a family of functions of real arguments. It is symmetric (IsSymmetric H) if for every permutation and every .
Fix a real parameter , . A function satisfies the recursion of type (SatisfiesRecursion α H), Eq. (2.111), if for every and with ,
At this is the objectivity requirement (2.110). Throughout the proof, for (2.114), and .
Let be symmetric solutions of the recursion of type , and suppose as . Then for every and ,
The constant fixes the units: for bits, for nats.
The result singles out the Shannon entropy among all symmetric information functions by a purely algebraic requirement, with no continuity, monotonicity or measurability assumption on . Milestone (2.130) is of independent interest: it shows that the symmetric solutions of the recursion of type are exactly the multiples of the Daróczy information of type , (known in physics as the Tsallis entropy), which is related to the Rényi information of order by (2.132). The goal then identifies the Shannon entropy as its limit, which fixes the information function used for the mutual-information distinguishability measure in the rest of the thesis.
The theorem is classical and its proof in the thesis is complete; none of these statements is formalized on the platform, and Mathlib contains the Shannon entropy only in the form of Real.negMulLog and binary entropy, without a characterization theorem. This mission produces a machine-checked characterization of the Shannon and Daróczy entropies from symmetry and recursivity, reusable by any development that needs to justify an entropy formula axiomatically.
Each step is elementary, but several are easy to get wrong. The reduction (2.115) iterates the recursion, which only applies when the first two entries are not both zero; distributions that begin with zeros must first be permuted using symmetry. The symmetry of (2.122) needs the substitution , and then a second substitution (2.127), each valid only away from the endpoints, so the boundary cases must be handled separately with . The final limit is a form in ; the thesis applies l'Hôpital's rule (its display (2.131) prints , a misprint for ), and entries must be checked to contribute on both sides.
H : (n : ℕ) → (Fin n → ℝ) → ℝ; its values off are irrelevant. The family in the goal is H : ℝ → (n : ℕ) → (Fin n → ℝ) → ℝ, with symmetry and the recursion assumed for every , .p 0, p 1, and the merged vector is Fin.cons (p 0 + p 1) (fun i => p i.succ.succ).0 / 0 = 0 imposes no extra condition on .Real.rpow, so for ; logarithms are natural (Real.log), and Real.log 0 = 0 gives .𝓝[≠] 1. "Up to a constant " is read as: if then ; a family with constant is a special case.Needed infrastructure: finite sums over Fin n with Fin.cons/Fin.succ reindexing, permutations of Fin n, Real.rpow identities for , and one-sided derivatives of for the limit. Proofs of any milestone, and alternative routes to the goal through (2.130), are welcome.
A forecaster, an economist or any expert who sells a probability distribution cannot be checked directly: a single outcome of an experiment never reveals whether the reported distribution was the expert's true state of knowledge. The only safeguard is to pay according to a scheme under which lying does not pay in expectation. This is the problem of keeping the expert honest, studied in the statistics and decision-theory literature on proper scoring rules (Good 1952; McCarthy 1956; Savage 1971; Aczél and Pfanzagl 1966).
Chapter 2 of C. A. Fuchs's thesis Distinguishability and Accessible Information in Quantum Theory (arXiv:quant-ph/9601020) uses this problem to derive a measure of distinguishability of probability distributions. If honesty is enforced by an optimal payment scheme, the expected loss an expert suffers by reporting instead of his true measures how far apart the two distributions are. Aczél's theorem (Theorem 2.3 of the thesis, p.21) says that for three or more outcomes the optimal schemes are exactly the logarithmic ones, and the expected loss is then the Kullback–Leibler relative information , eq. (2.76). This mission formalizes that theorem and its proof as given on pp.20–24 of the thesis.
An experiment has outcomes . A strictly positive -point distribution is a vector with every and (IsPosDist). An expert whose knowledge is reports a distribution and is paid when outcome occurs, where are fixed real functions chosen in advance. His expected earnings are .
The family keeps the expert honest (KeepsHonest F) if
for every pair of strictly positive -point distributions : telling the truth maximizes expected payment.
For ,
The printed theorem allows any constant ; the "if" direction is false for , and the statement here carries the correction , which the thesis's own proof derives.
The milestones follow the proof on pp.21–24, for any two distinct outcomes (the page's outcomes 1 and 2):
The theorem singles out the logarithmic payoff from an incentive requirement alone, without any appeal to additivity or to axioms about information. In the thesis it is the route from a decision problem to the Kullback–Leibler information (2.76), one of the classical distinguishability measures that Chapter 3 then optimizes over quantum measurements. The same characterization underlies the uniqueness of the logarithmic scoring rule among local proper scoring rules, a standard fact in forecast evaluation and in the theory of elicitation.
The result is classical and proved; this mission produces a machine-checked version of it. Neither Aczél's characterization nor the specific chain (2.50)–(2.69) is on the platform. Mathlib has Lebesgue's differentiation theorem for monotone functions and Gibbs-type inequalities; the platform has Gibbs' inequality without its equality case (gibbs_inequality) and the almost-everywhere differentiability of globally monotone functions (FamousTheorems.lebesgue_monotone_differentiation_6b), but neither in the form stated here.
The "if" direction is a short convexity argument. The difficulty is the "only if" direction: nothing is assumed about the , not continuity and not measurability, so regularity must be extracted from the inequality itself. Monotonicity follows by combining two instances of (2.50). Differentiability is the delicate step. The sandwich (2.61)–(2.62) only transfers differentiability from at to at ; one needs a point of differentiability of to start from, which is where Lebesgue's theorem enters, and the freedom to move through , which is exactly what provides. For , is pinned to and the theorem fails: Muszély's family (2.75) gives many non-logarithmic honest payoffs. The natural first idea, differentiating (2.47) in at with Lagrange multipliers, presupposes the differentiability that has to be proved.
Fin n; payoffs are F : Fin n → ℝ → ℝ; is Real.log.Contributions welcome: proofs of the milestones, in particular a reusable Lebesgue-type lemma for functions monotone on an interval and the transfer argument (2.66); the Shannon inequality with equality case is reusable well beyond this mission.
Allocating scarce vaccines, ventilators, or antiviral treatments can involve several ethical priorities at once. A reserve system attaches a quota to each category and gives that category its own ordering of eligible patients. Categories can express different claims on the same supply without making the medical units physically different. The mathematical question is which assignments simultaneously honor eligibility, avoid leaving a usable unit idle, and respect the applicable priorities. This mission concerns the deferred-acceptance characterization in Pathak, Sönmez, Ünver and Yenmez, arXiv:2008.00374v3, §§3.1–3.5, pp. 13–18.
A single ranking of patients need not express the priorities of every category. The model therefore allows category orders to differ independently. It also records the category through which a patient receives a unit. That information matters even when all units provide the same benefit: it identifies which quota was used and which priority order governed the assignment. The source explains this distinction in §3.2, pp. 13–14.
There is a finite set of patients and a finite set of categories . Category has a natural-number quota , with total supply . Its priority order is a strict linear order on . The distinguished outside option determines eligibility: patient is eligible for category exactly when . Categories may have overlapping eligible populations, independent priorities, or zero quotas. No scarcity inequality between supply and population size is assumed.
A matching is a function such that for every category. Each patient receives at most one unit, and means that patient is unmatched. Membership in the set of matchings imposes capacity alone. Eligibility is a separate axiom.
The source specifies three requirements. Compliance with eligibility requires every assigned patient to be eligible at her assigned category. Non-wastefulness requires a category to be full whenever an eligible patient is unmatched. Respect for priorities requires every patient assigned to a category to outrank every unmatched patient in that category's full order. This last requirement compares recipients with unmatched patients, including ineligible unmatched patients; it does not compare all pairs of patients assigned to different categories. These are Definitions 1–3, pp. 14–15.
An artificial preference profile assigns each patient a strict order on , with exactly when is eligible at . The set of all such compatible profiles is . These auxiliary orders may differ across patients; they do not describe differing values for the identical medical units.
The individual-proposing deferred-acceptance algorithm, abbreviated DA, begins with no patient held. Free patients apply to their highest-ranked untried eligible category. In each simultaneous round a category considers both its current incumbents and its new applicants, retains its highest-priority quota-many patients, and rejects the rest. Rejected patients continue down their lists. The source stops when a round makes no rejections and finalizes the holds. A matching is DA-induced when it is the output for some profile in ; see §3.5, pp. 17–18.
The single target is the complete statement of Proposition 1, printed/PDF p. 18 of arXiv:2008.00374v3. For every reserve system and every capacity-feasible matching ,
Equality here is equality of the whole assignment function, including the category assigned to every recipient. Both directions and all three axioms belong to the same target. There are no numbered supporting milestones: the proof in Appendix C.2, printed A.13–A.14 / PDF pp. 57–58 uses the definitions directly.
The characterization connects an axiomatic description of acceptable assignments with a concrete allocation procedure. It identifies exactly the assignments reachable as the auxiliary preference profile varies, rather than merely establishing existence of one acceptable assignment. Independence of category priorities preserves the possibility that different categories express different allocation criteria.
The paper supplies a mathematical proof. This mission provides its Lean statement and the definitions needed to formalize that proof; the goal is not yet proved in Lean. The general finite admissions market, assignment type, and simultaneous DA procedure are reused from published definition modules. The additional definitions expose the reserve model's full priorities, its three axioms, and the conversion to algorithm inputs. A completed proof would verify this connection while retaining zero quotas, partial eligibility, and arbitrary finite sizes.
The operational output and the axiomatic description express different kinds of information. A run records applications, rejections, and temporary holds; the axioms concern the final matching. Categories may displace incumbents, priorities may conflict across categories, and eligibility can exclude some pairs. These features make it necessary to track the actual simultaneous procedure faithfully.
The converse demands a realizing compatible profile for each prescribed matching satisfying the axioms. Producing an arbitrary fair matching, or only the same set of recipients, would not meet that requirement. Likewise, replacing respect for priorities by a familiar stability predicate would alter the target. These distinctions are present in the model and Proposition 1, pp. 13–18.
Patients and categories use Fin n and Fin m with arbitrary cardinalities, and Option supplies the outside option. Full strict orders are rank bijections, with smaller ranks better. This retains every order, including ranks below the outside option. Supply is defined as the sum of the quotas, eliminating a redundant parameter. Empty populations are included as a boundary generalization; every source instance remains available.
The published assignment type is combined with a separate capacity predicate. Published admissions feasibility and stability predicates do not replace the source's axioms. The adapter sorts the eligible restrictions of the full orders into acceptable lists. For compatible profiles, mutual-acceptability filtering removes no pair. The published recursion uses the number of permissible pairs as fuel and pads stationarily after termination; its terminal assignment agrees with the source's no-rejection stop convention. This is an encoding convention, not an additional hypothesis or a numerical bound asserted by Proposition 1.
DA-induced is defined using the computed output, never by choosing an assignment already satisfying the axioms. No algorithm-correctness or preference-realization fact is supplied as model data. The mission excludes the separate cutoff-equilibrium characterization, sequential-reserve comparative statics, and smart-reserve results. Work on the complete proof and its necessary internal invariants is within scope.
A retailer selling perishable products must choose both a selling price and an inventory position. The two decisions affect sales, spoilage, stock carried to the next period, and the information available for future decisions. Demand parameters may change during the selling horizon, while the distribution of demand disturbances and the distribution of perishability are initially unknown. The paper of Keskin, Li and Song proposes policies that combine price experimentation, statistical estimation, and change detection. This mission concerns its stated regret guarantees for both policies, including the intermediate results used in their analysis.
There are selling periods. A history policy chooses a real price and a real order-up-to level using past observed demands, perished proportions, and actions. Prices and inventory positions belong to nondegenerate compact intervals and with positive endpoints. Replenishment has zero lead time and no fixed ordering charge. Unmet demand is lost but observed.
Demand is . The known link is increasing and twice continuously differentiable. The unknown pair lies in a compact rectangle with negative price coefficient. It has change points; distinct parameter values are separated by a positive distance. There is no minimum duration for a constant segment. The disturbances are independent and identically distributed, centered, and have a bounded second moment and a local moment generating function bound. Their distribution may have atoms. A separate independent sequence of perished proportions has a beta distribution with an unknown, time-independent parameter in a positive compact rectangle.
Inventory evolves according to . A feasible decision satisfies . Known nonnegative holding, lost-sales, disposal, and ordering costs are denoted by . The standing restriction is for every allowed price. The single-period expected profit is defined by the actual cost integrals in equations (4)–(5), including perishability and both positive-part losses.
The full-information anticipatory benchmark, or FIA, knows the complete deterministic parameter sequence and the primitive laws, but cannot observe future shocks. It maximizes the expected total reward in equation (3), including terminal salvage. The paper explicitly assumes an interior optimal solution exists. Learner and benchmark have separate inventory trajectories on common primitive shocks. Their regret is the expectation of the signed sum of their single-period profit differences.
The principal target is both clauses of Theorem 1 in the supplied paper:
Each constant is positive, finite, and chosen before the horizon and the allowable locations and values of the changes. Constants may depend on the fixed change-count bound, model bounds, noise law, separation, and policy tuning. The learner's rules are chosen before the unknown noise law, change count, separation, and environment. The conclusion includes their executability; the theorem does not assume away failed constructions.
Both policies alternate experimentation and profit maximization. Their experimental lengths and cycle lengths are the printed ceiling formulas. Experimental observations support demand quasi-likelihood estimation, beta maximum likelihood estimation, and change detection. Demand estimation uses observations since the last detected change; perishability estimation uses all past experimental observations. DDPO-N optimizes a residual-based empirical profit on a sparse price grid. DDPO-E fits a known exponential family and optimizes its estimated profit over the full continuous price interval. Both then apply the printed inventory adjustment.
The eleven milestones are Proposition 1, comparing FIA with the full-information non-anticipatory policy; Propositions 2–3 on parameter estimation; Lemmas EC.2 and EC.1 on noise moments, sample-cost tails, and optimal inventory; Propositions 4–7 on the two profit proxies and the pricing and inventory decisions; Theorem 2 on estimation regret for both policies; and Proposition 8 on delayed detections and early false alarms for both policies. Every displayed clause and constant factor is retained.
The claimed bounds distinguish the effect of learning a general disturbance distribution from learning a known exponential-family representation. Their shared benchmark includes inventory carryover and anticipation of changing demand. A complete verification would therefore address more than a static estimation problem or a stationary pricing policy.
This mission supplies concrete statistical objects, observable histories, inventory dynamics, estimator relations, and the actual regret sums. Definitions contain no unproved assertions. The theorem declarations are open statement drafts, not machine-checked proofs. Formalization also exposes source defects that require scrutiny. In particular, an admissible small horizon produces contradictory experimental prices, and the general maximum-likelihood result does not assume identifiability. The stated targets retain those defects so that a proof or a disproof addresses the source claim.
Estimation, reset times, and optimizer choices depend on the same observed data. Replacing the resulting sample indices by a fixed independent sample changes the problem. Arbitrary disturbance laws also prevent silently assuming density lower bounds, smooth quantile inverses, or uniformly positive link derivatives. The source's proof of pricing convergence contains a derivative-sign gap; no such derivative hypothesis is added to the statement.
Partial operations create a separate issue. A quasi-likelihood equation may lack a root, a likelihood may lack a maximizer, and an experimental inventory position may be infeasible. An arbitrary default action would define a different algorithm. The execution relation instead retains all prescribed equations and actual optimizer requirements.
Prices and inventories remain continuous. Probability uses infinite independent primitive sequences, while actual rewards stop at . The infinite sequence matters for the literal indexing formula in Lemma EC.2. General exponential families use an explicit dominating measure, permitting continuous and discrete distributions without imposing identifiability or a convex parameter set. Measurable optimizer selections retain ties. Expectations that appear in asserted guarantees carry integrability content, preventing a divergent integral from becoming Lean's default zero.
The probability bounds with random are read literally: the event probability is a scalar, and its displayed comparison with the random right side holds almost surely on the stated range. The reset times remain random inside the event. Noise-only probabilities integrate the noise sequence with the perishability sequence fixed, recomputing the history and estimates. The inventory lemma asserts existence of the level identified by both formulas, without adding uniqueness. It uses extended-real infima and suprema, preserving empty-sign-set failures. A concrete lower-bound optimum makes the strict-negative-derivative set empty even in a model with an interior FIA solution; this source counterexample is recorded alongside the other findings.
Equation (6) is read consistently with equations (1)–(2), retaining . Proposition 8(b) uses the lower endpoint appearing in the final decomposition. Both readings are declared per item and recorded as source findings. The source basis is published, but the supplied artifact is internally dated January 3, 2021 and contains SSRN footers; citations use its own pages, not invented journal pagination. Empirical extensions, age-dependent spoilage, censored-demand experiments, and externally cited lower bounds are outside this mission.
An A/B experiment collects observations while a user decides whether the evidence is strong enough to act. A user may inspect the experiment repeatedly and stop when a result looks convincing. A test calibrated only for one sample size does not automatically retain its error guarantee under that behavior. A sequential test instead makes the stopping decision part of the statistical procedure. In the supplied Johari–Pekelis–Walsh preprint, the question goes beyond error control: how much sampling does a continuously monitored test require compared with every other test offering at least its power?
Different users can tolerate different delays. One may abandon an experiment after a modest number of observations; another may wait longer. The paper models these choices by a maximum sample count and a tolerated probability of false rejection. Its first-order efficiency claim concerns a single family of tests that can accommodate these choices without knowing them when the mixing distribution is selected. This mission addresses that claim, using the exact preprint version and theorem numbering stated below.
Let be independent identically distributed real observations under each parameter law . The natural parameter ranges over an arbitrary nonempty open interval , and is the null. The alternatives are all other parameters in the interval. The source's exponential family has densities . The cumulant is twice differentiable, has strictly positive second derivative, and each observation law has finite fourth absolute moment. These are the standing assumptions of Section 5.2, page 18.
A decision rule consists of a positive integer stopping time , possibly infinite, and a binary decision . Decisions use only the observations available at stopping. Rejection means ; a test that never stops must not reject. The rule has no access to the unknown parameter or to independent randomization outside the observation filtration. Its Type I error is .
Fix a mixing distribution on with continuous strictly positive density throughout the interval. For , define
The mixture sequential probability ratio test, or mSPRT, first stops at and rejects exactly when this time is finite. An empty crossing set gives infinity. A user with maximum count and tolerance instead observes samples and rejects when . Thus a crossing at the last allowed sample still rejects. These are equations (7)–(9) and Section 5.1.
The sole supporting milestone is equation (10), page 19. For every fixed admissible and every fixed alternative , set
The claim is
For the goal, the power profile of a bounded rule is and its relative run length is . A feasible competitor stops by almost surely, has Type I error at most , and has power at least the truncated mSPRT's power at every alternative. The competitor need not belong to a nested family of tests. Definition 3, page 21, defines
The goal is the complete Theorem 2, page 21: if is absolutely continuous on its parameter interval and finite on an open neighborhood of , then, for every fixed admissible ,
The constant is exactly one. Both infima stay inside the limit. All qualifying paths are included, even when tends to zero.
The efficiency claim compares sample use with an entire class of decision rules, while requiring that competitors match power at every alternative. It therefore addresses a stronger question than the runtime of one test at one parameter. The mixture is fixed before the user's asymptotic choices; the first-order claim does not optimize a new mixture at each tolerance.
The source presents this as a theorem. The present formalization supplies open Lean statements, not completed proofs. It also records two gaps in the printed argument and a support ambiguity in its likelihood notation. Formal work can determine whether the complete printed target is provable or admits a counterexample. Those findings do not replace the goal with a repaired or restricted claim.
Convergence of the runtime at each fixed alternative does not imply convergence after taking an infimum over all alternatives and all feasible rules. Alternatives can approach the null or move toward the boundary as the tolerance changes. The printed proof on pages 42–43 obtains a comparison at a selected alternative, which alone cannot lower-bound the full infimum. It also substitutes a parameter that need not approach zero into an expansion stated as the parameter tends to zero. These are identified proof gaps, not asserted counterexamples to the statistical theorem.
The model reuses the published scalar exponential-family definition with scale one and zero base log density. An arbitrary reference measure is allowed; choosing recovers every density family in the source. Observations may live on any measurable probability space, while the history sigma algebras are exactly those generated by the observed coordinates. Coordinate zero represents .
Stopping times use extended natural numbers. Nonnegative expectations and both infima use extended nonnegative reals. Infinite stopping times are never replaced by zero. At valid finite horizons, positive sample counts give positive finite denominators; the mSPRT's error control supplies a feasible competitor. These facts must follow from the definitions rather than enter as assumptions. The milestone includes square integrability and almost-sure finiteness in its conclusion. The goal uses every valid sequence to express the joint limit.
Equation (7) is read as the exponential likelihood ratio after cancellation of the carrier density. This agrees with its quotient wherever defined. A carrier with disconnected support can give a sample mean where the printed quotient is ; that issue is recorded explicitly. No everywhere-positive carrier assumption is added. Definitions of binary decisions, positive-density mixtures, natural histories, and efficiency support further sequential-testing work.
Objects. For a real let be the product over primes up to , written in Lean as a product over Nat.primesLE ⌊x⌋₊. Mertens' third theorem says this product is asymptotic to . Explicit two sided versions with small constants are used in sieve theory and in explicit work on almost primes.
Goal. The goal item is mertens_prod_lower: for every real , . The constant 1500 is deliberately crude. It comes from a fully elementary route, not from the zeta zero data behind the sharp Rosser and Schoenfeld constants.
Context. The lab file derives explicit forms of Mertens' second and third theorems from Mertens' first theorem by partial summation. The goal is obtained there from the block form of the third theorem at together with the single factor at . In the lab it is proved conditional on the open items listed in this mission: abel_recip (Abel summation for ), integral_A_sub (an integral error bound), neg_log_one_sub_inv_bounds (a two sided bound for ) and harmonic_mul_prod_le (the harmonic sum times the product is at most 1). The goal also depends on lab inputs not restated here, namely Mertens' first theorem in explicit form Decomp1528a.mertens1_abs, which is the subject of the earlier public mission bb2fc174 on Decomp1528a, and on several other fully proved lemmas of the same file. No item here is a CITED input.
Source. P. J. Campbell, arXiv 2608.09488 v1, 2026, Section 4, which uses Rosser and Schoenfeld, Approximate formulas for some functions of prime numbers, Illinois J. Math. 6, 1962, p. 70 (Theorem 7) as the sharp comparison.
Nothing is claimed about binary Goldbach, which remains open. The mathematics here is classical.
These statements come from an AI-run Lean lab; AI wrote the Lean code. Each statement was copied verbatim from the lab file and compiled against Mathlib, and an independent AI read-back of every item is attached for checking; the lab's owner submitted it without a separate line-by-line human audit. No proof is supplied here.
For a natural number let with , let , and let be the weighted count of representations of as a sum of three primes. The Hardy and Littlewood circle method proves ternary Goldbach type results by writing as the integral of over the unit interval, splitting the interval into major arcs and minor arcs, bounding the major arc integral from below and on the minor arcs from above.
This mission packages that frame as it is used by Liu and Wang. The goal ternaryAbove_of_arcs says: if for every odd there are a measurable set and reals , with the major arc integral at least , off in , and , then every odd is a sum of three primes. In the lab the goal is proved conditional on the open items listed here: orthogonality of on , the circle identity , Parseval for , the split of the integral over and its complement, the trivial minor arc bound, and the Chebyshev type bounds and . The item norm_S_le, the trivial bound , is an open leaf of the same file that the goal does not use. The step from to a representation is proved in the lab and is not restated.
The source is Ming-Chit Liu and Tianze Wang, On the Vinogradov bound in the three primes Goldbach conjecture, Acta Arithmetica 105 (2002), pp. 133 to 175, Section 3. These are standard facts; no item is a CITED deep result. Ternary Goldbach is a theorem of Helfgott; nothing is claimed about binary Goldbach, which remains open.
These statements come from an AI-run Lean lab; AI wrote the Lean code. Each statement was copied verbatim from the lab file and compiled against Mathlib, and an independent AI read-back of every item is attached for checking; the lab's owner submitted it without a separate line-by-line human audit. No proof is supplied here.
MuSig2 (BIP327) lets signers produce one BIP340 Schnorr signature for an aggregate key, indistinguishable on chain from a single-signer Taproot spend; FROST does the same for a threshold of signers. The correctness claim is that partial signatures which each pass their partial check combine into a signature that the ordinary Schnorr verifier accepts. Earlier this was judged infeasible here: the signature mission's secp256k1 is an executable transcription without a proof of the group law. This mission supplies that proof, by connecting the executable curve to Mathlib's elliptic-curve group, and then proves MuSig2 correctness end to end against the executable schnorrVerify, and FROST correctness in the group.
toPoint_padd, valid_padd, tp_padd, valid_pmul, tp_pmul, toPoint_pneg, eq_of_tp_eq, padd_comm, padd_assoc, pmul_add, pmul_padd, pmul_pmul, tp_G): the executable point addition, negation and scalar ladder are Mathlib's group operations on over ; hence they are associative, commutative and linear.n_prime, n_nsmul_Gpt, nsmul_Gpt_mem, addOrderOf_Gpt): and are prime (Lucas–Pratt certificates checked by the kernel) and the generator has order exactly .cpoint_spec, cpoint_cbytes): compressed points parse to reduced curve points and round-trip.musig2_partialSigAgg, musig2_sign_partialSigVerify, musig2_correct, musig2_partialSigAgg_secp256k1, partialSigAgg_schnorrVerify, the goal): the aggregation algebra in any module and on secp256k1, and the end-to-end statement that BIP327's PartialSigAgg of partial signatures that pass PartialSigVerifyInternal is a signature schnorrVerify accepts for the aggregate x-only key, with key aggregation coefficients, plain and x-only tweaks, and the parity negations of the BIP.lagrange_interpolate_zero, frost_partialSigAgg, frost_sign_partialVerify, frost_correct, frost_correct_secp256k1): Lagrange interpolation at 0 and the aggregation of shares into a Schnorr signature for the group key, in any ZMod n-module and on secp256k1.Correctness only, not security: nothing is claimed about unforgeability or the hardness of discrete logarithms. The end-to-end theorem assumes each signer key has order dividing (true of every secp256k1 point because the group has prime order, but proving needs point counting; for keys of the form it is discharged by nsmul_Gpt_mem), and that the aggregate nonce is not the point at infinity, where BIP327 substitutes and honest partial signatures no longer combine. FROST is proved in the group only: there is no executable FROST transcription. (BIP327, RFC 9591)
Miniscript is the structured subset of Bitcoin Script that wallets use to write and analyse spending policies: each fragment has a fixed translation to Script, a type that says what it does to the stack, and a satisfaction table that says which witnesses make it succeed. The claim that makes it trustworthy is compiler correctness: a well-typed Miniscript compiles to a script that the consensus interpreter accepts on exactly the witnesses the satisfaction table describes. This mission proves the soundness half of that claim against the script interpreter transcribed from Bitcoin Core.
runSeq_append, run_eq_runSeq, evalScript_eq_runSeq, compile_skip): the interpreter's loop composes, and a well-typed fragment inside a non-executing branch is inert.sem_consumes, goodVal_of_sem, goodVal_of_semW, sem_V_nil, sem_K_shape, typeOf_sound): the semantics respects the types and the z/o modifiers, B and W fragments leave valid script numbers, and the decidable checker is sound.sem_sound, semW_sound, sat_sound, dsat_sound, satV_sound, sat_spends, the goal): for every well-typed fragment over 23 constructors (all hash and time-lock leaves, pk_k, pk_h, multi, the and/or combinators, the seven wrappers), a satisfying witness makes the compiled script leave a true value above the untouched stack, a dissatisfaction leaves the empty element, a V satisfaction leaves nothing; and a satisfaction of a top-level B spends.compile_length, opsIn_compile_le): script size and counted opcodes are bounded by syntactic measures, which carry the theorems' operation and stack hypotheses.Soundness only: the converse ("nothing else succeeds") and the malleability analysis (the s, f, e properties, non-malleable satisfactions) are not proved. thresh is not in the fragment set, and v: appends an explicit OP_VERIFY instead of folding into a preceding *VERIFY opcode, which changes script bytes but not behaviour. The signature checks are the abstract oracle's. (Miniscript, miniscript.h)
The backbone mission proved chain growth, common prefix and chain quality for every typical execution: one in which, on every window of at least rounds, the adversary finds fewer blocks than there are uniquely successful honest rounds. Garay, Kiayias and Leonardos show that under honest majority executions are typical except with probability exponentially small in . This mission proves that half: the random mining process, its expectations, Hoeffding concentration per window, the union bound, and the end-to-end statement that every consequence of typicality holds with probability at least , against any adversary strategy.
iIndepFun_rounds, map_eval_P): independent rounds, each a product of independent Bernoulli() queries, honest and adversarial.integral_round*, expect_X, expect_Y, expect_Z, expect_Y_sub_expect_Z, margin_ge_of_honest_majority, expect_Z_add_le_expect_Y, expect_Z_lt_expect_Y): , , , and with and the margin is at least .sets_hoeffding, window_bound, window_bound_rate): a window of rounds fails the typicality inequality with probability at most .typicalOn_failure_le_of_window, typicalOn_failure_le, typicalOn_prob_ge, typical_toExecution_iff, typicalTrunc_failure_le): on a horizon of rounds, typicality fails with probability at most , independently of the network and of the adversary's chain choices.backbone_failure_le, backbone_prob_ge, the goal): any property implied by legality and typicality, in particular the backbone mission's common prefix, chain growth and chain quality, holds for every adversary strategy with that probability.The bound is Hoeffding's, with each round's difference ranging over values, not the paper's multiplicative Chernoff bounds (absent from Mathlib), so the rate is weak when is large and small; the window conditions , are sufficient conditions chosen for clean statements. The execution is frozen after the horizon (party 0 mines alone, the adversary finds nothing) so that the deterministic theorems apply to infinite executions. The paper's separate bounds on are not proved; the deterministic layer does not need them. The common-prefix instance is a one-line composition left out of the public theorems because a split file cannot import another mission's solution. (ePrint 2014/765)
At the pinned revision, Bitcoin Core's cluster mempool replaced BIP125 rule 3 ("the replacement's feerate must exceed every conflict's") with a single check: the replacement must strictly improve the feerate diagram of the affected clusters. The replace-by-fee mission had to take rule 3 from v29.0 for that reason. This mission transcribes the actual check (FeeFrac, CompareChunks, ImprovesFeerateDiagram), proves that Core's sweep computes the mathematical comparison of the two diagrams, and connects it to the existing no-free-relay theorems.
byRatio_eq_compare_ratio, byRatio_lt_iff, div_round_down_eq_floor, div_round_up_eq_ceil, mulFallback_value, divFallback_eq_div, evaluateFeeDown_eq_floor, evaluateFeeUp_eq_ceil, getFee_eq_evaluateFeeUp): Core's cross-multiplied comparison is the comparison of exact ratios; its divisions round as named on both code paths; the replacement mission's GetFee is EvaluateFeeUp.diagram_at_zero, diagram_total, diagram_concave): starts at the origin, ends at the total fee, and is concave for chunkings with non-increasing feerates.compare_chunks_sound, improvesFeerateDiagram_iff): CompareChunks returns greater, less, equivalent or unordered exactly according to the pointwise comparison of the two piecewise-linear functions; ImprovesFeerateDiagram is "strictly better".improves_total_fee, improves_total_fee_not_strict, no_free_relay_diagram, the goal): a strict improvement never lowers the total fee but need not raise it, and together with PaysForRBF the replacement adds at least the incremental relay fee: no free relay holds under the pinned revision's actual rules.All eleven CompareChunks cases of Core's rbf_tests.cpp, the FeeFrac arithmetic cases of feefrac_tests.cpp (including the fast-path thresholds and issue #32294), and hand-computed diagrams agree (tests/FeerateDiagramVectors.lean).
The chunk lists are input: the linearization of the affected clusters (txmempool.cpp, txgraph.cpp) is not modelled, nor which transactions belong to the clusters; no_free_relay_diagram relates the diagrams to a Replacement by a hypothesis on total fees. Fees and sizes are unbounded integers. (feefrac.cpp, rbf.cpp)
Eyal and Sirer's relative revenue is computed from the stationary distribution of their Markov chain, and the threshold result is read as "a pool above the threshold earns more than its share over time". The selfish-mining missions proved the formula for the stationary distribution, its uniqueness, and the threshold as statements about that distribution. This mission proves the time statement: started from no lead (or from any distribution), the chain's time-averaged occupation converges to the stationary distribution, the pool's realized revenue share converges to the paper's formula, and above the threshold it eventually exceeds the pool's hashrate.
dist_* step equations, dist_mass, dist_summable_lead, dist_nonneg, isDist_dist, isDist_distN, dist_stationary, distN_stationary, isDist_delta, le_one_of_isDist, distN_mix): one step of the chain as an operator on distributions, preserving distributions, with the stationary distribution as a fixed point.distN_zero_lead_le, distN_delta_lead_le): from any start, the probability of a long private lead is bounded geometrically, uniformly in time.cesaro_delta_tendsto, cesaro_zero_tendsto, cesaro_tendsto): the average occupation of every state over the first steps converges to the stationary distribution, from any initial distribution. The proof uses the uniqueness mission: limit points are invariant with mass 1.avgPoolGain_eq, avgOthersGain_eq, avgPoolGain_tendsto, avgOthersGain_tendsto, avgRelativeRevenue_tendsto, the goal; avgRelativeRevenue_eventually_gt): the time-averaged revenues converge to the paper's rates and the realized share to the relative revenue; above the pool's realized share eventually exceeds .firstReturn_zero, last_exit, renewal_equation): the last-exit decomposition and the renewal equation for returns to zero, with an aperiodic return-time distribution.Convergence is in Cesàro mean, which is what a long-run revenue share needs. Pointwise convergence of the -step distributions (which holds, the chain being aperiodic) is not proved; the renewal equation is the first step towards it. "Revenue" is the expected number of credited blocks; almost-sure convergence of the realized share along a single run is not stated. (arXiv:1311.0243)
The script mission's interpreter, reviewed twice and tested against Core's 994 vectors, is exact except at two documented limits: L1, the signature script code does not restart after an executed OP_CODESEPARATOR (a handful of historical transactions), and L10, OP_CHECKMULTISIG deletes only the checked signature from the script code instead of all of them (constructed test cases). Those nine vectors disagreed. This mission closes both limits with a second interpreter that tracks Core's pbegincodehash and performs Core's FindAndDeletes itself, and proves that the two interpreters agree wherever the limits do not bite, so that every published theorem about verifyScript carries over unchanged to the exact rule.
stepV2_codesep, stepV2_keeps, codesep_tracks): after an executed OP_CODESEPARATOR at byte position the script code is the script from ; nothing else changes it.checksig_deletes_one, fadAll_base, fadAll_witness, multisigSigs_eq, multisig_deletes_all): OP_CHECKSIG checks against the code with its own signature deleted; OP_CHECKMULTISIG against the code with all its signatures deleted, before any check, in SigVersion::BASE only.legacyOracle_eq, annotate_parse, annotate_suffix, annotate_op_suffix, stepV2_agree, eval_agree, evalBytes_agree, runOk_of_static, runOk_witness, evalOk_of_static, evalOk_witness, verify_agree, the goal): under the side condition that no executed OP_CODESEPARATOR and no multisig self-signature push occurs (statically implied by the absence of the two opcodes; in witness v0 only the separator matters), verifyScriptV2 = verifyScript.verifyScriptV2 agrees with Core on all 793 script tests and all 201 transaction tests of the pinned revision; the nine cases that disagreed with the published interpreter (seven L1, two L10) now agree, and no previously agreeing case changed (tests/CoreV2*.lean, REVIEW_V2.md).
The side condition for L10 is semantic (it depends on the signatures actually on the stack), so EvalOk is stated along the run, with static sufficient conditions. Policy flags (CONST_SCRIPTCODE and the rest) remain off as in the published model; the Taproot handler is unchanged. (interpreter.cpp)
Lightning's security against a counterparty who broadcasts an old, revoked commitment transaction rests on the penalty: the honest party, who holds the revocation secret for that commitment, can take every output at once, while the cheater can take nothing before to_self_delay blocks. The script missions proved what each commitment output's script enforces; this mission puts the pieces together at the script level, output by output, in both directions.
to_local_penalty_sig, to_local_penalty, the four HTLC penalty theorems, revoked_commitment_penalty, the goal): if the oracle accepts a signature for the revocation key, every penalisable output of the commitment transaction (to_local, offered and received HTLCs, legacy and anchors forms) has a witness VerifyScript accepts, with no delay and no condition on the spending transaction. to_remote_honest_only and the two anchor theorems state the facts for the outputs that have no revocation path.to_local_cheater_delayed, cheater_delay_in_tx_terms, cheater_delay_any_sequence, cheater_needs_delay, the four *_cheater_no_revocation theorems, htlc_cheater_one_block_anchors, received_cheater_height): if the oracle accepts no signature for the revocation key and knows no other preimage of its hash, every spend the cheater can make takes a non-revocation path: the balance only after to_self_delay (version 2, nSequence ≥ to_self_delay), the HTLCs only by preimage, success or timeout, with the one-block delay in the anchors form and the expiry bound for timeouts.penalty_any_block): the penalty transaction is final in any block, so the honest party wins whenever it confirms within the delay.The hypotheses are unforgeability stated on the oracle for one key (NoRevocationSig) and second-preimage resistance of hash160 for the revocation hash (NoRevHashPreimage); there is no model of key derivation (BOLT #3's per-commitment secrets), no signing oracle, no ECDSA security proof, and no network or fee model. The BIP68 consequence of nSequence ≥ to_self_delay (the cheater's transaction cannot enter a block within the delay) is stated in transaction terms, not composed with the block mission's sequence-lock check. The legacy (P2WPKH) to_remote has no published theorem and is not covered. (BOLT #5)
A Monte Carlo price estimate averages discounted payoffs over simulated scenarios. Its statistical error can be assessed from the variation of those payoffs. When a continuous-time stochastic model is replaced by a finite time grid, a second error enters: the simulated distribution differs from the model distribution. Increasing the number of scenarios does not remove that bias at a fixed grid. Broadie and Kaya address this problem for stochastic volatility by constructing samples of terminal stock price and variance from their joint law. Their published paper develops the Heston construction first and then considers jump extensions and pricing applications. This mission concerns the complete Heston construction of §3 and its unbiased-pricing consequence.
The Heston model describes a stock price and its instantaneous variance . Under the risk-neutral probability measure they solve
Here and are independent standard Brownian motions. The real number is the risk-neutral drift, is the speed of mean reversion, is the long-run variance, and is the volatility of variance. The correlation ranges over the closed interval . These are the dynamics in (1)–(2), p. 218.
Fix arbitrary deterministic times , write , and start at with and . The processes are continuous and adapted, with stochastic integrals interpreted locally in the Itô sense. The integrated variance is . The dimension parameter is any positive real number. The regime in which variance can reach zero remains in scope; the condition is not imposed.
The main target is equality of the joint laws of the original SDE and the paper's explicit ideal sampler:
For random starting states, this is an almost-everywhere equality of conditional probability measures given . The sampler is defined independently: it draws a scaled real-degree noncentral chi-square variance, uses the explicit continued characteristic function and Fourier inverse CDF for integrated variance conditional on that sampled variance, recovers the first Brownian integral algebraically, and uses an independent standard Gaussian for the stock draw. This is the four-step algorithm and its completion in §3.3.
For any measurable payoff on the two terminal coordinates, put and . Independent sampler repetitions give the ordinary empirical average . Whenever is absolutely integrable, the target includes
For nonnegative payoffs, expectation equality is also stated with possibly infinite values. If has a finite second moment, write . Then
Under the fixed per-path cost convention , , the latter equals . The asymptotic rate is , with the explicit coefficient fixed independently of sample count. This is the §1 cost convention and p. 219 standard-error identity. It is not a claim about the bit complexity of special-function evaluation.
Seven source displays supply the milestones: the stock exponential representation (6); the scaled noncentral chi-square transition law (8)–(9); the squared Bessel bridge transform (39); the square-root bridge Laplace transform (40); its characteristic-function counterpart (13); both Fourier inversion equalities (14); and Brownian-integral recovery (23). Each retains its coefficients and full parameter domain.
Equality of joint laws makes the pricing result applicable to payoffs depending on both terminal stock and terminal variance, a scope expressly described in §8. It also separates the assumptions needed for different conclusions: exact simulation is distributional, unbiased real-valued pricing needs an absolute first moment, and the RMS formula needs a second moment. These distinctions matter for unbounded payoffs.
The paper establishes these results mathematically. This mission supplies open Lean statements and concrete definitions for formalizing them; it does not claim that their proofs have already been checked. The reusable contributions include real-degree noncentral chi-square sampling, continuous endpoint bridge semantics, and a complex Bessel ratio that retains its branch and boundary conventions. The local Itô-integral foundation is reused from a published definition.
Knowing the marginal laws of terminal variance and integrated variance is insufficient. They are dependent, and the stock formula uses that dependence. Replacing the bridge draw by an independent marginal draw changes the joint law. Similarly, the conditional normal expression for the stock does not by itself prove that the inputs to that expression have the required distribution.
The characteristic expression (13) contains a modified Bessel function at a complex argument. The source explicitly requires continuation between branches in (22). Principal-branch evaluation alone can introduce a discontinuity. Zero variance endpoints create another difficulty: the raw numerator and denominator can both vanish or diverge, while their ratio has a meaningful continuous extension. Finally, Fourier inversion must establish a genuine continuous CDF and a valid inverse-transform draw; these properties cannot be supplied as premises.
The original processes are defined by SDE integral equations on a usual filtered probability space. The published local Itô relation uses bounded predictable approximations and convergence in probability, without requiring global expected squared energy. The generic square-root processes are separate from the paper-specific multiplicative stock model. Neither definition contains a terminal distribution or sampler-correctness field.
Conditional laws at random states use regular conditional distributions almost everywhere. For deterministic endpoints, bridge laws are specified by weak limits of conditioning on shrinking positive-width terminal observation windows. Their existence is asserted in the bridge theorems. The Bessel quotient cancels the common endpoint power through the entire factor from (21); the continued logarithm tracks the frequency path. Both infinite Fourier integrals are represented by limits of truncated integrals, and quantile well-definedness is part of the inversion conclusion.
The sampler uses ideal real and complex operations. The finite trapezoidal sum and numerical tolerance discussion in §3.2 describe an approximation to that ideal construction. They are not an exact finite-precision implementation. Jump-model extensions, conditional variance reduction, Greeks, and forward-start pricing are separate results outside this mission's selected goal. Proof contributions can develop the stochastic, analytic, or probability-measure foundations without changing the selected statements or their domains.
A retailer must learn demand while selling a fixed stock over a finite season. A high price preserves inventory but may leave profitable sales unrealized. A low price can exhaust stock before later customers arrive. Learning is harder when some customers behave unlike the population whose demand the retailer wants to learn. Those customers can arrive in a concentrated block and can adapt to what has already happened. The problem studied by Chen and Wang asks for pricing rules whose revenue loss remains controlled without knowing the number of these outliers or whether inventory will bind at the unconstrained optimal price.
This mission concerns the paper's modular general-inventory result. Its inputs are two pricing policies with guarantees in the two opposite inventory regimes. Its target is the guarantee claimed for the particular randomized meta-policy that combines them. The input guarantees remain assumptions, rather than being replaced by guarantees for a specially chosen pair of implementations.
There are T selling periods and real initial inventory , where . Prices lie in a compact nonnegative interval . The unknown typical demand curve decreases strictly from 1 to 0 across that interval. The curve and its inverse satisfy the two-sided Lipschitz assumptions printed in the paper. The demand-coordinate revenue, , is twice continuously differentiable on , with .
An adaptive adversary chooses whether each customer is an outlier and, if so, a measurable alternative demand curve into . These choices can use the full past of prices, sales, demand curves and outlier indicators. They precede the current price decision. The seller sees only earlier prices and sales, together with its own private randomness. The total number of outliers is at most almost surely for every policy. A fixed positive α satisfies . The seller does not receive ε, α, the typical curve, or the true inventory regime.
At a chosen price, sales are demand plus noise censored by the remaining physical stock. Sales belong to , and revenue is price times actual sales. Noise has mean zero conditional on the current price, as stated in §3; independence across periods and mean zero conditional on the entire history are not assumed.
The clearance price is , and the unconstrained revenue optimum maximizes over the continuous interval. The typical-demand fluid benchmark is
Regret is minus expected cumulative actual revenue. The expectation includes both seller randomization and customer randomness. The model and inventory rate stay fixed as T grows.
The supporting targets, in proof-use order, are the e-companion's Lemma EC.4, its Lemma EC.3, main-text Lemma 5, and Corollary EC.1. The first is the uniform martingale inequality
The next bounds the error in a sampled fixed-price demand average, using the corruption count within the selected periods and positive stock at their beginnings. Lemma 5 gives both simultaneous exploration-estimate errors, with every printed constant and its full expression. Corollary EC.1 asserts
with probability under its printed parameter and polynomial-threshold conditions.
The goal is Theorem 4, covering both strict regimes and . If the two supplied policies have their respective uniform regret guarantees, then the specified Algorithm 5 satisfies
for sufficiently large T. The absolute subroutine corruption budget is εT. The excluded equality case stays excluded. The polynomial parameter dependence and logarithmic factors are represented with constants and degrees chosen before horizons, contamination levels and environments.
The target transfers guarantees for policies that know their applicable inventory regime into a guarantee for the paper's specified combination. Its operational definitions separate reusable randomized observed-history policies from the pricing model, real inventory dynamics, exploration estimator and meta-policy. This makes the meaning of actual revenue and the seller's information available for inspection independently of any proof.
The source presents these results with proofs, but this mission supplies open Lean statements rather than completed machine-checked proofs. Source findings are retained separately: the printed exploration normalization admits a counterexample to Lemma 5, and the stated price-conditioned noise assumption admits a counterexample to Lemma EC.3. Those claims remain exactly the targets to prove or disprove; they are not silently replaced by corrected versions. Corollary EC.1 also retains a printed maximum whose use in the proof needs scrutiny.
Exploration competes with revenue collection for the same physical inventory. A successful estimate obtained after stock has been depleted cannot restore the lost opportunity. Outliers can cluster early, and the two input policies need different conditions to make their guarantees applicable. Neither the regime estimates nor successful exploration can be assumed in a faithful statement. The distinction between conditioning noise on price and conditioning it on the whole past is also consequential: the latter would impose a stronger statistical model than the paper prints.
All prices, sales and stock quantities are real. Time is indexed by elapsed periods starting at zero. The general policy interface takes only public initialization data, private randomness and observed price/sales history. Environment randomness ranges over arbitrary measurable spaces and is independent of the private tape; its response may depend on the current price. The almost-sure budget is required for every admissible policy. Measurability and integrability make expectations meaningful, without bounding uncensored noise.
Algorithm 4 uses the endpoint-inclusive grid and the printed estimate , with . Ties use the lowest index. Pricing outside a selected exploration set uses a separate private tape, preserving fresh exploration draws. Algorithm 5 samples a private epoch schedule, uses its realized cardinality for the grid, and interleaves exploration with the selected input policy. The prior epoch's observations determine the next branch. Each subroutine receives the nominal epoch horizon and nominal stock allocation; its history advances only on its assigned periods. The nominal quota is checked between selling periods to determine subsequent prices; individual sales are censored by actual global stock, which is shared and never reset.
The source omits zero/singleton-grid behavior despite giving those events positive probability. The explicit completion returns the lower endpoint for both estimates and uses the lower price on a singleton grid. No event is excluded from the goal. Theorems 1–3 and the independent lower-bound Theorem 5 are outside this mission's dependency scope. The meta-policy's regret guarantee occurs only in the goal conclusion, never in its definition or an algorithm-validity assumption.
opre.2022.2280.sm1.pdf, ec9–ec10 and ec13–ec17. Both pinned local PDFs belong to this single citation family.A linear optimization model can prescribe a decision that uses nearly all available capacity. If the coefficients measuring resource consumption are uncertain, even a small change can make that decision infeasible. Protecting against every simultaneous adverse change can instead sacrifice a substantial amount of the nominal objective. Budgeted robustness introduces a parameter controlling how many coefficients receive simultaneous protection. Bertsimas and Sim study this tradeoff in The Price of Robustness. This mission follows their authors' preprint, dated August 2001 and revised August 2002, whose pages and theorem numbers differ from the later journal publication.
The question is how a deterministic protection budget translates into a probability bound when the uncertain coefficients have independent symmetric distributions. The selected result is the complete Theorem 3, including its equality case, explicit analytic envelope, and normal limit. The source claims are the targets; concrete defects in the source's optimizer normalization are disclosed below.
A nominal linear program chooses a real vector to maximize , subject to and . Coordinates of may have either sign. In row , the finite set identifies uncertain entries. Each such entry has a nonnegative deviation radius and is realized as
The row noise consists of measurable real random variables in , each with the same distribution as its negative. Independence is mutual within the row. Different rows need not be independent, and neither densities nor identical distributions are required. Entries outside remain deterministic.
For each row choose a real protection budget . The robust program introduces and requires
Its objective remains . An optimal decision has a feasible extension and an objective at least as large as every feasible extension's objective. This definition does not presume that every input problem has an optimum.
Fix an optimal and write . Below full budget, a protection maximizer is any pair , with maximizing
Choose any minimum-weight index . The source defines on and outside . At full budget use and throughout the row. These definitions come from the preprint's model and Proposition 2, pp. 6–8.
The sole milestone is Proposition 2(a)–(b), p. 8. It asserts both
For the goal, put , , , and . Define
Theorem 3(a)–(d), pp. 10–11, consists of four separately quantified claims:
where and, for ,
with the standard normal cumulative distribution function.
These are the exact constants and endpoints of Eqs. (16)–(20). The last two assertions do not require an optimization instance or a probability-space construction.
The formulas express the source's proposed relationship between protection and reliability, with an equality regime that makes the meaning of “tight” precise. The analytic envelope addresses evaluation of large binomial sums, while the limit identifies square-root scaling of the protection budget. Together they distinguish an exact finite-dimensional claim from a computational approximation.
The source normalization has a concrete defect. With weights and budget , the maximizing pair , is permitted because the fractional coefficient vanishes. It gives and . A robust LP realizing these weights is feasible and optimal with , , , , and . Independent fair signs then give a normalized-tail probability , exceeding . This contradicts Proposition 2(b) and the inherited-coefficient reading of Theorem 3(a). The strict original-constraint violation probability is instead . The targets retain the source claims, making disproof a meaningful possible outcome.
The dependence of the normalization on arbitrary maximizing choices cannot be replaced by a presumed coefficient bound: doing so removes the counterexample. Integer budgets are especially sensitive because the extra index contributes nothing to the protection objective. Zero weights also make the printed quotient undefined. Separately, the appendix's claimed equivalence of integer-floor and nonintegral binomial thresholds fails, although that failure does not refute the limit itself. These findings concern Proposition 2 and the appendix, pp. 8–9 and 29–33, and are recorded with numerical evidence in the mission's insight record.
The general box-constrained LP is separate from the paper-specific robust model. Finite indices use Fin; arbitrary measurable probability spaces and Mathlib's mutual independence and Gaussian measure preserve continuous and discrete laws. Definitions contain no assumed probability bound. The two theorems are statements awaiting proof or disproof; a successful build checks their types, not their truth.
All maximizing pairs and minimizing indices remain quantified. Optional indices handle full budget and empty rows. Real division explicitly extends an undefined zero-denominator quotient by zero without removing any input. Model U is represented by , agreeing with its normalization at positive radii and retaining deterministic zero-radius entries without division. The fractional coordinate in Eq. (5) is read as the designated extra coordinate, following Eq. (9). Binomial thresholds use integer floors. The limit is stated for all real , disclosing its extension beyond the positive eventual-budget regime. The LP-equivalence, sensitivity, correlated-data and application results are outside this mission. No theorem clause is replaced by an approximation.
63f0bffaff9128b706a084acc869e1020ce79adf86108ac23b5b0dd598f189cb. Associated publication: Operations Research 52(1), 2004, 35–53, DOI. All numbered citations above use the preprint, whose PDF and printed page numbers coincide; the DOI identifies the later publication.Retailers sometimes offer a discount on a game only after a customer buys a console. Such add-on discounts let the customer choose individual additional products while the retailer controls both the original prices and the conditional offers. A retailer with limited transaction history must learn purchase probabilities while choosing these prices. Offering discounts on only a limited number of products adds a selection decision to the pricing problem. Simchi-Levi, Sun and Zhang study this joint learning and optimization problem in arXiv:2005.00947v1. This mission concerns their UCB-Add-On regret theorem and the five supporting lemmas used in its argument.
A retailer has core products, numbered by a positive integer , and supportive products, numbered by a positive integer . Core prices belong to a finite nonempty menu . Original supportive prices belong to , and discounted supportive prices belong to . All prices are nonnegative real numbers. There is no rational-grid assumption. The nonnegative integer limits the number of discounted supportive products; it may be zero or exceed .
A policy specifies a core price for each core product, an original price and discount price for each supportive product, and a Boolean selection . Feasibility means and for every supportive product, including those not selected. The operational problem has at least one feasible policy.
The demand tables are arbitrary fixed functions with values in . The mean primary purchases are for core products and for supportive products. Each core purchase creates an opportunity to buy each supportive product, with mean when selected and otherwise. Fresh primary purchases are independent Bernoulli observations; conditional on those purchases, the add-on opportunities receive independent Bernoulli observations. A period can contain any number of core purchases from zero to . There is no inventory depletion or assumption that a customer selects at most one core product.
The expected revenue is
The benchmark is the attained maximum over the feasible policies in equation (1). The same polynomial evaluates an algorithm output even if the printed procedure produces a tuple that fails the unconditional discount-price constraint.
Algorithm 1 optimizes supportive revenue at demand grid points, ranks the benefit of offering each discount, rounds core demand to the nearest multiple of , and recovers maximizing policies from a backward dynamic program. Algorithm 2 estimates all four parameter families. Primary counters count periods; add-on counters count core-purchase opportunities. At episode start , each positive-count upper confidence bound is , with the corresponding empirical mean for each family. Algorithm 1 receives these estimates and . Its output is held until an associated counter doubles, including overshoots.
Define and . Let be the minimum probability of nonzero total primary demand over feasible policies, including primary supportive demand. Regret is the expectation of under the algorithm's own trajectory law.
The goal is Theorem 2, page 16, equation (7):
One positive absolute multiplier precedes the instance and . The eventual horizon threshold may depend on the instance and , but precedes every controller and tie choice. At the upper bound is infinite.
The milestones retain the source's use order: Lemma 4 bounds expected episode length by its starting time; Lemma 5 bounds total bad-event episode regret by a horizon-independent constant; Lemma 1 asserts the exact supportive Lipschitz constant ; Lemma 3 asserts actual-revenue approximation error at most ; Lemma 6 bounds good-event episode regret by a constant times both terms of the displayed rate. The independent offline FPTAS theorem and lower-bound remark are outside this mission.
The regret claim quantifies the cumulative cost of learning demand while computing approximate pricing decisions. Its displayed dependence distinguishes the number of products, the number of candidate prices, the price scale and the approximation input. Keeping these factors explicit prevents an instance-dependent asymptotic constant from hiding the central claim of Theorem 2.
The formalization supplies concrete declarations for the pricing model, both algorithms, the observation law and the source's claims. The six theorem declarations are statements awaiting proofs or disproofs. Compiling them does not establish the printed results. In particular, the literal supportive subproblem has a counterexample to its claimed Lipschitz constant, and other source discrepancies require careful separation from the intended analysis.
Feedback for supportive add-on demand arrives only when a core purchase creates an opportunity. Those counts can remain zero even when total primary demand is always positive. Episode lengths and the histories at which confidence events are tested are random. Replacing this feedback by a policy-level reward observation changes the learning problem.
The source also leaves initialization and zero-start doubling unspecified. Its displayed bad event uses without the square root in the algorithm. Equation (3) reverses the strict price inequality used in equation (1), while Algorithm 1's ordinary branch can select an original price with no smaller discount available. These issues are retained explicitly; a corrected algorithm or corrected lemma would be a separate result. In particular, completing an unseen profitable core price with UCB zero can leave it unexplored forever and give linear regret. The universal-completion targets include this case; the initialization insight records the explicit two-price example.
Finite menus use injective real-valued labels and products use finite index types. Demand values zero and one are included. All rounding and maximizing ties are admitted. The generic probability-mass object is Mathlib's PMF; the paper-specific controller uses distributions on finite policy tuples and post-observation stopping probabilities. Recursively multiplied finite kernels define every finite-horizon expectation. No concentration, optimism, approximation error or regret inequality is included in a run condition.
Undefined zero-count UCB branches range over all causal values in . Undefined zero-start stopping branches range over all causal almost surely finite positive completions, while every defined positive-count doubling stop is enforced. These are declared generalizations, not a favorable initialization convention. The bad event likewise includes every history-determined Boolean completion at zero counts. Its positive-count radius remains literal. Event contributions use indicator weighting at the actual episode-start history and truncate the final episode; full conditional episode length uses an extended nonnegative tail sum.
The printed supportive maximum has its own feasible set and nonemptiness condition. Operational benchmark feasibility is separate. This separation keeps the reversed-price counterexample expressible without imposing it on the online model. The concrete definitions support future proof and disproof work without assuming any of the target bounds.
A seller choosing prices may learn about demand from purchases while earning revenue from those same purchases. The hidden customer characteristic can range continuously, even when there are only a few prices and observations. A policy must therefore trade off present reward and information that affects later decisions. Describing every possible belief about a continuous parameter makes a direct dynamic program difficult to represent.
Hao Zhang's Dynamic Learning and Decision Making via Basis Weight Vectors studies a different representation: the reward of a continuation policy as a function of the hidden parameter. The exact result in Section 4.1 states that polynomial primitives permit the relevant family of these functions to be recovered through operations on finite coefficient vectors. This mission concerns that exact result, including its whole efficient frontier at every period.
A parameter is selected before a horizon of decision periods and stays fixed. At each period an agent chooses an action from a finite nonempty set and receives a signal from a finite nonempty set . Conditional on action and the parameter, signal has probability . These probabilities are nonnegative and sum to one. The associated reward is real and may be unobserved. The discount factor satisfies .
A continuation policy is a finite tree whose root chooses an action and whose child is selected by the next signal. Its choices never observe . Its continuation-value function is its expected discounted reward conditional on that fixed parameter. A terminal continuation function supplies the boundary value. A finite efficient family of terminal functions is also permitted, covering the soft termination described in assumption (A2).
The positive-normal extreme frontier, written , retains strictly exposed members of a finite set. For vectors in , an exposing normal has nonnegative coordinates summing to one. It must give its chosen member a strictly larger inner product than every distinct competitor. For functions on , normals are all nonnegative square-integrable densities with integral one, and the comparison is . The two spaces have different families of normals.
The basis-weight representation uses monomials . A weight represents . Coefficients may be negative, even for a nonnegative probability function. Weight addition uses zero padding, and is ordinary coefficient convolution. Assumption (A1) supplies weights for every probability and reward function. Assumption (A2) supplies weights for every terminal frontier member.
The three supporting statements are Lemma 1, Corollary 1 and Lemma 3. The first retains both algebraic identities, including unequal vector lengths:
The second identifies expected-reward weights:
Here .
For a finite weight set and a nonnegative basis family, Lemma 3 says that every member of is represented by a member of , and
The goal is Theorem 1. Initialize . For every and every , compute
Then the independently defined function recursion of Eqs. (7)–(9) is recovered exactly:
Every period and action is retained. The terminal function family and terminal weight family are the prescribed boundary data. There is no approximation constant or degree truncation.
The result replaces the manipulation of continuation functions with finite coefficient arithmetic while preserving the complete frontier relevant to density normals. It concerns an entire family of policies and priors, rather than a value for a single selected prior. The polynomial degree and number of candidate vectors can still grow; exact representability does not assert inexpensive computation. The source's approximation methods and empirical comparisons are separate from this claim (Zhang, Sections 4.3–5.6).
Formalization makes the two exposure notions, the information restriction on policies, and the terminal boundary explicit. The theorem declarations are proof targets; their compilation checks their types and definitions, not the validity of the asserted results. A completed development would provide checked algebraic and geometric statements for this representation.
Exact coefficient arithmetic alone does not establish the theorem. A coefficient vector can be exposed by a simplex normal while its evaluated function is dominated on the parameter interval. The paper illustrates this with the weights representing , and : every coordinate vector is exposed in coefficient space, but only the constant function survives function-space exposure. Consequently, the outer function-space PNEP in the recovery equality is essential (Zhang, p. 17, footnote 5).
The operational function recursion and the weight recursion are defined independently. Their agreement is a conclusion. Finite observations do not turn the hidden parameter into a finite state space, and probability nonnegativity does not imply coefficient nonnegativity.
The interval is a subtype of the reals with its Lebesgue measure. Function equality is pointwise on that interval. The weight type is the real polynomial type, which represents finitely supported coefficients modulo trailing zeros. Finite normalized normals are tested at a common degree bound for each set; the bound is unrestricted. Polynomial multiplication supplies convolution. All primitive and generated functions are square integrable, so the density comparisons use integrable products.
Natural-number indices count remaining decisions: zero is terminal, and is computed from . For a horizon , the source period is at the update indexed by . Lemma 3 permits arbitrary nonnegative L2 basis families, with independence interpreted in the source Hilbert space. The definition layer also includes policy trees, operational probabilities and rewards, terminal representations and both recursions.
Definition 4's component count is read as , consistent with its zero-based indexing and its preceding example. This reading is recorded in insight I1 and in theorem differences. Gaussian, exponential, multivariate and spline extensions, numerical performance, and proofs of the approximation methods are outside this mission. Insights I2 and I3 retain the source findings about excluded appendices.
An exercise decision can depend on today's observed state even when the evolution of that state depends on its history. Examples include deciding when to exercise an option whose reward depends on several asset prices or on earlier observations. A simulator can produce complete trajectories without providing the conditional distributions needed for a conventional dynamic programming calculation. Sturt studies an approach that uses those trajectories to select stopping policies. The present target concerns the exact structure of an optimizer of the resulting robust sample problem. It is a deterministic result about a fixed collection of paths, rather than a convergence assertion about the simulator. Sturt, §§2–3
A state is a vector in . A trajectory is a sequence of states over a positive number of periods. A measurable exercise policy specifies a Borel stopping region at every period. The system stops when its current state first belongs to the corresponding region. Thus
where an empty minimum means . The policy may change with time, but at each time its action uses only the current state. This definition does not assert that the stochastic process generating states is Markovian.
The reward is a finite nonnegative number depending on the stopping period and the entire original trajectory. Dependence on both past and future coordinates is allowed. The reward for never stopping is . The structural result requires no global bound or continuity of . These conventions are those of §2.1.
Fix a positive number of sample paths and a radius . The uncertainty box at period around sample is
Each box includes its boundary and contains its center, also when . The full path uncertainty set is the Cartesian product, with no added dependence constraint between periods. The robust sample reward and its average are
The adversary changes the input used by the stopping rule. The second argument of the reward remains the original sample . This is problem (RO) in §2.2.
Assign one period to each sample. Define a policy by the assigned stopping regions
Let be the family of all policies produced by these assignments. It has at most members; assignments can yield identical policies. Every region is a finite union of closed boxes and hence is Borel measurable. The goal is the complete statement of Theorem 4, p.16:
There is no approximation factor or error term. The comparison is against the entire class of admissible policies on .
Six source statements accompany this goal. Define terminal feasibility by . Lemma 1 equates the unrestricted supremum with the supremum over these policies. For a terminal-feasible policy, write . Lemma 2 gives the attained minimum
A pruned version has smaller stopping regions and preserves every earliest full-box stopping minimum. Lemma 3 asserts for each sample whenever is a pruned version of . For the assignment , Claim EC.6 asserts region inclusion, Claim EC.7 asserts equality of the full-box stopping minima, and Lemma 4 asserts the complete pruning relation. Both claims carry the terminal-feasibility and canonical-assignment preamble of Lemma 4. §3.2 and Appendix D, pp.16–17 and ec17–ec18
The original decision variable is a collection of arbitrary measurable subsets of a continuum. The theorem ensures that an exact optimizer can nevertheless be represented by finitely many period assignments. This is the structural basis for the paper's subsequent combinatorial formulations and algorithms. The finite representation depends on the observed samples and radius; it does not impose a predetermined parametric family on all potential instances. §3, pp.13–18
Sturt supplies mathematical proofs of these statements. The present formalization supplies concrete definitions and compilable targets for formal proofs. The seven research results remain to be proved in Lean. The definition layer also supplies a reusable measurable policy interface separate from this particular robust objective, along with explicit first-exercise and never-exercise conventions.
A finite nonempty family has a maximizer within that family, but this alone says nothing about policies outside it. The difficult comparison is with arbitrary Borel stopping regions. Shrinking such regions can change which periods an adversary can reach, so ordinary set inclusion does not by itself establish reward improvement. The full-box minima and the Cartesian structure of uncertainty are essential to the statements under consideration. Overlapping boxes, coincident samples, and contact at a box boundary all remain part of the problem. §3.2
Lean represents periods and samples by Fin T and Fin N: index represents source index . Positive and are part of the instance data. States are functions Fin d → ℝ, with their Borel measurable structure. The additional singleton state space at is admitted as a declared generalization. Finite rewards use nonnegative real numbers. An optional finite index represents a stopping time, with the absent index meaning infinity and yielding zero reward.
Infima, averages, and optimal values use nonnegative extended real numbers. Each sample reward is finite because its uncertainty set contains the sample and every reward is finite. More strongly, every possible sample payoff belongs to the finite set ; this supplies a common finite bound on all policy objectives. Thus the encoding introduces no infinite optimal value. Lemma 2 uses a least-element assertion, preserving the source's minimum attainment.
No optimization property is assumed in the model. The policy family is computed by the displayed union formula, and arbitrary comparison policies may continue forever. The model permits zero radius, zero rewards, duplicate paths, empty stopping regions, and rewards that distinguish trajectories with the same current state. The probability, density, and reward regularity assumptions of §2.4 concern separate convergence results and are absent here. Theorems beyond the selected dependency chain are outside this mission's scope. Formal proofs of the stated targets, using the common definitions and finite-set, measurable-set, and order infrastructure, are the remaining contributions.
A chance constrained program chooses a decision before observing uncertainty and limits the probability that its constraints fail. For example, a service system can allow a prescribed fraction of demand realizations to exceed its available capacity. The optimization problem combines a cost objective with a probability requirement. Even when each realized constraint is convex in the decision, the probability requirement need not define a convex feasible region. This motivates tractable conservative approximations. Jiang and Xie compare two such approximations, ALSO-X and conditional value-at-risk, in arXiv:2012.04763v4, §§2–3.
The question here concerns the best objective value admitted by each exact approximation. A smaller value means that the approximation imposes less conservatism in the minimization problem. The source's phrase “better than” explicitly means “at least as good as,” so the target permits equality. It does not claim strict improvement on every instance or a guarantee for every numerical implementation.
Let the decision be and the uncertainty be , with an arbitrary probability law . A positive finite family of real random constraint functions defines
Every random section is measurable. On a common set of probability one, each function of the decision is convex and lower semicontinuous. The decision set is nonempty, closed and convex, and is contained in a closed pointed convex cone . The vector determines cost, while is the permitted violation probability. The original problem minimizes subject to and . These are the objects of A1–A2 and (1), pp. 1–2.
A real budget restricts decisions to . A functional slack is a measurable real function of the uncertainty; it is not a finite vector of sampled violations. The hinge-loss lower problem minimizes over , , and almost surely. Write for its complete set of optimal pairs.
The CVaR lower problem adds a real threshold . Its feasible triples satisfy and , almost surely, and its objective is
Write for its complete set of minimizers. These lower problems are the ones displayed in equations (7) and (13), not merely pointwise risk functions evaluated at a fixed decision.
Define the successful budget sets by
The goal is Theorem 1, p. 13: under A1–A2,
The comparison constant is exactly one and there is no additive tolerance.
The two milestones are the printed necessary-and-sufficient optimality characterizations in Appendix A.4, p. 42, in their source order. With , (KKT1) asserts that CVaR optimality is equivalent to the existence of multipliers satisfying
The corresponding hinge characterization (KKT2) asserts
Complementarity includes nonnegativity of both quantities and their zero product. Random equations hold almost surely. Both characterizations include multiplier existence and both directions of the equivalence.
The claimed ordering says that the exact ALSO-X formulation admits an objective value at least as favorable as the CVaR formulation under the stated convexity assumptions. It compares complete optimization models, including lower-level optimality and upper-level acceptance. It does not compare just the expected positive losses at one decision, nor does it quantify an approximation error relative to the original chance constrained optimum. The source treats algorithmic tolerance separately in Corollary 2, which is outside this mission.
Formalizing these claims also makes their domains and the distinction between feasibility and attainment explicit. The statement modules compile, but the three source claims have not been proved in Lean. Two source findings accompany the mission: (KKT1) lacks beta complementarity and is not sufficient, and the unqualified multiplier-existence assertion underlying (KKT2) fails at a boundary budget. These findings concern the printed claims and proof; they do not constitute a disproof of Theorem 1. The target statements retain the source claims so that their mathematical status remains visible.
The inclusion of the hinge lower problem among the CVaR choices at does not itself establish the desired outer-value ordering. The two upper levels use different acceptance conditions, and both require actual optimal lower-level decisions. A comparison of lower objective infima cannot replace those requirements. Infinite expectations and nonattained optima also require care under arbitrary laws and unbounded decision sets.
The source's KKT route introduces a further issue: A1–A2 do not provide the multiplier existence asserted on p. 42. The difficulty is therefore partly an audit of the source's stated reasoning, in addition to the construction of stochastic convex-analysis infrastructure. Adding a Slater assumption would change the requested theorem.
The development uses finite real coordinate spaces and Mathlib's convex cones and measure theory. Generic definitions of extended expectations, normal cones, subdifferentials and complementarity are separate from the paper's data and optimization models. The law of the measurable random vector encodes the original probability space without restricting its distribution to discrete samples. All positive finite counts of constraints are represented.
Outer values lie in the extended reals: the empty budget set has infimum , and an unbounded-below set has infimum . The nonnegative slack expectation is an extended integral. On the CVaR feasible set the objective is computed as , avoiding an undefined signed integral. Weighted signed expectations used in stationarity explicitly mark an infinite-positive-minus-infinite-negative expression as undefined; subgradients require a finite value at the candidate and inequalities on the defined domain.
A lower optimum means feasibility and comparison with every feasible competitor. Ties remain available for the existential upper-level choice. No global integrability, uniqueness, Slater condition, or certificate assumption is attached to the goal. The local A1–A2 wording controls over the global preamble's additional A3. Proofs, disproofs of the source milestones, and separately identified corrected variants can build on these definitions; a corrected variant does not replace a source target.
An inventory manager orders before seeing demand. Unsold stock incurs a holding cost, while unmet demand remains as a backlog and incurs a shortage cost. When the full demand distribution is unknown, a policy can be evaluated by its largest expected cost among distributions consistent with the available information. Dependence across periods matters because today's observation changes what is known about tomorrow. Xin and Goldberg study the case in which the conditional mean of the next demand equals the latest demand, and give an explicit optimal policy and a worst-case law against it (arXiv:1511.09437v2, §§2.2–2.3).
The target is their finite-horizon result, with its exact thresholds and value formula. Demand may have infinitely many possible rational values. Although the resulting policy uses only a small state, its benchmark includes every feasible deterministic policy depending on the entire observed demand history.
Fix a horizon , positive rational demand bound and backlog penalty , and rational initial stock and initial mean in . The holding cost per unit is one. Let . At period , a history policy chooses a rational post-order inventory level before demand is observed. It satisfies , , and at every history. The final inequality expresses nonnegative orders. Pre-order inventory may be negative, so backlogging remains part of the model.
The one-period cost is
There is no ordering cost or disposal decision. Write for the full class of these policies. For , let contain all probability laws on with mean , with arbitrary real probabilities and potentially countably infinite support. Let contain all laws of with and . Conditional restrictions apply at positive-probability histories.
The minimax value is the original optimization problem
This definition is separate from the Bellman recursion. With zero remaining periods the continuation value is zero; otherwise
The sets and are the actual feasible maximizing laws and minimizing stocks (pp.7–11).
The explicit thresholds use integer indices, including :
Empty products equal one. Set ; for positive , choose when . Define and
The proposed law is specified by equation (2.7). If lies in and , it interpolates between these two adjacent demand points to mean . If instead with , its atoms are , with upper-atom probability . At or , its atoms are , with upper-atom probability . Zero weights are allowed.
The goal retains all clauses of Theorem 3, p.13:
The recursively defined policy
is feasible and attains over the full history-policy class. The law with first marginal and subsequent conditional laws is an admissible martingale law and maximizes expected cost against this policy. Finally,
Only this last clause requires low initial stock. Fifteen supporting targets retain the independent-demand benchmark, analytical geometry, attainment, pasting and dynamic-programming verification statements from the source.
The result specifies both the inventory decisions and an adverse demand law, and connects their performance to the unrestricted minimax benchmark. The closed-form value applies in its stated initial-stock regime. These are separate claims: producing a two-point law or a stock threshold alone would not establish optimality in the original problem.
Formalization makes explicit the transition between the history-dependent model, the recursive optimization and the closed-form expressions. The present artifacts are theorem statements, not completed Lean proofs. They also retain printed supporting claims with documented source findings: Theorem 8's terminal singleton makes equation (7.34) false in a concrete two-period example, and Lemma 10's literal real endpoints conflict with the rational-support ambiguity class. Those claims remain available as disproof targets rather than being silently repaired.
The continuation cost changes geometry as demand crosses several thresholds. Convexity in the inventory decision does not give global convexity in demand. Restricting all competing laws to the two atoms of the proposed optimizer would change the problem. Likewise, allowing only Markov policies would remove part of the claimed comparison. Threshold ties, zero mean, maximal mean, backlogs and the one-period horizon all belong to the result (§3).
The development uses rational primitives and demand coordinates, real probability masses, countable sums, and unrestricted finite-history rules. Histories are reverse-order lists, with zero-based cost indices. Policies extend canonically by zero outside their valid history domain; this adds no restriction and makes equality in the uniqueness lemma precise. Analytical lemmas quantify over real intervals. Integer threshold indices preserve exactly. The stock index selects among all intervals for , including the final interval ending at ; at it equals .
Probability masses, history rules and conditional atom ratios form a separate reusable layer. The model, Bellman recursions, explicit formulas and induced policy/law constructions are distinct definitions. None assumes optimality or defines the minimax value by the proposed answer. Negative pre-order stock uses the same feasible actions as stock zero. The generic selector construction retains its printed first marginal at , while the explicit goal uses . Proofs and disproofs of these faithfully stated targets are the subsequent mathematical work.
A free-to-play multiplayer game earns subscription revenue only if players value the premium experience enough to pay for it. Yet converting free players into premium players also changes the experience of everyone else. Premium players may enjoy owning items that others lack, while free players may dislike comparisons with premium players. Advertising attracts new players, but its expense must be recovered during the game's finite lifespan. These interactions create a problem in which present revenue and future population growth respond to the same subscription price.
Mai and Hu (2022) study this interaction through a continuous-time model of social comparison, population growth, and operating profit. This mission concerns their main optimal-policy claim, Proposition 3, and its two numbered equilibrium dependencies, Lemmas 1 and 2. The target includes the full advertising and pricing trajectories in both unequal social-comparison regimes.
The market has total mass one. The active population is a fraction in , initially zero. Players receive a base utility . A premium player observing a free player receives a downward-comparison benefit , whereas a free player observing a premium player suffers an upward-comparison loss . Both parameters are positive and less than . Direct premium utility is normalized to zero, and the equality case is excluded, following the source.
If the premium share is , the subscription price rate is , and population is positive, free and premium utilities are
A stable premium share satisfies one of three conditions: everyone is free and strictly prefers that status; everyone is premium and strictly prefers that status; or an interior share equalizes utilities and a marginal increase in premium participation hurts premium players more than free players. When several stable shares exist, players select the equilibrium with the highest utility. The common friction term cancels in these comparisons.
The printed response is defined separately from the claim of stability. For , it is one below , equals on the inclusive interval , and is zero above . For , it is one at prices at most and zero above that threshold.
Advertising strength and price are nonnegative measurable controls. Average utility excluding friction is
The population follows the nonsingular form of the source's dynamics,
This equation also specifies behavior at zero population. In particular, its drift there is . Advertising has a twice differentiable cost with positive first and second derivatives on its nonnegative domain. For finite horizon and discount rate , operating profit is
Global optimality compares this quantity with every admissible control and trajectory, as in Problem (3), pp. 13–14.
Lemma 1 claims that, when , the stable shares are exactly the printed response. The middle share lies in and strictly decreases with price on . Lemma 2 claims that, when , the player-preferred stable shares are exactly the printed response. Both targets assert existence, through their two-way characterizations, including all stated boundary prices.
The goal, Proposition 3, asserts an attained globally optimal policy with strictly declining advertising and
It has an introduction threshold , possibly zero. Per-player payment is zero before the threshold and positive after it. If , price strictly decreases after introduction, with
If , price is identically on . No uniqueness is asserted. These are the exact endpoint prices and both regimes of Proposition 3, p. 14, with strict price decrease explicitly stated in the discussion on p. 15.
The source's claim describes when a developer starts charging and how its advertising and subscription price evolve. The downward-dominant regime allows scarcity of premium participation to influence population growth. The upward-dominant regime instead selects either universal premium participation or none, leading to a different asserted price path.
The formalization separates behavioral equilibrium, the stipulated population response, and global optimization. This distinction matters because a wrong equilibrium claim must not become an inconsistent assumption from which an optimal-control result follows automatically. The definitions are concrete, and the three theorem statements are open proof or disproof targets. There are no machine-checked proofs of those targets in this mission.
The source claims are preserved even where the source has defects. Lemma 1's inclusive boundary prices conflict with its strict definition of stability. The optimal-control proof has a discount-rate gap and a terminal division by zero; it also contains a payoff typo and a conflict between strict price decrease and a clipped formula. These findings are documented individually in the accompanying insights, without replacing the source targets by repaired claims.
The central issue is global optimization over time-dependent controls, rather than maximization of instantaneous revenue. Changes in price alter both revenue and population growth. The admissible set also contains the physical state boundary and unbounded advertising controls. Necessary optimality conditions alone do not state the required comparison against every policy.
Boundary conventions matter independently of analytic difficulty. The response must retain the source's inclusive middle price interval while stability retains its strict endpoint tests. The initial population is zero although the original utility expression contains reciprocal population. Endpoint prices must describe the path's limiting behavior, rather than arbitrary values assigned at individual times.
Four definition items provide a general scalar control system, the player model, the advertising-cost class, and Problem (3). The paper-specific system instantiates the general trajectory definition. An integrable-drift integral equation represents absolutely continuous state paths. Controls are measurable for completed Lebesgue measure; their values outside the horizon are irrelevant. Almost-everywhere equivalent controls describe the same optimization choice, while the asserted path shape belongs to a chosen representative.
Profit uses an extended nonnegative integral of discounted together with the finite baseline cost. Thus infinite expenditure has profit and cannot acquire a profitable default value. Revenue integrability is explicit. No normalization of , quadratic specialization, coercivity condition, control bound, small-discount condition, or positive initial population is imposed.
The advertising word “decreases” receives the stronger strict reading specified for this mission. One-sided endpoint limits prevent isolated assignments from manufacturing the claimed paths. These conventions are declared in each affected theorem's differences list. The mission's scope excludes the paper's independent matchmaking, partial-subscription, liquidity, and player-budget extensions.
An online platform must allocate resources before it knows which customers will arrive later. Advertising budgets, limited product inventories and workers' task opportunities can all be exhausted by early decisions. When the probabilities of a successful allocation are also unknown, a platform must learn from the same interactions that consume its scarce resources. Reserving inventory for future customers and gathering useful observations are therefore coupled decisions.
Cheung, Ma, Simchi-Levi and Wang introduce Inventory Balancing with Online Learning (IBOL) to separate the inventory mechanism from the choice of learning algorithm. Their general guarantee relates the physical revenue of the allocation process to a linear-programming benchmark and a particular learning-regret quantity. This mission formalizes that framework result, Theorem 1, with its exact finite-capacity coefficient, rather than an application-specific oracle analysis. The source is the pinned preprint arXiv:1810.05640v2, Sections 2–4 and Appendix A.2.
There are resources. Resource has positive integer capacity and earns reward each time one unit is consumed. Inventory is not replenished. Customers arrive over a finite horizon . Each arrival reveals a context from a known finite set. The context sequence is arbitrary but fixed by an oblivious adversary before the run. The algorithm receives the current context and past observations, without future arrivals or the horizon as inputs.
The action space is general. Given context and action , a fixed unknown distribution produces a Boolean vector . Several coordinates may be one, and coordinates may be correlated. Write . The chosen action generates a fresh conditional sample; outcomes for unchosen actions are unobserved. A successful coordinate consumes one unit only if inventory remains. Feedback is still observed for depleted resources. These are the model conventions in Section 2, pages 8–10.
Let count consumed units before round . IBOL uses the perturbed potential
to assign discounted rewards . An arbitrary randomized bandit oracle receives the ordered history of observed triples, and , and returns . No maximization property or particular regret bound is required of the oracle. These operations specify Algorithm 1 in Section 3, pages 12–16.
Physical revenue is
The auxiliary mean reward is . Its dynamic comparator evaluates the best action at the very same realized inventory. The relaxed regret is the signed quantity
It can be negative. It is neither regret against a fixed action nor the revenue gap to an independently run optimal allocation policy.
The LP benchmark chooses a probability allocation over actions in each period. It maximizes subject to for every resource. Each measure has total mass exactly one. Its optimal value is . For discrete actions these integrals recover equations (9)–(12) of the source.
The goal is Theorem 1 on page 17, equations (13)–(14). For every model, oblivious arrival sequence, randomized oracle and ,
where the exact coefficient is
The formal extended-order statement is . Since , this is equivalent to the displayed guarantee whenever the LP value is finite.
There are two supporting milestones, both with the full inherited domain . Claim 1, page 40, asserts that and form a feasible solution to the printed dual for every realized path, and that
Lemma 4, page 41, asserts for every positive integer and that
The two milestones are the numbered dependencies in Appendix A.2. Application-specific UCB and LazyUCB guarantees are outside this mission.
The theorem gives an interface between a learning algorithm and an allocation guarantee: the oracle's relaxed regret enters a precise physical-revenue bound. Its coefficient retains every resource capacity and the exploitation parameter. At unit capacity and , the resource coefficient is ; no large-inventory approximation is needed to interpret the target.
The paper supplies a mathematical proof. This mission supplies compiled statements and concrete definitions for a Lean proof of that result; the three theorem declarations remain open. The reusable outputs include a probability-measure packing LP and a model of randomized policies with correlated vector feedback. Establishing the stated theorems in Lean remains the solver's task.
Discounted rewards change with realized inventory, which depends on earlier actions and outcomes. Treating the auxiliary reward sequence as independent would therefore lose the process that the theorem concerns. Likewise, assuming that the oracle selects an actual maximizer would remove the learning contribution from the statement.
Several boundary cases affect the mathematics. Resources at capacity still produce feedback, although their physical and discounted rewards vanish. Relaxed regret need not be nonnegative. The discrete inventory grid includes its depleted endpoint. A general action space need not admit a best action, and the equality-constrained primal LP need not be feasible when there is no zero-consumption action. The definitions retain these cases without inserting extra optimization or feasibility assumptions.
Resources and finite contexts use finite index types; capacities are positive naturals. Histories carry the usual measurable structure obtained from the finite product space at each possible length. The run is built by successive probability-kernel sampling of an action and then its outcome. The oracle receives only observed history, current context and discounted rewards.
Action integrals extend the printed sums to general measurable spaces. Every discrete source allocation is included. Best-action suprema agree with the printed maxima whenever attained and additionally cover unattained values. The LP value uses extended reals, with for an empty feasible set. No indeterminate extended-real subtraction appears in the theorem. Claim 1 also asserts pathwise feasibility for arbitrary length- observation strings, including probability-zero strings generated by the same physical update rule.
All objectives, coefficients, policies and certificates are constructed from data. Neither a performance bound nor dual feasibility is packaged as a model assumption. Mathlib supplies kernels, measures, integrals, finite sums, exponentials and order operations. The separate definition modules distinguish the general LP from its inventory-specific instance. The explicit history definition on page 15 determines the indexing used in Algorithm 1; the shifted update indices in its printed line 9 are recorded as a source finding.
This mission formalizes K. Juschenko and N. Monod, Cantor systems, piecewise translations and simple amenable groups, Ann. of Math. (2) 178 (2013) 775–787, doi:10.4007/annals.2013.178.2.7. Page numbers are those of the journal.
The topological full group of a Cantor system is the group of homeomorphisms of given piecewise by powers of , on open pieces. Matui showed that for minimal its commutator subgroup is simple, and finitely generated exactly when is a minimal subshift. Grigorchuk and Medynets conjectured that is amenable. Juschenko and Monod proved the conjecture (Theorem A). Together with Matui's results this gave the first examples of infinite, finitely generated, simple, amenable groups (Corollary B); in the paper's words, “Until now, no example of a finitely generated simple group that is amenable (and infinite) was known.”
JuschenkoMonod, which reuses (IntervalExchange.wobbling ℤ), the topological full group (CantorSystems.topologicalFullGroup), amenability (Garrido.IsAmenable) and local finiteness (Chou.IsLocallyFinite) from published bundles.Theorem A (p. 776): the topological full group of any minimal Cantor system is amenable.
Theorem A is the first amenability proof for a class of groups that contains finitely generated infinite simple groups. Its method, a family of almost invariant densities on the Bernoulli space, became the starting point of extensive amenability (Juschenko, Matte Bon, Monod and de la Salle), which also yields amenability of interval exchange groups of low rank. The milestones also state the cited results that Corollary B combines with Theorem A: Matui's simplicity theorem and finite generation criterion, and Matui's uncountable family of pairwise non-isomorphic examples.
The analytic core (§2) is elementary but delicate: Theorem 2.1 shows that the densities are almost invariant under each piecewise translation, through a signed series controlled by Abel summation. §3 converts this into Theorem C, an invariant mean on finite subsets of concentrated on the sets containing , by Fourier analysis on and the Reiter criterion. §4 embeds into and shows the relevant stabilisers are locally finite, by the ubiquitous pattern property. The amenability of is then assembled from two general facts: an action with an invariant mean and amenable stabilisers forces amenability of the group (Lemma 3.2), and for a subgroup of it suffices that the stabilisers of the sets are amenable (Proposition 3.3). The external results on topological full groups (Matui, Giordano–Putnam–Skau, Elek–Monod) are substantial papers of their own; the Elek–Monod example shows that the one-dimensional structure is essential, since Theorem A fails for minimal -systems.
The definitions follow the paper closely, with a few encodings worth knowing. is the type of functions X → Fin 2 with the product of uniform measures. The lamplighter acts on finite subsets by . Means are finitely additive probability measures on all subsets, as in the bundle Garrido_Amenability. The net of almost invariant vectors in Lemma 3.1 is stated with finite sets of group elements and tolerances . Where a reading was needed — the range of in §2, how the constants of Lemma 2.6 depend on , the size of Matui's family — the milestone's Formalization note says which was taken.
Every numbered result is a milestone, with the unnumbered steps the proofs use: the inequality (2.ii), the remark after Theorem C, the finiteness of , and the homomorphism . The cited results stated as external milestones are Matui's simplicity theorem, finite generation criterion and uncountable family, the Giordano–Putnam–Skau classification, and the Elek–Monod -system. Left out: Schreier's remark on free subgroups of and the Grigorchuk–Medynets local embeddability theorem (motivation only), the local finiteness of forward-orbit stabilisers via Putnam's AF-algebras (context for Lemma 4.1, which the paper reproves), and Matui's theorem that the groups are never finitely presented.