Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Large service systems such as call centers, hospital wards and cloud server pools have many parallel servers, finite buffers and customers who leave when they wait too long. Their performance is usually analysed through heavy-traffic diffusion limits: the number of customers in the system, centred and rescaled, converges as the system grows to a diffusion process whose law is computable. The quality-and-efficiency-driven (QED) regime of Halfin and Whitt (Oper. Res. 29, 1981) is the scaling in which the number of servers and the arrival rate grow together so that the probability of delay stays strictly between and . Garnett, Mandelbaum and Reiman (M&SOM 4, 2002) proved the QED limit for the Erlang-A model with unlimited waiting room. Whitt (Math. Oper. Res. 30, 2005) added finite waiting rooms of size of order , which produce a reflecting upper barrier in the limit.
Pang, Talreja and Whitt (Probab. Surveys 4, 2007) give a self-contained martingale proof of these limits. Theorem 1.2 of that paper, the target of this mission, covers the model with finite waiting room and abandonment. It contains the Erlang-B (loss) model () and finite-buffer Erlang-C models () as special cases.
Fix a service rate , an abandonment rate , a constant and a barrier . For , model is an queue: servers, a waiting room of places, Poisson arrivals of rate , exponential services of rate , first-come first-served service, and an exponential patience of rate for each waiting customer. An arrival that finds all places occupied is blocked and lost.
The number in system is constructed from independent rate-1 Poisson processes , , and an independent initial value by
where counts blocked arrivals. The QED scaling is
and the scaled process is .
The limit is a reflected diffusion: a pair of processes with right-continuous paths with left limits, , nondecreasing and nonnegative, a standard Brownian motion independent of , and
The regulator increases only when sits at .
If in , then in , where solves the reflected equation above with , and every solution with initial law has the same law:
The goal fixes no rate of convergence and no stationary quantity; it asserts the process limit and its characterization by (9)–(10).
The theorem supplies the diffusion approximation behind square-root staffing rules for systems with finite buffers: it says that buffers of order are visible in the limit as a barrier at , and that the limit for (Erlang-B with or without abandonment) is a reflected Ornstein–Uhlenbeck-type process. Stationary blocking and delay probabilities of the limit then approximate those of the large finite system.
The result is proved in the literature (Whitt 2005; Pang, Talreja and Whitt 2007, whose proof of Theorem 1.2 is a sketch built on §7.1). It is not formalized anywhere. A formal proof would supply a checked martingale representation for a birth–death queue with blocking, a checked reflection map with state-dependent drift, and the continuous-mapping step through it. The unlimited-waiting-room case is posed separately on the platform as the Erlang-A limit of Garnett, Mandelbaum and Reiman and is not part of this mission.
The obvious route is the one used for the Erlang-A model: write as a continuous function of the scaled Poisson noise and apply the continuous-mapping theorem. With a finite waiting room this fails as stated, because the blocking process is not a function of the noise alone. It depends on the path of through the times the system is full. The proof must instead identify as the image of the noise under a reflection map with a drift inside it, prove that this map is well defined and continuous, and control the martingale terms through random time changes whose limits are deterministic. The barrier in model is , not , so the continuous-mapping step has to handle a moving barrier as well.
BellWilliams2001.ThresholdPolicy.IsCadlag. Brownian motion is ErlangA.Diffusion.IsStandardBM, indexed by ; martingales are Mathlib Martingales indexed by .ManyServerQED.Scheduling.IsPoissonProcess. is independent of the primitives and for all . Blocked arrivals are counted with the left limit , correcting (114) as printed. and are allowed.BellWilliams2001.ThresholdPolicy.CouplingConverges (Skorohod coupling with almost sure uniform convergence on compacts), equivalent to weak convergence for a continuous limit. Uniform distances use supDist on .ErlangA.Diffusion.drift; is independent of ; and are adapted to the filtration of and ; condition (10) is "the Lebesgue–Stieltjes measure of , extended by to negative times, gives zero mass to ". Uniqueness is uniqueness in law of . The limit space lives in Type.Contributions welcome: Stieltjes-integral and counting-process lemmas for , a reflection map with Lipschitz drift on , the Poisson functional central limit theorem, and martingale facts for randomly time-changed Poisson processes. The last three are reusable well beyond this mission.
The Kurdyka–Łojasiewicz (KL) inequality is the analytic engine behind most global convergence proofs for descent methods on nonconvex problems: proximal point and proximal gradient schemes, alternating minimization, ADMM variants and subgradient flows all reach a critical point with finite trajectory length once the objective satisfies a KL inequality. Its origin is Łojasiewicz's gradient inequality for real-analytic functions ([Łojasiewicz, 1963]); Kurdyka extended it to differentiable functions definable in an o-minimal structure, with a reparametrization ψ of the values, on bounded sets (Kurdyka, Ann. Inst. Fourier 48 (1998)).
Optimization objectives are rarely smooth or finite everywhere: indicator functions of constraint sets, ℓ₁ penalties, rank functions and maxima take the value +∞ or have kinks. Bolte, Daniilidis, Lewis and Shiota (SIAM J. Optim. 18(2) (2007), 556–572) proved that every lower semicontinuous function definable in an o-minimal structure satisfies a KL inequality for Clarke subgradients, globally in space. This mission formalizes that result (Theorem 14) and the chain of statements in §4 of the paper on which its proof rests.
Timeline. Łojasiewicz (1963): gradient inequality for real-analytic functions near a critical point. Kurdyka (1998): the inequality ‖∇(ψ∘f)‖ ≥ 1 for C¹ definable functions on bounded sets. Bolte, Daniilidis and Lewis (SIAM J. Optim. 17(4) (2007)): nonsmooth Łojasiewicz inequality for lower semicontinuous subanalytic functions with the limiting subdifferential. Bolte, Daniilidis, Lewis and Shiota (2007): this paper, for definable functions, Clarke subgradients, and unbounded sets.
Write ℝⁿ for Euclidean space with norm ‖·‖ and inner product ⟨·,·⟩, and let f : ℝⁿ → ℝ ∪ {+∞} be lower semicontinuous, with domain dom f = {x : f(x) < +∞} and graph Graph f = {(x, f(x)) : x ∈ dom f} ⊆ ℝⁿ⁺¹. Π : ℝⁿ⁺¹ → ℝⁿ forgets the last coordinate.
Subdifferentials. A vector x* is a Fréchet subgradient of f at x ∈ dom f if liminf_{y→x, y≠x} [f(y) − f(x) − ⟨x*, y − x⟩]/‖y − x‖ ≥ 0. The limiting subdifferential ∂f(x) collects the limits of Fréchet subgradients x_k at points x_k → x with f(x_k) → f(x); the singular subdifferential ∂^∞f(x) collects the limits of t_k x_k with t_k ↘ 0⁺. The Clarke subdifferential is
with the closed convex hull. It may be empty even on dom f, for example for −‖x‖^{1/2} at 0.
O-minimal structures. An o-minimal structure 𝒪 on (ℝ, +, ·) is a sequence of Boolean algebras 𝒪ₙ of subsets of ℝⁿ (the definable sets) that is stable under A ↦ A × ℝ, A ↦ ℝ × A and the projection Π, contains every algebraic set {p = 0}, and whose one-dimensional sets are exactly the finite unions of intervals and points. Semialgebraic sets, the globally subanalytic sets and the sets definable with the exponential each form such a structure. A function is definable if its graph is.
Stratifications. A C^p stratification of a set X is a locally finite partition of X into C^p submanifolds (strata) such that a stratum meeting the closure of another lies in its frontier. It is Whitney-(a) if tangent spaces T_{x_k}X_i converging to 𝒯 along x_k → x ∈ X_j satisfy T_xX_j ⊆ 𝒯, and a stratification of a set in ℝⁿ⁺¹ is nonvertical if e_{n+1} is tangent to no stratum. For x in a stratum X_i, ∇_R f(x) is the Riemannian gradient of f restricted to X_i.
For every lower semicontinuous definable f there are ρ > 0, a strictly increasing continuous definable ψ : [0, ρ) → ℝ, C¹ on (0, ρ) with ψ(0) = 0, and a continuous definable χ : ℝ₊ → (0, ρ) such that
Neither ρ, ψ nor χ is fixed: the goal asserts only their existence, so it is independent of any choice of exponent.
Corollary 9 (ii)–(iii) (finitely many Clarke critical and asymptotic critical values) and Corollary 12 (the KL inequality around the zero set) are included as further statements.
The result. Theorem 14 makes the KL property available, with no further verification, for every lower semicontinuous objective built from semialgebraic, globally subanalytic or exp-definable pieces. Global convergence theorems for proximal alternating minimization, proximal gradient methods, PALM and nonconvex ADMM take a KL inequality as hypothesis; definability is how that hypothesis is checked in applications. The inequality is relative to the value 0, holds globally through χ(‖x‖), and controls every Clarke subgradient rather than only the one of least norm. Corollary 9 is a definable, nonsmooth Morse–Sard theorem.
Formalizing it. The theorem has been proved since 2007; it has not been formalized. Lean's Mathlib has no o-minimal geometry: no cell decomposition, monotonicity theorem, definable choice or Whitney stratification. A complete development of this mission would supply the first machine-checked KL inequality for a general class of nonsmooth functions, and the o-minimal infrastructure it needs is reusable for every result in optimization and real algebraic geometry that cites "tame" functions.
The statements are short; the proofs rest on geometry absent from Lean. Lemma 8 is proved in the paper by citation of a stratification theorem for definable maps ([Shiota, Geometry of Subanalytic and Semialgebraic Sets, 1997, II.1.17]). Proposition 10 and Theorem 11 use the monotonicity lemma for definable functions of one variable and definable selection. The natural first idea — apply Kurdyka's inequality on each stratum and take a minimum — fails twice: Kurdyka's inequality is local on bounded sets, and the reparametrizations ψ_i of different strata must be compared near 0, which needs the monotonicity lemma once more. Passing from the strata to Clarke subgradients needs the projection formula of Corollary 9, which in turn depends on nonverticality and the Whitney-(a) condition.
ℝⁿ is EuclideanSpace ℝ (Fin n); ℝ ∪ {+∞} is EReal, with f never equal to ⊥ as a standing hypothesis; ℝⁿ⁺¹ carries the value in the last coordinate. The Fréchet and limiting subdifferentials are the published NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff. The Clarke subdifferential uses closedConvexHull. An o-minimal structure is a structure with a family O n of sets of subsets of ℝⁿ satisfying Definition 6 (Boolean algebra as: ∅, complements, binary unions; one-dimensional sets as finite unions of order-connected sets). Definability of ψ, χ and of the strata is part of every conclusion that asserts it. Tangent spaces are spans of Mathlib's tangentConeAt; C^p submanifolds are local graphs; the Riemannian gradient on a set U is a vector g in the tangent space with HasFDerivWithinAt h ⟪g, ·⟫ U x.
Inequality (22) is stated as ψ′(|f(x)|)·‖x*‖ ≥ 1, never as 1/ψ′ ≤ ‖x*‖, so that ψ′ = 0 cannot make it hold through 1/0 = 0. The goal mentions no strata, no auxiliary functions of the proof and no Clarke critical points; a formalization that adds such hypotheses, drops definability of ψ and χ, or restricts to bounded sets is a different theorem.
Welcome contributions: the elementary closure properties of o-minimal structures (definability of sums, compositions, images), the monotonicity theorem for definable functions of one variable, definable choice, cell decomposition and Whitney stratification — all reusable well beyond this mission.
Network revenue management decides, over a finite selling horizon, which products to offer to arriving customers when the products share limited resources: seats on flight legs, hotel room-nights, rental capacity. The exact dynamic program is intractable for realistic networks, so practice relies on heuristics built from a deterministic linear program (DLP), the fluid relaxation that replaces random demand by its mean. Its value is an upper bound on the revenue of every policy, and the quality of a heuristic is measured by its revenue loss against it.
For the fluid-based heuristics, the loss grows with the size of the system: a static policy derived from one DLP solution loses order when capacities and demand rates are both scaled by (Gallego and van Ryzin, 1997; Talluri and van Ryzin, 1998). Re-solving the DLP during the horizon is common practice, but for a long time it was unclear whether re-solving helps asymptotically; Cooper (2002) showed that naive re-solving can even hurt. Jasin and Kumar (Math. Oper. Res. 37(2), 2012, doi:10.1287/moor.1120.0537) proved that a re-solving heuristic with probabilistic allocation control (PAC) has a loss bounded by a constant independent of , in a model that also covers customer choice through random resource consumption. Later work (Bumpensanti and Wang, 2020, arXiv:1802.06192) removed the nondegeneracy assumption with a different re-solving rule.
The horizon is . Customer types arrive as independent Poisson processes of rates . Each of the offers belongs to one type ; iff , and . Presenting offer consumes a random vector of the resources, i.i.d. across presentations, and earns revenue , with ; models a customer who buys nothing. Resource starts with capacity , and bounds every . Write and . The DLP is
Assumption 2.1 requires to be nondegenerate with a unique optimal solution ; Assumption 2.2 requires that every optimum of the LP without capacity constraints violates .
PAC re-solves at times . At it solves with the remaining capacity, obtaining ; until it picks offer for an arriving type- customer with probability and presents it only if the remaining capacity is at least on every resource. In the -th system capacities are and rates ; is the DLP value and the revenue of PAC. Mid-point PAC re-solves at , , with the smallest integer such that : about re-solves.
There is , independent of , such that mid-point PAC satisfies
The goal fixes no constant: it asserts only that the loss is bounded uniformly in .
The result shows that re-solves suffice for a loss that does not grow with the size of the system, against an upper bound that is valid for every policy; so PAC is within a constant of the optimal policy, and the DLP bound, the optimal value and PAC are asymptotically equivalent to order . Theorem 5.3 makes the trade-off between re-solving frequency and loss explicit for any schedule, and Corollary 5.1 guarantees that re-solving in this form never worsens the static bound.
The result is proved on paper. No part of it is formalized: the mission produces a machine-checked model of a Poisson network with random consumption and a re-solving policy, a statement of LP perturbation theory for nondegenerate programs, and compound-Poisson moment bounds, each reusable for other re-solving and fluid-approximation results in revenue management.
The obvious argument compares PAC with its fluid path and bounds the deviation of the remaining capacity by a martingale estimate over the whole horizon. That gives only : deviations late in the horizon cannot be corrected. A constant bound needs re-solving to correct earlier deviations, which in turn needs the re-solved DLP solution to depend linearly and stably on the capacity deviation (the perturbation analysis of App. B) and a hitting-time estimate for when that linear regime fails. The capacity check and the coupling between the re-solved solutions and the random consumption make the process non-Markovian in the obvious state variables.
Types are Fin NT, offers Fin n, resources Fin m. The model is a structure holding , , , the consumption laws (measures on ), and the revenue functions. Standing readings (IsValid): and ; each is a probability measure with almost surely (the page has on p. 317 and on p. 327; the weaker one is used); revenue functions are measurable, vanish at , and are nonnegative and bounded by a common constant (implicit on the page). is a reading fixed by App. A.1.
is a backward recursion over the windows between re-solves. Each window holds a Poisson number of arrivals with i.i.d. types (superposition and marking), and the expected value is computed arrival by arrival with the capacity check on every resource. PAC is quantified over every DLP selector that returns an optimal solution and is measurable in the capacity, since the page leaves ties open after time 0. All constants are chosen after the instance and before , the selector, the schedule, and . Nondegeneracy follows Bertsimas–Tsitsiklis: every basic feasible solution has exactly active constraints.
Disclosed deviations from the page:
A formalization in which PAC does not check capacity, or stops checking after a hitting time, earns exactly and would make the goal trivial; the model here applies the check at every arrival. A constant chosen after would also be trivial, since the loss is at most times the revenue bound.
The source is the published Math. Oper. Res. version; printed page = PDF page + 311. Sample-path lemmas (B.2–B.4, C.1–C.3) are not stated. Contributions are welcome on the LP perturbation lemma, the compound-Poisson moment bound and the measurability of the PAC recursion, each of which stands alone.
First-order methods for nonsmooth, nonconvex optimization (proximal algorithms, alternating minimization, subgradient-type descent) are analysed through generalized derivatives. Convergence and complexity arguments need a lower bound on the size of those derivatives away from critical points. For the Clarke subdifferential of a general lower semicontinuous function no such bound is available: Clarke subgradients can be small, or even zero, at points where the function decreases steeply along a smooth piece of its domain.
Bolte, Daniilidis, Lewis and Shiota (SIAM J. Optim. 18(2), 2007) showed that the obstruction disappears for functions whose graph admits a Whitney stratification, a partition into smooth manifolds that fit together regularly. Semialgebraic functions, and more generally functions definable in an o-minimal structure, have such stratifications. For these functions every Clarke subgradient is at least as long as the gradient of the function along the stratum through the point. This projection formula is the step from the geometry of the graph to the nonsmooth Kurdyka–Łojasiewicz inequality of the same paper, which underlies the convergence theory of many splitting methods (Attouch–Bolte–Svaiter 2013; Bolte–Sabach–Teboulle 2014).
This mission covers §2–§3 of the paper: the definitions, the projection formula (Proposition 4) and its Corollary 5 (i). The Kurdyka–Łojasiewicz part (§4) is a separate mission of the same series.
Let be lower semicontinuous, with domain and graph .
A stratification of a nonempty set is a locally finite partition of into submanifolds (the strata) such that implies for . It has the Whitney-(a) property if, whenever converge to () and the tangent spaces converge to a subspace , then ; subspaces converge in the gap . A Whitney stratification is a stratification with this property.
A stratification of is nonvertical if for every and (condition (H)). Let drop the last coordinate. For let be the stratum containing and . Nonverticality makes the tangent space of the graph of a linear form over ; the vector representing it is the stratum gradient , characterized by .
For lower semicontinuous whose graph admits a nonvertical Whitney stratification, and every ,
Further items state that the stratum gradient exists and is unique under (H), the equality when (Remark 4), the chain of (7), nonverticality for locally Lipschitz functions (Remark 3), and the nonsmooth Morse–Sard theorem of Corollary 5 (ii).
The inequality (14) says that Clarke critical points of a stratifiable function are critical points of its restriction to a stratum, and that the Clarke subdifferential is never shorter than the smooth gradient along the stratum. Two consequences are drawn in the paper. With countably many strata and the classical Morse–Sard theorem it gives a nonsmooth Morse–Sard theorem: the set of Clarke critical values has measure zero (Corollary 5 (ii)). Combined with the o-minimal Łojasiewicz inequality for the restrictions it gives the nonsmooth Kurdyka–Łojasiewicz inequality for definable lower semicontinuous functions (§4), the hypothesis behind global convergence results for proximal and splitting algorithms on semialgebraic problems.
All results of this mission are proved in the paper. None has a machine-checked proof that we know of: Mathlib has the tangent cone, Fréchet differentiability and orthogonal projections, but no stratifications, no singular or Clarke subdifferential of an extended-valued function, and no projection formula. The work is to formalize the paper's proof, which reduces the projection formula to the behaviour of Fréchet normals under limits of tangent spaces.
The first step, (11), is local and smooth: along a curve in the stratum the function is differentiable, and a Fréchet subgradient must agree with the derivative in tangent directions. The difficulty is the passage to limits in (12). A limiting subgradient at is a limit of Fréchet subgradients at points which may lie in a different, higher-dimensional stratum ; nothing in the smooth argument relates to . The relation is supplied exactly by the Whitney-(a) property, together with the compactness of the Grassmannian and the local finiteness of the stratification. Without Whitney-(a) the inclusions fail, so a proof that never uses it is wrong. The singular part requires the same argument for rescaled subgradients , whose normals become horizontal in the limit.
is EuclideanSpace ℝ (Fin n), is EuclideanSpace ℝ (Fin (n+1)) with the function value as the last coordinate, and is EReal with never . The Fréchet and limiting subdifferentials are the published NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff; the tangent space (span of the tangent cone) and submanifolds (coordinate slices of some dimension) are the published ProjLikeRetr.Retractor definitions. The closed convex hull in (6) is closedConvexHull, not convexHull. Strata may be empty; local finiteness is required at points of the stratified set; a gap supremum over an empty unit sphere is . The stratification hypothesis is taken of class , the weakest case of the paper's "-Whitney".
The stratum gradient is defined intrinsically: with . It is not defined as a derivative of along the whole projected set . That set can fail to be a submanifold for a discontinuous lower semicontinuous , and every statement would then hold vacuously at such points. A companion item proves existence and uniqueness of the stratum gradient under (H), so the goal is not vacuous. The goal quantifies over all elements of ; this set may be empty (Remark 4), which is the page's restriction to , and no real-valued distance to is used.
A complete development needs the tangent space of a submanifold as the image of the chart derivative, convergence of subspaces and compactness of the Grassmannian of , Fréchet normals to epigraphs, and the density of in for lower semicontinuous . These pieces are reusable beyond this mission; the subspace gap and Whitney stratifications are prerequisites of the §4 mission. Contributions of any of the listed lemmas are welcome, as are proofs of the companion items.
Nonlinear semidefinite programming asks to minimize a smooth function subject to smooth equality constraints and a constraint that a smooth matrix-valued function be positive semidefinite. It covers robust control design, structural optimization, and nonconvex matrix problems such as low-rank approximation and nearest-correlation-matrix problems. Algorithms for it (sequential quadratic programming, augmented Lagrangian and semismooth Newton methods) converge fast locally only when the Karush–Kuhn–Tucker (KKT) point they approach is stable under perturbation, and the question is which checkable conditions guarantee that stability.
For classical nonlinear programming the answer has been known since the 1980s: at a local minimizer, Robinson's strong second order sufficient condition together with linear independence of the active gradients is equivalent to strong regularity of the KKT point (Robinson 1980; Jongen et al. 1987; Kojima 1980). D. Sun extended this equivalence to nonlinear semidefinite programs, where the constraint cone is not polyhedral and second-order analysis carries an extra curvature term.
Timeline.
is a finite-dimensional real inner-product space, is Euclidean space, and is the space of real symmetric matrices with the Frobenius inner product . is the cone of positive semidefinite matrices. The problem is
with , , twice continuously differentiable. Write and . The Lagrangian is , and the multiplier set consists of the with , and in the normal cone (so and ). A triple with is a KKT point.
For a closed set , is the tangent cone and its lineality space. Robinson's constraint qualification at is ; constraint nondegeneracy replaces by . The critical cone is .
For with Moore–Penrose pseudo-inverse , set . Let be the metric projector, , and with . Then and . The strong second order sufficient condition (SSOSC) at is
The KKT map is on ; its zeros are the KKT points. The KKT system is also the generalized equation with and . A solution is strongly regular if, for all small , the linearized equation has a unique solution near that depends Lipschitz-continuously on . Clarke's generalized Jacobian is the convex hull of the B-subdifferential , the set of limits of Jacobians at nearby differentiability points. is the directional derivative. The uniform second order growth condition and strong stability quantify over all -smooth parameterizations of the problem.
At a local minimizer satisfying Robinson's CQ, with , the following are equivalent:
The matrix analysis of : Lemma 1 (a B-subdifferential chain rule), Lemma 2, Propositions 3 and 4 (the block structure of and ), and Proposition 7 (the inequality ). Second-order theory: Proposition 8 (the strict CQ gives a unique multiplier and ), Theorem 10 (the classical second-order conditions with the sigma term) and Lemma 11 ( equals the sigma term on ). The equivalences: Remark 15 (strong regularity iff a natural map is a Lipschitz homeomorphism), Proposition 16 ((a) ⇒ (b) ⇒ (c) at any KKT point), Lemma 18 (uniform growth ⇒ SSOSC) and Lemma 20 ().
The theorem identifies the SSOSC, a condition that can be checked from the problem data, with the stability notions that local algorithms need. Strong regularity is the hypothesis under which Newton-type methods for the KKT system converge locally and solutions vary Lipschitz-continuously with the data. Nonsingularity of gives quadratic convergence of semismooth Newton methods. Uniform growth and strong stability are what sensitivity analysis uses. Without the theorem, each of these properties has to be verified separately for semidefinite programs. The theorem also shows that the classical nonlinear programming equivalence survives on a non-polyhedral cone if the curvature term is added.
The result is proved in the literature but has no machine-checked proof. Formalizing it requires the B-subdifferential and Clarke Jacobian of the PSD projector, second order tangent sets of , and the Robinson–Kummer characterization of strong regularity. None of these exists in Mathlib. Items (g) and (i), which use the topological degree, are not formalized.
The obvious route is to copy the nonlinear programming proof: write strong regularity as nonsingularity of a reduced Jacobian on the active constraints. This fails because is not polyhedral. The KKT map is only semismooth, and its generalized Jacobian at a non-strictly complementary point is a whole family of operators, parametrized by . Nonsingularity has to be shown for every member of that family. The curvature of the cone appears only through , which links the second-order condition to the Jacobian family. The converse directions combine several external theorems (Bonnans–Shapiro's stability theory, Clarke's inverse function theorem, Kummer's characterization), each needing nonsmooth infrastructure.
All objects are defined in SunNLSDP.Equiv.Setting. is the subspace of symmetric vectors in EuclideanSpace ℝ (n × n) for a finite index type n, so its inner product is exactly the Frobenius product. and are WithLp 2 products, carrying the sum of the inner products. is computed by the continuous functional calculus. The metric projector returns its argument when no minimiser exists; it is applied only to nonempty closed convex sets. Clarke's Jacobian, , the one-sided directional derivative, the normal cone and the lineality space are the published definitions NonsmoothNewton.Shared.clarkeJac, NonsmoothNewton.Local.dirDeriv and RobinsonSR.Reduction.Setting.
Conventions committed to:
Items (g) and (i) of Theorem 21 are omitted, because Brouwer degree is unavailable; no surrogate for the index is substituted. A formalization that reads the CQs or nondegeneracy as two decoupled equations, or states SSOSC only on instead of , proves a different theorem and is ruled out.
Reusable infrastructure: the PSD projector and its generalized Jacobians, second order tangent sets, the Moore–Penrose pseudo-inverse of symmetric matrices, and the characterization of strong regularity by Lipschitz homeomorphisms. Proofs of individual milestones are welcome, as are lemmas on and on strong regularity of generalized equations.
A linear multistage stochastic program chooses decisions over stages while a random vector is revealed one piece at a time; each decision may depend only on what has been observed so far. Such programs model production planning, capacity expansion, hydro scheduling and portfolio problems. Computing their optimal value exactly is intractable in general: Shapiro and Nemirovski argue that even medium-accuracy solutions are out of reach when the number of stages grows (Shapiro–Nemirovski 2005), and already the one-stage problem is #P-hard (Dyer–Stougie 2006, Theorem 3.2, as cited by the paper).
Linear decision rules restrict every decision to be an affine function of the observations. Introduced for robust optimization by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004) and carried into stochastic programming by Shapiro and Nemirovski and by Chen, Sim, Sun and Zhang (2008), they turn the problem into a finite one whose optimal value is an upper bound. Kuhn, Wiesemann and Georghiou (Optimization Online 2009/02/2218; Math. Program. 130, 2011) apply the same restriction to the dual problem, which yields a lower bound. They show that, for polyhedral supports, both bounds are values of explicit linear programs. This mission formalizes the multistage version of that statement, Theorem 3 of the preprint.
Stages are . The uncertainty is with and ; by convention and . The history at stage is , , and the truncation operator maps to . The law of has support , a nonempty bounded polyhedron spanning , whose first two constraints encode . denotes conditional expectation given , and is the second-order moment matrix.
A stage- decision is a square-integrable Borel function of (written ). The program minimizes
with deterministic matrices , and . The linear conditional mean assumption requires almost surely for some ; it holds, for example, for stagewise independent data.
The primal approximation sets and slacks . The dual approximation keeps general rules but imposes the slack equations only in the weak form . The linear programs (4.2) and (4.6) are written in the matrices , multipliers and slack matrices , with .
Under the standing assumptions, the linear conditional mean assumption, and strict feasibility of ,
as extended-real optimal values. Both equalities are part of the goal.
The theorem makes both linear-decision-rule bounds on a multistage stochastic program computable by linear programming, with size polynomial in , , and and hence typically linear in the number of stages. The gap between the two values measures the suboptimality of the primal linear rule. These results underlie later work on piecewise-linear and lifted decision rules and on multistage robust and distributionally robust optimization.
The preprint omits the proof of Theorem 3 ("it widely parallels the argumentation in Section 2"), so a formal proof has to supply the multistage details: the conditional-expectation bookkeeping, the truncation operators and the transfer of the one-stage cone description to non-anticipative slacks. No part of this paper has been machine-checked before; the companion mission of this series formalizes the one-stage Theorem 1.
The obvious route repeats the one-stage argument stage by stage, and it breaks at the slack constraints of . A slack must be a function of alone, while the one-stage cone characterization of moment vectors concerns functions of the full ; Lemma 3 bridges them only through the linear conditional mean assumption and conditional expectations. A second difficulty is the closure gap between that cone and its polyhedral outer description: the equality of and relies on strict feasibility, and a proof that ignores it is wrong. On the primal side, the passage from almost sure constraints to identities of matrices needs both that every point of is charged by and that spans .
Vectors are functions Fin d → ℝ; stage is the Fin T index and coordinate is index 0. The history dimension is kbar kk t, the truncation is the restriction to the first coordinates, and is also given as a matrix. is Mathlib's condExp with respect to the σ-algebra generated by . " is the support of " means: closed, , and every ball around a point of has positive mass. Decision rules are Borel functions of the history whose composition with is in . Optimal values are infima in EReal ( if infeasible, if unbounded), and "equivalent" means equal optimal values. The matrices are data, with the conditional-mean identity as a hypothesis.
Three conventions are fixed where the page is silent or misprinted. Strict feasibility of , not defined in §4, is the analogue of (2.9) for the standard form (4.1): slacks at least almost surely. The equality constraint of is printed with inside ; the formalization follows (4.7), where the sum covers only . The sign condition in (4.5c) is printed as for a function of , and is read as . The theorem's last sentence (polynomial size, efficient solvability) is informal and not formalized. One hypothesis is added: the goal's second equality assumes or that some row of (the rows of below (2.1b)) is nonzero (the first equality is stated without it). For the support is the single point , and if has no nonzero row beyond (2.1b) the cone of Proposition 3 is all of ; the printed second equality then fails (a strictly feasible one-stage instance has while (4.6) is unbounded below). The added hypothesis excludes exactly this case.
Expectations are Bochner integrals, which vanish on non-integrable functions; under the standing assumptions is bounded almost surely, so all integrands involving square-integrable rules are integrable and no constraint is satisfied vacuously. Matrix.inv returns on singular matrices, but is positive definite under the standing assumptions. The linear conditional mean hypothesis cannot be dropped from Lemmas 2 and 3: without it need not exist.
A complete development needs the support and moment facts of §2 (, almost sure constraints extend to ), Farkas-type duality for the polyhedron , the tower property of conditional expectation, and the cone results of Propositions 3 and 4 of the preprint. These are reusable across the series. Proofs of the milestones, or of these supporting facts as separate lemmas, are welcome.
Linear stochastic programs with recourse model decisions that are taken after an uncertain parameter has been observed: the decision is a decision rule , a function of the data. Computing the optimal value exactly is intractable in general. Dyer and Stougie showed that already two-stage linear stochastic programs are #P-hard (Math. Program. 2006), and the same holds for the one-stage problem below even when is uniform on a cube.
A widely used remedy restricts decision rules to be linear in . Ben-Tal, Goryashko, Guslitzer and Nemirovski introduced this restriction in robust optimization (Math. Program. 2004); Shapiro and Nemirovski (2005) and Chen, Sim, Sun and Zhang (Oper. Res. 2008) carried it into stochastic programming. The restriction yields an upper bound, but on its own it says nothing about how much optimality is lost. Kuhn, Wiesemann and Georghiou (Optimization Online 2009/02/2218; published in Math. Program. 2011) also apply the linear restriction to the dual multipliers. This gives a lower bound, so the gap between the two computable bounds estimates the approximation error. This mission formalizes the paper's model result for the case of fixed recourse and polyhedral support (§2, Theorem 1).
Uncertainty is a probability measure on . The support of is the smallest closed set of probability one. A decision rule is an element of , the Borel measurable, square-integrable functions . Inequalities between vectors and matrices are componentwise.
The data are a fixed recourse matrix , matrices and giving the costs and right-hand sides , and , . The stochastic program is
The standing assumptions of §2 are:
The second-order moment matrix is . is strictly feasible (2.9) if some , and satisfy and almost surely.
The two approximations are as follows.
Under the standing assumptions, (see Formalization scope) and strict feasibility,
where (2.3) and (2.8) are the linear programs
Because , Theorem 1 brackets the value of an intractable stochastic program between two explicit linear programs. The sizes of these programs are polynomial in . They depend on only through its support and its second-order moment matrix. The difference is therefore a computable certificate of how much the linear-decision-rule restriction can lose. Sections 3 and 4 of the paper extend the same scheme to random recourse (semidefinite programs) and to multistage problems; they are the subjects of the companion missions 2 and 3.
The theorem is proved in the paper. As far as a search of the platform shows, none of the statements above has a machine-checked proof. A formal proof would check the measure-theoretic steps that the paper passes over quickly. These are the passage from "almost surely" to "on the support", the density argument behind , and the approximation argument of Proposition 4. A formal proof would also produce reusable results on robust counterparts of polyhedral constraints and on moment cones.
The primal half is robust-optimization duality. Its only delicate point is that almost-sure constraints become constraints on all of , which uses the fact that every point of the support is charged. The dual half is harder. The constraint " has rows in " is a family of moment problems over nonnegative square-integrable densities, and is in general not closed. Replacing it by the polyhedral cone is exact only up to the boundary, and it is strict feasibility that removes the boundary effect. Without strict feasibility the optimal values of (2.6) and (2.8) are only known to bracket each other. The proof of Proposition 3 also needs a description of the closed cone generated by , and this description uses (2.1b).
Vectors in are Fin k → ℝ and matrices are Matrix (Fin m) (Fin k) ℝ. The paper's 1-based indices are 0-based in Lean, so is index 0 and the rows of (2.1b) are rows 0 and 1. The data form a structure Setting, and the standing assumptions form one predicate Standing. The support is encoded by three conditions on : it is closed, , and every ball centred in has positive mass. This is equivalent to "smallest closed set of probability one"; alone would not be enough. Decision rules are measurable functions with MemLp x 2 P. Expectations of vector- and matrix-valued quantities are written entrywise as Bochner integrals. Under the standing assumptions is bounded almost surely, so every integrand involved is integrable and no integral defaults to .
"Equivalent" means equal optimal values. Each optimal value is the infimum of the objective over the feasible set in EReal: if the problem is infeasible and if it is unbounded below. A one-sided inequality between the values, or the bare statement that the problems are linear programs, is not Theorem 1 and does not close the goal. Strict feasibility is a hypothesis of both equalities, as printed. Proposition 1 is stated for any with a nonempty polyhedron, since nonemptiness is the only property of it uses. Proposition 3, Proposition 4 and Theorem 1 carry one hypothesis the paper does not state, (some row of below the first two is nonzero). The printed statements are false without it: for , , , every assumption holds, , so while , and (2.8) loses the sign constraint that (2.6) keeps. Under the standing assumptions the hypothesis is automatic whenever . Theorem 1's closing sentence ("the sizes of these linear programs are polynomial … efficiently solvable") is informal and is not formalized.
A complete development needs strong LP duality or Farkas' lemma for inequality systems, the support of a measure in , density of -densities in nonnegative measures, and basic facts on interiors of polyhedral cones. The Farkas lemma is on the platform (LinearOptimization.farkas_lemma). Proofs of the milestones are welcome independently. Proposition 1 and Proposition 3 are reusable outside this paper.
Risk measures quantify the danger of an uncertain cost by a single number. The axiomatic theory of coherent and convex risk measures (Artzner, Delbaen, Eber and Heath, Coherent measures of risk, 1999; Föllmer and Schied, Convex measures of risk and trading constraints, 2002) is static: the risk is evaluated once, with no information beyond what is known at time zero. Multistage stochastic optimization and dynamic risk management need risk evaluated conditionally: at time 1 part of the uncertainty has been resolved, and the risk of a time-2 cost should be a function of what is known at time 1.
Ruszczyński and Shapiro, in Conditional risk mappings (preprint of February 21, 2004; journal version Mathematics of Operations Research 31(3), 2006), extend their earlier static theory (Optimization of convex risk functions, Math. Oper. Res. 31(3), 2006) to this conditional setting. They define conditional risk mappings by three axioms, derive a pointwise conjugate duality, and show that positively homogeneous conditional risk mappings are, under regularity conditions, suprema of countably many conditional expectations. The last result explains the word conditional: the conditional expectation is the prototype, and every positively homogeneous conditional risk mapping is a worst case over a countable family of them.
Let be a set with -algebras ; is the information available when risk is evaluated. Let be a real vector space of -measurable functions , and a subspace of -measurable ones. Let be a real vector space of finite signed measures on with , and pair them by
Both spaces carry locally convex topologies that are compatible with this pairing: the continuous linear functionals on each space are exactly the pairings with elements of the other. Two standing conditions hold throughout: (C) if is not a nonnegative measure, some nonnegative has ; (C′) for every .
A conditional risk mapping is a map with, writing :
Costs are minimised: smaller is better. All inequalities hold at every , not almost surely. is positively homogeneous if for , and lower semicontinuous if each is.
The conjugate is and the risk envelope is . denotes the probability measures in , and those with for all . A map is weakly* -measurable if every is -measurable. For such a selection of , the operator acts on . Assumption (K): is compact, and every such maps into itself with a closed graph. Finally, is the conditional probability of given if each is -measurable and for , ; then .
If is separable, (K) holds and is a positively homogeneous, lower semicontinuous conditional risk mapping, then there are probability measures , , with
each conditional expectation being the integral against a weakly* -measurable conditional probability of .
Corollary 1 (p. 10, singleton envelopes give a conditional expectation) and Proposition 2 (p. 7, for nonnegative -step functions ) are included as further statements.
Theorem 2 identifies the positively homogeneous conditional risk mappings with suprema of conditional expectations. It is the conditional analogue of the representation of a coherent risk measure as a worst-case expectation over a set of probability measures. It shows that the axioms (A1)–(A3), stated at every , are the right abstraction of "conditional": nothing beyond conditional expectations and a supremum is needed to generate them. Theorem 1, the pointwise duality on which it rests, is what makes conditional risk mappings usable in multistage problems. Its envelope form (3.8) is what the paper's composition results and dynamic programming equations in §5–§7 manipulate.
The results are proved in the paper, partly by reference: the duality of Theorem 1 by applying the authors' earlier unconditional theorem "verbatim" at each , Lemma 1 through a measurable-selection theorem, and Theorem 2 through Kakutani's fixed-point theorem. None of them is formalized. A formalization would check these deferred steps. In particular the passage, in the proof of Lemma 1, from a dense subset of to all of uses only lower semicontinuity of , and whether that suffices in every separable paired space is open to scrutiny.
Theorem 1 needs the Fenchel–Moreau theorem in a general locally convex space, paired through integrals against signed measures. Mathlib's convex duality is mostly finite-dimensional or normed, and the extended-real bookkeeping of conjugates is delicate. The main obstacle is Lemma 1. The envelope can be uncountable, and choosing countably many selections that are simultaneously measurable in and exhaust the supremum for every requires a measurable-selection theorem for multifunctions with values in , a space that need not be metrizable. The obvious argument fixes a dense sequence , picks -optimal measures for each , and passes to general by semicontinuity. As written, that last step appears to need more than the proof supplies: approximation of by uniformly over the chosen needs more than lower semicontinuity of . The fixed-point step needs a Kakutani-type theorem in a locally convex space, which Mathlib does not provide.
and are abstract real vector spaces with their own topologies (instances of IsTopologicalAddGroup, ContinuousSMul ℝ, LocallyConvexSpace ℝ), realised by injective linear maps into and into Mathlib's SignedMeasure Ω. They are not subspaces of with the pointwise topology. The ambient MeasurableSpace Ω is ; is a structure field. The pairing is , and integrability against is a field, so no integral takes a junk value. Compatibility includes continuity of both pairings as well as the representation of continuous functionals. The paper's space is not modelled; no statement uses it.
Committed conventions:
EReal;IsLUB), never sSup on ;Two hypotheses are added where the page relies on them implicitly. is nonempty in the goal, Corollary 1 and the fixed-point milestone. for every is assumed in the goal, Proposition 3 and Corollary 1, because the paper derives measurability of from weak* measurability.
The goal cannot be satisfied by an almost-everywhere version of a conditional expectation chosen separately for each , which would allow itself as a "version". Each is integration against one kernel that is a conditional probability of . The goal mentions no selection, fixed point or Kakutani; appears only inside (K).
Contributions are welcome on all of the following:
All three are reusable beyond this mission.
Stochastic models of covariance matrices need processes that stay in the cone of positive semidefinite matrices. Wishart processes (Bru, 1991) and their extensions underlie multivariate stochastic-volatility and term-structure models in finance (see §1 of Cuchiero et al. for the literature). They are used because their Laplace transforms are explicit: they are exponential-affine in the initial state, and their exponents solve matrix Riccati equations. Cuchiero, Filipović, Mayerhofer and Teichmann (arXiv:0910.0137, Ann. Appl. Probab. 2011) classify all such affine processes on the cone. Theorem 2.4 of that paper says that affine processes on correspond one-to-one to admissible parameter sets. This mission formalizes the converse direction of that correspondence: every admissible parameter set is realized by exactly one affine process.
Timeline:
Let be the real symmetric matrices with , let be the positive semidefinite cone, and let be its interior. Write when . A time-homogeneous, possibly killed Markov process on with transition kernels is affine if it is stochastically continuous and
for functions and .
An admissible parameter set (Definition 2.3) consists of the following:
These data define the operator (2.12),
with . They also define the functions and of (2.16)–(2.17), which drive the generalized Riccati equations , and , .
For every admissible parameter set there is a transition family and there are exponents such that:
Together with the necessity direction (companion mission I in this series), the goal makes admissibility an exact characterization. Every admissible parameter set, including those with jumps of infinite activity and state-dependent killing, defines a well-posed Markov model on . Its Laplace transform is then given by the Riccati flow, which is what makes the model computationally tractable. The intermediate results are reusable on their own:
The theorem is proved in the paper; it is not formalized anywhere. No formal library contains affine processes, generalized Riccati equations on matrix cones, quasi-monotone comparison theorems or martingale problems with jumps. Formalizing them requires all of that infrastructure.
The obvious route is to solve the Riccati equation (2.15) on by Picard iteration and to show invariance of the cone from the inward-pointing condition. That route fails because need not be Lipschitz at : the integral term can have unbounded derivative there (Remark 5.4). Standard invariance theorems therefore do not apply. Instead, quasi-monotonicity keeps the solution away from the boundary.
The obvious construction of the process is also blocked. Stroock's existence and uniqueness theory for martingale problems needs and a uniformly elliptic diffusion part, and neither holds on the cone, where the diffusion degenerates at the boundary. Existence must go through regularized operators with bounded smooth coefficients, then tightness in the Skorokhod space of and a limit. Uniqueness in law comes from the Riccati solutions. The killing terms and are added last.
Conventions committed to in Lean:
Fin d → Fin d → ℝ, with and its norm.∃!.EthierKurtz.HasCadlagPaths).Trivializing formalizations are excluded:
∃! over transition families would be false at negative times, so uniqueness is stated for .Needed infrastructure, reusable beyond this mission: matrix calculus on (square roots, spectral derivatives), comparison theorems for quasi-monotone ODEs, analytic dependence of ODE solutions, tightness in Skorokhod space, and martingale problems on locally compact spaces. Contributions are welcome at any of these levels, as are alternative proofs of the milestones.
Mathematical programs with complementarity constraints (MPCCs, also called MPECs) model optimization problems in which some constraints say that, for every index , at least one of two nonnegative quantities , must vanish. They arise in bilevel optimization, Stackelberg games, the design of equilibria in traffic and electricity markets, and contact problems in mechanics (Luo, Pang, Ralph 1996). Standard nonlinear-programming algorithms do not apply directly: at every feasible point of an MPEC the Mangasarian–Fromovitz constraint qualification fails, so the classical convergence theory of SQP or interior-point methods gives no guarantees.
Relaxation methods replace the MPEC by a sequence of better-behaved nonlinear programs with a parameter , solve each one approximately, and study the limits of the computed points. The question every relaxation method has to answer is what kind of stationary point such limits are, and under which constraint qualification.
Timeline of the result formalized here:
The MPEC (1) on is
with continuously differentiable data. At a feasible the index sets are , , (the biactive set) and .
A feasible is weakly stationary if there are multipliers with , , , such that
with on and on . It is M-stationary if the same multipliers satisfy, for every , either and , or .
The tightened program TNLP replaces the complementarity constraints by on , on and on . CPLD (constant positive linear dependence) for a nonlinear program says: whenever a set of active-constraint gradients is positive-linearly dependent at (a nontrivial vanishing combination with nonnegative coefficients on the inequalities), the same gradients stay linearly dependent on a neighbourhood of . MPEC-CPLD is CPLD for TNLP.
The relaxation of Kadrani et al. is, for ,
A stationary point of is a feasible point with KKT multipliers.
Local minimizers of an MPEC are M-stationary under weak constraint qualifications, whereas strong stationarity needs stronger ones such as MPEC-LICQ; a C-stationary point, the kind of limit the Scholtes relaxation delivers, may still admit first-order descent directions. Theorem 3.5 shows that the Kadrani et al. relaxation reaches M-stationary limits under a constraint qualification that is implied by MPEC-LICQ and MPEC-MFCQ and that holds, for instance, whenever all constraint functions are affine. It separates this scheme from the Scholtes and Steffensen–Ulbrich relaxations in the comparison of the paper.
The theorem is proved in the paper. As far as is known, no part of MPEC theory (constraint qualifications for MPECs, the stationarity hierarchy, relaxation schemes) has a machine-checked proof in Lean or Mathlib. This mission produces a formal account of the stationarity notions of Definition 2.3, of CPLD and MPEC-CPLD, and a complete formal proof of the convergence result, including the standard constraints , that the paper's proof skips for brevity.
The obvious argument passes to the limit in the KKT conditions of . This fails because the multipliers need not be bounded: unlike under MPEC-LICQ or MPEC-MFCQ, MPEC-CPLD does not by itself bound KKT multipliers, and the KKT points of the relaxed programs need not satisfy any constraint qualification themselves (Example 3.6 of the paper). The second difficulty is the biactive set : the product constraint contributes multipliers , to both and , with signs that are not fixed a priori, so a naive limit of the multipliers only gives C-stationarity-type information, or none at all.
is EuclideanSpace ℝ (Fin n) and gradients are Mathlib's gradient; indices are 0-based (Fin m, Fin p, Fin l), and may be zero. Explicit choices fixed by the formalization:
P.IsC1 of every analytic statement.LinearIndependent ℝ of a family indexed by a disjoint union of subtypes, so repeated gradients count as dependent.∀ᶠ y in 𝓝 x*.Two trivializing readings are ruled out. M-stationarity uses one multiplier tuple for both the weak-stationarity equation and the condition on ; separate multipliers would make the sign condition vacuous. MPEC-CPLD demands linear dependence on a whole neighbourhood of , not only at ; the pointwise version is a different hypothesis.
A complete development needs the gradient calculus of products and compositions on EuclideanSpace, a Carathéodory-type lemma (a conic combination can be reduced to one over linearly independent vectors with the same signs), and compactness of bounded sequences in finite dimensions. The Carathéodory lemma and the CPLD/positive-linear-dependence layer are reusable for any constraint-qualification argument in nonlinear programming. Proofs of individual milestones, and of the lemma behind (15), are welcome independently of the goal.
Open networks of single-server queues with general (non-exponential) interarrival and service times, generalized Jackson networks (GJNs), model manufacturing lines, communication networks and service systems. Their stationary distributions are almost never available in closed form. The standard engineering approximation replaces the scaled queue-length vector by the stationary distribution of a reflected Brownian motion (RBM) in the orthant, which is the diffusion limit of the network in heavy traffic, when every station is close to full utilisation.
The diffusion limit itself (Reiman, 1984) is a statement about the process on finite time intervals. Using the RBM's stationary law as an approximation of the network's stationary law requires interchanging two limits: time to infinity (steady state) and traffic intensity to one (heavy traffic). For a long time this interchange was assumed rather than proved.
Timeline.
There are stations. Station receives external arrivals with i.i.d. interarrival times of law (rate , or no arrivals at all) and serves jobs first-in-first-out with i.i.d. service times of law (mean , rate ). A job finishing at moves to with probability or leaves. The routing matrix is substochastic with spectral radius below one. Interarrival and service times have uniformly bounded conditional exponential moments of their residual lives (conditions (1)–(2)). The traffic equation gives the effective rates and the traffic intensities .
The queue lengths are not Markov. The state , which adds the elapsed interarrival and service times, is a Markov process on . A law on is stationary if implies for all .
Heavy traffic. Fix a critically loaded network ( for all ) and a vector . The network slows the arrivals of at station by the factor , so that for an explicit (display (17)). Let be any stationary distribution of , and let be the law of under .
The RBM. For a Brownian motion with drift and covariance , the RBM with parameters solves the Skorohod problem , with nondecreasing and increasing only when is on the boundary. Here and is the explicit covariance matrix of Reiman's theorem, built from , , and the squared coefficients of variation , of .
where is the unique stationary distribution of the -RBM. The formal goal asserts three things: a stationary distribution of the RBM exists, it is the only one, and converges weakly to it, for every choice of stationary distributions .
The result. Theorem 8 justifies the use of the RBM's stationary distribution, which is computable or at least numerically tractable, as an approximation of steady-state queue lengths of a heavily loaded network. Theorem 7 also shows that each stationary queue is of order uniformly in . Together with Theorem 8 this gives convergence of all moments (Corollary 2 of the paper) and, through Theorems 9–12, steady-state approximations of sojourn times and product-form limits.
Formalizing it. No part of this argument is machine-checked. The formalization would add reusable infrastructure for queueing theory in Lean: a Markov-state model of a generalized Jackson network with residual times, Lyapunov bounds on stationary distributions of general Markov processes (Theorems 5–6), and the link between tightness and identification of limit points for stationary laws. Reiman's theorem (Theorem 4) and the Harrison–Williams theorem (Theorem 3) are cited by the paper and are themselves open formalization targets.
Tightness and Reiman's theorem do not combine on their own. Reiman's theorem describes the network on finite time intervals, started empty, while a stationary distribution describes it as time goes to infinity; nothing in the finite-horizon limit forces a limit point of to be stationary for the RBM, or forces different subsequences to have the same limit. The interchange therefore needs the process limit from an arbitrary initial law and the uniqueness of the RBM's stationary law, besides tightness.
The tightness step is the technical core. Moment bounds must be uniform in and in the initial residual times. A Lyapunov argument on the workload over a time horizon of order requires deviation bounds of order for renewal processes started at arbitrary ages. This is why the residual-life conditions (1)–(2) appear, and why the strong approximation of Lemma A.2 is used. A naive drift argument over a fixed time horizon fails: in heavy traffic the drift of per unit time is only of order .
Fin J, vectors Fin J → ℝ, is Pᵀ, and the norm is the norm, written as an explicit sum. The spectral-radius condition is .IsGJN (positive times, conditions (1)–(2), substochastic ). and count renewal epochs in . The initial times , are residual lives given the elapsed ages , . States carry their elapsed times as reals; the predicate InStateSpace cuts out , and the uniform bounds over initial states (Lemma A.1, Propositions 2–3) and the initial laws of Theorem 4 range over only.Reiman84.QueueLength.Paths (Brownian motion with drift and covariance, and the reflection pair). An RBM stationary law must be a probability measure carried by . Weak convergence of laws on uses Mathlib's topology on ProbabilityMeasure. Theorem 4's process convergence is in coupling form with the uniform topology on .Classical arbitrage pricing fixes one probabilistic model of the underlying asset and prices a contingent claim as an expectation under an equivalent martingale measure. When the volatility is not known, a seller who wants to be safe under every plausible model has to superreplicate: hold an initial capital and a trading strategy whose terminal value dominates the claim under all models at once. The uncertain volatility model (UVM) of Avellaneda, Levy and Parás (Appl. Math. Finance 1995) and Lyons (Appl. Math. Finance 1995) is the standard instance: the volatility is only known to lie in an interval .
The family of laws describing such uncertainty is not dominated by a single reference probability, so "almost surely" and the usual stochastic integral are not available. Denis and Martini (Ann. Appl. Probab. 2006) replace them by a capacity and a quasi-sure stochastic integral, and show that the superreplication price of a broad class of path-dependent European claims is a supremum of expectations over martingale laws. This framework is a precursor of quasi-sure analysis and -expectations (Denis, Hu and Peng, Potential Anal. 2011; Soner, Touzi and Zhang, Electron. J. Probab. 2011).
Fix . is the space of continuous paths with , with the uniform norm, Borel -field and canonical filtration . A martingale measure is a probability on under which is an -martingale; denotes the set of these.
A nonzero measure on with continuous distribution function bounds the bracket. Hypothesis on a set says for every ; adds a lower bound . In the UVM, and .
The capacity of a bounded continuous is , extended to all functions through lower semicontinuous majorants. A set is polar if its capacity is , and a property holds quasi-surely (q.s.) outside a polar set. is the completion of under . Elementary integrands have integrals , and is their completion for . is the space of attainable gains. The superreplication price of a claim is
Assume and that is Hölder continuous. There is a set of martingale measures satisfying such that
for every bounded continuous of the form , or , with (and the cylindrical ) bounded continuous. The goal leaves unspecified, as the paper does.
In attack order: the transfer of a.s. inequalities to q.s. ones (Lemma A.7); the pathwise moment bound q.s. (Proposition 2.9) and its price form (Proposition 2.13); a universal bracket (Lemma 2.10) approximated by realized variance (Lemma 2.14); weak duality (Lemma 2.15); the representation over probabilities on the Stone–Čech compactification (§5, p. 19) and the Cauchy–Schwarz inequality for (Lemma 4.3); the martingale property and continuity of under each (Proposition 5.2); the bracket bounds for the induced law (Lemma 5.3); membership of the three claim families in the class of with (Lemmas 5.4–5.6); and Theorem 3.1 for the literal class .
Further statements: Theorem 6.1 (all martingale measures with form a valid ), Proposition 3.2 (the case ), Proposition 2.12 (measures not charging polar sets inherit the bracket bounds), Theorem A.8 (closedness of under ).
The theorem identifies the cheapest model-free hedge of path-dependent European claims (cylindrical payoffs, Asian-type averages, lookbacks on the maximum) with a worst-case expectation over martingale laws obeying the same bracket bounds. Theorem 6.1 specializes it to the generalized UVM, where the dual set is all martingale measures with ; the paper notes this is new even for the Lebesgue case. The result supplies a rigorous non-dominated duality on which robust pricing bounds and -expectation pricing rest.
The theorem is proved in the paper; no part of it is machine-checked. A formalization would produce the first Lean development of a capacity on path space, of a quasi-sure stochastic integral, and of a continuous-time quadratic variation on the canonical space. These objects are absent from Mathlib, which has discrete- and continuous-time martingales, the Stone–Čech compactification and the Riesz–Markov–Kakutani theorem, but no stochastic integral.
The family is not dominated, so neither the Itô integral of a single model nor a common null set is available: every inequality obtained under one by the Itô formula must be lifted to a quasi-sure one, and every limit taken in the capacity. The natural dual argument (Hahn–Banach on ) produces linear forms whose representation as measures on is not available because need not be all of . The paper's route works on bounded continuous claims and compactifies; the price is that the dual measures live on , where is unbounded and must be extended by truncation, and the identity linking back to holds only for a class of claims that has to be checked family by family.
is a subtype of C(Set.Icc 0 T, ℝ) (paths with ) with the Borel -field of the sup-norm topology. Distribution functions are continuous StieltjesFunctions vanishing at and positive at . The quadratic variation is a predicate: an adapted process with -a.s. continuous nondecreasing paths from such that is a martingale. The capacity takes values in with the Appendix's Lebesgue extension; q.s. means outside a set of capacity zero. , and are membership predicates on functions. is the image of the completion . and every supremum are extended reals. is Mathlib's StoneCech, and is the set of Borel probabilities on it dominated by on .
Standing assumptions, stated as hypotheses: on for all §2 results, where the page assumes it, and Hölder continuity of for every result of §4–§5 and the goal (p. 12: "From now on, we assume that is Hölder continuous"). The goal replaces the class , which is defined only inside the proof, by the three families of Lemmas 5.4–5.6. The literal form is a milestone. Lemma 2.14 adds . Lemma 5.3 is stated for the law on .
The following trivializing formalizations are ruled out. An empty with a real-valued would make the goal ; here both sides are . Defining q.s. as "a.s. for every " would make Lemma A.7 a tautology. Replacing by the closure of elementary integrals would shrink . Dropping the martingale condition from the quadratic-variation predicate would make satisfiable by any deterministic process.
A complete development needs Itô's formula and the Burkholder–Davis–Gundy inequalities for continuous martingales, Doob–Meyer uniqueness, a Kolmogorov continuity criterion, and the theory of regular Choquet capacities. These are reusable well beyond this mission, and contributions of any of them are welcome.
Large call centers, cloud server farms and hospital wards are modeled as many-server queues: identical servers, customers arriving according to a counting process, each customer served by one server for a random time drawn from a distribution , and customers who find all servers busy waiting in a first-come first-served queue. When is large, the number of customers is of order and the natural object of study is the fluid limit, obtained by dividing all quantities by and letting . For exponential service times the fluid limit is a finite-dimensional ordinary differential equation. For a general service distribution — and call-center data show service times far from exponential (lognormal, in Brown et al., 2005) — the state must record how long each customer in service has been served, and the fluid limit is a measure-valued process.
Kaspi and Ramanan (Ann. Appl. Probab. 21 (2011) 33–114) characterize this limit by a pair of fluid equations for general with a density, prove that they have at most one solution, show that the scaled -server processes converge to it, and describe its long-time behavior. This mission is the last of these results: in the critically loaded fluid system, every solution converges to equilibrium.
Timeline. Whitt (2006) introduced a fluid model of the many-server queue with general service times and abandonment, and stated the case of property (1) of the goal theorem without proof (his Theorem 7.3). Kaspi and Ramanan (2011) gave the measure-valued formulation with the age process, uniqueness and existence of fluid solutions, and the convergence to equilibrium formalized here. Reed (2009) treated the related queue in the Halfin–Whitt regime.
The service distribution has a density , is carried by , and has mean one: . Let , and let be the hazard rate on .
The fluid state at time is a number , the scaled number of customers in system, and a measure on of total mass at most one: is the scaled number of customers in service whose age (time already spent in service) lies in . The input is a nondecreasing càdlàg arrival function with , an initial number and an initial age measure , satisfying (servers are idle only when nobody waits). The set of such triples is .
A càdlàg pair solves the fluid equations if the cumulative departures are finite, the entries into service satisfy the transport equation
for every compactly supported test function on (ages grow at unit rate, customers leave at rate , new customers enter at age ), mass is conserved, , and the system is non-idling, .
The equilibrium measure is on , a probability measure by the mean-one normalization. With (arrival rate equal to the total service capacity), and is a constant solution. Assumption 2 asks that be bounded or lower semicontinuous near . The renewal measure of is , the unit mass at included.
Under Assumption 2:
Theorem 3.9(2) is the stability statement of the fluid model in the critically loaded case: whatever the initial occupancy and the initial ages, the age distribution of customers in service converges to the stationary excess distribution of . It justifies using as the operating point around which diffusion approximations of many-server queues are built, and it is the fluid counterpart of the classical fact that the age of a stationary renewal process has density . Part (1) gives the transient behavior of an underloaded or critically loaded system started empty.
The result is proved in the paper; nothing here is open. To our knowledge none of it has been formalized. A formalization adds machine-checked statements of a measure-valued fluid model that the companion mission (uniqueness of fluid solutions, Theorem 3.5) shares, and exercises renewal theory — the renewal measure, a key renewal theorem for laws with a density, Lorden's inequality — in a form usable by other queueing developments.
The naive argument would show that is given by an explicit formula and pass to the limit. The explicit age representation of a solution involves , which is known only through a renewal equation whose forcing term depends on itself; there is no closed form unless the system never fills up. For the system can alternate between full and not full, and the convergence must be proved without knowing when. Two ingredients carry the weight: a comparison showing that the occupancy tends to one, and a key renewal theorem for the backward recurrence time of a renewal process with a density, which needs total-variation rather than vague convergence because the test functions are only bounded and continuous. The uniform-in-time control of Lemma 6.3 is where the second moment enters.
Everything lives in ManyServerFluid.Equilibrium. The service law is a structure holding the density with , on , , and mean one. Time is , read on . Age measures are Mathlib FiniteMeasure ℝ carried by , with the weak topology, so "càdlàg" is in the paper's topology. The departures are lower integrals in ; and are Lebesgue–Stieltjes measures. The convolution powers are the published QueueingFundamentals.MG1.convPow.
Explicit choices, each also stated in the item that uses it:
Weak convergence in Theorem 3.9(2) is against all bounded continuous functions, not compactly supported ones; vague convergence would let mass escape towards and is not the theorem. The monotonicity in part (1) is part of the statement. A formalization in which these were dropped, or in which omitted the unit mass at , would state a different result.
Existence. The paper's proof of Theorem 3.9(2) compares an arbitrary solution with the solution started empty, which it obtains from its Theorem 3.7 (existence via the -server limit); that theorem is not part of this series. Here every solution is a hypothesis, so nothing false is stated, but a proof of the goal must construct the empty-start solution for . It is explicit: has density on while , and from on it equals (Proposition 6.1, Remark 3.8, Lemma 3.4).
Contributions welcome: general renewal theory (local finiteness of , Lorden's inequality, the key renewal theorem for spread-out laws in total variation), and lemmas on the fluid equations shared with the uniqueness mission (the monotonicity of , the renewal equation (4.5), the age representation (3.11)).
Affine processes are Markov processes whose Laplace transform depends exponential-affinely on the initial state. On the cone of positive semidefinite matrices they model stochastic covariance matrices in multivariate stochastic volatility, interest-rate and credit models. Examples include the Wishart process of Bru (Bru 1991) and Ornstein–Uhlenbeck processes driven by matrix Lévy subordinators (Barndorff-Nielsen and Stelzer 2007, reference [3] of the paper). Cuchiero, Filipović, Mayerhofer and Teichmann (2011) characterize all affine processes on by admissible parameter sets.
On the canonical state space , Duffie, Filipović and Schachermayer (2003) showed that regular affine processes are exactly the infinitely decomposable Markov processes: the law started at is a -fold convolution of laws started at the . That property drives their existence proof. On with it fails. The Wishart marginals are not infinitely divisible, a classical result of Paul Lévy. This mission formalizes the exact characterization: Theorem 2.9 of Cuchiero et al.
is the space of real matrices and the symmetric ones. carries the pairing and the norm . is the closed convex cone of positive semidefinite matrices, and its one-point compactification. The point is the cemetery, where a killed process goes.
A transition family consists of sub-stochastic kernels on satisfying and the Chapman–Kolmogorov equations. It is stochastically continuous if weakly as . The process is affine (Definition 2.1) if there are and with
Theorem 2.4 of the paper attaches to every affine process a unique admissible parameter set . In it, is the diffusion parameter, the constant drift, and the killing rates, and and the jump measures. The exponents solve the generalized Riccati equations , , with given by (2.16)–(2.17).
The canonical space consists of paths that stay at once they reach it, with coordinate process . is the set of families of laws on under which is a stochastically continuous Markov process with . The convolution is the image of under . A family is infinitely decomposable (Definition 2.7) if for every there is with . It is infinitely divisible if every marginal is.
For and , the following are equivalent:
The theorem separates two classes that coincide on . On with , a diffusion component, which must satisfy , is incompatible with taking -th roots, because the root would need drift . So the existence proof of Duffie–Filipović–Schachermayer, which builds a process from infinitely divisible kernels, covers exactly the pure-jump affine processes on . Processes with a diffusion part need the martingale-problem approach of the paper's §5. Proposition 5.11 gives the alternative existence proof for (§5.3).
The theorem is proved in the paper. As far as is known, none of it has been machine-checked: no formal library has affine processes on matrix cones, convolution of path measures, or the Lévy–Khintchine form on . Formalization contributes a checked equivalence that rests on the paper's other main theorem (Theorem 2.4), together with reusable statements about Cauchy's equations on cones and Laplace functionals of Markov families. It is the third mission of a series. Missions I and II formalize the two halves of Theorem 2.4.
The equivalence links three layers: path-space laws, one-dimensional kernels, and Riccati exponents. (i) (ii) first needs the multiplicative structure of Laplace functionals in the initial state. That gives affinity of the process and of each -th root, with exponents . Then it needs the fact that the root's parameter set is and is again admissible, so for all . The second step relies on the full necessity theorem, in particular Proposition 4.18. The first fails without strict positivity of the Laplace functional: Cauchy's exponential equation has non-exponential solutions that vanish somewhere (Remark 6.3). (ii) (iii) requires every Riccati solution to stay in the Lévy–Khintchine cone. This is clear for finite-variation jumps via Picard iteration, but the general case needs the approximation . (iii) (i) must produce a Markov family of -th roots on path space, not merely roots of each marginal. The case shows that cannot be dropped: there the Cox–Ingersoll–Ross process has and is infinitely decomposable.
Fin d → Fin d → ℝ, with and . is the subtype of matrices with Mathlib's PosSemidef.OnePoint of the cone, with its Borel σ-algebra. Addition is extended with absorbing. is the space of all paths with the product σ-algebra; every notion in the theorem depends only on finite-dimensional distributions. Absorption at and the Markov property with transition family are imposed through finite-dimensional distributions. The path-sum map is measurable, which is checked in Lean, so the convolution is a genuine push-forward.A multistage stochastic program chooses decisions over time periods while a random input is revealed one stage at a time; the decision at stage may use what has been observed so far and nothing more. Such models are used for capacity expansion, hydro-thermal power scheduling, asset–liability management and production planning. In practice the true input process is never used directly: it is replaced by an estimate, a discretization or a scenario tree with few branches, and the program is solved for that approximation. Whether the optimal value of the approximate program is close to the true one is therefore the basic question behind every scenario-tree method.
For two-stage programs () the answer is classical: the optimal value is Lipschitz continuous with respect to suitable distances of probability distributions (Rachev and Römisch, 2002). For that methodology breaks down, because the multistage objective depends on conditional expectations given the past, and hence on the information structure of the input, not only on its distribution. Heitsch, Römisch and Strugarek (SIAM J. Optim. 2006) showed that the gap is closed by adding one more term: a distance between the filtrations generated by the true and the approximate inputs. Their estimate is the basis of later work on scenario-tree construction and on the nested distance of Pflug and Pichler.
Let be a probability space and a process with . The information available at stage is , and is the σ-field it generates; is deterministic, so . The linear multistage program (1) is
where is a polyhedron, for are polyhedral cones, and are fixed matrices, and the costs and right-hand sides are affine functions of the current input . Write for the objective and for the feasible set.
Which data are random fixes two integrability exponents: if only the costs are random, and ; if only the right-hand sides are random, ; otherwise . The input lives in and the decisions in , and is the distance of two inputs.
Three conditions are imposed: (A1) complete fixed recourse, for ; (A2) is finite and is level-bounded locally uniformly at : for some there are and a bounded set such that the level set is nonempty and contained in whenever ; (A3) .
The filtration distance at stage compares how well a near-optimal decision of one problem is predicted from the other problem's information:
Under (A1)–(A3) and boundedness of there are positive constants , , such that
for every input with and finite. The constants are existential: the theorem asserts the shape of the estimate, not its numerical values.
The theorem identifies what an approximation of a multistage input must preserve: closeness in alone is not enough, and the filtration term measures exactly the information that is lost or gained. It justifies scenario-tree construction by forward selection and reduction (Heitsch and Römisch, 2009), where both terms are controlled, and it is the precursor of the nested distance, for which analogous Lipschitz bounds are proved. Without such an estimate a scenario tree that matches the marginal distributions can still give an arbitrarily wrong optimal value.
The result is proved in the paper; it has not been formalized. A machine-checked version needs, and would produce, a formal theory of linear programs with decisions adapted to a generated filtration in spaces, Lipschitz continuity of polyhedral set-valued maps, and measurable selections of conditional-expectation projections. Each of these is reusable well beyond this paper.
The obvious argument — take a near-optimal policy for and evaluate it for — fails at once: that policy is adapted to , not to , so it is not feasible for the perturbed problem, and projecting it by conditional expectation onto destroys the equality constraints. Any repaired policy must again be -measurable at every stage, and an error made at stage propagates to all later stages through the recursion , where it must stay controlled in the right norm. The three integrability regimes need separate estimates; in the regime the error must be bounded essentially, not only on average.
The program is encoded in a single definitions file. Stages are natural numbers with dimension functions , . is given by finitely many linear inequalities and each , , by finitely many homogeneous ones, so "polyhedral" and "polyhedral cone" are built in. The matrices are linear maps between Euclidean spaces; and . A randomness pattern (costs, rhs, both) carries the exponents and its restriction on the data: for costs, for rhs, none for both.
The committed conventions are:
condExp;Trivializing formalizations are ruled out: the constants , , are quantified before ; the theorem covers all three randomness patterns; the level sets are nonempty, so the suprema are not vacuous; and a sorry-free check exhibits data satisfying (A1) with a feasible policy, so the hypotheses are satisfiable.
Contributions are welcome on Lipschitz continuity of polyhedral set-valued maps (Walkup–Wets), measurable selections, conditional expectation of set-constrained random vectors, and any of the case estimates.
Nodal sets are the zero loci of Laplace eigenfunctions. Their size probes how geometry constrains high-frequency oscillation. The pinned manuscript supplies the research context.
The encoded manifold is S4×S1 with one smooth Riemannian metric. The sequence consists of nonzero smooth real eigenfunctions with positive eigenvalues tending to infinity.
The selected goal is OAI.Yau.Target.yau_nodal_set_upper_bound_counterexample. Its central assertion is
The theorem states that the defined proposition MainTarget holds, i.e. that there exist a smooth Riemannian metric g on the 5-manifold S⁴ × S¹ (the unit sphere in ℝ⁵ times the circle, modelled on ℝ⁴ × ℝ¹), a sequence of positive reals λₖ, and a sequence of smooth real functions uₖ on this manifold, each not identically zero, such that the following hold. At every point x, in the extended chart at x, the coordinate Laplacian of uₖ, namely (1/√det G) Σᵢ ∂ᵢ(√det G Σⱼ Gⁱʲ ∂ⱼ(uₖ∘chart⁻¹)), where G is the matrix of g in the chart's coordinate frame and Gⁱʲ its inverse, satisfies −Δ_g uₖ(x) = λₖ uₖ(x), so each uₖ is a Laplace eigenfunction with eigenvalue λₖ. Moreover λₖ → ∞, and the 4-dimensional Hausdorff measure (taken with respect to the distance induced by g) of the nodal set {uₖ = 0}, divided by √λₖ, tends to +∞ as k → ∞. Thus the nodal-set size grows faster than the order √λₖ, which is a counterexample to a Yau-type upper bound on nodal sets in this setting. The theorem is admitted in the source and not proved there.
The selected target is divergence relative to the square-root eigenvalue scale. It does not specify the fixed additional power ε0 asserted by the manuscript title and abstract. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The same smooth metric must support the whole eigenfunction sequence, and the nodal measure uses the distance induced by that metric.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.A symplectic form can be positive on complex lines without being invariant under the almost complex structure. The target asks whether some compatible form nevertheless exists in four dimensions. The pinned manuscript supplies the research context.
The manifold is smooth, compact, connected, Hausdorff and second countable, modeled on real four-space. The almost complex structure squares to minus the identity.
The selected goal is OAI.TamingCompatibility.taming_implies_compatibility. Its central assertion is
The theorem states that, for a smooth manifold X modeled on four-dimensional Euclidean space ℝ⁴ (charted with smooth transition maps) that is Hausdorff, second countable, compact and connected, and for an almost complex structure J on X, if some symplectic two-form α tames J, then there exists a symplectic two-form η that is compatible with J. Here a two-form assigns to each point x a continuous alternating real bilinear form on the tangent space at x, and an almost complex structure J is a smooth field of continuous linear endomorphisms of the tangent spaces with J(Jv) = −v for every tangent vector v. A two-form is symplectic when it is smooth (its pullbacks along smooth maps from open subsets of ℝ⁴ are smooth), closed (the exterior derivative of each such pullback vanishes), and nondegenerate (a tangent vector v with α(v,w) = 0 for all w must be zero). The form α tames J when α(v, Jv) > 0 for every nonzero tangent vector v at every point. The form η is compatible with J when it tames J and is J-invariant, meaning η(Ju, Jv) = η(u, v) for all tangent vectors u and v at every point. This is a formal statement admitted without proof.
The conclusion supplies a possibly different symplectic form. It does not assert that the original taming form is compatible or prescribe its cohomology class. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
A pointwise compatibility adjustment need not preserve closedness. The conclusion requires both global symplectic structure and positivity.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.Hochschild cohomology measures whether a cocycle equation admits a primitive. In an operator algebra the boundedness requirement is part of the mathematical problem. The pinned manuscript supplies the research context.
Cochains are continuous complex multilinear maps into the von Neumann algebra itself, with its natural left and right multiplication actions.
The selected goal is OAI.BoundedHochschild.KadisonRingrose.main_result. Its central assertion is
The theorem states that, for a complex von Neumann algebra M (a C*-algebra with a partial order making it star-ordered, equipped with the W*-algebra structure), and any natural number n, every bounded Hochschild cocycle of degree n+2 with values in M is a coboundary. Here a cochain of degree m is a continuous complex m-linear map from M^m to M. The Hochschild differential of a cochain f of degree m, evaluated at (v_0,...,v_m), is v_0 f(v_1,...,v_m) plus the sum over j from 0 to m-1 of (-1)^(j+1) f(v_0,...,v_j v_{j+1},...,v_m), where the j-th and (j+1)-th inputs are multiplied into one, plus (-1)^(m+1) f(v_0,...,v_{m-1}) v_m. The hypothesis is that f has degree n+2 and its differential vanishes at every (n+3)-tuple of elements of M. The conclusion is that there exists a continuous multilinear cochain g of degree n+1 whose differential equals f at every (n+2)-tuple of elements of M.
The goal covers every natural n, hence degrees at least two. It does not include a separately referenced degree-one inner-derivation theorem. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
An algebraic primitive is insufficient: the lower-degree cochain must remain continuous and bounded in the encoded operator-norm sense.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.Group von Neumann algebras encode a free group's regular representation as an operator algebra. Whether the rank remains visible in that algebra is the motivating isomorphism problem. The pinned manuscript supplies the research context.
The parameter runs over extended nonnegative reals greater than one. Integer ranks use group factors, infinity uses countably many generators, and other parameters use the encoded stabilized corner model.
The selected goal is OAI.FreeGroupFactorMain.Interpolation.allInterpolatedIsomorphic. Its central assertion is
The theorem states that for any two extended nonnegative real parameters r and s, both strictly greater than 1 (so either may be infinite), the interpolated factors attached to r and s are isomorphic as C*-algebras with trace and topology, meaning the type of normal tracial equivalences between them is nonempty. The interpolated factor at a parameter is chosen by cases: for r = ∞ it is the group von Neumann algebra of the free group on countably many generators; for r equal to a natural number n it is the group von Neumann algebra of the free group on n generators; otherwise it is the corner pAp of the stabilization of the rank-two free group algebra, cut down by a selected star projection p whose stabilized projection trace is the real number 1/√(r−1), with the trace being the stabilized trace rescaled by the inverse of that value. Each carries its canonical trace or this rescaled trace and an ultraweak-type topology. A NormalTracialEquiv between two such models consists of a ℂ-linear star-algebra isomorphism that preserves the traces and is continuous in both directions for the given topologies.
The goal is a nonempty type of normal tracial equivalences between the precise interpolated models. Statements about fundamental groups are not separate attached targets. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The required equivalence must preserve the algebra, involution and trace, and be continuous in both directions for the specified topologies.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.Replacing a hyperboloidal end by an asymptotically flat end can connect Bondi mass with ADM mass. The source seeks a replacement that preserves interior geometry, the energy condition, and almost all enclosing area. The source is OpenAI's September 2026 manuscript.
A CKS exterior datum describes a three-dimensional hyperboloidal end and its mass aspect. Its Bondi charge is energy-momentum , assumed strictly future timelike. An enclosing cut is a surface in the supplied geometric class; its area is computed from the metric.
For a connected, Hausdorff, second countable smooth 3-manifold N with boundary and a smooth Riemannian metric g with a smooth symmetric tensor field K, such that N is orientable, the boundary is compact and nonempty, g is complete, and (g,K) satisfies the pointwise local-chart physical dominant energy condition PhysicalDEC, the following holds. Suppose d is a CKS exterior-end datum for (g,K): a coordinate end outside radius d.chart.radius in which g and K are represented by smooth perturbations, together with a smooth mass aspect function on the sphere and the tensor patches realizing it. If the Bondi charge (energy, momentum) of d's mass aspect, (E,P), is timelike, meaning |P|<E, then there exist another such datum d', a radius R₀ with d'.chart.radius<R₀ and 12≤R₀, and a function ε with ε(R)→0 as R→∞, such that d' has Bondi charge (√(E²−|P|²),0), and the minimal enclosing area of g is finite. Moreover, for every R≥R₀ one has 0≤ε(R)<1 and there are a complete smooth metric gR, a smooth symmetric tensor field kR, spatial tensor fields G and k on Euclidean 3-space, and a number η with these properties. The pair (gR,kR) agrees with (g,K) at every point outside the chart domain or with chart coordinate norm at most R, and satisfies PhysicalDEC and integrable constraints. Also gR≥(1−ε(R))g as quadratic forms. On the end, gR and kR equal the end metrics built from G and k in d'.chart. Each Cartesian component of G minus the identity satisfies the order-1 Symbol condition from CKSADM, and k vanishes where ‖x‖>2R². As r→∞ the spatial ADM energy of G tends to √(E²−|P|²)+η and the ADM momentum of (G,k) tends to 0, with 0≤η≤2R^(−1/2). Finally, gR has finite minimal enclosing area, (1−ε(R)) times the minimum enclosing area of g is at most that of gR, and for every outer domain D the cut areas of g and gR are finite and satisfy (1−ε(R))·cutArea(g,D)≤cutArea(gR,D).
The goal is OAI.CKSSourceExterior.area_controlled_end_replacement. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The selected goal constructs end replacements with zero limiting ADM momentum and quantitative area comparison, including minimum enclosing area. The Schwarzschild equality examples are attached as a separate target. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Changing the end can create a cheaper enclosing surface or violate the dominant energy condition. Agreement on each retained interior region does not alone prevent either problem.
The manifold is a connected Hausdorff second-countable smooth three-manifold with compact nonempty boundary, and the original complete data satisfy the physical dominant energy condition. The main target is end replacement; it does not itself state the final Bondi–Penrose inequality. The equality-example target keeps its stronger boundary and no-additional-horizon hypotheses.
The shared definitions are supplied by CKSBondiPenrose, CKSBondiPenrose_002. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Standard generator subsets define natural subgroups in an Artin group. The source asks whether arbitrary conjugates of these subgroups remain in the same class after intersection. The source is OpenAI's September 2026 manuscript.
A standard parabolic subgroup is generated by a subset of the standard generators. A parabolic subgroup is any conjugate of one. There is no requirement that its Coxeter subgroup be finite.
The theorem, which is admitted in the source with a placeholder proof, states the following for a Coxeter matrix M on a finite, linearly ordered index set S, with Artin(M) the Artin group presented on generators S by the braid relations: the word of alternating generators s,t,s,... of length M(s,t) equals the alternating word beginning with t, for each pair s,t. For any two subsets X and Y of S and any two elements g and h of Artin(M), there exist a subset Z of S and an element k of Artin(M) such that the intersection of the two conjugate subgroups g P_X g⁻¹ and h P_Y h⁻¹ equals k P_Z k⁻¹. Here P_T is the standard parabolic subgroup generated by the images of the generators in T, and conjugation by g is the subgroup whose members x satisfy g⁻¹xg in P. There is no spherical-type or other restriction on M, so the intersection of two conjugates of standard parabolic subgroups is itself a conjugate of a standard parabolic subgroup.
The goal is OAI.HarmonicArtin.ParabolicIntersections.unconditional_parabolic_intersections. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The selected goal is closure under binary intersection. Attached results also give arbitrary intersections controlled by at most the rank many members, unique parabolic closure, and dynamics for irreducible non-clique groups. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Conjugation obscures the standard generating subsets, so intersecting and alone does not describe the subgroup intersection. The target must produce both a new subset and a new conjugating element.
The generating type is finite and linearly ordered. The Coxeter-matrix convention encodes an infinite label by zero. The dynamics milestone has additional irreducibility and non-clique assumptions; those are not imposed on the intersection theorem.
The shared definitions are supplied by ArtinParabolicIntersections. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
A classifying-space problem asks whether a natural complex captures a group without additional higher homotopy. The source addresses the finite-rank Artin problem through the lifted spherical-cell complex. The source is OpenAI's September 2026 manuscript.
An Artin group is presented by alternating braid relations from a Coxeter matrix. A subset of generators is spherical when its associated Coxeter parabolic subgroup is finite. Lifted cells pair a group element with such a subset, with incidence determined by reduced coset words.
For every Coxeter matrix M indexed by a finite type S of standard generators, the topological space SalvettiCover(M) is contractible. The Artin group Artin(M) is the free group on S modulo the braid relators, one for each ordered pair (s,t): the alternating word s t s t ... of length M(s,t) times the inverse of the alternating word t s t s ... of the same length. A subset T of S is spherical when the standard parabolic subgroup of the Coxeter group generated by the simple reflections in T is finite. A lifted cell is a pair (a,T) of an Artin group element and a spherical subset. One lifted cell (a,T) is a face of (b,U) when T is contained in U and there is a word w in letters of U that is reduced in the Coxeter group (its Coxeter length equals the word length), is of minimal length in its coset with respect to the parabolic subgroup generated by T, and satisfies a = b times the image of w in the Artin group. The preorder on lifted cells is the reflexive transitive closure of this face relation, and SalvettiCover(M) is the geometric realization, as a topological space, of the nerve of that preorder viewed as a category.
The goal is OAI.HarmonicArtin.salvetti_cover_contractible.
The goal makes the full topological realization contractible, rather than only asserting vanishing of a selected homotopy group. It supplies a precise target for the covering-space component of the source. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Local spherical pieces need not automatically fit into a globally contractible realization. The face relation and its transitive closure must retain the interaction between Artin words and Coxeter length.
SalvettiCover is the geometric realization of the nerve of the lifted-cell preorder. The generator type is finite but need not be equipped with a chosen enumeration. The mission preserves this published model instead of substituting a different complex.
The shared definitions are supplied by HarmonicArtin. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
An Ising spin system probes a quadratic form only on cube vertices. The source asks whether random orthogonal eigenvectors allow its pressure to be determined by the limiting eigenvalue distribution at every positive temperature. The source is OpenAI's September 2026 manuscript.
The pressure is the normalized logarithm of the average Boltzmann weight under the uniform spin prior. Eigenvectors are Haar orthogonal, and the deterministic empirical eigenvalue laws converge weakly to a compactly supported probability law. The variational formula uses an edge-extended spectral transform.
For a spin system on N Ising spins σ ∈ {−1,1}^N, the rotated pressure for eigenvalues λ₁,…,λ_N, an orthogonal rotation U and a field c is (1/N) times the log of the average over all 2^N spin configurations of exp(H(σ)), where H(σ) = (1/2)∑ᵢ λᵢ (Uσ)ᵢ² + ∑ᵢ cᵢσᵢ. The theorem states that, for any probability space (Ω,P), random N×N orthogonal matrices U_N that are measurable and whose laws are right-invariant under multiplication (Haar-type), and any deterministic eigenvalue arrays (eig_N,i), the following holds under these assumptions: ν is a probability measure on ℝ whose support lies in [a,b] and contains both a and b; for every ε>0, eventually in N all eigenvalues lie in [a−ε,b+ε]; the empirical spectral laws (1/N)∑ᵢ δ_{eig_N,i} converge weakly to ν; and the inverse temperature β is strictly positive. Then, with eigenvalues β·eig_N,i, rotation U_N(ω)⁻¹ and zero external field, the expected rotated pressure ∫ pressure dP converges as N → ∞, and the pressure itself converges for P-almost every ω, in both cases to the real part of the variational functional of the measureR transform of the β-rescaled law of ν, evaluated at the edge β·b.
The goal is OAI.InvariantIsing.positive_temperature_pressure_unconditional. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The selected goal is the all-positive-temperature zero-field pressure theorem. The attached results also cover field laws, random spectra, Gaussian-pattern pressure and ground energy, and related norm limits under their stated assumptions. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.
Weak spectral convergence does not control rare extreme eigenvalues. The explicit no-outlier condition is essential to the selected statement’s comparison with the limiting spectral functional.
The spin prior is uniform probability, and temperature is implemented by multiplying eigenvalues by . The no-outlier condition holds eventually within every enlargement of the limiting support interval. Almost-sure convergence and expectation convergence are both conclusions; other attached variants keep their own uniform-integrability and field hypotheses.
The shared definitions are supplied by InvariantIsing. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.
Rectangular matrix products arise when the two outer dimensions are much larger than the inner dimension. The dual exponent records the largest inner growth rate compatible with arithmetic exponent two. The source manuscript presents the surrounding research claim.
For k∈[0,1], ω_ℂ(1,k,1) is the infimum of exponents for multiplying an n×⌈nᵏ⌉ matrix by a ⌈nᵏ⌉×n matrix over ℂ. The dual exponent α is the supremum of k for which this infimum equals two.
Prove the strict bound
The additional published rectangular endpoint asserts ω_ℂ(1,709/1000,1)<523/250=2.092.
The selected formal target is OAI.MatrixMultiplication.complex_alpha_gt_93_div_200.
Strictness is part of both statements. The supplied goal concerns the complex dual exponent; the manuscript title’s square bound and broader field claims are not attached formal targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
An algorithm for one size does not establish an asymptotic exponent. The definition quantifies over every positive slack and all positive sizes with one bound constant for each slack.
Algorithms are division-free arithmetic programs with constants and input gates of cost zero and addition, subtraction and multiplication of cost one. Correctness is quantified over all input matrices. The dual exponent is a real supremum of exact exponent-two shapes, using the prescribed inner-dimension ceiling.
adc7f1241b42. Goal source.Singular integral estimates can detect geometric regularity in a measure whose support has no given parametrization. The mission turns a uniform Riesz-transform bound into uniform pieces of Lipschitz images. The source manuscript presents the surrounding research claim.
Let μ be a regular measure in ℝᵈ, with d≥4 and 2≤n≤d−2. Ahlfors–David regularity means that μ(B(x,r)) is comparable to rⁿ on its support at admissible radii. Hard-truncated Riesz transforms use the kernel (x−y)/|x−y|^(n+1), excluding distances at most ε.
With fixed dimension and bounds C_AD,C_R, prove that there exist θ>0 and M≥0 such that every eligible μ satisfies
for some M-Lipschitz map g from the open n-dimensional radius-r ball, at every support point and admissible radius.
The selected formal target is OAI.RieszRectifiability.quantitative_higher_codimension_riesz_rectifiability.
The constants θ and M are uniform across the entire class of measures with the prescribed analytic bounds. This is the exact quantitative ball-image conclusion. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.
Individual rectifiable pieces with constants depending on μ do not yield this quantifier order. The Riesz bound ranges over every positive hard truncation and every scalar L² input.
Ambient space is EuclideanSpace ℝ (Fin d). Radii are positive and bounded by the extended support diameter. The hypothesis uses μ.Regular, nonnegative Riesz constants, MemLp and eLpNorm; the conclusion uses the actual measure of the intersection with a Lipschitz image. No endpoint codimensions are included.
adc7f1241b42. Goal source.