Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A Faster Cutting Plane Method and its Implications for Combinatorial and Convex Optimization (Lee, Sidford, Wong) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the main convex-optimization guarantee of the Lee–Sidford–Wong cutting plane method (Theorem 42), the result cited as Theorem 5.23 in Nannicini's lecture notes.
For let . For a set , . Given a convex , a convex set and , an -separation oracle on for is a map that, on every input , either asserts , or outputs a half space with , and .
There are universal constants such that the following holds. Let , , and , and put
There is a randomized algorithm , depending only on , that queries an oracle at points of and returns a point , with the following property. For every , every convex , every convex set with containing a global minimizer of , and every -separation oracle on for :
The oracle only needs to satisfy its specification at points of . The result turns a cutting plane method into an optimization method whose number of oracle calls is linear in the dimension up to a logarithm, and many of the paper's applications rest on it.
Formalization Note A randomized algorithm is a probability mass function over deterministic adaptive query strategies (decision trees with real-vector queries). The paper prints in . Its proof gives , and is possible, which would make the printed non-positive, so is used in both places. Only the oracle part of the running time is formalized. The additional arithmetic time is omitted because the paper fixes no machine model for real arithmetic.
This is the main convex-optimization guarantee of the Lee–Sidford–Wong cutting plane method (Theorem 42), the result cited as Theorem 5.23 in Nannicini's lecture notes.
For let . For a set , . Given a convex , a convex set and , an -separation oracle on for is a map that, on every input , either asserts , or outputs a half space with , and .
There are universal constants such that the following holds. Let , , and , and put
There is a randomized algorithm , depending only on , that queries an oracle at points of and returns a point , with the following property. For every , every convex , every convex set with containing a global minimizer of , and every -separation oracle on for :
The oracle only needs to satisfy its specification at points of . The result turns a cutting plane method into an optimization method whose number of oracle calls is linear in the dimension up to a logarithm, and many of the paper's applications rest on it.
Formalization Note A randomized algorithm is a probability mass function over deterministic adaptive query strategies (decision trees with real-vector queries). The paper prints in . Its proof gives , and is possible, which would make the printed non-positive, so is used in both places. Only the oracle part of the running time is formalized. The additional arithmetic time is omitted because the paper fixes no machine model for real arithmetic.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Upper bounds on quantum query complexity inspired by the Elitzur-Vaidman bomb tester (Lin, Lin) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the quantum algorithm for finding the first marked element of an ordered list (Lin–Lin, Theorem 10).
A list of elements is given as a black box , where means that element is marked; it is accessed through the standard query oracle . An algorithm consists of rounds; each round applies to a fixed start state with unitaries independent of , measures in the computational basis, and chooses the next round (or halts with an answer) from the outcome. For an input let be the position of the first marked element, or if none is marked.
There is an absolute constant such that for every there is an algorithm , fixed before the input, such that for every :
The point is that the cost adapts to the position of the first marked element rather than to the length of the list; this is the search subroutine used to simulate classical query algorithms whose query results can be guessed.
Formalization Note Algorithms are finite trees of query rounds with measurements in between. Positions are 0-indexed, so the -th element is index and the bound reads . The error constant is the one achieved by the paper's proof (Appendix C). The source's time bounds are not formalized, because the paper fixes no model of time; only the query bounds are stated.
This is the quantum algorithm for finding the first marked element of an ordered list (Lin–Lin, Theorem 10).
A list of elements is given as a black box , where means that element is marked; it is accessed through the standard query oracle . An algorithm consists of rounds; each round applies to a fixed start state with unitaries independent of , measures in the computational basis, and chooses the next round (or halts with an answer) from the outcome. For an input let be the position of the first marked element, or if none is marked.
There is an absolute constant such that for every there is an algorithm , fixed before the input, such that for every :
The point is that the cost adapts to the position of the first marked element rather than to the length of the list; this is the search subroutine used to simulate classical query algorithms whose query results can be guessed.
Formalization Note Algorithms are finite trees of query rounds with measurements in between. Positions are 0-indexed, so the -th element is index and the bound reads . The error constant is the one achieved by the paper's proof (Appendix C). The source's time bounds are not formalized, because the paper fixes no model of time; only the query bounds are stated.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
A Quantum Approximate Optimization Algorithm (Farhi, Goldstone, Gutmann) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the headline MaxCut guarantee of the Quantum Approximate Optimization Algorithm (QAOA) at depth .
Let be a connected -regular simple graph on vertices. For a bit string let be the number of edges with ; as an operator, is diagonal in the computational basis. Let , let be the uniform superposition, and for angles let
the expected cut value of the string obtained by measuring in the computational basis. Then there exist angles and such that
Equivalently, is at least times the size of the maximum cut. The constant is the numerically computed (rounded-down) worst-case ratio, attained in the limit of graphs without triangles; the source's derivation is partly numerical.
Formalization Note The graph is a SimpleGraph (Fin n) with Connected and IsRegularOfDegree 3. The approximation ratio is measured, as in the source's argument (34), through the expectation at the best angles; the source's informal remark that order repetitions find a string with cut value near is not part of the statement.
This is the headline MaxCut guarantee of the Quantum Approximate Optimization Algorithm (QAOA) at depth .
Let be a connected -regular simple graph on vertices. For a bit string let be the number of edges with ; as an operator, is diagonal in the computational basis. Let , let be the uniform superposition, and for angles let
the expected cut value of the string obtained by measuring in the computational basis. Then there exist angles and such that
Equivalently, is at least times the size of the maximum cut. The constant is the numerically computed (rounded-down) worst-case ratio, attained in the limit of graphs without triangles; the source's derivation is partly numerical.
Formalization Note The graph is a SimpleGraph (Fin n) with Connected and IsRegularOfDegree 3. The approximation ratio is measured, as in the source's argument (34), through the expectation at the best angles; the source's informal remark that order repetitions find a string with cut value near is not part of the statement.
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
A Quantum Approximate Optimization Algorithm Applied to a Bounded Occurrence Constraint Problem (Farhi, Goldstone, Gutmann) establishes the selected mathematical guarantees below. The mission turns those original paper results into precise Lean proof targets.
This is the main result of Farhi, Goldstone and Gutmann on the level-one Quantum Approximate Optimization Algorithm (QAOA) for bounded-occurrence Max E3LIN2.
An instance of Max E3LIN2 on bits is a set of linear equations over , each of the form with three distinct variables and right-hand side , at most one equation per triple . Let be the number of equations satisfied by , viewed as the diagonal operator ; let and . For real put
so that is the expected number of equations satisfied by the string obtained by measuring in the computational basis.
Theorem. There is such that for every integer , every , and every such instance in which each bit occurs in at most equations, there exists with such that
A uniformly random string satisfies equations on average; the theorem shows that one round of QAOA beats random guessing by a term of order , uniformly over all bounded-occurrence instances, and in particular that every such instance has an assignment satisfying that many equations.
Formalization Note The source's qualifier "for large " is rendered as an existential threshold quantified before , and the instance. The objective is the unshifted count of satisfied equations; the paper's shifted operator (6) differs by the constant , which only contributes a global phase to .
This is the main result of Farhi, Goldstone and Gutmann on the level-one Quantum Approximate Optimization Algorithm (QAOA) for bounded-occurrence Max E3LIN2.
An instance of Max E3LIN2 on bits is a set of linear equations over , each of the form with three distinct variables and right-hand side , at most one equation per triple . Let be the number of equations satisfied by , viewed as the diagonal operator ; let and . For real put
so that is the expected number of equations satisfied by the string obtained by measuring in the computational basis.
Theorem. There is such that for every integer , every , and every such instance in which each bit occurs in at most equations, there exists with such that
A uniformly random string satisfies equations on average; the theorem shows that one round of QAOA beats random guessing by a term of order , uniformly over all bounded-occurrence instances, and in particular that every such instance has an assignment satisfying that many equations.
Formalization Note The source's qualifier "for large " is rendered as an existential threshold quantified before , and the instance. The objective is the unshifted count of satisfied equations; the paper's shifted operator (6) differs by the constant , which only contributes a global phase to .
These are known results from the cited paper. The current contribution consists of source-reviewed, compiler-checked theorem statements and mathematical definitions. Formal proofs remain open. Only the listed selected results are in scope; no whole-paper completeness is claimed.
A complete solution must establish every quantified conclusion under the exact stated hypotheses, including error, probability and resource conditions wherever present. The source assumptions and conventions are recorded in the attached statements and independent readbacks.
Definitions preserve the existing reviewed Lean interfaces. Every target proof is currently sorry, so each target is Open. Printed-source corrections, where necessary, are labeled with the printed claim, the change and its reason.
Quantum signal processing transforms the eigenphases of a unitary operator by a sequence of controlled operations and single qubit rotations. To know which transformations such a sequence can realize, one must characterize the matrix functions produced by the sequence. Haah's product decomposition theorem gives such a characterization without the restriction on the projectors used in some earlier quantum signal processing constructions. The result concerns exact functions; the numerical synthesis algorithm and its precision analysis are separate parts of the paper.
Let be a nonzero complex number. A rank one orthogonal projector on is a Hermitian matrix with and trace one. Its complementary projector is . The associated primitive matrix is
For , this matrix is unitary with determinant one. Given such projectors, indexed in their multiplication order, and a constant matrix , the product of interest is
The leftmost primitive factor is , and the product has exactly primitive factors. At the product of primitive factors is the identity and is the constant matrix . Although the physical interpretation uses points on the unit circle, the formula defines at every nonzero complex . These conventions follow §2, equations (2) and (3).
A matrix Laurent polynomial of width is written
where each is a complex matrix and all coefficients outside vanish. The set consists of these polynomials for which whenever . A member has degree when or . The subset consists of members whose nonzero exponents have the parity of , so for every odd integer . The notation conjugate transposes each coefficient while leaving its exponent unchanged: . These are the conventions of Definition 1 and equations (4) and (5).
The goal is all of Theorem 2. First, every product of primitive matrices belongs to . Conversely, every of degree has a unique ordered tuple satisfying the product formula, with and each a rank one orthogonal projector. For , the final projector is determined by the leading coefficient:
The formula includes the assertion that its denominator is nonzero under the theorem's hypotheses; that is a consequence to establish, rather than an extra assumption. The case retains the product characterization and uniqueness, while having no final projector. The milestones state the source's primitive matrix observation, polynomial identities, leading coefficient conditions, degree reduction, and the relation between the two extreme coefficients.
The theorem identifies the Laurent polynomials that admit the specified quantum signal processing product and says that the factors are uniquely recoverable from the matrix function when the number of factors is fixed. This supports the exact synthesis question motivating the paper: whether a desired valued function on the unit circle is achievable by the primitive operations. The formula for also identifies the last factor directly from a coefficient of the target function. Haah's §4 algorithm uses the decomposition, but its numerical guarantees are outside this mission.
The paper proves Theorem 2. The formalization target is a machine checked version of that known theorem and its source stated intermediate claims. The definitions of matrix Laurent polynomial evaluation, parity restricted coefficient families, and primitive projector factors can also support later work on polynomial matrix functions. The mission does not claim that these statements have already been proved in Lean.
Membership in is given only on the unit circle, while coefficient identities needed for the decomposition concern Laurent polynomials throughout . A pointwise unitary identity on the circle must therefore be promoted to an identity of Laurent polynomials before its extreme coefficients can be compared. The main structural difficulty is that a matrix product may lose its highest and lowest powers even when its factors are nonzero. Identifying a projector that lowers the degree must control both extremes at once and preserve the parity and conditions. Uniqueness also depends on fixing exactly factors: extra complementary factors can cancel.
Lean represents a Laurent polynomial by a coefficient family with explicit width support, and evaluates it by a finite sum of integer powers. Equalities of Laurent polynomials are stated for every nonzero complex . The positive integer is represented as a natural number, with integer casts for exponents. The special unitary group is Mathlib's ; the paper's rank one orthogonal projectors are represented by Hermitian idempotence together with trace one. This trace condition is equivalent to rank one for these projectors. An ordered function on supplies precisely factors. The last factor has index in Lean.
The set retains both the width and conditions of and adds the parity condition. It is defined from coefficients, not from the existence of a product decomposition. Allowing rank zero or rank two projectors, dropping unitarity, or allowing a variable factor count would change the theorem. The source's remark that any orthogonal projector yields a member of is read with the rank one condition of equation (2): the literal unrestricted remark fails for and . The singular leading coefficient milestones require , and the last projector formula has the same domain.
The development needs facts about determinants, conjugate transpose, projectors, finite matrix products, and uniqueness of finite Laurent expansions. The Laurent polynomial infrastructure and rank one matrix facts are reusable beyond this theorem. Contributions proving the source stated milestones, their faithful supporting algebraic lemmas, and the main product characterization are in scope. The parity refinement of §3.1, Lemma 4, and the §4 synthesis algorithm with its running time claim are outside this mission.
Clustering points drawn from a mixture of well-separated distributions is a basic problem of unsupervised learning. Practical data sets also contain outliers, points that belong to no cluster and may be placed anywhere. Srivastava, Sarkar and Hanasusanto (arXiv:1912.07546v3; Operations Research 71(1), 2023) propose a robust spectral clustering algorithm. It thresholds a Gaussian kernel matrix through a linear program, then applies spectral clustering to the result, and they prove that its error decays exponentially in the squared signal-to-noise ratio when the outliers, placed arbitrarily, are a small fraction of the points. The authors report that their bound is tighter than those obtained for related semidefinite relaxations, for example by Mixon, Villar and Ward (arXiv:1602.06612), which use a reference matrix in a similar way (pp. 10–11). This mission formalizes the first of the paper's two main results: the estimation error of the thresholded kernel matrix.
There are points in : inliers and outliers. Each inlier has a label , and the clusters are with sizes and . The inlier observation is
where are the cluster centres and the noise vectors are independent, identically distributed within each cluster, and sub-gaussian with parameter : for every , (Definition 3). The outliers are arbitrary random vectors, with no independence or distributional assumption. Write , and .
The algorithm forms the Gaussian kernel over all points and solves the Robust-LP
where and is the all-ones matrix. Its solution has the closed form if and otherwise. The true clustering matrix has exactly when and are inliers with the same label. The error is measured in the entrywise norm , and denotes the inlier block.
Fix and , and set , , and . There are constants , depending only on and , such that if , and , then with probability at least ,
and
The constants are left existential, as on the page.
The milestones follow the structure of the paper's proof:
Theorem 1 is the quantitative core of the paper. It says that thresholding a Gaussian kernel at a level between two explicit values recovers the cluster structure among the inliers up to an error that is exponentially small in , plus a sampling term of order , whatever the outliers do. The paper's Theorem 2 feeds this bound into Davis–Kahan perturbation theory to bound the fraction of misclassified points after spectral rounding, and Proposition 2 uses it to identify the outliers.
Formalizing it produces more than the theorem. As printed, Theorem 1 is false: the kernel uses while the thresholds use , a factor-two mismatch that the proof silently drops. A mechanically checked statement settles the corrected thresholds. The proof also rests on three cited probabilistic results that are not proved in the paper and are not in Mathlib: the Hsu–Kakade–Zhang tail bound for quadratic forms of sub-gaussian vectors, and Bernstein inequalities for one- and two-sample U-statistics (the two-sample version is asserted "following the arguments" of earlier work, with no proof). None of these results has a machine-checked proof at present.
The deterministic part (Lemmas 1–3, (E.2), (E.18)) is elementary linear algebra on -matrices. The difficulty is probabilistic. The kernel entries are not independent: each point appears in entries. So the natural first idea, a Chernoff or Hoeffding bound on the number of threshold violations treated as a sum of independent indicators, does not apply. The paper handles the dependence by writing the counts of violations as U-statistics and invoking Bernstein-type bounds for them. Those bounds need Hoeffding's representation of a U-statistic as an average of sums of independent terms, which is not available in Mathlib. A second obstacle is the Hsu–Kakade–Zhang inequality: the norm of a sub-gaussian vector whose coordinates may be dependent concentrates at the scale , not , and the coordinate-independent Hanson–Wright inequality does not give it.
Fin n ⊕ Fin m (inliers, then outliers) and vectors live in EuclideanSpace ℝ (Fin d). The labels are fixed. The paper draws them from a multinomial distribution, but its proof conditions on them, and appears in the probability bound.HasSubgaussianMGF of every projection . The proof uses this parameter, not the "largest eigenvalue of the second moment matrix" mentioned in §2.2.A Fisher market allocates a common supply of items among buyers with separate budgets. When the items form a continuum, such as positions in a measurable interval, a buyer's valuation and the market price are functions rather than finite lists. This is a useful model for divisible resources and for settings in which an allocation can be described as a measurable subset of a continuous item space. Gao and Kroer develop equilibrium and convex-programming results for this setting in Infinite-Dimensional Fisher Markets and Tractable Fair Division. Their Section 6 extends the analysis from linear utility to quasilinear utility, where the buyer subtracts the cost of the allocated bundle from its value.
Quasilinear utility changes the role of money. A buyer can retain an unspent part of the budget and value it outside the market. Consequently, normalizing each buyer's valuation independently, which is harmless for linear demand, changes quasilinear demand. The extension therefore needs its own equilibrium definition and its own pair of optimization programs. This mission concerns the existence and exact equilibrium characterization stated in Theorem 10 of the cited preprint, rather than the numerical algorithms discussed elsewhere in that paper.
There are buyers and an item space , a compact subset of , with restricted Lebesgue measure . Buyer has an integrable, nonnegative valuation density with , and a strictly positive budget . A bundle is an essentially bounded, nonnegative measurable function on . An allocation is feasible when almost everywhere. A pure allocation assigns almost disjoint measurable sets to buyers, so almost everywhere; some items may remain unallocated.
A price density is nonnegative and integrable. The pairing gives the value of a bundle and its cost. At price , buyer chooses an affordable bundle maximizing , with affordability . A quasilinear market equilibrium (QLME) is a feasible allocation and price at which every buyer makes such a choice and unsold items have zero total price: .
The quasilinear Eisenberg–Gale primal program uses a nonnegative variable for each buyer and maximizes , where . Its dual program minimizes subject to and . The primal is represented by with at an optimum. This saturated form has the same optimum as the displayed program and makes the optimality conditions unambiguous.
The goal is the full four-part statement. The primal attains its maximum at a pure allocation. The dual attains its minimum with a unique vector and price density almost everywhere. For feasible primal and dual points, simultaneous optimality is equivalent to market clearance and
Finally, is a QLME exactly when there are and for which and are optimal in the two programs. The same given must appear on both sides of this equivalence.
The milestones follow the statements in the proof of Theorem 10: attainment of the utility-space program (A.14), uniqueness of the minimizer in the reduced dual program, weak duality (A.15) with its additive constant , the KKT characterization, and each direction of the QLME equivalence. The earlier paper's Lemma 1 identifies the feasible utility set with utilities of pure allocations and supplies the compactness used here. It belongs to the first mission of this series and is not duplicated as a target in this one.
The theorem establishes that the two infinite-dimensional programs describe the quasilinear market exactly. Attainment guarantees actual optimal allocation and price objects rather than only approximating sequences. Pure attainment gives a measurable partition-type allocation. The unique pins down each buyer's utility price, while identifies the price density almost everywhere. The KKT equations give precise tests for a candidate optimal pair, and the final equivalence translates between optimization solutions and buyer-level equilibrium behavior. These are the claims made by Theorem 10 and its appendix proof.
The result is proved in the paper; the work here is to formalize its statement and, in later solver contributions, its proof in Lean. A complete development will also provide reusable infrastructure for integrating valuation densities against essentially bounded bundles, representing continuum-item allocations, and relating a finite buyer-indexed vector to pointwise price maxima. No machine-checked proof of this mission's goal is supplied with this draft.
The optimization variables include functions in and , and the positive cone of has no useful interior for a direct appeal to standard infinite-dimensional convex-duality theorems. The finite-dimensional utility vector is easier to optimize over, but recovering a pure allocation from it requires the measurable-allocation result established earlier in the paper. The dual price is a pointwise maximum of integrable densities, and equality of prices is meaningful almost everywhere. Equilibrium demand compares a buyer's assigned bundle with every affordable essentially bounded bundle, so an optimality statement about program variables must account for that full comparison.
Lean represents densities and bundles as functions on the ambient Euclidean space, with the measure restricted to ; values outside do not matter. The standing hypotheses are compactness of , integrability and almost-everywhere nonnegativity of every , strictly positive total valuation, and strictly positive budgets. There is no assumption that total budgets or total item measure equal one. The buyer type Fin n is zero-based; the paper numbers buyers from one. The empty-buyer case is allowed and has the expected trivial finite-vector interpretation.
The equilibrium predicate includes supply feasibility. The printed QLME definition on page 29 omits it, although the linear-market definition includes it and Theorem 10(d) requires it. Without it, a buyer can receive more than unit supply on part of the item space while buyer optimality and market clearance still hold. The primal uses the saturated value ; leaving free below that value makes the printed KKT converse false. These two choices are disclosed in the item descriptions and moderation notes, with concrete counterexamples there.
The paper treats as a limiting infinite cost. Lean's real logarithm is total, so optimality compares only points whose logarithm arguments are positive. The utility KKT equation is multiplied by to avoid division by zero. Valuation and price densities are integrable, and bundles are essentially bounded, so pairings are genuine finite integrals. The pointwise maximum over buyers is an indexed supremum; feasibility and uniqueness use almost-everywhere equality for price functions and exact equality for the finite vector . These conventions prevent degenerate total-function values from deciding the theorem.
Contributions can address the measurable utility-set and pure-allocation infrastructure, finite-dimensional attainment, weak duality, the equality conditions, or the demand comparison. The intermediate milestones are stated at the strength used in the paper; the goal contains the entire four-part result.
A Fisher market divides a supply of goods among buyers with fixed budgets. In a finite market, each good is a separate coordinate. Fair division can instead involve a continuum of items, such as locations along an interval or points in a region, where a buyer's valuation varies measurably from point to point. Finite dimensional existence and duality arguments do not automatically apply: the allocation is now a function, and the feasible set need not be compact in its natural function space. Gao and Kroer formulate a market and two Eisenberg–Gale programs for this setting, then prove that their optima exist and characterize equilibrium Gao and Kroer, §3.
The result also connects market equilibrium to fair division. A pure allocation assigns measurable regions of the item space to buyers, allowing overlap only on null sets. Existence of a pure optimizer means that a market outcome can be represented by such a division, rather than by fractional shares at each item. The same paper derives Pareto optimality, budget weighted envy freeness, and proportionality for equilibrium allocations Gao and Kroer, Theorems 1 and 3.
The item space is a compact subset of with restricted Lebesgue measure . There are buyers. Buyer has a budget and a nonnegative integrable valuation density with . The utility of a bounded nonnegative bundle is . An allocation is feasible when almost everywhere. It is pure when each equals the indicator of a measurable set , up to almost everywhere equality, and these sets are pairwise disjoint up to null sets. Leftover items are allowed.
A nonnegative integrable price density defines a buyer's affordable bundles by . A market equilibrium is a feasible allocation and price at which every buyer maximizes utility among affordable bundles and . Thus unallocated supply may remain only where it has zero price. The paper's primal Eisenberg–Gale program, , maximizes weighted log utility over feasible allocations. Its dual program, , minimizes total price minus weighted log multipliers subject to almost everywhere Gao and Kroer, pp. 6–8.
The goal is the three part Theorem 1. In the notation above, it asserts attainment of the primal objective at a pure allocation, attainment of the dual objective with a unique multiplier vector and price almost everywhere, and the equivalence
The milestone list follows the results the paper uses to reach that goal. Lemma A.1 gives a convex, compact range for utility matrices and, under atomlessness, identifies mixed and partition based ranges. Lemma 1 specializes this to the market's feasible utility set , proving that is compact and convex and equals the pure utility set . Lemma 2 establishes attainment and uniqueness in the finite dimensional reduction of the dual problem. Lemma 3 gives weak duality with the paper's constant and its three optimality conditions. Theorem 2 expands the equivalence between optimality and equilibrium, including budget exhaustion and the utility formula . These are the paper's numbered results on pp. 8–10 and a1 Gao and Kroer, §3 and Appendix A.1.
The proposal also states Theorem 3, Lemma 4, and Corollaries 1–3 as companion results. They record the resulting fairness properties, normalized equilibrium bounds, winning sets, a construction of dual prices from a pure optimum, and a test for a pure equilibrium Gao and Kroer, pp. 10–11.
Theorem 1 shows that the two programs give actual allocations and prices in the continuum market, not merely limiting objective values. The pure optimizer provides measurable regions for buyers. The dual multipliers give a unique utility price for each buyer, while the price density is determined almost everywhere. Theorem 2 makes these program outputs economically interpretable: each buyer exhausts its budget at equilibrium. Theorem 3 then supplies efficiency and fairness guarantees for those allocations Gao and Kroer, Theorems 1–3.
These results are proved in the cited paper. This mission asks for machine checked Lean proofs of those mathematical statements. Its definitions of allocations, demand, equilibrium, the two programs, and feasible utilities could also support formalization of the paper's later geometric and quasilinear results. The draft declarations compile as open statements; compilation does not establish the theorems.
The feasible allocations are bounded in an infinite dimensional function space, but that does not make the set compact in the topology used for the optimization problem. The paper instead needs compactness of the finite dimensional set of achievable utility vectors. The range result in Lemma A.1 is therefore central, and its atomless conclusion must be strong enough to replace fractional allocations by measurable partitions Gao and Kroer, Lemma 1 and Appendix A.1.
Standard constraint qualification arguments also do not supply the required duality theorem here: the positive cone in has empty interior. The proposal consequently asks for the paper's specific weak duality inequality, attainment, and optimality characterization rather than assuming a general finite dimensional duality theorem applies Gao and Kroer, Remark 1.
Lean uses real valued measurable functions on the ambient Euclidean space with measure . It identifies prices and allocations up to almost everywhere equality, as the paper identifies and equivalence classes. Bundles must belong to and prices and valuations must be integrable; these conditions prevent a nonintegrable product from receiving Lean's default integral value of zero. The number of buyers may be zero, consistent with the finite index formulation, while the standing positivity hypotheses apply to every buyer present.
The real logarithm in Lean returns zero at zero. The optimization predicates instead require positive utility or positive dual multipliers and compare only with other positive points, matching the paper's objective convention. The maximization over buyers is the finite supremum . Price and allocation uniqueness is stated almost everywhere; multiplier uniqueness is exact. Lemma A.1 uses the paper's divisible measure condition for atomlessness and fixes its unnamed almost everywhere partition convention by requiring everywhere. Corollary 3 explicitly requires each denominator to be positive. Lemma 4 alone assumes the normalizations and , which the paper recalls before its statement.
The goal remains the full three part theorem. It does not assume the range theorem, duality equality, or optimality conditions it is meant to establish. Contributions to the measure range theorem, utility set compactness, the dual reduction, and the equilibrium characterization are all within scope.
Simulating the time evolution of a quantum system is a standard task in quantum algorithms: given a Hamiltonian, the algorithm must reproduce the phase acquired by each of its energy eigenstates. The cost is often measured by how many times the algorithm queries an operator describing that system. Low and Chuang's 2016 preprint connects this task to quantum signal processing, a method that programs a sequence of rotations of one ancillary qubit. Its Theorem 2 gives the quantitative link: a finite Fourier approximation of a desired phase function determines a phase sequence whose induced eigenvalue transformation has error at most and success probability at least .
The paper uses this link in a later Hamiltonian-simulation result with an optimal asymptotic query count (Theorem 3, p. 4). The present mission targets the finite, explicitly quantified signal-processing theorem that makes that application possible. The criterion for which response functions can be produced by the rotation sequence was established in earlier work by Low, Yoder and Chuang and is quoted as Theorem 1 in this paper.
An ancilla qubit has basis states and . Let be its Pauli matrices. For real angles and , a signal rotation is
The signal fixes the rotation angle; chooses its axis in the qubit's plane. A list of phases gives the response sequence , with acting first. Its four real Pauli coefficients are defined by
The ancilla state selects the scalar response . The realizability theorem characterizes these pairs when is positive and even: is a cosine series with frequencies through , is a sine series with frequencies through , , and for every (Theorem 1, p. 3).
For a finite-dimensional unitary , choose an orthonormal eigenbasis and real eigenphases , so . The signal operator applies to the ancilla in each eigenspace: . The ordered product therefore uses one common phase list on all eigenspaces. After preparing and projecting the ancilla on , the effective system operator is its block . The desired operator for a real phase function is (Eqs. (2)–(6), pp. 2–3).
Let be -periodic, valued in , and odd on the interior , and let be respectively a cosine and a sine series of degree at most for positive even . If at every real angle, the goal is one phase list for which, uniformly over angles and input unitaries,
The milestones state the exact realizability criterion, the paper's displayed scalar bounds, and the eigenspace identity that carries those bounds to the operator statement. The constants and are fixed because the mission formalizes Theorem 2 and Eqs. (7)–(11), pp. 3–4, rather than an unspecified approximation rate.
The theorem makes a Fourier approximation into a phase transformation of every eigenstate of an arbitrary finite-dimensional input unitary. Its quantified success guarantee means that projecting the ancilla succeeds with probability close to one when the approximation error is small. In the paper, the particular target connects this mechanism to sparse Hamiltonian simulation (Eq. (14), p. 4).
The result is proved in the cited paper; this mission asks for machine-checked proofs of its statements in the specified matrix model. The quoted characterization of achievable responses is also a proof target. A complete development would add reusable facts about products of qubit rotations, constrained trigonometric series, sum-of-squares completion, and block-diagonal operators. No machine-checked proof of this exact theorem was found in the local Prove2Me index at drafting time.
An arbitrary Fourier approximation is not automatically the response of a unitary rotation sequence. It may violate the squared-magnitude bound or the required value at zero, even though it is uniformly close to the target function. Those restrictions are exactly what the realizability theorem requires. The difficult part is the converse direction of that characterization: the paper quotes it from earlier work, while the present statement asks for all admissible pairs and all positive even sequence lengths. The completion of a nonnegative trigonometric polynomial into the remaining Pauli components is another substantial mathematical target; the needed factorization is not already packaged as the paper uses it in this Mathlib environment.
The qubit is a complex matrix indexed by . Rotations use the matrix exponential and the factor exactly as printed. The signal product has exactly factors in the paper's order. Cosine and sine series use the inclusive frequencies stated in Theorem 1. The operator model takes a finite unitary eigenbasis as data, with the ancilla as the first factor of the tensor product. The success inequality is pointwise in ; the error inequality is homogeneous in every system vector and represents the paper's maximum over unit vectors. The phases are chosen before the input unitary, so they cannot depend on its eigenspaces.
The paper writes ; the Lean target extends its domain periodically to and retains that codomain range. Oddness is imposed on the interval's interior, where both and belong to the printed domain. The phrase “real Fourier series in ” is represented by the cosine form for and sine form for that its proof applies directly. “Efficiently compute” is represented by existence of phases; no runtime claim is made. The source calls the operator-vector error a trace distance; the formalization uses precisely its displayed vector norm, rather than a distance between density matrices.
Some intermediate squared inequalities need or ; those conditions appear only on the corresponding milestone clauses. The goal has no separate bound on : its approximation hypothesis already forces . A valid formalization must use the concrete matrix product and matrix-entry Pauli components; defining response functions merely to satisfy the target would empty the theorem of its claim. Contributions that establish the realizability criterion, trigonometric completion, the explicit inequalities, and the operator lift are all in scope. The controlled- circuit of Fig. 1 and the asymptotic oracle-complexity claim of Theorem 3 are outside this mission.
Policy evaluation asks for the value of a fixed decision rule in a Markov decision process whose transition probabilities are unknown. It is the inner loop of policy iteration, the subroutine behind actor-critic methods, and the question an operator faces before deploying a policy in an inventory, queueing or routing system that can only be simulated. The simplest estimator is the plug-in (model-based) one: sample transitions from a simulator, build the empirical transition kernel, and compute the value of the policy in the resulting empirical MDP.
How many samples this estimator needs has a short history. Azar, Munos and Kappen (Machine Learning, 2013) introduced the total-variance argument that yields the dependence for planning with a generative model. Agarwal, Kakade and Yang (COLT 2020) proved minimax-optimal guarantees for model-based planning, but only when the sample size per state-action pair exceeds roughly . Pananjady and Wainwright (IEEE Trans. Inf. Theory, 2021) gave instance-dependent policy-evaluation bounds and a minimax lower bound, again under a sample-size requirement of order . Li, Wei, Chi and Chen (arXiv:2005.12900v8; Operations Research, 2024) removed this barrier: their Theorem 3 shows that the plug-in estimate is accurate across the whole accuracy range once the sample size exceeds up to logarithmic factors. This mission formalizes that theorem and the lemmas its proof rests on.
A discounted Markov decision process consists of a finite state set , a finite action set , a transition kernel (for each pair , is a probability vector over ), a reward and a discount factor . A deterministic policy is a map . Its value function is
Write for the state transition matrix of and for its reward vector, so that . For a vector , is the one-step variance of under the chain.
The generative model returns, for every pair , independent next states . The empirical kernel is , and for a policy chosen independently of the data the plug-in estimate is the value function of in the empirical MDP , that is, . Norms are maxima of absolute entries; and is natural.
There is a universal constant such that for every MDP as above, every fixed policy , every and every ,
The constant is not specified, so the goal survives any later improvement of the constants.
In attack order: Lemma 10 (elementary facts on , p. 23); the matrix form (27) of (p. 12); Lemma 11, for with (p. 24); the total-variance bound (70) of Azar et al. (p. 24); the deterministic instance-dependent bound (80) under a Bernstein-type condition (pp. 25–26); Lemma 2, the worst-case bound under the same condition (p. 15); the high-probability Bernstein bound (82) for a fixed policy (p. 27); and Lemma 1, the explicit-constant version of the goal with an instance-dependent refinement (p. 13):
with and .
The theorem says that the plug-in estimate of a fixed policy's value beats a random guess as soon as exceeds up to logarithmic factors, and that its sample size matches the minimax lower bound of Pananjady and Wainwright (2019, Theorem 2(b)) up to a factor over the full range . Lemma 2, which does not require the policy to be independent of the data, is the step the paper reuses to analyze the data-dependent optimal policy of the empirical MDP (Theorems 1 and 2, posed in sibling missions of this series).
The result is proved in the paper; none of it is formalized. The mission produces a machine-checked account of the variance-aware analysis of tabular MDPs: the resolvent calculus of Lemma 10, the total-variance bounds (70) and Lemma 11, which recur across the reinforcement-learning sample-complexity literature, and a high-order expansion argument that turns a Bernstein-type condition into an error bound. A formal proof of (70), which the paper quotes without proof, would itself be a reusable result.
The obvious argument writes and bounds the two factors separately. The resolvent of the empirical chain is correlated with the deviation , and bounding crudely by its row sums loses a factor that forces ; this is exactly the barrier in earlier work. Removing it requires controlling a whole sequence of auxiliary vectors , each defined through the variance of the previous one, up to a logarithmic depth, and showing that their norms do not blow up (Lemma 11). The Bernstein step must also use the variance, not the range, of ; a Hoeffding bound gives the wrong power of .
States and actions are finite types; the kernel is P : S → A → S → ℝ with P s a s' , a probability vector for each (s, a) (the published IsTransitionKernel). The standing setting is the predicate IsDiscountedMDP P r γ: a kernel, , , and nonempty state and action sets (, , p. 5). Policies are deterministic maps S → A; the value function is the published series PolicyValue of the induced point-mass policy. Vector norms are Mathlib's sup norm on finite function types, matching ; vector inequalities and square roots are entrywise.
The data set is the finite type of arrays of next states per pair, its law is the product of the kernel probabilities, and of an event is a finite sum. "With probability at least , " is stated as . The goal assumes , the standing assumption of the empirical kernel (3), which is implied by the sample-size condition since is nonempty. Index ranges "" range over the integers in that interval. The deterministic milestones (80) and Lemma 2 are stated for an arbitrary transition kernel , which is what their proofs use.
Three formalizations would trivialize the goal and are ruled out: computing from the true kernel instead of the empirical one; letting be chosen after the data are seen; and letting depend on , , , , or (the existential over precedes all of them).
A complete development needs: the matrix form of the value function, Neumann series and nonnegativity of ; variance identities for finite distributions; a Bernstein inequality for i.i.d. bounded categorical samples with a union bound over states and indices; and the algebra of the recursive expansion. The resolvent and total-variance lemmas are reusable for any tabular discounted MDP. Proofs of individual milestones are welcome independently; (70) is a standalone classical result.
Impact investing selects securities by a non-financial score, an ESG rating, a carbon intensity, a measure of social benefit, and asks whether such a selection earns an excess return. A. W. Lo and R. Zhang (SSRN 3944367; published in Management Science, DOI 10.1287/mnsc.2022.01168) model the score as an impact factor and study the returns of securities ranked by with the tools of induced order statistics (concomitants), introduced by Bhattacharya (1974) and David (1973).
Section 4.3 of the paper gives an equilibrium reading of the apparent excess return. In a -factor asset-pricing model with no mispricing, an investor who accounts only for the first factor sees the contribution of the omitted factors to security 's return as alpha. If the impact factor is correlated with these omitted factors, ranking by impact selects omitted-factor risk, and the selected portfolio appears to earn an excess return. Empirical studies of sin stocks (Blitz and Fabozzi, 2017) and ESG scores (Madhavan, Sobczyk and Ang, 2021) report exactly this effect. Proposition 5 quantifies it in closed form.
There are securities. For security , is its impact factor and the total net contribution of the omitted factors to its return. Write and , random vectors on a probability space .
Order statistics. Sorting the entries of increasingly gives , the order statistics of . If is the sorting permutation, , and the induced order statistic is the omitted-factor return of the security with the -th smallest impact factor. The order is induced by , never by (display (6), p. 11).
Assumption (A2) (p. 19). The vector is Gaussian with exchangeable first and second moments: , , , , , and for , , , . The paper normalises and and keeps a free premium . The adjusted correlation is
Under (A2), for every rank and every pair of ranks ,
The goal states (27) with the factor on the last term. The paper prints without it. That is a slip: replacing by with multiplies the left side by and leaves every correlation unchanged, so the printed formula fails whenever . With , the correct value is , which is the goal's right side.
The result. Proposition 5 shows that the apparent alpha of the security ranked -th by impact is . A selection rule that looks unrelated to return characteristics still produces nonzero excess returns when it is correlated with omitted priced factors, and the size of the effect is governed by the single number . The authors use this to argue that impact estimates are unreliable until all known factors are accounted for, and that a persistent impact premium may signal a new factor (an "ESG factor" or a "carbon factor"). The variance and covariance formulas give the risk of any portfolio of impact-ranked securities, through the moments of Gaussian order statistics.
Formalizing it. The paper proves (25) in full and states that (26)–(27) "can be proven similarly"; the printed (27) is off by the factor . A machine-checked proof settles the corrected constants. No part of this result, and no theory of induced order statistics, is formalized in Lean or elsewhere to our knowledge. The development needs a usable library on concomitants of Gaussian order statistics, which would serve the rest of the paper (Propositions 2, 4 and 6) and the data-snooping analysis of Lo and MacKinlay (1990), which uses the same tools.
The mean formula looks like linearity of expectation, but is evaluated at a random index that depends on , so is not for any fixed . The decomposition of milestone 1 is what handles this. It requires the full joint Gaussian law of , because uncorrelated is not independent otherwise. It also needs a correction term through the cross-sectional average, because the cross-correlations and make depend on all of . In Lean, the sorting permutation must be shown measurable in , and the moments of the order statistics must be shown finite.
Fin N → Ω → ℝ on a probability space. (A2) is the predicate IsA2: joint Gaussianity of the -vector (Mathlib's HasGaussianLaw on (Fin N → ℝ) × (Fin N → ℝ)), plus the moments (22)–(23) stated as covariances with .IsA2. is free.Fin N): Lean's rank is the paper's . Sorting uses Tuple.sort, which breaks ties by index; ties have probability zero and the statements hold for any tie-breaking rule. Moments are Mathlib's integral, variance and covariance. The milestones use where the page writes in .Tuple.sort as a function of the data; integrability and moments of Gaussian order statistics; moments of a vector independent of read at an -dependent random index. Each of these is reusable well beyond this mission.Many allocation problems divide work, not goods: shifts among employees, teaching loads among faculty, cleaning duties among housemates, maintenance tasks among the owners of a shared resource. For divisible goods the standard fair and efficient solution is the competitive rule (competitive equilibrium from budgets): give every agent a budget, find prices at which every agent demands what she receives, and the outcome is Pareto optimal and envy-free (weighted by budgets). For goods with additive utilities this rule is single-valued and is the solution of the Eisenberg–Gale convex program, which yields polynomial-time algorithms.
For chores (bads) the competitive rule keeps its fairness and efficiency guarantees but loses the convex structure: Bogomolnaia, Moulin, Sandomirskiy and Yanovskaya (BMSY17) showed it is generally multi-valued, with competitive allocations corresponding to critical points, not maximizers, of the Nash social welfare on the Pareto frontier. Brânzei and Sandomirskiy (arXiv:1907.01766v2, Mathematics of Operations Research, 2024) enumerate all competitive utility profiles in strongly polynomial time when the number of agents or the number of chores is fixed. Their counting result is the target of this mission.
There are agents and divisible chores, one unit of each. Agent 's value for one unit of chore is , and her budget is . A feasible allocation is with for every chore ; agent 's utility is , the utility profile is , and is the set of utility profiles of feasible allocations.
A feasible allocation is competitive for budgets if there are prices such that for every agent the bundle costs and maximizes among all bundles with . A competitive utility profile is for a competitive .
is Pareto optimal if no feasible allocation makes every agent weakly better off and some agent strictly better off; the Pareto frontier consists of their utility profiles. For weights the face of the Pareto frontier is the set of maximizers of over .
The proof runs through graphs. The consumption graph links agent and chore when . The maximal weighted welfare (MWW) graph links and when for every agent . A family of graphs is rich if every Pareto optimal profile in is for a feasible whose consumption graph is in the family. Along a path the product of disutilities is .
For , and ,
The result. Corollary 25 says that the competitive rule for chores, although multi-valued and non-convex, has at most polynomially many outcomes when or is fixed, and that the Pareto frontier has polynomially many faces meeting the negative orthant. It is the exact mathematical content of the paper's algorithmic Theorem 17: an enumeration that tries every graph of a rich family and recovers at most one candidate profile from each cannot miss a competitive profile and cannot produce more than of them. For the bound is attained in Example 1 of the paper by the face count.
Formalizing it. The result is proved in the paper; nothing is known to be machine-checked. The mission builds a reusable layer for linear Fisher-type economies with bads: the competitive rule with negative prices and budgets, welfare theorems, the trading-cycle and weighted-welfare criteria of Pareto optimality, and the graph-theoretic description of the faces of a polytope of feasible utilities. Lemma 14 and Lemma 18 are of independent use for any linear allocation model.
The obvious argument for goods, uniqueness of the equilibrium utility profile via a strictly concave program, fails: for chores there may be several competitive profiles, even on a single closed face (in Example 1 of the paper, both competitive profiles lie on one edge of the frontier). The count must therefore pass through combinatorics. Two steps carry the weight. First, the faces of the Pareto frontier, a continuous object, must be put in bijection with a finite set of graphs, and the graphs must be chosen so that each competitive profile is realized by an allocation whose consumption graph is exactly an MWW graph, not merely contained in one. Second, the size bound cannot come from counting bipartite graphs, which gives only ; it has to exploit the structure of MWW graphs, and its second term, polynomial in for fixed , requires the agent–chore symmetry of Lemma 22, whose natural route goes through the second welfare theorem.
Agents are Fin n, chores Fin m (0-based); values, budgets and prices are real functions; graphs are Finset (Fin n × Fin m) of edges; a path is a record of its length , agents and chores. Faces are the sets of maximizers of over for , the dual representation of p. 16. Counts are Set.encard in and the bound is computed in . Added relative to the paper: and (the paper's sets of agents and chores are non-empty) where a statement needs them. Not formalized: the running-time claims (Theorem 17, the second bullet of Lemma 23), item 4 of Lemma 38 (critical points of the Nash social welfare), and the sentence on p. 27 that each face carries at most one competitive profile, which is false for closed faces.
The following formalizations would trivialize the goal and are ruled out: a competitive allocation without the budget constraint ; non-negative values, budgets or prices; faces exposed by or by of arbitrary sign; counts over sets assumed finite; Pareto optimality restricted to a subclass of allocations.
All definitions live in CompetitiveChores.RichFamily; Mathlib supplies only finite sums and products, Finset, and Set.encard. Contributions welcome: proofs of the appendix lemmas (pure linear algebra on finite sums), of Lemma 14 (the cycle-cancelling argument of Appendix B), and of the two-agent splits-and-cuts count inside Lemma 23.
Reinforcement learning with a generative model (a simulator) is a basic way to measure how many samples planning needs. A learner may query, for any state , action and step , a fresh next state drawn from the unknown transition law , and must output a near-optimal policy. Model-based planning is the simplest approach: estimate each transition law by empirical frequencies, then solve the estimated model exactly by dynamic programming. It is widely used, and its sample complexity is the reference point for model-free methods.
G. Li, Y. Wei, Y. Chi and Y. Chen (arXiv:2005.12900v8; Operations Research, 2024) show that model-based planning is minimax optimal over the full range of accuracies, for discounted MDPs (Theorems 1–3) and for time-inhomogeneous finite-horizon MDPs (Theorem 4). This mission covers the finite-horizon case. Earlier model-based analyses of the finite-horizon setting, such as Yin et al. (2021), required samples per triple up to logarithmic factors before any guarantee applied; Theorem 4 needs only .
A finite-horizon MDP has a finite state space , a finite nonempty action space , a horizon , and for every step a transition kernel and a reward . The kernels may differ across steps (time inhomogeneity).
A deterministic nonstationary policy chooses action at step in state . Its value and Q-function satisfy the backward Bellman equations
so is the expected sum of rewards from step to started at , and lies in . The optimal values are and .
The generative model returns, for every triple , independent samples , all samples independent. The empirical kernel is
and the empirical MDP replaces every by , keeping the rewards. Model-based planning returns the policy obtained by backward dynamic programming on : at each step, maximizes the empirical optimal Q-function . So depends only on .
There is a universal constant such that for every finite-horizon MDP, every and every : if
then with probability at least ,
The constant is not specified, so the goal survives any improvement of constants.
The result. The total number of samples is , so Theorem 4 gives -optimal policies from samples, which matches the known lower bound up to logarithmic factors, for every . The extra factor of compared with the discounted case is the price of time inhomogeneity: each step has its own kernel to estimate. The guarantee holds from samples per triple on, instead of . Unlike the paper's discounted results, no reward perturbation or conservative action selection is needed. The step-by-step independence of the data makes the plain planner analyzable.
Formalizing it. The theorem is proved in the paper; nothing here is open mathematically, and no machine-checked proof of it is known. A formalization checks the details the paper leaves implicit: the index ranges of the backward recursions, the use of as an integer, the sample-size condition of Lemma 9 when it is applied to the planner's policy, and the independence argument that lets a data-dependent policy enjoy fixed-policy concentration. The finite-horizon layer here (time-inhomogeneous kernels, backward propagation, the DP planner, the empirical kernel and the finite law of the data) is reusable by other finite-horizon sample-complexity results.
The planner's policy is built from the same data that define , so the obvious route, applying a concentration inequality to as if were fixed, is not justified by itself. The argument has to use the backward structure: the step- quantities depend only on the data of later steps, which are independent of .
A second difficulty is the sample-size range. A Hoeffding-type bound on each one-step error, summed over steps, gives an accuracy that only becomes meaningful when . Reaching requires Bernstein-type bounds and the control of a whole sequence of auxiliary value vectors , of which Lemma 12 bounds the size. Lemma 9 then has to close the recursion in after about levels.
Fin H, 0-based: the paper's step is Lean's . Backward propagation returns at every index , which encodes . The paper's ranges in (63) and (66) are written h.val + 1 < H.sel (any argmax rule), fixed before the data and quantified outside the probability. Empirical Q-values tie with positive probability, and the proof needs to be a fixed function of the empirical kernels.Trivializing formalizations are ruled out: the planner is computed from the empirical kernels, not from the true ; the model is time-inhomogeneous, with one kernel per step; and cannot depend on , , or the MDP.
The only external definition is the published FoundationsML.ReinforcementLearning.IsTransitionKernel. A complete development needs Bernstein's inequality for bounded i.i.d. averages (on finite product laws), a union bound, and the independence of the per-step data. Contributions are welcome on all six milestones and on general lemmas about the finite law of the data, such as independence across steps and the distribution of .
When one agent breaches a contract, the breach often forces its counterparty to breach its own contracts in turn, and the losses propagate. Supply chains are the standard example: a supplier that fails to deliver makes its customer fail to deliver to its own customers. Gudmundsson, Hougaard and Ko (Management Science 70(3), 2024) ask how the total loss of such a cascade should be shared among the agents involved. Their aim is a rule simple enough to be written into a smart contract that settles disputes automatically. They first treat a single chain of agents and characterize the fixed-fraction rules by four axioms (Theorem 1). Section 5 then extends the model to loss trees, in which one agent may cause losses to several others, as when a firm supplies several downstream firms. Theorem 4 shows that the same four axioms, suitably extended, characterize the fixed-fraction rules on trees. This mission formalizes Theorem 4 and the steps of its proof in Appendix A.
The tree model follows a line of work on sharing liability and costs along hierarchies and networks; the paper compares its setting with Oishi, van der Laan and van den Brink (2023).
Agents are natural numbers. An edge records that agent causes a loss to agent . A finite edge set covers the vertices . It is a tree if it has a root (a vertex with no incoming edge) and every other vertex has exactly one incoming edge and is reached from the root. The root is the initiator of the cascade. Leaves are victims only. The agents who share the losses are the non-leaf vertices . A loss is a function on edges, and the total loss is .
A rule assigns a liability to each agent . Liabilities are non-negative and sum to . A rule is required to be invariant to agent labels: renaming the agents by a bijection of renames the liabilities. It is also continuous along as , the paper's standing assumption.
The fixed-fraction rule with parameter makes each agent pay the fraction of the losses it causes directly. The root also pays the remaining fraction of the total:
The elementary tree problem is the chain with a unit loss on its last edge. For a vertex , is the set of edges on the path from the root to , is the number of vertices on that path, and is the subtree rooted at .
The four axioms are as follows.
For every rule on loss trees,
Theorem 4 says that the axioms which single out the fixed-fraction rules on chains still single them out on trees, with nothing added. Because the rule only needs each agent's direct losses and the identity of the initiator, it can be computed locally. This is what the paper uses to implement liability sharing in a smart contract (Section 6, Figure 3). The characterization also justifies applying the rule to supply networks, where firms supply several customers, rather than only to chains.
The paper's proof of Theorem 4 is a short sketch: it reduces trees to chains by trimming and relabelling, then cites the chain argument. No machine-checked version of any part of the paper exists. Formalizing it would check the reduction in full, including the bookkeeping that the printed proof compresses. While preparing this mission, three places where the printed text differs from what the argument establishes were found; they are corrected here (see Formalization scope). The tree machinery built here (paths, depths, subtrees, relabelling of finite rooted trees over ) is reusable for other liability and cost-sharing models on hierarchies.
The obvious argument works edge by edge: use additivity to isolate one edge, use zero truncation to cut the tree down to the path through that edge, then relabel the path into a chain. The first gap is that additivity yields only rational homogeneity. Continuity, or the monotonicity that additivity and non-negativity give, is needed for real multiples. The second is that zero truncation only adds or removes leaf edges, so trimming must proceed leaf by leaf, keeping a tree at every step. It must also be shown that agents removed from the tree carried no liability, which needs balance and non-negativity. The third is that relabelling requires a bijection of all of that maps the path onto , together with a loss on the relabelled tree. Label invariance must hold for every such loss, not only one chosen extension. Finally, the chain part (Proposition 2) pins down by an induction that chains population-monotonicity inequalities with merging proofness.
Trees are Finset (ℕ × ℕ) with the root, unique-parent and reachability conditions above. Vertex labels keep the paper's numbering ( uses ); Lean's also contains , which label invariance makes harmless. A rule is a function φ T ℓ i on all edge sets, real functions and naturals. Every axiom and every conclusion is quantified only over trees, non-negative losses and agents . The conclusion is equality at those arguments. A function equality would be false, since a rule's other values are arbitrary. The rule conditions (non-negativity, balance, label invariance, continuity) are a hypothesis of every statement. Dropping them makes Theorem 4 false: the parameter need not lie in , and a rule need not respect the tree's labels. The root of is detected as the vertex with no incoming edge, never hard-coded as label 1.
Three disclosed departures from the printed text:
Continuity is taken from Section 2, where it is standing; the proof of Proposition 3 invokes it. A complete development needs finite rooted trees over , reachability (Relation.ReflTransGen), the extension of a finite injection to a permutation of , and leaf-by-leaf induction on trees. Proofs of any milestone are welcome, as are alternative routes to Theorem 4, for example through monotonicity instead of continuity.
Many service relationships let a firm pause an agent instead of firing them: a sales representative who brings in no customers for a while is suspended, a contractor is laid off for a season and recalled. Pausing is not free. Every restart carries a switching cost (re-training, re-establishing a territory, setting up the work environment), so a principal who suspends too readily pays for it. Cao, Sun and Tian (Management Science, 2024) study the optimal dynamic contract for this trade-off in continuous time, building on the Poisson-arrival moral-hazard model of Sun and Tian (2018). Their main result (Theorem 2) splits the parameter space into three regimes: never hire, hire and keep the agent working forever, and a control-band contract with suspension episodes of fixed length. This mission covers the first regime under the paper's Condition 1.
A principal earns a revenue per arrival of a Poisson process. Without effort the arrival rate is ; an agent who works, at private cost per unit time, raises it to . Write . The principal's cost rate while the agent works is , every start of work costs , and the principal and the agent discount at rates . Assumption 1 is . The derived constants are
The state of a contract is the agent's promised utility . The paper's verification theorem reduces optimality to a pair of functions: for the working state and for the suspended state. For a function on , with its left derivative, the operators are
and satisfies the optimality condition (20)–(22) if , , on , and , .
The working-state candidate is built from the delay differential equation (25): for , is the function on with
and for . may be convex near ; is the point up to which , and the concavification replaces on by its tangent line at . Condition 1 is " or " with
Under it there is a unique with (Lemma 3). Three hats occur in the paper: of Definition 1 (a payment threshold), of Lemma 3 (used here), and of Proposition 6 (not used here). For , Lemma 4 gives a tangent pair : the line touches at . Finally (K1).
Under Condition 1 and , for the pair of (29),
satisfy (20)–(22).
Propositions 2 and 3 are the analytic certificates behind Theorem 2(i): combined with the verification theorem (Theorem 1), they show that under Condition 1 and the principal's utility from any incentive-compatible contract promising is at most , so never hiring the agent is optimal, and is exactly the switching-cost threshold of that regime. The same objects (, , the tangent pairs) reappear in the low-cost control-band regime (Propositions 6–7), so a formal development of the delay ODE and its concavification is reused there.
The paper proves all these results; none is formalized. The mission formalizes the deterministic half of the guess-and-verify argument. The stochastic contract model (point processes, promise keeping, incentive compatibility), Theorem 1 and the optimality theorems are outside its scope.
The obvious approach, verifying (20)–(22) by direct computation, works for the linear pieces but not for , which has no closed form: (25) is a delay equation solved backwards from in steps of length , and the closed form (EC.52) of the paper holds only on the last step . Every property of used in the goal (monotonicity, the single change of convexity, the comparison in that makes unique) has to be extracted from the equation itself, across the kinks of . On the second branch of , is not a pointwise identity either: it requires , which is where enters.
ℝ → ℝ; every statement quantifies over only. In , is the left derivative (derivWithin f (Set.Iic w) w, the paper's p. 15 convention); in statements about and , derivatives are taken within ; in (25), within .Needed infrastructure: existence and uniqueness for linear ODEs with a terminal condition, extended step by step across a delay; one-sided derivatives of piecewise functions; concavity from sign conditions on second derivatives. Proofs of the milestones, and reusable lemmas about delay equations of this form, are welcome.
Online platforms such as ride-hailing, delivery and marketplace companies routinely test a new policy (a pricing rule, a dispatching algorithm) by switching it on and off over time on a single unit, a city or a market, rather than by randomizing over users. These switchback experiments avoid the interference that user-level randomization creates in two-sided markets, but they face a different problem: a treatment administered at one time keeps affecting outcomes for several periods afterwards (carryover effects). Bojinov, Simchi-Levi and Zhao, Design and Analysis of Switchback Experiments (arXiv:2009.00148, Management Science 69(7), 2023), derive the minimax-optimal design when the carryover lasts at most periods, and then ask how to do inference with it. This mission formalizes the inference half: under the optimal design, the Horvitz–Thompson estimator of the lag- effect is asymptotically normal as the number of epochs grows, which is what justifies the paper's normal-approximation test and confidence intervals.
The result is a finite-population central limit theorem: the potential outcomes are fixed, non-random numbers, and all randomness comes from the experimenter's coin flips. It belongs to the line of design-based limit theorems of Li and Ding (2017), Aronow et al. (2017) and Bojinov et al. (2021). Its probabilistic engine is the central limit theorem of Romano and Wolf (2000) for triangular arrays of -dependent random variables, which goes back to the -dependent central limit theorem of Hoeffding and Robbins (1948).
There are time periods . An assignment path records treatment () or control () in each period. The potential outcomes are real numbers . They are assumed non-anticipating (Assumption 1: depends only on ) and to have -carryover effects (Assumption 2: for , does not depend on ). Assumption 3 bounds them: . Write and for the outcome after consecutive treatments, respectively controls. The lag- causal effect is
A regular switchback design flips an independent coin with success probability at each randomization point , and every period copies the most recent coin. The Horvitz–Thompson estimator weights the observed outcome at time by the inverse probability that the last assignments were all treatments (respectively all controls).
In the -replica experiment , and the optimal design of the paper's Theorem 2 uses fair coins at
The periods split into blocks , , with block sums , and block errors , so that . Assumption 4 (non-negligible variance) requires for some and all large .
For fixed , under Assumptions 1–2, Assumption 3 with one bound for all , and Assumption 4,
The statement fixes no rate and does not require to converge.
Corollary 1, the conservative bound with the unbiased estimator , and Corollary 2(i), that (10) still holds when the design is built for an overestimated order .
Theorem 3 is what turns the optimal design into a usable inferential procedure: together with Corollary 1 it gives the test statistic and its normal -value, a conservative large-sample test of the null of no lag- effect that needs no model for the outcomes. Corollary 2 extends the guarantee to a misspecified carryover order . Lemma EC.1 is a general tool, applicable to any statistic that decomposes into a sum of weakly dependent pieces, such as block designs, time-series bootstraps and spatial experiments.
The paper proves these results. None of them is formalized: Mathlib has the central limit theorem for i.i.d. sequences only, and no central limit theorem for dependent arrays exists on the platform. The work here is to formalize the known proof: the exact second-moment computations of the design, the 1-dependence of the blocks, and a proof of the Romano–Wolf theorem itself, which the paper takes from the literature.
The randomness is a finite set of coin flips and the outcomes change with , so no i.i.d. structure is available: the block errors are neither independent nor identically distributed, and the classical Lindeberg–Lévy theorem does not apply. The obvious reduction, treating neighbouring blocks as independent, fails, because adjacent blocks share a coin. This is why the cross terms appear in (10), and why a dependent-array central limit theorem is needed. The variance normalisation is random-design specific and may oscillate in , so the limit theorem has to be proved with a self-normalisation that does not converge. Lemma EC.1 is the main obstacle: a -dependent central limit theorem for triangular arrays with Lyapunov-type moment conditions, which is not in Mathlib.
A path is a function ℕ → Bool of which only is read; potential outcomes are ℕ → Path → ℝ. The design law is encoded as independent coins at the randomization points, mapped to paths; in the -replica experiment the probability space is the uniform measure on the coin vectors of . Row of the sequence has and potential outcomes Y n. Rows exist in Lean but are degenerate and irrelevant to the limit. Convergence in distribution is Mathlib's TendstoInDistribution, and the limit is gaussianReal 0 1. and are explicit constants with an eventual threshold. The estimand, estimator and variance in the goal are the model's definitions, not a hand-written formula in the coins.
Three hypotheses are added to the printed statements, each necessary and disclosed in the item's Formalization Note:
The goal does not assume 1-dependence, the variance formula or any condition of Lemma EC.1; those are milestones, so the goal cannot be discharged by a hypothesis.
A complete development needs:
The last two, Lemma EC.1 and Definition EC.1, are reusable well beyond this mission. Contributions to any milestone, including alternative proofs of Lemma EC.1, are welcome.
Graph alignment asks for the correspondence between the vertices of two graphs that are noisy copies of each other with hidden labels. It arises in the de-anonymization of social networks, where an anonymized friendship graph is matched against a public one (Narayanan–Shmatikov 2009), and in computational biology, where protein–protein interaction networks of related species are aligned. The standard random model is the correlated Erdős–Rényi model of Pedarsani–Grossglauser 2011, for which exact recovery thresholds are known (Cullina–Kiyavash 2016) and almost-exact recovery is known to be impossible when (Cullina–Kiyavash–Mittal–Poor 2018).
Hall and Massoulié (arXiv:2007.00533) study the weaker goal of partial recovery: output a permutation that agrees with the hidden one on a constant fraction of the vertices. This mission formalizes their impossibility theorem; a companion mission (II) formalizes their possibility theorem.
Fix and scalars . A parent graph is copied twice and each copy keeps every edge independently with probability , giving graphs and with adjacency matrices and . Every unordered pair of distinct vertices independently carries the pair with law (equation (3)):
Two independent edges of have law (equation (4)):
The Kullback–Leibler divergence is .
A hidden permutation of the vertices, drawn uniformly from the permutations, relabels into : . An algorithm sees only and returns a permutation , possibly at random. Its quality is the overlap
The mutual information is that of the joint law of and the observation, and counts the permutations that are -close to a given one, out of .
Let , bounded below by a constant for large . If
then for every sequence of algorithms,
The theorem gives a sufficient condition, in terms of a single per-pair divergence, under which no algorithm (efficient or not) recovers even a fraction of the alignment. Together with the companion possibility result (Theorem 2.3: partial recovery is possible when exceeds an explicit constant under sparsity conditions), it brackets the partial-recovery threshold; the paper's Corollary 2.2 specializes it to in the regime .
On the formal side, the mission produces a finite, self-contained model of correlated random graphs with a planted permutation, a generalized Fano inequality for finite hypothesis classes with an arbitrary distance, and the bound of mutual information by a product divergence. The Fano inequality and the mutual-information bounds are reusable for other information-theoretic lower bounds (community detection, planted matching, testing). The paper proves the results on paper; none of them is formalized, and no Fano inequality is proved on the platform.
The Fano inequality (Theorem 3.1) is cited from Lemma 20 of Banerjee–Hegde–Massoulié (2012) and not proved in the paper, and the entropy calculus it rests on is not in Mathlib in a finite, real-valued form. The counting step (Proposition 3.3) concerns rencontres numbers; the paper uses the asymptotic , which is valid only for fixed , while the statement needs control uniform in . Bounding requires relating the conditional law of the observation, a relabelled product law, to the unlabelled reference law on a space of matrix pairs, most of which have probability zero.
A natural first idea for the goal, taking arbitrary as printed, fails: if , the identity algorithm succeeds whenever has a fixed point, with probability tending to , even when the divergence condition holds. The argument needs to grow like , which needs bounded below.
Vertices are Fin n; a vertex pair is an off-diagonal element of Sym2 (Fin n); an edge state is a Bool × Bool with first coordinate , second . The probability of a configuration is the product of over pairs, and is computed through . Every probability is a finite sum; logarithms are natural. Standing assumptions on the parameters are (pp. 5 and 7); the remark "we assume " of p. 6 is not used and not imposed.
Algorithms are real stochastic kernels from the observed pair to permutations, so randomized algorithms are included and deterministic ones are the 0/1 kernels. The algorithm's argument is the observation only: it does not see or . Mutual information and Kullback–Leibler divergence are defined as finite sums (Lean's ).
Hypotheses added relative to the page, each disclosed in the item's note:
Proposition 3.3 reads as .
Trivializing formalizations are ruled out: the algorithm cannot be given (an oracle wins) or nothing (the statement becomes empty); the little- hypothesis is a limit of a ratio, not an inequality; the configuration law is built from (3) and sums to 1, not chosen by the solver.
Infrastructure a complete development needs: finite entropy and mutual information with the chain rule and data processing; Gibbs' inequality; derangement and rencontres counts (numDerangements in Mathlib); Stirling-type lower bounds on . Contributions are welcome on each milestone independently; the Fano inequality is the piece with the widest reuse.
The source is the arXiv preprint v5 (13 Jan 2022); its numbering is used throughout.
Phase estimation asks: given access to a unitary and an eigenvector with , determine . It is the subroutine behind Shor's factoring algorithm, quantum chemistry energy estimation, and amplitude estimation, and is one of the standard sources of quantum speed-up.
Martyn, Rossi, Tan and Chuang, A Grand Unification of Quantum Algorithms (PRX Quantum 2, 040203, 2021), present search, phase estimation and Hamiltonian simulation as instances of one primitive, the quantum singular value transformation (QSVT) of Gilyén, Su, Low and Wiebe (arXiv:1806.01838, STOC 2019). Most of the paper's numbered results restate QSVT theory from earlier work. Its own proved content is Appendix B: the analysis of phase estimation by QSVT (Section V, Algorithm 3), a bit-by-bit binary search in the spirit of Kitaev's iterative phase estimation, where each bit is read by applying a sign function to a singular value. A closely related QSVT phase-estimation algorithm was found independently by Rall (arXiv:2103.09717).
This mission formalizes that analysis: the exact-arithmetic correctness of the bit search (Theorems 6 and 7), and its robustness when the sign function is only approximated (Theorem 8).
Fix a unitary , an eigenvector , and the phase . Write for the fractional part of .
For and , the matrix acts on with singular value
The procedure keeps a binary fraction , initially , and runs iterations for a positive integer . Iteration halves , evaluates the sign function at through QSVT, measures one ancilla bit , and sets the first binary digit of to :
An additional iteration then sets the units digit , and the output is .
The ideal measurement returns when and when . In practice the sign function is replaced by a polynomial that is reliable only outside the Δ-region ; inside it either bit may be returned.
If
then in every run of the procedure, the singular value can fall in the Δ-region only at the first iteration , and the output satisfies
A companion item states (68): the matrix of Figure 10 is unitary and block-encodes .
Theorem 8 is what makes phase estimation by QSVT implementable: a sign function cannot be realized exactly by a polynomial, and the theorem shows that a polynomial approximation which fails on a band of width about around costs at most one bit of accuracy, and only at one iteration. Combined with the per-iteration failure probability analysis (71)–(72), it yields the paper's claim that queries give an -bit estimate with probability .
On the formal side, the paper proves these results in Appendix B by case analysis on binary digits with carries. No machine-checked version of the analysis exists on the platform, and no QSVT-based phase-estimation result has been formalized elsewhere to the curators' knowledge. The mission separates the deterministic correctness of the bit search from the quantum machinery, so the combinatorial core can be checked independently of QSVT itself.
The obvious argument tracks the digits of one at a time, and it works for an -bit phase. It fails when has more than digits: the sign function rounds rather than truncates, so a bit can be set to when the true digit is , carries propagate, and the invariant must be a rounding statement with a carry bit (Lemma 12's nine-case induction). The final bit can carry into the units place, which is why the additional iteration exists.
For Theorem 8, the natural first idea, that a bit error makes all later bits unreliable, is false; the content is that after an error at the distance stays a fixed amount away from the Δ-region at every later iteration. Turning this into the threshold requires precise bounds on near .
Everything is stated in Lean 4 with Mathlib, over , in the namespace QSVTPhaseEst.BitSearch. The conventions:
Bool; is Int.fract (2^j * φ).A formalization in which the outcome rule mentions , its digits or its rounding, in which is written through the digits of , or in which the output is defined as a rounding of , would make the theorems circular; none of these is used.
Not formalized: QSP and QSVT themselves (Theorems 1–4, 9, 10; Theorem 1 is already an open goal on the platform), the polynomial of (69), the -error probability analysis (71)–(72), and the runtime. Contributions of reusable lemmas on binary roundings (Int.fract of , nearest dyadic rounding with carry) and on near are welcome.
Sampling from a Gibbs distribution on is a basic task in Bayesian statistics, statistical physics and machine learning. A standard approach simulates the Langevin diffusion , whose invariant distribution is , through its Euler scheme, and averages a test function along one long trajectory. The discretization introduces a bias of the order of the step size, so a single-step-size average with accuracy costs more than steps. Dalalyan (arXiv:1412.7392) and Durmus–Moulines (arXiv:1605.01559) quantified this for strongly log-concave targets; for occupation measures of the Euler scheme the best previous bound was of order (Durmus–Moulines, Bernoulli 2019, denoted [DM19] in the paper).
Egéa and Panloup (arXiv:2109.07753, Math. Oper. Res., 2025) combine Giles's multilevel Monte Carlo idea (Oper. Res. 2008) with pathwise averages. Each level is one long trajectory, not many independent samples. This mission formalizes their result for a uniformly strongly contractive, twice differentiable drift. In that case the multilevel occupation measure reaches accuracy at a cost of order , the order of an unbiased Monte Carlo method.
Let be -Lipschitz and satisfy Assumption : for all , with . Let . The additive diffusion is , driven by a standard -dimensional Brownian motion . Let be its invariant distribution. Its Euler scheme with step is , , with invariant distribution . Write and for the Lipschitz constant of .
Given a first step , steps , horizons , a warm start , and independent Brownian motions , the multilevel occupation measure (7) is
where both schemes of level start at and are driven by . Its cost is .
When is with bounded derivatives, set (Frobenius norm of the Jacobian) and . The constant (19) is
Take , , and . There is a universal constant such that for every with ,
The constant is the same for all , , , , , and .
Under , and dimension-free bounds on , and , the choice , gives .
The milestones follow the paper's proof in order:
The result. Theorem 2.3 gives an explicit algorithm whose cost to reach accuracy on is of order , uniformly over Lipschitz . Under (22) the cost is . Apart from constants depending on and , this is the complexity of a Monte Carlo method without bias, an improvement over the known for single-level occupation measures. Corollary 2.2 of the paper applies it to Gibbs distributions with a potential.
Formalizing it. The theorem is proved in the paper. A machine-checked version needs a formal multilevel estimator over infinite horizons, uniform-in-time strong error bounds for the Euler scheme, and an application of Itô's formula to , none of which exists in Lean. Formalizing also checks the paper's constants. For instance, the printed exponential rate in the contraction behind is , while its proof gives , and the milestone states . No part of this result has been machine-checked.
Two steps resist a direct approach. First, the order-one strong error (Lemma 5.2(ii), Proposition 5.1(ii)). Bounding the one-step error by the Lipschitz constant alone gives order per step, hence order globally; this is Lemma 5.2(i) and the regime, with an extra in the cost. The gain to needs the second-order structure of along the Brownian path, through a martingale term and the Laplacian of . Second, the error must be controlled uniformly over infinite horizons. Every estimate has to combine the contraction with the step-size restriction ; a Gronwall argument on a finite horizon gives constants that grow with time.
For the goal itself, the cost bound (21) is arithmetic once the parameters are fixed. The content is the error bound with a constant that is universal, not merely independent of .
EthierKurtz.SDEState d, and Brownian motions are the published EthierKurtz.IsStandardBrownian.eLpNorm · 2 P, valued in . The schemes are evaluated at grid times, except in and (47), which use the continuous-time scheme.ContDiff ℝ 2 b plus a uniform bound on the first and second Fréchet derivatives.The goal does not assume –, Proposition 2.2 or any variance or bias estimate. It assumes only , Lipschitz and regularity of , , invariance of and the parameter choices. Those results appear only as milestones.
Contributions that would be reusable elsewhere: uniform-in-time moment and strong-error bounds for Euler schemes of contractive SDEs, Itô's formula for a function of Brownian motion, and the general multilevel complexity theorem (Remark 4.1). Proofs of the milestones are welcome independently.
Networks observed over time, such as communication graphs, contact networks and financial exposure graphs, often change structure abruptly. Change-point detection asks whether the law of the network changed during the observation window. In practice not every pair of nodes is observed at every time: links are missing because of sampling, privacy or measurement failure. Enikeeva and Klopp (arXiv:2106.14470, published in Operations Research, 2025) give the minimax detection boundary for this problem in a sparse inhomogeneous random graph model with missing links, for a change at a known time and at an unknown time.
This mission formalizes the upper bound at a known time (their Theorem 1): a test based on the spectral norm of a matrix-valued CUSUM statistic has level and type II error at most as soon as the change is a constant multiple of plus a logarithmic term. The companion missions of this series formalize the matching lower bound (Theorem 2) and the unknown-time test (Theorem 3).
There are vertices and snapshots. At time the network has a symmetric, zero-diagonal connection-probability matrix , and each pair is sampled independently with probability , where the sampling matrix is symmetric with . What is observed is , symmetric with zero diagonal, whose entries , , are independent Bernoulli variables with success probability , independent over ; is the entrywise product.
The column-wise norm measures the largest expected observed degree. The null class is
A change at time replaces by after time . With and the spectral norm , the change-point energy is , and the alternative class collects the pairs in whose energy is at least .
A test maps the data to . Its type I error is the supremum over the null class of the probability of rejecting, and its type II error is the supremum over of the probability of accepting.
The Matrix CUSUM is
and the test at the known time is
with and a constant depending only on .
For every there are constants and , depending only on , such that for all , , and : if
then and . The constants are existential and are not pinned to particular values; the statement asserts the shape of the boundary.
Theorem 1 is the upper half of the minimax detection boundary for a change at a known time. Together with Theorem 2 of the same paper (a lower bound of order ) it shows that, up to the logarithmic term, the CUSUM test in spectral norm is rate-optimal, and that missing links enter only through the observed degree bound . The same noise bound (Lemma 12) drives the unknown-time test of Theorem 3.
The result is proved in the paper; no machine-checked version exists. Formalizing it produces a checked finite-sample statement with explicit leading constant , a reusable formal Bernoulli network model with missing links, and, through Proposition 11, a formal statement of the Bandeira–van Handel tail bound, which is used well beyond change-point problems. The printed proof of Lemma 12 applies Proposition 11 after conditioning on the event , which destroys centring and independence; a complete proof needs a truncation argument that the paper does not give.
Under the null the CUSUM is pure noise, so both errors reduce to a high-probability bound on whose leading term is exactly after rescaling. Matrix Bernstein inequalities give a bound with an extra factor on the leading term, which is too weak for the stated threshold; the sharp constant requires the Bandeira–van Handel inequality, whose proof goes through moment comparisons for random matrices with non-identically distributed entries. The entries of are themselves sums over time with coefficients up to order in aggregate, so the boundedness hypothesis of Proposition 11 does not hold directly and must be recovered with probability bounds. Finally, the level and the power must hold for the same threshold constant , uniformly in , , and the parameters.
An observation is a function from the snapshots and the pairs to Booleans; time is 0-based in Lean (snapshot is the paper's ). The latent adjacency and sampling matrices are integrated out: only is modelled, by its exact product-Bernoulli law, and probabilities are finite sums over the finite observation space, so every test is measurable. Tests are Boolean-valued (true rejects). The sampling class carries the paper's standing assumptions and . Errors are real suprema over sets contained in ; an empty alternative class has type II error . The spectral norm is the published HighDimProb.RandomMatrices.matrixOpNorm. Proposition 11 alone uses measure theory, with independence of the entries on and above the diagonal and an added (implicit) .
Disclosed readings: (24) prints , which is read as as in the proof; Lemma 12's matrices are the symmetric, zero-diagonal centred observations of the model; Lemmas 3 and 4 take " is a constant of Lemma 12" (with ) as a hypothesis, stated as a predicate. The goal does not assume that predicate: it asserts the existence of and , both chosen before , , , , , and , so neither constant can be tuned to the instance, and tests range over all functions of the data. Choosing huge constants does not trivialize the goal, since for large the energy condition is met by nonempty alternatives that the test must detect.
The development needs: the product-Bernoulli law of the network, the Matrix CUSUM algebra, the Bandeira–van Handel inequality, and a truncation argument for Lemma 12. The Setting and Proposition 11 are reusable for the unknown-time test and for spectral methods on random graphs. Proofs of any milestone, and alternative routes to Lemma 12, are welcome.
In a principal–agent problem with moral hazard, a principal (an employer) pays an agent whose effort she cannot observe; she sees only an output process whose drift the effort controls. Continuous-time versions of the problem, starting with Holmström–Milgrom (1987) and Sannikov (2008), are solved by turning the agent's continuation utility into a state variable and writing a Hamilton–Jacobi–Bellman (HJB) equation for the principal's value.
Most of this literature assumes two-sided commitment: the agent cannot leave. In labour markets the agent can quit whenever an outside offer beats his continuation utility, and the principal must then hire someone else. Zhang and Zhu (arXiv:2208.06473; Mathematics of Operations Research, 2025) study this one-sided commitment: the principal is committed to the contract, the agent is free to quit at a stopping time of his choice, and after each quitting the principal pays a cost and hires a new agent, possibly of another type. The principal's value then depends on every future hire, and the paper characterises it by a coupled system of HJB equations.
Fix a horizon and a payment cap . A standard Brownian motion on is the output. Agents have types . An agent of type receiving a payment rate and exerting effort has running utility and running cost ; is increasing and concave in , is convex in (Assumption 2.2). Effort shifts the drift of through the Girsanov measure (weak formulation). The agent's optimal effort against a sensitivity process is , the inverse of , and denotes expectation under the corresponding measure.
A contract started at time is described in forward form by : the agent's continuation utility is
with and the constraint . The agent's utility is capped by the upper barrier . He quits at the first time reaches the lower barrier , where is his market value and his quitting cost (Assumptions 2.7, 3.1). The relevant domain is
When the -th agent quits at , the principal pays and hires an agent of type at utility (the quitting sequence (5.8)). The principal's value is
and the value of the best new hire at time is .
The family is the minimal continuous viscosity solution of
with boundary conditions
The last condition couples the equations for different types. The goal also asserts that the value sets in (6.1) are nonempty and bounded above, so that is a genuine real-valued function.
The theorem identifies the principal's value under one-sided commitment as a PDE object, which makes it computable and comparable with other contracting regimes. Along the way the paper shows that the principal sees only finitely many quittings (Proposition 6.1) and that tolerating more quittings never lowers her value, so contracts that prevent quitting altogether (self-enforcing contracts) are in general suboptimal. The coupling through turns the problem into an infinite system of HJB equations indexed by agent types, a structure that also appears in switching and re-hiring problems.
The result is proved in the paper; none of it is formalized. A formalization would add to the platform a continuous-time moral-hazard model in the weak formulation, hitting-time stopping driven by an Itô integral, a quitting sequence with random restarts and type switching, and a viscosity-solution notion for a fully nonlinear HJB equation on a time-dependent domain. The paper's own proof leaves several steps to the reader (the dynamic programming principle, the viscosity property, comparison for a truncated equation), so a complete development would also supply these.
The obvious route is "dynamic programming principle, then viscosity property, then comparison". Each step is harder here than in a textbook control problem. The control is unbounded, so the Hamiltonian can be and the viscosity property must be derived without a finite Hamiltonian. The process is stopped at a hitting time of a moving barrier and restarted at a random level with a new type, so the dynamic programming principle must handle restarts. Minimality cannot come from a standard comparison principle, because the boundary datum at depends on the competitor itself and no growth condition is imposed on competitors; the paper argues through approximation by and Theorem 4.5 instead.
All objects are defined in the namespace DynPrincipalAgent.HJB. Process time is ; deterministic data are functions of real time. The Itô integral is the published Peng1990.SMP.IsItoIntegral, with a continuous version required wherever hitting times read paths. Controls started at are progressively measurable for the filtration of . Value functions are real suprema of value sets that record an expectation only when it is genuine (integrable payoffs, almost surely integrable drifts and running rewards, summable quitting costs); these conditions hold for every admissible control.
Pinned readings, all disclosed in the items: viscosity solutions are the standard Crandall–Ishii–Lions notion with test functions on , tested on the interior of , with the supremum in the HJB operator never formed; the boundary condition at requires a real right limit compared against every ; carries a σ-algebra and , , are jointly measurable; Assumption 2.7 (ii) is read as ; a modulus of continuity is nondecreasing, vanishes at and satisfies ; generic constants depend only on and are fixed before the model; and take the closed forms of (2.11)–(2.12). The agent's BSDE and reflected BSDE (Propositions 2.3, 3.2), §7's standard contracts and the economic interpretation of , , are out of scope.
A formalization in which a value function equals a junk value (an empty or unbounded real supremum, a Bochner integral of a non-integrable payoff, a hitting time of an empty set) or in which the viscosity notion is vacuous does not count: the goal states that the value sets are nonempty and bounded, and the definitions avoid junk by construction. Competitors in the minimality clause satisfy exactly the printed boundary conditions, with no added growth bound.
Reusable infrastructure: Girsanov measures for BMO drifts, forward utility processes, hitting times of continuous semimartingales, and viscosity solutions of HJB equations on non-cylindrical domains. Contributions on any milestone, and on general lemmas such as the dynamic programming principle for controlled diffusions stopped at hitting times, are welcome.
Mean-variance (MV) preferences, , are the standard objective of portfolio selection since Markowitz. They are not monotone: an investor can prefer a terminal wealth to a wealth that is larger in every state, because the extra upside raises the variance. Monotone mean-variance (MMV) preferences (Maccheroni, Marinacci, Rustichini and Taboga, 2009) repair this. They are the largest monotone preferences that agree with MV preferences on the domain of monotonicity .
A natural question is when switching from MV to MMV changes the optimal investment. In continuous-time markets driven only by Brownian motions, the optimal strategies under the two preferences coincide (Trybuła and Zawisza, 2019, for a stochastic factor model; Strub and Li, 2020, for continuous semimartingale markets), and whether this persists with jumps was left open by Trybuła and Zawisza. Li, Liang and Pang study a market whose risky asset also jumps and whose coefficients depend on a stochastic factor. They show that the two problems agree if and only if a pathwise condition on the jumps, Assumption 1, holds.
On a probability space live two independent Brownian motions and an independent Poisson random measure with finite Lévy measure and compensated measure . The filtration is generated by . A stochastic factor follows
with . Investing the amount in the risky asset gives the (discounted) wealth
on , with . Write and .
The MMV preference is
The infimum runs either over the Doléans-Dade measures or over all of . A measure in has density , where is the stochastic exponential of with , and .
The optimal utilities from are suprema over the admissible strategies of the paper's Definitions 2 and 3: predictable whose wealth has , under for MV and under every for MMV. Both solutions are expressed through the solution of the nonlinear parabolic PDE (20),
Through it also enters Assumption 1. Let be the first jump time after at which . Assumption 1 requires at every jump in up to time .
The same holds when ranges over instead of .
The result separates the two preferences by an observable property of the market. The Brownian theory gives agreement for free. With jumps the MV-optimal wealth can leave , and that happens exactly when a jump of size can occur before the first jump with . In that case MMV and MV investors hold different portfolios. The paper's §5.4 examines in market data whether Assumption 1 is reasonable. The explicit closed forms (the value , the variance of the optimal wealth, the efficient frontier) are what applied work uses.
The result is proved on paper, in an arXiv preprint later published in Mathematics of Operations Research (2025). None of it is machine-checked. A formal proof would check the verification arguments for a stochastic differential game with jumps, a Feynman–Kac representation with a jump density, and the comparison with Maccheroni et al.'s monotone hull. The paper's own proofs are brief at several of these steps. The underlying infrastructure (Itô calculus with Poisson jumps, Doléans-Dade exponentials, verification theorems) would be reusable for most of continuous-time portfolio theory.
The obvious argument would show along the optimal wealth and conclude. Lemma 4 shows this argument breaks: the optimal MV wealth need not lie in . Remark 7 also notes that membership in alone does not identify the optimal values; both optimal strategies must be found and compared.
Finding them needs a verification theorem for a two-player stochastic differential game with jumps (Theorems 1 and 4). That in turn needs Itô's formula for jump diffusions and martingale properties of Doléans-Dade exponentials that may vanish (Lemma 2, Mémin's criterion). Identifying the two strategies needs the moment identities , which come from a Feynman–Kac argument with a jump-driven density (Lemma 3). The converse direction needs a stopping argument at the first "bad" jump. None of this exists in Mathlib, which has Brownian motion but no stochastic integral and no Poisson process.
Peng1990.SMP.Stochastic. The admissible classes , , therefore contain only strategies whose Brownian integrands are in ; all strategies used in the paper qualify.JacodTodorov10.LLN.IsFPoisson with finite and . The compensated integral is the pathwise sum over atoms minus the compensator integral.Function.leftLim. Feedback strategies come with an existence claim, never as bare assumptions.EReal over the full admissible classes. Measures in are probability measures.A formalization that replaces either optimal utility by a closed form or by the utility of one fixed strategy is out of scope: it assumes Theorems 4 and 7 and empties the goal. So is one that removes the jumps, freezes the factor, or replaces Assumption 1 by a sufficient condition such as ; each of these makes the "only if" vacuous or false. Contributions that build general infrastructure (an Itô formula for jump diffusions, Doléans-Dade exponentials, a Feynman–Kac theorem) are especially welcome.
Sampling from a Gibbs distribution on , or computing integrals against it, is a basic task of Bayesian statistics, statistical physics and stochastic optimization. A standard route is to simulate a diffusion whose invariant law is the target, for instance the overdamped Langevin equation , discretize it with the Euler scheme, and average a function along one long trajectory. Discretization introduces a bias of order of the step size, and the long-time average introduces a variance that decays like the inverse of the horizon, so reaching root-mean-square accuracy with a single Euler scheme costs more than steps.
Egéa and Panloup (arXiv:2109.07753, Mathematics of Operations Research, 2025) adapt Giles's multilevel Monte Carlo idea (Giles 2008) to this infinite-horizon setting: they combine a coarse pathwise average with corrections between coupled Euler schemes of successively halved steps, run over decreasing horizons. Their general complexity theorem (Theorem 2.1) is stated under four abstract assumptions (H₁)–(H₄). This mission formalizes the first concrete instance the paper gives: an additive diffusion with a strongly contractive drift, where the assumptions are verified with explicit dependence on the dimension and the cost is of order .
Let and be the Euclidean norm and inner product on . Let be -Lipschitz and satisfy the contractivity assumption :
with . For this is uniform strong convexity of . Let and let be a standard -dimensional Brownian motion. The additive diffusion started at is ; a probability is invariant for it if for all and Borel .
The Euler scheme with step is , , extended to continuous time by , . A probability invariant for one step of the scheme is its invariant distribution.
The multilevel occupation measure with start , coarse step , levels , steps , horizons and warm-start time is
where level uses its own Brownian motion , independent across levels, and both schemes of a level share it. Its cost is , the number of simulated Euler steps. Write for the Lipschitz constant of and
There is a universal constant such that, for , , the parameters
and every with ,
The constant does not depend on , , , , or ; all dependence on the problem sits in the explicit cost.
The goal gives a complexity of order for approximating by a pathwise average of Euler schemes, within a logarithmic factor of the of an unbiased Monte Carlo method, with constants explicit in , , , . When , the cost is of order . The intermediate results (uniform-in-time strong error of the Euler scheme, Wasserstein bias of its invariant law, step-independent contraction) are standard tools of Langevin Monte Carlo and are reusable on their own.
The results are proved in the paper; none of them is machine-checked. A formal proof would certify both the abstract multilevel argument as instantiated here and the explicit constants. The formal statements also pin three printed slips: the ceiling in (14) (cube of the ceiling, not ceiling of the cube), the first line of (12) (the function of Lemma 5.1 (ii)), and the factor in (15).
The obvious argument controls bias and variance separately for each level. The bias of a pathwise average involves the long-time behaviour of the scheme, and the variance of a correcting level involves the distance between two coupled schemes over an unbounded horizon: both require estimates uniform in time, which fail for a merely Lipschitz drift (the strong error of the Euler scheme grows exponentially on finite horizons). Contractivity is what makes the strong error uniformly in , and the delicate point is to obtain this with constants that do not degrade with or with the step. The complexity bound then requires balancing , the horizons and the warm start so that the long-time bias, the discretization bias and the variances all sit at level , with a universal constant.
is EuclideanSpace ℝ (Fin d) (published EthierKurtz.SDEState); Brownian motions are published EthierKurtz.IsStandardBrownian, one per level, mutually independent as path-valued variables. The diffusion is a pathwise solution of the integral equation with continuous paths; no Itô integral is needed because the noise is additive. Invariance of and is stated through transition probabilities. norms are eLpNorm … 2 in , so an infinite moment is never read as zero. is used in its Kantorovich–Rubinstein form, as an explicit integral, and the clause as the existence of a coupling with that quadratic cost (Mathlib has no Wasserstein distance; optimal couplings exist, so the forms agree). (H₁)–(H₃) are stated at grid times, (H₄) over all . "" is an existential constant quantified before every datum.
Standing assumptions carried as hypotheses: -Lipschitz, , (and where the paper requires it), . Added and disclosed: the §5.1 hypotheses in Lemma 5.2, in Proposition 5.2 (needed by Proposition 5.1), integrability of under , existence of and in Remark 4.1. The goal's (a maximum of a set that need not be an interval) is replaced by the inequality defining it.
The goal assumes only the contractive setting, the diffusion's invariance of and the parameter choices; it does not assume (H₁)–(H₄), a bias or a variance bound, which appear only as milestones, so it cannot be discharged by restating its hypotheses.
A complete development needs: second-moment and Grönwall estimates for the Euler scheme and the diffusion, existence and uniqueness of invariant laws of Feller chains under a Lyapunov condition, independence and variance decompositions for the multilevel estimator, and the abstract Theorem 2.1. The Gaussian-increment and Wasserstein tools are reusable well beyond this mission. Proofs of any milestone, and a Mathlib-style for general laws, are welcome.
A fund manager who tracks a benchmark (a stock index, a price index, the cost of higher education) wants the managed wealth to stay above the benchmark at all times. Under a strict floor constraint the set of admissible strategies can be empty when the benchmark is random. Bo, Huang and Yu (arXiv:2302.08302, Math. Oper. Res.) relax the constraint: the manager may inject capital so that , and pays per unit injected. The problem becomes a consumption–investment problem with a running-maximum cost, of the type studied with viscosity methods by Barron–Ishii (1989) and Bokanowski et al. (2015). The paper obtains instead a classical solution of the associated HJB equation and an explicit optimal feedback control. The reduction from the constrained problem to the auxiliary problem below is due to Bo, Liao and Yu (2021) and is not part of this mission.
A market has risky assets with return vector and invertible volatility matrix ; the riskless rate is . On a filtered probability space satisfying the usual conditions with a -dimensional Brownian motion , write and with . The benchmark is , where is a geometric Brownian motion with drift and volatility driven by , and is the running maximum of , .
A strategy invests and consumes at rate ; the class consists of progressively measurable pairs for which the wealth equation is well defined on every bounded interval. The auxiliary states are the reflected wealth surplus , started at ,
where is the minimal nondecreasing process keeping (the injected capital), and the reflected distance started at . With power utility , , and discount rate , the objective is
The candidate value function is built from a probabilistic representation. On a space with independent Brownian motions , let be a reflected drifted Brownian motion , let be a correlated one with local time , and let be a geometric Brownian motion. With the coefficients of (2.9) and (3.4),
for , and
For model parameters with and there is such that for every : (i) is a classical solution of the HJB equation (4.2) with the Neumann conditions and , with and ; (ii) for every admissible strategy and every ,
with equality for the feedback strategy , along a solution of the reflected feedback system (4.4). The threshold is asserted to exist, not fixed: the paper's formula (4.45) for it depends on and is not self-contained.
The theorem settles two questions about the relaxed tracking formulation: the optimal portfolio–consumption pair exists in feedback form, and the value function is a classical (not only viscosity) solution of an HJB equation with two Neumann boundary conditions. Together with the paper's Lemma 4.4, it shows that the expected discounted capital injection of the optimal strategy is finite, so the relaxed problem is well posed. The dual representation also gives the value in a separated form, three expectations of functionals of reflected Brownian motions, which is what makes the derivatives and the feedback explicit.
The result is proved in the paper; nothing here is open. No part of it is formalized. A formal proof would need Itô's formula for reflected processes, the smoothness of expectations of local-time functionals, and the duality argument; any of the milestones on its own is a self-contained target.
The last term of couples the reflected process with the local time of a second reflected process correlated with it through . Differentiating in directly fails: the local time is not differentiable in its starting point in any pathwise sense, and the correlation prevents conditioning one process on the other. The paper first treats the independent case (Lemmas 3.3–3.4), where the expectation factors through the law of , and then removes the correlation by a homogenization of the Neumann conditions (Proposition 3.5). A second difficulty is the verification step itself: the admissible class is unbounded and the state reflects at two boundaries, so the local martingale terms must be controlled by moment bounds that depend on the growth (4.7) of the feedback.
EthierKurtz.IsStandardBrownian), and every statement holds for every such space. The control problem lives on any filtered space satisfying the usual conditions with an -Brownian motion (published RankBasedSDI.LoadBalancing.UsualConditions, IsFBrownian).skorokhodReg), and as explicit exponentials. The only stochastic integral is , through the published EthierKurtz.HasBrownianItoIntegral with a continuous version required.lintegrals; statements about assert their finiteness. Stieltjes integrals use the Lebesgue–Stieltjes measure of the path. The objective is compared in the extended reals as , which agrees with whenever is defined and never produces ; is computed in so that for .ContDiffOn ℝ 2), the PDE on the open set the paper names, Neumann conditions pointwise on the faces; derivatives are taken within the closed coordinate domains. The suprema in (4.2) are least upper bounds (IsLUB), the consumption supremum over .The definitions of reflected processes, Stieltjes integrals against local times, and classical Neumann solutions are reusable beyond this mission. Proofs of any milestone, and of the deterministic facts (, , (3.9) solving (3.8)), are welcome.
Optimal control of partial differential equations under uncertainty arises whenever a physical system is steered by a control while its sources, coefficients or loads are only known in distribution. A typical requirement is a state constraint: the state (a temperature, a concentration, a displacement) must stay below a threshold everywhere in the domain. When the source term is random, demanding this for every realization is often impossible or too conservative, and the natural relaxation is a probabilistic (chance) constraint: the state must stay below the threshold uniformly on the domain with probability at least .
Probabilistic constraints are classical in operations research (Prékopa, Stochastic Programming, 1995), but in a PDE setting the constraint is an infinite family of random inequalities, one per point of the domain, and the probability function is not differentiable in general. C. Geiersbach and R. Henrion (arXiv:2306.03965v2, Math. Oper. Res. 2025) derive optimality conditions for such problems in terms of the Clarke subdifferential, building on the spherical-radial decomposition of Gaussian vectors developed by Hantoute, Henrion and Pérez-Aros (Math. Program. 2019) and van Ackooij and Henrion. This mission formalizes the PDE half of §2 of that paper: explicit formulas for the subdifferential of the probability function and the resulting optimality conditions.
Let , , be a nonempty, open, bounded set of class S: there are and with for all and . For the Dirichlet problem in , on has a unique weak solution in ; the solution operator is linear and continuous.
Fix and a threshold . The control-to-state operator is
The random vector on a probability space is Gaussian with positive definite, and is the random state. With and the probability function , the problem is
with convex and Fréchet differentiable and .
The analysis uses the spherical-radial decomposition. Let be the uniform distribution on the unit sphere , the chi distribution with degrees of freedom and density , the square root of . The radial probability function is and the radius function is the supremum of that set. For , is defined by , and
is the Clarke subdifferential, with identified with , and integrals of set-valued maps are Aumann integrals.
Assume a control with (41), and let be feasible with expected state satisfying on (42). If solves (24), there is with
and these conditions are sufficient when is a singleton for -a.e. with , or the set is bounded. The goal has no hard-coded constants; it asserts the form of the optimality system.
In attack order: well-posedness of the state equation with the bound (Lemma 1.2); measurability of the random state (Lemma 1.4); convexity and global Lipschitz continuity of (Lemma 2.9); moderate growth (Lemma 2.10); the Lipschitz and subdifferential conclusions of the general theory under (26) (Corollary 2.11); the optimality conditions (21), (22) for (24) (Corollary 2.12); when (Lemma 2.13); the explicit formula when (Lemma 2.14); and the upper estimate (40) of with its equality cases (Theorem 2.15).
The result turns an abstract statement — lies in a multiple of the Clarke subdifferential of a probability function that has no closed form — into a condition written in the problem data: Green-type functions , the expected state, and the radius function along each direction of the sphere. This is what makes the conditions usable for checking candidate controls and for designing algorithms, and Example 2.18 of the paper computes a solution this way. The sufficiency half identifies when the nonconvex chance-constrained problem behaves like a convex one.
The paper's proofs are on paper only; to our knowledge none of these results, nor the spherical-radial decomposition, Clarke calculus in Hilbert spaces, or Aumann integrals in , has a machine-checked proof. Formalizing Theorem 2.16 requires connecting elliptic regularity, Gaussian measure theory and nonsmooth analysis, and the milestones are reusable on their own: Lemma 1.2 is a regularity statement for the Poisson equation, and Lemmas 2.13 and 2.14 are max-function subdifferential formulas in an infinite-dimensional space.
The obvious route — differentiate and use a Lagrange multiplier — fails because is generally not differentiable even for smooth data (Example 2.17 of the paper), and because is only Lipschitz, being a maximum over . The general subdifferential estimate (Theorem 2.2, from Hantoute–Henrion–Pérez-Aros) needs a growth condition and only gives an inclusion, since the radial probability function is not Clarke regular; the radius function is an infimum over the open set where , which is neither compact nor independent of , so standard max-function formulas do not apply directly. Directions with require a separate limiting argument through the Mordukhovich subdifferential (Lemma 2.13). The regularity input, continuity of solutions on for class-S domains (Kinderlehrer–Stampacchia 1980), is not in Mathlib.
All declarations are in the namespace ChanceStateCtrl.PDE. and are EuclideanSpace ℝ (Fin d) and EuclideanSpace ℝ (Fin m), indices are Fin m, is Lp ℝ 2 (volume.restrict D). Weak derivatives are the published HunterPDE.Shared.HasWeakDeriv; a weak solution is a function continuous on , zero on , in with weak first derivatives in , satisfying the weak form against .
Standing hypotheses on every theorem: open, bounded and nonempty, , class S, and CompactSpace (closure D) (a consequence of boundedness). Nonemptiness of is the one added hypothesis: Lean's supremum over an empty domain is , not , and Lemma 2.9's identification of events fails for . is a continuous linear map to together with the hypothesis that it returns the weak solution; it is never an arbitrary operator. , as the uniform distribution on requires. is the positive semidefinite root; is its operator norm. The Clarke directional derivative is (the page's denominator is a misprint). takes values in . clco is the norm closure of the convex hull. The integral in (40)/(43) is over the restriction of to , not a renormalization. A solution is a global minimizer over ; the page's "solution to (9)" refers to this instance of the abstract problem (9).
Trivializing formalizations are ruled out: every Clarke subdifferential is taken at a point where the function is locally Lipschitz (proved in Corollary 2.11 and Theorem 2.15), the state operator is tied to the PDE, the multiplier carries its sign and complementarity, Aumann selections must be scalarly integrable, and optimality is global.
Needed infrastructure: elliptic regularity in for class-S domains; the spherical-radial decomposition of ; Clarke calculus (chain rule, max functions) on Hilbert spaces; Clarke's theorem on subdifferentials of integral functionals. Contributions of any of these as stand-alone theorems are welcome.