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.
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?
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.
The dial-a-ride problem (DARP) asks for minimum-cost vehicle routes that carry users from individual pick-up points to individual drop-off points, subject to vehicle capacities, time windows, route durations and a bound on each user's ride time. It models door-to-door transport for elderly and disabled people, shared taxis and on-demand microtransit. Cordeau (Oper. Res. 54(3), 2006) gave a mixed-integer formulation of the DARP and the first branch-and-cut algorithm for it, and reported that instances with up to 30 users can be solved to optimality in reasonable time. The algorithm's strength comes from families of valid inequalities: linear constraints satisfied by every feasible route plan that cut off fractional points of the linear relaxation. Several of these families were adapted from the precedence-constrained asymmetric TSP (Balas, Fischetti and Pulleyblank 1995; Grötschel and Padberg 1985) and from the pick-up and delivery problem (Ruland and Rodin 1997); others, notably the generalized order-matching inequalities, were new in this paper.
Let be the number of users. Nodes are with pick-up nodes , drop-off nodes , origin depot and destination depot ; user travels from node to node . An instance fixes, for each node , a load , a service duration and a time window ; for each pair of nodes a travel time ; for each vehicle in a finite set a capacity and a maximal route duration ; and a maximal ride time . The standing conditions are , for , and .
A feasible solution gives each vehicle a route through distinct nodes of , start-of-service times and loads such that every node of is visited by exactly one vehicle, and are on the same route with first, and along each travelled arc, the ride time lies in , the route lasts at most , and the time windows and capacity bounds hold at every visited node. These are the constraints (2)–(14) of the paper's model.
The arc variables are when vehicle travels from to , and . For a node set write , , , , and . An inequality in is valid for the DARP when the aggregated arc variables of every feasible solution satisfy it.
Let be distinct users and let satisfy and . Then every feasible solution satisfies
The handle and the teeth are not required to be disjoint from one another beyond , and is arbitrary.
The mission also states the other propositions of §4: the lifted subtour elimination inequalities (33) and (34) (Propositions 1 and 2), the predecessor inequality (30), the two liftings (36) and (37) of the generalized order constraint (Propositions 3 and 4), the redundancy of the strengthening (40) of (39) under (30) for fractional points (Proposition 6), and the infeasible path inequality (41) under the triangle inequality for travel times (Proposition 7).
Valid inequalities are what make branch-and-cut work: each family is added to the linear relaxation by a separation heuristic, and the paper's computational section reports how the bound improves as families are added. Validity is the one property the algorithm cannot check at run time, since a cut that removes a feasible route plan silently returns a suboptimal answer. Remark 2 of the paper observes that (39) is stronger than the TSP comb inequality on the same sets, and Proposition 6 shows that its natural strengthening adds nothing once the predecessor inequalities (30) are present, which tells an implementer which families to separate.
All propositions are proved in the paper, partly in an appendix; none is formalized. A machine-checked development would give a precise route-based model of the DARP that later DARP and pick-up and delivery papers can reuse, and certified validity of the cut families that branch-and-cut codes for these problems separate.
The proofs are short on paper but argue about the shape of routes: "there exists a path connecting all nodes in ", "this path cannot finish at node because of the precedence constraint". Turning a tight subtour count into a single covering path requires knowing that the arcs of a feasible solution inside a subset of form vertex-disjoint paths, which in turn rests on each node of having exactly one predecessor and one successor and on routes containing no cycles. The arithmetic step from tight teeth to the bound on the handle needs the degree identities for every subset of , and counting the arcs leaving needs the distinctness of the users . Reasoning directly with the linear constraints (2)–(14) does not suffice: those constraints alone do not exclude cycles of zero duration.
Nodes are natural numbers, so and appear literally; , , and are Finset.range (2n+2), Icc 1 n, Icc (n+1) (2n) and Icc 1 (2n). All data and arc variables are real-valued, and every right-hand side is computed in . Feasible solutions are route-based: each vehicle has a duplicate-free list of nodes of , and the constraints of the model are imposed along that list. Read literally, the program (1)–(14) admits closed cycles when around a cycle, on which every proposition fails, and imposes (11)–(13) also at nodes a vehicle does not visit; the route encoding follows the paper's verbal definition of the DARP and its proofs, which reason about routes. Precedence ( before ) is a field of the solution, since with zero travel and service times the nonnegativity of ride times does not order the visits. The routing cost plays no role and is omitted. No positivity is assumed for travel or service times.
Added hypotheses, each necessary: sets in the subtour bound and in (30) are nonempty ( gives ); the users of Proposition 5 are distinct; the generalized order constraint (Propositions 3 and 4) has (for it is false); the ordered sets of Propositions 1 and 2 have nodes, the standing assumption of the paragraph that introduces them; Proposition 7 has and a path through distinct nodes. Proposition 6 is the only statement about fractional points: it assumes nonnegativity, no loops, (2), (3) and (30), and drops the remaining constraints of the relaxation, which makes it stronger.
The inequalities are stated for the arc variables of every feasible solution, not for an arbitrary – vector satisfying a few degree constraints; a statement of the latter kind is a different and false theorem. Useful contributions include the path structure of the arcs of a feasible solution inside a subset of , the degree identities, and the milestone proofs, which are reusable for the other propositions.
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 .In an online decision problem a decision maker chooses actions one period at a time, and only after each choice learns what that choice cost. The classical instance is prediction with expert advice: each day one of experts is followed, and afterwards every expert's loss is revealed. The goal is a strategy whose total cost is close to that of the best single fixed action in hindsight, whatever the sequence of costs.
Many structured problems have exponentially many actions, such as paths in a graph whose edge delays change daily. Weighted-majority methods keep one weight per action and are then inefficient. A. Kalai and S. Vempala (J. Comput. System Sci. 71 (2005) 291–307) showed that it suffices to be able to solve the offline problem: given total costs, find the best single action. Their algorithm, Follow the Perturbed Leader (FPL), adds a random perturbation to the accumulated costs and calls the offline solver once per period. The idea goes back to J. Hannan (1957); the paper's analysis made it short and broadly applicable, and FPL has since become a standard tool in online learning and online combinatorial optimization.
Timeline.
Decisions and states are vectors in . The decision set is a possibly infinite set and the state set is . In period the decision maker picks , then the state is revealed, and the cost is the dot product . The state sequence is fixed in advance (an oblivious adversary).
Write , with . The offline oracle is a map with
Because costs are linear, the best fixed decision after periods has cost
Three parameters measure an instance, with :
FPL(), for a parameter : in each period , draw uniformly at random from the cube and play . Its expected cost is .
Hannan(): the same rule with uniform on .
For every state sequence and every ,
The constants are the paper's. With the expected regret is at most .
For any state sequence in , any and any ,
This bound needs no knowledge of . It is included as a separate theorem, not a milestone of the goal.
The result. Theorem 1.1(a) reduces online linear optimization over any decision set to its offline counterpart, at the price of one oracle call per period and regret . Applied to online shortest paths, spanning trees and other combinatorial problems it gives efficient algorithms where weighted majority would maintain exponentially many weights. Later uses of FPL (approximate oracles, robust optimization via online learning) start from this bound.
Formalizing it. The theorem has been proved in print for twenty years; it has no machine-checked proof that we know of. The platform already holds a formalization of Ben-Tal, Hazan, Koren and Mannor's approximate-oracle variant (OracleRO.ApproxFPL), which takes a maximising oracle and an oscillation bound and therefore yields a weaker constant () in this setting. This mission states the exact-oracle bound with the paper's constant , where bounds itself. A correct proof must handle that constant carefully; see the next section.
Display (4), Lemma 3.1 and display (5) are finite-sum arguments from the defining property of . Lemma 3.2 is a statement about Lebesgue measure of a cube and its translate.
The central difficulty is the stability step: bounding, period by period, how much worse it is to play than . The obvious argument says that the two perturbed points have laws that agree on a fraction, and on the rest "one can only be larger". Under the printed definition of the difference of two costs can be as large as , so this per-period bound fails for costs of mixed sign: with , and suitable , the per-period difference is , while . The theorem itself, with , remains true, but a proof cannot proceed by the per-period comparison as written. Proving the goal with the stated constant, rather than , is the substantive part of the mission.
Fin n → ℝ; is dotProduct (⬝ᵥ); is written out as ; is the Lean norm ‖x‖, which on Fin n → ℝ is the sup norm. The sets are Dset and S; the diameter is Ddiam.s : ℕ → Fin n → ℝ indexed from (s 0 is unused); the hypothesis is imposed for .IsArgminOracle Dset M: and for all . Every theorem quantifies over all such ; the oracle is never a chosen Classical.epsilon minimiser.OracleRO.ApproxFPL.FPL: prefixSum s t ; perturbLaw n ε, the uniform law on ; and fplExpectedReward M s ε T , which with an argmin oracle is the expected cost of FPL() (its name reflects a maximisation source). Using one integral per period is the paper's own observation that fresh and shared perturbations give the same expectation.Contributions welcome: proofs of the milestones, the goal and Theorem 3.3, and reusable lemmas on uniform laws over translated cubes.
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)).
Principal component analysis estimates the eigenvalues of a population covariance matrix by those of the sample covariance matrix . Before random matrix theory turned to the regime where the dimension grows with the sample size, the classical question was the opposite one: the number of variables is fixed and the number of samples tends to infinity. In that regime almost surely, and the next question is the size and shape of the fluctuations of the sample eigenvalues. When has a repeated eigenvalue, the sample eigenvalues near it do not fluctuate independently: they repel each other, and their joint limit law is that of the eigenvalues of a random Hermitian (or symmetric) matrix. Anderson (1963) derived these limits for real Gaussian samples.
Baik, Ben Arous and Péché (2005) study complex Gaussian samples whose covariance matrix is the identity apart from finitely many "spiked" eigenvalues, and find a phase transition for the largest sample eigenvalue as together. Their Proposition 1.1 is the fixed-dimension counterpart: with fixed and all population eigenvalues equal, fluctuates on the scale with the law of the largest eigenvalue of a Gaussian unitary ensemble (GUE). The paper places it beside its Theorem 1.1(b), where a -fold spike above the critical value gives the same GUE limit when . This mission formalizes Proposition 1.1.
Fix and . A standard complex Gaussian is with independent centred real Gaussians of variance , so . For each , let , , , have independent standard complex Gaussian entries (sampleLaw M k), and let the samples be : mean zero, covariance . The sample covariance matrix is
a Hermitian matrix (sampleCov), and is its largest eigenvalue (largestEig). The general model sampleVec U ℓ G m is specialized to and , because a Hermitian matrix with all eigenvalues equal to is .
Write (vandSq). The finite-GUE distribution (Definition 1.2) is
the distribution function of the largest eigenvalue of a GUE matrix. In Lean these are G k x and Z k.
For every real and every ,
The second statement is in probability.
With , , and :
The proposition identifies the fixed-dimension limit of the top sample eigenvalue under a degenerate population spectrum: the sample eigenvalues near , rescaled by , behave like a GUE spectrum, and like its maximum. For it reduces to the central limit theorem for the sample variance of one complex Gaussian variable, with limit by (29). For general it shows that the GUE limit of the supercritical regime in Theorem 1.1(b) is already present when the dimension does not grow.
The result is proved in the paper (§5, p. 1691) by an exact computation. No machine-checked proof of it, of the complex Wishart eigenvalue density, or of the Gaussian and Laguerre cases of Selberg's integral is known to exist in Mathlib or on the platform. The formalization requires the joint eigenvalue density of a complex Wishart matrix (a Weyl-type integration formula over the unitary group), two Selberg-type integral evaluations, a Stirling asymptotic for products of factorials, and a dominated-convergence argument on . The first three are reusable well beyond this mission.
The limit itself follows from (304) and the constant asymptotics. The hard part is (302): passing from the law of the matrix to the joint law of its eigenvalues. This requires the change of variables with unitary, the Jacobian , and the integration over the unitary group. A direct central limit argument for the entries of gives the Gaussian limit of as a GUE matrix. To get from there to one needs the continuity of the largest eigenvalue in the matrix entries and a matching normalisation, so it is a different route from the paper's. Either route requires spectral facts about Hermitian matrices that Mathlib does not yet package. The Selberg evaluations (27) and (303) are classical but have no short proof: the standard arguments use orthogonal polynomials or an induction with a Dixon–Anderson type integral.
(sampleLaw M k).real of explicit sets.Contributions are welcome on each milestone. Particularly reusable are the complex Wishart eigenvalue density, the Gaussian and Laguerre Selberg integrals, and the measurability and continuity of eigenvalues of Hermitian matrix families.
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.In the local model of differential privacy, no trusted curator ever sees the raw data: each individual randomizes their own record before handing it to the analyst. This is how private telemetry is collected in practice (randomized response and its descendants), and it raises a basic question: which learning tasks remain possible when the learner only sees locally randomized records?
Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith answered it in What Can We Learn Privately? (arXiv:0803.0924v3, the accepted version of SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090; theorem numbers below are the arXiv v3's). They showed that local private learning is equivalent, up to polynomial factors, to learning in Kearns' statistical query (SQ) model (Kearns 1998), where an algorithm sees a distribution only through approximate expectations. This mission formalizes one direction of that equivalence: every SQ algorithm can be run by a local algorithm (§5.1.1, Theorem 5.7). The other direction (Lemma 5.8) is a separate mission of this series.
Timeline. Blum, Dwork, McSherry and Nissim (PODS 2005) observed that SQ algorithms can be simulated by a trusted curator adding noise to sums. Dwork, McSherry, Nissim and Smith (TCC 2006) introduced the Laplace mechanism. Kasiviswanathan et al. (FOCS 2008; journal version 2011) showed the simulation works even in the local model, with each record entering a single randomizer.
A database is a vector ; two databases are neighbors if they differ in exactly one entry. A randomized algorithm is -differentially private if for all neighbors and all measurable sets of outputs. An -local randomizer is an -differentially private map applied to a single record: for all .
The Laplace distribution has density .
An SQ oracle for a distribution on receives a query and a tolerance , and may return any with . An SQ algorithm with queries asks , where may depend on the earlier answers (adaptive), and outputs a function of all answers. A vector is a valid transcript against if every is within of the true mean of the query asked at that point.
For one query , the randomizer with is applied to each record, and the local algorithm outputs the average . The simulation of an SQ algorithm answers its -th query by running on the -th block of fresh entries and finally outputs what the SQ algorithm outputs on these answers.
There is an absolute constant such that, for every SQ algorithm with queries into , and every ; the accuracy claim further takes every tolerance at least , , and :
On that event the simulation outputs exactly what the SQ algorithm outputs against a valid oracle. The constant is left unspecified, as in the paper.
Theorem 5.7 is the inclusion "SQ ⊆ local" in the paper's characterization of local private learning: every concept class learnable with statistical queries is learnable by an -local algorithm, with sample size growing like . Combined with the converse simulation (Lemma 5.8), it identifies local private learnability with SQ learnability (Theorem 5.14). It thereby transfers the known SQ lower bounds, such as the one for parity, to the local model. It also shows that nonadaptive SQ algorithms become noninteractive local protocols.
The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization fixes what "the simulation gives the same output" means against an adversarial oracle and an adaptive algorithm. It also supplies reusable Lean objects for local differential privacy, Laplace noise and SQ algorithms.
The privacy half is the easy-looking part, but it is adaptive: the query asked in block depends on the noisy answers from blocks . A database change in block therefore changes the law of all later answers, not only . The argument must use that every entry enters exactly one randomizer and compose along the adaptive transcript.
The accuracy half has the same adaptivity issue: the union bound over queries needs, for each , the failure probability of block conditioned on everything before it. That is where the fresh blocks and measurability are used. The concentration step for Laplace averages is sub-exponential, not sub-Gaussian. The naive use of the paper's appendix lemma (A.3) fails: it is stated as an equality for every deviation , but its proof only covers deviations of order the Laplace scale.
Databases are Fin n → D (0-based). Randomized algorithms are identified with the laws of their outputs (Measure); differential privacy is required on all measurable sets. An SQ algorithm is a deterministic adaptive strategy (SQAlg): a randomized one is a mixture over its coins, to which the result transfers. "At most queries" is "exactly " after padding with dummy queries. Queries are real valued with , as the paper allows after Definition 5.4. Block consists of the database indices , so the blocks are disjoint by construction, and the simulated answers are a deterministic function of the database and the noise array. The natural logarithm replaces the paper's base 2, which only changes . Constants are existential and quantified before everything else.
Explicit choices, each recorded in the item that makes it:
A trivializing formalization is ruled out: the oracle is not replaced by the exact expectation, accuracy is required for every query actually asked (not only the first), privacy holds for every database (not only i.i.d. samples), and the constant cannot depend on , , , , or the algorithm.
Needed infrastructure: the Laplace distribution as a probability measure and its moment generating function, a Hoeffding bound for bounded i.i.d. variables, the Laplace mechanism, and adaptive composition along a transcript. All of these are reusable beyond this mission. Proofs of the milestones, of standalone Laplace and composition lemmas, and of the goal are welcome.
Markov decision processes assume that the transition law is known exactly. In practice it is estimated from data, and the optimal policy computed for the point estimate can perform badly when the true law differs. Robust dynamic programming replaces each transition law by a set of plausible laws and evaluates a policy by its worst-case expected reward over that set. The worst case is taken against an adversary (nature) who may choose a law from the set at every step.
For this worst case to be computable by backward induction, the set of path measures of a policy has to decompose epoch by epoch. Garud Iyengar named this property Rectangularity and proved that under it the classical finite horizon theory carries over: a robust Bellman equation holds, and deterministic Markov policies are optimal among all history dependent randomized policies, with state and action sets that may be countably infinite and ambiguity sets that need not be convex (Iyengar, CORC Tech Report TR-2002-07, rev. 2004; published in Math. Oper. Res. 30(2), 2005).
Timeline:
A finite horizon ambiguous Markov decision process (AMDP) has decision epochs , , and a terminal epoch . States lie in a countable set and actions in a countable set . In state at epoch the admissible actions form a nonempty set . For each admissible action , the next state is drawn from some probability measure , where is a nonempty set of probability measures on , the ambiguity set. The decision maker receives when is taken in and the next state is , and at the terminal epoch.
A history at epoch is . A policy assigns to each history a probability measure on . It is deterministic () if every is a point mass, and deterministic Markov () if moreover the chosen action depends on the current state alone. denotes all history dependent randomized policies.
Under Rectangularity (Assumption 1), the set of path measures consistent with is a product of one-epoch sets: nature chooses, for every epoch , every history and every admissible action , a measure , and the path measure is . The robust value of from and the robust value function are
The optimistic values , replace the infimum over by a supremum.
For , depends on only through ; for , ; and
The mission also contains, as a draft theorem that is not a milestone, the per-policy identity of the proof of Theorem 1, eq. (12): for each policy, .
Theorem 2 is the basis of robust dynamic programming in finite horizon: computing an optimal robust policy reduces to backward passes, each a family of one-stage problems . It also justifies restricting attention to deterministic Markov policies, which is what every algorithm in the robust MDP literature computes. Theorem 1 isolates the role of Rectangularity: without it the worst case over path measures does not decompose and the recursion characterizes nothing.
The results are proved on paper; no machine-checked proof is known. The platform holds the finite-state, Markov-controller special case (the Nilim–El Ghaoui RobustMDP series, posed, not proved), whose comparison class is too small to express the claim suffices against . A formal proof here supplies the history dependent policy and adversary machinery on countable spaces that the discounted robust theory and the robust MDP literature reuse.
The obvious argument writes the robust value as an inf–sup over path measures and pushes the infimum inside the expectation epoch by epoch. That step is the content of (12): the infimum of an expectation equals the expectation of an infimum only because nature's continuation choice may depend on the realized action and next state, so near-worst continuations for different branches can be glued into one admissible adversary. Infima need not be attained (the ambiguity sets are arbitrary, the state set countable), so the gluing is an -argument over countably many branches. The supremum over policies needs a matching splicing of -optimal continuation policies (13)–(14). Finally, randomized decision rules must be eliminated (15), which uses Rectangularity again, now per action. Restricting either the policies or the adversary to Markov ones from the start is not allowed: it changes the comparison class and makes the goal circular.
S and one countable action type A serve all epochs; the page's epoch-dependent sets embed into their disjoint union. Epochs are 0-based natural numbers, with terminal epoch M.N and 1 ≤ N.(Fin n → S × A) × S. Probability measures are PMF; as a tsum. The expected reward under a policy and an adversary is computed by backward iterated sums, which is the expectation under the product path measure (3).t < N; the supremum over equals that over the page's because uses only . An adversary chooses for every epoch, history and admissible action.Definitions: AMDP, History, History.extend, IsPolicy, Policy, IsDeterministic, IsDetMarkov, Adversary, Selection, expect, expTail, expectedReward, V, Vstar, Vbar, VbarStar, all in RobustDP.FiniteHorizon. Lemmas about gluing adversaries along history prefixes and about suprema of bounded families indexed by subtypes are reusable. Contributions to any milestone are welcome, in any order; (15) is a one-epoch statement independent of the rest.
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.
A mathematical program with complementarity constraints (MPEC, also called MPCC) is a nonlinear program in which some pairs of constraint functions must be nonnegative with at least one of each pair equal to zero. Such programs model bilevel optimization, Stackelberg games, contact problems in mechanics, and traffic equilibrium design; see Luo, Pang and Ralph, Mathematical Programs with Equilibrium Constraints (Cambridge University Press, 1996). The complementarity constraints make every standard constraint qualification of nonlinear programming fail at every feasible point: neither LICQ nor MFCQ ever holds. Off-the-shelf NLP theory and solvers therefore do not apply directly.
Relaxation methods work around this by replacing the MPEC with a family of ordinary nonlinear programs indexed by a parameter and letting . The oldest of these is the global relaxation of Scholtes (SIAM J. Optim. 11, 2001). The relaxed programs are only useful if they are themselves well posed: a local minimizer of a relaxed program should carry Lagrange multipliers, so that the sequence of KKT points the method computes actually exists. Hoheisel, Kanzow and Schwartz (Preprint 299, Univ. Würzburg, 2010; published in Mathematical Programming) compare five relaxation schemes, prove convergence under weaker MPEC constraint qualifications than before, and ask which standard constraint qualification the relaxed programs satisfy. This mission formalizes their answer for Scholtes' scheme, Theorem 3.2.
A standard nonlinear program (2) on minimizes subject to and for finitely many and . At a feasible , the active set is . A family is positive-linearly dependent if some combination vanishes with and not all coefficients zero. The Mangasarian–Fromovitz constraint qualification (MFCQ) holds at if the gradients are linearly independent and some direction has for every active and for every .
The MPEC (1) minimizes subject to
with continuously differentiable data. At a feasible point the indices of the complementarity pairs split into (), () and (). The tightened program TNLP replaces each pair by equalities on the components that vanish at and a sign constraint on the other. MPEC-MFCQ holds at if standard MFCQ holds for TNLP at .
Scholtes' relaxed program , for , keeps , , , and replaces by . Its feasible set is . Lean notation: the MPEC is MPEC n m p l, TNLP is P.TNLP xs, is P.RS t, and MFCQ of an NLP Q at x is Q.IsMFCQ x.
If is feasible for the MPEC and MPEC-MFCQ holds at , there are a neighbourhood of and such that
The neighbourhood is fixed before and works for every .
Theorem 3.2 says that the relaxed programs inherit a standard constraint qualification from the MPEC. Consequently every local minimizer of near is a KKT point, which is exactly the hypothesis of the convergence theorem for Scholtes' method (Theorem 3.1 of the paper: limits of KKT points of are C-stationary under MPEC-MFCQ). Without it, the convergence theorem could be about sequences that do not exist. The result also replaces the MPEC-LICQ-based regularity results of earlier work by the weaker MPEC-MFCQ.
The theorem is proved in the paper; to our knowledge no part of this theory has been machine-checked. A formal development delivers a reusable layer for nonlinear programming in Lean: positive-linear dependence, MFCQ and its dual characterization, the tightened program of an MPEC and the MPEC constraint qualifications. Sibling missions of this series formalize Theorem 3.1 and the Kadrani–Dussault–Benchakroun relaxation (Theorem 3.5) on the same vocabulary.
The obvious argument is a continuity argument: MFCQ is an open condition, so it should persist near . This fails as stated, because MFCQ for is not a perturbation of MFCQ for TNLP: the two programs have different constraints, and the active set of at changes with and . Near a biactive index , the product constraint can be active, and its gradient tends to zero as . So it cannot be treated as a small perturbation of any gradient in the TNLP family. In addition, the neighbourhood must be uniform in , while the active product constraints depend on . The step that needs care is the regrouping of the multiplier equation of into a combination of TNLP-type gradients, with every coefficient's sign accounted for. The separate step from MPEC-MFCQ to positive-linear independence needs a theorem of the alternative (Motzkin's transposition theorem), which is not in Mathlib in this form.
EuclideanSpace ℝ (Fin n); is the inner product of gradient f x with d. Indices are Fin m (0-based), and are allowed.P.IsC1 on the goal and on milestones 3–5. Milestones 1–2 do not need it.𝓝 xs chosen before .The goal would be trivialized by a weakened MFCQ, for instance one that omits the linear independence of the equality gradients or requires the strict inequality only for some of the active constraints. Such a formalization is ruled out: IsMFCQ requires both conditions, over the full active set of . The neighbourhood must be a genuine element of 𝓝 xs, so an empty is excluded.
Welcome contributions: a proof of Remark 2.2, general lemmas on persistence of positive-linear independence under continuous perturbation, and the final assembly. These lemmas apply to nonlinear programming in general, not only to this mission.
Volume-preserving box transport supplies geometric operations for a finite computation. The selected goal assembles these into a force and a fixed particle observer. The pinned manuscript supplies the research context.
A finite machine and input determine effective velocity and force coefficients. The force depends affinely on positive viscosity, and after time one the velocity is periodic and depends only on the machine.
The selected goal is OAI.BalancedTransport.balanced_three_stack_realization. Its central assertion is
The theorem states that there exist velocity fields U(M,w), force coefficients f₀(M,w) and f₁(M,w), material flows X(M,w), and a globally 1-periodic velocity field R(M) for each finite deterministic tape machine M, with the following properties for every finite input word w. On nonnegative time and ℝ³, U, f₀ and f₁ are smooth and vanish outside a common spatial compact set independent of time; every mixed space-time derivative of U is uniformly bounded. Moreover, f₀ = ∂ₜU + (U·∇)U and f₁ = −ΔU. All three families are uniformly effective from the encoded machine and input: algorithms approximate every mixed derivative component at rational space-time points within 2⁻ⁿ, provide global integer bounds on these derivatives, and provide integer support radii. The velocity is 1-periodic after time 1 and satisfies U(M,w)(t,x) = R(M)(t,x) for every t ≥ 1, so its later field depends only on M. The flow satisfies X(0,a) = a and ∂ₜX(t,a) = U(t,X(t,a)); its trajectory starting at (4,0,0) enters (−1,2)³ at some nonnegative time exactly when M halts on w, meaning that a configuration with no next transition is reached after finitely many machine steps. For every viscosity ν > 0, the force f = f₀ + νf₁ is smooth, has uniformly bounded mixed derivatives, and is 1-periodic after time 1; U with pressure zero solves the incompressible Navier–Stokes equation ∂ₜU + (U·∇)U = νΔU + f with U(0,·) = 0. This velocity is unique among smooth zero-data solutions in the comparison class, and every such solution has spatially constant pressure. The comparison class requires the velocity and all spatial derivatives through order two to be continuous in time as L² functions, the velocity to be continuously differentiable in time in L², velocity and first spatial derivatives to be bounded on each finite time slab, and pressure, after subtracting a time-dependent scalar, together with its first spatial derivatives to be continuous in time in L²; (U,0) belongs to this class. Finally, derivative approximations and global derivative bounds for f are computable when ν is computable, and computable relative to any rational name of ν whose nth approximation has error at most 2⁻ⁿ.
The balanced three-stack realization is the main goal; balanced box routing is a separate supporting reference. The exact conclusion permits spatially constant pressure in competing solutions and explicitly states its comparison 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.
Uniform effectiveness, compact support, periodic behavior and uniqueness must all coexist with exact halting detection.
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.
Additional published targets are included as separate references:
adc7f1241b42. Selected goal source.A force whose derivatives decay rapidly can still encode a computation in a particle trajectory. The selected construction makes the observer condition and effectiveness requirements precise. The pinned manuscript supplies the research context.
For each finite deterministic machine and valid input, compilers produce smooth force and velocity fields on nonnegative time and real three-space, with common compact spatial support.
The selected goal is OAI.AlternatingNS.alternating. Its central assertion is
The theorem states that for every positive real viscosity ν computable by rational approximations with error at most 2⁻ⁿ, there exist computable compilers for a force f and velocity U, and one compact set K⊂ℝ³, with the following property for every well-formed finite deterministic Turing machine M and valid finite input w. The compiled programs describe smooth fields f,U on [0,∞)×ℝ³, both spatially supported in K for all nonnegative times, such that every mixed space-time derivative D satisfies sup_{t≥0,x}(1+t+‖x‖)ᴶ‖Df(t,x)‖<∞ and the analogous bound for U, for every nonnegative integer J. Each program supplies rational approximations to all mixed derivatives at rational space-time points with requested error 2⁻ᵏ, effective moduli of continuity on bounded regions, and integer bounds for all these weighted derivative norms. The velocity starts from zero, is divergence-free, and solves the classical forced Navier–Stokes equation ∂ₜU+(U·∇)U=νΔU+f with identically zero pressure; specifically f=∂ₜU+(U·∇)U−νΔU. On every interval [0,T], U is continuous in H² and continuously differentiable in L², and U and its spatial derivative are uniformly bounded in space and time. Moreover, any classical solution (v,p) with the same force and zero initial velocity equals (U,0) pointwise for all nonnegative times, provided on every [0,T] it has v continuous in H², continuously differentiable in L², and uniformly bounded, and p continuous in H¹. Here these Sobolev continuity conditions mean continuous L² representatives of every spatial derivative through the indicated order; time derivatives at zero are taken within [0,∞). Every initial point a has a unique trajectory X(a,t) for t≥0 satisfying X(a,0)=a and ∂ₜX(a,t)=U(t,X(a,t)). Finally, the trajectory starting at (−1,0,0) has strictly positive first coordinate at some nonnegative time if and only if M halts on w, where encountering a missing instruction also counts as halting.
The goal is the alternating-coordinate construction at every positive computable viscosity. It includes Sobolev time regularity, effective bounds, zero initial velocity and the exact observer condition, rather than all three manuscript constructions. 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 encoding must preserve all weighted derivative bounds and uniqueness in the stated comparison class while recording arbitrarily long computations.
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.Incompressible transport can implement prescribed geometric operations on coding sheets. The selected statement concerns one such finite transport construction with effective smooth forcing. The pinned manuscript supplies the research context.
Source and target rectangles have rational data and specified positive diagonal ratios. In the formula, D_i(y)=q_i+diag(r_i)(y−p_i), with source and target centers p_i and q_i. Space is represented periodically with period ten, and the viscosity is a positive computable real.
The selected goal is OAI.Solenoidal.sheet_theorem. Its central assertion is
The theorem states that, for any natural number N, any sheet datum D of size N, and any computable real viscosity ν>0, there exist a forcing field f and a velocity field u (each a time-dependent vector field on ℝ³) and a flow map X such that the following hold. Here D consists of N source rectangles and N target rectangles with rational corners, all inside the square [2,3]², with the sources pairwise separated by a positive distance and likewise the targets, together with positive rational ratios in each of two coordinates such that the diagonal affine map from source i to target i, which sends the source center to the target center and scales offsets by the ratios, maps the source rectangle exactly onto the target rectangle. Both f and u are periodic in space with period 10 in every coordinate and are C^∞ in space and time jointly. The forcing f is effective, meaning that all its mixed space-time partial derivatives can be approximated to any rational accuracy by a single fixed partial recursive procedure from computable names of the evaluation point. Moreover f has zero mean over the fundamental cell [0,10)³ at every time, is divergence free, and is 1-periodic in time. The field u is a classical solution on t≥0 of the forced Navier–Stokes equations ∂ₜu + (u·∇)u = −∇p + ν Δu + f with zero pressure, zero initial data, incompressibility and spatial periodicity, so u is a solution driven by f without pressure. Any classical solution v with pressure p for the same f and ν and with zero initial velocity coincides with u, and has p identically zero, for all t≥0. The flow map X satisfies X(0,a)=a and solves the particle-path equation dX/dt=u(t,X) for t≥0, and for each i and each point y of the i-th source rectangle, the time-1 flow image of the sheet point (y₀,y₁,2) agrees modulo the torus ℝ³/(10ℤ)³ with the sheet point at the diagonal-map image of y. Further, u vanishes in a neighborhood of every integer time, the advection term (u·∇)u vanishes everywhere, and both f and u have all their mixed space-time derivatives uniformly bounded by rational bounds computable from the derivative multi-index by a fixed partial recursive procedure. Finally, if N=0 then f and u are identically zero.
The target is the sheet theorem, including its encoded uniqueness statement and zero-advection conditions. Machine-halting detection is not a conclusion of this published goal. 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 construction must simultaneously enforce smoothness, incompressibility, temporal periodicity, effective bounds and exact transport on every point of each sheet rectangle.
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.An optimal coupling can exist even when no deterministic transport maps attain its cost. The target separates attainment from equality of infima for a three-marginal repulsive cost. The pinned manuscript supplies the research context.
All three marginals are the same smooth compactly supported probability density in real three-space, with smooth compactly supported square root. Coincident points have infinite Coulomb cost.
The selected goal is OAI.Problem356.coulomb_counterexample_and_equal_infima. Its central assertion is
The theorem states, without a proof being verified here, that there exists a function ρ on three-dimensional Euclidean space ℝ³ satisfying a full Coulomb conclusion. This means ρ is a nonnegative C^∞ function with compact support, whose square root is also C^∞ with compact support, and with integral 1 over ℝ³; its density measure μ (Lebesgue measure weighted by ρ) is a probability measure. Consider three-marginal couplings of μ, namely probability measures on triples (x,y,z) of points of ℝ³ all of whose three coordinate marginals equal μ, with cost 1/|x−y| + 1/|x−z| + 1/|y−z| valued in [0,∞] (the inverse of distance zero is ∞). The Kantorovich value of μ is the infimum of the expected cost over all such couplings, and the theorem asserts it is finite and attained by some coupling. Further, no pair of measurable maps T₂,T₃ each preserving μ (pushing μ forward to itself) is a Monge optimizer: for every such pair, the expected cost of the triple (x,T₂x,T₃x) under μ is strictly larger than the Kantorovich value. Nevertheless, the Monge value, the infimum of this graph cost over all such pairs of μ-preserving maps, equals the Kantorovich value, and for every ε>0 there are μ-preserving maps T₂,T₃ with finite graph cost at most the Kantorovich value plus ε.
The goal includes a finite attained Kantorovich value, no Monge minimizer, equal infima and arbitrarily accurate finite-cost maps. Other dimensions and Riesz exponents are not part of this selected target. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Every measure-preserving pair of maps must be strictly suboptimal, while a sequence of such pairs still approaches the coupling minimum.
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.Homogeneous minimizers model possible free-boundary singularities. A nonflat example in seven dimensions supplies one side of the claimed critical-dimension threshold. The pinned manuscript supplies the research context.
The one-phase Bernoulli energy on a ball is the integral of squared weak gradient plus the indicator of positivity. Competitors are nonnegative Sobolev functions with the prescribed H1-zero-boundary difference.
The selected goal is OAI.Bernoulli.nonflat_in_seven. Its central assertion is
The theorem states that there exists a function u: ℝ⁷ → ℝ that is nonnegative almost everywhere, belongs locally to H¹, and is a global minimizer of the one-phase Bernoulli energy E_B(u) = ∫B (|∇u|² + 1{u>0}) dx. Here ∇u is a distributional gradient, and global minimality means that, for every open ball B of positive radius and every nonnegative almost-everywhere Sobolev competitor v ∈ H¹(B) with v − u ∈ H¹₀(B), one has E_B(u) ≤ E_B(v). Membership in H¹₀(B) requires approximation by smooth functions compactly supported in B, with both the functions and their gradients converging in L². The function is nonzero in the sense that it is not equal to zero almost everywhere, and it is homogeneous of degree one: for each real r > 0, u(rx) = r u(x) for almost every x. Nevertheless, it is not flat: there is no unit vector e ∈ ℝ⁷ for which u(x) = max(⟨x,e⟩, 0) almost everywhere. All almost-everywhere statements and integrals use Lebesgue measure.
The selected goal is existence of a nonzero nonflat one-homogeneous global minimizer in dimension seven. Flatness in dimensions at most six and singular-set dimension bounds are not attached conclusions. 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 stationary cone is insufficient: the example must minimize against all admissible ball competitors and fail every half-space profile.
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.Negative curvature suggests strong analytic control, but bounded holomorphic coordinates impose a different global condition. The target constructs a complex threefold separating them. The pinned manuscript supplies the research context.
The construction uses the encoded Hartogs domain and a complete Kähler metric with sectional curvature between two negative constants. Holomorphic coordinate obstructions are stated in the published main proposition.
The selected goal is OAI.PinchedHartogs.main_theorem. Its central assertion is
The theorem states that there exist a subset M of ℂ³ (realized as ℂ² × ℂ) and a matrix-valued function g assigning a 3×3 complex matrix to each point, together with real numbers A and B, such that M is open, nonempty and contractible, and g is a Kähler metric on M, meaning g is C^∞ on M, Hermitian at each point (g_ij = conj(g_ji)), positive definite (the Hermitian form of g at u has positive real part for every nonzero u), and satisfies the closedness condition ∂g_kj/∂z_i = ∂g_ij/∂z_k, with ∂ the Wirtinger derivative (1/2)(∂_x − i∂_y). Moreover the metric is geodesically complete on M: for every point p in M and every vector v there is a C^∞ curve γ: ℝ → M with γ(0)=p, γ'(0)=v that satisfies the geodesic equation γ''k + Σ Γ^k{ac} γ'_a γ'_c = 0 for all t, where the Christoffel symbols are built from the inverse of g and the ∂ derivatives of g. The metric is also negatively pinched: 0 < A ≤ B and, for every point of M and every real-linearly independent pair u, v, the sectional curvature, computed from the explicit curvature tensor formula in the source, lies between −B and −A. In addition, M has no bounded coordinates: there is no map F from ℂ³ to ℂ³, holomorphic on a neighbourhood of every point of M and bounded in every component on M, whose complex Jacobian determinant is nonzero at every point of M. Finally, M is not biholomorphic to a bounded domain, that is, there is no bounded open set N with holomorphic maps F on M and G on N, each analytic near the respective set, mapping M into N and N into M, which are mutually inverse.
The selected main theorem requires a nonempty open contractible domain, a geodesically complete Kähler metric with two-sided negative real-sectional pinching, no bounded holomorphic map to complex three-space with everywhere-nonsingular differential, and no biholomorphism to a bounded domain. The controlled potential and metric-transfer statements are attached as supporting milestones. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Metric completeness and two-sided negative curvature must coexist with a global obstruction to bounded holomorphic coordinates.
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.
Additional published targets are included as separate references:
adc7f1241b42. Selected goal source.Affine maximal graphs satisfy a nonlinear fourth-order geometric equation. The target asks whether completeness forces such a locally uniformly convex graph to be a paraboloid. The pinned manuscript supplies the research context.
The dimension is between three and nine. The domain is nonempty, open and convex, the function is smooth with positive-definite Hessian, and completeness uses intrinsic Euclidean graph length.
The selected goal is OAI.AffineBernstein.affine_bernstein. Its central assertion is
The theorem states that, for every integer dimension 3 ≤ n ≤ 9, a nonempty open convex set Ω ⊆ ℝⁿ and a function u : ℝⁿ → ℝ that is smooth on Ω satisfy the following conclusion under three hypotheses. First, the Hessian H = D²u is positive definite at every point of Ω. Second, u satisfies the affine maximal equation ∑ᵢⱼ Uᵢⱼ ∂ᵢ∂ⱼw = 0 throughout Ω, where U = (det H)H⁻¹ and w = (det H)^{−(n+1)/(n+2)}. Third, the graph is complete for its intrinsic Euclidean path distance: the distance between x and y in Ω is the infimum over C¹ paths γ in Ω joining them of ∫₀¹ √(‖γ′(t)‖² + (Du(γ(t))γ′(t))²) dt, and every Cauchy sequence for this distance has a limit in Ω for the same distance. Then Ω = ℝⁿ and there exist a symmetric positive definite real n × n matrix A, a vector b ∈ ℝⁿ, and c ∈ ℝ such that u(x) = ½xᵀAx + b·x + c for every x ∈ ℝⁿ. Moreover, an invertible affine map of ℝⁿ × ℝ carries the standard paraboloid {(x, ‖x‖²)} onto the graph {(x, u(x)) : x ∈ Ω}.
The goal also gives an invertible affine map from the standard paraboloid to the graph. The wider immersed-hypersurface formulation is not included as a separate target. 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 domain is not initially assumed to be all of space. Both global domain exhaustion and the quadratic form must follow from the equation and completeness.
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.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.Fixed-point bounds compare Hamiltonian dynamics with critical points of smooth functions. Degenerate fixed points are central to the unrestricted formulation tested here. The pinned manuscript supplies the research context.
The space is the complex projective quadric threefold, represented through its unit quadric and quotient tangent directions. Hamiltonian maps are endpoints of the specified smooth isotopies.
The selected goal is OAI.ArnoldCounterexample.main. Its central assertion is
The theorem states that the complex projective quadric Q = {[z] ∈ ℂP⁴ : ∑ⱼ₌₀⁴ zⱼ² = 0} admits a Hamiltonian bijection φ with exactly three fixed points, whereas every smooth real-valued function on Q has at least four critical points, including functions with degenerate critical points; equivalently, 3 < 4 ≤ the infimum of their critical-set cardinalities, with infinite cardinalities recorded as ∞. Here Hamiltonian means that φ is the endpoint of an isotopy starting at the identity whose forward maps, inverse maps, and Hamiltonian have globally smooth extensions on ℝ × ℂ⁵. For times in [0,1], the maps preserve the unit quadric, are inverse there, and commute with multiplication by unit complex scalars; the Hamiltonian is invariant under these scalars. They satisfy ω(∂ₜFₜ(z),v) = dHₜ(Fₜ(z))[v] for every horizontal v at Fₜ(z), where ω(u,v) = 2 Im ∑ⱼ conjugate(uⱼ)vⱼ and horizontality at z means both ∑ⱼ conjugate(zⱼ)vⱼ = 0 and ∑ⱼ zⱼvⱼ = 0. Smooth functions on Q are those with smooth local extensions after pullback to the unit quadric, and criticality means that every such extension has zero derivative in all horizontal directions. Moreover, φ has a degenerate fixed point: some unit representative z and nonzero horizontal vector v admit a smooth local lift G of φ with G(z) = z and DG(z)v − v = a iz for some real a. Thus the induced derivative on the quotient tangent has a genuine nonzero eigenvector with eigenvalue 1.
The goal includes the lower bound on all smooth critical sets and at least one degenerate fixed point. A rational cup-length computation is not a separate conclusion of this target. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Counting fixed points is insufficient: the construction must satisfy the Hamiltonian lift conditions and give a genuine nonzero quotient-tangent eigenvector at a degenerate point.
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.Sharp filling inequalities compare the mass of a cycle with the least mass needed to fill it. The selected formulation extends a Euclidean coefficient to proper CAT(0) metric spaces. The pinned manuscript supplies the research context.
Integral currents are encoded metric currents with integer-multiplicity chart decompositions and integral boundary. The input is a compactly supported n-cycle for n at least two. In the displayed coefficient, σ_n=(n+1)ω_{n+1}, where ω_{n+1} is the Euclidean volume of the unit ball in dimension n+1; this is the published sphereArea convention.
The selected goal is OAI.CAT0Fillings.sharp_integral_filling. Its central assertion is
The theorem states that, for a proper metric space X with its Borel σ-algebra that is CAT(0), meaning there is a choice of geodesic parametrization segment(x,y,t) from x to y (with segment(x,y,0)=x, segment(x,y,1)=y, and dist(segment(x,y,s),segment(x,y,t))=|s−t|·dist(x,y) for s,t in [0,1]) satisfying the comparison inequality dist(segment(o,x,s),segment(o,y,t))² ≤ (s·d(o,x) − t·d(o,y))² + s·t·(d(x,y)² − (d(o,x) − d(o,y))²), the following filling property holds for every integer n ≥ 2. Let T be an integral n-current on X, that is, a metric current (a multilinear functional on a bounded Lipschitz function and n Lipschitz functions, with locality, continuity and finite mass) that is a countable sum of disjointly supported integer-multiplicity bi-Lipschitz chart pieces and whose boundary has the same properties, and suppose T is compactly supported and a cycle, meaning its boundary is zero. Then there exists a compactly supported integral (n+1)-current S on X whose boundary is T and whose mass satisfies mass(S) ≤ c_n · mass(T)^((n+1)/n), where c_n = 1/((n+1)·(σ_n)^(1/n)), σ_n = (n+1)·ω_{n+1} is the area of the unit n-sphere and ω_{n+1} is the volume of the unit ball in Euclidean (n+1)-space. This is an admitted theorem statement, not a verified proof.
The goal is the CAT(0) integral-current filling inequality. Euclidean coefficient optimality is an additional reference. The manifold perimeter comparison and equality-rigidity statements in the manuscript 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 sharp coefficient must hold without a smooth manifold model, while preserving integrality, compact support and the exact boundary.
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.
Additional published targets are included as separate references:
adc7f1241b42. Selected goal source.Recursive potentials can define tree norms with controlled midpoint behavior. The central question is whether that control forces an asymptotically uniformly convex renorming. The pinned manuscript supplies the research context.
The encoded constructions include root-sum and zero-root completions, finite tree heads, aggregation spaces and variable-exponent coordinate models. Two least nonnegative potential fields determine the norms.
The selected goal is OAI.ComparatorModel.RecursivePotentials.main. Its central assertion is
The theorem states (its proof is admitted with sorry) that the defined proposition MainClaim holds. MainClaim asserts that there exist constructions, over index types in universe 0, of the finite rooted tree head structure, the tree-vector spaces, the zero-root tree-vector spaces, the aggregation-vector spaces, and their l^p-coordinate models, such that eleven statements about completions of finite-support vectors on rooted trees hold simultaneously. These comprise: (1) completion statements saying that the root-sum tree space for the sequence tree and for the joined tree, and the zero-root space for the joined tree, are complete, infinite-dimensional, with continuous coordinates extending the vector coordinates, continuous potential fields P and Q extending the finite-tree ones, norm equal to P+Q at the root (or both P and Q at the root in the zero-root case, where the root coordinate vanishes), and with norm-nonincreasing idempotent coordinate projections onto initial subtrees having finite-dimensional range, closed finite-codimensional tails and approximation of tail elements by vectors vanishing on the head, and that XZero and XJoined are reflexive; (2) a main statement giving the lower bound t^3/128 on the averaged modulus of XSigma and XJoined for 0<t<1, a cubic-type uniform convexity inequality (‖x+z‖+‖x-z‖)/2 ≥ ‖x‖+‖z‖^3/(8(2‖x‖+‖z‖)^2) for x supported on a head and z vanishing there, and that no equivalent norm on XSigma, XZero or XJoined has the AUC property (positive modulus at every positive t); (3) positivity of the averaged modulus of XSigma at every positive radius t; (4) a separation statement for XJoined: for each ε>0 there is η in (0,1), equal to min(1/2, logarithmicGamma(2, ε/16)) when ε≤2, such that if ‖x±z_n‖≤1 for all n and the z_n are pairwise at distance at least ε, then ‖x‖≤1-η; (5) properties of the variable-exponent l^2-sum of height-h tree spaces with exponents 1+1/h, namely completeness, reflexivity, separable dual, a root-sum functional ν (nonnegative, definite, subadditive, absolutely homogeneous) bounded above and below by explicit multiples of the l^p norm, dense finitely supported vectors, and finite-rank projections; (6) a recursive characterization of the l^p-model potentials by least pairs, with ν equal to the root P plus Q; (7) for every equivalent norm A on the variable space, the modulus at lower/upper vanishes; (8) the absence of any equivalent AUC norm there; (9) a sixth-power stability inequality and (10) a cubic stability inequality for admissible heads, with explicit constants; and (11) a weak-tail estimate: if x and a weakly null sequence y_j with ‖y_j‖≥ε, 0<ε≤1, satisfy ‖x±y_j‖≤1, then ‖x‖≤θ(ε)<1.
The published MainClaim is an eleven-part package, not only the displayed midpoint inequality. Its additional completion, separation, stability, weak-tail and no-AUC assertions remain part of the goal. 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 bundled target must coordinate completion, continuous coordinate maps, finite-head approximations, reflexivity and uniform estimates across several related spaces.
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.Independent positive multipliers on a branching tree generate concrete subspaces of real L1. Their asymptotic geometry can distinguish midpoint estimates from AUC renormability. The pinned manuscript supplies the research context.
A nonconstant positive multiplier has probability law μ, mean one and finite second moment. Path products are multiplied along nonempty prefixes, and their L1 classes generate a closed real span.
The selected goal is OAI.IndependentProducts.main_general. Its central assertion is
The theorem states that, for any Borel measure μ on ℝ satisfying the multiplier hypotheses, the closed real L¹ span of the path products is infinite-dimensional, and no equivalent norm on it is AUC. The hypotheses say that μ is a probability measure, almost every value is positive, μ is not almost surely equal to any constant, its mean is 1, and the identity function has a finite second moment (is in L²). Vertices are finite lists of positive integers, a sample assigns a real number to each nonroot vertex, and the product measure is the infinite product of independent copies of μ, one per nonroot vertex. The path product of a vertex v multiplies the sample values at the nonempty prefixes of v, and is 1 for the root. productSpan(μ) is the topological closure, in L¹ of the product measure, of the real linear span of the classes equal almost everywhere to some path product. The theorem concludes first that productSpan(μ) is not finite-dimensional over ℝ. Second, for every seminorm N on productSpan(μ) that is an equivalent norm, meaning there are constants 0<a≤b with a‖x‖≤N(x)≤b‖x‖ for all x, N fails the AUC property, which requires that, for every t>0, the one-sided asymptotic modulus of N at t is strictly positive. That modulus is the infimum over N-unit vectors x of the supremum over closed finite-codimension subspaces F of the infimum of N(x+ty)−1 over y in F with N(y)=1. The statement is given as an admitted theorem without proof.
The selected general target asserts infinite dimension and absence of AUC renormings. Specific exponential and Gaussian-square midpoint estimates are separate published targets, retained as additional references. 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 obstruction must work for every admissible multiplier distribution and every equivalent norm, rather than only a particular exponential example.
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.
Additional published targets are included as separate references:
OAI.IndependentProducts.main_exponential (Open).OAI.IndependentProducts.main_gaussian_12 (Open).OAI.IndependentProducts.main_gaussian_24 (Open).adc7f1241b42. Selected goal source.