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?
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.
The proximal algorithm is the basic implicit scheme for minimizing a function : from the current point it moves to a minimizer of plus a quadratic penalty on the distance travelled. For convex its convergence theory is classical (Martinet 1970, Rockafellar 1976). For nonconvex, nonsmooth the situation is different: descent and boundedness give only that limit points are critical, and the whole sequence may fail to converge even for smooth (Palis–de Melo; Absil, Mahony and Andrews, SIAM J. Optim. 2005).
Attouch and Bolte (Math. Program. 116, 2009, online 2007; author's version hal-00803898) showed that the Łojasiewicz inequality, which holds for real-analytic functions and for continuous subanalytic functions, restores convergence of the whole sequence for the nonsmooth proximal algorithm, together with explicit rates. The argument is Łojasiewicz's original gradient-flow idea transferred to a discrete, nonsmooth setting. It became the template for the later convergence analyses of proximal alternating minimization, forward–backward splitting and PALM under the Kurdyka–Łojasiewicz property, which are used throughout nonconvex optimization, signal processing and machine learning.
Timeline:
Points live in with the Euclidean norm . Let be proper (never , finite somewhere) and lower semicontinuous, with domain .
The limiting subdifferential is the set of limits of Fréchet subgradients along sequences with . A point with is critical, and the set of critical points is .
Fix and step sizes . From an arbitrary the proximal algorithm produces
Any minimizer may be selected. The standing hypotheses are
with the convention (Remark 4). The number in (5) at a point is a Łojasiewicz exponent of that point.
denotes the set of limit points of .
Under (H1), (H2), (H3), if is bounded then
It fixes no constants and holds for every admissible step sequence and every selection in (2).
Theorem 5 (rates): with a Łojasiewicz exponent of , gives finite termination, gives with , and gives . Also: well-posedness of (2) under (H1), Proposition 2 (v), and Remark 2.
The theorem turns subsequential convergence into convergence of the whole sequence, with finite length, for a class that includes semi-algebraic, real-analytic and continuous subanalytic functions. Finite length is the property later used to analyse splitting and alternating schemes under the Kurdyka–Łojasiewicz property, and Theorem 5 is the first rate classification by the Łojasiewicz exponent for a nonsmooth algorithm.
The results are proved on paper. No machine-checked proof of Theorem 4 or Theorem 5 is known to exist. A formalization adds a checked convergence theorem for the nonsmooth proximal algorithm with extended-real-valued , and a reusable set of descent, limit-set and uniformization lemmas that apply to other Łojasiewicz-type analyses.
Descent and give only , which does not imply convergence: the iterates can circle a continuum of critical points with square-summable but non-summable steps, as in the counterexamples for smooth functions. The step that must be supplied is summability of itself. The local inequality (5) holds only near one critical point with its own constants, while the iterates approach a whole compact set , so the local constants first have to be made uniform near that set. The nonsmooth setting adds two difficulties: takes the value , and subgradients are limits of Fréchet subgradients, so their closure properties have to be established for this subdifferential.
is EuclideanSpace ℝ (Fin n); is allowed. is EReal-valued and proper means never and somewhere not . Lower semicontinuity is Mathlib's LowerSemicontinuous. (H2) is ContinuousOn f {x | f x ≠ ⊤}. The limiting subdifferential and are the published platform definitions NonconvexSplitting.Shared.LimitingSubdiff and NonsmoothLojasiewicz.Continuous.crit. Algorithm (2) is a predicate on a sequence (every step is some minimizer), not a proximal map. Limit points are cluster points of the sequence. The power in (5) is lojPow θ s = if s = 0 then 0 else s ^ θ, which implements ; real values of are used only where is finite.
Standing assumptions carried by the goal and Theorem 5: proper and lower semicontinuous, (H1), (H2), (H3), with , a sequence complying with (2), and boundedness of its range. Milestones drop the assumptions their claims do not use. The milestones (8) and (9) also assume for all and use . Both come from the proof's normalization. This reduction is not a hypothesis of Theorem 4: a goal that assumed it, mentioned the constants , or assumed (8) would not be the paper's theorem.
The development needs the closure properties of the limiting subdifferential, the Fermat rule for proximal steps, and compactness and connectedness of limit sets of sequences with vanishing steps. These are reusable for every Łojasiewicz-type convergence proof. Proofs of individual milestones, of the rate lemmas in the proof of Theorem 5, and of the example are welcome.
Augmented Lagrangian methods (the method of multipliers of Hestenes, Powell and Rockafellar) solve a constrained nonlinear program by a sequence of easier subproblems in which some constraints are moved into the objective through a penalty term plus a multiplier estimate. Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18 (2007); preprint HAL hal-01295437) split the constraints into upper-level constraints, which are penalized, and lower-level constraints, which are kept in every subproblem and may be arbitrary (not only bounds). This is the design of the solver ALGENCAN and of its successors.
A practical method usually cannot guarantee that its iterates approach a feasible point: the problem may be infeasible, and even when it is not, a local method may stall. The question this mission formalizes is what a limit point of the method is when the penalty parameter is or is not driven to infinity. The answer, Theorem 4.1 of the paper, states that infeasible limit points are not arbitrary: they are stationary for the problem of minimizing the upper-level infeasibility over the lower-level set, unless a weak constraint qualification fails there.
The problem is (2.1):
with , , , , , all continuously differentiable. Write and .
The PHR augmented Lagrangian (2.2) with respect to is, for , , ,
Algorithm 3.1 has parameters , , , boxes and , and tolerances with . At outer iteration it finds and lower-level multipliers , satisfying the approximate KKT conditions (3.1)–(3.4) of minimizing over to tolerance ; it chooses new safeguarded multipliers , in the boxes; and it keeps when
and sets otherwise. A run is a sequence produced this way in which the subproblem of Step 2 is always solvable.
A point is a KKT point of a problem with objective , equalities and inequalities if it is feasible and for some and some vanishing on inactive inequalities. The constant positive linear dependence condition (CPLD, Qi and Wei) holds at if every nontrivial null combination of gradients of equalities and active inequalities, with nonnegative coefficients on the inequalities, has gradients that remain linearly dependent at every point near . CPLD is weaker than both LICQ and the Mangasarian–Fromovitz condition.
Let be a run and a limit point of it. If is bounded, then . Otherwise at least one of the following holds:
Theorem 4.1 is the feasibility half of the global convergence theory of the method; Theorem 4.2 of the same paper (a companion mission) shows that feasible limit points satisfying CPLD are KKT points of (2.1). Together they say that the method either finds a stationary point of the original problem or a stationary point of the infeasibility, under a constraint qualification weaker than MFCQ and only at the limit point. Because the lower-level set is arbitrary, the theorem covers the many variants in which bounds, linear constraints or structured sets are kept out of the penalty.
The result is proved in the paper; no machine-checked proof of it is known. Formalizing it requires the gradient of the PHR function, a conic Carathéodory theorem with linear independence (Mathlib contains only the convex-hull version), and the subsequence and normalization arguments of the proof. Each is reusable: milestone 5 is used again, unchanged, in the proof of Theorem 4.2.
The bounded case is elementary. The unbounded case is where the work lies. Dividing the approximate stationarity condition by removes the objective and the multiplier estimates, but the lower-level multipliers divided by need not stay bounded, so no limit can be taken directly. The supports of the lower-level combinations must first be reduced to linearly independent ones, uniformly along a subsequence, before the bounded/unbounded dichotomy on the reduced multipliers yields either a KKT point of (4.1) or a nontrivial null combination at whose gradients are independent at points arbitrarily close to . Taking limits of the original multipliers without this reduction does not work.
is EuclideanSpace ℝ (Fin n); constraint maps are families of real functions indexed by Fin m. Continuous differentiability "on a sufficiently large and open domain" is read as on all of . The norm in (3.1) is the Euclidean one; (3.4), Step 4 and the vectors , use the sup norm. The paper's norm is arbitrary and the results do not depend on the choice. A run is a predicate on sequences indexed by : x 0 is the initial point , the outer iterations are , the three subproblem tolerances are kept separate, and is the true gradient of the defined function (2.2). "Limit point" is a cluster point of the sequence; "bounded" is boundedness above of . KKT and CPLD are defined once for arbitrary finite index types; CPLD carries no feasibility clause, and linear independence is that of a family indexed by a disjoint union, so a repeated gradient counts as dependent.
No hypothesis is added to Theorem 4.1 beyond the reading. Junk values cannot trivialize the statement: the run evaluates (2.2) and only at ; the gradients are taken of functions; the run is satisfiable; and both alternatives (i) and (ii) can fail at the same point, so the second half of the theorem has content.
Contributions are welcome on every milestone. The gradient computation (4.2) and the conic Carathéodory theorem are self-contained and useful beyond this paper.
Multistage stochastic linear programs model sequential decisions under uncertainty: capacity and reservoir planning, hydro-thermal scheduling, inventory and asset–liability management. When the data process is stagewise independent, the problem decomposes by dynamic programming into one linear program per stage, coupled through expected cost-to-go functions. These functions are convex and piecewise linear, and the stochastic dual dynamic programming (SDDP) method of Pereira and Pinto (1991) approximates them from below by cutting planes. SDDP is the standard solution method in the long-term planning of hydro-dominated power systems, and its convergence theory determines what the bounds it reports actually mean.
Shapiro's paper (Optimization Online 2009/12/2509; European J. Oper. Res. 209(1), 2011, doi:10.1016/j.ejor.2010.08.007) analyses SDDP applied to a sample average approximation (SAA) of the true problem, with all of the data random. Its convergence result, Proposition 3.1, asserts finite convergence with probability one when the forward scenarios are subsampled independently. A related almost-sure finite convergence theorem for a different algorithm (DOASA, with randomness only in the right-hand sides and cut sharing across outcomes) is due to Philpott and Guan (2008); it is posed as a separate mission on this platform and is not restated here.
There are stages. The decision satisfies and, at the first stage, with deterministic data . For the data are replaced by a sample , , each with probability , independently across stages, and the stage- constraint is . The SAA cost-to-go functions are defined backwards from :
A scenario is a choice ; there are of them, each of probability . A policy depends only on the outcomes up to stage ; it is optimal for the SAA problem if it is feasible on every scenario and its expected cost is minimal.
SDDP keeps, for each stage, a finite set of cuts whose maximum lies below . An iteration has a forward step: scenarios are sampled, and along each of them the decisions solve the stage problems with in place of , (3.13)–(3.14). It also has a backward step: from down to , at each trial point the stage- problems with the current cuts are solved for all outcomes, and the cut (3.17) is added, where averages over basic optimal (extreme-point) dual solutions .
Suppose the forward scenarios are drawn independently and uniformly from the SAA scenarios, (A1) holds ((3.13) and (3.14) have finite optimal values for every scenario at every iteration), and the backward steps use basic optimal dual solutions. Then
The goal fixes no iteration count, no rate and no number of forward scenarios .
The result separates SDDP's sampling from its convergence: on a finite scenario tree, independent subsampling of forward paths suffices for the method to stop at an optimal policy, without ever enumerating the tree. It explains why the lower bound eventually equals the SAA optimal value, which is what makes the gap-based stopping rules of the paper (§3, Remarks 4–6) meaningful. The paper's closing remark stresses that without independence of the forward scenarios there is no guarantee of convergence.
The proposition is proved in the paper. No machine-checked proof of it, or of any SDDP convergence theorem, exists to our knowledge. Formalizing it requires a precise account of what the method is: which dual solutions, which forward solutions, which order of updates. Several of these points are left implicit on the page.
Finiteness of the cut universe (milestones 4–5) is a statement about extreme points of dual polyhedra whose dimension grows with the cut sets of the next stage, so it must be organized stage by stage from down. The central difficulty is the last step of the argument. Once the approximations have stopped changing, one must show that the stable cuts are exact where the forward policy goes, so that the forward policy satisfies (3.18). The obvious argument, "if (3.18) fails at the last stage where it fails, the next cut there increases ", does not work as printed: (3.18) holding at later stages does not by itself make the next-stage approximation exact at the trial point. Closing this step is where the conventions on forward solutions and on sampling listed below become essential.
The Lean development is in the namespace ShapiroSDDP.Convergence. Stages are numbered
; the data of stage are stored under index (the coupling matrix is indexed by the
decision it multiplies); V t is , with V t ≡ 0 for . Cost-to-go
values are real infima, used only on reachable decisions. The explicit readings are:
iIndepFun);Optimality of a policy is defined by expected cost, never by (3.18), so that milestone 6 is not definitional. Sampling is stated as i.i.d. uniform draws, not as "every scenario recurs", which is milestone 7. All of depend on the outcome. If some lacks full row rank, no basic dual solution exists and no run exists; a sorry-free witness instance shows that all hypotheses of the goal can hold together.
Useful infrastructure: LP weak and strong duality (LinearOptimization.lp_weak_duality,
LinearOptimization.lp_strong_duality exist on the platform in their own encoding), finiteness of
extreme points of polyhedra, attainment for polyhedral objectives, and the second Borel–Cantelli
lemma (ProbabilityTheory.measure_limsup_eq_one). Proofs of any milestone, and reusable lemmas on
LPs with cut epigraphs, are welcome.
In shop scheduling, jobs consist of chains of operations, each to be processed on a prescribed machine, and the goal is to minimize the makespan, the time at which the last operation finishes. Almost every approximation algorithm for job shops, acyclic job shops and flow shops is analysed against one quantity: the trivial lower bound , where the congestion is the largest total processing time requested on one machine and the dilation is the largest total processing time of one job. Any schedule has makespan at least .
How weak can this bound be? Leighton, Maggs and Rao (1994) showed that for acyclic job shops with unit-length operations the optimum is . For operations of arbitrary length, Feige and Scheideler (2002) proved an upper bound of for acyclic job shops, and gave acyclic job shop instances whose optimum is . Flow shops, in which every job visits every machine in one common order, are much more structured, and no flow shop instance with optimum was known. Feige and Scheideler asked whether flow shops admit a significantly better upper bound. Mastrolilli and Svensson (J. ACM 2011, Theorem 1.1) answered this negatively by constructing flow shops whose optimal makespan is a factor above .
Timeline:
A job shop instance has machines and jobs; job is a sequence of operations , operation needs time units without interruption on machine . A feasible schedule assigns a start time to every operation so that each operation starts after the previous operation of its job has completed, and no two operations on one machine overlap. A zero-length operation therefore still occupies an instant on its machine: it cannot be performed strictly inside another operation there. The makespan is the largest completion time.
The instance , for natural numbers :
Operations of positive length are long-operations, the others short-operations. For a schedule, the -th long-operation of a job of frequency is good if the delay from its end to the start of the next long-operation of is at most ; the last long-operation of a job is never good. is the set of first halves of the good long-operations on machine , and the total time they cover.
For all natural numbers and : every job of has length , every machine has load (so ), and every feasible schedule satisfies
With this gives the paper's statement, an optimal makespan of .
The theorem shows that the lower bound , against which all known flow shop algorithms are analysed, can be off by a factor growing with . Any flow shop algorithm with guarantee relative to the optimum must therefore use a stronger lower bound than . The same frequency construction is the gap gadget behind the paper's inapproximability results for generalized flow shops and job shops (Theorems 1.2 and 1.3).
The result has been proved since 2011; as far as is known it has no machine-checked proof. The mission produces a formal model of the instance , a formal proof of the explicit bound for every , , and reusable statements about delays and first-half intervals in the published job shop model JobShopLTAS.Core.Instance.
The bound must hold for every feasible schedule, with no structural restriction such as a permutation or non-delay schedule. The obvious approach, comparing each machine's load with the makespan, only gives , since every machine carries exactly . The gain comes from interaction between machines of different frequencies in one group: a high-frequency job running in parallel with a low-frequency long-operation is held back by its zero-length operation on the low-frequency machine. Turning this into a quantitative bound requires controlling, for every job at once, how long it waits between consecutive long-operations, and that waiting is only bounded when the makespan is already small. Encoding the index arithmetic of (groups, frequencies, copies, positions of the long-operations) and the zero-length operations faithfully is a substantial part of the work.
JobShopLTAS.Core.Instance: machines Fin m, jobs Fin n, real processing times and start times, IsFeasibleSchedule Finset.univ s (nonnegative starts, chain precedence, disjunctive machine constraint s o + p o ≤ s o' ∨ s o' + p o' ≤ s o) and makespan Finset.univ s. Under that constraint a zero-length operation cannot sit strictly inside another operation on its machine, which the paper's argument needs.Welcome contributions: proofs of the counting facts about the encoding, of the milestones, and general lemmas about feasible schedules in JobShopLTAS.Core.Instance (completion time of a job bounds its delays; disjoint intervals in have total length at most ).
A sparse graph that approximates a dense one, in the sense that both have nearly the same Laplacian quadratic form, can stand in for it in every algorithm that only reads cuts or solves Laplacian linear systems. Spielman and Teng introduced such spectral sparsifiers and built them in nearly linear time; the construction is the sparsification step of their nearly-linear-time Laplacian solver (arXiv:0808.4134, SIAM J. Comput. 40(4), 2011).
Sampling edges at random works well only inside a graph of high conductance, where no vertex set is separated from the rest by few edges. A general graph is therefore first cut into pieces of high conductance, with few edges running between the pieces. Section 7 of the paper proves that such a decomposition always exists. A similar result was obtained independently by Trevisan (2005). The decomposition theorem, together with the sampling theorem of §6, already shows that every graph has a spectral sparsifier with edges; the algorithmic decomposition of §8, which the fast algorithm uses, is an approximate version of it, and its analysis rests on the same certificate lemma.
Let be a finite simple undirected graph with edges, and write for the degree of vertex . For disjoint , is the set of edges with one end in and one in . The volume of is ; in particular .
For a vertex set and , the conductance of inside is
and the conductance of is over proper subsets, with when . Volumes are always measured with the degrees of , never with the degrees inside the induced subgraph ; consequently is at most the usual conductance of , and lower bounds on transfer to it.
A decomposition of is a partition of . It is a -decomposition if for all , and its boundary is the set of edges between different parts,
In Lean: vol G S, cutEdges G S T , condRel G B S , cond G B , and decompBoundary G P for a Finpartition P of the vertex set, all in the namespace SpectralSparsify.Decomp.
Every graph without isolated vertices has a decomposition with
The constants are the paper's. Both conditions must hold for one and the same partition.
The theorem says that every graph is, after removing at most half of its edges, a disjoint union of pieces of conductance . By Cheeger's inequality each piece then has normalized spectral gap , which is the hypothesis under which the random sampling of §6 produces a spectral approximation; applying the theorem recursively to the removed edges gives the existence of spectral sparsifiers with edges (§7.2). Decompositions of this kind, now called expander decompositions, have become a standard tool in graph algorithms.
The theorem is proved in the paper; to the knowledge of this mission it has no machine-checked proof. What the mission produces is a formal proof of the existence statement with the paper's explicit constant, a formal Lemma 7.2 (the certificate lemma that also drives the approximate version, Theorem 8.1), and reusable Lean definitions of volume, relative conductance and decomposition boundary for finite simple graphs.
The obvious argument, cutting along any sparse set until no sparse set is left, controls the conductance of the final parts but not the number of edges cut: a long sequence of small sparse cuts can remove far more than half of the edges. The difficulty is to show that one well-chosen cut leaves a remainder whose conductance is certified without further search, which is the content of Lemma 7.2. Its hypothesis is a maximality condition over all subsets of , and its conclusion concerns all subsets of , a different set measured with the same ambient degrees, so the two cannot be compared directly. The existence statement then needs a well-founded description of the recursion, a bound on its depth, and an accounting of the cut edges level by level, all against the explicit constant .
Graphs are SimpleGraph V on a finite vertex type with decidable adjacency; vertex sets are Finset V; volumes, conductances and the bound on are real numbers; decompositions are Finpartition (Finset.univ : Finset V); is Real.logb (4/3).
Hypotheses made explicit:
∀ v, 0 < G.degree v) in Theorem 7.1, Lemma 7.2 and the milestones that divide by a volume. The paper leaves it implicit: is for sets of isolated vertices, and with Lean's Lemma 7.2 would be false (one edge plus two isolated vertices is a counterexample). Under the hypothesis forces , and Theorem 7.1 is then trivially true.Conventions: is the minimum over proper subsets, the empty set contributing ; for ; counts ordered adjacent pairs in , which is the edge count for disjoint sets. Neither conclusion of Theorem 7.1 may be dropped: the partition into singletons satisfies the conductance bound and the partition into one part satisfies the boundary bound, so a formalization keeping only one conclusion is trivial.
Not formalized: idealDecomp as an object (step 2 involves a choice, so it is a relation rather than a function; the goal is the existence statement), its termination and depth bound as separate items, the λ-spectral decomposition remark via Cheeger's inequality, the existence sketch for sparsifiers in §7.2, and the algorithmic analogue of §8. Contributions welcome: proofs of the milestones, a formal recursion for idealDecomp, and lemmas on volume and edge-boundary arithmetic that other graph-partitioning missions can reuse.
Many graph algorithms run in time proportional to the number of edges. A sparsifier of a weighted graph is a graph on the same vertices with far fewer edges that approximates for the purpose at hand, so that the algorithm can be run on instead. Benczúr and Karger (1996) showed that every graph has a sparsifier with edges preserving the weight of every cut up to a factor . Spielman and Teng (2004) introduced the stronger spectral notion, in which the Laplacian quadratic form is preserved for every real vector, not only for cut indicators; their sparsifiers had edges for a large constant and were the first step of their nearly-linear-time solvers for symmetric diagonally dominant linear systems.
Spielman and Srivastava (arXiv:0803.0929, STOC 2008, SIAM J. Comput. 2011) proved that independent sampling of edges, each edge with probability proportional to its weight times its effective resistance, yields a spectral sparsifier. The result improved both earlier bounds, replaced a recursive partitioning construction by a one-line sampling rule, and made effective resistance a standard tool in graph algorithms. Batson, Spielman and Srivastava (arXiv:0808.0163) later obtained edges deterministically, by a slower method built on the same matrix .
Let be a connected weighted undirected graph with vertices, edges and weights . Orient every edge arbitrarily, so that it has a head and a tail (distinct vertices).
There are an absolute constant and a threshold such that, for every , every connected weighted graph on vertices and every , with , with probability at least
The constant is left unfixed; the statement asserts the shape with the paper's explicit dependence on .
Theorem 1 says that every weighted graph is spectrally approximated by a reweighted subgraph with edges. A spectral approximation preserves cut weights, the eigenvalues of the Laplacian up to , effective resistances, and the condition number of as a preconditioner, so any algorithm whose output depends on these quantities can run on . Combined with fast approximate computation of effective resistances (the second mission of this series), it gives a nearly-linear-time construction, and it is the sampling step used in Laplacian solvers, in sparsification of sums of rank-one matrices, and in leverage-score sampling for regression, where is exactly the statistical leverage of a row.
The result is proved in the paper; to our knowledge no machine-checked proof exists. This mission formalizes the statement and the paper's proof structure: the linear algebra of (Lemma 3), the deterministic reduction from quadratic forms to a spectral-norm bound (Lemma 4), and the matrix concentration inequality (Lemma 5), which is the substantive analytic input and is itself a reusable result about sums of independent rank-one matrices.
The deterministic part is linear algebra over the pseudoinverse. The obstacle is concentration: the expected Laplacian of equals , but bounding the deviation uniformly over all is a statement about the spectral norm of a random matrix, and a union bound over a net of directions costs a factor of in the sample count rather than . Scalar Chernoff bounds per cut, which suffice for cut sparsifiers, do not give the spectral statement. Lemma 5 is the matrix inequality that removes this loss, and no inequality of this kind (a concentration bound for the spectral norm of a sum of independent random matrices) is in Mathlib.
All declarations sit in the namespace EffResSparsify.Sampling.
WGraph V E with orientation maps head, tail : E → V, weights w : E → ℝ, and the fields head e ≠ tail e (no loops) and 0 < w e. Parallel edges are allowed; nothing in §3 uses simplicity. Connectivity is a separate hypothesis on the underlying simple graph and includes . In Theorem 1 the vertex type is Fin n; the edge type is an arbitrary finite type.HarmonicGames.Decomposition.pinv of on Euclidean ; it equals the spectral formula above and is the gauge-fixed inverse, never "some solution of ".Matrix.Norms.L2Operator); vector norms in Lemma 5 are Euclidean; is natural (the base is absorbed into ).Reusable beyond this mission: the weighted Laplacian with its pseudoinverse and effective resistances, and Lemma 5, which applies to any sampling scheme for sums of rank-one matrices (leverage-score sampling, column subset selection). Contributions toward a matrix Chernoff or Rudelson-type inequality in Mathlib are welcome.
The effective resistance between two vertices of a weighted graph is the voltage difference that appears between them when the graph is viewed as an electrical network, edge weights being conductances, and one unit of current is injected at one vertex and extracted at the other. Effective resistances drive the spectral sparsification algorithm of Spielman and Srivastava (arXiv:0803.0929): sampling each edge with probability proportional to its weight times its effective resistance yields a sparse graph whose Laplacian approximates the original one. They are also used as a distance on graphs in the analysis of social and small-world networks, where they reflect how many short paths connect two vertices.
Computing every effective resistance exactly requires the pseudoinverse of the Laplacian, which costs far more than the size of the graph. Section 4 of the paper shows that all of them can be approximated in nearly linear time: a random projection compresses the relevant vectors to dimensions, and the projected vectors are obtained from calls to a fast approximate Laplacian solver (Spielman–Teng). This mission formalizes the deterministic statement that makes this procedure correct, Lemma 9: approximate solves, at a stated accuracy, do not destroy the approximation that the random projection provides.
Let be a connected, simple, weighted undirected graph with vertices, edge set and edge weights . Orient every edge arbitrarily, so that it has a head and a tail. The signed incidence matrix has if is the head of , if is its tail, and otherwise. With the diagonal matrix of weights, the Laplacian is , a symmetric positive semidefinite matrix whose kernel is spanned by the all-ones vector when is connected. Its Moore–Penrose pseudoinverse is , where are orthonormal eigenvectors of with nonzero eigenvalues .
For a vertex let be its indicator vector. The effective resistance between and is
and for an edge with endpoints . The -norm of is . Let and be the smallest and largest edge weights.
A resistance sketch is a matrix (columns indexed by ) with
where is the Euclidean norm. In the paper, for a random matrix with , and the Johnson–Lindenstrauss lemma makes it a sketch with high probability. Write and for the -th rows of and of an approximation , as vectors in .
Let . If is a resistance sketch, if every row satisfies
and if
then for every pair
The lemma is stated for arbitrary , and : nothing about the random projection or the solver enters beyond (4) and the sketch property.
Lemma 9 is the correctness half of the paper's Theorem 2: together with a Johnson–Lindenstrauss lemma and the Spielman–Teng solver it yields a data structure, built in time, that returns any effective resistance to within a factor in time. This in turn makes the effective-resistance sampling of the paper's Theorem 1 run in nearly linear time, and the same sketch-and-solve pattern has been reused in later work on Laplacian solvers, graph sparsification and electrical-flow algorithms.
The result is proved in the paper. Formalizing it produces machine-checked statements of three facts that recur throughout spectral graph theory: the trace identity (Foster's theorem in its weighted form), the lower bound on effective resistances by comparison with the complete graph, and the stability of a resistance sketch under relative -norm errors. Neither Mathlib nor this platform states any of them for the linear-algebraic definition of effective resistance used here.
The hypothesis (4) controls the error row by row, in the -norm on , while the conclusion concerns the columns of applied to , in the Euclidean norm on , and it is a relative bound for every pair at once. A relative bound cannot hold unless is bounded below uniformly over all pairs of distinct vertices, which is where the factors , and of (5) come from. Such a lower bound is false for multigraphs, whose parallel edges can make arbitrarily small, and the relation between the -norm of a row and the Euclidean norms of the columns involves every edge of the graph, not only a path between and .
Proposition 10 is classically derived from Rayleigh's monotonicity law. Its standard formal statement on this platform concerns the probabilistic definition of effective resistance through hitting probabilities of a random walk, which is a different definition from ; no theorem relating the two is available.
The graph is a structure WGraph V E over finite types (vertices, Fintype.card V) and (edges), with head, tail : E → V, head e ≠ tail e, weights w : E → ℝ with 0 < w e. Connectivity is that of the underlying simple graph (Mathlib's SimpleGraph.Connected, which includes ); simplicity means that no two edges join the same unordered pair. Matrices are Mathlib matrices indexed by and . is the published Moore–Penrose pseudoinverse HarmonicGames.Decomposition.pinv of on the Euclidean space , converted back to a matrix; for symmetric this is the spectral pseudoinverse of §2.2. is the sum of squares of the coordinates, not Lean's sup norm. is the real number .
Choices committed to, relative to the page:
A trivializing formalization is ruled out: the goal does not assume the intermediate inequality of the proof, nor a stronger condition on than (5); its hypotheses are satisfiable (for example with and ), and its conclusion is not vacuous for .
Infrastructure that a complete development needs, and that is reusable beyond this mission: the identity and as the projection onto for a connected Laplacian; the trace identity; Loewner-order monotonicity of in the edge weights; and the effective resistances of the complete graph. Contributions of any of these as separate lemmas are welcome. The random projection (Johnson–Lindenstrauss) and the solver's running time are outside this mission.
Markov decision processes model sequential decisions under uncertainty, and their optimal policies are computed from transition probabilities that in practice are estimated from data. Optimal policies can be sensitive to estimation error in those probabilities. Robust dynamic programming replaces each transition law by a set of plausible laws and evaluates a policy by its worst-case expected reward over that set. Garud Iyengar's Robust dynamic programming (CORC Tech Report TR-2002-07, 2002, rev. 2004; Mathematics of Operations Research 30(2), 2005) set up this theory for countable state spaces and history-dependent policies. It isolated the Rectangularity assumption under which the robust problem keeps a Bellman equation. In the same period, Nilim and El Ghaoui studied robust control of Markov decision processes with finite state spaces.
Timeline:
A discounted ambiguous Markov decision process has a countable state set , for each state a nonempty set of admissible actions, for each admissible pair a nonempty set of probability measures on (the ambiguity set), a bounded reward and a discount factor . Decisions are made at epochs .
A policy maps each history to a probability measure on . is the set of all such policies. A deterministic Markov policy plays for maps with . A stationary policy uses one such rule at every epoch.
Under Rectangularity, the adversary picks a law separately at every epoch and history, and may pick a different law each time a state–action pair recurs. This is the dynamic model, and the set of path measures it generates is . In the static model the adversary fixes one per pair. The robust value of a policy and the robust value function are
Let be the bounded functions on with . For a set of deterministic Markov rules, the robust Bellman operator is
is the only bounded solution of this equation, and for every some stationary deterministic policy has .
Corollary 2(b) justifies computing the robust value function by solving a state-wise max–min equation. Value iteration, policy iteration and their approximations all rely on that equation. It also shows that a decision maker facing a history-dependent adversary loses at most by committing to a stationary deterministic rule. Corollary 2(a) and Lemma 2 make robust policy evaluation a fixed point problem and a robust optimization problem. Lemma 3 shows that, for stationary policies, the dynamic model costs nothing relative to the static model, in which the true transition law is fixed but unknown.
The results are proved on paper. The page proves Theorem 4 only by citation to Puterman's non-robust arguments. No machine-checked proof of any of them is known. The platform has finite-state analogues posed by the Nilim–El Ghaoui and Satia–Lave missions, which compare only stationary or Markov controllers. This mission poses the countable, history-dependent version, and proving it would establish them in this generality.
The contraction property is a state-by-state -argument. The hard step is to identify the fixed point with the value of the game against all history-dependent randomized policies. The adversary's choices at different epochs interact only through Rectangularity, so splitting the infimum over path measures into a first-step infimum and a continuation infimum must be justified for an infinite horizon, uncountably many adversary strategies and no attainment of the infima. The ambiguity sets need not be convex or closed. The naive route, "take the minimizing law at each state", is unavailable, and every bound must be carried with an slack. Truncating the infinite sum needs the uniform reward bound. Theorem 4 needs a separate argument that randomization and history dependence do not help the decision maker against the dynamic adversary.
States and actions are countable Lean types; and are sets, assumed nonempty, with no convexity or closedness. Laws are PMFs and as a tsum. The rewards satisfy on admissible actions. This is the reading of the page's "", which its bounds require. The discount factor satisfies . Epochs start at , so the first reward is undiscounted.
A policy maps to a PMF supported on . The dynamic adversary maps to a law in . The path law is built by PMF.bind, and the discounted reward is , which converges absolutely. Values are real infima and suprema over nonempty families bounded by , so no junk value arises. is the predicate "bounded", and is a supremum (the page writes max). All uniqueness claims are uniqueness among bounded functions.
is a supremum over all history-dependent randomized policies. Defining it over deterministic Markov or stationary policies would make Theorem 4 trivial and weaken the goal, so it is ruled out. The adversary in is the dynamic one; the static adversary appears only in Lemma 3.
The mission deviates from the page in three places:
Only the first claim of Lemma 1 is posed. Its second claim, that an -greedy rule is -optimal, is false as printed.
A complete development needs a general toolkit that is reusable beyond this mission: path laws of countable controlled processes with history-dependent policies, a uniform -optimal selection argument for real infima over arbitrary sets, and the Banach fixed point theorem on bounded functions (Mathlib's ContractingWith). Proofs of individual milestones are welcome in any order. Theorem 5(a) is the natural entry point.
Many classical search algorithms are random walks: a Markov chain on a finite state space is run until it hits a marked state. Szegedy (2004) attached to every such chain a unitary quantum walk , and Magniez, Nayak, Roland and Santha (SIAM J. Comput. 2011, arXiv:quant-ph/0608026) used it to search quadratically faster than the classical walk for every reversible ergodic chain. The search runs Grover-style rotations, and each rotation needs the reflection about the stationary state . Preparing exactly can cost far more than one step of the walk, so the paper builds an approximate reflection from the walk alone, by phase estimation. Theorem 6 of the paper is the guarantee for that circuit, and this mission formalizes it.
Timeline:
is a finite set of size . A Markov chain is a row-stochastic matrix . It is ergodic if some power of has all entries positive. A stationary distribution satisfies , and . The time-reversed chain is defined by , and is reversible if .
The space is with basis . Put and , and
For a subspace , , where is the orthogonal projector onto . The quantum walk is , and the stationary state is .
The discriminant matrix is . Its singular values lie in . The phase gap is , where is the smallest angle in such that is a singular value of .
The phase-estimation circuit acts on . It is
where is the Walsh–Hadamard matrix and is the -point Fourier transform.
The circuit uses and acts on . It is built in three steps:
For ergodic and reversible on states, and every integer :
The milestones follow the order in which the paper's proof uses them:
Theorem 6 replaces the reflection about with a circuit that only calls the walk. Its cost scales as rather than as the cost of preparing . Combined with , where is the eigenvalue gap, this gives the search cost of Theorem 7, up to logarithmic factors. The same approximate-reflection device recurs in later quantum-walk and amplitude-amplification algorithms.
The results are proved in the paper, which takes Theorem 4 from Szegedy and Theorem 5 from Cleve et al. As far as the platform index shows, none of Theorems 4, 5 or 6 has a machine-checked proof. The mission produces three reusable components: a Lean definition of the Szegedy walk and of the phase-estimation circuit, a formal Jordan-type spectral theorem for products of two reflections, and the analysis of phase estimation on an eigenvector.
Most of the work is linear algebra. The proof of Theorem 6 has a short outline: expand in eigenvectors of , apply Theorem 5 to each, and bound each amplitude by . Three steps carry the weight:
EuclideanSpace ℂ (X × X), with the first coordinate the first register.Fin (2^s), and registers by Fin k → Fin (2^s); the all-zeros state is the zero index.Submodule.reflection.Matrix.IsPrimitive.LinearMap.singularValues.Real.logb 2 and the ceiling is Nat.ceil.Deviations from the page.
Only exact statements are formalized. The cost halves (gate counts, calls to -, "", the qubit count, uniformity) are out of scope.
The circuit is the explicit composition above, built from . It is neither "some circuit with properties 2–3" nor anything defined through the projector onto , either of which would make the goal a tautology.
Contributions welcome: proofs of the milestones, Jordan's lemma for two subspaces as a standalone result, and the bound of §3.3.
In an online linear decision problem a decision maker chooses, on each period , a decision from a set , and only then learns a state vector and pays the cost . The online shortest path problem, the experts problem, online binary search trees and list update are all of this form. Kalai and Vempala showed that a single offline optimisation oracle is enough to compete with the best fixed decision in hindsight: Follow the Perturbed Leader plays the leader of a randomly perturbed history (Kalai & Vempala 2005; the idea goes back to Hannan 1957).
Each period of FPL calls the oracle once and may change the decision. When an oracle call is expensive, or when switching decisions carries a cost (rotating a search tree, re-routing traffic), this is wasteful. The same paper introduces Follow the Lazy Leader: versions FLL and FLL* of FPL and FPL* that correlate the perturbations across periods so that the decision rarely changes, while each single period is distributed exactly as before. Lemma 1.2 of the paper is the statement that this works, and it is the result of this mission.
Vectors are elements of ; , and with .
The four algorithms, period :
For every period :
The first line is the FLL half, the second the FLL* half. The constant is the paper's.
Lemma 1.2 transfers every guarantee proved for FPL and FPL* to FLL and FLL*: Theorem 1.1 of the paper bounds expected costs period by period, so equal per-period expectations give the same additive bound and the same multiplicative bound for the lazy algorithms. In addition, the expected number of oracle calls and decision changes over periods is at most , which is at the usual tuning . The paper uses this for online binary search trees with few rotations.
The result is proved in the paper. As far as is known there is no machine-checked proof of it. This mission produces a Lean statement of all four claims and of the six steps of the proof, against explicit Lean definitions of the grid point, the FLL* step and the law sequence . The uniformity of a random-grid point and the invariance of a Laplace law under a Metropolis-type step are reusable facts beyond online learning.
The FLL half asks for the exact law of the grid point , a piecewise translation of whose pieces depend on . The page settles it in one line ("by symmetry"); in Lean it is an equality of push-forward measures, and the obvious attempt, a single change of variables , fails because the shift is different on different pieces of the cube.
The FLL* half is a statement about measures on given as a mixture of point masses. The page argues with densities, pointwise in ; the formal statement is an equality of measures, with the update written as a Measure.bind against a kernel whose two branches move mass in different directions. The density computation of display (8) does not by itself give this equality.
Fin n → ℝ, is dotProduct, is written out as ∑ i, |x i|. States are indexed from 1; s 0 is unused.prefixSum and is perturbLaw n ε from the published definition OracleRO.ApproxFPL.FPL. The oracle is the predicate IsArgminOracle Dset M, and every statement holds for every such .laplaceLaw n ε carries its normalising constant , so it is a probability measure for .fllGridPoint ε x p is the explicit formula . It is the unique grid point in the half-open cube for , and it is measurable. The half-open and closed cubes differ by a null set, and the closed-cube law is used throughout.fllStarJoint ε v ν of , built with Measure.bind and Measure.dirac. The acceptance probability is . The law fllStarLaw ε s t is the recursion started at , not itself.The formalization rules out the following trivializations:
Classical.choose;Welcome contributions:
Measure.bind lemmas for finite mixtures of Dirac kernels;Grover's algorithm finds a marked element among with queries by alternating two reflections: one about the initial state and one that flips the sign of marked states. In quantum-walk search, the initial state encodes the stationary distribution of a Markov chain, and the reflection about is too expensive to implement exactly. Magniez, Nayak, Roland and Santha (arXiv:quant-ph/0608026, SIAM J. Comput. 2011) obtain the reflection approximately, by phase estimation on the quantum walk, and need a search procedure that tolerates the approximation error without paying extra cost to reduce it. Their Section 4 supplies one: a variant of the recursive amplitude amplification (RAA) of Høyer, Mosca and de Wolf (ICALP 2003) in which the reflection about is replaced, at recursion level , by an approximate circuit of precision . The two lemmas of that section, stated "in full generality for potential further applications" (p. 11), are the exact engine of the paper's headline Theorem 3 (search with cost ).
Timeline: Grover (1996) gives quadratic speedup for unstructured search; Brassard, Høyer, Mosca and Tapp (2002) generalize it to amplitude amplification; Høyer, Mosca and de Wolf (2003) introduce RAA to tolerate a bounded-error marking reflection; Szegedy (2004) defines quantum walks for arbitrary reversible chains with detection guarantees; Magniez, Nayak, Roland and Santha (STOC 2007, SIAM 2011) adapt RAA to an approximate initial-state reflection and obtain search, not only detection, for every reversible ergodic chain.
Let be a finite set and a set of marked elements. The state space is . The initial state is any unit vector (Lemmas 1 and 2 never use its quantum-walk form), and the marked weight is , where projects onto the basis states with .
For each level an extra register (a finite-dimensional space with a basis state ) is given together with a unitary on , playing the role of :
On the marked subspace consists of states whose first register is marked, and .
Approximate RAA is the unitary with and
where multiplies by every basis state in which some register , , is not , and otherwise applies to . Write and .
Tolerant RAA first samples (succeeding with probability ); otherwise, for , it applies to the state left over from the previous failed measurement, with , and measures ; a failure collapses the state to .
Let , let satisfy whenever , and let be the smallest non-negative integer with . The probability that Tolerant RAA ends with a marked element satisfies
With the smallest non-negative integer such that , for every ,
In the order of the proofs: Fact 1 (the error operator kills and has norm on states with clean registers ); the one-level bound ; the two trigonometric inequalities on ; the surrogate bound ; Lemma 1; the three terms of the drift recursion (5); and the accumulated drift .
Lemma 2 turns any family of approximate reflections whose error decays like into a search procedure that succeeds with constant probability, needs only a lower bound on , and costs calls. Combined with the phase-estimation reflection of the paper's Theorem 6 it yields Theorem 3, the general quantum-walk search theorem that has become the standard tool for walk-based algorithms (element distinctness, triangle finding, group commutativity). Nothing in the lemma refers to Markov chains, so it applies to any setting with an approximate reflection about the initial state.
The results are proved in the paper. None of them is machine-checked: the platform holds a formal Grover search with one marked basis state and exact reflections, but no amplitude amplification with approximate or recursive reflections. A formal proof would also settle the steps the paper passes over quickly, notably that the trigonometric inequalities, claimed for angles in , are applied to the actual angles , which may exceed by at the last level.
The ideal analysis (every reflection exact, angle tripled at each level) is a two-dimensional rotation argument. With approximate reflections the state leaves the plane spanned by and , and each level both triples the error already present and injects a new one; the errors stay bounded only because converges and the injection at level is weighted by . Fact 1 is not a restatement of the hypothesis on : it holds only because step 4 flips the phase of states whose earlier registers are dirty, and because never touches . In Lemma 2 the attempts reuse the leftover state, not a fresh , so the state at the decisive attempt has drifted; bounding the drift needs the normalised unmarked parts to move little from level to level, which again depends on the error bounds of Lemma 1.
EuclideanSpace ℂ (X × X × ((j : Fin T) → κ (j+1))); operators are complex matrices. Registers are 0-based in Lean (index is ).Real.arcsin; the interval is closed.Contributions welcome: proofs of the trigonometric milestones and of (pure real analysis), Fact 1 (finite-dimensional linear algebra with a block structure on registers), and the vector inequality that the drift bounds share. The register and controlled-unitary infrastructure is reusable for other recursive quantum algorithms.