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?
A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, without revealing why it is true. Groth, Ostrovsky and Sahai (J. ACM 59(3), 2012) gave NIZK proofs for Circuit SAT of size for a circuit and security parameter , the first perfect NIZK arguments for all of NP, and the first non-interactive zaps based on a standard cryptographic assumption. These constructions use a single algebraic primitive, the homomorphic proof commitment: a commitment scheme with two kinds of keys, together with a short proof that a committed value is or .
The paper gives two instances of this primitive. One rests on the subgroup decision assumption in composite-order groups. The other, the subject of this mission, rests on the decisional linear assumption of Boneh, Boyen and Shacham (CRYPTO 2004) in prime-order bilinear groups. Prime-order groups are the setting of most later pairing-based proof systems, including the Groth–Sahai proofs (EUROCRYPT 2008), and their decisional-linear instantiation uses commitment keys of the same linear-tuple form as this mission.
A DLIN bilinear group is a tuple : is a prime, and are groups of order , is bilinear ( for all , ), generates , and generates . A triple is a linear tuple with respect to .
The scheme (Figure 2 of the paper) works as follows.
The perfect properties of Section 3 are: homomorphism, perfect binding, perfect extractability, perfect trapdoor opening and its indistinguishability, perfect completeness, perfect soundness, perfect witness indistinguishability (WI), and perfect non-erasure WI. Non-erasure WI asks that a simulator turn the randomness of a proof made with one witness into randomness that explains the same proof under the other witness.
For every DLIN bilinear group, the scheme of Figure 2 is homomorphic on both kinds of key and perfectly binding and extractable on binding keys. On hiding keys it has perfect trapdoor opening and perfect trapdoor-opening indistinguishability. Its 0/1 proof is perfectly complete on both kinds of key, perfectly sound on binding keys, and perfectly WI and perfectly non-erasure WI on hiding keys. Soundness, for example, reads
The milestones follow the paper's proof:
The perfect properties are what the paper's later results consume. Perfect soundness and extractability on binding keys give the perfectly sound NIZK proof of knowledge for Circuit SAT (Theorem 6). Perfect WI, trapdoor opening and non-erasure WI on hiding keys give perfect zero-knowledge (Lemma 8 and Theorem 11) and the adaptive and UC-secure variants of Sections 7 and 8. Theorem 4 transfers all of this to prime-order bilinear groups under the decisional linear assumption.
The theorem is published and its proof is short, but the printed construction contains an error. With the signs of in and as printed in Figure 2, an honest proof fails the fourth and sixth verification equations whenever . A machine-checked proof fixes the corrected construction, under which the paper's own witness-indistinguishability argument goes through. No formalization of this scheme, or of the decisional linear setting, exists on the platform or in Mathlib.
The algebra is modest. The work lies in carrying exponents in through powers in groups of order , and in getting the soundness argument right. An accepted proof only constrains discrete logarithms of the proof elements, so the six pairing equations must first be turned into six equations between exponents. That step is valid only because , and are nondegenerate. Soundness then needs the observation that the product of two specific linear forms vanishes, and it fails outright on a hiding key (). Witness indistinguishability is an exact identity between proofs, which holds only for the corrected prover.
G →* G →* GT, which is equivalent to bilinearity. generates and generates .ZMod p, acting through their representative in .Classical safety-stock formulas assume that demand is stationary: independent and identically distributed around a fixed mean. Many products do not behave that way. Their demand level drifts, and the forecast has to follow it. Graves (A single-item inventory model for a nonstationary demand process, Manuf. Serv. Oper. Manag. 1(1):50–61, 1999) works out what such drift costs in inventory when it is modelled by the simplest nonstationary time series used in forecasting practice. The model is the integrated moving average process of order , for which the exponentially weighted moving average is the optimal forecast (Muth, 1960; Box, Jenkins and Reinsel, 1994).
The paper answers two questions. For one stage under an adaptive base-stock policy, it gives the exact distribution of the inventory, and hence the safety stock. For two stages in series, it shows that the order stream the downstream stage passes upstream is again of the same type, amplified. This is an explicit instance of the bullwhip effect of Lee, Padmanabhan and Whang (1997). The paper then gives the distribution of the upstream inventory. That last distribution, equation (16), is the goal of this mission.
Time is indexed by periods ; operation starts in period . Fix a mean level , a parameter with , a downstream lead time and an upstream lead time . The shocks are independent random variables, each normal with mean and variance .
Downstream stage (§2). The demand is the IMA(0,1,1) process
The forecast , made after observing , is the exponentially weighted moving average
The order , placed in period and delivered in period , follows the adaptive base-stock policy
The inventory at the end of period (negative values are backorders) obeys
where is an initial inventory chosen by the planner. Orders may be negative.
Upstream stage (§3). It sees the orders as its demand. It forecasts them with smoothing constant ,
orders for and for (15), and holds inventory
with initial inventory .
In Lean, IsStage μ α L ε d F q x is the conjunction of (1), (3), (6), (7) and the boundary condition. IsUpstream μ β K q G p y is (11), (14), (15) and its boundary condition. upBeta α L is , and IsTwoStage is the conjunction of the two stages.
For every period (and ), the upstream inventory is normally distributed with
Two further statements of the paper are included as plain theorems: the order amplification (p. 55), stated as: and are independent of with laws and , and the critical-fractile rule (p. 54). Under that rule, setting gives .
Equation (8) is a closed-form safety-stock formula for nonstationary demand. For the standard deviation of the inventory grows faster than , so the textbook square-root law understates the safety stock. Equation (16) carries the formula one stage up a supply chain. With , the upstream safety stock depends on the downstream lead time , not only on the upstream lead time . The paper concludes that shortening the downstream lead time can matter more than shortening the upstream one. P1 and P2 underlie these conclusions: they write each inventory as a fixed linear combination of a bounded window of shocks.
All results here are proved in the paper. None of them, and none of the model's objects, is formalized on Prove2Me or, as far as is known, anywhere else. The mission produces machine-checked versions of the closed forms and distributions. It also produces a reusable statement that a finite linear combination of independent Gaussian shocks is Gaussian, which Mathlib has only for two summands.
The pathwise milestones are inductions on the period, but they are not uniform. The inventory recursion (6) reads orders periods back, so P1 has two regimes: , where every order read is a policy order, and , where some are the boundary orders . The paper treats the second regime only by "direct substitution", and a single statement has to cover both.
P2 is not a second copy of P1. The upstream stage is defined by its own recursions (11), (14), (15). It becomes an instance of the single-stage model only after (10) and the forecast identity have been proved, and P1 must then be applied with parameter and shocks . The distributional statements (8) and (16) need the law of a finite weighted sum of independent normal variables. Mathlib provides the two-variable case; the finite-sum version, with a -indexed window of shocks, has to be built from it.
All sequences are functions ; lead times are natural numbers, cast to in indices and to in coefficients, so no truncated subtraction occurs. The model is a predicate on sequences, and the objects are constrained only by the paper's recursions (1), (3), (6), (7), (11), (14), (15) and the boundary conditions for . None of the closed forms (2), (5), (9), (10), P1 or P2 is built into a definition. In particular the upstream stage is not defined as an instance of the downstream one, which would assume (10). The paper's convention for is implemented by a masked sequence masked ε in P1 and P2, not by a hypothesis. The standing assumption is a hypothesis of every theorem.
In (8) and (16) the shocks live on a probability space . They are measurable and mutually independent over periods (iIndepFun over ), each with law gaussianReal 0 (σ²). The system equations hold for every outcome, and the initial inventory is a constant. "Normally distributed with mean and standard deviation " is the law equality P.map (y t) = gaussianReal m (s²). A statement only about the variance would be weaker than the paper's claim and does not count. The critical-fractile theorem adds and ; without them the inventory is constant and the claim fails.
Contributions are welcome on the finite Gaussian-sum lemma, which is independent of this paper, and on any milestone in any order.
A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, computed from a common reference string that both parties share, without revealing anything beyond the truth of the statement. NIZK proofs were introduced by Blum, Feldman and Micali (STOC 1988) and are a building block of chosen-ciphertext secure encryption, signatures and secure multi-party computation. For a long time every NIZK proof for all of NP was zero-knowledge only computationally: a simulator produced proofs that no efficient adversary could tell apart from real ones.
Groth, Ostrovsky and Sahai (J. ACM 59(3), 2012; conference versions at Eurocrypt 2006 and Crypto 2006) gave the first NIZK argument for all of NP whose zero-knowledge is perfect: real and simulated proofs have exactly the same distribution, so even an unbounded adversary learns nothing. The construction is the Circuit SAT proof of their Figure 3, run on a perfectly hiding key of a homomorphic proof commitment scheme. Its zero-knowledge is Lemma 8 of the paper, and it is the zero-knowledge half of their Theorem 11.
A homomorphic proof commitment scheme has a message space (a finite cyclic group with generator , here ), a randomizer space and a commitment space , all finite abelian groups, and a commitment function . A hiding key generator outputs a commitment key together with a trapdoor . The scheme is assumed to have:
A NAND circuit on wires is a list of gates and an output wire ; a witness satisfies it, , if for every gate and . The prover of Figure 3, with , commits to every wire, with , proves that each commitment contains or , and for each gate proves that contains or .
The simulator is , returning and , and , which commits to on every wire except the output wire, and makes all the 0/1 proofs from openings it knows or obtains with the trapdoor. In the zero-knowledge game an adaptive adversary reads , submits pairs to an oracle one at a time, sees each answer before choosing the next, and outputs a bit. The real oracle answers with , the simulation oracle with ; both answer failure when .
For every adaptive adversary ,
where is restricted to its first output.
Lemma 8 makes the Circuit SAT argument of Section 7 the first perfect NIZK argument for every language in NP. Combined with the computational indistinguishability of binding and hiding keys it also gives the computational zero-knowledge of the proof of Figure 3 (Theorem 6), and it is the template for the perfect zero-knowledge of the universally composable NIZK of the paper's Section 8. The same simulation pattern, commit to everywhere and use the trapdoor where an opening is needed, recurs in later pairing-based proof systems such as Groth–Sahai proofs.
The result is proved in the paper; to our knowledge it has not been machine-checked. A formal proof fixes the simulator completely, including the cases the paper leaves to the reader, and makes the adaptive multi-query argument explicit: the paper's proof treats one proof at a time and does not spell out why answering many adaptively chosen queries preserves equality of distributions.
The real and simulated proofs never use the same randomizers, so the proof cannot compare outputs value by value; it must compare laws. Two gaps in the printed argument need to be closed. First, witness indistinguishability is assumed only for one opening to against one opening to , while comparing a simulated gate proof with a real one compares two openings that may carry the same message; the trapdoor supplies the missing intermediate opening. Second, the printed gate recipe gives the gate commitment the message only when no input of the gate is the output wire; when the output wire is an input, the message is or , and has no 0/1 opening, so the simulator must open the gate commitment itself with the trapdoor. The adaptive adversary adds a third point: equality of laws must survive an arbitrary interaction in which later queries depend on earlier answers.
ZMod N with (the paper describes Figure 3 for order at least 4, p. 14); and are finite nonempty types, a commutative group. Key generators and the 0/1 prover's randomness are probability mass functions; the coins are uniform.A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, without revealing why it is true. NIZK proofs are a basic building block of public-key cryptography: chosen-ciphertext secure encryption, signature schemes and secure multi-party computation all use them. Groth, Ostrovsky and Sahai, New Techniques for Noninteractive Zero-Knowledge (J. ACM 59(3), 2012; conference versions at Eurocrypt 2006 and Crypto 2006), built the first NIZK proofs for all of NP that are perfectly sound and the first NIZK arguments that are perfectly zero-knowledge, using bilinear groups.
The construction rests on a single primitive, the homomorphic proof commitment: a commitment scheme with two kinds of keys (perfectly binding and perfectly hiding) together with a short non-interactive proof that a commitment contains or . Section 4 of the paper instantiates this primitive in a bilinear group of composite order , building on the encryption scheme of Boneh, Goh and Nissim (TCC 2005); Section 5 gives a second instantiation in prime-order groups. Theorem 2 states that the composite-order scheme of Figure 1 has all the required properties. This mission formalizes the part of Theorem 2 that is an exact mathematical statement.
Timeline: Boneh, Goh and Nissim (2005) introduced the subgroup decision assumption and the encryption in groups of order . Groth, Ostrovsky and Sahai (Eurocrypt 2006) used it for perfect NIZK; the simple 0/1 proof used in Figure 1 is due to an observation of Boyen and Waters (Eurocrypt 2006), as the paper's footnote 7 records. The journal version (2012) presents both instantiations through the abstract notion of a homomorphic proof commitment.
A BGN bilinear group is a tuple where are primes, and are finite commutative groups of order , is bilinear ( for all , ), generates , and generates .
The commitment key is for an element of one of two kinds:
The commitment to a message with randomizer is . The trapdoor opening is . The 0/1 proof for a commitment is , and the verifier accepts when . The extractor computes and searches for with .
For every BGN bilinear group, the scheme above satisfies:
with binding, soundness and extractability on binding keys, and trapdoor opening and witness indistinguishability on hiding keys.
The milestones follow the proof of Theorem 2 (p. 9) and Figure 1 (p. 10): the homomorphic property; perfect binding; the extraction identity ; the trapdoor identity and the uniqueness of openings on a hiding key; the completeness display ; the decomposition of every element as on a binding key; the step " of order or implies or "; perfect soundness; and the uniqueness of the proof on a hiding key, which gives witness indistinguishability.
Theorem 2 is one of the two instantiations on which every exact result of the paper rests. Plugged into the Circuit-SAT construction of Section 6, the binding-key properties give a perfectly sound NIZK proof and a perfect proof of knowledge for every NP relation, and the hiding-key properties give a perfect zero-knowledge NIZK argument. The same composite-order techniques underlie later pairing-based proof systems, notably the Groth–Sahai proofs.
The paper's proof is about one page of group computations and has, as far as the planning of this series found, no machine-checked counterpart. The mission produces a reusable model of composite-order bilinear groups and of the BGN commitment, and checks details the paper leaves implicit: the message space versus exponents taken modulo , the role of the non-degeneracy of , and the order arguments behind soundness.
Each property is elementary on its own, but soundness is not a plain computation: the verifier only sees and , and the conclusion asks for an opening of with message in from a single pairing equation. An argument that only manipulates the equation symbolically cannot reach it; the statement depends on the orders of elements in , on generating (with a degenerate pairing soundness is false), and on and being distinct primes. A second subtlety is that a message is only determined modulo by a commitment under a binding key, while the conclusion asks for a message that is exactly or in .
Fintype.card = p * q; is a homomorphism G →* G →* GT, which is exactly bilinearity; generates and generates (both as hypotheses of the structure BGNSetup).ZMod n; is to the representative of in . The paper's message space is , but is not well defined for in a group of order ; binding and extraction therefore compare messages modulo .A prophet inequality compares two players facing the same random sequence of rewards . The gambler sees the values one at a time and must decide, as each value arrives, whether to stop and collect it; a value passed over is lost. The prophet knows the whole sequence in advance and simply takes its maximum. In 1978 Krengel, Sucheston and Garling showed that when the are independent, non-negative and , the gambler has a stopping rule with
and that the factor cannot be improved. This inequality, labelled (1) in Kleinberg and Weinberg's Matroid Prophet Inequalities (arXiv:1201.4764, STOC 2012), is the starting point of optimal stopping theory's prophet inequalities and, more recently, of a large literature in online algorithms and algorithmic mechanism design, where it is the reason that a single posted price can extract a constant fraction of the optimal welfare or revenue.
Timeline.
This mission formalizes that §3.1 result.
Let be a probability space and . Let be real random variables on that are independent (as a family), non-negative, and such that the prophet's value has finite expectation. Define
The single-threshold rule observes in order and stops at the first time with , collecting . If no reaches , the rule accepts nothing and collects . Write for the amount collected; it equals on the event , which has probability , and off it.
In Lean the variables are X : Fin n → Ω → ℝ with [NeZero n]; is maxX X, is thr P X, is stopProb P X, and is reward P X, all in the namespace MatroidProphetKW.RankOne.
This is inequality (1) for an explicit rule, which is stronger than (1)'s existence statement. The constant is sharp, so the goal is stated with it.
The result. A threshold that depends on the distributions only through one number, , already matches the optimal worst-case guarantee of the best stopping rule. Because it is a single price, the rule translates directly into a posted-price mechanism: a seller who posts the price to arriving buyers obtains half of the expected maximum value. The same accounting, in which accepted value is charged against the threshold and rejected value against the probability of having accepted nothing, is what Kleinberg and Weinberg generalize to matroids (missions 1 and 2 of this series).
Formalizing it. The result is proved and classical; the work here is to formalize its known proof. No machine-checked proof of the factor-2 prophet inequality is in Mathlib, and none was found among the platform's published theorems in October 2026. A completed development provides the inequality itself, the tail comparisons, and the layer-cake bookkeeping for a stopped reward, all of which are reusable for other single-threshold prophet inequalities (Samuel-Cahn's median rule, -choice and posted-price variants).
The expected reward of the rule is not a function of the marginals of the individual alone in an obvious way: the event that the rule is still running when arrives depends on , and the reward is at a random index. The natural first attempt, comparing and pointwise, fails, since on a given outcome the rule may stop early at a value just above while the maximum comes later. The comparison has to be made between distributions, at each level , and it has to use independence to decouple "nothing accepted before time " from "". The rest is measure-theoretic bookkeeping that is routine on paper and not routine in Lean: expressing expectations of non-negative variables as integrals of tail probabilities, splitting them at , and keeping track of integrability.
Ω with a MeasurableSpace, P : Measure Ω with [IsProbabilityMeasure P].X : Fin n → Ω → ℝ, [NeZero n]; each X i measurable; iIndepFun X P (mutual independence); 0 ≤ X i ω for all i, ω; Integrable (maxX X) P, which is the paper's .Finset.sup' over the nonempty index set; no junk supremum.∫ ω, … ∂P) and Measure.real probabilities. Tail integrals are Lebesgue integrals of over and .The threshold is a definition, , not a free parameter constrained by hypotheses; a formalization in which is arbitrary and the upper-tail bound is assumed would make the goal a rearrangement of its hypotheses, and is ruled out.
Infrastructure that a complete development needs, and that is welcome as separate contributions: the layer-cake formula for non-negative integrable split at a level (Mathlib has the unsplit form, MeasureTheory.integral_eq_integral_meas_lt); measurability and integrability of the stopped reward (it is dominated by ); and the probability of the event "the first values are below and " as a product under iIndepFun.
Transient stability asks whether a power grid, after a large disturbance such as a fault or a line trip, returns to synchronous operation in which all generators rotate at a common frequency. The classical approach builds energy functions for the swing equations and estimates regions of attraction numerically; it gives no closed-form test relating synchronization to the network's parameters, and it handles transfer conductances (losses) only when they are "sufficiently small" without saying how small.
Dörfler and Bullo (arXiv:0910.5673v4; SIAM J. Control Optim. 50(3), 2012) observe that, for strongly overdamped generators, the network-reduced swing equations behave like a first-order non-uniform Kuramoto model, and they give purely algebraic conditions under which this model synchronizes. The same model is a generalization of the classical Kuramoto model of coupled oscillators, studied in physics, neuroscience and control, with heterogeneous time constants, asymmetric effective coupling and phase shifts. This mission formalizes the first of the paper's two synchronization conditions, Theorem V.3, which is also statements 1)–2) of the paper's main result, Theorem III.2.
There are oscillators with phases . Each has a time constant and a natural frequency ; each pair has a coupling weight and a phase shift , with . The non-uniform Kuramoto model is
The phases live on the torus. For an arc length , the set consists of configurations whose phases all lie in the interior of some arc of length , and is its closure (with the synchronized configurations). A set is positively invariant if every solution starting in it stays in it. A solution achieves exponential frequency synchronization if all frequencies converge exponentially fast to a common value .
The condition of the theorem compares two numbers built from the parameters, with :
is the weakest lossless coupling of an oscillator to the network; measures the spread of natural frequencies and the losses. When , put , and .
If is complete ( for ) and
then (1) is positively invariant for every , and every solution starting in eventually stays in for each ; (2) every solution starting in achieves exponential frequency synchronization to some , and when the solution starts in .
The milestones follow the paper's proof. Theorem V.1 is a frequency-synchronization theorem for phase-cohesive oscillators under a globally reachable node, with the explicit rate
when and . Its supporting steps are the frequency dynamics (20) and a dihedral-angle bound. The phase-cohesiveness argument of Theorem V.3 is split into a trigonometric lower bound, a pointwise bound on the growth rate of the arc containing all phases, the characterization of by inequality (30), positive invariance, and the entry into .
The theorem turns synchronization of a heterogeneous, lossy oscillator network into one inequality among explicit parameters. For the classical Kuramoto model it specializes to (Remark V.4), which improved the sufficient conditions known at the time. For power networks it gives, through Theorem III.2, a computable sufficient condition for transient stability when generator inertia is small relative to damping.
To our knowledge none of these results has a machine-checked proof. The development needs ODE comparison arguments for a non-smooth Lyapunov function (the arc length) and an exponential convergence theorem for time-varying consensus. Both are general tools that are not in Mathlib and would be reusable for other consensus and synchronization results. The mission also records two clauses of the printed theorem that are false as stated, with counterexamples, and states the corrected theorem.
The arc length is only Lipschitz, so its decrease along solutions must be argued through Dini derivatives and a comparison lemma rather than by differentiation. Positive invariance at the boundary holds with a non-strict inequality, so a naive "strictly decreasing at the boundary" argument does not apply there. Frequency synchronization rests on a contraction property of linear consensus with time-varying, state-dependent weights. The weights are positive only after the phases have entered . Before that the frequency range can expand, which is why the range clause of the printed theorem fails for initial arcs longer than .
Phases are represented by real lifts . means that all pairwise differences of the lift are at most , and that they are strictly less than . Conclusions are stated for the same continuous lift, which is at least as strong as membership on the torus. A solution is a map with derivative (one-sided at ) equal to the right-hand side of (8) for all . Every statement quantifies over all such solutions. always denotes the vector field along the solution. Minima and maxima over are over ordered pairs, and is assumed so that they exist. The conventions are explicit hypotheses. and are defined by , and a milestone certifies that they are the unique solutions in the printed ranges. is the second-smallest eigenvalue of the symmetric Laplacian.
The source is the arXiv preprint v4 of the SICON article, cited with its own page and theorem numbers. Three corrections relative to the printed text are made and disclosed in the items:
No statement is trivially satisfiable. The solution predicate holds for actual solutions (for example the synchronous solution), condition (26) is satisfiable (take and ), the exponential rate is required to be strictly positive, and are specific numbers rather than existential witnesses.
Contributions are welcome on all milestones. The trigonometric bound, the dihedral-angle bound and the characterization are elementary. The comparison lemma for Dini derivatives and the consensus contraction theorem are reusable infrastructure.
A spectral sparsifier of a graph is a much sparser weighted graph whose Laplacian quadratic form is within a factor of the original on every vector. Spielman and Teng introduced the notion in Spectral Sparsification of Graphs as a strengthening of the cut sparsifiers of Benczúr and Karger: a spectral sparsifier preserves every cut, and in addition every quantity determined by the Laplacian quadratic form, such as effective resistances, eigenvalues and the behaviour of random walks. Sparsifiers are the reason linear systems in graph Laplacians can be solved in nearly linear time: one preconditions with a sparsifier and solves the sparse system instead (Spielman–Teng, arXiv:cs/0607105).
The construction in the paper has two halves: decompose the graph into pieces of high conductance, then sparsify each piece by random sampling. This mission is the second half, Theorem 6.1 of §6: in a graph whose normalized Laplacian has a spectral gap, keeping each edge independently with probability inversely proportional to the smaller degree of its endpoints, and reweighting kept edges by the inverse probability, produces a -spectral approximation with few edges, with high probability.
Timeline. Benczúr and Karger (1996) sampled edges with probabilities depending on edge strength and preserved cuts. Achlioptas and McSherry (2001) analysed random sampling of matrices through the random-matrix norm bound of Füredi and Komlós (1981), corrected by Vu (2007). Spielman and Teng (arXiv 2008, SIAM J. Comput. 2011) proved Theorem 6.1 by refining the Füredi–Komlós trace method for downsampling graphs that may already be sparse. Spielman and Srivastava (2008) later replaced conductance-based probabilities by effective resistances.
Let be an unweighted graph on a finite vertex set , , with degrees , adjacency matrix , diagonal degree matrix and Laplacian . Its quadratic form is
A weighted graph on with weights has the form . is a -approximation of if for all
When every degree is positive, the normalized Laplacian is ; its eigenvalues lie in , and a lower bound on its smallest non-zero eigenvalue measures how well connected each component of is (by Cheeger's inequality it is equivalent to high conductance up to squaring).
Sampling. For a parameter , edge is assigned
each edge is kept independently with probability , and a kept edge gets weight . The sampled adjacency matrix then has ; is the diagonal matrix of weighted degrees of the sampled graph.
The procedure. In Theorem 6.1 sampling is applied only to the edges of an induced subgraph , ; the other edges are kept with weight 1. sets and uses the degrees of ; the paper takes .
For , without isolated vertices whose smallest non-zero normalized Laplacian eigenvalue is at least , , and an even integer : with probability at least , simultaneously
Theorem 6.1 is the sampling engine of the first nearly-linear-time spectral sparsification algorithm: combined with a decomposition of an arbitrary graph into high-conductance pieces (§7–§10 of the paper), it yields sparsifiers with edges, which in turn give the nearly-linear-time Laplacian solvers that underlie fast algorithms for electrical flows, maximum flow approximation and graph partitioning. Lemma 6.3 is a self-contained random-matrix result: a norm bound for the normalized deviation of a downsampled graph that does not assume the original graph is dense.
The result is proved in the paper. As far as is known, none of it is formalized in Lean or Mathlib: Mathlib has the graph Laplacian (SimpleGraph.lapMatrix) and the spectral theorem for Hermitian matrices, but no normalized Laplacian, no spectral approximation and no trace-method bounds for random matrices. A complete formalization would be the first machine-checked proof of a spectral sparsification theorem, and the milestones (the trace-method moment bound, Chernoff for weighted two-point sums) are reusable on their own.
The obvious argument — bound each entry of and apply a matrix concentration inequality — needs either a matrix Chernoff bound (not in the paper, and not in Mathlib) or the Füredi–Komlós trace method, which assumes every edge can appear and so fails when the graph is already sparse: a vertex of small degree has no room for its entries to average out. The paper's sampling probabilities keep every edge at a vertex of degree at most , and the trace computation has to exploit exactly this through the moment bound of Lemma 6.6 and a combinatorial count of closed walks. Formally, the obstacles are the walk-counting argument of Lemma 6.4, the passage from a trace bound to an eigenvalue bound for the non-symmetric (similar to a symmetric matrix), and Lemma 6.2's restriction to the orthogonal complement of the kernel, which must handle disconnected in the goal.
V; graphs are SimpleGraph V with decidable adjacency; weighted graphs are weight functions V → V → ℝ (symmetric, nonnegative, loopless). The quadratic form is ; a -approximation keeps both inequalities of (2).In the job shop problem, jobs are sequences of operations, each to be processed on a given machine for a given time, and the goal is a schedule of minimum makespan (the time at which the last job finishes). Two numbers bound the optimum from below: the longest job and the most loaded machine. Their maximum is written . The best approximation algorithms for job shops have a performance guarantee polylogarithmic in (Shmoys, Stein and Wein 1994; Goldberg, Paterson, Srinivasan and Sweedyk 2001). Whether flow shops and job shops admit a constant-factor approximation was Open Problem 7 of Schuurman and Woeginger (1999).
Mastrolilli and Svensson (J. ACM 58(5), 2011) answered it negatively for the generalized flow shop. Their Theorem 1.2 states that for all sufficiently large constants it is NP-hard to distinguish generalized flow shop instances with a schedule of makespan from instances in which no schedule finishes more than half of the jobs within . The proof is a gap-preserving reduction from graph colouring. This mission formalizes the combinatorial heart of that reduction.
Timeline. Shmoys, Stein and Wein (1994) gave an -approximation for job shops, improved by a factor by Goldberg et al. (2001). Williamson et al. (1997) proved that approximating flow shops with unit operations within a ratio better than is NP-hard. Feige and Scheideler (2002) gave acyclic job shop instances with optimum and asked whether flow shops admit a much better upper bound than . Khot (2001) proved the colouring hardness this reduction starts from. Mastrolilli and Svensson (FOCS 2008; J. ACM 2011) proved Theorem 1.2 and its job shop variants.
A generalized flow shop (flow shop with jumps) is a job shop with a fixed linear order on the machines in which every job visits its machines in increasing order but may skip machines. Operations may have length . A zero-length operation still occupies its machine for an instant, so it cannot be processed strictly inside another operation on the same machine.
Let be a simple graph with vertices whose vertices are partitioned into independent sets . Vertex has frequency . For an integer write . The instance has groups of machines, each with one machine per vertex. The machines are ordered by group first and, within a group, by decreasing frequency. A vertex of frequency owns groups of identical jobs. The job has a long-operation of length on each of the machines , where . It also has a short-operation of length on every machine of every neighbour of , in every group. A long-operation is good if the next long-operation of the same job starts at most time units after it ends. is the set of first halves of the good long-operations on , and is the time they cover.
is the chromatic number of and the size of its largest independent set.
For every graph with a proper colouring into classes and every integer , with :
Remark 3.6 (lengths, loads, operation count), Claim 3.8 (an independent set's jobs fit in ), Lemma 3.7 (completeness), Lemma 3.10 (most long-operations are good), Lemma 3.11 (adjacent vertices have disjoint -intervals), Lemma 3.12 (one group carries of first-half time), and Lemma 3.9 (soundness: an independent set of size ).
The result. Together with Khot's colouring hardness, the gap shows that no polynomial-time algorithm approximates the generalized flow shop within any constant factor unless P = NP, and rules out an -approximation under a stronger complexity assumption (Theorem 1.3). It also shows that on the no-instances of the reduction every schedule has makespan greater than , far above the trivial lower bound . Because soundness bounds the number of jobs finished early, the same reduction also gives hardness for the sum of completion times (footnote 2).
Formalizing it. The paper proves every statement of this mission; none is open. As far as the catalog shows, none has a machine-checked proof. The soundness argument rests on a timing property of zero-length operations: a job of higher frequency must wait for a long-operation of an adjacent lower-frequency job. Such properties are easy to state loosely and easy to get wrong, so a verified proof would be useful. A formal proof would also make explicit the thresholds the paper leaves as "sufficiently large ".
Completeness is constructive and routine once the job and machine indexing is under control. The difficulty is soundness. One might argue directly that jobs of adjacent vertices never overlap in time, but that is false: a schedule may run them in parallel at the cost of delays. The argument controls it only on average. It throws away the jobs that finish late and the long-operations followed by a long delay. It shows that the first halves of the remaining long-operations of adjacent vertices are disjoint in each machine group. Then it finds a moment covered by many such first halves. Each step needs a precise count: of good operations per job, of covered time per group, and of overlap multiplicity at a point. The degenerate conventions (empty colour classes, , the last long-operation of a job) have to be handled throughout.
The instance is the published JobShopLTAS.Core.Instance (machines and jobs Fin (r^{2d} n), real nonnegative processing times, disjunctive machine constraint under which a zero-length operation cannot sit strictly inside another operation on its machine), with its IsFeasibleSchedule and makespan. The graph has vertex set Fin n and the partition into independent sets is a Mathlib proper colouring G.Coloring (Fin d). Frequencies are 1-based, as are group indices. Within a group the paper leaves machines of equal frequency unordered; they are ordered by vertex index. Every job's operation list is its machine set sorted by the global order. is the Lebesgue measure of the union of the intervals.
Explicit readings of the paper's wording:
Not formalized: "NP-hard", "for all sufficiently large ", "in time polynomial in and ", Khot's Theorem 1.7, the choice , , and the randomized Lemma 3.1 behind Theorem 1.3.
A model in which zero-length operations occupy no machine time would make soundness false, and stating soundness only for schedules of an independent set's jobs would make it vacuous. The goal is about every feasible schedule of , built from , in the published model, where zero-length operations do conflict.
A complete development needs counting lemmas for the indexing of jobs and machines, sorting facts for the operation lists, and a measure-theoretic averaging argument (a point covered by many intervals). The averaging argument and the good-operation counting are shared with the flow shop gap of Theorem 1.1 and reusable there. Proofs of any milestone, and sorry-free sanity checks on small instances, are welcome.
Many models in operations management and economics need the demand or valuation distribution to be regular in some way, so that an optimal price, order quantity or contract is unique. Pricing a service to one customer whose valuation has survival function is a typical example. The seller maximizes . The first-order condition is , where is the generalized failure rate and is the ordinary failure rate. When is increasing (the IGFR property, introduced by Lariviere and Porteus 2001), the optimal price is unique and solves .
The best-known regularity class is the class of IFR laws, those with increasing failure rate. Every IFR law has finite moments of all orders (Barlow and Proschan 1965). IGFR laws are a larger class that includes heavy-tailed laws, and Lariviere (2006) identifies exactly which of their moments are finite. The answer is given by one number, the limit of the generalized failure rate. A consequence used in pricing models is that a valuation law with a finite mean has eventually, so the pricing problem has a finite solution.
Let be a nonnegative random variable with distribution function and survival function . Assume has a density . The failure rate is
and the generalized failure rate is . is IGFR if is weakly increasing on . has support , with , if exactly for and for every . For a real , the -th moment is .
The comparison law is the Pareto law with scale and parameter , which has density for . Its generalized failure rate is identically on , and its -th moment is finite exactly when . For a level with , write for conditional on . A random variable is stochastically smaller than if for all real .
In Lean, is its law μ : Measure ℝ, is cdf μ, is survival μ, is failureRate μ φ, is genFailureRate μ φ, and is nthMoment μ n.
Suppose is IGFR with support and , where may be infinite. Then for every real ,
The statement fixes no constants. It covers (all moments finite) and the boundary case (infinite moment).
The two Pareto facts of the §3 preamble come first:
Six claims from the proof follow:
Two consequences stated after the theorem are included as further targets. First, an IGFR law with support and a finite mean has beyond some finite point. Second, a strictly IGFR law with a finite -st moment satisfies the two conditions of Van Mieghem and Dada (1999): has at most one zero, and .
The theorem gives a complete moment criterion for IGFR laws in terms of the single number . Among IGFR laws, finiteness of the mean, the variance or any higher moment can therefore be read off the tail of . One consequence is that a finite mean is enough for the IGFR pricing problem to have a finite solution, which replaces the separate condition " exceeds one at a finite point". The theorem generalizes Lemma 2 of Lariviere and Porteus (2001), and the paper uses it to connect IGFR laws to the Van Mieghem–Dada condition.
The result is proved on paper but has not been formalized. Formalizing it adds three things:
Pareto.lean lacks;The core of the proof is a comparison: a pointwise bound beyond a level becomes a stochastic order against a Pareto tail. This needs the representation , which uses the fundamental theorem of calculus for across the left end of the support, where may have a kink. It also needs to be stated for the conditional law, whose density is a rescaled restriction.
An obvious first attempt is to bound directly by with the given bound on . That bound controls , not , so it says nothing directly. The survival representation is what converts it.
A second obstacle is the boundary case , with finite. A strict margin is no longer available there. It needs the non-strict bound , which follows from monotonicity, and a Pareto law with parameter exactly .
Laws, not random variables. Every statement is about distributions, so is represented by a probability measure μ on ℝ with μ (Set.Iio 0) = 0. In the goal, nonnegativity also follows from the support hypothesis, and the separate hypothesis is kept for uniformity with the other items.
The density version is pinned. and read pointwise, while "Φ has density φ" determines only up to a null set. The predicate IsRegDensity requires and . It also requires to be the right derivative of at every point of and wherever . The exponential law with satisfies all hypotheses of the goal, with .
IGFR is weak monotonicity of on , as printed. On this set , so Lean's convention never enters.
is an extended nonnegative real. The limit hypothesis is Tendsto (fun ξ => ENNReal.ofReal (g ξ)) atTop (𝓝 κ) with κ : ℝ≥0∞. A real-valued would silently drop the case .
Moments are lower Lebesgue integrals ∫⁻ x, ENNReal.ofReal (x ^ n) ∂μ with a real exponent. The Bochner integral would make "finite" automatic, because it returns for a non-integrable function, so it is not used.
Conditioning and Pareto. is Mathlib's ProbabilityTheory.cond μ (Set.Ioi y), always with . The Pareto law is Mathlib's paretoMeasure S k. "Stochastically smaller" is the published definition StochasticOrders.Usual.UsualOrder applied with the identity map.
Trivialization is ruled out. The goal is a full equivalence with a possibly infinite and an infinite-valued moment. It is not the weaker " implies finite", and the hypotheses are jointly satisfiable.
Recorded deviations. The printed bound "" is a slip (it fails for ). Only the finiteness it is used for is formalized. The Pareto moment fact is stated as an equivalence, which contains the printed "only if".
Infrastructure. A complete development needs:
cond and cdf.The survival representation and the failure-rate/Pareto comparisons are reusable for any heavy-tail result stated through hazard rates. Contributions are welcome at every level, including partial results such as the Pareto lemmas alone.
Search engines sell advertising space query by query. Each advertiser states a bid for each keyword and a daily budget; queries arrive one at a time, and each must be assigned to an advertiser immediately, without knowledge of the queries still to come. The revenue-maximizing assignment of the day can only be computed offline. The adwords problem asks how close an online rule can get to it. It generalizes online bipartite matching, for which Karp, Vazirani and Vazirani (KVV 1990) showed that randomized ranking attains ratio , and -matching, for which Kalyanasundaram and Pruhs (KP 2000) showed that the deterministic BALANCE algorithm attains as the budget grows.
Mehta, Saberi, Vazirani and Vazirani (J. ACM 2007) gave a deterministic algorithm for arbitrary bids that weighs each bid by a function of the fraction of budget already spent, and proved that it is -competitive when bids are small compared to budgets. The algorithm and its tradeoff function became the reference point for the online budgeted-allocation literature, including the primal-dual analysis of Buchbinder, Jain and Naor (ESA 2007).
There are bidders, each with budget , and a sequence of queries . Bidder bids for the query at position . An allocation assigns each query to at most one bidder. Bidder 's spend before position is , and is alive while its spend is below . The revenue of is .
Fix an integer and split each budget into equal slabs; a spent fraction lies in slab , and in slab . Given a tradeoff function on slabs, the discrete tradeoff algorithm assigns each arriving query to an alive bidder maximizing
ties broken arbitrarily. Every allocation produced this way, for any tie-breaking, is a run.
The analysis uses the factor-revealing LP : maximize subject to and , written , , , and its dual . Its optimal dual solution is , and Theorem 8's tradeoff function is
For every there is such that for every there is such that, for every instance with bids in , every run of the algorithm with , and every allocation ,
The goal fixes no rate in or : it asserts only that the ratio tends to .
Theorem 8 gives an online algorithm for budgeted allocation with arbitrary bids whose revenue is within a factor of the offline optimum, the best possible ratio even for randomized algorithms (Theorem 9 of the same paper, the second mission of this series). It reduces to BALANCE when all bids are equal, and its tradeoff function in the limit is the function used in later work on online budgeted allocation and display-ad allocation.
The result is proved in the paper; none of it is formalized. The work here is to formalize the proof in a version that holds for actual runs. The paper's argument makes two simplifications with "negligible error": bidders of type spend exactly of their budget, and the offline optimum exhausts every budget. A formal proof must carry the bid size through the slab boundaries and compare with an arbitrary offline allocation. The LP lemmas (Lemmas 3–5) are self-contained statements about one triangular linear program and are reusable for factor-revealing analyses of BALANCE.
The milestones are short: Lemmas 3–5 are finite linear algebra with geometric sums, Lemma 6 is one application of the assignment rule plus monotonicity of spend, and Lemma 7 regroups finite sums. The difficulty is in Theorem 8. The paper's proof chains Lemmas 4, 5 and 7 through the LP , whose right-hand side is computed from the numbers of bidders of each type under the assumption that a bidder of type spends exactly . In an actual run this identity fails: a single bid can straddle a slab boundary, and types are intervals, not points. So the chain does not compose literally, and the natural first attempt, instantiating Lemma 5 with the run's quantities, does not apply. The slab-wise inequalities that do hold, with an error of order , have to replace the equalities, and the comparison with an offline allocation that does not exhaust budgets has to be made through capped revenues.
Bidders are Fin N and query positions Fin M, zero-based; slabs and LP coordinates keep the paper's 1-based ranges, with vectors as functions read on . Budgets are (the paper's standing simplification of §2). Bids are real and nonnegative.
A run is a predicate on the whole allocation: at position , if some bidder is alive the query goes to an alive maximizer of bid , where spends are computed from earlier positions only; the query is unassigned only when all budgets are exhausted. Every tie-breaking rule gives a run, and the goal holds for all of them. is the full bid of the chosen bidder; revenue is capped at the budget.
Conventions the statements commit to:
Trivializing formalizations are ruled out: a run cannot leave a query unassigned while a bidder has budget, so the empty allocation is not a run; no hypothesis of the form "bidders of type spend exactly " or "the optimum exhausts every budget" is imposed, since either would make the goal vacuous on most instances.
All definitions are local to the namespace AdWordsMSVV.Tradeoff. Related platform items analyse a different algorithm: BJNAdAuctions.Basic.* and OnlinePrimalDual.AdAuctions.* formalize the Buchbinder–Jain–Naor primal-dual algorithm, which updates a covering variable multiplicatively and has ratio ; they are not reused. Proofs of any milestone, and lemmas carrying the bid-size error through slab boundaries, are welcome.
Large service systems (call centers, hospital wards, cloud server pools) run with many servers, and for many of them no exact formula describes how the number of busy servers moves over time. Heavy-traffic limits replace such a system by a diffusion process that is easier to analyze. The many-server regime, in which the number of servers and the arrival rate grow together, goes back to Halfin and Whitt (1981) and is the basis of square-root staffing rules in call-center practice.
The simplest many-server model is the queue. Its stationary number in system is Poisson with mean , so the centered and -scaled stationary count is asymptotically normal when . The question here is about the whole process: does the scaled number in system converge, as a random path, to a diffusion? The classical answer, the Ornstein–Uhlenbeck limit, was first established by Iglehart (1965) with Stone's theorem for birth-and-death processes, and was revisited by strong approximation (Mandelbaum, Massey and Reiman 1998) and, for general service times, by Krichagina and Puhalskii (1997).
Pang, Talreja and Whitt (2007) is a tutorial survey that proves this limit, and its finite-waiting-room extension, with martingale methods. The authors present the argument as a template for non-Markovian and network models (Reed 2009; Dai and Tezcan; Gurvich and Whitt). This mission formalizes the result and the steps of the paper's proof.
Fix a service rate . For each , the -th system has arrival rate . Let and be independent Poisson processes of rate , and let be a random initial number of customers, independent of and . The number in system is the -valued process with right-continuous paths having left limits that satisfies, almost surely,
The departure term is a random time change: each of the customers in service completes service at rate . The diffusion-scaled process is , the paper's (3). The space consists of paths on that are right-continuous with left limits, and denotes convergence in distribution.
The limit is the Ornstein–Uhlenbeck (OU) process , driven by a standard Brownian motion , with independent of :
The proof also uses the scaled martingales and , the fluid processes and , and stochastic boundedness. A sequence of real random variables is stochastically bounded if it is tight, and a sequence of processes is stochastically bounded in if is, for every .
If in , with an arbitrary limit law , then
where is the OU process (5) with . The goal fixes no initial distribution and assumes no moment condition on .
Theorem 1.1 describes the transient behavior of a large infinite-server system, not only its stationary law: fluctuations of order around the offered load form a Gaussian Markov process that relaxes at rate . It is the reference case for the Halfin–Whitt regime, whose finite-server version, Theorem 1.2 of the same paper (the queue), is the subject of the companion mission. The milestones are general tools reused well beyond queueing: Gronwall's inequality, the Lipschitz integral map, the Poisson FCLT, stochastic boundedness via Lenglart's inequality, and the fluid limit from stochastic boundedness.
The theorem is proved and classical; no machine-checked proof of it, or of the milestones below, is known. No formal library currently has the Poisson functional central limit theorem in , compensators of counting processes, or random time changes of martingales. Formalizing the paper's proof would produce these, plus a template for the martingale method of heavy-traffic analysis. Alternative proofs, such as the paper's §4.3 route without martingales, are equally welcome as solutions.
Equation (12) is a fixed-point equation: appears inside the argument of . The integral map of Theorem 4.1 is continuous, so the obvious argument is to apply the continuous-mapping theorem to the martingale representation. That reduces the goal to the joint convergence of . But is a Poisson martingale evaluated at the random time , and its limit is identified only after the fluid limit is known. The fluid limit is itself a statement about the whole sequence , and it needs a separate argument, either Gronwall at fluid scale or stochastic boundedness. Lemma 3.2 requires optional stopping at the continuum of stopping times , and the moment conditions (22) must be checked through the crude bound. Removing needs a truncation of the initial conditions (§6.3).
CouplingConverges): a Skorokhod representation with almost-sure uniform convergence on compact intervals. Convergence to a deterministic path is uniform convergence on compacts in probability (UocInProb). is stated with bounded continuous test functions.Type.A formalization that fixes , assumes converges almost surely, adds to the goal, or replaces convergence in by convergence of finite-dimensional distributions proves a weaker theorem and does not close the goal.
Contributions are welcome at every level. The Poisson FCLT, Lenglart's inequality and the composition map are reusable library results, independent of queueing.
Large service systems such as call centers, hospital wards and cloud server pools have many parallel servers, finite buffers and customers who leave when they wait too long. Their performance is usually analysed through heavy-traffic diffusion limits: the number of customers in the system, centred and rescaled, converges as the system grows to a diffusion process whose law is computable. The quality-and-efficiency-driven (QED) regime of Halfin and Whitt (Oper. Res. 29, 1981) is the scaling in which the number of servers and the arrival rate grow together so that the probability of delay stays strictly between and . Garnett, Mandelbaum and Reiman (M&SOM 4, 2002) proved the QED limit for the Erlang-A model with unlimited waiting room. Whitt (Math. Oper. Res. 30, 2005) added finite waiting rooms of size of order , which produce a reflecting upper barrier in the limit.
Pang, Talreja and Whitt (Probab. Surveys 4, 2007) give a self-contained martingale proof of these limits. Theorem 1.2 of that paper, the target of this mission, covers the model with finite waiting room and abandonment. It contains the Erlang-B (loss) model () and finite-buffer Erlang-C models () as special cases.
Fix a service rate , an abandonment rate , a constant and a barrier . For , model is an queue: servers, a waiting room of places, Poisson arrivals of rate , exponential services of rate , first-come first-served service, and an exponential patience of rate for each waiting customer. An arrival that finds all places occupied is blocked and lost.
The number in system is constructed from independent rate-1 Poisson processes , , and an independent initial value by
where counts blocked arrivals. The QED scaling is
and the scaled process is .
The limit is a reflected diffusion: a pair of processes with right-continuous paths with left limits, , nondecreasing and nonnegative, a standard Brownian motion independent of , and
The regulator increases only when sits at .
If in , then in , where solves the reflected equation above with , and every solution with initial law has the same law:
The goal fixes no rate of convergence and no stationary quantity; it asserts the process limit and its characterization by (9)–(10).
The theorem supplies the diffusion approximation behind square-root staffing rules for systems with finite buffers: it says that buffers of order are visible in the limit as a barrier at , and that the limit for (Erlang-B with or without abandonment) is a reflected Ornstein–Uhlenbeck-type process. Stationary blocking and delay probabilities of the limit then approximate those of the large finite system.
The result is proved in the literature (Whitt 2005; Pang, Talreja and Whitt 2007, whose proof of Theorem 1.2 is a sketch built on §7.1). It is not formalized anywhere. A formal proof would supply a checked martingale representation for a birth–death queue with blocking, a checked reflection map with state-dependent drift, and the continuous-mapping step through it. The unlimited-waiting-room case is posed separately on the platform as the Erlang-A limit of Garnett, Mandelbaum and Reiman and is not part of this mission.
The obvious route is the one used for the Erlang-A model: write as a continuous function of the scaled Poisson noise and apply the continuous-mapping theorem. With a finite waiting room this fails as stated, because the blocking process is not a function of the noise alone. It depends on the path of through the times the system is full. The proof must instead identify as the image of the noise under a reflection map with a drift inside it, prove that this map is well defined and continuous, and control the martingale terms through random time changes whose limits are deterministic. The barrier in model is , not , so the continuous-mapping step has to handle a moving barrier as well.
BellWilliams2001.ThresholdPolicy.IsCadlag. Brownian motion is ErlangA.Diffusion.IsStandardBM, indexed by ; martingales are Mathlib Martingales indexed by .ManyServerQED.Scheduling.IsPoissonProcess. is independent of the primitives and for all . Blocked arrivals are counted with the left limit , correcting (114) as printed. and are allowed.BellWilliams2001.ThresholdPolicy.CouplingConverges (Skorohod coupling with almost sure uniform convergence on compacts), equivalent to weak convergence for a continuous limit. Uniform distances use supDist on .ErlangA.Diffusion.drift; is independent of ; and are adapted to the filtration of and ; condition (10) is "the Lebesgue–Stieltjes measure of , extended by to negative times, gives zero mass to ". Uniqueness is uniqueness in law of . The limit space lives in Type.Contributions welcome: Stieltjes-integral and counting-process lemmas for , a reflection map with Lipschitz drift on , the Poisson functional central limit theorem, and martingale facts for randomly time-changed Poisson processes. The last three are reusable well beyond this mission.
The Kurdyka–Łojasiewicz (KL) inequality is the analytic engine behind most global convergence proofs for descent methods on nonconvex problems: proximal point and proximal gradient schemes, alternating minimization, ADMM variants and subgradient flows all reach a critical point with finite trajectory length once the objective satisfies a KL inequality. Its origin is Łojasiewicz's gradient inequality for real-analytic functions ([Łojasiewicz, 1963]); Kurdyka extended it to differentiable functions definable in an o-minimal structure, with a reparametrization ψ of the values, on bounded sets (Kurdyka, Ann. Inst. Fourier 48 (1998)).
Optimization objectives are rarely smooth or finite everywhere: indicator functions of constraint sets, ℓ₁ penalties, rank functions and maxima take the value +∞ or have kinks. Bolte, Daniilidis, Lewis and Shiota (SIAM J. Optim. 18(2) (2007), 556–572) proved that every lower semicontinuous function definable in an o-minimal structure satisfies a KL inequality for Clarke subgradients, globally in space. This mission formalizes that result (Theorem 14) and the chain of statements in §4 of the paper on which its proof rests.
Timeline. Łojasiewicz (1963): gradient inequality for real-analytic functions near a critical point. Kurdyka (1998): the inequality ‖∇(ψ∘f)‖ ≥ 1 for C¹ definable functions on bounded sets. Bolte, Daniilidis and Lewis (SIAM J. Optim. 17(4) (2007)): nonsmooth Łojasiewicz inequality for lower semicontinuous subanalytic functions with the limiting subdifferential. Bolte, Daniilidis, Lewis and Shiota (2007): this paper, for definable functions, Clarke subgradients, and unbounded sets.
Write ℝⁿ for Euclidean space with norm ‖·‖ and inner product ⟨·,·⟩, and let f : ℝⁿ → ℝ ∪ {+∞} be lower semicontinuous, with domain dom f = {x : f(x) < +∞} and graph Graph f = {(x, f(x)) : x ∈ dom f} ⊆ ℝⁿ⁺¹. Π : ℝⁿ⁺¹ → ℝⁿ forgets the last coordinate.
Subdifferentials. A vector x* is a Fréchet subgradient of f at x ∈ dom f if liminf_{y→x, y≠x} [f(y) − f(x) − ⟨x*, y − x⟩]/‖y − x‖ ≥ 0. The limiting subdifferential ∂f(x) collects the limits of Fréchet subgradients x_k at points x_k → x with f(x_k) → f(x); the singular subdifferential ∂^∞f(x) collects the limits of t_k x_k with t_k ↘ 0⁺. The Clarke subdifferential is
with the closed convex hull. It may be empty even on dom f, for example for −‖x‖^{1/2} at 0.
O-minimal structures. An o-minimal structure 𝒪 on (ℝ, +, ·) is a sequence of Boolean algebras 𝒪ₙ of subsets of ℝⁿ (the definable sets) that is stable under A ↦ A × ℝ, A ↦ ℝ × A and the projection Π, contains every algebraic set {p = 0}, and whose one-dimensional sets are exactly the finite unions of intervals and points. Semialgebraic sets, the globally subanalytic sets and the sets definable with the exponential each form such a structure. A function is definable if its graph is.
Stratifications. A C^p stratification of a set X is a locally finite partition of X into C^p submanifolds (strata) such that a stratum meeting the closure of another lies in its frontier. It is Whitney-(a) if tangent spaces T_{x_k}X_i converging to 𝒯 along x_k → x ∈ X_j satisfy T_xX_j ⊆ 𝒯, and a stratification of a set in ℝⁿ⁺¹ is nonvertical if e_{n+1} is tangent to no stratum. For x in a stratum X_i, ∇_R f(x) is the Riemannian gradient of f restricted to X_i.
For every lower semicontinuous definable f there are ρ > 0, a strictly increasing continuous definable ψ : [0, ρ) → ℝ, C¹ on (0, ρ) with ψ(0) = 0, and a continuous definable χ : ℝ₊ → (0, ρ) such that
Neither ρ, ψ nor χ is fixed: the goal asserts only their existence, so it is independent of any choice of exponent.
Corollary 9 (ii)–(iii) (finitely many Clarke critical and asymptotic critical values) and Corollary 12 (the KL inequality around the zero set) are included as further statements.
The result. Theorem 14 makes the KL property available, with no further verification, for every lower semicontinuous objective built from semialgebraic, globally subanalytic or exp-definable pieces. Global convergence theorems for proximal alternating minimization, proximal gradient methods, PALM and nonconvex ADMM take a KL inequality as hypothesis; definability is how that hypothesis is checked in applications. The inequality is relative to the value 0, holds globally through χ(‖x‖), and controls every Clarke subgradient rather than only the one of least norm. Corollary 9 is a definable, nonsmooth Morse–Sard theorem.
Formalizing it. The theorem has been proved since 2007; it has not been formalized. Lean's Mathlib has no o-minimal geometry: no cell decomposition, monotonicity theorem, definable choice or Whitney stratification. A complete development of this mission would supply the first machine-checked KL inequality for a general class of nonsmooth functions, and the o-minimal infrastructure it needs is reusable for every result in optimization and real algebraic geometry that cites "tame" functions.
The statements are short; the proofs rest on geometry absent from Lean. Lemma 8 is proved in the paper by citation of a stratification theorem for definable maps ([Shiota, Geometry of Subanalytic and Semialgebraic Sets, 1997, II.1.17]). Proposition 10 and Theorem 11 use the monotonicity lemma for definable functions of one variable and definable selection. The natural first idea — apply Kurdyka's inequality on each stratum and take a minimum — fails twice: Kurdyka's inequality is local on bounded sets, and the reparametrizations ψ_i of different strata must be compared near 0, which needs the monotonicity lemma once more. Passing from the strata to Clarke subgradients needs the projection formula of Corollary 9, which in turn depends on nonverticality and the Whitney-(a) condition.
ℝⁿ is EuclideanSpace ℝ (Fin n); ℝ ∪ {+∞} is EReal, with f never equal to ⊥ as a standing hypothesis; ℝⁿ⁺¹ carries the value in the last coordinate. The Fréchet and limiting subdifferentials are the published NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff. The Clarke subdifferential uses closedConvexHull. An o-minimal structure is a structure with a family O n of sets of subsets of ℝⁿ satisfying Definition 6 (Boolean algebra as: ∅, complements, binary unions; one-dimensional sets as finite unions of order-connected sets). Definability of ψ, χ and of the strata is part of every conclusion that asserts it. Tangent spaces are spans of Mathlib's tangentConeAt; C^p submanifolds are local graphs; the Riemannian gradient on a set U is a vector g in the tangent space with HasFDerivWithinAt h ⟪g, ·⟫ U x.
Inequality (22) is stated as ψ′(|f(x)|)·‖x*‖ ≥ 1, never as 1/ψ′ ≤ ‖x*‖, so that ψ′ = 0 cannot make it hold through 1/0 = 0. The goal mentions no strata, no auxiliary functions of the proof and no Clarke critical points; a formalization that adds such hypotheses, drops definability of ψ and χ, or restricts to bounded sets is a different theorem.
Welcome contributions: the elementary closure properties of o-minimal structures (definability of sums, compositions, images), the monotonicity theorem for definable functions of one variable, definable choice, cell decomposition and Whitney stratification — all reusable well beyond this mission.
Network revenue management decides, over a finite selling horizon, which products to offer to arriving customers when the products share limited resources: seats on flight legs, hotel room-nights, rental capacity. The exact dynamic program is intractable for realistic networks, so practice relies on heuristics built from a deterministic linear program (DLP), the fluid relaxation that replaces random demand by its mean. Its value is an upper bound on the revenue of every policy, and the quality of a heuristic is measured by its revenue loss against it.
For the fluid-based heuristics, the loss grows with the size of the system: a static policy derived from one DLP solution loses order when capacities and demand rates are both scaled by (Gallego and van Ryzin, 1997; Talluri and van Ryzin, 1998). Re-solving the DLP during the horizon is common practice, but for a long time it was unclear whether re-solving helps asymptotically; Cooper (2002) showed that naive re-solving can even hurt. Jasin and Kumar (Math. Oper. Res. 37(2), 2012, doi:10.1287/moor.1120.0537) proved that a re-solving heuristic with probabilistic allocation control (PAC) has a loss bounded by a constant independent of , in a model that also covers customer choice through random resource consumption. Later work (Bumpensanti and Wang, 2020, arXiv:1802.06192) removed the nondegeneracy assumption with a different re-solving rule.
The horizon is . Customer types arrive as independent Poisson processes of rates . Each of the offers belongs to one type ; iff , and . Presenting offer consumes a random vector of the resources, i.i.d. across presentations, and earns revenue , with ; models a customer who buys nothing. Resource starts with capacity , and bounds every . Write and . The DLP is
Assumption 2.1 requires to be nondegenerate with a unique optimal solution ; Assumption 2.2 requires that every optimum of the LP without capacity constraints violates .
PAC re-solves at times . At it solves with the remaining capacity, obtaining ; until it picks offer for an arriving type- customer with probability and presents it only if the remaining capacity is at least on every resource. In the -th system capacities are and rates ; is the DLP value and the revenue of PAC. Mid-point PAC re-solves at , , with the smallest integer such that : about re-solves.
There is , independent of , such that mid-point PAC satisfies
The goal fixes no constant: it asserts only that the loss is bounded uniformly in .
The result shows that re-solves suffice for a loss that does not grow with the size of the system, against an upper bound that is valid for every policy; so PAC is within a constant of the optimal policy, and the DLP bound, the optimal value and PAC are asymptotically equivalent to order . Theorem 5.3 makes the trade-off between re-solving frequency and loss explicit for any schedule, and Corollary 5.1 guarantees that re-solving in this form never worsens the static bound.
The result is proved on paper. No part of it is formalized: the mission produces a machine-checked model of a Poisson network with random consumption and a re-solving policy, a statement of LP perturbation theory for nondegenerate programs, and compound-Poisson moment bounds, each reusable for other re-solving and fluid-approximation results in revenue management.
The obvious argument compares PAC with its fluid path and bounds the deviation of the remaining capacity by a martingale estimate over the whole horizon. That gives only : deviations late in the horizon cannot be corrected. A constant bound needs re-solving to correct earlier deviations, which in turn needs the re-solved DLP solution to depend linearly and stably on the capacity deviation (the perturbation analysis of App. B) and a hitting-time estimate for when that linear regime fails. The capacity check and the coupling between the re-solved solutions and the random consumption make the process non-Markovian in the obvious state variables.
Types are Fin NT, offers Fin n, resources Fin m. The model is a structure holding , , , the consumption laws (measures on ), and the revenue functions. Standing readings (IsValid): and ; each is a probability measure with almost surely (the page has on p. 317 and on p. 327; the weaker one is used); revenue functions are measurable, vanish at , and are nonnegative and bounded by a common constant (implicit on the page). is a reading fixed by App. A.1.
is a backward recursion over the windows between re-solves. Each window holds a Poisson number of arrivals with i.i.d. types (superposition and marking), and the expected value is computed arrival by arrival with the capacity check on every resource. PAC is quantified over every DLP selector that returns an optimal solution and is measurable in the capacity, since the page leaves ties open after time 0. All constants are chosen after the instance and before , the selector, the schedule, and . Nondegeneracy follows Bertsimas–Tsitsiklis: every basic feasible solution has exactly active constraints.
Disclosed deviations from the page:
A formalization in which PAC does not check capacity, or stops checking after a hitting time, earns exactly and would make the goal trivial; the model here applies the check at every arrival. A constant chosen after would also be trivial, since the loss is at most times the revenue bound.
The source is the published Math. Oper. Res. version; printed page = PDF page + 311. Sample-path lemmas (B.2–B.4, C.1–C.3) are not stated. Contributions are welcome on the LP perturbation lemma, the compound-Poisson moment bound and the measurability of the PAC recursion, each of which stands alone.
A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, computed from a common reference string that both parties share, without revealing why the statement is true. NIZK proofs were introduced by Blum, Feldman and Micali (STOC 1988). They are a basic component of chosen-ciphertext secure encryption, signature schemes and secure multi-party computation.
Groth, Ostrovsky and Sahai (J. ACM 59(3), 2012; conference versions at EUROCRYPT 2006 and CRYPTO 2006) built NIZK proofs for all of NP from bilinear groups. The construction rests on one abstraction, the homomorphic proof commitment, and one protocol, the NIZK proof for Circuit SAT of their Figure 3. Theorem 6 says that the Figure 3 protocol works for every homomorphic proof commitment. This mission formalizes the part of Theorem 6 that holds exactly, with no computational assumption.
A homomorphic proof commitment scheme (Section 3) has a message space , a finite cyclic group with generator . It also has a randomizer space and a commitment space , both finite abelian groups. It comes with algorithms :
The exact properties used here are the following. The homomorphic property is on keys of either mode. Perfect binding says that on binding keys no commitment has openings to two different messages. Perfect completeness of the 0/1 proof says that honest proofs for are always accepted, on keys of either mode. Perfect soundness of the 0/1 proof says that on binding keys an accepted proof implies for some . Perfect extractability says that on binding keys for .
A NAND circuit on wires is a list of gates , with inputs and output , and an output wire . An assignment satisfies it, , when for every gate and .
The protocol of Figure 3 takes with . The prover commits to every wire, , with . It proves with that each contains or . For each gate it proves that contains or , using message and randomizer . The verifier checks and every 0/1 proof.
If and the scheme has the homomorphic property, perfect binding, and perfectly complete and perfectly sound 0/1 proofs, then
The theorem holds for every scheme with these properties, with no assumption on how the scheme is built.
Theorem 6 is the step from a commitment primitive to NIZK proofs for an NP-complete language. With the subgroup-decision commitment of Section 4 or the decisional-linear commitment of Section 5 it gives Corollaries 9 and 10: perfectly sound NIZK proofs for Circuit SAT with proofs of size . When the common reference string is instead a hiding key, the same protocol becomes the perfect NIZK argument of Theorem 11. Its completeness clause is the hiding-key half of the completeness formalized here.
The result is proved in the paper. Lemma 5 and the soundness of the circuit protocol are left to the reader there or proved in three sentences. No machine-checked proof of this theorem, or of any commitment-based NIZK, was found in Mathlib or in the public Lean libraries searched. This mission states its exact content against an abstract scheme interface. The same interface can then be instantiated by machine-checked versions of the concrete commitments, which are the third and fourth missions of this series.
The argument is short, so the difficulty lies in the bookkeeping. On a binding key the verifier only learns that each commitment opens to some bit. Perfect binding is what identifies the message a gate proof certifies with , which in turn identifies it with the wire bits. Lemma 5 must then be checked in rather than in the integers, where , and must be shown to differ from and . This is exactly where enters: for the all-zero assignment passes every gate check, since . The output wire is handled by the literal check together with binding. Completeness needs the prover's convention to be used consistently in the gate proofs.
ZMod N. A finite cyclic group with a chosen generator is this group, and every theorem that needs it assumes 4 ≤ N, the paper's restriction on p. 14.AddCommGroup and a finite CommGroup. Key generators are PMFs. takes its randomness as an argument.Prop, quantified over the support of the relevant generator. The paper's "for all adversaries, " (or ) is equivalent for unbounded adversaries.Fin n with an output wire. No acyclicity is required, so the statements cover every system of NAND constraints.Dropped, because they are computational:
Perfect zero-knowledge on hiding keys (Lemma 8) is the second mission of this series. The definitions of this mission (the scheme interface, NAND circuits, the protocol) are reusable by any formalization of commitment-based proof systems. Proofs of the milestones are welcome in any order.
Search engines sell advertising slots query by query. Each advertiser states a bid per keyword and a daily budget; queries arrive one at a time, and the engine must assign each to an advertiser immediately, without knowing which queries will come later. Mehta, Saberi, Vazirani and Vazirani (J. ACM 2007) called this the adwords problem and gave a deterministic online algorithm whose competitive ratio, the worst-case ratio of its revenue to the best offline revenue, tends to when bids are small compared to budgets. Section 7 of the same paper shows that this ratio cannot be beaten, even by randomized algorithms and even under the small-bids assumption. That lower bound is the subject of this mission.
Timeline of the special cases:
An instance of online b-matching has bidders and a sequence of queries . Every bidder has the same integer budget . Each query comes with the set of bidders that bid on it; the others bid .
A deterministic online algorithm processes the queries in order. When query arrives it sees the bid sets and nothing later, and it either proposes a bidder or leaves the query unallocated. The proposal succeeds if the bidder bids on the query and has won fewer than queries so far; the bidder then pays . The algorithm is not required to be greedy. Its revenue is the number of queries won. A randomized online algorithm is a probability distribution over deterministic online algorithms, fixed before the instance is chosen; its expected revenue is .
An offline allocation assigns each query to a bidder or to nobody, with full knowledge of . Its revenue is : each bidder pays for the queries it bids on, up to its budget.
The permuted round instances of the proof are as follows. For a permutation of the bidders, the instance consists of rounds of queries each, and bidders bid on the queries of round . The distribution is the uniform distribution over these instances, and denotes the average over it. The paper writes this instance with budget , bids and queries per round; the Lean development uses the same instance scaled by .
For every there is such that for all , all and every randomized online algorithm for bidders and queries, there are an instance and an allocation with
The constant is the paper's. The slack is not a weakening of the paper's claim: a competitive ratio better than would mean a ratio for some on every instance. The threshold is independent of the budget, which is how "for large " is rendered.
The result. Theorem 9 shows that the ratio attained by BALANCE for large budgets, and by the paper's tradeoff algorithm for adwords with small bids, is optimal among all online algorithms, randomized or not. Since b-matching is a special case of adwords with small bids, the same bound applies to adwords. It also answers the question of Kalyanasundaram and Pruhs on whether randomization helps for b-matching. With it contains the bipartite matching lower bound of Karp, Vazirani and Vazirani.
Formalizing it. The result has been proved since 2007; to our knowledge it has no machine-checked proof. The b = 1 case is posed on the platform as KVVMatching.UpperBound.theorem_2 (Karp–Vazirani–Vazirani), with columns arriving in reverse index order and an analysis of the algorithm RANDOM; this mission poses the budget-uniform statement in its own model. A formalization yields a reusable model of online algorithms with budgets (histories that hide the future, randomized algorithms as mixtures of deterministic rules) and a formal instance of Yao's principle for online problems.
The bound must hold for every deterministic online algorithm, including ones that are not greedy, waste proposals, or base each decision on the entire revealed history. A tempting argument fixes the algorithm's behaviour per round and treats it as oblivious to earlier rounds; that only covers a subclass. The history of the permuted instance reveals, before round , exactly which bidders dropped out in earlier rounds, so the information available to the algorithm grows round by round, and the bound on has to hold conditionally on everything revealed. Budgets interact across rounds: whether a proposal in round succeeds depends on wins in earlier rounds. Finally, the printed "at most " is false at every finite : the sum in milestone 5 exceeds by a bounded amount (about for large ), so the analytic step is genuinely asymptotic.
Fin N and query positions Fin M, both zero-based. An instance is Fin M → Finset (Fin N). A history is Fin M → Option (Finset (Fin N)) with unrevealed entries none. A deterministic algorithm is Fin M → History N M → Option (Fin N), a randomized one is a PMF over deterministic algorithms, and expected revenue is a finite sum.Khot, Kindler, Mossel and O'Donnell, Optimal Inapproximability Results for MAX-CUT and Other 2-Variable CSPs? (SIAM J. Comput. 37(1), 2007), prove that, assuming the Unique Games Conjecture, the Goemans–Williamson approximation ratio for MAX-CUT is optimal, and they extend the method to MAX-q-CUT and to Γ-MAX-2LIN(q). For the q-ary problems the key analytic input is the theorem of Mossel, O'Donnell and Oleszkiewicz (arXiv:math/0503503), the MOO theorem. It bounds the noise stability of a low-influence function with mean µ by a Gaussian quantity, the correlated Gaussian orthant probability Λ_ρ(µ): the probability that two ρ-correlated standard Gaussians both exceed the threshold t at which a single one has tail mass µ.
The hardness bounds of the paper for Γ-MAX-2LIN(q) are stated in terms of Λ_ρ(1/q). They are explicit only after Λ_ρ(µ) is estimated. Proposition 6.1 of the paper gives such an estimate in closed form, by slightly improving a bound from the proof of Lemma 11.1 of de Klerk, Pasechnik and Warners (Approximate graph colouring and MAX-k-CUT algorithms based on the theta function, J. Combin. Optim., 2004). The same quantity at µ = 1/2 is Sheppard's orthant probability (Phil. Trans. R. Soc. A 192, 1899), the source of the arccos formulas used throughout the MAX-CUT part of the paper.
This mission formalizes Proposition 6.1 and the steps of its printed proof.
Let φ be the standard Gaussian density and N the Gaussian tail probability function:
So N(x) = Pr[X ≥ x] for a standard Gaussian X. N is strictly decreasing from 1 to 0, and N(0) = 1/2.
Let X and Y be independent standard Gaussian random variables. For ρ ∈ [0, 1] put
Then (X, X′) is a centred normal pair with unit variances and covariance ρ, the pair of Definition 8 of the paper. For 0 < µ < 1 let t be the unique real number with Pr[X ≥ t] = µ, and define
The threshold t is positive exactly when µ < 1/2. Λ_ρ(µ) is the noise stability, in Gaussian space, of the indicator of a half-line of measure µ.
The proof uses two exponents. For u, v ∈ ℝ, with ρ < 1 and t > 0,
In Lean these are phi, tailN, orthantProb ρ t, Lambda ρ μ, gExp ρ t u v and hExp ρ t u v in the namespace OptInapprox.Orthant.
For any 0 ≤ µ < 1/2, let t > 0 be the number with N(t) = µ. Then for all 0 ≤ ρ ≤ 1,
The endpoint ρ = 1 is part of the goal. There X′ = X, Λ₁(µ) = µ, and (4) becomes the classical Mills-ratio inequality N(t) ≤ φ(t)/t.
Proposition 6.1 makes the MOO theorem quantitative for thresholds. With the lower bound of milestone 4 it determines Λ_ρ(µ) up to the factor 1 + ρ, and up to 1 + o(1) as µ → 0, since φ(t)/t ∼ N(t) as t → ∞ (Corollary 10, part 1). Through Corollary 10 it yields the asymptotics of qΛ_ρ(1/q) used in the paper's hardness results for MAX-q-CUT and Γ-MAX-2LIN(q). These quantities also appear in later work on q-ary noise stability and on the approximability of 2-CSPs.
The proposition is proved in the paper; nothing here is open. Mathlib (at the pinned revision) contains no proof of it, of the bivariate-normal integral representation (18), or of the Mills-ratio inequality N(t) ≤ φ(t)/t. On the platform, Mills' inequality appears only as an open statement in the two-sided form Pr[|X| > z] ≤ √(2/π)·e^{−z²/2}/z (KLTNuclear.Lasso.gaussian_tail), and there is no item for orthant probabilities. A complete development provides:
Each of these is reusable for Gaussian tail and orthant estimates.
The inequality itself is elementary once (18) and (20) are available. The work lies in the two integral identities and in their measure-theoretic glue.
For (18), the orthant probability is defined as a measure of a set under the product of two one-dimensional Gaussian laws. Writing it as a double integral of the bivariate density is a linear change of variables with Jacobian √(1 − ρ²). The shift and scaling by t then has Jacobian 1/t², and the quadratic form has to be expanded exactly.
For (20), the region u, v ≥ 0 becomes the wedge |s| ≤ r after the rotation, so the inner integral is a truncated Gaussian integral rather than a full one. The closed form appears only after an integration by parts in r, or an equivalent completion of the square.
The endpoint ρ = 1 is not covered by the printed argument, because (18) divides by √(1 − ρ²). It needs Mills' inequality separately. A proof that only treats ρ < 1 does not close the goal.
stdGaussPair is the product of two copies of Mathlib's gaussianReal 0 1 on ℝ × ℝ. orthantProb ρ t is the real-valued measure of {X ≥ t, ρX + √(1 − ρ²)Y ≥ t}, which is the representation the paper itself uses on p. 31.Lambda ρ μ chooses a t with Pr[X ≥ t] = µ, where the probability is taken under gaussianReal 0 1. Such a t is unique, so the choice does not matter. For µ ∉ (0, 1) no such t exists and the value is a placeholder 0 that no statement uses.The two remarks printed right after Proposition 6.1 (on Λ_ρ(1/2) and on removing the factor 1 + ρ) are not part of this mission.
Contributions are welcome on all four milestones, on the case ρ = 1 of the goal (Mills' inequality), and on general lemmas: N as Pr[X ≥ x], monotonicity and positivity of N, and the law of (X, ρX + √(1 − ρ²)Y) as a bivariate normal.
First-order methods for nonsmooth, nonconvex optimization (proximal algorithms, alternating minimization, subgradient-type descent) are analysed through generalized derivatives. Convergence and complexity arguments need a lower bound on the size of those derivatives away from critical points. For the Clarke subdifferential of a general lower semicontinuous function no such bound is available: Clarke subgradients can be small, or even zero, at points where the function decreases steeply along a smooth piece of its domain.
Bolte, Daniilidis, Lewis and Shiota (SIAM J. Optim. 18(2), 2007) showed that the obstruction disappears for functions whose graph admits a Whitney stratification, a partition into smooth manifolds that fit together regularly. Semialgebraic functions, and more generally functions definable in an o-minimal structure, have such stratifications. For these functions every Clarke subgradient is at least as long as the gradient of the function along the stratum through the point. This projection formula is the step from the geometry of the graph to the nonsmooth Kurdyka–Łojasiewicz inequality of the same paper, which underlies the convergence theory of many splitting methods (Attouch–Bolte–Svaiter 2013; Bolte–Sabach–Teboulle 2014).
This mission covers §2–§3 of the paper: the definitions, the projection formula (Proposition 4) and its Corollary 5 (i). The Kurdyka–Łojasiewicz part (§4) is a separate mission of the same series.
Let be lower semicontinuous, with domain and graph .
A stratification of a nonempty set is a locally finite partition of into submanifolds (the strata) such that implies for . It has the Whitney-(a) property if, whenever converge to () and the tangent spaces converge to a subspace , then ; subspaces converge in the gap . A Whitney stratification is a stratification with this property.
A stratification of is nonvertical if for every and (condition (H)). Let drop the last coordinate. For let be the stratum containing and . Nonverticality makes the tangent space of the graph of a linear form over ; the vector representing it is the stratum gradient , characterized by .
For lower semicontinuous whose graph admits a nonvertical Whitney stratification, and every ,
Further items state that the stratum gradient exists and is unique under (H), the equality when (Remark 4), the chain of (7), nonverticality for locally Lipschitz functions (Remark 3), and the nonsmooth Morse–Sard theorem of Corollary 5 (ii).
The inequality (14) says that Clarke critical points of a stratifiable function are critical points of its restriction to a stratum, and that the Clarke subdifferential is never shorter than the smooth gradient along the stratum. Two consequences are drawn in the paper. With countably many strata and the classical Morse–Sard theorem it gives a nonsmooth Morse–Sard theorem: the set of Clarke critical values has measure zero (Corollary 5 (ii)). Combined with the o-minimal Łojasiewicz inequality for the restrictions it gives the nonsmooth Kurdyka–Łojasiewicz inequality for definable lower semicontinuous functions (§4), the hypothesis behind global convergence results for proximal and splitting algorithms on semialgebraic problems.
All results of this mission are proved in the paper. None has a machine-checked proof that we know of: Mathlib has the tangent cone, Fréchet differentiability and orthogonal projections, but no stratifications, no singular or Clarke subdifferential of an extended-valued function, and no projection formula. The work is to formalize the paper's proof, which reduces the projection formula to the behaviour of Fréchet normals under limits of tangent spaces.
The first step, (11), is local and smooth: along a curve in the stratum the function is differentiable, and a Fréchet subgradient must agree with the derivative in tangent directions. The difficulty is the passage to limits in (12). A limiting subgradient at is a limit of Fréchet subgradients at points which may lie in a different, higher-dimensional stratum ; nothing in the smooth argument relates to . The relation is supplied exactly by the Whitney-(a) property, together with the compactness of the Grassmannian and the local finiteness of the stratification. Without Whitney-(a) the inclusions fail, so a proof that never uses it is wrong. The singular part requires the same argument for rescaled subgradients , whose normals become horizontal in the limit.
is EuclideanSpace ℝ (Fin n), is EuclideanSpace ℝ (Fin (n+1)) with the function value as the last coordinate, and is EReal with never . The Fréchet and limiting subdifferentials are the published NonconvexSplitting.Shared.IsRegularSubgrad and LimitingSubdiff; the tangent space (span of the tangent cone) and submanifolds (coordinate slices of some dimension) are the published ProjLikeRetr.Retractor definitions. The closed convex hull in (6) is closedConvexHull, not convexHull. Strata may be empty; local finiteness is required at points of the stratified set; a gap supremum over an empty unit sphere is . The stratification hypothesis is taken of class , the weakest case of the paper's "-Whitney".
The stratum gradient is defined intrinsically: with . It is not defined as a derivative of along the whole projected set . That set can fail to be a submanifold for a discontinuous lower semicontinuous , and every statement would then hold vacuously at such points. A companion item proves existence and uniqueness of the stratum gradient under (H), so the goal is not vacuous. The goal quantifies over all elements of ; this set may be empty (Remark 4), which is the page's restriction to , and no real-valued distance to is used.
A complete development needs the tangent space of a submanifold as the image of the chart derivative, convergence of subspaces and compactness of the Grassmannian of , Fréchet normals to epigraphs, and the density of in for lower semicontinuous . These pieces are reusable beyond this mission; the subspace gap and Whitney stratifications are prerequisites of the §4 mission. Contributions of any of the listed lemmas are welcome, as are proofs of the companion items.
Packing arc-disjoint arborescences is one of the basic tractable problems of combinatorial optimization. Edmonds' branching theorem (1973) says that a digraph contains arc-disjoint spanning arborescences rooted at a vertex if and only if every non-empty vertex set is entered by at least arcs. Its undirected counterpart is the Tutte–Nash-Williams theorem on edge-disjoint spanning trees, and Frank showed how the undirected theorem follows from the directed one through an orientation argument. Both results underlie network-design and connectivity-augmentation algorithms, and the cut condition in Edmonds' theorem is the model for many min–max theorems on packings.
Katoh and Tanigawa (2013), motivated by the rigidity of frameworks with boundaries, introduced matroid-based packings of rooted trees in undirected graphs: the roots of the trees are elements of a matroid, and every vertex must be covered by trees whose roots form a base. Durand de Gevigney, Nguyen and Szigeti (arXiv:1207.1985, 2012) gave the directed counterpart. Their Theorem 1.6 characterizes digraphs with roots that admit a matroid-based packing of arborescences, contains Edmonds' theorem as the special case of the free matroid with all roots at one vertex, and implies Katoh and Tanigawa's undirected theorem through Frank's orientation theorem. Its proof is short and purely combinatorial.
Timeline:
A digraph has a finite vertex set and a finite set of arcs, each with a tail and a head; parallel arcs are allowed. For , is the set of arcs entering (tail outside, head inside) and . An arborescence rooted at is a sub-digraph that is a directed tree in which has in-degree and every other vertex has in-degree ; the single vertex is an arborescence.
Let be a finite set and a placement of its elements at vertices (several elements may sit at one vertex). The triple is a digraph with roots. Write and . Let be a matroid on with rank function .
In Lean these are Digraph, Arborescence, MIndependent, MConnected and IsBasicPacking in the namespace BasicPackArb.Main; the proof-side notions (tight sets, domination, good and bad arcs, the parallel extension) are in a second definitions module.
The statement is universally quantified over the vertex, arc and root types, the digraph, the placement and the matroid. It has no constants.
The result. Theorem 1.6 is a good characterization: both sides can be certified, and the condition (3) is a cut condition with a submodular right-hand side. It unifies Edmonds' branching theorem (free matroid, all roots at one vertex) with matroid-constrained packings, and through Frank's orientation theorem it yields Katoh and Tanigawa's theorem on rooted-tree decompositions, which is used in combinatorial rigidity. The same paper derives from it a description of the convex hull of basic packings and a polynomial algorithm for the minimum-cost version.
Formalizing it. The result is proved on paper; no machine-checked proof of Theorem 1.6, of Edmonds' branching theorem, or of any of the claims is known on this platform. A formal proof needs a multi-digraph library with arc deletion, arborescences as sub-digraphs, in-degree functions of vertex sets and their submodularity, and matroid rank and span arguments on top of Mathlib's Matroid. The milestones follow the paper's induction on the number of arcs.
The necessity direction is a counting argument. Sufficiency is the substance. The natural first attempt, building the arborescences greedily or splitting into Edmonds instances, fails because the arborescences are not spanning and the covering condition is a base condition at every vertex, coupled through the matroid. The hard step is Claim 2.4: deleting an arc can destroy condition (3), and it must be shown that some bad arc, together with a suitable new parallel root, can be removed without doing so. Condition (3) has to be controlled for every vertex set at once, with a right-hand side that changes with the matroid. Formally, the lifting step requires gluing two arborescences with an arc and checking that the base condition survives the identification of the parallel pair.
Fintype V with decidable equality. Arcs: an ambient type with tail, head and a finite arc set arcs, so parallel arcs and loops are allowed and deletes one arc.Matroid S with ground set all of (a finite type); rank is Matroid.eRk with values in ; base is IsBase, independence is Indep.Option S with the new element none; is the comap of along , which makes none parallel to and restricts to on .A formalization in which arborescences need not lie in , or need not be reachable from their root, or in which the packing is a set of arborescences, or the per-vertex condition is "spanning" or "independent" rather than "base", states a different theorem and is ruled out by the definitions above.
Contributions welcome: proofs of the claims in any order, general lemmas on submodularity of and on tight-set uncrossing (reusable for other arborescence-packing results), and a proof of Edmonds' branching theorem as a corollary of the goal.
Training a model in machine learning means minimizing an expected loss over a data distribution, using a finite sample from it. Two families of methods dominate. Stochastic gradient methods step along the gradient of the loss at one data point: each step is cheap, but the noise forces small steps and many sequential iterations. Batch methods average the gradient over a large set of points: each step is accurate and parallelizes well, but costs a pass over the data. Bottou and Bousquet (The tradeoffs of large scale learning, NIPS 2007) compared the two by the total work needed to reach accuracy and concluded that stochastic gradient descent is preferable in large-scale learning.
Byrd, Chin, Nocedal and Wu (Sample size selection in optimization methods for machine learning, Math. Program. 2012) analyse a third option: a dynamic batch method, which takes gradient steps on mini-batches whose size grows over the run. A small batch makes early progress cheap; a large batch later makes the steps accurate. Their Theorem 4.2 shows that when the batch size grows geometrically, steepest descent with a fixed step converges linearly in expectation, and their Corollary 4.3 derives from it a total work bound of the same order as stochastic gradient descent. The analysis underlies a line of work on adaptive sampling and variance-controlled batch methods (for example Friedlander and Schmidt, Hybrid deterministic-stochastic methods for data fitting, SIAM J. Sci. Comput. 2012; Bottou, Curtis and Nocedal, Optimization methods for large-scale machine learning, SIAM Review 2018, §5.2).
Let be a probability space of data points ; in the paper is an input–output pair with distribution . The parameter is ( is the number of variables). A per-sample loss is given with gradient in , and the objective is the expected loss (2.1)
The gradient of the objective is the expected per-sample gradient, .
Uniform convexity (4.2): is twice continuously differentiable and there are constants with
Then has a unique minimizer .
For a random vector , is the sum of its componentwise variances. The variance bound (4.22) asks for a constant with
The algorithm. Fix sample sizes and a starting point . At iteration draw a batch of points, independently with law and independently of earlier batches, form the batch gradient (4.19)
and take the dynamic batch steepest descent step (4.24)
The iterates are random, and expectations below are over all batches.
If for all , for some , and (4.22) holds, then
The constants are the paper's. The goal also asserts that is integrable for every .
Milestones 3–6 are the paper's conditional expectations given , stated at a fixed point with the batch drawn afresh.
Theorem 4.2 is the convergence guarantee of the dynamic sampling strategy: it says that the noise of a mini-batch gradient does not destroy the linear rate of steepest descent, provided the batch grows geometrically. The rate makes the trade-off explicit: the optimization contracts by per step, the noise by , and the slower of the two governs. From it the paper's Corollary 4.3 bounds the total number of sample-gradient evaluations to reach by , which places dynamic batch methods on the same footing as stochastic gradient descent in the Bottou–Bousquet comparison, while keeping the parallelism of batch methods.
The result is proved in the paper; to our knowledge no machine-checked proof exists. A formalization produces a reusable account of the one-iteration analysis of a mini-batch gradient step (descent lemma, variance of an i.i.d. sample mean of random vectors, conditional expectation over a fresh batch), and of the passage from a conditional one-step recursion to an unconditional bound over a run driven by an infinite i.i.d. array. Corollary 4.3 is not part of this mission: it involves bounds, a cost model for gradient evaluations and an iteration count treated as a real number.
The arithmetic of the induction on p. 12 is short. The difficulty is in making the probability rigorous. The iterate is random, and the paper's one-step bound (4.27) is a conditional expectation given , with on the right-hand side. Turning it into an unconditional recursion requires that the batch of iteration be independent of , that be a measurable function of the earlier batches, and that and be integrable at every step, none of which is automatic for a run driven by an infinite array of draws. A naive formalization that treats as a fixed point, or as an abstract random vector with a postulated variance bound, skips exactly this content.
The variance identity for a sample mean of random vectors in and the bound from (4.2) are standard but not packaged in this form in Mathlib.
EuclideanSpace ℝ (Fin m). The paper's is written lam (λ is a Lean keyword). (4.2) is ContDiff ℝ 2 J, 0 < lam < L, and the two-sided bound on fderiv ℝ (fderiv ℝ J) w d d.Measure.infinitePi over . The finite-population factor is not modelled.Measure.infinitePi. All three are reusable beyond this mission.Barak, Goldreich, Impagliazzo, Rudich, Sahai, Vadhan and Yang proved that general-purpose program obfuscation in the virtual black-box sense is impossible (J. ACM 59(2), 2012). A natural question is whether the impossibility proof relativizes, that is, whether it survives when every party gets access to the same oracle. Proposition 4.14 of the paper shows that it does not: there is an oracle relative to which efficient circuit obfuscators exist. This is evidence that the impossibility results are not formal consequences of black-box reasoning, and a further example that relativization is a poor guide to what can be proved.
The construction obfuscates a circuit by publishing a random image , and its security comes down to one information-theoretic statement, Claim 4.14.2, restated and proved in Appendix B as Lemma B.1. A random injective function is a pseudorandom generator even against distinguishers that may query the function itself. The proof is a counting (compression) argument in the style of Gennaro and Trevisan's proof that a random permutation is one-way against nonuniform adversaries (FOCS 2000). Arguments of this kind recur in lower bounds for black-box constructions and in the theory of random oracles.
Fix natural numbers and and finite sets , of these sizes. A distinguisher receives an element and may ask an oracle for values , choosing each query point adaptively from the input and the answers so far; finally it outputs a bit. Formally is a family of query trees: a leaf carries an output bit, and an internal node carries a query point and one subtree for each possible answer in . Running against follows the branch labelled at each node; is the bit at the leaf reached. The query complexity of is the largest depth of its trees. Nothing restricts the computation between queries.
Let be uniformly random among the injective functions . For a distinguisher the two acceptance probabilities are
where and are uniform. tries to tell the output of a random seed from a uniform element of while it may query .
There is a constant such that for all sufficiently large , all , and every making at most oracle queries,
The constant is left unspecified, as in the paper; the threshold for may depend on only.
The milestones follow the proof on pp. A:43–A:45, for small and :
Lemma B.1 is the step that makes Proposition 4.14 work. Once the oracle is fixed everywhere except at the values , the simulator's only dependence on the remaining randomness is through queries to , and Lemma B.1 says that such a simulator cannot distinguish 's outputs from uniform except with probability over the oracle. A union bound over circuits and adversaries of bounded description then yields the obfuscator relative to the oracle. More broadly, the lemma is a clean instance of the principle that a random function is pseudorandom against adversaries with few queries to it, which is used in random-oracle and black-box separation arguments.
The paper gives only a sketch, and formalizing it adds more than a check. The sketch proves the density bound but asserts ; the counting bound supports the stronger statement, but the step is not written. More seriously, Property 2 of Claim B.1.1 as printed (no query of lands in , including at itself) cannot be met: a one-query distinguisher that inverts makes every bad violate it, so Claim B.1.1 is false as stated and the proof needs repair. As far as the platform's records show, no part of the argument has been machine-checked.
The naive attempt is a union bound: fix , compute the expected gap over , and apply a concentration inequality over . This fails because queries , so the events "" for different are correlated through in ways that depend on 's adaptive strategy. Neither independence nor a bounded-differences argument applies directly, since changing one value of can change many runs.
The compression argument avoids this, but each of its steps needs care. The set on which 's runs are "independent" must be chosen from a fixed so that it is cheap to describe. The simulator must answer queries without the part of being described. The saving from the Chernoff count must exceed the cost of describing inside . Queries a run makes at its own preimage must be handled separately, which is where the printed argument breaks.
The query trees are an inductive type QTree K L with constructors out : Bool → QTree K L and query : Fin K → (Fin L → QTree K L) → QTree K L, and , are Fin K, Fin L. A distinguisher is D : Fin L → QTree K L, and "at most queries" means every D y has depth at most (a real power). Distinguishers are deterministic: the probabilities in the goal are over , and only. Randomized distinguishers, averaged over their coins, are not covered, and the paper's application fixes the simulator's coins.
Every probability is a counting fraction over a finite uniform sample space: Fin K, Fin L, the embeddings Fin K ↪ Fin L, or the subsets of a given size (Finset.powersetCard). Sizes the paper writes as non-integers are floors or inequalities: and . Each is an explicit constant that depends only on . "Sufficiently small " is either an explicit range (for the elementary steps) or an existential (for the counting steps), and "sufficiently large " is an explicit threshold .
The goal quantifies , so cannot depend on or . The probability over is taken outside the absolute value: averaging the gap over would give a much weaker statement and is ruled out. Non-adaptive distinguishers or a fixed query set would also weaken the goal and are not used.
Milestone 1 is stated in a corrected form: it excludes the query at itself and reads the misprint as . Claim B.1.1 is not a milestone because it is false as printed. Milestones 4 and 6 use the printed Property 2. Contributions repairing the link between the corrected averaging step and the compression step are welcome, as are sorry-free proofs of the generic concentration milestones (2 and 5), which are reusable beyond this mission.
Training a machine-learning model usually means minimizing an expected or empirical loss over parameters . Exact gradients of such objectives are expensive, because each one requires a pass over the whole data set; practical methods replace by a cheaper approximation , for instance a gradient computed on a subsample. This raises a basic question for the analysis of optimization algorithms: how accurate must the approximate gradient be for steepest descent to keep its linear rate of convergence?
Byrd, Chin, Nocedal and Wu (Math. Program. 2012) answer this question with a relative-error condition, and use the answer to motivate a rule that increases the sample size during the run. Their §4.1 treats the deterministic case: the approximations are arbitrary vectors, and only a geometric condition linking to is assumed. That deterministic result, Theorem 4.1, is the goal of this mission. The stochastic counterpart (Theorem 4.2, dynamic batch sizes) is a separate mission of the same series.
Relative-error conditions of this kind ("the error is a fixed fraction of the step") appear throughout the literature on inexact gradient and inexact Newton methods (e.g. Bertsekas and Tsitsiklis 2000 on gradient methods with errors), and the condition (4.8) below is the deterministic template for the adaptive sampling tests later developed for stochastic optimization.
Let be twice continuously differentiable and uniformly convex: there are constants such that
Such a has a unique minimizer ; following the paper, it is normalized so that .
Fix . Given a sequence of vectors (the approximate gradients), the fixed-steplength steepest descent iteration is
The approximate gradient at iteration satisfies the relative-error condition if
Write
The constants are those of the paper and are kept explicit.
In the order the paper's proof uses them:
Theorem 4.1 says that the linear convergence of steepest descent on a uniformly convex function survives arbitrary gradient errors, provided each error is at most a fixed fraction of the approximate gradient's own norm. The price is explicit: the per-step contraction factor is instead of a factor of the form with an absolute constant , and the iteration bound (4.11) grows like times a logarithm. Because (4.8) is relative rather than absolute, no a priori bound on the error is needed, and the error may be large far from the solution. In the paper this is the motivation for requiring the sample variance of a subsampled gradient to be small relative to , which leads to the dynamic sample-size rule analysed in §4.2.
The result is proved in the paper (pp. 9–10). No machine-checked proof of it, or of any relative-error inexact gradient method with explicit constants, has been published. A formal proof provides a checked reference statement for inexact first-order methods with the paper's constants, and the milestones (4.5), (4.6), (4.13), (4.14) are reusable facts about strongly convex smooth functions and about relative-error gradient approximations.
Each step is classical, but the proof combines second-order information with metric estimates. The descent estimate (4.15) needs a second-order Taylor bound from the upper Hessian bound in (4.2), which in Lean means passing from a bound on the second Fréchet derivative to a quadratic upper bound on along a segment. The inequalities (4.5) and (4.6) relate the gradient norm to the optimality gap through the lower and upper Hessian bounds and the minimizer, and must be derived without an explicit averaged Hessian unless one is built. The convergence in (4.10) requires turning convergence of the function values into convergence of the iterates, which again uses uniform convexity. Finally, (4.11) is a logarithmic iteration count whose boundary cases (, ) must be handled. A naive reading of the iteration with exact gradients does not apply: the step is , not , and the direction is only known to be a descent direction through (4.14).
The space is EuclideanSpace ℝ (Fin m). Assumption (4.2) is a definition HessianBounds J lam L (with lam for , a Lean keyword): ContDiff ℝ 2 J, 0 < lam < L, and both bounds on the quadratic form fderiv ℝ (fderiv ℝ J) w d d. The gradient is Mathlib's gradient J. The minimizer is a point wstar with J wstar ≤ J w for all w, and J wstar = 0 is a hypothesis of the goal and of (4.17), exactly as in the paper; (4.5) and (4.6) are stated with and without it. The constant is a definition beta θ; it is never a free variable. The approximate gradients are an arbitrary sequence and nothing is random. The iterates are any sequence with w (k+1) = w k - ((1 - θ) / L) • g k for all k.
The one-step claim (4.9) assumes (4.8) only at the index ; (4.10)–(4.12) assume it at every index. (4.11) is stated in the form the proof derives in (4.18): every strictly beyond the bound has . The logarithm is natural; when Lean's convention applies, which is harmless because every iterate is then optimal. No positivity hypothesis on is added.
A trivializing formalization is excluded: the step size is fixed by the paper, and the Hessian bounds are pinned, and the hypotheses are satisfiable, e.g. by with , and .
A complete development needs: a second-order Taylor (or mean-value) bound from a Hessian bound, the strong-convexity inequalities (4.5)–(4.6), and elementary real-analysis facts about geometric sequences and logarithms. The milestones (4.5), (4.6), (4.13) and (4.14) are independent of the iteration and reusable. Proofs of any milestone, and alternative proofs with sharper constants stated as separate theorems, are welcome.
Nonlinear semidefinite programming asks to minimize a smooth function subject to smooth equality constraints and a constraint that a smooth matrix-valued function be positive semidefinite. It covers robust control design, structural optimization, and nonconvex matrix problems such as low-rank approximation and nearest-correlation-matrix problems. Algorithms for it (sequential quadratic programming, augmented Lagrangian and semismooth Newton methods) converge fast locally only when the Karush–Kuhn–Tucker (KKT) point they approach is stable under perturbation, and the question is which checkable conditions guarantee that stability.
For classical nonlinear programming the answer has been known since the 1980s: at a local minimizer, Robinson's strong second order sufficient condition together with linear independence of the active gradients is equivalent to strong regularity of the KKT point (Robinson 1980; Jongen et al. 1987; Kojima 1980). D. Sun extended this equivalence to nonlinear semidefinite programs, where the constraint cone is not polyhedral and second-order analysis carries an extra curvature term.
Timeline.
is a finite-dimensional real inner-product space, is Euclidean space, and is the space of real symmetric matrices with the Frobenius inner product . is the cone of positive semidefinite matrices. The problem is
with , , twice continuously differentiable. Write and . The Lagrangian is , and the multiplier set consists of the with , and in the normal cone (so and ). A triple with is a KKT point.
For a closed set , is the tangent cone and its lineality space. Robinson's constraint qualification at is ; constraint nondegeneracy replaces by . The critical cone is .
For with Moore–Penrose pseudo-inverse , set . Let be the metric projector, , and with . Then and . The strong second order sufficient condition (SSOSC) at is
The KKT map is on ; its zeros are the KKT points. The KKT system is also the generalized equation with and . A solution is strongly regular if, for all small , the linearized equation has a unique solution near that depends Lipschitz-continuously on . Clarke's generalized Jacobian is the convex hull of the B-subdifferential , the set of limits of Jacobians at nearby differentiability points. is the directional derivative. The uniform second order growth condition and strong stability quantify over all -smooth parameterizations of the problem.
At a local minimizer satisfying Robinson's CQ, with , the following are equivalent:
The matrix analysis of : Lemma 1 (a B-subdifferential chain rule), Lemma 2, Propositions 3 and 4 (the block structure of and ), and Proposition 7 (the inequality ). Second-order theory: Proposition 8 (the strict CQ gives a unique multiplier and ), Theorem 10 (the classical second-order conditions with the sigma term) and Lemma 11 ( equals the sigma term on ). The equivalences: Remark 15 (strong regularity iff a natural map is a Lipschitz homeomorphism), Proposition 16 ((a) ⇒ (b) ⇒ (c) at any KKT point), Lemma 18 (uniform growth ⇒ SSOSC) and Lemma 20 ().
The theorem identifies the SSOSC, a condition that can be checked from the problem data, with the stability notions that local algorithms need. Strong regularity is the hypothesis under which Newton-type methods for the KKT system converge locally and solutions vary Lipschitz-continuously with the data. Nonsingularity of gives quadratic convergence of semismooth Newton methods. Uniform growth and strong stability are what sensitivity analysis uses. Without the theorem, each of these properties has to be verified separately for semidefinite programs. The theorem also shows that the classical nonlinear programming equivalence survives on a non-polyhedral cone if the curvature term is added.
The result is proved in the literature but has no machine-checked proof. Formalizing it requires the B-subdifferential and Clarke Jacobian of the PSD projector, second order tangent sets of , and the Robinson–Kummer characterization of strong regularity. None of these exists in Mathlib. Items (g) and (i), which use the topological degree, are not formalized.
The obvious route is to copy the nonlinear programming proof: write strong regularity as nonsingularity of a reduced Jacobian on the active constraints. This fails because is not polyhedral. The KKT map is only semismooth, and its generalized Jacobian at a non-strictly complementary point is a whole family of operators, parametrized by . Nonsingularity has to be shown for every member of that family. The curvature of the cone appears only through , which links the second-order condition to the Jacobian family. The converse directions combine several external theorems (Bonnans–Shapiro's stability theory, Clarke's inverse function theorem, Kummer's characterization), each needing nonsmooth infrastructure.
All objects are defined in SunNLSDP.Equiv.Setting. is the subspace of symmetric vectors in EuclideanSpace ℝ (n × n) for a finite index type n, so its inner product is exactly the Frobenius product. and are WithLp 2 products, carrying the sum of the inner products. is computed by the continuous functional calculus. The metric projector returns its argument when no minimiser exists; it is applied only to nonempty closed convex sets. Clarke's Jacobian, , the one-sided directional derivative, the normal cone and the lineality space are the published definitions NonsmoothNewton.Shared.clarkeJac, NonsmoothNewton.Local.dirDeriv and RobinsonSR.Reduction.Setting.
Conventions committed to:
Items (g) and (i) of Theorem 21 are omitted, because Brouwer degree is unavailable; no surrogate for the index is substituted. A formalization that reads the CQs or nondegeneracy as two decoupled equations, or states SSOSC only on instead of , proves a different theorem and is ruled out.
Reusable infrastructure: the PSD projector and its generalized Jacobians, second order tangent sets, the Moore–Penrose pseudo-inverse of symmetric matrices, and the characterization of strong regularity by Lipschitz homeomorphisms. Proofs of individual milestones are welcome, as are lemmas on and on strong regularity of generalized equations.
Augmented Lagrangian methods are among the standard ways to solve smooth nonlinear programs. They replace a constrained problem by a sequence of subproblems in which some constraints are moved into the objective through a penalty term and multiplier estimates. The method of Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18(4), 2007) is the theory behind the ALGENCAN solver. It moves only the "upper-level" constraints into the objective, keeps arbitrary "lower-level" constraints in the subproblems, and requires the subproblems to be solved only approximately.
A convergence theory for such a method has to say what the limit points of the iterates are. This mission is about the second half of that theory (Theorem 4.2): a limit point that is feasible is a KKT point of the original problem, provided it satisfies a weak constraint qualification, the constant positive linear dependence condition (CPLD) of Qi and Wei (SIAM J. Optim. 10(4), 2000). Earlier global convergence results for augmented Lagrangian methods, such as Conn, Gould and Toint's, assumed linear independence of the active gradients (LICQ) at all limit points. CPLD is implied by MFCQ and by LICQ, holds automatically for linear constraints, and is required only at feasible points.
Timeline of the relevant notions:
The problem (2.1) is
with and constraint maps into , all continuously differentiable. and .
The augmented Lagrangian with respect to (2.2) is
Algorithm 3.1 works in outer iterations with a penalty parameter and safeguarded multipliers , that stay in fixed boxes. At iteration it finds and lower-level multipliers , that satisfy the KKT conditions of "minimize on " up to a tolerance . It then computes the first-order estimates and . Finally it increases by a factor unless a feasibility-complementarity measure has decreased by the factor .
A point satisfies CPLD if, whenever some gradients of constraints active at have a nontrivial vanishing linear combination with nonnegative coefficients on the inequalities, those gradients remain linearly dependent at every point of a neighbourhood of .
If is a limit point of and satisfies CPLD with respect to all constraints of (2.1), then is a KKT point of (2.1). If moreover satisfies MFCQ and , then
The theorem says that the algorithm has the right limit points: a feasible limit point is stationary under a constraint qualification weaker than MFCQ and LICQ, with no assumption on the penalty parameters. Milestone 3 is a result of independent interest: an "approximate KKT" sequence converges to a KKT point under CPLD. This sequential argument was later developed into the theory of approximate KKT conditions (Andreani, Haeser & Martínez 2011), and it applies to any algorithm that produces approximate KKT points, not only to this one. Milestone 4 gives the classical fact that MFCQ bounds the multipliers of such sequences.
All results are proved in the paper. As far as is known, none has a machine-checked proof. Neither CPLD nor the augmented Lagrangian method of this paper is formalized in Mathlib or on the platform. The companion missions of this series formalize Theorem 4.1 (feasibility of limit points) and Theorem 5.4 (boundedness of the penalty parameters).
The obvious argument divides the approximate KKT relation by the size of the multipliers, passes to the limit and obtains a contradiction with the constraint qualification. Under CPLD this argument fails, because CPLD does not bound the multipliers: they may diverge along the sequence even though the limit is a KKT point, and the limit of the normalized relation need not contradict anything at itself. CPLD speaks about linear dependence on a whole neighbourhood of , while the relation holds only at the iterates, so the information has to be transferred from to nearby points. A pointwise version of CPLD (dependence at only) is plain positive linear dependence, and with it the statement is false.
A second difficulty is complementarity (milestone 2). The safeguarded multipliers do not vanish on inactive constraints. Whether does depends on whether the penalty parameters are bounded, which needs the update rule of Step 4.
is EuclideanSpace ℝ (Fin n) and is Mathlib's gradient. The problem is a structure of component functions indexed by Fin m. The standing assumption "continuous first derivatives on a sufficiently large and open domain" is read as ContDiff ℝ 1 on all of .
A run of Algorithm 3.1 is a predicate on sequences (IsRun), not a computed object:
KKT, CPLD and MFCQ are defined once for an abstract program with finite index types. The constraints of (2.1) enter as the families and :
"Limit point" is MapClusterPt. (4.8) is required for every strictly increasing reindexing converging to , and it bounds the unsafeguarded estimates , ; the safeguarded ones are bounded by construction and would make (4.8) trivial.
Trivializing formalizations are ruled out:
Contributions welcome: proofs of the four milestones and of the goal, and in particular a reusable conic Carathéodory lemma and a library-level "approximate KKT + CPLD ⇒ KKT" theorem (milestone 3), which is useful well beyond this paper.
Augmented Lagrangian methods solve a constrained problem by minimizing a sequence of penalized subproblems while updating estimates of the Lagrange multipliers. Each subproblem carries a penalty parameter . When grows without bound the subproblems become ill-conditioned and hard to solve, and the method behaves like a plain external penalty method. Avoiding that growth is one of the main reasons for using multiplier updates at all, so conditions under which stays bounded matter both in theory and in practice (Bertsekas 1982; Conn, Gould, Toint 1991).
Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18 (2007); HAL hal-01295437) propose an augmented Lagrangian method, Algorithm 3.1, in which only some of the constraints are penalized. Their §5 shows that, under classical local hypotheses at the limit point and a subproblem tolerance tied to the current infeasibility, the penalty parameters remain bounded. This mission formalizes that result for equality-constrained problems (Theorem 5.4), together with the general case (Theorem 5.5) as a companion statement.
Let , , , , be continuously differentiable. Problem (2.1) is
The upper-level constraints are penalized by the PHR augmented Lagrangian
while the lower-level constraints stay in the subproblems.
Algorithm 3.1 fixes , , , a box , a bound and tolerances . At outer iteration it finds and lower-level multipliers such that is an -approximate KKT point of minimizing over the lower-level set, in the sense of (3.1)–(3.4). It then forms the first-order multiplier estimates
and safeguarded estimates , which in §5 are the projections of on their boxes. Finally it updates the penalty parameter: with ,
In §5.1 there are no inequality constraints (): problem (5.1), with Lagrangian . Assumptions 1–6 at the limit of are: convergence, feasibility, linear independence of all constraint gradients, near , the second-order sufficient condition with multipliers , and in the interior of the safeguard box.
Under Assumptions 1–6, , and for a sequence ,
with and . 4. (5.10): if , then for large. 5. Contraction: if , then for large.
Theorem 5.5, the general problem (2.1) under Assumptions 7–13 (LICQ, , a second-order condition on the tangent subspace of all active constraints, multipliers inside the safeguard boxes, strict complementarity for the active upper-level inequalities), with ; and two steps of its proof, (5.13) and (5.14).
Theorem 5.4 tells a user of the method when it does not degenerate: if the safeguard box contains the true multipliers and the subproblems are solved to a precision proportional to the current infeasibility, then the penalty parameter is eventually constant. The Remark after Theorem 5.5 draws the practical conclusion that the box should be large enough to contain the true multipliers. The result underlies the analysis of the ALGENCAN solver built on Algorithm 3.1.
The results are proved on paper. To our knowledge none of them, nor the PHR augmented Lagrangian method itself, has a machine-checked formalization. A formal proof would also pin down two gaps in the printed statements, recorded under Formalization scope: the case and the early iterations in Lemma 5.3. The local analysis (a uniformly nonsingular KKT matrix and implicit-function error bounds for multiplier estimates) is reusable for other augmented Lagrangian and SQP methods.
Without the second-order structure there is no reason for to stay bounded: the update test compares consecutive infeasibilities, and nothing in the global theory forces them to decrease geometrically. The local argument has to show that contracts by a factor of order , which requires error bounds for both and that hold uniformly as varies in an interval containing . The uniformity in the perturbation parameter , around the singular-looking limit , is the central difficulty. Applying the implicit function theorem at each fixed does not give it.
is EuclideanSpace ℝ (Fin n). Constraint maps are families of real functions indexed by Fin m, and problem (5.1) is (2.1) with . The norm in (3.1), on and on is Euclidean. Every , and the norms in (3.4), on and on , are the sup norm. The paper's norm is arbitrary and the constants absorb the change. A run of Algorithm 3.1 is a predicate on sequences: x 0 is , the outer iterations are , and the three tolerances of Step 2 are kept separate. The gradient in (3.1) is the true gradient of the defined augmented Lagrangian. "Continuous first derivatives" is on ; "continuous second derivatives near " is ContDiffAt ℝ 2. Hessians are derivatives of gradients. Every statement that uses a Hessian assumes at , so it cannot be a junk value. Assumption 5 is pinned to Fletcher's equality-constrained second-order sufficient condition. Linear independence is that of a family indexed by a sum type, so equal gradients count as dependent.
Added hypotheses, each stated in the item's Formalization Note:
Statements that would trivialize the goal are excluded. These include a run predicate that no sequence satisfies, merging the three tolerances into , collapsing gradient families into sets, a junk Hessian, and assuming or in the goal. The last two appear only as milestone hypotheses.
A complete development needs the PHR gradient formula, uniform invertibility of a continuous family of matrices on a compact interval, a quantitative inverse function estimate for maps, and the convergence of multiplier estimates under LICQ. Proofs of any milestone, and reusable lemmas for these pieces, are welcome.