Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A firm selling a fixed stock of a perishable product over a finite season must set prices without knowing how demand responds to them. Online retail and travel platforms often see a customer's segment before quoting a price, so they can price-discriminate across consumer types. Learning a separate demand curve for each type, however, seems to cost more exploration as the number of types grows. Chen and Gallego (arXiv:1812.09234v3, 2021; Mathematics of Operations Research, 2022) give a learning algorithm whose regret does not depend on the number of types. Their key step is to learn a single scalar first: the shadow price of inventory.
Earlier work on the single-type problem frames the question. Besbes and Zeevi (Operations Research, 2009) defined the regret against the fluid benchmark and showed that no policy can achieve regret decaying faster than . Wang, Deng and Ye (Operations Research, 2014) gave a single-product algorithm whose regret matches this rate up to logarithmic factors. Chen and Gallego extend the rate to types with one inventory constraint.
There are consumer types, a season and an inventory . When the firm charges price to type , type- consumers arrive at rate . Prices range over , where is a choke price with . Assumption 1 asks that each be strictly decreasing, bounded and Lipschitz, and that the revenue rate be Lipschitz and twice differentiable, with .
The fluid problem (2) maximizes subject to . Its optimal value is . Its dual is one-dimensional. With
the dual optimum is , and the optimal fluid prices are the constants .
In the -th system demand and inventory scale together: type arrives as a Poisson process with rate , and the inventory is . The firm does not know . It knows , , , the constants of Assumption 1 and, by Assumption 2, intervals and that contain every and . A policy has expected revenue , and its regret is
Algorithm 1, the primal-dual learning algorithm, runs phases of shrinking lengths . In each learning phase it tests a price grid inside the current interval estimators of every . It then minimizes an empirical dual function on a grid of and re-centres the interval estimators of and . In the last phase it either charges a marked-up price (sufficient capacity), or tests two prices and interpolates between them so that total sales end close to (insufficient capacity). Its tuning depends on a constant .
For every one can choose and a constant , independent of , such that
Theorem 1 states that personalized pricing for types under a shared inventory constraint is learnable at the single-type rate , up to logarithms, with a constant independent of . Combined with the Besbes–Zeevi lower bound, the algorithm is rate-optimal. Learning the scalar shadow price , instead of the joint optimum of an -dimensional problem, is what avoids the curse of dimensionality.
The result is proved in the paper; no machine-checked version exists. A formalization would add to the platform a multi-type Poisson pricing model with stock-outs, the one-dimensional Lagrangian dual of the fluid revenue-management problem, an exactly specified multi-phase learning algorithm, and reusable Poisson deviation lemmas. Lemmas 1, 2, 9 and 10 and Proposition 1 can be proved independently of the probabilistic analysis.
The obvious argument estimates every directly and charges the estimate. With interval estimators of width this loses revenue of order per unit time when the inventory constraint binds (), because is then not the unconstrained maximizer of . The paper's (11) and (19) show the loss. The bound requires steering the total sales to within of the inventory, which is Lemma 8, and a second-order expansion of the revenue around that uses the first-order condition .
Formally, a further difficulty is the closed loop: the prices of a phase depend on the counts of earlier phases, and the counts are Poisson only conditionally, through the random time change .
All declarations live in the namespace PrimalDualPricing.Regret. Printed page numbers equal PDF page numbers in the cited preprint.
Fin M. Each satisfies Assumption 1 on and is otherwise any extension with ; the last-phase prices and can leave . encodes the choke price. and are fields carrying their optimality properties.IsPoissonProcess) with right-continuous, jointly measurable paths. The inventory of the -th system is units, and nothing is sold after the stock-out. Lemmas 6–8 use the uncapped sales of the paper's modified system (§4).A formalization that lets the policy read the true demand, measures regret against anything other than , ignores the stock-out in , or assumes the high-probability events of Lemma 5 would trivialize the goal; none of these is done here.
Contributions to the reusable parts are welcome: Poisson tails, the envelope theorem for , and the time-change construction of policy-driven Poisson sales.
In online learning with bandit feedback, the learner chooses one action and sees only that action's loss. This is the information pattern of sequential trials in which testing one option does not reveal the outcomes of the others. The learner must keep its cumulative loss close to that of a good fixed action while learning which actions are good. A full-information method can update from every arm's loss each round; here the unseen losses have to be handled through the observations the learner actually receives. Chapter 9 of Orabona's text develops this distinction for multi-armed bandits.
Two environments are treated in the chapter. With an oblivious adversary, all losses are fixed before play, although the learner does not know them. With a stochastic environment, each arm has a fixed loss distribution and new losses are drawn across rounds. An algorithm with a guarantee in both environments does not need to be told which generated its data. Theorem 9.17 gives such a pair of guarantees for the FTRL version of Tsallis-INF, using the precise constants stated in the pinned version of the book.
There are arms and rounds, numbered . In round , the learner forms a probability vector on the simplex , draws an arm with probability of choosing , and observes only . The loss of an unchosen arm is not revealed. For an oblivious adversary, the entire table is deterministic and the expectation is over the learner's draws.
Algorithm 9.6 uses the importance-weighted estimate if , and otherwise. Its Tsallis-INF FTRL prediction minimizes, over ,
The minimizer has positive coordinates. Thus each denominator used by the estimator is positive. In the stochastic environment, arm has mean ; if is a best arm, its gap is . The pull count is the number of rounds through in which arm is selected. Stochastic pseudo-regret compares the learner's expected loss with , the expected loss of always playing the best arm.
The mission's main theorem is the adversarial claim of Theorem 9.17, p. 165. For every fixed comparator arm and losses in ,
Taking to be the best arm in the fixed loss table yields the stated adversarial regret bound. The companion item formalizes the second claim of the same theorem: if the losses are stochastic with a unique best arm and , then
The milestone list contains the chapter's pseudo-regret decomposition (Lemma 9.10), its sub-Gaussian sample-mean bound (Corollary 9.9, reused from an existing formal statement), and the probability-sensitive Tsallis-INF inequality (9.8). These are distinct mathematical claims rather than alternate names for the final bound.
The adversarial bound grows like and remains valid for any fixed bounded loss table. The stochastic bound instead measures the difficulty of distinguishing arms through the positive gaps and grows logarithmically with the horizon for fixed gaps. Both refer to the same FTRL update and the same importance-weighted estimator. The finite-horizon constants and are part of the target, not unspecified factors hidden in asymptotic notation.
Both claims are proved in the book. The work here is to give their hypotheses, random experiment, and algorithm a machine-checkable Lean interface, then formalize the known arguments. At this drafting stage the theorem bodies are open Lean problems; a successful build checks that their statements are well formed, not that the regret bounds have been proved. The resulting finite-history bandit protocol and stochastic pseudo-regret definitions can also support other loss-based bandit algorithms. The existing formalized sub-Gaussian tail bound can be reused for concentration results elsewhere in the chapter.
The learner observes only one coordinate, while regret is measured against losses across all arms. The importance-weighted estimate corrects the missing observations in expectation, but its size can grow when a selected arm has small probability. Consequently, a bound based only on a uniform estimate of its magnitude loses the probability dependence needed for the theorem's constants. The stochastic claim adds another difficulty: the learner's choices depend on past observed losses, so a current loss must be related to a random pull count without letting the choice depend on that current loss.
There are two tempting but invalid shortcuts. Permitting to inspect would change the bandit protocol, and taking an expectation under an arbitrary path measure would no longer describe the arm draws of Algorithm 9.6. The formal statements tie each prediction to its FTRL objective and each path probability to the predictions made along that history.
Arms are Fin d; the main theorem permits , where both its regret and bound are zero. Rounds retain the book's indexing. A finite path has a dummy coordinate zero, fixed to an arbitrary anchor arm; this coordinate is never played or scored. The adversarial losses are a fixed table, selected before any draw. A path has probability equal to the product of the algorithm's conditional arm probabilities, and regret against a fixed arm is a finite weighted sum over paths. The FTRL run predicate requires simplex membership, strict positivity, minimization against every simplex point, and dependence only on past arm choices. The last two properties specify the intended update on every possible history.
The stochastic model first samples a loss table from a probability measure and then draws an arm path conditionally using the same Algorithm 9.6. Current-round loss vectors are independent across rounds, while coordinates within one round need not be independent. Each arm has the same mean in every round. The policy is a measurable function of the observed history (past arms and their losses); its expected loss is explicitly integrable. Loss bounds are imposed on every outcome in the chosen sample space, which can be taken as the support of bounded distributions. The stochastic statement adds to make the logarithmic formula's domain explicit, and the unique-best-arm assumption ensures every denominator in the displayed sum is positive. Lemma 9.10 also spells out the integrability of its means and pull counts.
The development needs finite probability laws, real integrals, simplex geometry, and properties of the square-root regularizer. The independent tail bound for sample means is already available as a referenced theorem. Contributions that establish existence and interiority of the FTRL minimizer, the normalization of the path law, or the stated regret inequalities fit this scope. A choice rule that sees the current loss, a path law unrelated to , or a zero integrability default does not satisfy the intended bandit model.
In stochastic programming the objective is an expectation that cannot be evaluated, and an algorithm sees only noisy gradients drawn from a stochastic first-order oracle. Stochastic gradient descent and its relatives are the standard methods. For convex the optimal rate is known: Lan's accelerated stochastic approximation method (Lan, Math. Program. 2012) reaches an expected optimality gap of order after oracle calls. For smooth nonconvex , Ghadimi and Lan's randomized stochastic gradient (RSG) method (arXiv:1309.5549, SIAM J. Optim. 2013) bounds the expected squared gradient norm at a randomly chosen iterate, but it is only nearly optimal when happens to be convex.
Saeed Ghadimi and Guanghui Lan (arXiv:1310.3787v1, 2013; Mathematical Programming 156, 2016) combined the two lines: the randomized stochastic accelerated gradient (RSAG) method has a guarantee for nonconvex problems, and with suitable step sizes it attains the optimal rate on convex ones. This mission formalizes that result, Theorem 3 of the paper, together with the steps of its proof in §3.1.
Let be differentiable with Lipschitz gradient: for all , with . Gradients are available only through a stochastic oracle: at its -th call, with input , it returns , where are random variables on a probability space and is jointly measurable.
Algorithm 3 (RSAG). The inputs are , step sizes , for , , , an iteration limit , and a probability mass function . A termination index with is drawn first, independently of the noise. With , for ,
and the method stops at and outputs . The oracle error is .
Assumption 1 asks that the oracle be unbiased, , with variance . The paper does not require the to be independent.
The weights are , , and for a horizon
Fix . The expectations are taken over and .
a) If is bounded below with , for , and (3.4), then
b) If is convex with a minimizer , is nonincreasing (2.10), and (3.6), and (3.7), then
The goal keeps every printed constant and leaves the step sizes free. Corollary 3 specializes them; it is not part of this mission.
Part a): the quadratic bound (2.1) (already proved on the platform); a pathwise one-step inequality for (p. 16); a stochastic version of (2.17) bounding ; the summed inequality with martingale terms (pp. 16–17); its expectation (p. 17); the identity expressing as a -weighted average (p. 17); Theorem 3 a). Part b): Lemma 1 (p. 4); the convexity bound (2.21); (3.10) with a sign corrected; the stochastic version of (2.22); (3.11); its two consequences at (p. 18); the weighting identity for (p. 18); Theorem 3 b).
The result. Theorem 3 gives one stochastic first-order method with two guarantees. On a nonconvex problem it finds an approximate stationary point with an explicit bound on . On a convex problem its optimality gap matches the lower bound for stochastic convex optimization, which the RSG method does not. The method does not need to know which case it is in; only the step-size policy changes. Later work on accelerated and variance-reduced methods for nonconvex stochastic problems builds on the same analysis, and Theorem 4 of the paper extends it to composite problems with mini-batches.
Formalizing it. The result is proved in the paper and, as far as we know, has not been machine-checked. A formal proof would check the bookkeeping that a reader usually takes on trust: the nested sums in and , the conditional-expectation arguments that make a martingale difference sequence, and the passage from fixed horizons to the random output . The printed proof has small errors (see Formalization scope), so the formal statements record the corrected forms.
The deterministic analysis of the AG method (Theorem 1) bounds along a single trajectory. In the stochastic case the same chain produces cross terms and . These cross terms do not vanish pathwise, and the variance terms come with coefficients involving that grow backwards in time. The obvious argument would take expectations termwise. It fails unless one shows that each cross-term coefficient is measurable with respect to the past, so that its product with has zero mean under conditional unbiasedness. This also requires square-integrability of every iterate, which the hypotheses do not state and which has to be established by induction. A second difficulty is the random output: the bound is on , an integral over and the noise jointly, so the independence of from the noise has to be used explicitly.
EuclideanSpace ℝ (Fin n) (the published GhadimiLan.RSG.E n). is the published predicate ConvexOptAlg.SmoothGD.IsBetaSmooth Ψ g LΨ, with , and .GhadimiLan.RSG.AssumptionA1 applied to the middle points: for a filtration to which the noise is adapted, a.s. and . This conditional form is what the paper's martingale-difference step uses. It holds when the are independent, and it allows dependent noise, as the paper does.The following versions would make the goal trivial and are excluded: a deterministic oracle ( hard-wired), fixed to , an oracle not tied to , and an unconditional unbiasedness hypothesis too weak to support the martingale step.
A complete development needs conditional expectations of vector-valued random variables, square-integrability of the iterates, and the independence calculus for the random index. These parts are reusable for the companion RSG and mini-batch RSAG missions. Contributions are welcome on any milestone. The pathwise milestones (one-step bound, (2.17), (2.21), (2.22), (3.10)) need no probability theory.
The simplex method for linear programming moves from vertex to vertex along the edges of a polyhedron. A lower bound on the number of pivots of any edge-following method is the graph diameter of the feasible polyhedron: the largest number of edges needed to connect two of its vertices. Whether this diameter is bounded by a polynomial in the dimension and the number of facets is the polynomial Hirsch conjecture, open since the 1950s. The original Hirsch conjecture, , was refuted for unbounded polyhedra by Klee and Walkup (1967) and for bounded ones by Santos (2012) (doi:10.4007/annals.2012.176.1.7).
Timeline.
A polyhedron is the set of solutions of finitely many linear inequalities,
It need not be bounded. A vertex of is a point for which some half-space satisfies , equivalently an extreme point of . Two vertices are adjacent when for some half-space ; the segment is then an edge. A path of length is a sequence of vertices with consecutive vertices adjacent, is the least such , and the diameter is over pairs of vertices. A -polyhedron is a -dimensional polyhedron with facets, and
the maximum taken over bounded and unbounded polyhedra alike. All logarithms are to base 2.
The goal fixes no constant beyond the paper's own exponent and leaves no case of , or boundedness open.
The result. The bound is never larger than the Kalai–Kleitman bound. It equals the true value in dimensions 1 and 2, and it depends on only through the Hirsch quantity . Since , it is also symmetric under linear-programming duality, which exchanges the roles of and . For fixed it is polynomial in . It applies to the unbounded feasible regions that arise in practice in linear programming.
Formalizing it. The theorem has been proved since 2014. The platform has a proof of the bounded case only: Hirsch.todd_bound assumes , a nonempty interior and Bornology.IsBounded. This mission's goal extends it to all polyhedra, bounded or not, and to . That is the statement the paper proves, and the one an analysis of the simplex method on unbounded feasible regions needs. The unbounded form of Lemma 1 and the common-facet bound are open on the platform as items of the Kalai–Kleitman series and are reused here. Klee's unbounded three-dimensional bound has no formal proof on the platform: the published Hirsch.klee_three_dimensional_bound and Hirsch.dimension_three_bound cover bounded polyhedra only. The bounded recursion Hirsch.kalai_kleitman_recursion and the bounded facet reduction Hirsch.facet_reduction are proved and may serve as models.
Two steps are hard. The first is the unbounded case. Statements proved for polytopes do not transfer directly, because an unbounded polyhedron may have no vertices or a single one, unbounded edges (rays) that are not edges of the graph, and redundant or implicit-equality rows. Each geometric milestone must hold for these. The second is Klee's three-dimensional bound, which the paper cites without proof. Assuming boundedness to apply the published polytope versions is ruled out: Klee and Walkup showed that unbounded and bounded diameters differ from dimension four on, so the unbounded case carries content of its own. The arithmetic milestones are elementary but sensitive to edge values of and the real power.
All statements use the published definitions Hirsch.Hpoly, Hirsch.Adj and Hirsch.DiamLE (Hirsch_model). Vertices are Set.extremePoints ℝ. DiamLE P B says that any two extreme points are joined by a walk of exactly steps, each step staying put or crossing an edge. So the bound includes connectivity of the vertex–edge graph.
DiamLE (Hpoly a b) B. This ranges over all polyhedra given by inequalities in , including lower-dimensional, empty and redundant ones. It is equivalent to the paper's statement: a lower-dimensional polyhedron of dimension with facets has .Real.logb 2 and the power is Real.rpow. A distance is at most exactly when it is at most the floor , abbreviated toddBound d n in the milestone on the ten cases. The clause is a separate conjunct, because in Real.rpow.Trivializing encodings are excluded: no Bornology.IsBounded hypothesis; no definition of by sSup over , which would be on unbounded families; no use of Hirsch.gdist, which is when no walk exists; and no dropping of the clause.
Contributions are welcome on every milestone. A complete development needs facial structure of unbounded polyhedra (facets as polyhedra one dimension lower, tight rows at vertices), the relaxation argument of Lemma 1, Klee's three-dimensional argument, and real-power and logarithm estimates. The facet machinery and Klee's bound are reusable for any diameter result on unbounded polyhedra.
Many graph-colouring questions ask whether a proper colouring can be produced indirectly, from local data, instead of being assigned vertex by vertex. In the 1-2-3 Conjecture, the colours are produced by weighting the edges of a graph and colouring each vertex with the sum of the weights at it. Karoński, Łuczak and Thomason asked in 2004 whether weights from always suffice (J. Combin. Theory Ser. B 91 (2004)). The question started as a local version of the irregularity strength problem, where all vertices, not only adjacent ones, must receive different sums. It became one of the most studied problems on graph labellings. Surveys: Seamone (arXiv:1211.5122) and Grytczuk (DOI 10.1016/j.ejc.2020.103213).
Timeline.
Let be a finite simple graph and write for the neighbourhood of a vertex . A -edge-weighting is a function . The weighted degree of is
Two adjacent vertices have a coloring conflict if . The weighting is vertex-coloring if no edge is a coloring conflict, that is, if is a proper vertex colouring of .
If has a connected component consisting of a single edge (a component isomorphic to ), then for every , so no weighting is vertex-coloring. This is the only obstruction.
The proof uses a few further objects:
The Lean names are wdeg G ω v for , IsWeighting G k ω, IsVertexColoring G ω, NoK2Component G and IsGoodPartition G U R B.
If no connected component of is isomorphic to , then there is with
Every finite connected graph with has a vertex-coloring -edge-weighting. This is the statement the case analysis of the proof establishes. Theorem 1 follows by treating each component separately.
In the order the proof uses them:
The result. Theorem 1 settles a conjecture that was open for nineteen years. The constant is optimal: the triangle has no vertex-coloring -weighting (two of its three edges get the same weight, and then two vertices tie), and deciding whether a vertex-coloring -weighting exists is NP-complete (Dudek and Wajc, 2011). Theorem 1 also closes the sequence of upper bounds on the number of weights needed. Variants remain open: total weightings with vertex weights and edge weights (the 1-2 Conjecture), and list versions.
Formalizing it. The theorem is proved, in a 16-page paper. As far as is known it has no machine-checked proof. A formal proof would verify the case analysis at the end of the paper (pp. 11–14, about fifteen sub-cases with three auxiliary graphs), which is where errors in such arguments usually hide. The flow lemma is quoted from the 2023 paper and not reproved here. Formalizing it means proving an integral max-flow statement for a specific unit-capacity network, and the result can be reused for other flow-based weighting arguments.
The obvious approach is to fix the weights greedily, edge by edge or vertex by vertex. This fails because changing one edge weight changes two weighted degrees at once, so a repair at one vertex can create a conflict at a neighbour. With only three weights there is no room to absorb this. Every earlier bound above used the extra weight as slack.
The difficulty in the paper is parity. The construction needs the set of blue vertices to have even cardinality, and cannot always be made even. The proof therefore removes one or two vertices, applies one of three base lemmas, and re-inserts the vertices. That re-insertion may need one more round of weight changes along a path. Each sub-case has to keep track of parities, of exact weighted degrees on , and of the connectivity of simultaneously.
Representation.
SimpleGraph V on a finite vertex type V with decidable adjacency. The paper's "graph" is a finite simple graph: weighted degrees are finite sums, and the proof uses a maximum cut and vertex orderings.ω : Sym2 V → ℕ on unordered pairs. IsWeighting G k ω requires for every edge of ; values on non-edges are unconstrained and never used.G.neighborFinset v. Since in Sym2, the single sum equals both sides of Theorem 1's displayed inequality.G.between R B, induced on wherever that vertex set is not all of .Conventions that differ from the page. There are two, both disclosed in the item statements:
Lemma 5's condition is stated in , and Lemma 3's is computed in .
Ruled out. None of the following formalizations is faithful:
Infrastructure. A complete development needs:
The flow and cut definitions are stated for arbitrary finite graphs and can be reused. Contributions are welcome at every level: proofs of individual lemmas, general flow-decomposition results, and the final case analysis.
In a stochastic multi-armed bandit, a player repeatedly chooses one of arms and receives a random reward drawn from the chosen arm's unknown distribution. The classical lower bounds of Lai and Robbins (1985) and Burnetas and Katehakis (1996) describe the regret of good strategies when the horizon tends to infinity: it grows like , with a constant determined by Kullback–Leibler divergences. They say nothing about small horizons.
Garivier, Ménard and Stoltz (Math. Oper. Res., 2019; arXiv:1602.07182v3) show that the regret has a definite shape over the whole range of : it is almost linear at first ("explore first"), and only afterwards logarithmic ("exploit next"). Their §3 gives three non-asymptotic lower bounds for the initial phase, each for a natural class of strategies. This mission is the third of them, Theorem 4 (p. 13): a collective lower bound on the total number of pulls of all suboptimal arms. It is the bound that remains informative when many arms are suboptimal, and it is the one illustrated for large in the paper's §3.4.
A bandit problem is a family of probability distributions on , each with an expectation . A model is a set of such distributions, and is in when every . Put .
At each round a strategy chooses an arm from the past rewards (possibly with auxiliary randomization) and observes a reward . The number of pulls of arm up to round is , and is the expectation when interacts with .
The set of optimal arms is , of cardinality , and the set of worst arms is , the arms of smallest mean. The paper defines a partial order: when for every optimal arm of and for every other arm. Two classes of strategies enter the theorem.
With the Kullback–Leibler divergence, the constant of the theorem is
The Bernoulli divergence is , (5).
For every model , every strategy pairwise symmetric for optimal arms and monotonic on , every bandit problem in and every ,
Theorem 4 bounds the regret from below through , (13). While is small compared with , the right-hand side of the theorem is of order , so the regret is linear: a reasonable strategy cannot avoid spending a constant fraction of the first rounds on the suboptimal arms. Unlike the per-arm bounds of Theorems 2 and 3, the bound concerns all suboptimal arms at once and does not degrade as grows; §3.4 of the paper shows numerically that it gives the stronger regret bound for many arms.
The theorem is proved in the paper; to our knowledge no part of it has been machine-checked. A formal proof would exercise the published canonical bandit model of the platform (StochasticBandit, BanditPolicy, banditMeasure) on a genuine lower-bound argument with two auxiliary bandit problems, together with a local Pinsker inequality for Bernoulli divergences in that is reusable in other bandit lower bounds.
The obvious attempt applies the fundamental inequality (6) to and an alternative in which one suboptimal arm becomes optimal, as in Theorem 2. That gives a bound arm by arm, which deteriorates with and does not see the number of optimal arms; it also needs a hypothesis of the type "smarter than uniform", which is not assumed here. Nothing is known about how a general behaves on itself, so the two hypotheses on must carry all the information, and both are weak: Definition 3 only constrains pairs of optimal arms with equal laws, and only through the joint distribution of their pull counts under the canonical bandit measure; Definition 4 only compares problems ordered by . On the analytic side, the classical Pinsker inequality loses the factor and gives a weaker theorem, so a local refinement is required, and every divergence is valued in .
Arms are indexed by Fin K (the paper's arm is index ), with assumed in the goal. A bandit problem is the published BanditAlgorithm.StochasticBandit K, a strategy is a published BanditPolicy K (a family of Markov kernels from histories to arms; every strategy of the paper with auxiliary uniform randomization induces one with the same law of arms and rewards), and is the integral of the pull count against banditMeasure. A model is a Set (Measure ℝ) whose members are probability measures with an integrable identity, the standing assumption of §1.1–§1.2. Definitions 3 and 4 leave implicit and are read "for all "; in Definition 3 equality of distributions is equality of the image measures of the pair of counts, not of their expectations. , and take values in ; the goal assumes , since otherwise the printed bound is and a real-valued conversion would silently replace by . The Bernoulli divergence is defined as the divergence between two Bernoulli laws on , so it is where (5) is, rather than a finite junk value. The auxiliary problems of the proof are not constructed; the milestones quantify over them with their defining properties.
The paper's "In particular" clause, for , is not stated: it follows from the main display only when (at the main bound is negative), and whether it holds in general is not known here.
A formalization that weakens the strategy classes (full permutation symmetry, or equality of expected counts in Definition 3), drops the requirement that the problems lie in the model, or uses a real Bernoulli divergence with finite values at does not count.
A complete development needs the fundamental inequality (6) on the canonical bandit model (the subject of mission I of this series; the chain rule for the divergence of bandit measures is already proved on the platform), the symmetry argument on the canonical measure, Lemma 6 and Lemma 2. Contributions of any of these, and of the identity integrated against banditMeasure, are welcome; Lemma 6 and the symmetry lemma are reusable beyond this mission.
A stochastic multi-armed bandit learner repeatedly selects one of finitely many arms and sees only the reward from the selected arm. The learner must gather information about uncertain rewards while trying to select high-mean arms. Expected regret summarizes the lost reward relative to always selecting an optimal arm, but regret alone does not explain how much sampling each particular arm must receive. Garivier, Ménard, and Stoltz study this allocation question directly in Explore First, Exploit Next: The True Shape of Regret in Bandit Problems. Their Section 3 gives lower bounds for small horizons, before the longer-run logarithmic behavior becomes dominant.
The paper's first small-horizon result concerns strategies that allocate at least a uniform share to every optimal arm, on every problem in a specified model. This requirement excludes a strategy that always selects one fixed label and succeeds only when that label happens to be best. Such a requirement still permits many adaptive policies; it constrains their performance on optimal arms rather than prescribing their decisions round by round. The result establishes a compulsory initial allocation to every arm, including one whose mean is below the best mean. It is Theorem 2 on page 10 of the pinned arXiv:1602.07182v3.
A bandit problem consists of probability laws on . At each round, a strategy chooses an arm using the observed past and randomization, then receives an independent reward drawn from that arm's law. The mean reward of arm is . Write , and call an arm optimal when . The count is the number of times arm is chosen during the first rounds. These objects and the information available to a strategy are specified in Section 1.1, pages 2–3.
A model is a collection of possible arm laws, each a probability measure with an expectation. The notation means that every arm law belongs to . A strategy is smarter than uniform on when, for every bandit problem in the model, every optimal arm , and every integer , it satisfies
This is Definition 2 on page 10. It imposes a lower bound on each optimal arm, even when several arms tie. The requirement is evaluated across the whole model, so a strategy cannot be declared smarter based only on its behavior on the one problem used in the theorem.
For a law , a real threshold , and the model , the information number is the infimum of over those whose mean exceeds . The infimum is if there is no such . This is the definition on page 4. It measures how close an arm law is, in Kullback–Leibler divergence, to another admissible law that would give it a mean above the present optimum.
The main target is Theorem 2. For a model , a strategy smarter than uniform on it, a bandit problem , every arm , and every integer , the finite- case states
The theorem includes optimal and suboptimal arms. Its printed companion says that when , the arm receives at least expected selections. In the formal statement this threshold is , which also expresses the intended case . Both claims come from Theorem 2, page 10.
The milestone list follows the source's intermediate claims. Lemma 6, page 20 bounds Bernoulli relative entropy using the maximum of over an interval. The proof of Theorem 2 on page 11 states that Bernoulli relative entropy increases in its second argument on the interval starting at its first argument. The same page applies the paper's fundamental inequality (6) to the fraction of rounds spent on one arm, then states a lower bound against a single alternative arm law. These are the four curated milestones for the main theorem.
The theorem turns a model-relative performance condition into a numerical constraint on early sampling. If an arm's law is close in divergence to a law that would make it best, then the bound keeps its expected pull count near the uniform allocation until the horizon is large enough for the term under the square root to matter. It identifies the divergence scale at which this particular guarantee becomes weak. The paper contrasts this absolute bound with later relative and collective bounds that capture different dependencies on the number of arms in Section 3, pages 10–14.
The mathematical result is proved in the paper. The remaining work in this mission is a machine-checked development of the statement and its source-backed intermediate inequalities in the canonical stochastic-bandit model. The published bandit structure, policy kernels, and information number provide reusable foundations. Shared definitions supply the Bernoulli divergence, model predicate, and expected pull counts; the local strategy class makes the hypothesis of this particular theorem explicit. The Bernoulli inequalities and the pull-count change-of-measure statement can be reused in other lower-bound results.
A performance condition about optimal arms does not directly constrain an arm that is suboptimal in the problem of interest. The small-horizon bound must remain valid even though the strategy may adapt to observed rewards, and the relevant alternative arm laws can have divergences approaching an infimum without attaining it. The paper's lower bound is therefore sensitive to the exact orientation of the two bandit problems, the expected count multiplying their divergence, and the boundary conventions for Bernoulli relative entropy. Replacing the infimum with a chosen alternative or changing a divergence to an ordinary real with an arbitrary boundary value would alter the statement.
Lean uses arms Fin K, indexed from zero; the paper indexes them from one. The horizon is a natural number, and counts are integrated against the probability measure on -round histories generated by a stochastic kernel policy. Such kernels represent the arm-and-reward histories induced by the paper's strategies with auxiliary randomization. The model is a set of probability measures on whose identity function is integrable. The published StochasticBandit, BanditPolicy, and ConsistentBanditPolicy definitions supply the basic problem, history measure, pull count, means, and .
Bernoulli divergence and take values in . The real square-root formula assumes : when it is infinite, the paper's right-hand side is , while converting infinity directly to Lean's real value would produce a false numerical bound. The starting bandit problem is explicitly in , a condition needed for the proof's use of Definition 2 on a one-arm modification, although the printed quantifier on page 10 omits it. The arm parameter guarantees ; every target assumes , so its real divisions by and have the stated meaning.
A faithful development must retain Definition 2's quantification over all model problems and each optimal arm, rather than only over the bandit problem used in the conclusion. It must use the full Bernoulli relative entropy, including infinite endpoint values, and the infimum over precisely those model laws with mean greater than . The local instance of (6) also assumes integrable arm rewards in both bandit problems, as Section 1.1 requires. Contributions that establish the four milestones, the companion threshold claim, or reusable count-integrability and divergence facts are in scope.
In a stochastic multi-armed bandit, a decision maker repeatedly chooses one of several unknown reward sources. Sampling an arm reveals its reward but uses a round that could have been spent on a better arm. A good strategy must therefore reduce sampling of inferior arms, yet it cannot stop sampling them too early: it must still distinguish the current problem from a nearby one in which an apparently inferior arm is best. This tension produces the logarithmic lower bounds that benchmark bandit algorithms.
Garivier, Ménard and Stoltz revisit that benchmark in Explore First, Exploit Next. Their Theorem 5 gives a finite-horizon lower bound with explicit terms beyond the leading logarithm. It concerns every uniformly super-fast convergent strategy on a well-behaved model, not a particular algorithm. The distinction matters when comparing an algorithm's upper bound to what any strategy with that uniform performance guarantee must pay. The theorem is proved in the paper; this mission asks for a machine-checked statement and proof of that established result.
There are arms. Arm has an unknown probability distribution over real rewards, with finite mean . The vector is a bandit problem. Its best mean is , and the gap of arm is . An arm with is suboptimal. A strategy selects an arm each round using the previous arms and rewards, possibly with randomization. Write for the number of times it selects arm by round , and for the expected count under the problem .
A model specifies the probability distributions that an arm may have. All its laws have a finite first moment, and a bandit problem is in when every arm law belongs to it. For a law and a target mean , the paper's minimal information cost is
where an empty infimum is . This measures how much the law of an arm must change to make its mean exceed . The Bernoulli divergence used in the intermediate change-of-measure bound keeps its infinite values at the boundary.
Let be the interior of the set of expectations of laws in . A model is well behaved when positive functions and satisfy, whenever , , , and ,
A strategy is uniformly super-fast convergent with constant when for every problem in , every suboptimal arm, and every . The same constant applies throughout. Finally, records the inverse-squared gaps of all suboptimal arms.
For each suboptimal arm let . The goal is Theorem 5, with and
For every satisfying , , , and , the target is
The milestones follow the paper's displayed bounds: the one-alternative inequality (15), the optimized inequality (17), the inverse-information-cost bound after (17), and the product inequality quoted immediately before Theorem 5. They preserve the same constants and the same .
The leading term is the familiar distribution-dependent sampling barrier. The explicit , , and quantify the correction at a finite horizon; the paper observes that their combined contribution has order under its conditions. This makes the result useful when an algorithm's upper bound includes a second-order term and one wants to know the scale that a lower bound permits. It also identifies precisely which model regularity and uniform strategy guarantee support that comparison.
Formalizing Theorem 5 would add a reusable finite-horizon lower bound to the bandit library. The published definitions of stochastic bandits, policies, pull counts, and supply the base model; this mission adds the paper's well-behavedness and super-fast convergence predicates and states the intermediate inequalities as separate targets. The paper's proof is established mathematically, while these mission statements remain open Lean theorems until solvers supply machine-checked proofs.
The information cost is an infimum over alternative reward laws, so the finite-horizon bound must remain meaningful when the feasible set is empty or its divergence is infinite. The displayed formulas also divide by that information cost and use logarithms of quantities involving the strategy's uniform constant. For Theorem 5, the explicit correction factors must all lie in the range where the paper's final product inequality applies. A purely asymptotic statement would discard exactly the constants and horizon conditions that distinguish this theorem.
Arms are Fin K, so the paper's arm has Lean index . A strategy is represented by Markov kernels on observed arm-reward histories; its expected pull count is an integral of a bounded count. The model consists of probability measures on with integrable identity. The information cost and Bernoulli divergence live in ; a finite positive cost is converted to a real number only where a displayed reciprocal requires it. The goal contains a suboptimal arm, which rules out the empty-arm and single-arm cases. The model's witness functions are total in Lean, with requirements only on their paper-defined domains.
The theorem explicitly assumes and , which are implicit in the paper's use of and . It also assumes : the printed proof invokes a product inequality requiring that sign, although the theorem prints only . The version of (17) in the milestone list assumes in the case of a negative logarithm. These conditions and the model's integrability prevent vacuous or totalized-value readings of the lower bound. Contributions toward the four displayed milestones, the required measure-theoretic change of measure, and the finite-horizon arithmetic are in scope.
A seller with several goods can sell them one at a time or offer a mechanism that links allocation and payment across goods. Separate selling asks the seller to solve a one-good pricing problem for each item. A general mechanism can offer lotteries and menus whose outcomes depend on the buyer's whole valuation vector. The difference matters because the buyer's private information covers several values at once, and an optimal multidimensional mechanism need not resemble an ordinary posted price. Hart and Nisan ask how much revenue is guaranteed by simple selling rules when the joint valuation distribution is unrestricted apart from the stated independence assumptions (Hart and Nisan, arXiv:1204.1846v3).
This mission isolates their two-good, identically distributed result, Theorem B. The paper first gives a one-half guarantee for two independent goods with potentially different distributions, then improves the guarantee to when their distributions agree. The improvement is a claim about every probability law on nonnegative values. It assumes neither a density nor a regularity condition on the tail of that law. The paper proves the result in Appendix A.1 after stating it in the introduction (Hart and Nisan, pp. 6 and 31–35).
There is one risk-neutral buyer and one seller. For two goods, the buyer's private valuation is a vector with . Values are additive: receiving both goods is worth . The seller knows the distribution of the vector but not the realized values. In this mission, and are independent and have the same arbitrary probability law on . A law, rather than a named pair of random variables on a probability space, carries all the data needed by the revenue quantities.
A direct mechanism takes a reported pair and returns an allocation probability for each good and a real payment to the seller. The buyer's payoff from reporting truthfully is . The mechanism is incentive compatible (IC) if truthful reporting is at least as good as any other report for every possible valuation, and individually rational (IR) if truthful payoff is nonnegative everywhere. These requirements hold on the whole nonnegative orthant, as in Section 2.1 of the paper (Hart and Nisan, pp. 11–14).
Write for the expected payment under a valuation law and for the supremum of over feasible, IC, IR mechanisms. For one good, write . The separate-selling revenue for two identically distributed goods is . Equation (1) of the paper identifies the one-good value with the supremum of posted-price revenue ; the supremum formulation covers laws for which no maximizing price exists (Hart and Nisan, p. 12; Myerson, 1981).
The goal is the exact upper bound written at the start of the paper's proof:
Equivalently, separate selling guarantees at least of optimal revenue whenever the ratio has an ordinary meaning. The inequality itself is the stable formulation at zero and infinite revenues. The formal goal uses the exact constant , not the rounded percentage in the theorem's prose (Hart and Nisan, Theorem B, p. 6; proof, p. 31).
The milestones include the one-good posted-price identity, the fact that nonnegative payments suffice when optimizing, symmetrization for identical independent goods, Lemma 19's lower-valuation revenue bound, equation (12), and the two expectation estimates and final numerical bound used after it. Proposition 5's IC characterization is also a draft theorem, though it is not a milestone. Each statement retains its source's domain and the constant . The final inequality for the right side of (12) is stated for every nondecreasing allocation function into , as required by the paper's argument on pp. 33–35.
Theorem B gives a distribution-free quantitative guarantee for an easy-to-describe selling rule in a setting where the optimal rule may depend on the buyer's entire two-dimensional private type. Its guarantee is stronger than the one-half guarantee for merely independent goods stated as Theorem A. The conclusion concerns the best revenue available from all feasible IC and IR mechanisms, so the benchmark includes randomized allocations and payments depending on both reported values (Hart and Nisan, pp. 6 and 11–13).
The formalization target is a machine-checked version of a proved result, not a new conjecture. The proposal currently contains compiled Lean statements with unproved theorem bodies. A completed development would prove the stated inequality and its selected supporting results. It would also supply reusable definitions for direct mechanisms with additive nonnegative values, extended-real revenue, optimal revenue as a supremum, and symmetry of two-good mechanisms. No machine-checked proof of these proposed Hart–Nisan statements is claimed here.
The one-good posted-price formula does not directly control an arbitrary two-good mechanism: allocation of either good and the payment can depend on both reported values. Applying a one-good bound separately to the two coordinates therefore leaves terms that depend on the other coordinate. In particular, a direct comparison between each marginal posted-price optimum and the total payment loses the improved constant. The proof has to control the dependence created by a joint mechanism while retaining the exact numerical estimate. A second formal difficulty is that an admissible mechanism can have a negative expected payment even though optimal revenue is nonnegative, while an unrestricted law can give infinite optimal revenue. Replacing every expectation by an ordinary real integral or clipping each mechanism's revenue would change Lemma 19 and the intermediate inequalities (Hart and Nisan, pp. 31–35).
Valuations are finite vectors ; the main theorem fixes . The two-good law is the product of the same one-good probability measure in both coordinates, so independence and identical distribution are built into the data. The model represents allocation probabilities as real numbers with explicit bounds . It requires IC and IR pointwise on all reports. No positive transfer (NPT) means and is imposed only on supporting statements where the paper uses it. Following the paper's footnote 12, admissibility also requires the payment function to be measurable.
An individual expected payment is an extended real difference of positive and negative Lebesgue integrals. For IC mechanisms, the negative part is finite because the payment is bounded below by its value at zero. Optimal revenue is the supremum of the nonnegative clips of admissible mechanisms' expected payments; the zero mechanism makes this the same supremum as in the paper. Lemma 19 and equation (12) keep individual revenue in the extended reals. Supporting inequalities that write as a real number explicitly assume ; Theorem B does not. Integrals of bounded threshold functions use ordinary real expectation, while the nonnegative term uses a nonnegative Lebesgue integral. The goal cannot be satisfied by a correlated joint law, a bounded-support special case, a vacuous assumption on , or a rounded constant.
The reusable work includes one-good posted-price revenue for arbitrary laws, a nonnegative-transfer reduction, a faithful single-mechanism revenue type, and probability identities for two independent coordinates. Theorem A, Theorem 7, Theorem 16, and a full formalization of the paper's other selling rules are outside this mission.
The Decision-Estimation Coefficient (DEC) of Foster, Kakade, Qian and Rakhlin (arXiv:2112.13487) is a single complexity measure that bounds the minimax regret of interactive decision making (bandits, reinforcement learning, and their structured variants) from above and from below. Its lower bound (Theorem 3.2 of the paper) states that every algorithm suffers expected regret at least a constant times , so concrete lower bounds on regret follow from concrete lower bounds on the DEC of localized model classes.
The multi-armed bandit is the first test of this program. Its minimax regret is classical (Auer et al., 2002; Audibert and Bubeck, 2010). Section 5.1 of the paper recovers it through the DEC: posterior sampling (Proposition 5.1) and inverse gap weighting (Proposition 5.2) bound the DEC by from above, and Proposition 5.3 bounds it by from below. The lower bound is proved through a hard family of models (Definition 5.1, Lemma 5.1), the device that the paper reuses for linear, ReLU and gap-dependent lower bounds in §§6–7.
A decision space is a finite set; here , the arms. A model assigns to every arm a distribution over rewards in (observations are trivial). Its mean reward is , and is an optimal arm. The squared Hellinger distance between distributions on a finite set is (no factor , the paper's (5)).
For a class of models, a reference model and , the DEC (2) is
With , the -localized class (12) is .
A reference model and models , , form an -family (Definition 5.1) if there are with , , and . is the Bernoulli distribution with mean .
For arms, and every , with ,
The mission also states monotonicity of the DEC in the class (the step from the family to the localized class), Proposition 5.1 (posterior sampling bounds the dual square-loss DEC by ), and Proposition 6.7, the gap-dependent variant: for bandits with gap exactly , some in the class has . Proposition 5.2 (inverse gap weighting) and the decoupling step of Proposition 5.1 are already proved on the platform and are included as references.
Proposition 5.3 is the DEC half of the minimax lower bound for multi-armed bandits: combined with Theorem 3.2 and , it shows that the general DEC theory loses nothing in rate on the most basic interactive problem, and that the upper bounds of Propositions 5.1 and 5.2 are tight up to constants. Lemma 5.1 is reusable: any lower bound on the DEC of a class can be obtained by exhibiting a hard family, and the paper uses it for linear bandits (Proposition 6.2), ReLU bandits (Proposition 6.6) and gap-dependent bounds (Propositions 6.7, 6.8).
The results are proved in the paper. As far as is known, none of them is machine-checked. A formal development provides a verified Bernoulli Hellinger bound, a reusable hard-family lemma for the DEC as published on the platform, and the first verified DEC lower bound for a concrete class.
The DEC is an inf-sup, so a lower bound must hold against every exploration distribution . A natural first attempt picks a single alternative model and compares; this fails because can concentrate on the arm where that alternative differs and then the Hellinger penalty cancels the regret. The family must be spread so that no single is good for all of its members at once, and the constants must balance the regret term against the information term at the chosen . In Lean, an additional difficulty is that the DEC is written with real sInf/sSup, which are on empty or unbounded sets: every lower bound requires showing that the relevant sets are nonempty and bounded, and passing from the family to the localized class needs monotonicity of the DEC, which the paper uses without comment.
m : S → Y → ℝ with every m π a probability vector; expectations are finite sums. The DEC is the published FoundationsRL.GeneralDM.decGf, the Hellinger distance hellingerSq, the mean reward fM.Y = Bool, reward on true), a subclass of the paper's all-distributions-on- class. The DEC is monotone in the class and the localized class shrinks with the class, so the Bernoulli lower bounds imply the paper's.piStar with the hypothesis that it picks a maximizer of ; every statement holds for every such selector, so for whichever maximizer the paper meant (the reference has every arm optimal).decGf evaluate to the junk value ; the goal is stated over a class containing with bounded rewards, so the inequality is the genuine one, and its right side is strictly positive.Contributions welcome: proofs of the milestones in attack order, sorry-free lemmas on nonemptiness and boundedness of the DEC's inner sets (reusable for every DEC lower bound in this series), and a proof of the gap-dependent companion.
Generalized Turán problems ask for the maximum number of copies of a fixed graph in an -vertex graph that avoids a family of forbidden subgraphs. The ordinary Turán number counts edges (); Alon and Shikhelman (arXiv:1506.03397) started the systematic study of the general function , building on earlier results of Erdős on cliques, Bollobás and Győri on pentagons in triangle-free graphs, and Győri and Li on triangles in graphs without a long odd or even cycle. Counting cycles in graphs with forbidden cycles is closely tied to extremal problems for Berge hypergraphs, and the constructions used are sparse hypergraphs of large girth.
Gerbner, Győri, Methuku and Vizer, Generalized Turán problems for even cycles (arXiv:1712.07079, J. Combin. Theory Ser. B, 2020), determine or bound for many cycle families. This mission covers one of their results in §6.2: the number of odd cycles in a graph in which every shorter cycle is forbidden and, in addition, one longer odd cycle is forbidden. Its companion (Theorem 17, a separate mission of this series) forbids a longer even cycle instead, and there the paper obtains a sub-quadratic upper bound; with an odd extra cycle only a quadratic upper bound is proved.
All graphs are finite and simple. For an integer , is the cycle of length . For a set of integers , write ; a graph is -free if it contains no with as a (not necessarily induced) subgraph. The family consists of all cycles .
For graphs and , is the number of copies of in : subgraphs of isomorphic to , counted without labelling. The generalized Turán number is
For a vertex of , is the set of vertices at distance exactly from .
A hypergraph is a finite set of hyperedges (vertex sets); it is -uniform if each hyperedge has vertices. A Berge cycle of length is a sequence of distinct vertices and distinct hyperedges with and . The girth of a hypergraph is the length of its shortest Berge cycle; "girth at least " means there is no Berge cycle of length .
For all integers , as ,
Both the lower and the upper bound are part of the goal; the implied constants may depend on and only.
The supporting published theorem erdos_gallai_path_conjecture (the Erdős–Gallai path theorem: a graph on vertices with no path of edges has at most edges) is included as a reference item; the paper's proof of Claim 19 invokes it.
Theorem 18 shows that forbidding all cycles up to length together with one odd cycle still permits polynomially more than copies of , at least , and at most . Compared with Theorem 17, where an even cycle is forbidden and the count is , it isolates the role of the parity of the extra forbidden cycle. The authors conjecture that the true order is sub-quadratic (Conjecture 34, §8 of the paper), so the gap between the two exponents in Theorem 18 is a stated open question; a formal development of the known bounds is the base on which any improvement would be checked.
The result is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it produces: a reusable encoding of generalized Turán numbers for cycle families on top of Mathlib's copyCount; Berge cycles and the girth of uniform hypergraphs; distance layers ; and a formal statement of the Nešetřil–Rödl existence theorem, which is used as a black box by many extremal constructions.
The upper bound requires careful bookkeeping of distance layers around a vertex in a graph without short cycles. The obvious estimate, bounding the copies of through by the number of pairs of vertices of , gives only per vertex and hence nothing better than the trivial bound overall; the content of Claim 19 is that forbidding the single cycle makes the edge count inside linear, and the parity of is used essentially.
The lower bound rests on Theorem 29, a cited result that is not proved in the paper, and for which Mathlib has no supporting theory of uniform hypergraphs or Berge cycles. For the construction itself, the paper only asserts that the cycle-replacement graph has no short cycle other than the inserted 's; a cycle of the graph may wander through many hyperedges, and relating it to the girth of the hypergraph is the step a formal proof has to supply.
Fin n; graphs are SimpleGraph (Fin n). Cycles are Mathlib's SimpleGraph.cycleGraph, and is Mathlib's unlabelled copyCount.Set.Icc 3 (2 * l) ∪ {2 * k + 1}: every length , not only .edist, so vertices of other components lie in no layer.Finset (Finset V); "girth at least " is a predicate (no Berge cycle of length ), not an infimum, so a hypergraph without Berge cycles has every girth.Asymptotics.IsBigO along atTop, with real exponents; both directions of the goal are stated.A formalization that states only the upper bound, uses labelled copies, lets a constant depend on the graph, omits the short cycles from the forbidden family, or defines by a supremum that can take a junk value, does not prove this theorem.
Contributions welcome: proofs of the milestones, a proof of Theorem 29, and general lemmas on breadth-first layers in graphs of large girth, which are reusable by the companion missions of this series.
Neural networks trained by empirical risk minimization are sensitive to small adversarial perturbations of their inputs. Distributionally robust optimization addresses this by training against the worst distribution in a neighbourhood of the data distribution. Sinha, Namkoong, Volpi and Duchi (arXiv:1710.10571v5, ICLR 2018) take the neighbourhood to be a Wasserstein ball and relax the hard constraint to a Lagrangian penalty with multiplier . For large the inner maximization becomes strongly concave and is solved per data point by a transportation map , which turns each training example into its worst-case perturbation.
The average transport cost is the amount of robustness the trained model actually certifies on the sample: by the paper's duality result, the empirical worst-case loss at level is computable, and it is the certificate of robustness that the paper advertises. A certificate measured on the training sample is only useful if it transfers to the population. This mission formalizes the result that it does: concentrates around its population counterpart, uniformly over the parameter set.
Parameters range over a set and data over a set , both with the Euclidean norm. A transportation cost satisfies and Assumption A: is continuous and is -strongly convex for each . A loss satisfies Assumption B: its partial gradients , are Lipschitz in each variable, with constants .
For the problem is -strongly concave on , and the transportation map is its maximizer,
Given i.i.d. samples with and empirical distribution , the empirical robustness level and its population counterpart are
The complexity of enters through its covering number , the least number of points such that every is within of some ( if there is no finite such family).
Two alternative regularity conditions close the setting, with a constant : (i) is -Lipschitz on in each argument; or (ii) and is -Lipschitz. Put in case (i) and in case (ii).
For every ,
In case (i), and this is exactly the last display of the proof of Theorem 4 (p. 44); case (ii) is the "identical reasoning" the paper invokes with . is an arbitrary subset of : no compactness is assumed, and an infinite covering number makes the bound vacuous rather than false.
In the order the proof uses them:
The tail bound gives a -type generalization rate for the gap between the robustness certified on the sample and the robustness achieved on the population: with for bounded , the deviation is of order . It also implies, as the paper notes, that the certified level stays positive for large whenever the loss is not invariant to the data.
The paper states the result as Theorem 4, display (17), in "with probability " form with the constant . That form does not follow from the proved tail bound as printed: inverting the tail bound gives a deviation with a covering radius that depends on the deviation rather than on , whereas (17) uses in both places and drops and . The mission therefore poses what the proof establishes, the tail bound above, and does not claim (17). None of this paper's results has a machine-checked proof; Hoeffding's inequality and covering numbers are in Mathlib, the argmax stability and the cover argument are not.
Concentration at a single fixed is Hoeffding's inequality and carries no information about the trained model, whose parameter depends on the sample. The supremum over an arbitrary, possibly uncountable is the content. A union bound needs a finite family, and transferring control from a finite family to all of needs the deviation to be Lipschitz in . The deviation is built from the transportation map, which is an argmax and has no closed form; its regularity in comes only from strong concavity, which holds only for . In case (ii) the cost itself has no Lipschitz assumption, and the Lipschitz property of has to be extracted from the optimality of at two different parameters. Finally, the supremum event is not obviously measurable.
Spaces are EuclideanSpace ℝ (Fin d) and EuclideanSpace ℝ (Fin m); the paper's general norm is specialised to , in Assumptions A and B, in cases (i) and (ii), and in the covering number. The cost is real valued and constrained on only; the loss is typed on , but Assumption B and the argmax property of the transportation map are required only for and , matching the paper's . The transportation map is a function together with its argmax property. Samples are the coordinates of the product measure ; of the supremum event is its outer measure, so no measurability of the event is assumed. The supremum is a real supremum of quantities bounded by . The covering number is Mathlib's Metric.coveringNumber (closed balls, centres in , values in ). The definition on p. 9 does not say where the centres lie; the proof applies Hoeffding's inequality "for any fixed " at the centres, and the loss is only defined on , so the centres are taken in .
Hypotheses made explicit that the page leaves implicit:
Case (ii) is assumed for only, as printed in Theorem 4.
A bound for one fixed , a supremum taken outside the probability, a covering radius not tied to , or a covering number of a set other than would be a different and much weaker statement; the goal has the supremum over inside the event and the radius .
A complete development needs the stability of maximizers of strongly concave functions under Lipschitz perturbation of the gradient, a finite-cover union bound for outer measures, and Hoeffding's inequality for bounded i.i.d. coordinates of a product measure. The first two are reusable well beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for the goal.
In a prophet inequality, a gambler sees prizes one at a time and must decide when to stop, while a prophet knows every realization and takes the largest. A stopping guarantee compares the gambler’s expected prize with the prophet’s. The order of arrival changes the problem: here the prizes are independent but can have different distributions, and every permutation of their arrival is equally likely. Before seeing any prize, the gambler chooses a threshold for each distribution and accepts the first prize above its threshold. Such a rule has no need to update thresholds after observing rejections. Correa, Foncea, Hoeksma, Oosterwijk, and Vredeveld prove that this restricted rule still earns at least a fraction of the prophet’s expected maximum (Theorem 1, pp. 1455, 1459).
The random-arrival stopping model also supplies guarantees for posted-price mechanisms. A posted price gives a buyer a take-it-or-leave-it offer; the first buyer who accepts ends the sale. The paper explains the connection between its stopping rules and expected revenue under random buyer arrival (§1.1 and §5). This mission formalizes the stopping theorem itself, which is the mathematical guarantee used before that economic translation.
Let , and let be independent, nonnegative real random variables with known, possibly different distributions. Their realizations arrive in a uniformly random order. A nonadaptive threshold rule chooses constants before any realization is observed. It accepts the first arriving index with and receives . If no prize crosses its threshold, its reward is zero. An infinite threshold deliberately excludes an index. The strict comparison matches Theorem 1, even though an earlier description in §1.2 uses a weak comparison (pp. 1454–1455).
For fixed realized prizes, write . Conditional on the set of indices with , each accepted index is equally likely to arrive first. The conditional expected reward is therefore
The prophet benchmark is . The theorem compares with , including distributions for which either expectation may be infinite. The variables need no common distribution and no atomlessness assumption.
The paper’s main supporting result is the Bernoulli Selection Lemma. It starts with independent Bernoulli indicators of success probabilities , fixed real prizes , and a chosen subset . Its payoff is the average , again zero when the denominator vanishes. The lemma compares the best subset with a finite linear optimization problem over and (Lemma 1, p. 1455).
The goal is the exact constant of Theorem 1:
The quantifiers range over every finite nonempty family of independent nonnegative variables. The thresholds are deterministic and indexed by the distributions, and the assertion covers atoms as well as continuous laws. This is the paper’s headline nonadaptive result (Theorem 1, p. 1459).
The milestone list includes the paper’s multilinear formulation (4), its substitution (5), Proposition A.1, Lemmas 2 and 3, and the Bernoulli Selection Lemma. The latter states, in particular, that the maximum expected selected average dominates times the optimum over feasible . Two further milestones express the decomposition of the expected maximum and the upper-tail comparison used for continuous distributions (§2–3 and Appendix A). These targets fix the finite selection problem and the probabilistic quantities that the goal must connect.
The guarantee identifies what fixed, distribution-specific thresholds can achieve under random arrival: the expected accepted prize reaches a constant fraction of the prophet’s benchmark for every collection of independent nonnegative distributions. The paper also gives examples showing why a rule that keeps every positive prize is inadequate and studies where the factor is tight (§2.1 and §3.1). These are claims about the performance of a restricted class of stopping rules, not about an optimal adaptive strategy.
The paper proves Theorem 1; a machine-checked proof of this mission’s goal remains to be supplied. The finite Bernoulli model, its subset optimum, and the nonnegative expectation conventions would be reusable for other random-order stopping and allocation results. This mission makes the paper’s claimed constants, event comparisons, and boundary cases explicit in the theorem statements so a later proof has a fixed target.
Taking the first value above a single low threshold can accept a modest prize before a rare large one arrives. Raising every threshold can instead reject too many prizes. The paper’s example with a constant prize and a rare large prize shows that accepting all available values does not meet the claimed factor (p. 1460). The difficulty is obtaining one set of fixed thresholds that balances those risks across different distributions, while the benchmark selects the largest realization after seeing them all. The Bernoulli selection inequality carries the sharp constant; connecting it to general distributions must also account for ties and atoms.
Lean represents the index set by Fin n with , so its index zero is the paper’s index one. The existing published definition SamuelCahnProphet.Median.Setting.maxX supplies the sample maximum; this mission defines the strict accepted set and its real-valued reward ratio. Thresholds live in because the paper explicitly uses to exclude a variable. Expectations are nonnegative extended integrals of ENNReal.ofReal, preserving infinite values and avoiding a default zero for nonintegrable real integrals. The source’s nonnegativity assumption is represented almost surely, which is enough for these expectations and does not restrict the distributions further.
The Bernoulli law is a finite product formula. Its probabilities lie in , while prizes are arbitrary real numbers as in the printed lemma. The feasibility condition includes : these variables are probabilities, and allowing negative values would change the optimization problem. The finite subset optimum is an attained maximum. Proposition A.1 is stated for ; an empty contradicts the budget conclusion for . It also includes the printed case. Lemma 2 includes as printed: the removable division by zero in (6) is assigned its continuous value . The comparison milestones for continuous distributions assume atomlessness explicitly; the goal does not.
The accepted set depends only on fixed thresholds and the realized values. It cannot depend on the sampled arrival order or on prior observations. A constant choice such as accepting every positive prize does not prove the target guarantee. Contributions that establish the finite Bernoulli selection result, its analytic bounds, the random-order reward identity, or the passage from continuous to arbitrary distributions all serve the stated goal. The random-order identity and the discontinuous case are further work beyond the current milestone list.
Mobile devices run applications whose computational load can exceed what the device itself can serve in reasonable time and with reasonable battery drain. Computation offloading sends part of that load elsewhere: to a cloudlet, a small cluster of servers one wireless hop away, or to a distant cloud reached through the wide-area network. The cloudlet is shared, so its response time depends on how much load all users send to it, and each user's best offloading decision depends on everybody else's. Cardellini, De Nitto Personé, Di Valerio, Facchinei, Grassi, Lo Presti and Piccialli (Math. Program., 2016, DOI 10.1007/s10107-015-0881-6) model this as a non-cooperative game between users and study it with the tools of variational inequalities.
The game is a generalized Nash equilibrium problem (GNEP): not only the costs but also the feasible sets of the players depend on the other players' choices, because all users share one capacity constraint on the cloudlet. GNEPs with a shared convex constraint (jointly convex games) can be reduced to a single variational inequality, a reduction the paper takes from Facchinei, Fischer and Piccialli (Oper. Res. Lett. 2007, DOI 10.1016/j.orl.2006.03.004); Facchinei and Kanzow survey the area (Ann. Oper. Res. 2010, DOI 10.1007/s10479-009-0653-x). This mission formalizes the first step of the paper's analysis: the game has an equilibrium.
There are users and three tiers (mobile device, cloudlet, cloud). User chooses the fractions of its tasks run on each tier. A profile is .
The data are reals (arrival rates divided by service or transfer rates), powers , the number of cloudlet servers, the offloadable fraction and a utilisation cap . Assumption A requires and every to lie in .
User 's private feasible set is
the shared constraint is , and the joint feasible set is . User minimises the mean response cost
over . A solution of the GNEP is a profile at which no user can lower its cost by a deviation that keeps the shared constraint satisfied.
The map stacks the users' partial gradients,
and solves the variational inequality if and for all . Such solutions are the variational (or normalized) solutions of the game.
Under Assumption A, and provided every is nonempty,
Milestones 3 and 5 give the goal; milestones 1 and 2 are what milestone 3 rests on, and milestone 4 is what milestone 5 rests on. The platform's Proved statement of Brouwer's fixed-point theorem (AGT.brouwer_fixed_point) is included as a reference item for milestone 5.
The result. Existence of an equilibrium is the precondition for everything else in the paper: the monotonicity of (Theorem 1), the reformulation with a cloudlet price as an extended game (Theorem 2), and the distributed algorithm whose convergence is Theorem 3. Proposition 1 also shows that variational solutions exist, which is the specific equilibrium the paper's algorithm computes.
Formalizing it. The result is proved in the paper, in three lines that cite two textbook theorems. The work here is to make those citations machine-checked for this concrete model: that the closed-form is indeed the stacked partial gradient, that each user's problem is convex despite the rational cost terms, that the VI-to-GNEP reduction holds, and that a VI on a compact convex set with continuous map has a solution. None of these steps is formalized in Mathlib for GNEPs; the last is a finite-dimensional Hartman–Stampacchia theorem, which Mathlib does not contain. No part of this paper has a machine-checked proof.
The obvious argument is to apply Kakutani's theorem to the best-response correspondence. With a shared constraint this needs lower semicontinuity of the feasible-set map , which is a separate argument, and Kakutani is not in Mathlib either. The VI route avoids it but has its own points. The cost has the rational terms and , and convexity and differentiability must be checked on the region where the denominators are positive; on a user's feasible set this needs Assumption A and the shared constraint, not the private constraints alone. The existence of a VI solution needs a fixed-point theorem on a compact convex set, and Mathlib has no Brouwer theorem. That is why the platform's statement of it is attached to this mission.
Users are Fin N (0-based) and tiers an inductive type Tier with three constructors; a profile is Fin N → Tier → ℝ. The inner product is the coordinatewise double sum (not Mathlib's sup norm on Pi types). The cost and are the paper's closed forms; is not defined as a derivative, so milestone 1 has content. Lean's makes both formulas junk where a denominator vanishes. Under Assumption A both denominators are positive on and at every point the GNEP definition compares, and milestone 1 assumes the two positivity conditions explicitly.
Standing hypotheses in every statement: Assumption A, , . Nothing is assumed of or the powers, as in the paper. Added hypothesis: every is nonempty, in the goal and in milestone 5. The printed proposition is false without it: if then , so . The condition is equivalent to . Milestone 4 adds convexity of to the paper's "continuous and compact".
Trivializing formalizations are ruled out: cannot be empty under the added hypothesis, is not a derivative by definition, no statement evaluates the cost at a point with a vanishing denominator, and the GNEP keeps the shared constraint in each player's feasible set (dropping it gives a different game, a NEP).
Contributions welcome: a finite-dimensional Hartman–Stampacchia theorem (reusable well beyond this mission), the general VI-implies-GNEP reduction for jointly convex games, and proofs of the model-specific milestones.
In many production and service settings a single resource is shared by parties with different goals: two departments sending orders to the same machine, two customers of a contract manufacturer, or two classes of requests on one processor. Multi-agent scheduling models this directly. Each agent owns its own jobs and its own objective, and a schedule is judged by the pair of objective values it gives the two agents rather than by a single combined criterion.
Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004, pp. 229–242) set up the systematic study of the two-agent single-machine problem. For each pair of classical objectives they ask how hard it is to optimise one agent's objective while the other agent's objective stays within a given bound. This mission formalises their §9, the case in which both agents minimise their own total completion time. With a single agent, minimising the total completion time is solved by sorting the jobs by length (the shortest-processing-time rule of Smith, 1956). §9 shows that two agents, each with this easiest of objectives, already give an NP-hard problem (Theorem 9.2), and that the problem is solved in pseudopolynomial time by a dynamic program (Theorem 9.3).
There are two agents, A and B. Agent A owns jobs with processing times ; agent B owns jobs with processing times . All jobs are available at time and are processed on one machine, one at a time, without interruption. Since both objectives are nondecreasing in the completion times, a schedule is a sequence of all jobs processed back to back from time . The completion time of a job is the total processing time of the job and of all jobs before it. Agent A's cost is and agent B's cost is .
The recognition problem asks, for thresholds , whether some schedule has
The source problem is PARTITION (Problem 9.1): given integers with , is there a set with ?
The paper's reduction numbers the integers so that and gives both agents identical job sets, jobs of lengths , with thresholds , where
Writing for the pair , an SPT schedule processes in order, each pair in either internal order; denotes the total length of the pairs in which B goes first.
Here is polynomial-time many-one reducibility between languages of binary codes: a polynomial-time Turing-machine-computable map on strings that sends codes of PARTITION yes-instances, and only those, to codes of yes-instances of the recognition problem. Together with the NP-completeness of PARTITION (Karp 1972) this is the statement " is binary NP-hard".
With each agent's jobs numbered by nondecreasing length and the total length of , the recursion
with for and for yields , and when no schedule meets the bound.
Theorem 9.2 fills one cell of the paper's complexity table: even when both agents use the objective that is trivial for one agent, sharing the machine makes the constrained problem NP-hard. Together with Theorem 9.3 it places exactly: NP-hard under binary encoding, solvable in pseudopolynomial time, hence not strongly NP-hard unless P = NP. The later literature on two-agent and multi-agent scheduling (for example the monograph of Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal, Multiagent Scheduling, Springer 2014) cites this classification.
Neither result has a machine-checked proof that we know of. The mission adds a formal record of the reduction and of the dynamic program, reusable definitions for the two-agent total-completion-time problem, and a correction of the printed proof: the equivalence between PARTITION and the constructed instance, as printed, holds only when the integers are pairwise distinct. For PARTITION has no solution, yet a schedule meets for both agents. Theorem 9.2 itself is not affected, since PARTITION remains NP-hard, but a complete formal proof needs a reduction that is correct on every input.
The equivalence for distinct integers rests on two facts: the overall total is at least for every schedule, with equality only for sequences in nondecreasing order of length; and, with distinct lengths, such a sequence is made of consecutive pairs, whose split is controlled by . The naive formal argument stops at the second fact, which is false with repeated lengths: a block of equal-length jobs can be shared between the agents in ways no sequence of pairs realises. The goal adds the encoding layer: the reduction must be computable in polynomial time on a Turing machine, must handle repeated and zero sizes and odd (where is not an integer and the language's thresholds are), and must send strings that do not code a PARTITION instance outside the target language. For Theorem 9.3, the dynamic program is correct only because some optimal schedule orders each agent's jobs by length, and the constraint makes this exchange argument less direct than for a single agent.
Jobs are Fin nA ⊕ Fin nB (Sum.inl h is , Sum.inr k is , 0-based). Schedules, completion times and the idle-free sequence model are the published MooreLateJobs.Shared.completionTime (Moore 1968 series): a schedule is a duplicate-free list containing every job once, and completion times are real numbers. Processing times and thresholds of the language are natural numbers. Reducibility is the published CookPvsNP.PolyReducible, and PARTITION, the alphabet and the binary codes are the published ProjSchedTW.Complexity.Encoding (partitionLang, whose sizes are natural numbers including ). The target language allows any job counts and any processing times; identical job sets are a property of the construction only.
The following readings are explicit:
The goal cannot be met by a trivial reduction: PolyReducible requires the map to be computed by a polynomial-time Turing machine and to be correct on every string, and the target language contains every two-agent instance, not only those with identical job sets. Contributions welcome: the exchange lemmas for total completion time on the shared sequence model, the SPT formulas, and Turing-machine constructions for list sorting and arithmetic on binary codes, which other reductions of this series reuse.
In many production and logistics settings a single resource is shared by parties with different goals: two departments of a plant that send orders to the same machine, two customers of a contract manufacturer, or two classes of traffic on one processor. Multi-agent scheduling models this directly. Each agent owns its own jobs and its own objective, and a schedule is judged by the pair of objective values it gives the two agents rather than by one combined criterion.
Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004, pp. 229–242) set up the systematic study of the two-agent single-machine problem. For each pair of classical objectives they ask how hard it is to optimise one agent's objective while the other agent's objective stays within a given bound. Their Table 1 lists the outcome for each pair. This mission formalises one entry, Theorem 5.2: when agent A minimises its total weighted completion time and agent B only requires its makespan to stay below a bound, the problem is NP-hard under binary encoding of the numbers. The corresponding single-agent bicriteria problem had been shown NP-hard in the strong sense by Lenstra, Rinnooy Kan and Brucker (1977); the two-agent version differs because only B's jobs are constrained.
There are two agents, A and B. Agent A owns jobs ; job has a processing time and a weight . Agent B owns jobs with processing times . All jobs are available at time and are processed on one machine, one at a time, without interruption.
Because both objectives are nondecreasing in the completion times, there is no reason to leave the machine idle, so a schedule is a sequence of all jobs processed back to back from time . The completion time of a job is the total processing time of and of all jobs sequenced before it. Agent A's cost is ; agent B's cost is its makespan .
The paper's recognition problem asks, for given thresholds , whether some schedule has
The source problem is KNAPSACK (Problem 5.1): given nonnegative integers , and integers , is there with and ?
Here is polynomial-time many-one reducibility between languages of binary codes: a Turing-machine-computable, polynomial-time map on strings sending codes of KNAPSACK yes-instances, and only those, to codes of yes-instances of the recognition problem. Together with the NP-completeness of KNAPSACK (Garey and Johnson 1979) this is the statement " is binary NP-hard".
The paper's reduction builds, from a KNAPSACK instance, the two-agent instance with , , a single B-job of length (where , ), and thresholds , . The milestones are the two directions of the proof and their combination:
Theorem 5.2 fixes the complexity of one cell of the two-agent classification. It shows that the polynomial algorithm for the unweighted case (Theorem 5.5 of the same paper) cannot be extended to arbitrary weights unless P = NP. Through §8 it also settles . The hardness is binary, not strong: the reduction produces numbers of size about , so pseudo-polynomial algorithms are not ruled out, which is consistent with the dynamic programs studied in later two-agent literature.
The result is proved in the paper; no machine-checked proof is known to exist. Formalizing it produces a complete reduction from a two-constraint knapsack problem to a scheduling recognition problem, with the encoding, the degenerate instances and the polynomial running time all made explicit. The model and the KNAPSACK language are reusable by other two-agent reductions (Theorems 9.2, 10.1 and 10.2 of the paper reduce from PARTITION in the same frame).
The two directions of the equivalence are short computations with completion times. The printed argument, however, is not correct as written in two places. The bounds "smaller than " and "smaller than " in the derivation of (1) hold only with equality allowed. The strict inequalities in (2) fail when , and then the reduction itself fails: with all and the KNAPSACK instance is a no-instance while the constructed instance has and every schedule meets both thresholds. A complete reduction must recognise such instances and treat them separately.
The construction also produces integer thresholds that can be negative (, or ), while instances of the target are coded with natural numbers. Finally, the reduction must be a polynomial-time Turing machine computation over binary codes, including the decoding of arbitrary strings and the binary multiplication ; that is where most of the formal work lies.
Fin nA ⊕ Fin nB (0-based: Sum.inl h is , Sum.inr k is ). Schedules and completion times are the published MooreLateJobs.Shared sequence model (IsSchedule, completionTime) of the Moore (1968) series: a duplicate-free list of all jobs, processed without idle time from time . Integer processing times are cast to .CookPvsNP.PolyReducible (Cook's Definition 3, one-tape Turing machines). Codes use the published binary encoding ProjSchedTW.Complexity.Encoding (alphabet BSym, encNat, encInt) of the Neumann–Schwindt–Zimmermann series. A KNAPSACK instance is coded as the integers ; a target instance as the natural numbers , the processing times and weights, and . The target language allows any ; the reduction uses .Contributions welcome: proofs of the two directions, of the equivalence, the treatment of the degenerate instances, and the Turing machine for the reduction, which would also serve the other binary-coded reductions on the platform.
That noncooperative play usually wastes something is part of the folklore of game theory, with the Prisoner's Dilemma as its emblem: each player's best reply leads to an outcome that both would trade for another. Pradeep Dubey's paper turns this folklore into a theorem about smooth games. For games whose payoffs are twice continuously differentiable, and for all payoffs outside a negligible (closed, nowhere dense) set, Nash equilibria are finite in number and are Pareto-inefficient unless some player sits at a vertex of his strategy set. The same conclusion applies to Nash's mixed extensions of finite games (Nash 1951), where a vertex is a pure strategy.
The question is basic to welfare analysis of strategic interaction: market games, oligopoly, public goods and trading mechanisms (Shapley and Shubik 1977) all ask whether equilibrium outcomes can be efficient. Dubey's answer is that efficiency of an equilibrium is non-generic, so a model that delivers it is exploiting special structure.
Timeline. Nash (1951) introduced equilibrium points and multi-matrix games. Smale (1973, "Optimizing several functions") gave the first-order condition for Pareto optimality of several smooth functions: at an efficient interior point the gradients are linearly dependent. Harsanyi (1973, IJGT 2:235–250) proved that generic finite games have finitely many, indeed an odd number of, mixed equilibria. Dubey's Cowles Foundation Discussion Paper 508R (1978) stated finiteness and inefficiency; the version formalized here is the rewrite IIASA WP-83-74 (1983), published as Mathematics of Operations Research 11(1):1–8 (1986).
There are players . Player 's strategy set is the unit simplex
whose vertices (extreme points) are the origin and the unit vectors. Profiles range over , .
Fix open neighbourhoods and . The space consists of the functions with finite -norm . A game is . For , replaces by for . A profile is -efficient if no gives for all with strict inequality for some . It is a Nash equilibrium if it is -efficient for each , efficient if it is -efficient, and a strong Nash equilibrium if it is -efficient for every . The three sets are , , .
In the proof, is the matrix with rows ; is the subspace of matrices whose -th row vanishes on player 's block of columns; is the set of matrices with linearly dependent rows.
There is an open dense set such that for :
For interior profiles ( for all ):
; the linear perturbation satisfies (the computation behind (**)); claim (*) for : for an open dense set of games is transverse to on a compact neighbourhood of ; under that transversality is finite; and the Theorem restricted to interior profiles.
The Theorem (Multi-Matrix) (p. 14): for an open dense set of payoff vectors , the mixed Nash equilibria of are finite, an efficient one has a player using a pure strategy, and a strong one is pure. From the example of §3: every game on with payoffs has a unique Nash equilibrium (p. 9); Lemma 1, (p. 9); Lemma 2(a), an interior equilibrium is efficient iff or (p. 10).
The theorem gives the generic structure of equilibrium sets in smooth games: isolated and finitely many equilibria, and a sharp location of the only places where efficient equilibria can survive, namely the vertices. It explains why efficiency results for noncooperative models need boundary solutions or non-generic structure, and in its multi-matrix form it shows that strong equilibria of generic finite games are in pure strategies. It also supplies the finiteness of equilibria used in comparative-statics and index arguments.
On the formalization side, the result is proved on paper but has no machine-checked version. A complete development would give Lean its first generic-finiteness theorem for Nash equilibria of smooth games, a first-order Pareto condition in the form of Smale's lemma, and a parametric transversality argument in finite dimensions. The multi-matrix companion connects to the published vocabulary of finite games (agt_games), and the example of §3 is an elementary, fully explicit check of the general picture.
The interior case reduces, by (i) and (ii), to a dimension count: should be zero-dimensional and empty. Neither holds for every game: they hold only when is transverse to and to the strata of , and the step that requires work is showing that transversality is an open and dense condition in the topology. Density is not obtained by adding linear functions to the payoffs: a linear function has finite -norm on only when is bounded, so perturbations must be localized. The step from interior profiles to the whole of is a second difficulty. It requires repeating the argument on every product of faces of the simplices and on every subgame, and then intersecting finitely many open dense sets. Efficiency at a boundary point is not -efficiency in a subgame, so the reduction has to be made with care.
Players are Fin n with 2 ≤ n; block sizes k : Fin n → ℕ with 1 ≤ k i; profiles are ∀ i, Fin (k i) → ℝ. The simplex is the paper's corner simplex {x ≥ 0, ∑ x ≤ 1}, not the probability simplex; "vertex" is Set.extremePoints. The neighbourhoods are taken open, and the goal is stated for every such choice, not assuming bounded or convex. Payoffs are total functions; a game is ContDiffOn ℝ 2 on with finite -norm, which takes values in , so no junk real supremum enters. "Open dense in " is written in -form for the product of -norm topologies; Lean's sup-type norms are equivalent to the Euclidean ones, so the open dense sets are the same. Deviations range over all strategies in , not only pure or vertex deviations.
Added hypotheses, all disclosed in the items: openness of ; interiority of every on milestones (i), (ii) and the finiteness step (the proof's standing case assumption); in claim (*). The printed "By (i), " is stated for interior equilibria, which is where (i) applies.
A trivializing formalization is ruled out: the open dense set must contain games arbitrarily close to every game (the zero game is a game, so it is never empty), interiority appears only in the milestones and not in the goal, and efficiency is with respect to all deviations in .
Not stated: (*) for a general submanifold , and the decomposition of into submanifolds of codimension , both of which need embedded submanifolds of ; Remarks 1–4 (Remark 4's openness claim for strictly concave payoffs is false as printed); Lemma 2(b); §5, which the author leaves as a conjecture. Contributions welcome: a finite-dimensional parametric transversality theorem, Smale's first-order Pareto condition, and the face-by-face reduction.
Nonlinear model predictive control (NMPC) computes a feedback law by solving, at every sampling time, an optimal control problem that starts from the currently measured state. The control actually applied is the first control of that problem's solution. When the dynamics are fast relative to the time an optimizer needs, solving each problem to convergence is impossible, and the delay between measuring the state and applying the control degrades or destabilises the closed loop.
Diehl, Bock and Schlöder (SIAM J. Control Optim. 43(5), 2005) analysed the real-time iteration: a scheme that performs a single Newton-type iteration per sampling time and then moves on to the next problem. The scheme is the basis of widely used NMPC software (for example the ACADO toolkit and acados) and of much of the later theory on suboptimal and "anytime" MPC. The paper's Theorem 4.1 is the first contraction result for it; Theorem 5.1 bounds the price paid in closed-loop cost for not solving each problem to optimality.
A discrete-time system , , has states and controls . For and a state , the shrinking-horizon problem is
Its primal-dual vector is and its Lagrangian is
The projection drops the block .
A Newton-type method solves by steps , where is the KKT matrix with its Hessian blocks (and the terminal block) replaced by approximations, for instance those of the constrained Gauss–Newton method. The real-time iteration starts from a guess and, for , computes for , applies , lets the system evolve to , and sets .
The analysis uses a neighbourhood and its projections , norms on with and , two constants (the Hessian approximation error) and (a Lipschitz-type constant of ), the rates , and the ball .
Assume is twice continuously differentiable on , is continuous with bounded inverse on , the conditions (4.1a)–(4.1c) hold with , and . Then for
for
and the Newton-type iterates of started at converge to a stationary point with
No constant is chosen by the formalization: all of them are the paper's.
The proof has three parts (contraction, well-definedness, distance to the stationary points). The milestones are its steps: the gradient transition identity between consecutive problems; the block identity ; the one-step contraction; the recursion ; the lifting of a nearby point of to ; the contraction (4.7) of the Newton-type method on a fixed problem; and the convergence of those iterates to .
If moreover on , then , and for the loss is . The intermediate estimate (5.4), , is a separate item.
Theorem 4.1 says that a scheme which never solves any problem to convergence still produces iterates that contract at the rate of the underlying Newton-type method and approach the exact solutions of the problems along the closed loop, geometrically. It justifies the "one iteration per sample" design of real-time NMPC under explicit, checkable conditions on the Hessian approximation, and its constants are those of the classical affine-invariant Newton-type convergence theory, so it extends to Gauss–Newton and other approximations. Theorem 5.1 turns the contraction into a closed-loop performance guarantee: the suboptimality is quadratic in the first step, quartic for exact Newton.
The results are proved in the paper; none is formalized. A formal proof would supply the details the paper leaves implicit (that the segments used by the integral mean value theorem stay in the domains, that the ball around lies in ), would give a reusable Lean model of discrete-time optimal control problems with their KKT structure and shrinking-horizon projections, and would make the classical local contraction argument for Newton-type methods available for general norms.
Each single estimate is a variant of the textbook local convergence proof for Newton-type methods. The difficulty is that the real-time iteration changes the problem at every step: the next step is computed for a different, smaller problem at a different initial state, so the textbook argument does not apply as is. The proof needs two structural facts that tie consecutive problems together, the gradient transition along the undisturbed closed loop and the block identity of the Hessian errors, together with the compatibility of the norms with the projections. A second obstacle is well-definedness: the iterates must be shown to stay in regions where the hypotheses hold, which requires tracking the projections of through all shrinking spaces.
is a Euclidean space whose coordinates are indexed by (multiplier, state or control block, stage, component) for the stages ; is a restriction and its transpose the extension by zero. The gradient and Hessian are Mathlib's gradient and fderiv; the inverse is ContinuousLinearMap.inverse. The approximations of the stage Hessian blocks depend on (the paper's misprinted read as ), the terminal block may be approximated as in §2.2, and symmetry of the approximations is not required. The norms are a structure carrying the norm axioms and the two compatibility conditions. The real-time iterates follow the undisturbed closed loop. The hypotheses (4.1a)–(4.1c) are imposed at the points of where the paper's functions are defined, that is, for with ; no convexity of is assumed. Theorem 5.1 is stated with Euclidean norms on every , because its last step bounds by ; is the objective at the primal part of , not an infimum.
Mathlib's inverse is at a non-invertible operator and its derivative is at non-differentiable points; either junk value would make every step vanish and every bound trivial. The statements therefore require invertibility and twice continuous differentiability at the points of , keep the membership (4.2) as a conclusion, and pin as the limit of the Newton-type scheme started at , so it cannot be chosen after the fact. Degenerate norms are excluded by the norm axioms.
Some milestones add a hypothesis that Theorem 4.1 supplies internally: a segment , the ball around the starting point contained in , or for the abstract δ-recursion. Contributions welcome: proofs of the milestones, a sorry-free instance of the hypotheses for a linear-quadratic problem, and general lemmas on the integral mean value theorem for gradients in arbitrary norms.
The Riemann zeta function at a real number is the convergent series . Number theorists studying its special values distinguish between proving that a family contains irrational numbers and determining the arithmetic nature of one specified member. This mission asks for a proof that is irrational. The target remains unproved in this development; the supporting results below do not close it.
Two landmarks explain the distinction:
An integer linear form in the target value is , where . It is useful for irrationality only when its actual value is nonzero and tends to zero along an infinite sequence. A pair is primitive when ; its direction identifies with .
The principal construction uses even integers and the rational function
For a polynomial with rational coefficients, set and . Its actual partial fractions and harmonic sums determine rational coefficients in the exact identity
The coefficient map sends to this ordered row of five rational coefficients. The matrix has row equal to the coefficient row of , for . These are coefficients constructed from the actual rational function; their definition does not assume independence of odd zeta values. The map is bijective over for every even in the completed supporting theorem The actual five-dimensional rational coefficient map is bijective. This later theorem is separate from the dated source packages.
The integer-output lattice consists of the rational polynomial-coordinate rows
Its weighted norm is the Euclidean norm after multiplying coordinates by . A shortest nonzero row has a primitive integer output; a fixed convention resolves ties. An integer output can have a rational polynomial preimage. Integer polynomial coefficients and their denominator cost require additional arithmetic statements.
The stable goal is
The goal imposes no chosen decay constant or prescribed construction. The coefficient-map route supplies supporting targets; a complete independent construction of nonzero integer linear forms tending to zero would also settle the goal.
The joint-margin condition J in the research notes asks for a fixed positive exponent margin on infinitely many even indices in the actual weighted-lattice and arithmetic diagnostics. It remains mathematically open. Under the written volume and transport results, it is an equivalent exit to the target and to failure of eventual fixation of the shortest primitive output direction. The stronger shape condition S is sufficient with the written volume estimate; it is not an additional necessary hurdle. Precise conditions and dependencies.
A complete proof would determine the arithmetic nature of one specified odd zeta value. The formal development also produces reusable links between rational-function coefficients, absolutely convergent series, polynomial inverse images, and primitive integer outputs.
Completed machine-checked supporting stages include harmonic-denominator clearing and stability, finite-prime arithmetic, the actual short-zero coefficient's signed lower bound and nonvanishing, and unconditional harmonic denominator rates using an actual prime-number-theorem dependency. The coefficient route has complete proofs of highest-pole identities, all nine local orders, full local-array injectivity, global partial fractions, reflection and cancellation, finite harmonic identities, absolute summability, and the exact infinite linear form. Its genuine aggregate map is bijective over rational quartics for even , with a unique rational preimage of every rational target. The actual fifteen-coordinate connection system also has unique polynomial solutions for every . The supporting results The actual inverse multiplier has its prescribed sum and absolute convergence and The five original connection systems have unique bounded rational solutions state these later conclusions with their exact domains.
The 7 October 2026 authenticated readback reconfirmed the 51 complete accepted supporting proofs and their public Proved statements. The irrationality goal remained Open. The three separately published explicit-matrix statements were also Open; local Matrix proofs and completed kernel-and-inverse results do not imply platform acceptance of those separate statements. These are statuses of existing supporting results, not a completion count for this new mission.
Public supplements provide independently rebuilt sources for nine complete proofs and for the later coefficient-sign and unconditional denominator-rate developments. Each package records its precise scope and standard foundational axioms. They do not contain a proof of the root goal. Nine-proof supplement, advanced source supplement, independent source-package review.
Small real values alone do not settle irrationality: an integer form may be exactly zero. Under a rationality assumption, the shortest primitive output can eventually follow the unique integer zero relation. The existing volume and approximation estimates do not exclude that behavior. Finite changes of direction, large matrix determinants, or a few certified small nonzero forms do not establish the required infinite assertion. Direction frontier and boundaries.
Alternative routes retain different gaps. Growing-dimensional positive Gram constructions have positive exponentially decreasing real errors but lack control of the full reduced denominators. A differentiated rational-sum construction isolates but has polynomial endpoint leakage; its eightfold-zero repair removes that leakage and still needs eventual nonvanishing, the actual analytic rate, and primitive-content estimates. These are alternatives, not conditions that must all be solved. Alternative constructions and exact boundaries.
The Lean goal applies Irrational to the real part of Mathlib's complex
riemannZeta at . The coefficient construction fixes rational quartics,
the output order , and even for
the inverse and infinite identity. Connection results retain their own
domain and regular-point hypotheses. Saturated integer kernels,
positive common denominators, Smith factors, primitive normalization, weighted
norms, and shortest nonzero vectors must use the actual objects in the notes.
An arbitrary replacement map, zero witness, or hypothesis already asserting
the required transport or infinite margin cannot discharge these targets.
Four principal formalization work packages remain:
These four packages distinguish remaining Lean work from the separate missing mathematical input for J. Rational matrices, integer modules, formal power series, summability, asymptotic analysis, and geometry of numbers are reusable infrastructure. Faithful formalizations, independent audits, and new mathematical approaches are welcome. Written research record.
A risk-controlling prediction set is a set-valued predictor that, with probability at least over a calibration sample, has expected loss at most a target level . Bates, Angelopoulos, Lei, Malik and Jordan (arXiv:2101.02703, J. ACM 2021) build such sets for any black-box predictor and any bounded loss by a procedure called upper confidence bound (UCB) calibration: for each value of a tuning parameter , compute from the calibration data an upper confidence bound for the risk , and pick the smallest beyond which all these bounds sit below . The guarantee of the procedure (their Theorem 1) holds for any choice of the pointwise bound, so the size of the resulting sets is governed by how tight that bound is.
The paper compares several such bounds: Hoeffding, Bentkus, the empirical Bernstein bound of Maurer and Pontil, and a bound adapted from the hedged capital confidence interval of Waudby-Smith and Ramdas (arXiv:2010.09686). The last one, the Waudby-Smith–Ramdas (WSR) bound, adapts to the unknown variance of the loss and is the one the authors recommend for non-binary losses; their experiments use it throughout. Proposition 5 of the paper states that the WSR bound is a valid upper confidence bound for the mean of a -valued loss. This mission formalizes that proposition.
Timeline: Ville (1939) proved the maximal inequality for nonnegative supermartingales that underlies all betting-based confidence bounds. Waudby-Smith and Ramdas (2020) introduced the hedged capital process and its confidence sequences for bounded means. Bates et al. (2021) extracted the one-sided, fixed-sample variant stated as Proposition 5, with the explicit betting fractions below.
Fix the tuning parameter ; it is dropped from the notation. The calibration losses are independent and identically distributed with law on (the loss is nonnegative and, by the standing assumption of §3.1 of the paper, bounded by one), and their mean is the risk
Fix a level . For define the running mean and variance
so , and for the betting fraction
which depends only on . For a candidate mean , the capital process is
the wealth of a gambler who, starting with one unit, bets the fraction of their wealth against the hypothesis that the mean is . The WSR bound is
the smallest candidate mean the gambler has discredited by multiplying their wealth by more than . In Lean these are obs, muHat, sigmaSqHat, nu, K and wsrUCB in the namespace RiskControl.WSR, and is filt n.
For and ,
the probability being the product law of the sample.
The result is the validity half of the WSR bound: with it, UCB calibration (Theorem 1 of the paper) applied to gives the paper's Theorem 4, a risk-controlling prediction set built from the variance-adaptive bound that the experiments of the paper use for classification, segmentation and protein-structure tasks. It is also a self-contained instance of the betting approach to confidence bounds for bounded means, which now underlies a family of nonasymptotic, variance-adaptive procedures in statistics and machine learning.
The proposition is proved in the paper (p. 26), following the proof of Theorem 4 of Waudby-Smith and Ramdas. To our knowledge neither it nor the hedged capital construction has a machine-checked proof. The mission produces one: a Lean statement of the WSR bound with its exact constants, and a proof that reuses the platform's Ville inequality. The capital process and its martingale property are the reusable part; the same construction with other predictable betting fractions gives other confidence bounds.
The bound is not obtained by inverting a tail inequality for the empirical mean, so Hoeffding- or Bernstein-type arguments do not apply. The probabilistic core is the martingale step: one must show that is a measurable function of only (it involves , which involves every for ), and compute a conditional expectation on the product space using independence of the coordinates. Ville's inequality then holds only at the true mean , a single unknown point, while is an infimum over all candidate means; the passage between them needs the monotonicity of in its argument, which fails without the bound (a factor can turn negative). A union bound over candidate means, the first idea, gives nothing here.
The sample is under Measure.pi (fun _ => Q), with for (1-based indices as on the page). is the law of the loss for the fixed , assumed concentrated on : this is the §3.1 standing assumption together with . The goal adds two hypotheses implicit on the page: and (so that ). The empty sum gives ; "" is written as an existential over ; the infimum is an extended-real infimum, equal to when no candidate qualifies. The failure probability is bounded through the outer measure of , which equals the page's statement for a measurable event. The martingale is extended constantly past time so that it is indexed by .
Two printed slips are corrected: the proof's "then " (a stray ) is stated as the event, and "increasing in " is stated as nondecreasing on .
The infimum must not be a real infimum: a real sInf of an empty set is , which would make true for every positive mean and the goal false; with the extended-real infimum the empty case gives , and the goal is the paper's proposition, not a vacuous one.
Contributions welcome: the measurability of with respect to , conditional expectations of products of independent coordinates under Measure.pi, and a finite-horizon form of Ville's inequality (Mathlib's Doob maximal inequality MeasureTheory.maximal_ineq is an alternative route).
General relativity predicts that a black hole, once it has settled down after collapse, retains almost no memory of the matter that formed it. The no-hair theorem, also called the black hole uniqueness theorem, states that all stationary black-hole solutions of the Einstein–Maxwell equations are completely characterized by three externally observable parameters: mass, angular momentum and electric charge; all other information ("hair") disappears behind the event horizon. The phrase "black holes have no hair" was popularized by John Archibald Wheeler. Its observational content is tested in gravitational-wave ringdown signals and in black-hole imaging.
Despite its name, there is no rigorous proof of the general statement: mathematicians refer to it as the no-hair conjecture.
Timeline.
Counterexamples are known in dimensions above four, for non-abelian Yang–Mills fields and for some non-minimally coupled scalar fields; this mission concerns only the four-dimensional Einstein–Maxwell theory with zero cosmological constant.
A spacetime is a smooth 4-manifold with a Lorentzian metric of signature , an electromagnetic field (a 2-form) and a time orientation . The pair is electrovacuum if, in geometrized Gaussian units,
The spacetime is stationary if a one-parameter group of isometries preserves , and it has a stationary asymptotically flat end if coordinates , , cover an open set on which is the time translation and , , .
With the chronological future and past, the domain of outer communications is , the black-hole region is and the future event horizon is .
The Kerr–Newman family, in Kerr–Schild coordinates, is with
with potential . For , its domain of outer communications is , .
Under the standing hypotheses (smooth electrovacuum, stationary, asymptotically flat end, globally hyperbolic , nonempty black-hole region, connected event horizon), there are , , with , an angle and a diffeomorphism with
A proof of the goal would establish that the Kerr–Newman metrics exhaust the stationary, asymptotically flat electrovacuum black holes with connected horizon, which is the mathematical basis for treating astrophysical black holes as described by three numbers. It would also remove the analyticity and non-degeneracy hypotheses from the known vacuum results.
No machine-checked proof of any statement in this mission is known. Milestones 1, 7 and 8 are classical computations; milestones 3–6 are published theorems whose proofs rely on substantial Lorentzian geometry and elliptic PDE; the goal is open.
Uniqueness proofs reduce the problem to an elliptic boundary-value problem on the orbit space once enough symmetry is available. In the general stationary case the extra axial symmetry is not known to exist: Hawking's rigidity argument produces it only for analytic metrics, because it extends a Killing field off the horizon by analytic continuation. Without analyticity, unique continuation for the Killing equation across the horizon is the obstruction. Degenerate (extremal) horizons further break arguments that rely on a bifurcation surface.
Spacetimes are Mathlib smooth manifolds modelled on EuclideanSpace ℝ (Fin 4); the metric and field are fields of continuous bilinear forms on tangent spaces, and curvature and field equations are imposed through components in every chart. Causal sets use curves parametrized by . The Kerr–Newman comparison spacetime is the region of Kerr–Schild coordinate space with the explicit metric. Magnetic charge is accommodated by the duality angle .
The hypotheses are not vacuous: milestone 2 asserts that every Kerr–Newman black hole satisfies them. The connected-horizon hypothesis excludes the static multi-black-hole Majumdar–Papapetrou solutions, which would otherwise contradict the goal.
Needed infrastructure: Levi-Civita connection and curvature on manifolds, causal theory (global hyperbolicity, Cauchy surfaces), Killing fields and their flows, and the elliptic theory of harmonic maps used in uniqueness proofs. Contributions on any of these, and on milestones 1, 7 and 8, are welcome.
Loop quantum gravity (LQG) is a proposal for a quantum theory of the gravitational field in which space itself is built from discrete quanta. Its kinematics rests on two mathematical facts that C. Rovelli's review Loop quantum gravity: the first 25 years (Class. Quantum Grav. 28 (2011) 153002, arXiv:1012.4707) singles out. First, the spin–geometry theorem of Penrose, in the extended form based on a theorem of Minkowski (1897): the angular-momentum vectors attached to the links around a node of a spin network, once they satisfy the closure (gauge-invariance) relation, are exactly the data of a flat polyhedron, so every quantum of space carries a geometry (§2.1). Second, the discreteness of geometric spectra: areas take values with half-integer spins , with a strictly positive area gap (§2.1, §2.3, §4.3), which the review calls "the most solid result in loop gravity".
Timeline. Minkowski proved the existence and uniqueness of a convex polyhedron with prescribed face normals and areas in 1897. Penrose introduced spin networks and the spin–geometry theorem around 1971. The discreteness of area and volume in LQG was found by Rovelli and Smolin (1995), with the full area spectrum computed by Ashtekar–Lewandowski and others in 1995–1997.
Work in Euclidean three-space with its standard inner product . Given finitely many vectors and real numbers , the half-space polyhedron is
and its -th face is . The area of a set lying in a plane orthogonal to a nonzero vector is its two-dimensional Lebesgue measure, computed as the measure of its orthogonal projection onto the plane . For a nonzero vector , is its direction.
On the quantum side, a node of a spin network with links carries vectors (the left-invariant derivative operators), subject to the closure relation (eq. (6)). The review's classical content is: the behave as the area-weighted normals of a polyhedron, whose face areas are and whose volume (for ) is given by the triple product (eq. (10)). Spins label links; the quantity is the square root of the Casimir. The area spectrum (eq. (26)) is the set of numbers over finite families of spins, with the Barbero–Immirzi parameter, the reduced Planck constant and Newton's constant.
For nonzero with pairwise distinct directions , spanning , and with :
and any two such polyhedra are translates of each other.
The goal theorem is the precise mathematical content behind the statement that "the algebraic structure of the momentum operators determines the existence of a metric at each node and therefore equips each quantum of space with a geometry" (§2.1). Its necessity half (milestone 1) is the classical counterpart of the gauge-invariance constraint (6); its sufficiency and uniqueness halves are what allow LQG states to be read as quantum polyhedra and underlie the "twisted geometry" and polyhedral-volume constructions. The spectral milestones encode the review's discrete-geometry claims in the elementary, operator-free form in which they are stated in eqs. (13), (18) and (26).
All statements here are known theorems; none is open. A search of Mathlib (at the revision used to check these statements) found no theory of convex polytopes, facet areas, the Brunn–Minkowski inequality, or Minkowski's theorem for polyhedra.
The necessity direction (closure) is a divergence-theorem or projection argument, but requires relating the facets of an H-described polytope to its boundary. The existence direction of Minkowski's theorem is a variational argument (maximize volume subject to a linear constraint on support numbers) whose difficulty lies in showing that the optimum has all prescribed faces with positive area; uniqueness is classically deduced from the equality case of the Brunn–Minkowski (or Minkowski mixed-volume) inequality. The spectral milestones are elementary.
Lean represents as EuclideanSpace ℝ (Fin 3). A polyhedron is given by a finite family of normals and support numbers (halfspacePolyhedron), faces by polyhedronFace, and face area by planarArea, the Haar (Lebesgue) measure of the orthogonal projection onto the plane orthogonal to the normal, valued in ; areas are compared as extended reals so that an infinite area cannot be confused with . Unit normals are obtained as (unitDir). The cross product is Mathlib's crossProduct transported to EuclideanSpace. Spins are encoded as with , and the area spectrum sums over finite multisets of spins.
The goal excludes trivializing readings: the spanning and distinct-direction hypotheses are the classical non-degeneracy conditions of Minkowski's theorem (without them the existence claim is false), and the conclusion demands a bounded polyhedron with nonempty interior, so empty or flat polyhedra do not count. The review's eq. (10) omits numerical constants; the milestone uses the exact Euclidean constant . The operator-theoretic statements of the review (spectra of area and volume operators on ) are out of scope; only their stated numerical content is formalized.
Reusable infrastructure: H-polytopes in , facet areas, the closure identity, and the Brunn–Minkowski equality case. Contributions of general convex-geometry lemmas are welcome.
The classical singularity theorems of general relativity, starting with Penrose's theorem (Penrose 1965), show that spacetime cannot be continued indefinitely along all light rays once gravity has trapped a surface. Every such theorem assumes a positivity condition on the stress–energy tensor, typically the null energy condition . Quantum fields violate every such pointwise condition, so the classical theorems say nothing about the regime where quantum effects near a would-be singularity are strongest.
Wall (2013) replaces the energy condition by the fine-grained generalized second law (GSL) of horizon thermodynamics: the generalized entropy (horizon area over plus the entropy of the fields outside) of the exterior of any causal horizon never decreases. Generalizing the notion of trapped surface to a quantum trapped surface, on which the generalized entropy rather than the area decreases, the paper proves that a globally hyperbolic spacetime with a noncompact Cauchy surface containing a quantum trapped surface is null geodesically incomplete (Theorem 4).
Timeline: Penrose (1965) proved the classical theorem under the null energy condition; Hawking and Ellis (1973) give the standard textbook account; Wall (2010) derived the achronal averaged null energy condition from the GSL; Wall (2013) proved the quantum singularity theorem discussed here.
A spacetime is a smooth manifold with a smooth Lorentzian metric of signature and a continuous timelike vector field fixing the time orientation. Future-directed timelike and causal curves define the chronological relation and the causal relation , and the sets , . Following §3.2 of the paper, is globally hyperbolic if there are no closed timelike curves and is compact for all . A Cauchy surface is a set met exactly once by every inextendible timelike curve. is null geodesically complete if every null geodesic can be extended to all values of its affine parameter.
The generalized entropy assigns a real number to the part of a time slice lying in a region. An observer is a future-infinite timelike worldline (or a null ray with infinite affine parameter); its causal horizon is , with exterior . The fine-grained GSL (eq. (10)) says that for Cauchy surfaces nowhere to the past of ,
A compact surface on a connected Cauchy surface , whose exterior on is noncompact, is quantum trapped if the generalized entropy outside the null surface shot outwards and to the future from is decreasing at every point of .
The result. Theorem 4 makes the inevitability of black-hole and (time-reversed) Big Bang singularities independent of energy conditions, conditional only on the GSL, which is expected to hold in quantum gravity. Section 4 of the paper derives from it and its ingredients the absence of traversable wormholes, of warp drives between asymptotic regions, of time machines and of viable baby universes.
Formalizing it. No machine-checked account of Lorentzian causality theory, global hyperbolicity or the Penrose argument is currently available in Mathlib. This mission builds a self-contained Lean model of time-oriented Lorentzian manifolds, geodesics in coordinates, chronological and causal futures, Cauchy surfaces and global hyperbolicity, and pins down the exact logical content of the GSL-based singularity argument. The appendix milestones are pure matrix analysis (majorization under positive unital trace-preserving maps) and are reusable independently.
The goal splits into a thermodynamic step and a topological step. The thermodynamic step (every generator of terminates) is short once the hypotheses are in place. The topological step is the classical Penrose argument: turning "every generator terminates" into compactness of the achronal boundary and contradicting the noncompactness of the Cauchy surface. That requires the structure theory of achronal boundaries (generators, edges, the hypersurface property), limit-curve arguments for a uniform bound on the termination parameter, and the homeomorphism of achronal boundaries onto subsets of a Cauchy surface along a timelike flow. None of this exists in Mathlib.
M modelled on a finite-dimensional real inner product space E, smooth (), Hausdorff and second countable. The metric is a field of bilinear forms g x on the model space, smooth in every chart, with a continuous timelike field timeField giving signature and the time orientation.Sgen : Set M → ℝ. The paper gives no rigorous definition of it or of "semiclassical", so the physical input enters as explicit hypotheses: the fine-grained GSL (eq. (10), extended to infinite null rays as in §2.2) and, at points of , the comparison principle of Theorem 1 restricted to comparisons against causal horizons (the formal stand-in for "the semiclassical approximation is valid near ").Sgen would satisfy every hypothesis. is required nonempty. "Exterior noncompact" means the closure of the exterior is noncompact.Many problems in signal processing, statistics and machine learning take the form , where is smooth and is convex but nonsmooth (a norm, the indicator of a constraint set). The forward-backward method takes a gradient step on followed by a proximal step on . Its accelerated, inertial version — FISTA of Beck and Teboulle, built on Nesterov's method — reaches the rate for the objective values. In practice the gradient or the proximal step is computed only approximately, so it matters whether the accelerated method survives errors, and whether its iterates converge at all, not only its objective values.
Let be a real Hilbert space. Let be proper, lower semicontinuous and convex, and let be convex and continuously differentiable, with gradient Lipschitz continuous with constant . Write and .
The proximal map of () sends to the unique minimizer of .
Fix , a step with , and perturbations . The perturbed inertial forward-backward algorithm (55) generates
With and this is FISTA. The analysis uses and, for , the energy
If , , and , then
The goal makes no claim about rates of the iterates and no claim of strong convergence.
For , with an explicit constant depending on , , and ,
The proof's steps, in order: the proximal-gradient inequality (63); the energy step (66); the discrete Gronwall–Bellman Lemma A.9; the bound (68) on ; Theorem 5.1; the descent inequality (69); the velocity bound (72); the second-order inequality (80) for ; Lemma A.5; Opial's Lemma A.3.
The result. Theorem 5.3 gives convergence of the iterates of a FISTA-type method that tolerates computational error, and summability estimates that are stronger than the value rate: implies the rate along the sequence. The summability condition is the discrete counterpart of for the perturbed dynamics, which makes the algorithm a faithful discretization of the continuous model studied in the same paper. For (FISTA itself) convergence of the iterates was not known when the paper was written.
Formalizing it. The unperturbed case () is already on Prove2Me and proved: the weak convergence theorem and the energy, descent and summability facts (namespace NesterovFB), and the proximal-gradient inequality, which this mission reuses as milestone (63). This mission poses the perturbed statements, which no existing item covers: the error terms change the energy step, require boundedness of through a Gronwall-type argument, and turn the Fejér-type estimate into an inhomogeneous one. The discrete Gronwall–Bellman and Opial lemmas are reusable well beyond this paper.
Without errors the energy is nonincreasing and every estimate follows from summing (66). With errors, (66) has the extra term , which can only be summed once is known to be bounded — and the bound on itself comes from the energy. The circularity is broken only by an implicit quadratic inequality and a discrete Gronwall–Bellman argument; a direct summation fails. The same issue reappears for the velocities, where (71) bounds in terms of itself. Finally, weak convergence needs that exists for every minimizer; for the inertial scheme is not monotone, and one must pass through the second-order inequality (80) and Lemma A.5 rather than a Fejér argument.
is a real inner product space, complete; nothing is finite-dimensional, and weak convergence is the published WeakTendsto ( for every ), not norm convergence. is EReal-valued with IsProperClosedConvex, and is a map with IsProx s Φ P (published definitions). is the published NesterovFB.Rates.theta Φ Ψ; that definition names its arguments the other way round (nonsmooth first). is a nonnegative real and "" is written , . The algorithm is the predicate IsPerturbedRun on two sequences ; is free, which covers every value of the unspecified . Series are Summable statements, sums such as are tsums used only under the summability hypothesis.
Two printed statements are corrected as their proofs require. In Theorem 5.3 iii) the limit minimizes (the page says , the proof applies Opial's lemma with ). In Theorem 5.1 the constant uses , the quantity the proof derives, instead of the printed . Theorem 5.1 and (68) assume so that the constant is a real number; Theorem 5.3 does not.
A trivializing formalization is ruled out: the step condition is rather than (which is unsatisfiable for in Lean), and a sorry-free check confirms that , , and constant sequences satisfy every hypothesis of the goal, so the hypotheses are jointly satisfiable.
Theorem numbers and pages are those of the Optimization Online preprint 5179 (October 2015), not of the Mathematical Programming typesetting. Welcome contributions: proofs of the appendix lemmas A.3, A.5, A.9 (independent of the algorithm), of (66) and (69) from the referenced inequality (63), and the chain (68) → Theorem 5.1, (72), (80) → Theorem 5.3.
A retailer choosing which products to display faces a physical limit: different products consume different amounts of shelf space. Under a nested logit choice model, the value of an assortment also depends on how customers substitute among products within a nest and on whether they leave without buying. Gallego and Topaloglu study this combination of choice and feasibility constraints in Constrained Assortment Optimization for the Nested Logit Model. Their authors' manuscript of September 11, 2013 is the numbered source for this mission. Its §5 isolates a finite family of candidate assortments for each nest, despite the per-nest space-constrained problem being a knapsack problem. A small family matters because the paper's earlier Theorem 4 can then combine the families across nests while controlling expected revenue.
The paper contrasts this case with cardinality constraints. When every product consumes one unit, the per-nest optimization can be solved exactly by a short list of candidates. General space requirements turn it into a knapsack problem, so the paper gives quantitative approximation factors instead. The factor improves when no single product occupies much of a nest's capacity. These statements and their dependencies occur in §§5.1–5.2, pp. 19–22 of the manuscript.
There is a finite set of nests and a nonempty finite product set in each nest. In nest , product has preference weight , real revenue , and space requirement . The nest's capacity is , and each product fits by itself: . An assortment is feasible when its total space requirement is at most . The empty assortment is feasible and gives zero revenue. The full nested logit model has a no-purchase preference weight and a dissimilarity parameter for each nest; these parameters are relevant to the cross-nest expected revenue, but the local problem of this mission uses only one nest's product data.
For an assortment , write and , with . The paper's parameterized local problem, problem (7), maximizes over feasible assortments for each . Since the within-nest no-purchase weight is zero, equation (8) gives its equivalent sum of product utilities:
Problem (10) is this objective written as a zero-one knapsack: each product decision is zero or one and . Its LP relaxation permits . At parameter , the product's utility-to-space ratio is . Rounding a relaxation solution down retains precisely the products with . The candidate family also contains each singleton assortment .
Theorem 6 asserts that a collection of at most quadratic size includes a two-approximate solution to problem (7) for every . Here an assortment is -approximate at if it is feasible and is at least the objective of every feasible assortment. The statement is pinned to the explicit bound .
The §5.2 target keeps the same collection and adds the finer guarantee whenever each product is small relative to capacity. For every such that for all , and for every , some member of satisfies
The two members need not be the same, but the finite family is fixed before and are chosen. Together the claims yield the paper's factor . The main goal formalizes both parts; Theorem 6 and the paper's intermediate statements are milestones.
The local result converts infinitely many parameter values into a finite search domain. Theorem 4 of the same paper says that if each nest has candidates containing an -approximate local solution for every , then some cross-nest combination obtains at least the optimal expected revenue divided by . Theorem 2 relates the best combination of candidates to a linear program. Thus the finite collection in this mission supplies the local ingredient needed for the paper's global factor two, or the smaller factor under the product-size condition. These consequences are stated in the paragraphs immediately following Theorem 6 and the §5.2 conclusion.
The paper already proves these mathematical results. This mission asks for machine-checked proofs of its specific knapsack relaxation, rounding inequality, and approximation statements. It also creates reusable finite-knapsack definitions and explicit interfaces between the paper's local objective and the published nested logit model. The goal and milestones here remain open Lean statements until solvers provide proofs; compiling a statement with sorry checks its syntax and types, not its mathematical validity.
The parameter ranges over a continuum, yet one family of bounded size must work for all of it. Different values of change the objective coefficients and may change which products belong in an LP optimum. At ties or sign changes, the optimum need not be unique, so a statement about a particular chosen solution requires care. A second difficulty is the fractional LP coordinate: its value can exceed the rounded set's objective, and the refined factor uses a comparison between its utility and the space already occupied. The displayed chain in §5.2 contains quotients that can have zero denominators; the formal milestone states its endpoint inequality directly. A fractional product with zero utility need not force capacity to be filled, which is why the capacity-consumption milestone states positive utility explicitly.
The existing NestedLogitVariants.LP.Model supplies the nested logit instance and its and functions. A general finite continuous-knapsack definition is separate from the paper-specific assortment data. Products use Fin n, nests use a finite type, and assortments use finite sets. The empty finite set represents . The model's within-nest no-purchase weight is fixed to zero, as in the manuscript's main local formulation. Revenues remain arbitrary real numbers; there is no assumption that they are nonnegative or sorted. The capacity and product space requirements are real numbers, with and . Positive preference weights and nonempty are explicit. No condition on or is needed for this local problem (7).
The candidate family is a finite set of rounded LP optima and all singletons. Its size is bounded before and are quantified. Each approximation compares against feasible integer assortments using problem (7), including the empty assortment. The LP optimum itself is never substituted for the integer comparator. General unequal space requirements remain in scope. Contributions that formalize the parametric LP behavior, its one-fractional-coordinate optimum, and the paper's two rounding guarantees fit this mission.