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?
Many problems in statistical learning and signal processing take the form of minimizing an expectation plus a regularizer or constraint , where the only access to is through samples . The classical tool is the stochastic (proximal) subgradient method, which replaces at the current point by a random linear function. Two other methods use richer local approximations: the stochastic proximal point method keeps the whole sampled loss , and the stochastic prox-linear method linearizes only the smooth inner part of a composite loss . In experiments the richer models are markedly less sensitive to the choice of step size.
Davis and Drusvyatskiy (arXiv:1803.06523, SIAM J. Optim. 29(1), 2019) treat all three methods as instances of one scheme, stochastic model-based minimization, in which each step minimizes a sampled one-sided model of plus plus a quadratic penalty. Their main theorem (Theorem 4.3) covers weakly convex problems through the Moreau envelope. This mission formalizes the companion result for the convex setting, Theorem 4.1: when the models lower-bound in expectation without quadratic error and is convex, the expected function gap at a weighted average of the iterates decays like . As the paper notes (p. 22), for the stochastic proximal subgradient method this improves earlier bounds (Cruz 2017; Duchi–Singer 2009) because no subgradient norm of enters the estimate.
Work in with the Euclidean norm. The problem is
where is locally Lipschitz and is closed (its epigraph is closed) with nonempty domain . A function is -weakly convex if is convex; is ordinary convexity.
Assumption B (p. 18) fixes a probability space , an open convex set , real constants , a measurable model on and a measurable such that:
Algorithm 4.1 (p. 19) starts at and, for , samples and sets
The convex setting is and . Write for the step sizes and let be any minimizer of .
For every ,
and with the constant step , ,
The factor in front of is the constant the paper's proof establishes; see Formalization scope.
Theorem 4.1 is the function-value guarantee of the model-based framework. Theorem 4.3 measures progress by the gradient of the Moreau envelope, which is the right quantity for nonconvex problems but says nothing directly about suboptimality; under convexity, Theorem 4.1 gives the familiar rate for the gap itself. It applies to the stochastic proximal point and prox-linear methods as well as to the proximal subgradient method, and §4.2 of the paper uses it for minimizing an expectation of a pointwise maximum of convex functions, such as the conditional value-at-risk. The estimate (4.8) behind it is also the engine of the strongly convex rate (Theorem 4.2, a separate mission of this series).
The result is proved in the paper; nothing in it is open. To our knowledge none of these statements has a machine-checked proof. The formalization contributes a checked version of the one-step estimate (4.8) with its corrected constant, a reusable Lean encoding of Assumption B and of Algorithm 4.1 with extended-valued , and the passage from conditional one-step bounds to expectations over the product measure of the samples.
The argument is short on paper; the work lies in the measure theory the paper leaves implicit. The iterate is an argmin that depends on and on the fresh sample , and the one-step estimate holds only conditionally, with frozen. Turning it into an inequality between unconditional expectations requires measurability of the iterates, independence of from the past, and integrability of and , which the paper takes for granted. The convex function is extended-valued, so the function gap is meaningful only because every iterate and every average lies in .
A naive one-step argument that bounds and separately, each by a Lipschitz constant times , gives the constant in (4.8) and not the printed . The printed constant is false (see below), so the constant cannot be improved simply by tightening that one step.
EuclideanSpace ℝ (Fin d). The extended-valued is a real function together with its domain D; closedness of is closedness of , and convexity is ConvexOn ℝ D. is L and is Lfun.Measure.pi), Fubini–Tonelli over , measurability of the run, Jensen's inequality for a convex function on a convex set, and strong convexity of the subproblem. Proofs of any milestone are welcome, as are a general "conditional one-step bound to expectation over the run" lemma reusable by the other missions of this series.Many problems in statistical learning and signal processing minimize an expectation plus a regularizer or constraint , with access to only through samples . The standard tool is the stochastic (proximal) subgradient method, which replaces at the current point by a random linear function. Two other methods use richer local approximations: the stochastic proximal point method keeps the whole sampled loss , and the stochastic prox-linear method linearizes only the smooth inner map of a composite loss . The richer models are markedly less sensitive to the step size in practice.
Davis and Drusvyatskiy (arXiv:1803.06523, SIAM J. Optim. 29(1), 2019) treat all three methods as instances of one scheme, stochastic model-based minimization: each step minimizes a sampled one-sided model of , plus , plus a quadratic penalty. Their main theorem (Theorem 4.3) concerns weakly convex problems. This mission formalizes the companion result for the strongly convex setting, Theorem 4.2: when the models lower-bound in expectation and is -strongly convex, the expected function gap at a nonuniformly weighted average of the iterates decays like . The weighting is the technique of Schmidt, Le Roux and Bach (2012) for the projected stochastic subgradient method; the paper extends it to the fully proximal, model-based setting (p. 23).
Work in with the Euclidean norm. The problem is
where is locally Lipschitz and is closed (its epigraph is closed) with nonempty domain . A function is -weakly convex if is convex; a negative modulus is -strong convexity.
Assumption B (p. 18) fixes a probability space , an open convex set , real constants , a measurable model on and a measurable such that:
Algorithm 4.1 (p. 19) starts at and, for , samples and sets
The strongly convex setting is and with , run with . Let be any minimizer of .
For every integer ,
together with integrability of the function inside the expectation. The paper prints ; see Formalization scope.
The result. Theorem 4.2 is the rate for a whole family of stochastic methods at once: the stochastic proximal point, prox-linear and proximal subgradient methods all satisfy Assumption B (§4.2 of the paper). The rate is in function values at an explicit averaged point, with explicit constants, and needs neither smoothness of nor bounded subgradients of : the regularizer enters only through the strong convexity of the subproblems. The order is the one Schmidt, Le Roux and Bach obtained for the projected stochastic subgradient method; Theorem 4.2 extends it to models that are not linear and to a general closed .
Formalizing it. The result is proved in the paper; it is not formalized anywhere to our knowledge. Formalizing it pins down the exact constant (the printed one does not follow from the paper's lemmas; see below), the measure-theoretic content of "iterates generated by Algorithm 4.1" (a measurable selection of the argmin, the product measure of the samples, conditional expectation as an integral over one fresh sample) and the integrability that the expectations presuppose. The one-step estimate (4.8) is shared with mission 4 of this series (Theorem 4.1, convex setting); a proof of it serves both.
The telescoping that turns the one-step bound into the rate is elementary once the weights are chosen. The work lies in two places. First, (4.8) itself: it combines the strong convexity of the subproblem, the one-sided accuracy (B2) used in expectation, the Lipschitz bound (B4) at the random point (so the exceptional null set must not depend on that point), Cauchy–Schwarz, and Lemma 4.1. Second, the passage from one step with held fixed to expectations over the whole run: this needs the independence of from (Fubini on the product measure) and integrability of , and along the run, none of which is stated on the page. A natural first attempt, bounding at the average by the average of before checking that the average lies in , is valid only because the weights sum to one and is convex by (B3).
EuclideanSpace ℝ (Fin d). The extended-valued is encoded by its domain D and its real values on D; closedness is closedness of . -strong convexity is -weak convexity: convexity of on D.Measure.pi; expectations are Bochner integrals, and every bounded expectation comes with an integrability conclusion, so a junk value cannot make a bound hold. in (4.8) is the integral over one fresh sample with held fixed.Distributed programs often establish a conversation among several participants, then exchange messages without waiting for each send to be received. A specification of each participant in isolation does not by itself say whether their actions will fit together. Multiparty asynchronous session types address this by describing the intended conversation once as a global type and checking each participant against a projected local type. Honda, Yoshida and Carbone develop this calculus and state a progress result for a restricted class of well-typed programs: if execution has not finished, another reduction is available. The restriction matters because independently initiated sessions can interfere and deadlock even when their communications are individually typed. Honda, Yoshida and Carbone (2016)
A program is a process before execution: it contains no message queues or restricted session channels, even after structural rearrangement, and it has no free session channels or process variables. A requester on a shared name starts a session with participants numbered through . Each participant receives the same vector of fresh session channels. An asynchronous send appends a message to the appropriate FIFO queue; a receive reads the queue head. Requests, sends, delegations and selections are emitting prefixes. Accepts, receives and branches are receiving prefixes. The reduction relation includes these communications, conditionals, guarded declaration unfolding, and closure under parallel composition, restriction and structural congruence . Honda, Yoshida and Carbone (2016), Figs. 1–3 and Def. 2.1
A global type specifies which numbered role sends a value or choice to another role on channel index , followed by the remainder of the conversation. It may also contain parallel components and guarded recursion. A partial projection gives role its endpoint type. Global types must be linear: causally ordered actions on a common channel have both input and output dependency chains. A global type is coherent when it is linear and projects to all its participants; the runtime typing is coherent when each session family comes from such a global type. Honda, Yoshida and Carbone (2016), Defs. 3.12, 4.1–4.2 and 5.9
The runtime judgement records the types of the process and the queue channels it mentions. Type contexts remember messages already in transit and compose with endpoint types. A process is queue-full when the channels in equal the channels occurring in . A prefix is active when it is outside another prefix and outside either branch of a conditional, after permitted declaration unfolding. A process is well-linked when every reachable process has each active shared-name prefix in a redex. A process is simple when it has a typing derivation whose session environments obey the singleton and emptiness restrictions of Definition 5.25, with no delegation input or output rule. Honda, Yoshida and Carbone (2016), pp. 28–37
The goal is Corollary 5.30. For every simple, well-linked program whose free names have shared sorts, and every reachable process ,
Here is inaction, and includes completed sessions whose empty queues disappear by structural congruence. The milestones are the closed-typing preservation clause of Theorem 5.19(3), the linearity and message agreement clauses of Theorem 5.22, and the immediate-step claim of Proposition 5.29(1). Those are statements of the paper and give separate targets before the progress corollary. Honda, Yoshida and Carbone (2016), pp. 34–37
For the specified class of programs, progress excludes a reachable state that is neither finished nor reducible. It combines static endpoint information with the operational facts about queues and shared-name synchronisation. The communication-safety milestone also states that a value receive is paired with a value message of matching arity, channel reception with a channel vector of matching length, and branching with an offered label. These claims describe behavior of the paper's asynchronous multiparty calculus, rather than a property of a particular implementation. Honda, Yoshida and Carbone (2016), Theorem 5.22 and Corollary 5.30
The paper supplies mathematical proofs, but this mission's statements have no completed machine-checked proofs. Formalizing the result requires a precise account of the calculus, including queue messages, scope, recursive calls, type contexts, projection and the limited form of simplicity. The definitions can support later work on subject reduction and session fidelity in the same model. A contribution may prove any milestone or the goal, or improve the shared definitions while preserving the source's hypotheses and conclusions.
Typing each participant does not immediately give a reduction of their parallel composition. A send can be present while a receive is blocked by an earlier queue message, and a session initiation can be blocked by a shared-name prefix in a different session. Communication safety must relate active prefixes to a unique queue and its actual head message. Progress additionally needs the restrictions on derivations and shared-name links to rule out interference among sessions. The rules for structural congruence and declaration unfolding make the location of a redex depend on more than the outer syntactic constructor. Honda, Yoshida and Carbone (2016), §§5.4–5.5
Lean uses natural numbers for role identifiers, shared names, channels, labels and process variables. Channel indices are one based, following . A global type, value sort and endpoint type are separate syntax classes; finite branch families are lists with nonempty, distinct labels where a well-formed type is required. Recursion is read equi-recursively by an endpoint bisimulation, and global-type linearity is checked on every finite unfolding. Projection returns an optional endpoint type so undefined projections cannot acquire a default value. The session typings are finite maps represented by association lists, with distinct roles and disjoint channel domains. The judgement's subscript lists queue channels, while the domain of lists all sessions under typing.
The formalization uses named process binders and a structural-congruence relation containing alpha conversion. Received-value and call substitution is capture avoiding under explicit freshness conditions. Expression evaluation is fixed to the ordinary Boolean connectives used in the paper's typing rules. Runtime typing includes the queue rules and the partial composition of type contexts. The restricted typing system for simplicity retains runtime queue rules and excludes both delegation directions. The paper prints “[RCV]” in Definition 5.25(2), but its appendix explicitly excludes “[SREC]”; this draft follows the appendix and records that reading in its audit notes. The result quantifies over actual programs and makes simplicity imply typability, so a free, blocked input or an untyped syntax check cannot satisfy the goal. Honda, Yoshida and Carbone (2016), Def. 5.25 and Appendix B.8
Every prefix rule acts on a singleton entry (Notation 4.5); process-variable signatures carry one singleton entry per session vector, as in [VAR]; [SREC] receives the channel names it binds, without substitution (Remark 2.2). Proposition 5.29(1) and Corollary 5.30 are false as printed for open terms: a free name of sort bool used as a conditional guard, or a free process variable, is a stuck simple process. The formal statements therefore add that the free names of the process have shared sorts and, for Proposition 5.29(1), that it has no free process variables (a program has none by definition).
The development needs Mathlib's finite sets, lists and reflexive-transitive closure, plus its own definitions of the process calculus and typing judgements. The Lean declarations in this proposal are draft statements and definitions for review; they are not proofs of the paper's results.
Multiparty communication protocols involve several participants who send messages over shared session channels. An implementation may send a later message before an earlier one has been received, so a written sequence of interactions does not by itself prevent a receiver from taking the wrong message. Honda, Yoshida, and Carbone use global types to specify the whole conversation and a linearity condition to rule out conflicting uses of a channel. Their condition is part of the type system that supports subject reduction and session fidelity in the same paper. Honda, Yoshida, and Carbone, 2016
Global types can contain recursion. Reading their full behaviour as a regular tree may therefore involve infinitely many copies of the same interaction. Proposition 3.13(1) says that checking just one finite unfolding suffices to determine whether every later finite unfolding satisfies the paper's linearity condition. This mission formalizes that proposition and the definitions on which its statement depends. Honda, Yoshida, and Carbone, 2016, §3.5 and Appendix A
A global type describes actions among roles on channels identified by positive indices . Its constructors are a value communication , a labelled branch , parallel composition , recursion , a recursion variable , and termination . The carried value type may contain shared names whose sorts include another global type, or it may be a located end-point type. The formal syntax represents end-point sends, receives, selections, branches, recursion, variables, and termination because shared global types can occur within the sorts carried by those types. Honda, Yoshida, and Carbone, 2016, Figs. 4 and 6
An action node is an occurrence of a communication or branching action in the tree of a finite unfolding. Each node has a sender, receiver, and channel index. The action order holds when one action lies before another in the same continuation or branch, according to Definition 3.7. Actions in different branches or parallel components have no order solely because they appear next to each other in the syntax. Honda, Yoshida, and Carbone, 2016, pp. 15–16
The paper refines that order into three dependency relations. An II step matches receivers; an IO step connects a receiver to a later sender; and an OO step matches both sender and channel. An input dependency is a chain of IO steps ending in II. An output dependency is a nonempty chain of OO or IO steps. A finite type is linear when every ordered pair of actions on the same channel has both dependencies, including the corresponding condition on the global types carried within its values. The last II step matters because a chain ending at an output has not checked the ordering of the final input. Honda, Yoshida, and Carbone, 2016, Defs. 3.11–3.12
Write for the finite result of unfolding every recursion in times and replacing remaining recursion variables by . For a single recursion , the paper gives and . Unfolding does not enter carried types. The one-time unfolding is . Honda, Yoshida, and Carbone, 2016, p. 20 and Notation A.1
The milestone is the direction the paper calls the “if-direction”: for a well-formed global type and a positive unfolding index, linearity at that index implies linearity at the first one.
The mission goal is Proposition 3.13(1), the equivalence between the first unfolding and any positive unfolding.
The lower bound is essential. The paper explicitly begins its Appendix A induction at and gives examples that satisfy linearity at the zeroth unfolding but fail after one unfolding. Proposition 3.13(2), the paper's decidability claim, is outside this mission: formalizing computational decidability would require an effective representation and decision procedure rather than a classical Decidable instance. Honda, Yoshida, and Carbone, 2016, p. 20 and Appendix A
The proposition turns a property stated over arbitrarily deep recursive behaviour into a fixed finite test. It supports the paper's decidability result and supplies the channel-ordering premise used later in coherent global types and runtime typing. Without the stabilization claim, checking a recursive global type by inspecting one finite copy would leave later channel conflicts unresolved. Honda, Yoshida, and Carbone, 2016, Props. 3.13–3.14 and Def. 4.2
The result is already proved in the paper. The formalization work is to give the paper's finite unfolding, action order, dependency chains, and recursive carried-type condition exact Lean meanings, then verify the equivalence against those meanings. The local mission currently contains open theorem statements and compiled definitions; it does not claim a machine-checked proof of Proposition 3.13(1). Those definitions can also be reused when formalizing the paper's coherence and subject-reduction results.
The main obstacle is the interaction between recursion and causality. Unfolding creates further occurrences of actions, while an input dependency requires a chain with a specific final II edge and an output dependency allows only OO or IO edges. The action order also depends on a node's place in a branch, continuation, or parallel component. Merely comparing channel labels across two unfoldings does not establish the required dependencies. The carried-type condition adds another level: unfolding the outer type leaves its carried types intact, but their own linearity must still be checked. Honda, Yoshida, and Carbone, 2016, Defs. 3.7, 3.11–3.12 and Appendix A
Lean represents roles, labels, type variables, and channel indices by natural numbers, with channel indices interpreted as one-based. Branches are lists; WellFormed G records nonempty branches with distinct labels, closed guarded recursion, positive channel indices, and distinct sender and receiver, also checking carried global types. Both theorem statements assume it to make the paper's standing syntax conventions explicit. The sort grammar includes Boolean and natural-number sorts, shared-name sorts, and coded additional base sorts for the paper's ellipsis. The recursion constructor is named mu and the sort type SType because rec and Sort have special meanings in Lean.
Node names are finite child-index paths. Prec is the transitive closure of the five clauses of Definition 3.7. Every II, IO, or OO step includes this order. Input dependency requires at least one step, resolving the printed against the same sentence's mandatory final II step. Carried types are reached through value and end-point type syntax, and nested carriers are included transitively. Linear checks each such carried type at every finite unfolding. The definitions also encode the paper's positive-index and non-reflexive interaction conventions in WellFormed. A linearity predicate that ignores carried types or treats separate parallel components as ordered would change the target theorem. Honda, Yoshida, and Carbone, 2016, pp. 12–13, 16, 19–20
Useful contributions include results about finite unfolding and the action order, preservation of labels at recurring positions, and dependency-chain properties under unfolding. The two folding claims in Appendix A are not listed as milestones here because a faithful folding operation for nested recursion and multiple occurrences has not yet been specified. Their absence is a scope limit on the attack path, not an assumption in the goal.
Many stochastic models use a process whose response to a disturbance depends on the time elapsed since that disturbance. An ordinary stochastic differential equation uses only the current state and instantaneous coefficients. A stochastic Volterra equation instead weights its past drift and noise through a convolution kernel. Such equations include the constant kernel as a familiar limiting case, while singular or decaying kernels allow different memory patterns. The paper Affine Volterra processes studies this class to obtain non-Markovian models that retain tractable affine transform formulas. Before any transform can be used for a nonnegative state variable, the underlying equation must actually admit a solution that stays nonnegative. Abi Jaber, Larsson and Pulido, §§1–3.
The mission focuses on the paper's existence and invariance theorem, Theorem 3.6 of the pinned preprint. It is a separate question from uniqueness or explicit transforms: the coefficients are only continuous with linear growth, so classical contraction arguments for Lipschitz coefficients do not directly settle it. The proof also has to preserve the boundary of the nonnegative orthant despite a drift and noise term that depend on the entire past. Abi Jaber, Larsson and Pulido, Theorems 3.3–3.6.
Fix dimensions . The kernel is a deterministic function from nonnegative time to real matrices. The drift maps to , and the diffusion coefficient maps to real matrices. Given a deterministic initial state and an -dimensional Brownian motion , a continuous adapted process solves
The deterministic and stochastic terms are matrix-vector convolutions: an event at time has an effect at time weighted by . A weak solution is allowed to choose its stochastic basis and Brownian motion. A strong solution is adapted to the completed filtration generated by its prescribed Brownian motion. All bases satisfy the usual completeness and right-continuity conditions. The equation is read at each fixed time almost surely, with having continuous sample paths. Abi Jaber, Larsson and Pulido, (1.1), §3.
The paper's condition (2.5) asks each scalar kernel entry to be locally square-integrable and to satisfy two estimates of order as : the integral of its square over , and the squared difference between its time shift by and itself over each finite interval. The exponent satisfies and may differ by entry. For the goal, is diagonal. Each diagonal entry is nonnegative, nonzero, nonincreasing and continuous on positive time. Its resolvent of the first kind is a nonnegative measure whose convolution with is the constant one; condition (3.4) also requires the interval mass to be nonincreasing in for every . Abi Jaber, Larsson and Pulido, (2.5), (2.13), (3.4).
The goal is Theorem 3.6. Write . Suppose is diagonal and satisfies (2.5) and (3.4) componentwise. Suppose and are continuous, satisfy , and obey the boundary condition for every :
Then the target is
The milestone list records the paper's moment bound, strong existence for Lipschitz coefficients, and general weak existence with a first-kind resolvent. They are numbered results from the same preprint and establish distinct parts of the existence framework. Abi Jaber, Larsson and Pulido, Lemma 3.1 and Theorems 3.3, 3.4, 3.6.
The conclusion says more than finite-time nonnegativity of a proposed process: it asserts that a stochastic basis, Brownian motion and continuous solution actually exist for every nonnegative initial condition under the stated kernel and boundary assumptions. This supports later use of the affine transform results on state spaces with nonnegative coordinates. The paper treats this existence theorem as one of the main inputs to its square-root and rough-volatility examples. Abi Jaber, Larsson and Pulido, §§3, 6.
The theorem is already proved in the source paper. The formalization task is to state and eventually verify that known result in Lean, including the exact memory-kernel condition and the stochastic basis chosen by weak existence. The published Brownian and Itô-integral definitions are reused. A verified solution would leave reusable definitions for Volterra kernels, first-kind resolvents, and weak convolution equations, as well as machine-checked statements for the supporting existence theorems.
For Lipschitz coefficients, the paper obtains a unique strong solution. The goal permits only continuous coefficients of linear growth. Approximating them by better-behaved coefficients does not by itself guarantee that a limit solves the original convolution equation or remains in the nonnegative orthant. The stochastic convolution depends on the full history through , and the boundary condition must be propagated through that memory. A direct appeal to an ordinary SDE invariance theorem therefore does not cover the claim. The first-kind resolvent and the monotonicity in (3.4) are central to the stated assumptions. Abi Jaber, Larsson and Pulido, proofs of Theorems 3.4 and 3.6.
Lean uses EthierKurtz.SDEState d, a Euclidean -vector, for states; real matrices for and ; nonnegative real process time; and real arguments for deterministic kernels and interval integrals. Local membership is componentwise, which is equivalent to membership under any norm on the finite-dimensional matrix space. The matrix norm in linear growth is the Euclidean operator norm. The big- bounds in (2.5) are taken as tends to zero from the right. Each diagonal kernel has its own exponent and its own positive resolvent measure. A general matrix first-kind resolvent is encoded entrywise as the difference of two measures finite on compact positive-time intervals, so it may have infinite total mass.
The weak-solution predicate existentially quantifies the stochastic basis, Brownian motion and continuous process. Each stochastic convolution has a witness satisfying the published Brownian Itô relation; an unconstrained process cannot witness the equation. Drift terms carry interval integrability, avoiding a default-zero value for a nonintegrable integral. The stochastic basis is complete at time zero and right-continuous. The goal asserts orthant membership at every fixed time almost surely; continuous paths yield an orthant-valued version. The zero-time equation and empty-index cases are included. Contributions that formalize stochastic-convolution continuity, compactness of path laws, first-kind resolvent calculus, or invariance of the orthant are in scope.
A local quantum system is built from degrees of freedom placed at sites of a lattice. Its Hamiltonian may contain many terms, each acting on a small group of sites. Even though a term is local, time evolution can spread an observable beyond its original support. A Lieb–Robinson bound limits the size of a commutator between the evolved observable and one supported elsewhere. It gives a quantitative way to say that information propagates with an effective finite velocity. The Appendix C bound of Haah, Hastings, Kothari and Low treats interactions with exponential spatial decay and makes the effect of almost commuting Hamiltonian terms explicit.
The paper studies quantum simulation, where a system's real time evolution is approximated by a circuit. Lemma 12 is an analytic ingredient: it controls how far a local observable can spread during the simulated evolution. The mission targets that lemma and the displayed estimates in its proof, with the constants printed in the pinned arXiv version. The paper proves the results; the remaining task here is to give the stated finite system version machine checked proofs.
Let be a finite set of sites equipped with a metric . Each site has the same local Hilbert space , and the whole system has product basis indexed by configurations . An operator supported on is a matrix of the form : it may change the configuration on , but acts as the identity on every site outside . The matrix norm throughout is the spectral operator norm.
For every , let be a Hermitian operator supported on , and define the time independent Hamiltonian . The sum includes all subsets, including the empty set. Let
For site sets, write when , and when is nonempty. The diameter is for nonempty . The paper imposes two quantitative conditions. First, for some , every pair of terms has a small commutator:
Second, for some , the interactions decay in the weighted sense
Neither condition bounds each by one. This matters because the result is meant to include large but nearly commuting terms. These conventions are from Appendix C.1 of the source.
The goal is Lemma 12. For an operator supported on and an operator supported on a disjoint set , and every real , the proposed formal statement is
The coefficient of in the exponential is proportional to . The goal keeps the paper's explicit factor , its inside the exponential, and the full sum over sites in . The statement is for , as the displayed formula is undefined at ; a family satisfying (14) with also satisfies it for any positive .
The milestones follow the source's numbered displays: the initial estimates for and in (28), their integral inequalities (24) and (27), the linked set series (32), the four estimates of Proposition 13, and the bound on its th line in (37). Here takes a supremum over supported operators of norm at most one, and . The milestone list is a map of the quantities that the proof controls, while the goal itself mentions only the physical operators and the two hypotheses.
The bound shows that a commutator is small when the support of is far from , with a rate determined by the decay parameter and the small commutator parameter . It applies to finite systems of any size with the same constants in (14) and (15). This makes it useful for reasoning about local approximations of time evolution in the quantum simulation setting of the paper. The authors also explain why a velocity proportional to can occur under their hypotheses, so a linear dependence on is not generally available. See the discussion immediately after Lemma 12 in Appendix C.1.
Formalizing the result would supply a reusable finite matrix model of local observables and a checked version of the analytic estimates for near commuting interactions. The source paper provides a proof, but this proposed statement and its milestones currently have no machine checked proof in the mission. The definitions of support, Heisenberg evolution and linked interactions may also be reused in later formalizations of quantum lattice dynamics.
The obvious global norm bound ignores the distance between supports. Merely bounding also loses spatial information and can grow with the whole system. The sharper statement simultaneously tracks where an interaction overlaps the current support and how the small commutator factor enters repeated interactions. A rigorous treatment must control a supremum over local operators, time dependent matrix exponentials, and an infinite series of finite linked set sums without changing any of the paper's constants.
Sites form an arbitrary finite metric space, a disclosed generalization of the lattice setting used for the main algorithm. A common local dimension is used at every site; qubits occur at . Operators are complex matrices on the configuration space , with Mathlib's scoped L2 operator norm. Every term is Hermitian and explicitly supported on its stated set, and is the sum over all subsets. Time is real and is constant in time. The paper mentions a piecewise continuous time dependent extension, which this mission does not state.
The goal explicitly requires . The printed sentence of Lemma 12 omits this, but its derivation on page 24 assumes it; without disjointness the right side is zero at while the left side need not be. The positive condition is likewise explicit. These are the two repairs to the printed lemma, and they are recorded on each relevant item. The milestones (24) and (27) are restricted to , the direction for which the displayed forward integral uses and .
For an empty set, the Lean point to set distance and the local set distance are taken to be zero; a supported operator on the empty set is a scalar, so its commutators vanish. uses a real supremum of a nonempty, bounded set, and (32) states an actual sum with HasSum. The integral milestones involve continuous finite dimensional evolution. The support definition includes nonconstant single site operators, and the case is part of the goal. These choices prevent the result from being obtained through a vacuous support predicate, an entrywise norm, division by zero at , a default value of an unbounded supremum or divergent sum, or omitted disjointness. Contributions that establish the support calculus, matrix evolution estimates, integral inequalities, or linked set bounds are all within scope.
Makespan minimization on identical parallel machines, , asks to assign jobs with processing times to machines so that the largest machine load is as small as possible. It is strongly NP-hard, and the question has long been how fast a -approximate schedule can be found. After rounding and scaling, a guess of the optimal makespan becomes a constant, the job sizes take only distinct values, and the problem becomes an integer program over machine packings: the configuration IP.
A short history of the running times for this problem:
Fix , a vector of job sizes and a capacity . The knapsack polytope is , and a configuration is an integral point of it:
A configuration describes one machine: jobs of size , of total load at most . The support of a vector is the set of its nonzero coordinates, . Throughout, . A configuration is simple if and complex otherwise; is the set of complex configurations.
Given the number of jobs of each size and the number of machines, the configuration IP [conf-IP] asks for multiplicities , one per configuration, with
Its LP relaxation [conf-LP] replaces by . The support of a solution is .
If [conf-IP] is feasible, it has a feasible solution with
A solution with these three properties is called thin.
The result. Theorem 1 says that, up to machines, every feasible configuration IP can be solved using simple configurations only. There are simple configurations, far fewer than configurations in general, so an algorithm can guess the support of a solution among a much smaller family. This is what yields the EPTAS for , and through the same structure PTASs for and for -norm and max–min objectives. Corollaries 5 and 6 are structural facts about knapsack polytopes in their own right: the integer hull has only simple vertices, and the configuration LP can be restricted to simple configurations.
Formalizing it. The results are proved in the paper; none of them has a machine-checked proof that this mission knows of. The development produces a reusable formal model of configurations and of the configuration IP and LP, a formal Eisenbrand–Shmonin support bound for this IP (a Carathéodory-type statement for integer cones that recurs across integer programming), and the sparsification lemma with its potential-function argument. The constants and are the paper's and are stated exactly.
The obvious argument applies the sparsification lemma repeatedly, replacing any complex configuration used twice by two configurations of smaller support, and then shrinks the support with the Eisenbrand–Shmonin exchange. The second step can undo the first: the exchange moves weight between configurations and may raise the multiplicity of a complex configuration above one again, so alternating the two steps has no evident termination measure. A proof has to control both properties at once. The counting behind the support bound needs the explicit inequality for every , which must be carried out with the exact constants rather than up to .
Fin d → ℕ with ; solutions of [conf-IP] are finitely supported functions (Fin d → ℕ) →₀ ℕ vanishing outside , and solutions of [conf-LP] are finitely supported real-valued functions, nonnegative and vanishing outside .Real.logb 2 and every bound is a real inequality; no floor is taken.Set.extremePoints). The asymptotic count of Corollary 5 is replaced by the explicit bound of its proof, with the added hypothesis (at the explicit bound is while ).The goal theorem refers only to [conf-IP], its solutions, supports and the simple/complex split; it does not mention the potential, the matrix or a minimality assumption, so it cannot be discharged by choosing a special solution in the hypotheses.
Needed infrastructure: finite sums over Finsupp, the pigeonhole principle on finsets, elementary bounds on Real.logb, and, for Corollaries 5 and 6, convex hulls and extreme points of finite sets in . The definitions of configurations and of the configuration IP/LP are reusable for other configuration-IP papers (bin packing, cutting stock, scheduling). Contributions of auxiliary lemmas on supports of integer conic combinations are welcome.
Many problems in statistics, signal processing and machine learning minimize an expected loss that is neither smooth nor convex: robust phase retrieval, blind deconvolution, covariance estimation with the loss, training of networks with ReLU activations, and composite problems with convex and smooth . A common structural feature of these objectives is weak convexity: adding a quadratic makes the function convex. For such problems the classical stochastic algorithms — the stochastic proximal point method, the stochastic prox-linear method, and the stochastic proximal subgradient method — were used in practice long before any nonasymptotic complexity guarantee was available for them.
Damek Davis and Dmitriy Drusvyatskiy (arXiv:1803.06523, SIAM J. Optim. 29(1), 2019) gave such guarantees for all of these methods at once. They abstract each method as minimization of a stochastic one-sided model of the objective, and prove that the expected squared gradient of the Moreau envelope at a randomly selected iterate decays at rate , i.e. a sample complexity of . This mission formalizes that main theorem (Theorem 4.3) and the lemmas its proof uses.
Timeline. Nurminskii (1973, 1974) showed that when the sample losses are -weakly convex and there is no regularizer, the stochastic subgradient method converges subsequentially to stationary points almost surely; no rate was given. Ghadimi and Lan (2013) proved complexity for smooth nonconvex stochastic problems. Davis and Grimmer (arXiv:1707.03505, 2017) gave a rate for a proximally guided variant of the stochastic subgradient method on weakly convex problems. Davis and Drusvyatskiy (2018) obtained the complexity for the basic proximal stochastic subgradient method and, through the one-sided model framework, for the stochastic proximal point and prox-linear methods.
Work on with the Euclidean norm. An extended-valued function has domain and is closed when its epigraph is closed. A function is -weakly convex when is convex. For the Moreau envelope and proximal map are
The problem is with closed and locally Lipschitz, where is accessible only through a random model , . Assumption B asks for constants , an open convex and a measurable such that: and on (one-sided accuracy); is -weakly convex for almost every ; and .
Algorithm 4.1 fixes and parameters , draws i.i.d. samples , and sets
It returns , with drawn with . With it is the stochastic proximal point method; with a linearization it is the proximal stochastic subgradient method; with it is the stochastic prox-linear method.
and for with ,
The result. By Lemma 2.2, , and the proximal point satisfies and . A small envelope gradient therefore certifies that is close to a nearly stationary point. Theorem 4.3 gives this certificate, with explicit constants, for every algorithm fitting Assumption B, in particular the first complexity bounds for the stochastic proximal point and stochastic prox-linear methods on weakly convex problems. Companion results in the same paper (Theorems 4.1 and 4.2, separate missions) specialize to convex and strongly convex models.
Formalizing it. The theorem is proved on paper; no machine-checked version exists, on this platform or in Mathlib, of Theorem 4.3, of Lemma 2.2 for extended-valued weakly convex functions, or of the one-sided-model framework. A formalization yields a reusable Moreau-envelope library for weakly convex functions with constraints (via the domain of ), and a template for iterate-level stochastic analysis on product probability spaces.
The algebra of each step is short; what is hard is making it rigorous. First, Lemma 2.2 must be proved for extended-valued closed functions: existence and uniqueness of the proximal point need strong convexity of the subproblem together with lower semicontinuity and a quadratic minorant, and differentiability of the envelope is not a consequence of a generic envelope theorem. Second, the conditional expectations in Lemma 4.2 must be realized on the product space of samples, with integrability of , and established along the iterates rather than assumed; the paper takes all of these for granted. Third, Assumption B gives the Lipschitz bound (4.2) only in one direction and only almost surely, and the argmin of Algorithm 4.1 exists only almost surely, so every pointwise step must be carried through null sets that depend on the current iterate.
EuclideanSpace ℝ (Fin d). The extended-valued (and ) is a pair ; closedness, weak convexity, the envelope (an infimum over ) and proximal points are defined in this encoding. The envelope parameter is written lam.Bayesian inverse problems and conditioned diffusions lead to probability measures on function spaces, and these are sampled in practice through finite-dimensional approximations on with large. A Markov chain Monte Carlo method is useful in this setting only if its convergence rate does not deteriorate as the discretisation is refined. Random walk Metropolis (RWM), the default Metropolis–Hastings algorithm, is known from diffusion-limit analyses to need step sizes of order for Gaussian-type targets (Roberts, Gelman and Gilks 1997; Beskos, Roberts and Stuart 2009). Those results describe a scaling limit of the chain in stationarity; they do not bound the speed of convergence of the chain itself.
Hairer, Stuart and Vollmer (arXiv:1112.1392v4, Ann. Appl. Probab. 2014) prove that the preconditioned Crank–Nicolson algorithm has a spectral gap bounded below uniformly in , and in §2.4 they show by an explicit example that RWM does not: its -spectral gap vanishes as , faster than any power of unless the step size decays at least like . This mission formalizes that negative result.
Fix . The target is the Gaussian measure
on : the coordinates are independent and . Its covariance satisfies .
A Metropolis–Hastings kernel with proposal kernel and acceptance probability is
RWM with step size proposes with and accepts with probability . The resulting kernel is reversible with respect to . The expected acceptance probability from is .
For a Markov kernel with invariant probability measure , write , and
is the -spectral gap. The conductance is
The step size is scaled with the dimension as with and ; is for and .
For , and every , there is a constant , independent of , such that
For and there is a constant , independent of , such that for all .
The theorem separates two algorithms that differ only in their proposal. For the same Gaussian targets (the case of the paper), the preconditioned Crank–Nicolson algorithm has an -spectral gap bounded below uniformly in , while RWM's gap collapses. For a reversible chain the spectral gap determines the worst-case asymptotic variance of ergodic averages over observables, so for RWM at a fixed step-size decay that worst case grows faster than any polynomial in . Proposition 2.16 is reusable on its own: it bounds the spectral gap of every Metropolis–Hastings kernel by the acceptance probability or by the proposal's flow, on any measurable space. It also turns diffusion-limit statements about acceptance rates into bounds on the spectral gap.
The results are proved in the paper (Cheeger's inequality is cited from Lawler and Sokal 1988 and Sinclair and Jerrum 1989). No part has a machine-checked proof. The prove2me library has Cheeger's inequality for finite-state reversible chains (MarkovMixing.cheeger_upper), not for kernels on general measurable spaces with the operator norm. A complete development would contain the first formal Cheeger upper bound in that generality, the Metropolis–Hastings conductance bounds, and an explicit Gaussian computation for RWM.
Three steps resist a direct transcription. First, Cheeger's inequality has to be stated and proved for the Markov operator on of a general measurable space: is a Bochner integral that is finite only -almost everywhere, and every identity relating to the flow between sets passes through invariance and centring. Second, the acceptance bound is an exact Gaussian computation in dimensions with explicit constants, where an off-by-one in the coordinate weights changes the target. Third, the asymptotic step: the acceptance probability is small only on sets where the weighted quantity is controlled, but a typical draw from has of order . A bound on over all of , or over a Euclidean ball, gives no decay, and the set used in Proposition 2.16 must keep -mass bounded away from uniformly in while decays on it faster than every power of .
Fin m → ℝ. The Lean coordinate i : Fin m is the paper's , with variance and weight . The target is Measure.pi of gaussianReal 0 (1/(i+1)^2).Q.withDensity α + Kernel.id.withDensity (rejection mass), with α : X → X → ℝ≥0∞. Every statement assumes α ≤ 1 and joint measurability (without it withDensity is the zero kernel). The RWM acceptance probability is Algorithm 2's with , with the exponential (display (1.4) omits it, a misprint).eLpNorm. For a -invariant Markov kernel the ratio set is bounded by , and for with it is nonempty, so is not a junk value.A seller with several goods and a single buyer is the smallest setting in which multi-dimensional mechanism design differs from the one-good theory. For one good, Myerson's theorem (Myerson 1981) says the optimal mechanism posts a price. For two or more goods the optimal mechanism may use lotteries, may be non-monotone in the buyer's values, and is in general not known in closed form. Practitioners nevertheless use simple mechanisms, and the question that Hart and Nisan (arXiv:1204.1846v3) ask is quantitative: what fraction of the optimal revenue does a simple mechanism guarantee?
This mission concerns the simplest mechanism of all, bundling: one posted price for the set of all goods. When the goods are independent and identically distributed, bundling is known to become nearly optimal as the number of goods grows for a fixed distribution (Armstrong 1999; Bakos and Brynjolfsson 1999). That limit is not uniform over distributions. Theorem D of Hart and Nisan gives the uniform guarantee: for every and every distribution, bundling i.i.d. goods earns at least of the optimal revenue.
Timeline. Armstrong (1999) and Bakos–Brynjolfsson (1999) proved the asymptotic optimality of bundling for a fixed distribution. Hart and Nisan circulated the first version of this paper in 2012 (EC 2012), proving Theorems A–D; the version formalized here is arXiv:1204.1846v3 (2017), published in J. Econ. Theory 172 (2017). Li and Yao (2013) later improved separate selling for i.i.d. goods to , and Babaioff, Immorlica, Lucier and Weinberg (2014) showed that the better of separate selling and bundling is a constant-factor approximation for independent goods.
There are goods and one buyer with additive valuation , drawn from a known distribution. A mechanism assigns to every reported valuation an allocation vector (the probabilities of receiving each good) and a payment . The buyer's payoff is . The mechanism is incentive compatible (IC) if for all , and individually rational (IR) if for all . For a random valuation , the expected revenue is and the optimal revenue is
For one good, . The bundled revenue is the one-good revenue of the total value, , and the separate revenue is .
" i.i.d. goods" means that are independent with a common law on . Write and .
Two auxiliary objects appear in the milestones. A real random variable is stochastically dominated by if for every . The equal-revenue (ER) law is that of with for . The constant is the unique real solution of .
The constant is absolute: it is chosen before and before the distribution. This is the statement as printed; it fixes neither the constant nor the base of the logarithm.
The milestones follow the paper's proof: Myerson's formula (1); monotonicity of one-good revenue under domination (Proposition 11); the ER characterization (Lemma 20) and the tail of a weighted sum of two ER goods (Lemma 21); (Proposition 24); for two independent goods (Proposition 13 (i)); for i.i.d. goods (Proposition 14 (ii)); the decomposition Theorem 7; the power-of-two bound ; monotonicity of and in ; and the explicit bound above.
Theorem D says that for identically distributed goods the gap between the simplest mechanism and the optimal one grows at most logarithmically in the number of goods, uniformly over all distributions, including heavy-tailed ones with infinite mean. The i.i.d. hypothesis is essential: for independent goods with different distributions bundling can recover only a fraction (Example 27 of the paper). Together with Theorem C (separate selling, ) it places the two simple mechanisms on a common scale, and the decomposition Theorem 7 it rests on is a general tool for independent groups of goods.
The result is proved in the paper; no machine-checked version is known to exist. A formalization adds: a Lean model of multi-good mechanisms with IC, IR and expected revenue in the extended reals; a checked version of Myerson's one-good formula for arbitrary laws on ; the equal-revenue law and its two-good convolution; and a checked reduction from the decomposition theorem to the logarithmic bundling guarantee. Shorter arguments or a better constant are also welcome.
The obvious argument fails at the first step: revenue is not monotone in the valuation for two or more goods (Hart and Reny 2015), so one cannot bound by replacing each good by a dominating ER good. Every comparison therefore has to pass through one-dimensional quantities, and the multi-good step (Theorem 7) is a statement about expectations of a mechanism's payments conditioned on an independent block of goods. Proposition 14 (ii) must handle distributions where no optimal one-good price exists and may be infinite (the paper's proof speaks of "an optimal price"). Proposition 24 is an exact evaluation whose answer is defined only implicitly, through . The induction itself must track how block sums of i.i.d. goods are again i.i.d.
Valuations are laws: a -good random valuation is a probability measure on Fin k → ℝ≥0, and i.i.d. goods with law form Measure.pi (fun _ : Fin k => ν). Two independent groups have the product law on the disjoint union of their index types (jointLaw); the two-good statement Proposition 13 (i) uses this encoding on Unit ⊕ Unit. A mechanism is a pair of functions; the admissible class requires , IC, IR, and a measurable payment rule, the last being the without-loss-of-generality pin of the paper's footnote 12. The expected revenue of one mechanism is an EReal difference of two lower integrals, never a Bochner integral (which would be for non-integrable payments). is a supremum in ℝ≥0∞, so infinite revenues are represented. is a real parameter with the hypothesis , not a Lambert- value. Logarithms are natural in Theorem D and base 2 (Real.logb 2) in the proof's explicit bounds, as printed; every statement with a logarithm keeps .
The paper states Theorem D as a lower bound on an infimum of ratios ; the formal goal is the multiplicative inequality, which agrees with it wherever the ratio is defined and requires when . A formalization in which may depend on or on the distribution, or in which is computed with a Bochner integral, would trivialize the statement and is ruled out by the binder order and the definitions above.
The definitions are a mission-local copy of the model shared by this series (missions 1–5), so they can be merged later. Not posed here: Theorem C, Proposition 25, Corollary 23, Lemma 22, Example 32, the GFOR notation, and the asymptotic optimality of bundling (Appendix A.5). Proofs of any milestone are welcome, as are reusable lemmas on posted prices, stochastic domination of sums of independent variables, and binomial medians.
A population can disappear because its average growth rate is negative when it is rare, even if its deterministic dynamics would support coexistence. Interactions among several species make this harder to assess: a species may be rare while the remaining species fluctuate among several possible long-run configurations. Hening and Nguyen study this problem for nonlinear systems driven by correlated environmental Brownian noise. Their analysis treats the noncompact state space , where population sizes have no fixed upper bound. The central result of this mission gives a quantitative form of approach to the boundary when one boundary community acts as a sink: the expected positive moment of the smallest population size tends to zero. The source is Hening and Nguyen, Coexistence and extinction for stochastic Kolmogorov systems, arXiv:1704.06984v1, Theorems 1.2 and 5.1.
There are species. Their abundances form . Species has per capita drift and environmental noise intensity at state . A matrix correlates the noise: for a vector of independent standard Brownian motions, and . The stochastic Kolmogorov system is
The factor makes the state absorbing in that coordinate. Consequently each collection of present species defines an invariant face of the orthant. The interior consists of states where every species is present. The paper uses throughout. Its standing Assumption 1.1 requires local Lipschitz coefficients, nondegenerate noise in each population subspace, and a negative large-state drift condition (1.2) expressed through positive and . These conditions place the same control on the unbounded part of the orthant in every theorem below. Source, §1.1, pp. 3–4.
A probability measure is invariant if the law of remains when has law . It is ergodic if it is an extreme point of the invariant probability measures. Let contain the ergodic invariant measures supported on the boundary . This set includes the Dirac law at zero. For any invariant , the invasion rate of species is
The term records the effect of environmental variation on logarithmic population growth. For , let be its present species and its coordinate face. The set contains boundary ergodic measures supported on the boundary of that face. Assumption 1.3 requires for every and, when , a positive invasion rate among for every finite convex combination of measures in . Thus the missing species decline near , while the community on its face resists collapse to a smaller face. Source, pp. 5–6.
The goal is Theorem 1.2 in the explicit quantification of Theorem 5.1. Let satisfy the paper's bound (3.2). For every and every ,
This is the moment form of approach to the boundary. It does not specify which species tends to zero on a given path. The companion targets retain the paper's route: strong solutions and face invariance in Lemma 3.1, moment and Feller estimates in Lemma 3.2, zero resident invasion rates in Lemma 5.1, the weighted negative margin (5.1)–(5.2), the averaged drift bound in Lemma 5.2, local contraction in Proposition 5.1, global control in Lemma 5.3, the capped one-step bound (5.11)–(5.12), and transience in the interior. Source, §§3 and 5.
The conclusion detects extinction pressure without asking in advance which coordinate disappears. Since the minimum of the coordinates is small whenever the system is near any boundary face, it applies even when trajectories may approach different faces. The paper uses this result before its stronger classification theorem, which adds assumptions to determine the fate of particular species. Theorem 1.2 is proved in the cited paper; this mission seeks a machine-checked development of that known result and its supporting stochastic estimates. In particular, the formalization makes explicit how invariant measures on smaller faces control a statement about solutions starting in the full interior. Source, Theorems 1.2 and 1.3.
A negative invasion rate at one boundary law does not by itself control the whole trajectory. The surviving species can fluctuate toward a still smaller face, where a missing species may have a different growth rate. Assumption 1.3 excludes that obstruction by quantifying over boundary ergodic laws of the selected face. Another obstacle is unbounded population size: a local bound near the face cannot alone give convergence of expected moments. The paper combines face-specific estimates with global moment control; encoding both regimes faithfully is the main mathematical burden. The compact-state intuition cited in the paper does not immediately apply to the noncompact orthant. Source, Remark 1.6 and §5.
Lean represents by the published EthierKurtz.SDEState n, with coordinates indexed by Fin n from zero to . The SDE uses the published strong Brownian solution interface; a common probability space, Brownian motion, and solution family replace the paper's notation and . The model reads coefficients at the componentwise positive part off the orthant, where the source never evaluates them. Assumption 1.1(3)'s strict limit superior becomes an equivalent eventual negative bound. Ergodicity is extremality. The index set is defined through positive -mass of . Finite convex combinations, rather than a closure of their hull, implement the paper's .
The stated goal requires and ; would make the displayed expectation equal to one. Theorem 5.1 suppresses the latter restriction, while Theorem 1.2 states it. Lemma 5.2's displayed average divides by , so its is positive, as its proof says, despite the printed . The weights, time threshold, and contraction exponent are chosen before the points and times over which their bounds hold. Boundary ergodic measures are not assumed to be absent; the explicit target records nonemptiness. The definitions of , invariant measures and invasion rates, together with finite-dimensional stochastic integration and moment estimates, are reusable beyond this mission. Contributions that establish these interfaces or prove the listed paper statements are in scope.
The radius of (3.1) is positive. The freely chosen is below one, as Appendix A uses, and the extinction weights are selected with . Scaling all positive weights and the margin preserves (5.2) and makes the paper's finite. Bounds involving real expectations explicitly include integrability, so Lean's value for a nonintegrable integral cannot satisfy them by default. The transience target applies to each compact interior set with nonempty interior, as the proof on p. 24 does.
Ecologists model interacting populations — competitors, predators and prey, food chains — by Kolmogorov systems, in which the growth of each species is proportional to its current abundance. Environmental fluctuations turn these into stochastic differential equations, and the basic question becomes which species persist and which go extinct. Hening and Nguyen (arXiv:1704.06984, Ann. Appl. Probab. 28(3), 2018) gave sharp answers for a general class of such systems on the non-compact state space , extending the compact-simplex theory of Schreiber, Benaïm and Atchadé (SBA11).
The paper has three main results: persistence when every boundary ergodic measure repels (Theorem 1.1), extinction in mean when one boundary measure attracts (Theorem 1.2), and a classification of which species die out (Theorem 1.3). This mission formalizes the third. When the community does not persist, Theorem 1.3 says that each path settles near exactly one "sink" measure on the boundary, and identifies the species that vanish and their rates of decay.
Timeline: Schreiber, Benaïm and Atchadé (2011) proved persistence criteria for stochastic population models on the simplex . Evans, Hening and Schreiber (EHS15, 2015), studying patch-selection strategies in stochastic environments, extended the limit theorem for occupation measures to locally compact state spaces. Hening and Nguyen (2017/2018) proved persistence with exponential convergence and the extinction classification for general Kolmogorov systems.
Let , , , , and . The abundances solve
where for an -dimensional standard Brownian motion , and . Assumption 1.1 asks that be positive definite, that be locally Lipschitz, and that a dissipativity condition (1.2) with a vector and a constant hold at infinity.
An invariant probability measure is one with for all ; it is ergodic if it is an extreme point of the invariant probability measures. is the set of ergodic invariant probability measures supported on ; it contains the Dirac mass at the origin. For , is the set of species charged by and its complement. The Lyapunov exponent of species at is
A measure is a sink (Assumption 1.3) if for all and, if , every finite convex combination of ergodic measures living on the relative boundary of the face of has . is the set of sinks and .
The occupation measures of a path are , and is the set of weak limits of as . Assumption 1.4 asks that for some ; Assumption 1.5 asks that or that every finite convex combination of measures of has .
Under Assumptions 1.1, 1.4, 1.5 and , for every ,
In the order the proof uses them: ; Lemma 3.3 (moment bound and a zero-mean identity for invariant measures); Lemma 5.1 ( for ); Lemma 5.4 (bounded weighted time averages and a strong law for the stochastic integral); Lemma 5.5 (time spent in a compact set, and staying away from a face on a finite horizon); Lemma 5.6 (convergence of unbounded time averages); Lemma 5.7 ( consists of invariant measures); Lemma 5.8 (a limit set inside the face of a sink is that sink); Lemma 5.9 (sinks attract nearby paths with high probability); and the case , where .
Theorem 1.3 turns local information — the signs of finitely many Lyapunov exponents at boundary ergodic measures — into a global almost-sure description of long-run behaviour: the community converges, in the sense of empirical distributions, to one of the sinks, each sink is reached with positive probability, and the species absent from it decay exponentially at explicit rates. In the applications of §2 of the paper (competitive Lotka–Volterra systems, food chains) this answers which species survive.
The theorem is proved on paper. No part of it is machine-checked. A formalization would produce a checked interface between Itô calculus for multidimensional SDEs, ergodic theory of Feller processes (occupation measures, invariant and ergodic measures), and the stochastic-persistence framework; the statements of Lemmas 5.4–5.7 are reusable for other SDE models with a Lyapunov-type condition.
The obvious argument — the occupation measures converge to some invariant measure, and the Lyapunov exponents at that measure decide the fate of each species — breaks down at two points. First, the state space is not compact and the functions are unbounded, so weak convergence of occupation measures does not by itself give convergence of time averages of these functions; a pathwise uniform-integrability bound (Lemmas 5.4 and 5.6) is required, and this is where Assumption 1.4 enters. Second, a limit point of occupation measures is in general a mixture of ergodic measures, possibly including repellers; ruling out every mixture that is not a single sink requires the separate arguments of Lemma 5.8 and of the step, together with a supermartingale built from a Lyapunov function near each sink (Lemma 5.9).
The state space is EuclideanSpace ℝ (Fin n) with the published Ethier–Kurtz strong-SDE layer; coordinates are indexed by Fin n, the norm in every assumption is the norm, and is a hypothesis. The process is a family of strong solutions , one from each , driven by one Brownian motion on one probability space. The coefficients are read at the positive part of the state, which is the state itself on . Ergodic means extremal among invariant probability measures, is the set of coordinates that are not -a.s. zero, means finite convex combinations with positive weights (as on p. 5), and weak limits are taken along sequences, tested against bounded continuous functions. The sum in (1.11) is an unconditional sum in over the set , with no finiteness assumption.
Deviations from the page, each disclosed in the item: (5.19) is stated for every finite horizon rather than for , which is undefined under the lemma's hypotheses; Lemma 5.9 takes ; the convention of Assumption 1.4 is an explicit hypothesis where the exponent appears; integrability claims that the paper treats as automatic are part of the conclusions; and (5.17) is stated for every continuous version of the Itô integral. Lemma 5.6 is stated for each path that stays in the orthant, which the solution does almost surely. The proof's claim "" is left as source context: its inclusion in the finite convex hull of requires an additional argument when is infinite.
The statements cannot be made vacuous by the definitions: is itself a milestone, so is never empty, and the occupation measures are probability measures for ; every constant (, , , ) is chosen before the points it must be uniform in.
A complete development needs Itô's formula for , the strong law for continuous martingales with bounded quadratic-variation growth, Prokhorov's theorem and lower semicontinuity of integrals under weak convergence, and the Feller and strong Markov properties of (1.1). Contributions of any of these, and of the milestones in any order, are welcome.
A seller who owns several goods and faces buyers with private values must decide how to sell them. The revenue-maximizing mechanism is known in closed form only for one good: for a single buyer it is a posted price, and for several buyers it is Myerson's optimal auction (Myerson 1981). With two or more goods the optimal mechanism may use lotteries, may be impossible to describe compactly, and may behave non-monotonically in the value distribution. This makes simple mechanisms with provable revenue guarantees the practical question: how much of the optimal revenue does a seller lose by selling each good separately with its own optimal one-good mechanism?
Hart and Nisan (arXiv:1204.1846v3) answer this for one buyer and two independent goods (their Theorem A): selling separately earns at least half of the optimal revenue. Their Theorem 18 (p. 29), proved in Appendix A.7 as Theorems 33 and 34, extends the factor to any number of buyers. This mission formalizes the dominant-strategy half, Theorem 33, in which the buyers may be arbitrarily correlated with one another, as long as the two goods are independent.
One seller sells goods to buyers. Buyer 's value for good is a number ; a valuation profile is , and is buyer 's valuation vector. The profile is random, , with a commonly known joint law.
A mechanism gives each buyer an allocation (the probability that receives each good) and a payment , as functions of the reported profile, subject to feasibility: for every good . Buyer 's payoff is , and the seller's revenue is .
The expected revenue is , and
For two goods write and for the vectors of the buyers' values for good 1 and good 2, so . is the optimal dominant-strategy revenue from good 1 alone, sold to the same buyers. Finally .
If and are independent, then
No independence among buyers is assumed: the values for the same good may have any joint law.
With independent buyers and two independent goods, so that all values are independent (footnote 27), the same inequality holds for Bayesian Nash implementation: .
The result. Theorem 33 shows that the factor- guarantee of separate selling does not depend on there being a single buyer, nor on the buyers being independent, provided incentive compatibility is required in dominant strategies. It reduces a two-good, -buyer design problem, whose optimum is not characterized, to two one-good problems, each of which can be handled by known single-good auction theory. Remark (a) on p. 29 records that the dominant-strategy statement holds for correlated buyers, while Remark (b) there explains, via Crémer and McLean (1988), why the Bayesian Nash analogue cannot be extended to correlated buyers.
Formalizing it. The result is proved in the paper; to our knowledge no machine-checked version exists. A formal proof requires multi-agent mechanisms on , the Lebesgue integral of a possibly non-integrable revenue, conditioning on an independent coordinate of a product law, and the subdomain property of Remark (b). The definitions here (feasible multi-buyer mechanisms, IC-DS, IR-DS, , and the Bayesian Nash counterparts) are reusable for any multi-buyer revenue-maximization result.
The obvious first idea is to apply the one-buyer Theorem A buyer by buyer. It fails: the feasibility constraint couples the buyers, so a multi-buyer mechanism does not decompose into single-buyer mechanisms, and the revenue extracted from one buyer depends on the reports of all the others. Any reduction to one-good problems must produce, from a two-good mechanism, one-good mechanisms that remain feasible and dominant-strategy incentive compatible for every buyer at once. On the measure-theoretic side, payments of an incentive compatible mechanism may be negative and non-integrable, so expectations must be handled in the extended reals, and the passage from bounds that hold for each fixed value of one good to a bound in expectation needs the product structure of the law of .
x : Fin n → ι → ℝ≥0 (x j i ); a random profile is given by its law, a probability measure on that space. One good is ι = Unit, two goods are ι = Fin 2 (good 1 is index 0). The law of two independent goods is twoGoodsN μY μZ, the image of the product law ; μY and μZ are arbitrary probability laws on , so correlation among buyers is allowed.Function.update x j x'. Feasibility is part of admissibility; without it a mechanism could sell each good to every buyer.EReal difference of the integrals of and , never a Bochner integral, which would vanish on non-integrable revenues. takes values in .Contributions of every kind are welcome: proofs of the milestones, of Theorem 34, and general lemmas on multi-buyer mechanisms.
The generalized Turán number is the largest number of copies of a graph in an -vertex graph containing no member of a family . With it is the classical Turán number; the systematic study of general began with Alon and Shikhelman (2016), and cycles are its most studied case: Bollobás and Győri bounded , and Gerbner and Palmer determined .
Gerbner, Győri, Methuku and Vizer, Generalized Turán problems for even cycles (J. Combin. Theory Ser. B, 2020; arXiv:1712.07079), count copies of one cycle in graphs avoiding another. For even cycles they show . Most extremal constructions there are bipartite, so they also study the bipartite generalized Turán number. For the first non-trivial pair, six-cycles in a graph avoiding eight-cycles, they determine its leading term exactly. This mission formalizes that result, Theorem 12 of the paper.
All graphs are finite and simple. A -cycle is a cycle with vertices. A copy of in is a subgraph of isomorphic to ; is the number of copies, so a cycle is counted once regardless of its starting point and direction. A graph is -free if no subgraph of it is isomorphic to (induced or not). A graph is bipartite if its vertices can be split into two classes and with every edge joining to .
The proof works with a fixed bipartition of a -free graph and uses the following notions.
In Lean, is exBip n (cycleGraph 6) {8}, and is Mathlib's copyCount.
This is two-sided: for some constant and all large .
Theorem 12 is the only case of the paper where a bipartite generalized Turán number of two even cycles is determined up to a lower-order term. Theorem 10 gives the order in general, and Remark 2 gives bipartite upper and lower bounds whose ratio tends to 1 only as . Theorem 12 settles exactly. The authors conjecture that the non-bipartite number has the same asymptotics, but this is open. The argument also links graph counting to Berge hypergraphs: Claim 7 reduces the fat 6-cycles to a Berge--free hypergraph, whose total edge size is controlled by Corollary 7.
Theorem 12 is proved in the paper. As far as a search of the Prove2Me catalogue shows, neither it nor any of its claims has a machine-checked proof. Formalizing it means:
The obvious bound fails. Every 6-cycle in a bipartite graph has three vertices in each class, and each pair of them has some common neighbours. If no pair had more than three common neighbours, each triple in would lie on at most six-cycles, giving roughly cycles, not . The leading constant needs two refinements. First, triples on more than cycles must be shown to be rare. Second, cycles through pairs with many common neighbours (fat pairs) must be bounded separately, by . That second bound is the main obstacle. A fat pair alone can lie on many cycles, so counting fat pairs is not enough. What makes the bound work is the near-disjointness of the common neighbourhoods (Claims 4–6) together with a hypergraph Turán estimate.
Vertices and copies. Graphs are SimpleGraph (Fin n), or a general finite type in milestones about a single graph. Copies are unlabelled (copyCount, the number of subgraphs isomorphic to ): has copies of , not .
Bipartiteness. In it is Colorable 2. In the milestones it is an explicit bipartition that excludes edges inside a class. -freeness is (cycleGraph 8).Free G.
The maximum. is a supremum of natural numbers over a nonempty finite set, since the empty graph is admissible. It is therefore a true maximum; a sanity file proves this.
Cycles inside the proof. Labelled 6-cycles are injective maps from with consecutive images adjacent. Claim 8 counts fat 6-cycles labelled, which changes only the constant.
Landau terms. Every is an explicit constant, quantified before and the graph. The goal uses Mathlib's IsBigO of against .
Corrections to the printed text.
Ruled-out encodings. Some encodings would make the statements trivial or wrong, and none of them is used:
Infrastructure. A complete development needs:
The Berge-cycle and -free bounds can be reused beyond this mission. Contributions are welcome at any level: proofs of individual claims, of Corollary 7, or the final assembly.
A seller who knows the distributions of a buyer's values for several goods can, in principle, design a mechanism that offers lotteries and prices conditional on the buyer's reported values. Finding the best such mechanism can be difficult even with two goods. Separate selling is much simpler: choose a one-good price for each item and let the buyer decide item by item. The question is how much revenue this simplicity can cost when the goods' values are independent. Hart and Nisan establish a guarantee that declines only with the square of the logarithm of the number of goods, even though the distributions need not be identical or bounded. Their result is Theorem C of Approximate Revenue Maximization with Multiple Items, stated on p. 7 and proved on p. 26.
The paper grew from the problem of comparing easy selling formats with fully optimal mechanisms. For one good, a posted price characterizes optimal revenue. With multiple goods, the choice of a mechanism becomes genuinely multidimensional: its allocation rule can correlate the disposition of the goods and use lotteries. The guarantee in this mission applies uniformly over all independent distributions on nonnegative valuations, so a seller does not need a regularity, density, or finite-moment assumption to use it.
There is one seller, one risk-neutral buyer, and goods. The buyer's valuation vector is ; receiving a set of goods gives the sum of the values of its members. The seller knows the joint law of the random vector , but not its realization. In this mission the coordinates are independent, with possibly different probability laws .
A direct mechanism consists of an allocation rule for each good and a real payment . At a truthful report , the buyer's payoff is . The mechanism is incentive compatible if truthful reporting is at least as good as every alternative report, and individually rational if for every . The seller's expected payment is its revenue. The optimal revenue is the supremum of revenue over such mechanisms. Payments are taken to be measurable, following footnote 12 on p. 12 of Hart and Nisan.
For one good, equals the supremum of over prices , as in display (1) on p. 12. The separate revenue is . The bundled revenue is , where the sum is treated as one good. Both formats are defined through one-good revenue, even when the full optimum can use multidimensional allocations.
The goal is the inequality form of Theorem C, with one constant that works for every number and every family of independent goods:
Here has law , and the joint law is their product. The paper phrases the headline as a guarantee for an approximation ratio; the displayed inequality is the form used in its proof on p. 26. It handles zero and infinite optimal revenues without introducing a ratio with an undefined denominator.
The milestone list records the one-good posted-price formula, monotonicity under first-order stochastic domination, the equal-revenue comparison of Lemma 20, Proposition 13(ii)'s comparison of separate and bundled revenue, the two inequalities of Theorem 7, and the two-good base case of Theorem A. It also records the power-of-two estimate and the zero-padding assertion stated in the proof of Theorem C. Each milestone is attached to its source page in the pinned preprint.
The theorem gives a distribution-independent performance floor for a mechanism that can be run using one price per good. It applies to unequal and unbounded independent distributions, for which expected values can be infinite while one-good optimal revenues remain finite. The comparison is with the best incentive-compatible and individually rational multi-good mechanism, including randomized allocations, rather than with another simple selling format. The result is proved in the 2017 preprint; the open work here is a machine-checked formalization of that known result and its selected supporting statements.
The formal development also supplies reusable objects: a law-based direct-mechanism model, extended-real expected revenue, product laws for independent groups of goods, and first-order stochastic domination of one-good laws. These are useful for other comparisons among separate selling, bundling, and optimal mechanisms in the same paper. The mission does not pose the paper's distinct i.i.d. bundling theorem, multi-buyer results, or tightness examples.
The main obstacle is that optimal multi-good revenue is not monotone in the values of the goods. Increasing each coordinate of a valuation vector does not, by itself, give a valid comparison between the optimal revenues of the two vectors' laws; Hart and Nisan, p. 23 explicitly warn against that inference. One-good revenue does have the needed monotonicity, but the full optimum can depend on how the goods interact in an incentive-compatible mechanism. Theorem 7 is a substantive bridge between these two regimes. Infinite expected values also make a real-valued integral or an ordinary ratio unsuitable for the general statement.
Goods are indexed by finite types, and valuations lie in . Each good's law is a probability measure; independence means the product law, while Theorem 7 allows dependence among coordinates within each of its two independent groups. A one-good law is represented by a singleton coordinate type. Revenue takes values in , and the expectation of a mechanism's possibly negative payment is represented in extended reals. The supremum defining optimal revenue ranges only over feasible, incentive-compatible, individually rational mechanisms with measurable payments. Theorem C quantifies before and the laws, and the restriction keeps the logarithmic coefficient in its stated domain.
The equal-revenue law is represented by the density on , mapped to nonnegative reals. First-order stochastic domination compares the upper-tail probabilities at nonnegative thresholds, which is equivalent to testing every real threshold for nonnegative valuations. A complete proof will need measure-theoretic facts about that law, the posted-price characterization, product measures, and operations on extended nonnegative revenue. Contributions to those reusable facts and to the selected milestone theorems are within scope.
The Turán number is the largest number of edges in an -vertex graph with no copy of . Its generalized version, introduced systematically by Alon and Shikhelman (JCTB 2016), replaces edges by copies of a second graph : is the largest number of copies of in an -vertex graph containing no member of the family . When both and the forbidden graphs are cycles, these numbers measure how many long cycles a graph can carry while some cycle lengths are excluded and they refine the Bondy–Simonovits even-cycle theorem (JCTB 1974), which bounds the number of edges of a -free graph by .
Gerbner, Győri, Methuku and Vizer (arXiv:1712.07079, J. Combin. Theory Ser. B 2020, DOI 10.1016/j.jctb.2020.05.005) study for cycles. Their Theorem 10 gives ; Theorem 14, the subject of this mission, adds a girth condition: when all cycles of length are forbidden together with , the order of magnitude of the number of 's is . The case answers the question of how many 's a -free graph of girth can have.
All graphs are finite and simple. A copy of a graph in is a subgraph of isomorphic to , and is the number of copies. is the cycle of length ; is the path on vertices (of length ).
For a set of integers, each at least , let ; a graph is -free if it contains none of these cycles as a subgraph. Write . The generalized Turán number is
For vertices , is the number of paths with edges between and . A pair is fat if , and a copy of is fat if all of its pairs of opposite vertices are fat.
The -theta graph joins two vertices by internally disjoint paths of length . For a graph , the theta- graph replaces each edge of by an -theta graph with and adds isolated vertices up to ; here for and for .
For integers and with ,
Both bounds are part of the goal; the constants depend on only.
Theorem 14 locates at for every admissible triple, so in graphs of girth forbidding one further even cycle (with ) caps the number of -cycles at the count achieved by a blown-up -cycle of long paths. The paper uses it to settle the order of magnitude of for every family with , and (Theorem 20), and its case recovers Theorem 10.
The result is proved in the paper; nothing here is open mathematically. To the best of a platform search (2026-10-08), no part of it is formalized: Mathlib has copyCount, cycleGraph and pathGraph, but no generalized Turán numbers, no theta graphs and no counting of paths between two vertices. The mission produces a machine-checked proof of the theorem and of the counting lemmas of §5, which are reusable for other generalized Turán problems with cycles.
The lower bound is an explicit construction, and its difficulty is bookkeeping: proving that a subdivided multigraph has no cycles other than those of lengths and , and counting the -cycles. The upper bound is the substance. A direct count of 's through codegrees, which works for , fails here because paths of length between a pair are not controlled by a single neighbourhood. The paper's route separates fat from non-fat cycles and runs a greedy multiplicity procedure; Claim 14 then grows a by an induction on the cycle length in steps of , which needs the precise intersection pattern of Claim 12 and the detour paths of Claim 13. For the argument goes through layered neighbourhoods and Lemma 27. The argument divides by , so for a different route (Theorems 10 and 11 of the paper) is needed.
Graphs are SimpleGraph (Fin n) for the extremal function and graphs on an arbitrary finite type for the lemmas. Copies are unlabelled (copyCount, subgraphs isomorphic to the pattern); and are Mathlib's cycleGraph a and pathGraph l. exCyc n H A is the supremum, over -free graphs on Fin n, of the copy count; the set is finite and contains the empty graph's count whenever every length in is at least , so it is a maximum. The forbidden family of the goal is Set.Icc 3 (2 * l - 1) ∪ {2 * k}, every length from to together with . , and are Mathlib's asymptotic relations along atTop, with constants fixed before and the graph. counts injective vertex sequences (paths, not walks). The theta graph thetaCycle n m l is an explicit graph on Fin n.
Added or pinned hypotheses, all disclosed in the items: in the goal (the page writes only ; at the family is empty and the statement fails); in Claim 12; where the page divides by ; Lemma 27 with the explicit bound of its proof, which is uniform in ; Claim 15 under the full family , which its proof needs. Claim 14 assumes only girth , not -freeness, since on the page its conclusion at is the contradiction.
The statements rule out the trivializing readings: the goal is two-sided, so an upper bound alone does not close it; exCyc is a genuine maximum, not a junk supremum; copies are unlabelled; the constants come before and the graph; the forbidden family contains all short cycles, not only .
A complete development needs path counting in graphs of large girth (uniqueness of short paths), layered neighbourhoods, the degeneracy argument of Lemma 27, a random bipartition argument for Lemma 25, and cycle structure in theta graphs. Contributions of any milestone, and of general-purpose lemmas on paths and cycles in SimpleGraph, are welcome.
The classical Turán problem asks for the maximum number of edges of an -vertex graph that avoids a fixed subgraph. For even cycles this is one of the central open problems of extremal graph theory: Bondy and Simonovits proved that a -free graph has edges, and this order is known to be sharp only for .
A generalized Turán problem replaces "edges" by "copies of a fixed graph ". The question of how many copies of one cycle a graph may contain while avoiding another cycle goes back to Erdős's question on pentagons in triangle-free graphs, and was taken up systematically by Alon and Shikhelman (2016). For two even cycles, Solymosi and Wong asked whether forbidding the single cycle (instead of all cycles up to length ) still forces few copies of . Gerbner, Győri, Methuku and Vizer answer this question by determining the order of magnitude: the maximum is , much larger than in the girth-restricted setting. The same order of magnitude was obtained independently by Gishboliner and Shapira; the proof formalized here is different and gives explicit constants.
Timeline:
All graphs are finite and simple. For graphs and , is the number of subgraphs of isomorphic to (unlabelled copies). is the cycle on vertices. A graph is -free if it has no subgraph isomorphic to (induced or not). The generalized Turán number is
For a non-negative integer and , the falling factorial is .
For distinct vertices of , the codegree is the number of common neighbours of and . Sums written range over unordered pairs of distinct vertices.
Two graphs appear in the lower bounds. The first is the complete bipartite graph . The second is the blow-up of : keep alternate vertices of , and replace the vertex between and (indices mod ) by a class of new vertices, each joined to and . The new vertices are split as evenly as possible among the classes.
As with and fixed:
The goal is the conjunction of the three bounds, each with its own parameter range. Note that the upper bound has the power , while the second lower bound has the falling factorial .
The lower bounds:
The upper bound:
Theorem 10, combined with Theorem 11 on , gives for all . The one exception is the lower bound at , which comes from the Erdős–Rényi polarity graph. This answers the Solymosi–Wong question in the negative: forbidding one even cycle allows many more copies of a shorter or longer even cycle than forbidding all short cycles does. The codegree method of the upper bound, which bounds by sums of and controls those sums through -counts and paths of length two, is reused in the paper's later results on graphs of given girth (Theorem 14).
On the formal side, none of these results is formalized in Lean. Mathlib has copyCount, cycleGraph and edge-extremal numbers, but no generalized Turán numbers, no Erdős–Gallai circumference theorem and no Bondy–Simonovits theorem. The mission produces:
The paper's printed version of the Erdős–Gallai bound, , is incorrect. The mission states the bound that Erdős and Gallai proved, which is all the argument needs.
The two lower bounds are explicit counts. The difficulty there is combinatorial bookkeeping in Lean. One task is matching unlabelled copies (copyCount) with the Hamiltonian cycles of . The other is showing that the blow-up contains no cycle other than 4-cycles and full -cycles, so that its -cycles are exactly one choice per class.
The upper bound rests on two classical theorems that are absent from Mathlib:
Without (1) one has only and no control of . Without Claim 1 the chained sums in (3) are not bounded by per step. The naive estimate, which bounds each by the maximum codegree, does not work: in a -free graph a single codegree can be of order , and that only gives .
Graphs are SimpleGraph (Fin n). Cycles are Mathlib's cycleGraph. is G.copyCount H, the number of unlabelled copies (not labelledCopyCount, which is times larger). is exCyc n H A, an sSup over -free graphs on Fin n. The underlying set is finite and contains , from the empty graph, so the value is an attained maximum and not a junk sSup.
Each is a function with , depending only on and and chosen before , with the bound holding for all large . Sums over are over unordered pairs (Sym2 off the diagonal). With ordered pairs every constant would change by a factor of two, and (2) would be false. Tuples of distinct vertices are embeddings Fin l ↪ V, with indices mod . is Nat.descFactorial (k - 1) l.
Hypotheses added relative to the page:
Theorem 2 states the corrected bound .
The following do not count as the goal: a one-sided goal with only the upper or only the lower bound; a version with labelled copies; a constant or that depends on or on the graph; and a single unified parameter range.
A complete development needs:
The Erdős–Gallai theorem, Bondy–Simonovits and the codegree identities are reusable well beyond this mission, and contributions of any of them are welcome.
An extremal graph question asks how many copies of one pattern can occur when other patterns are forbidden. When the counted pattern is a cycle, the answer depends strongly on which shorter cycles may occur. Excluding only an even cycle and excluding all cycles up to a given length are different constraints. The latter imposes a girth condition, meaning that nearby vertices cannot be connected by the many short alternative routes that otherwise create small cycles. For odd cycles, this makes a direct application of ordinary edge-count bounds inadequate: many graphs with relatively few edges can still arrange those edges into many copies of a fixed cycle.
Gerbner, Győri, Methuku and Vizer study generalized Turán numbers for cycles and paths. Their Theorem 17 bounds the number of copies of a particular odd cycle when every cycle of lengths through , and one further even cycle of length , is forbidden. The lower and upper exponents differ; the theorem supplies a nontrivial interval for the possible growth rate rather than an exact asymptotic formula. The preprint, Theorem 17 is the source used here; its printed page numbers agree with its PDF pages.
Write for the simple cycle on vertices. For a set of integers at least , let . A graph is -free if no member of the family occurs as a subgraph of . The copies need not be induced: an extra edge between vertices of a copy does not erase that copy. When , write for this family. Thus excludes every cycle of length from to and also excludes the single cycle . This notation follows §1 of the paper.
For graphs and , let be the number of unlabelled copies of in : subgraphs of isomorphic to , counted once each. The generalized Turán number is
The graph with no edges is eligible for the forbidden families in this mission, and the finite vertex set makes the maximum well defined. For a vertex and integer , is the set of vertices whose graph distance from is exactly . Vertices in another connected component lie in no with finite .
The lower-bound milestone also uses a hypergraph, a set of hyperedges that are subsets of a common vertex set. It is -uniform when every hyperedge has exactly vertices. A Berge cycle of length alternates distinct vertices and distinct hyperedges; consecutive vertices lie in their connecting hyperedge. Hypergraph girth at least means that no Berge cycle has length less than . These definitions are used in Theorem 29 and §6.2.
Fix integers . The goal is the two-sided statement of Theorem 17, p. 7:
Both estimates concern with and fixed. The paper does not claim that either exponent is optimal for every pair , and these formulas should not be read as an equality of growth rates.
The milestones record the source statements needed on the two sides. Theorem 29 gives -uniform hypergraphs of prescribed Berge girth with at least hyperedges. The lower-bound paragraph of §6.2 turns such hypergraphs into graphs with many copies. Lemma 27 bounds the edges of a graph under a path-restricting partition condition. The local layer identity and Claim 18 control edges in the distance layers and . The final milestone is the low-cycle-vertex conclusion from the paper's deletion passage on p. 28.
The upper exponent is strictly below , so the theorem rules out quadratic growth for this generalized Turán number under the stated forbidden family. The lower exponent shows that the number of permitted odd cycles nevertheless grows faster than linearly. Together they locate the problem between two explicit power laws. These statements belong to a wider set of cycle-count results in the paper, where changing the forbidden family or the parity of its extra cycle changes the resulting bounds; see Theorems 17 and 18.
The paper proves these bounds. The work here is to state its objects and claims so that Lean can check future proofs: the maximum over admissible graphs, unlabelled cycle counts, Berge-cycle girth, and graph distance layers. The present proposal supplies proof targets; their Lean declarations have placeholders for proofs. The finite graph and hypergraph definitions can also serve later formalizations of generalized Turán and girth questions. The exact growth rate between the two exponents is left open by this theorem.
Counting cycles from an ordinary upper bound on the number of edges loses the relation between a cycle and its position around a vertex. The no-short-cycle condition constrains individual distance layers, but a layer can still contain edges that close a . Controlling those edges uniformly across all graphs and vertices is the central issue in the upper bound. A bound with a constant chosen after seeing the graph would say little about the asymptotic maximum; Claim 18 instead requires a constant depending only on and . The lower side has a different requirement: the construction must preserve both the abundance of odd cycles and every exclusion in . The precise assertions are in §6.2, pp. 27–28.
Graphs on vertices are represented as simple graphs on , and is Mathlib's cycle graph. A copy is a subgraph isomorphic to , counted without labels. The extremal number is the supremum of its finite, nonempty set of attainable natural-number counts; in this setting that supremum is the paper's maximum. Distance layers use extended graph distance, which assigns unreachable pairs infinity. The family of forbidden lengths is exactly ; it does not omit any short cycle.
The hypergraph representation is a finite set of distinct finite vertex sets. Berge-cycle existence requires injective lists of vertices and hyperedges, and girth at least is expressed by absence of lengths through rather than a numerical infimum with an exceptional value on acyclic hypergraphs. Theorem 29's threshold is chosen after and before . Claim 18's constant is chosen after and before the graph or vertex. The upper and lower asymptotic bounds are both present, with real exponents; neither is replaced by a one-sided or purely existential statement.
Lemma 27 is given with the explicit edge bound from its proof, uniform in the number of partition classes. The final deletion milestone uses an existential constant because the page mixes several powers of its intermediate constant ; this is recorded in the accompanying audit notes. A complete proof development needs Mathlib's simple-graph copies, paths, graph metric, finite-set counting, and asymptotic notation, plus the hypergraph interface defined for this mission. Proofs of the goal and any of these milestones are welcome.
Which cycle lengths a graph must contain is a classical question of extremal graph theory. A graph on vertices is pancyclic if it has cycles of every length from to ; Bondy's meta-conjecture (Bondy 1971) and a long line of results ask which density or expansion conditions force pancyclicity or, more modestly, force the set of cycle lengths to contain a long interval. For sparse graphs, expansion is the natural hypothesis: random graphs and explicit expanders are sparse, yet very well connected.
Friedman and Krivelevich, Cycle lengths in expanding graphs (arXiv:1912.11011v2; Combinatorica 41, 2021), study two expansion conditions. For the usual vertex expanders they show that cycle lengths are numerous and well spread, but they also note that an expander need not contain any interval of cycle lengths of non-trivial length. Section 4 of the paper therefore introduces a different, two-set expansion condition, the β-graph, and shows that it does force a complete interval of cycle lengths of length linear in . This mission formalizes that result, Theorem 3.
Timeline.
All graphs are finite and simple. For a graph and a vertex set , the external neighborhood of is
Let have vertices and let . is a β-graph if every two disjoint vertex sets with are joined by an edge. For , the complete graph is a β-graph for every ; when , only the complete graph is. No graph on zero vertices is a β-graph.
The set of cycle lengths of is . A cycle of length has distinct vertices.
The proof works with the tree : two complete -ary trees of depth (every internal vertex has children, every leaf is at distance from the root) whose roots are joined by a path of length . A graph contains a copy of a tree if there is an injective map from the vertices of to those of sending edges to edges.
Logarithms are to base .
For every there exist positive constants and such that every β-graph on vertices satisfies
The goal fixes the shape of the bound, not its constants: the proof's choice is , and is a multiple of . As the interval widens towards . The upper end is tight up to the constant: the disjoint union of with isolated vertices is a β-graph.
In the order of the proof (pp. 15–18):
The result. Theorem 3 proves the conjecture of Hefetz, Krivelevich and Szabó in a stronger form: β may be any constant below instead of tending to zero with , and the lower end is of optimal order. Since spectral expanders satisfy the β-graph condition (by the expander mixing lemma an -graph with is a β-graph), the theorem gives long intervals of cycle lengths in pseudo-random graphs. The method, embedding two large trees joined by a path and closing the cycle across their leaf sets, is a template for producing cycles of prescribed length in expanding graphs.
Formalizing it. The result is proved on paper. As far as the platform's records show, none of it is formalized: Mathlib has trees, walks, cycles and graph copies, but no tree-embedding theorem for expanders and no result on cycle lengths of this kind. The main piece of new infrastructure is Haxell's theorem (milestone 3), which the paper cites without proof. Its proof (in Haxell's paper and in Balogh–Csaba–Pei–Samotij) is a few pages of inductive embedding with a Hall-type invariant. A formal proof of Theorem 4.1 would be reusable for any embedding argument for bounded-degree trees, for example in Ramsey and size-Ramsey problems for trees and paths. The printed proof also has a rounding gap (below), so the formal proof will have to settle a slightly different argument from the printed one.
The β-graph condition only speaks about pairs of large sets, while cycles are built edge by edge, so short and long cycles both need a mechanism. The obvious approach, finding a long path and then shortcutting it, does not control which lengths occur. The proof instead needs a robust embedding theorem for trees with about leaves inside a subgraph with good expansion of small sets, and that is Theorem 4.1, a deep result.
A second difficulty is quantitative. In the printed verification of claims (1) and (2) on p. 17, a complete -ary tree of depth is counted as having about vertices, as if exactly. In fact can be almost , and for claim (2) the honest count only covers rather than . For the gap is larger. Theorem 3 is unaffected, because its constants are only and pruning the trees to leaves repairs the count. But a solver following the printed proof will need to repair that step. The two claims are therefore not posed as milestones.
Graphs on vertices are SimpleGraph (Fin n). Vertex sets are Set with Set.ncard, and every inequality involving β, a logarithm or is stated in ℝ after casting. Logarithms are Real.logb 2. Cycles are Mathlib's Walk.IsCycle, so every cycle length is at least . "Contains a copy" is SimpleGraph.IsContained (injective and edge-preserving, not induced). The subgraph of Lemma 4.1 is the induced subgraph on a set , with . The tree is defined on words of length at most over (two tagged copies) plus path vertices.
Conventions of the goal:
Infrastructure needed: Haxell's theorem (reusable well beyond this mission), counting leaves and vertices of complete -ary trees, and turning an embedded plus one edge into a Walk.IsCycle. Contributions to any milestone are welcome, in particular a proof of Theorem 4.1 and a repaired version of claims (1) and (2) with pruned trees.
Interactive decision making covers bandits, contextual bandits and reinforcement learning: a learner repeatedly chooses a decision, observes a reward and an observation drawn from an unknown model, and tries to accumulate nearly as much reward as the best decision for that model. Foster, Kakade, Qian and Rakhlin (arXiv:2112.13487) introduced the Decision-Estimation Coefficient (DEC), a single quantity that gives lower bounds on the regret of every algorithm and, through the Estimation-to-Decisions (E2D) meta-algorithm, matching upper bounds. This mission formalizes the upper-bound side in its strongest form: E2D run with Hellinger confidence sets (Option II of Algorithm 1) has regret controlled by the localized DEC, the same quantity that appears in the paper's lower bounds (Theorems 3.1 and 3.2).
The basic E2D guarantee (33) in terms of the global DEC is already posed on Prove2Me as an open goal (FoundationsRL.GeneralDM.e2d_general_regret_bound_v2, the restatement in Foster and Rakhlin's lecture notes, arXiv:2312.16730, Proposition 26). It is not posed again here.
A decision space is a finite set. An outcome consists of a reward and an observation and ranges over a finite set , and is its reward. A model assigns to every decision a probability distribution on . Its mean reward is , and is a decision maximizing . The learner knows a model class that contains the true model . At round it plays a distribution on , and its regret is
Write for the squared Hellinger distance. For a reference model and the DEC is
The localized class keeps only the models whose optimal value exceeds that of by at most .
E2D with Option II receives at each round an estimate from an online estimation oracle. It keeps the confidence set of models whose accumulated Hellinger error against past estimates, , is at most . It plays a minimizer of the DEC problem over at . Assumption D.1 asks that, with probability , the oracle's Hellinger error on the rounds where is at most a known bound . It also asks that .
With , rewards in and , with probability at least ,
The bound is the paper's most general upper bound. Together with the lower bounds of §3, it shows that the localized DEC characterizes the regret of interactive decision making up to the estimation term. With an aggregating estimator satisfying (App. A.3), it recovers the finite-class guarantee of Theorem 3.3. The companions extend E2D to general divergences, randomized estimators and adversarially chosen contexts. That last setting contains SquareCB for contextual bandits.
All results of this mission are proved in the paper. None was machine-checked before. Formalizing them produces a checked reduction from decision making to estimation for finite decision and outcome spaces, stated against the published DEC and localized-class definitions, so that later bounds on the DEC of specific classes (bandits, tabular RL) can be combined with it.
The non-localized bound follows from the per-round step (138) by summation. The localized bound does not: the per-round DEC is taken over the confidence set , and replacing it by a localized class requires that every model surviving in have optimal value close to that of the current estimate . The confidence set constrains Hellinger errors against past estimates, not optimal values, and the estimate itself is in general not a member of the class. Bridging these is the content of Lemma D.2 and the containment. The first round is a boundary case: there the confidence set is the whole class, so the containment holds only if the radius is at least the full range of the rewards.
Fintype), a finite outcome set , and models m : S → Y → ℝ with every m π a probability vector. Expectations are finite sums. Contexts in Theorem 8.1 range over an arbitrary type.decGf, and dec for the supremum over ) and the localized class are the published FoundationsRL.GeneralDM definitions, referenced and not redefined.IsOptionIIRun (lines 7 and 8 and ). "With probability at least " becomes the hypothesis EventD1, the event of Assumption D.1. Line 8's arg min is relaxed to "certifies the minimax value from above", as Remark 4.1 permits. Rounds are 0-based, and is evaluated at the paper's index.IsOptionIIRun. The open bound (33) is not restated.decGf in the class are reusable beyond this mission.In a cost sharing game (or, symmetrically, a revenue sharing game) self-interested players each pick a set of resources, every resource generates a welfare that depends on who uses it, and a distribution rule splits that welfare among the users. Network formation, atomic routing, coverage and distributed-control problems all fit this model (Anshelevich et al. 2004; Marden and Wierman, Distributed welfare games, 2013; see §2 of the paper). The designer controls only the distribution rule, and the first requirement on a rule is that the games it induces have a pure Nash equilibrium; without one, equilibrium-based efficiency guarantees say nothing.
Which rules guarantee equilibria? The Shapley value and its weighted and generalized-weighted versions do, because they induce potential games (Hart and Mas-Colell 1989). Chen, Roughgarden and Valiant (2010) and Marden and Wierman (Overcoming the limitations of utility design for multiagent systems, 2013) showed that, among budget-balanced rules, these are the only ones that work for every welfare function, by exhibiting one worst-case welfare function (Proposition 1 of the paper, p. 9). Marden and Wierman (Distributed welfare games) also showed that when players may choose only one resource, other budget-balanced rules can work. That left open what happens when the designer knows the welfare functions in advance, and whether dropping budget-balance enlarges the set of good rules. Gopalakrishnan, Marden and Wierman 2014 answered both questions: for any fixed set of welfare functions, with or without budget-balance, the equilibrium-guaranteeing rules are exactly generalized weighted Shapley values on suitable ground welfare functions.
Players are with ; resources are with . A local welfare function is and a distribution rule is , where is the share of player when sharing with the coalition (and for ). Each player has a nonempty action set . In an allocation , the users of are and player receives
Resources with equal welfare functions use the same rule. For a nonempty set of welfare functions, is the class of all such games with every , any number of resources and any action sets. A rule is budget-balanced for if .
A weight system consists of positive weights and an ordered partition of into priority classes. For nonempty , with the first class meeting . With the basis coefficients , the generalized weighted Shapley value is
The distributed welfare of a rule is , display (10).
with the distributed welfare of . One weight system serves all of .
The "if" direction (Appendix A, p. 16). For a single and a budget-balanced guaranteeing equilibria: when contains no contributing coalition (Lemma 1) and for non-contributing (Lemma 2); (Lemma 3). The basis rules of the recursion (27) are budget-balanced for the inclusion functions (Lemma 5), recover (Lemma 7), obey an inclusion–exclusion principle (Corollary 1), and are generalized weighted Shapley basis rules (Lemma 8). Across welfare functions the basis shares are consistent pairwise (Lemma 9) and around cycles (Lemma 10); the induced relation on players is a partial order modulo equivalence (Lemma 11), and one universal weight system replaces all (Lemma 13).
Proposition 2: for welfare functions normalized by , iff and . Theorem 2: the same characterization with generalized weighted marginal contributions on .
The theorem settles the design space completely: a designer who wants equilibria in every game over known welfare functions must use a generalized weighted Shapley value, and the only freedom is the weight system and the ground welfare functions, which control budget-balance. Since these rules induce (generalized weighted) potential games, potential games are necessary for guaranteed equilibrium existence in this model, and computing shares inherits the exponential cost of Shapley values. Theorem 2 gives the marginal-contribution form, which needs one marginal contribution per share.
The paper proves Theorem 1 with a full appendix of counterexample constructions; none of it has a published machine-checked proof. The mission asks for a Lean proof of the characterization, of the reusable structure behind it (necessary conditions, basis decomposition, inclusion–exclusion for basis rules, consistency of weight systems), and of the Shapley–marginal-contribution correspondence.
The "if" direction is a potential argument. The "only if" direction is not: every necessary condition is proved by building, from a hypothetical violation, a specific game with no equilibrium, and the games grow more elaborate as the conditions do. Lemma 8 needs the inclusion–exclusion principle to isolate a single basis share, using many weighted copies of resources; Lemma 10's proof combines best-response cycles over welfare functions and is partly omitted on the page ("We omit the proof for brevity", p. 51), so it is the hardest milestone. A tempting shortcut, applying the worst-case result of Chen et al. and Marden–Wierman (Proposition 1, p. 9), fails: it uses one worst-case welfare function, while here is arbitrary and may not contain it.
Players are Fin n, resources Fin m, an action is a Finset (Fin m) (the empty action is allowed). The family of rules is one function f : Welfare n → Rule n, which encodes that equal welfare functions get equal rules. GuaranteesPNE 𝕎 f quantifies over every m > 1, every assignment Fin m → 𝕎 (repetitions allowed: the counterexamples rely on many copies of one welfare function) and every family of nonempty action sets. A weight system stores a block index Fin K per player (empty blocks allowed) and positive weights. Rules are compared only at . Contributing coalitions exclude (Appendix A's normalization ). The recursion (27) divides by and is used only for contributing ; where it reads with , the paper's convention off is a hypothesis.
The ground welfare in Theorem 1 is the distributed welfare (10), written out, never an arbitrary function: an existentially quantified ground welfare would make the right side easier and the theorem a different one. The weight system is quantified before the welfare functions, and empty action sets are excluded; with them no game would have an equilibrium and the theorem would claim that no rule is a Shapley value.
Disclosed readings: Lemma 11's "partial order" is antisymmetry modulo the equivalence , as the proof states; in (74) the first block is read on as its positive-share block . Proposition 2 carries so that the paper's basis support, which ranges over all coalitions, agrees with the local support of nonempty coalitions.
A complete development needs: finite games and pure equilibria on resource-selection models, Möbius inversion on Finset lattices, the potential argument for generalized weighted Shapley values (shared with the companion mission on generalized weighted potential games), and counterexample games built from copies of resources. The game model and the basis-rule recursion are reusable for other cost-sharing results. Proofs of any milestone, and alternative arguments for the necessary conditions, are welcome.
In random-feature models, also called extreme learning machines or random neural networks, the inner weights of a one-hidden-layer network are drawn at random and only the linear readout is trained. Training is then a least-squares problem, which is why such models, and their dynamic counterparts reservoir computing and echo state networks, are used in practice. The question is how well such a network can approximate a target when it is not allowed to choose its inner weights. Gonon, Grigoryeva and Ortega (Ann. Appl. Probab. 33 (2023) 28–69) answer it with explicit, non-asymptotic bounds. Their first result, Theorem 1, covers static ReLU networks on an arbitrary separable Hilbert space. The later results of the paper, on finite-dimensional inputs and on echo state networks, are built on it.
Timeline:
is a separable real Hilbert space with inner product , and is the rectifier. The inner weights , , are i.i.d. with law . For a readout matrix the random ReLU network is
The target is assumed to have a Fourier representation on the ball of radius : for , with complex measures whose total variations have finite second moments (condition (15)). The sampling law has the product form . Two further quantities enter: , and the density , where . The input is an -valued random variable with law and , independent of the inner weights.
If , condition (i) or (ii) on holds, and the integrals (16) of and are finite, then there is a readout , a measurable function of , with
and for every , with probability at least , . Here and
Milestones 2–6 are stated for a single output component (), to which the proof reduces.
Theorem 1 says that only the readout has to be trained. With inner weights drawn from an essentially arbitrary product law satisfying (i) or (ii), a least-squares readout achieves error with a constant computable from the Fourier data of and the sampling law (Remark 3, p. 38). The finite-dimensional rates of Section 4.2 (Proposition 3, Corollary 1) follow from it, and so do, through the reservoir functional's Fourier representation, the echo state network bounds of Sections 5–6.
The result is proved on paper but has no machine-checked proof. A formal proof needs integral representations of Fourier-type functions by ReLU units, Radon–Nikodym arguments for signed measures on product spaces, and the variance identity for i.i.d. averages. A side product of formalizing it is a correction: the printed constant is false for small and has to be replaced by , which agrees with it for .
There is an obvious argument: sample features from and use Maurey's empirical method. It does not apply, because the features here are ReLU ridge functions of a real-valued bias drawn from , not complex exponentials. The proof must first rewrite the oscillatory representation as an integral of rectifiers, (18)–(20). That step uses the realness of , which is not given and follows only from being real near . The signed measure obtained this way must then be absolutely continuous with respect to the sampling law , with a density whose second moment is controlled by (16). In case (ii), may vanish outside a bounded interval, and the support of has to be matched to it.
A complete development needs the following:
The variance identity (25) and the bound (26) are independent of the Fourier setting and reusable. Contributions to any milestone are welcome, and so are alternative proofs of (19) and (20).
The Turán problem asks for , the largest number of edges in an -vertex graph with no copy of a fixed graph . For even cycles the answer is still not known in general: Bondy and Simonovits proved in 1974, and the order of magnitude is known to be sharp only for .
The generalized Turán problem replaces edges by copies of another graph : how many copies of can an -vertex graph contain if it has no copy of ? Its systematic study was started by Alon and Shikhelman (arXiv:1506.03807, 2016). Gerbner, Győri, Methuku and Vizer (arXiv:1712.07079, J. Combin. Theory Ser. B, 2020) treat the case where both and the forbidden graph are cycles. This mission formalizes their Theorem 11, the case , , which is the one case of the paper where the asymptotics, including the leading constant, are determined exactly for every .
Timeline:
All graphs are finite and simple. For graphs and , is the number of copies of in : the number of subgraphs of isomorphic to (unlabelled copies). is the cycle on vertices. A graph is -free if it has no subgraph isomorphic to (not necessarily induced). The generalized Turán number is
In Lean, vertices are Fin n, is Mathlib's cycleGraph a, is G.copyCount H, the -free condition is CycleFree {2 * k} G, and is exCyc n H A.
The proof works with the following objects, all defined in the mission's definitions file. The codegree of two vertices is their number of common neighbours. A pair of distinct vertices is fat if it has at least common neighbours. A copy of with vertices in cyclic order has the two opposite pairs and ; it is a fat if both opposite pairs are fat. A greedy run processes the fat 's in an arbitrary order and picks from each one of its four edges that has been picked the fewest times so far; the multiplicity of an edge is the number of times it is picked. is the complete bipartite graph with classes of sizes and (bipGraph n a).
For every ,
The is a sequence depending only on . At the statement says .
The result. Theorem 11 gives the exact leading constant for the maximum number of four-cycles in a graph without a -cycle. The extremal number of edges of such a graph is only known up to a constant factor, and only for is even its order known; counting four-cycles instead of edges turns the problem into one with a clean answer, attained by the unbalanced complete bipartite graph . The same upper bound on four-cycles is used again in the paper's Theorem 10, on the number of 's in -free graphs.
Formalizing it. The theorem is proved in the paper; it has not been formalized. A complete development needs counting of four-cycles through codegrees, the greedy multiplicity bookkeeping of §4.1, an argument producing long cycles in graphs with many fat four-cycles, and the Bondy–Simonovits theorem, which is itself not in Mathlib. The milestones isolate each of these; Theorem 1 is a stand-alone classical theorem of independent value.
The non-fat four-cycles give the main term directly. The difficulty is that fat four-cycles can a priori be numerous: a dense bipartite graph has of them. One must show that -freeness forces them down to , which is . The argument that bounds the non-fat ones does not transfer: a fat pair can lie in arbitrarily many four-cycles as an opposite pair, and nothing a priori bounds the number of fat pairs by less than . The bound must instead come from the global absence of , which is a statement about long cycles, while the objects being counted are short ones; Claim 2 is where the two meet, and its bookkeeping (new vertices must avoid the current cycle, and the four-cycles that fail to extend it must be outnumbered) is the core of the proof. The upper bound then still rests on the Bondy–Simonovits theorem, whose proof is a substantial argument of its own.
Graphs are SimpleGraph (Fin n) (or a general finite vertex type for the per-graph milestones). Copies are unlabelled (copyCount); a labelled count would be 8 times larger for . is an sSup over naturals; with forbidden lengths at least 3 the set is nonempty and finite, so it is a true maximum, which a sorry-free sanity file in the workspace checks. Landau notation is in with fixed first: is a real sequence chosen before and the graph, with the equality holding for all large , and the of Theorem 1 is an explicit constant chosen before and the graph. The constant is computed in .
Statements that are trivially true are ruled out: the goal states both the upper and the lower bound as an equality, the maximum is not a junk sSup, copies are unlabelled, constants and functions are fixed before the graph, and the forbidden family is exactly .
Two hypotheses differ from the page, both in Claim 2. The paper's standing graph is -free, which would make Claim 2 vacuous (its conclusion at is a ); the milestone assumes instead the property its proof uses, that any vertices have at most common neighbours. It also assumes that the edge is picked at least once, which follows from the multiplicity bound when and is needed for the base case at . The fat-four-cycle milestone states the explicit bound that the proof establishes, rather than the obtained after Theorem 1.
Contributions welcome: proofs of any milestone; a formal proof of the Bondy–Simonovits theorem, reusable well beyond this mission; general lemmas on counting four-cycles via codegrees and on copies in complete bipartite graphs.
In interactive decision making, an algorithm chooses actions while learning which model governs its observations. A low-regret guarantee for one algorithm does not by itself say whether every algorithm could do better. The Decision-Estimation Coefficient (DEC) was introduced to express the cost of choosing useful decisions while distinguishing plausible models. Foster, Kakade, Qian and Rakhlin's Theorem 3.2 gives the corresponding lower bound: when a localized model class has large DEC, an adaptive algorithm must incur expected regret under at least one model in the class. This mission formalizes that result for finite decision and outcome alphabets.
The paper's protocol covers bandits, partial monitoring, and reinforcement-learning examples through a common model that maps each decision to a distribution over rewards and observations. Its lower bound concerns the protocol itself, rather than any one algorithm or application. The theorem therefore gives a common test for the limits of learning in several interactive settings. The finite-alphabet representation here retains adaptive decision kernels, which are central to the theorem.
Let be the set of decisions, the set of joint reward–observation outcomes, and the reward map. A model assigns a probability distribution on to each . Its mean reward is , and is a maximizing decision. The gap function is .
At round , an adaptive algorithm assigns a distribution on decisions using the full preceding history. It samples a decision from that distribution and receives an outcome drawn from . The joint law of the length- history is . Following equation (1) of the paper, regret sums the gaps averaged under the algorithm's chosen distribution at each round. Thus its expectation is over the history law, while the inner gap is averaged under . This formulation retains the algorithm's dependence on earlier outcomes.
For probability distributions on , write for squared Hellinger distance. For a reference model and , the DEC of a class is
The uniformly localized class contains those for which for every decision. The density-ratio bound is the supremum of event likelihood ratios over both models, decisions and events, with a lower cutoff of . It may be infinite. These conventions are equations (2), (5), and (12), and the definition immediately before Theorem 3.1 in the source.
Suppose is nonempty, every model is a probability kernel, and for every and . For , set and . The goal is the following supremum form of Theorem 3.2, equation (13):
The paper writes the result with a maximum over and a supremum over , and says that one model attains the resulting bound. Its proof explicitly permits a limit sequence when the inner supremum is not attained. The displayed statement records exactly the resulting bound on the supremum of expected regret. It implies an arbitrarily close model-specific bound for each fixed and .
The milestones follow the statements the paper's proof (App. C.1.3, pp. 90–91) uses, in attack order: the multiplicative Hellinger comparison of Lemma A.11; the difference comparison of Lemma A.12; the Hellinger bound on adaptive history laws, with ; the DEC comparison at the reference model's average play , (129); the localized gap comparison (132); and the final inequality for . Their source wording and page citations are preserved in the milestone list.
The theorem supplies a quantitative obstruction to uniformly small expected regret. It uses the same coefficient that appears in the paper's upper-bound framework, so a model class with matching upper and lower DEC estimates can have its regret scale characterized through one object. In particular, the coefficient is sensitive to the model neighborhood relevant at horizon ; replacing it by a global coefficient would lose the theorem's stated localization. The paper applies this framework to bandit and reinforcement-learning classes.
The goal and milestone declarations here are open Lean statements with checked syntax and types. A complete formalization would supply proofs of the Hellinger comparisons, the history-law inequality, and the lower bound itself. The history and density-ratio definitions are reusable for other adaptive finite-alphabet lower bounds; the published FoundationsRL mean reward, Hellinger distance and DEC definitions are reused directly.
A fixed sequence of decision distributions does not describe the theorem's algorithms: later decisions depend on outcomes produced by the unknown model. The comparison must therefore use two different laws on entire histories generated by the same adaptive kernels under two models. A bound on a single round's divergence cannot simply be multiplied by without accounting for the dependence of future decision distributions on past observations. The DEC itself involves a minimum over decision distributions and a supremum over models, which need not be attained.
The Lean representation uses finite and ; probability laws and expectations are finite vectors and sums. This is a finite-alphabet specialization of the paper's measurable-space setting. Histories are functions from round indices to decision–outcome pairs. The algorithm is a family of kernels from every possible past history to a decision distribution. Its law is the product of its decision probabilities and the model's outcome probabilities. Rounds are indexed from zero in Lean, corresponding to the paper's rounds .
Every model in and every algorithm kernel is normalized and nonnegative. The mean reward range , nonempty model class, maximizing selector, and positive horizon are explicit hypotheses. They keep the real-valued supremum and infimum in the published DEC from taking Lean's default values on empty or unbounded sets. An event with positive numerator and zero denominator has infinite likelihood ratio; remains allowed because the theorem uses . Its logarithm therefore has a finite, positive argument for . The goal uses the exact constants and . The proof's constant is printed on p. 90 as ; the formalization uses , the hypothesis of Lemma A.13 (98) from which is derived. Without it the history bound fails for two nearly equal models, and with it still holds, so the goal is unaffected. The intermediate results that select a model approaching a supremum carry an arbitrary slack , the paper's "limit sequence".
Contributions should preserve the adaptive history law and equation (1)'s decision-distribution regret. A statement restricted to predetermined decisions would leave out the central quantifier of Theorem 3.2. The published FoundationsRL definitions of , and provide the shared finite model interface; the new history and density-ratio layer can support further lower bounds in this series.
In online selection, items reveal information one at a time, and each decision to accept an item is irrevocable. A matroid constraint permits some subsets and excludes others; it covers choices such as selecting linearly independent vectors or acyclic edges. A fractional solution can assign an acceptance probability to each item, but independent activations can produce a set that violates the constraint. An online contention resolution scheme (OCRS) turns these activations into a feasible selection while respecting the order in which items arrive. The matroid result of Feldman, Svensson and Zenklusen gives a guarantee that survives even when an adversary knows all random outcomes before choosing the arrival order.
This mission concerns the paper's matroid theorem, Theorem 2.1. The same paper develops schemes for matching and knapsack constraints and a rule for combining schemes for intersecting constraints. Those results are separate missions in this series. Here the central question is how much of a fractional matroid point can be retained by a deterministic greedy rule as each active item is revealed.
Let be a finite ground set and let be a matroid on . Its independent subsets form a down-closed family : if is independent, every subset of is independent. The rank of is the maximum size of an independent subset of . The matroid independence polytope is
Its points have . For a point , the active set contains each independently with probability . A deterministic greedy OCRS assigns a down-closed family to and accepts an active element when adding it to the already accepted set stays in . The empty set belongs to every . The rule depends on before the active set and arrival order are revealed.
An element is selectable for an active set if for every with . A greedy OCRS is -selectable if this event has probability at least for every and every . The event implies that can be added regardless of which eligible active elements arrived first. These definitions are from §1.1 of the paper.
For every and every finite loopless matroid , the target is a deterministic greedy OCRS with
The loopless condition is a disclosed correction to the printed Theorem 2.1: a loop cannot belong to any independent singleton, so its selectability is zero. The printed bound would demand positive selectability for that loop whenever . The theorem keeps the paper's constant exactly.
The milestones reproduce six statements from §2.1–2.1.1, in attack order: validity of a family defined by a chain of matroid minors (independence of the union of layer-wise independent sets is Soto, Theorem 5.1); a characterization of selectability through span in one layer; monotonicity of the first chain set as coordinates of increase; the description of the base polytope as the set of maximal vectors of ; the weighted span bound of Lemma 2.4,
strict when ; and the proper-inclusion conclusion of Corollary 2.5. They expose the distinct matroid and probability claims on which the main theorem rests.
The theorem gives a fixed greedy family for each fractional point, with a per-element probability guarantee that is independent of the arrival order. Offline contention resolution schemes for matroids were introduced by Chekuri, Vondrák and Zenklusen; the online, almighty-adversary version here is stronger. A solver can use that guarantee as the matroid component in larger online selection problems. In the source paper it feeds the intersection and application results; those applications require further models and statements beyond this mission. The factor makes the tradeoff explicit: using a more heavily scaled fractional point raises the risk of contention.
The result is proved in the cited paper. This mission asks for a machine-checked Lean proof of its corrected statement and the source's supporting claims. A successful development would add reusable finite representations of independent activation, matroid polytope inequalities, span probabilities, and chain families. It would also make the loop boundary explicit, preventing a formally false version of the printed theorem from being published as a target.
Independent activation does not itself respect matroid independence. A greedy family that simply contains every independent set can make an element unavailable after earlier active elements are accepted, and the arrival order can expose the worst such history. The central issue is therefore a uniform selectability event: the same element must remain addable after every feasible subset of the active set. The paper measures that obstruction through spans in successive matroid minors. The first chain set must be proper so that the construction can continue, which is why the strict part of the weighted span inequality matters.
The ground set is a finite Lean type, subsets are Finsets, and Mathlib's Matroid supplies independence, closure, contraction and restriction. Matroid rank is converted from Mathlib's extended natural rank to a real number; finiteness makes this conversion finite on every subset. The independence and base polytopes are defined by the paper's inequalities. The scalar multiple is pointwise set scalar multiplication, including .
Probabilities are finite sums of product weights over all active sets. In particular, the event in Lemma 2.4 uses , whereas the recurrence defining uses . These are separate definitions. Every point used for activation lies in , as enforced by the polytope and . The base-polytope condition on Corollary 2.5 is the standing assumption stated before the lemma in the source.
The loopless condition applies to the goal, to Corollary 2.5, and to the strict clause of Lemma 2.4 only; its non-strict clause, the chain statements and the monotonicity statement hold for every matroid and are stated without it. Three trivializing formalizations are ruled out: every greedy family must contain the empty set, so an empty family cannot satisfy selectability vacuously; every member of a greedy family must be independent in , so is not admissible; and every point used for activation lies in , so is a genuine probability. The quantified scheme depends only on , and its success condition ranges over every feasible subset of the realized active set. Contributions that establish the chain family's independence, finite probability identities, and rank or closure facts are within scope. Polynomial-time implementation and the Monte Carlo estimates of Lemma 2.6 are outside this mission's mathematical target.