Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
This mission develops Chapter 4 of An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation by Daniel Gottesman. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is the key claim in the proof that Steane error correction satisfies property EC A (Gottesman intro p.28).
Let be binary linear codes with , and let be their CSS code, spanned by the states for . Steane error correction is applied to a data block in an arbitrary state . The state may be entangled with a reference system , and its incoming error is unrestricted. The procedure runs as follows:
The faults are arbitrary operators. They may act within on the prepared ancillas, and within the pairs (data qubit , ancilla qubit ) for , resp. , right after the two CNOTs. During the Hadamard and measurement of the phase ancilla they act within , and during the measurement of the bit-flip ancilla within . Put . Then for every pair of outcomes the corrected (unnormalized) data–reference state satisfies
and moreover .
In words: after Steane error correction, the data is a codeword (possibly a different logical state) with errors only on the qubits where faults occurred during error correction. This gives EC A when .
Formalization Note The circuit is the chunk-local definition steaneECOutput. It returns the post-measurement branch for the given outcomes, i.e. the amplitude of the ancillas on . In that branch the map is linear, so the arbitrary fault operators per Kraus branch and the arbitrary incoming vector cover the source's 'no restrictions as to the types of errors'. The hypothesis of EC A is omitted because the claim's proof never uses it.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 10 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is the complexity theorem for the Harrow–Hassidim–Lloyd (HHL) algorithm for the quantum linear systems problem (QLSP), in the form of Childs, Kothari and Somma (2017), Theorem 2.
The problem. Let be an Hermitian, invertible matrix with operator norm , condition number (known to the algorithm), and at most nonzero entries in every row and every column. Let be a vector in and , and write , , with indices held in qubits. The matrix is accessed through a black box consisting of the two unitary maps
where is the row index of the -th nonzero entry of column and the entry is written exactly as a -bit string in a fixed encoding. The vector is accessed through a unitary black box with . A use of a black box (possibly controlled, possibly inverted) is one query; the gate complexity is the number of other 2-qubit gates. The goal is to output, with probability at least and with a flag qubit indicating success, a state that is -close in Euclidean norm to .
The theorem. There are absolute constants and , and for every entry encoding constants , , such that for all , all , and there is a single quantum circuit, depending only on and the encoding, which solves every QLSP instance with these parameters, and whose number of queries to and number of uses of satisfy
and which is gate-efficient: its number of 2-qubit gates satisfies
Success means: started in on a flag qubit, output qubits and some number of work qubits, the final state has flag with probability , and the normalized flag- branch is within Euclidean distance of for some unit work-register state .
This is the benchmark against which the later precision improvements (Theorems 3–5 of Childs–Kothari–Somma) and de Wolf's §10.3 singular-value-transformation algorithm are measured.
Formalization Note A -sparse matrix with automatically has and ; these ranges are stated so that the logarithms are positive. The polylogarithmic factors with are written , which is equivalent. The gate-efficiency constants may depend on the fixed exact encoding of matrix entries, because the source treats the entry representation as exact and does not account for its arithmetic; the query constants do not. The source's assumption that runs in time concerns the cost of , which is counted only through . The theorem is vacuous for (the column map cannot exist), where the bound for is stronger anyway. The output may differ from by a global phase, absorbed into the work-register state.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 20 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is the Gottesman–Knill theorem.
Let be the -qubit Pauli group. A measurement-controlled Clifford circuit family consists, for each number of qubits , of a sequence of at most operations, a polynomial, each of which is a Pauli gate, a Hadamard gate , the phase gate , a CNOT gate, or the projective measurement of a Pauli with projectors . The next operation is computed from , a string of uniformly random bits ( a polynomial) and the outcomes of the earlier measurements by a classical polynomial-time algorithm. Running on the computational basis state , , produces a random final pure state ; write for the distribution of its density matrix .
A stabilizer description (tableau) is a list with phases that pairwise commute, are independent (none is a phase times a product of the others) and do not generate ; it describes the state with density matrix .
Theorem. For every measurement-controlled Clifford circuit family there is a randomized classical polynomial-time algorithm such that for every and every :
Thus Clifford circuits with intermediate Pauli measurements and classical (randomized) control, started on a basis state, can be sampled exactly by a classical computer; the quantum advantage requires non-Clifford resources such as the gate.
Formalization Note The source says the simulator is "given C"; following its own remark on p.187 that one strictly has to speak of families , the simulator is fixed for the family (chosen before and ) and receives encoded as a bit string. Polynomial time is the Turing-machine notion PolyTimeComputable of this repository, applied to the input followed by a uniformly random string of polynomial length. Distributions over states are compared via density matrices, so the global phase is ignored, as in the source's footnote 3 on p.185.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 7 of Stabilizer Codes and Quantum Error Correction by Daniel Gottesman. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Fix an erasure probability . The qubit erasure channel acts independently on each qubit sent: with probability the qubit passes unchanged together with a classical flag , and with probability it is replaced by the maximally mixed state together with the flag , so that the receiver knows which qubits were erased. On qubits the channel is .
A rate is achievable (for quantum codes, equivalently one-way entanglement purification) if for every and there is such that for every there are a number of logical qubits, an encoding quantum channel from qubits to qubits and a decoding quantum channel from the channel output (qubits and erasure flags) to qubits with
where is the entanglement fidelity with respect to the maximally entangled state of two -qubit registers. The theorem states that the quantum capacity of the erasure channel is , in the strong form that the set of achievable rates is exactly
In particular every rate below is achievable (random stabilizer codes), no rate above is (a no-cloning argument), and for the capacity is zero.
Formalization Note The supremum of achievable rates is not written as a real sSup (which would be junk on an empty or unbounded set); instead the achievable set itself is characterized. Because the definition of achievability already has the slack , the achievable set is closed, so the capacity is itself an achievable rate. The author's errata note that the thesis's proof of the upper bound assumes there is no superadditivity when a noiseless channel is added to a zero-rate channel; the theorem itself is the established value (Bennett–DiVincenzo–Smolin).
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 30 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is the quantitative quantum adiabatic theorem.
There are absolute constants (the constants of the first- and second-order perturbation bounds and ) with the following property. Let be a finite-dimensional Hilbert space with , and let , , be a twice continuously differentiable family of Hermitian operators on , with derivatives and (one-sided at the endpoints). Suppose that for every the ground state of is nondegenerate, and let be the gap between the smallest eigenvalue of and the nearest distinct eigenvalue. Norms of operators are spectral norms. Let and let the total evolution time satisfy
If solves the Schrödinger equation on and is a unit ground state of , then there is a unit ground state of with
The theorem quantifies how slowly a Hamiltonian must be varied for a system started in its ground state to end close to the final ground state, with the required time governed by the spectral gap; it underlies adiabatic optimization and adiabatic quantum computation.
Formalization Note The instantaneous ground state is fixed only up to a global phase, so the conclusion asserts the existence of some unit ground state of within . The constants are quantified before the dimension and the Hamiltonian. The derivatives are given as functions with derivative-within- hypotheses and continuous; the gap is the difference of the two smallest eigenvalues counted with multiplicity, which equals the source's when the ground state is nondegenerate.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
A Markov decision process (MDP) is optimized for a transition kernel that, in practice, is estimated from data, and the optimal policy for the estimated kernel can perform poorly under small perturbations of it. The robust MDP approach replaces the single kernel by an uncertainty set of kernels and asks for the policy with the best worst-case expected reward. It goes back to Satia and Lave (1973).
Whether a robust MDP is tractable depends on the shape of the uncertainty set.
Rectangular sets let the adversary choose the transitions out of different states independently, which is conservative when all transitions depend on a few common factors, such as a patient's physiology across health states. Factor uncertainty couples the states, and it is the first coupled model in which an optimal robust policy can still be computed.
There are finite sets of states and actions , with and . The rewards satisfy , is an initial distribution on , and is the discount factor. Fix factors indexed by and coefficients with . A factor matrix has probability vectors on as columns, and it induces the kernel
The uncertainty set is a nonempty convex compact set of factor matrices. It is r-rectangular if , so that each factor is chosen independently of the others.
A stationary policy gives a distribution on at each state. It is deterministic if each is a point mass. Write and . The decision maker's value function and the expected discounted reward are
The policy evaluation problem computes . The policy improvement problem computes . Let
Algorithm VI-PI is the iteration , .
Assume is r-rectangular. Then has a unique fixed point , and
Write . If , then , and the deterministic policy that VI-PI computes at that iteration is -optimal. The test is passed as soon as .
The milestones follow the paper's route to the goal.
Theorem 3.2, the policy-evaluation analogue of the goal (Algorithm VI-PE), is included as a further item.
The theorem shows that factor uncertainty, in which transitions out of different states are coupled, is as tractable as (s,a)-rectangular uncertainty, provided the factors are independent. An optimal robust policy exists among deterministic stationary policies, the robust and nominal problems share a saddle point, and value iteration on a -contraction computes the robust value. The structure is also what the companion mission builds on: the robust maximum principle and robust Blackwell optimality are derived from (5.1) and Theorem 4.2.
The results are proved in the paper. None of them is formalized: no factor-matrix robust MDP exists in Lean. The platform's robust-MDP items for (s,a)-rectangular sets (Nilim–El Ghaoui, Iyengar) and s-rectangular sets (Wiesemann et al.) are other uncertainty models and do not specialize to this one. A formal proof would also check a printed statement, since one clause of Theorem 4.2 needs correcting (see below).
The obvious argument writes a robust Bellman equation state by state and appeals to the contraction principle. Here that argument fails. Under factor uncertainty the adversary cannot choose the transitions out of each state separately, because one factor enters every row with . Minimizing state by state therefore yields kernels that need not come from a single feasible . The decision maker's equation for does not close on its own.
The step that requires care links two dynamic programs, the decision maker's over and the adversary's over , and shows that factor-wise minimization is feasible. That is where r-rectangularity enters. The paper's Appendix A gives an instance in which the factor-wise minimizers are infeasible once a constraint couples the factors.
Fin r (0-based).Fin r → S → ℝ whose values are probability vectors. It is nonempty, convex and compact. Nonemptiness is implicit in the paper and explicit here. is the projection of , and r-rectangularity is a hypothesis (IsRRect). Proposition 3.1, Lemmas 4.3, A.2 and A.3, and both contraction statements are stated without it. Lemma 3.3 is stated with it, since it is false without it.IsLeast/IsGreatest, and Lemma A.2 states the invertibility of , because Lean's matrix inverse is on singular matrices.Reusable infrastructure includes the discounted value of a stationary policy for a stochastic matrix, monotone sup-norm contractions with the standard stopping rule, and minimization of linear forms over compact sets. Contributions to any of these are welcome.
Many engineering and operations problems must guarantee that a system operates safely with high probability, when the uncertain parameters are only partially known. A chance constraint asks that the safety condition hold with probability at least for a tolerance . When the distribution of is itself uncertain, the distributionally robust version asks this for every distribution in an ambiguity set built from what is known: moments, supports, confidence regions. Two problems then arise: computing the worst-case probability (uncertainty quantification), and optimizing a design under the constraint (chance constrained programming).
Hanasusanto, Roitch, Kuhn and Wiesemann (Math. Program. 151, 2015) chart which combinations of ambiguity sets and constraint structures admit exact finite reformulations and which are strongly NP-hard. This mission takes the positive core of that chart: for Markov ambiguity sets (first-order moment information plus a conic support), the worst-case probability is the value of a finite conic program, and an individual chance constraint is equivalent to a finite system of linear conic inequalities.
Timeline. Chebyshev-type bounds for worst-case probabilities under moment information go back to the generalized Chebyshev inequalities of Vandenberghe, Boyd and Comanor (2007), and to the duality theory of moment problems summarized by Shapiro (2001). Wiesemann, Kuhn and Sim (2014) introduced the nested conic ambiguity sets used here to evaluate worst-case expectations. Hanasusanto et al. (2015) applied them to worst-case probabilities of polytopes and to chance constraints, proving Theorem 3 (moment problem reformulation) and Theorem 7 (individual chance constraints over Markov sets), together with strong NP-hardness results, such as Theorem 8, showing that the restrictions cannot be dropped.
Let be the uncertain parameters and an auxiliary random vector. Fix , , , and a confidence set
where , , and is a proper cone (closed, convex, pointed, with nonempty interior); means , and is the dual cone. The Markov ambiguity set is
the case , of the paper's nested set (4).
Two regularity notions enter. is essentially strictly feasible if it contains a point satisfying all non-polyhedral constraints of its description strictly. The Slater condition (S) for requires to lie in the interior of .
For the safety system with rows , , let be the rows that can be violated on . Problem (17) at maximizes over , , and, for , , , subject to , , and, for , , , .
For an individual constraint () write . System (26) asks for , , , with
Under essential strict feasibility of , (S), and ,
Theorem 7 turns an individual distributionally robust chance constraint over a Markov ambiguity set into finitely many linear conic constraints whose size is polynomial in the data. Since and are affine in the design , the chance constrained program becomes a single conic program, solvable with standard software. The paper notes (p. 18) that, apart from the Wasserstein set, all ambiguity sets of its Section 2.3 are Markov sets or intersections of Markov sets with structural ambiguity sets, and Theorem 8 shows that adding a second confidence set already makes the problem strongly NP-hard, so the theorem marks a precise tractability boundary. Theorem 3 underlies the paper's later results and its §5 heuristic for intractable cases.
All five statements are proved in the literature: the paper defers its proofs to an accompanying technical report. None is machine-checked. A formal proof would supply a verified duality theory for moment problems with conic supports, a reusable bridge between semi-infinite constraints and conic certificates, and a verified basis for the paper's hardness results to be stated against.
The sufficiency halves are weak-duality arguments. The converse directions are not: the worst-case probability is an infimum over an infinite-dimensional set of measures, and the conclusion of Theorem 7 requires the dual certificate to be attained, not just approached. Two separate duality steps must both close without a gap and with attainment: the moment problem against its semi-infinite dual, which is where (S) enters, and each semi-infinite constraint against its conic dual over , which is where essential strict feasibility enters. The event is open, so the semi-infinite constraint must also be passed to its closure. Mathlib has neither a duality theorem for moment problems nor conic strong duality with attainment.
The mission covers Markov ambiguity sets only (, ). The general nested case of Theorem 3 is not stated, because the paper does not make (S) explicit for . Symmetry and unimodality information, joint chance constraints and the hardness results are out of scope. The paper's proofs are in a technical report that the mission does not use.
Conventions committed to in Lean:
Fin n → ℝ, the single confidence set is index 0 : Fin 1 of the published DRConvexOpt.Reform.AmbData, and its field c 0 is .μ.real. The local paperAmbiguitySet reuses the published data and confidence-set definitions and requires integrability only of . This makes the expectation condition void when , as the paper states.sInf ∅ = 0.Replacing essential strict feasibility by full strict feasibility, adding to (26), or imposing the -constraints for would each change the theorem and is ruled out. The hypotheses are jointly satisfiable: , , , satisfies all of them, with a nonempty ambiguity set.
A complete development needs conic duality with attainment under partial Slater conditions, Lagrangian duality for moment problems, and the reduction of a measure-valued infimum to finitely supported measures. All three are reusable well beyond this mission, and contributions to any of them are welcome.
The main conjecture of Iwasawa theory is an identity between two objects attached to an odd prime and the tower of cyclotomic fields : an algebraic object built from the -parts of their ideal class groups, and an analytic object, the Kubota–Leopoldt -adic -function, which interpolates special values of Dirichlet -functions (generalized Bernoulli numbers). It was formulated by Iwasawa, partly by analogy with Weil's description of the zeta function of a curve over a finite field through the action of Frobenius on its Jacobian: the group plays the role of Frobenius, the inverse limit of class groups plays the role of the Jacobian, and the -adic -function plays the role of the zeta function.
Timeline:
Fix an algebraic closure and a prime . For let (Lean: F p n), and let (Lean: A p n) be the -primary part of the ideal class group of ; by class field theory , with the -Hilbert class field of . The Iwasawa module is
the inverse limit along the norm maps (Lean: Hinf p). It is a -module with a continuous action of through , . Put (Lean: V p).
The cyclotomic character sends to the unique with for every -power root of unity . The subgroup consists of the elements whose character is a -st root of unity, and on the Teichmüller character is . Let be the -eigenspace of on (Lean: eigenspace p i). Let , let be a topological generator, and let be its cyclotomic character: . Let , the characteristic polynomial of on written in the Iwasawa variable (Lean: charPoly p i γ).
On the analytic side, is the generalized Bernoulli number of a character modulo . The Kubota–Leopoldt -adic -function satisfies for , and is the power series with (Lean: IsIwasawaPowerSeries p u j G).
For every odd integer ,
The main conjecture describes the Galois-module structure of the class groups in the whole cyclotomic tower by -adic -functions. The Herbrand–Ribet theorem and the Gras conjecture follow quickly from it, and its generalizations (totally real fields, CM fields, elliptic curves and modular forms, the latter by Skinner–Urban) feed into results on the Birch–Swinnerton-Dyer conjecture. The theorem has been proved (Mazur–Wiles 1984); no machine-checked proof is known. A formal proof requires Iwasawa's structure theory of -modules, the construction of -adic -functions, and either the Eisenstein-ideal argument of Mazur–Wiles or Rubin's Euler-system argument. Each of these is reusable well beyond this mission.
One divisibility can be reduced, via the analytic class number formula, to the other. The hard direction is to show that the characteristic ideal of the class-group side is divisible by the -adic -function. Stickelberger's theorem gives only annihilation, not the characteristic ideal. Divisibility needs a construction of many unramified abelian -extensions: Ribet's method with Galois representations attached to cusp forms congruent to Eisenstein series, or Kolyvagin–Rubin Euler systems. Neither is in Mathlib today.
AlgebraicClosure ℚ generated by the roots of . The groups are the -primary components of ClassGroup (𝓞 (F p n)); the norm maps come from Ideal.relNorm, and the Galois action comes from mapping ideals. The Hilbert class field does not appear: the source's own identification is used.The Selmer group is the main computable invariant attached to the rational points of an elliptic curve (more generally, of an abelian variety) over a number field. J. W. S. Cassels named it in honour of E. S. Selmer, whose numerical work on the curves exposed the limits of descent methods (Selmer 1951). For an elliptic curve over a number field and an integer , the -Selmer group is a finite group, computable in principle, which contains and whose remaining part is the -torsion of the Tate–Shafarevich group . Finiteness of the Selmer group is the cohomological core of the weak Mordell–Weil theorem, and hence of the Mordell–Weil theorem that is finitely generated.
Timeline.
Let be a number field with algebraic closure and absolute Galois group , a profinite group with its Krull topology. Let be an elliptic curve over , given by a Weierstrass equation, and let . For a field write for the group of -points and for the -torsion of ; the group acts on both.
For a topological group acting on an abelian group (regarded as discrete), the continuous first cohomology is the group of locally constant maps with , modulo the maps .
For each place of (finite or infinite), let be the completion, , and fix a -embedding ; it induces the restriction and . The local Kummer map is
The -Selmer group is
and the Tate–Shafarevich group is the set of classes in whose restriction to every is trivial.
The result. Finiteness of gives, through the exact sequence, finiteness of (weak Mordell–Weil) and of . Combined with the theory of heights it yields the Mordell–Weil theorem. The Selmer group is also the object that descent algorithms compute, and the starting point of Iwasawa-theoretic and Bloch–Kato generalisations.
Formalizing it. The finiteness theorem is classical (see e.g. Silverman, Ch. X). A complete development produces continuous Galois cohomology of elliptic curves over number fields, the Kummer sequence, local conditions at all places, and a formal weak Mordell–Weil theorem for arbitrary number fields and arbitrary .
The group itself is infinite, so finiteness can only come from the local conditions, and conditions at all places must be used. The essential input is global arithmetic: the finiteness of the class group and the finite generation of the unit group of a ring of -integers of a finite extension of . The local analysis (behaviour of the Kummer image at places of good reduction not dividing ) and the profinite cohomology must both be built for elliptic curves before that input can be applied.
WeierstrassCurve K with [E.IsElliptic]; is a NumberField. The source treats an isogeny of abelian varieties; this mission specialises to elliptic curves and to the isogeny , .Field.absoluteGaloisGroup L with its Krull topology. is defined from scratch as locally constant 1-cocycles modulo coboundaries (discrete coefficients).v.adicCompletion K; infinite places are InfinitePlace K with completion w.Completion. Restriction uses a fixed embedding chosen by IsAlgClosed.lift.The nontrivial zeros of the Riemann zeta function control the distribution of the prime numbers: the explicit formula expresses the error in the prime number theorem as a sum over these zeros. Almost every quantitative argument about primes therefore needs to know how many zeros there are up to a given height. The Riemann–von Mangoldt formula answers this question, and it is used throughout analytic number theory: in explicit prime-counting estimates, in zero-density arguments, in numerical verifications of the Riemann hypothesis, and in the study of the spacing of zeros.
Timeline.
The Riemann zeta function , defined for , extends to a meromorphic function on with a single pole at . Its zeros with positive imaginary part all lie in the critical strip . For real , the zero-counting function is
where each zero is counted with its multiplicity. The main term is
For a positive integer and a Dirichlet character modulo , is the analytic continuation of , and counts, with multiplicity, its zeros with and . The Lindelöf hypothesis asserts for every , and the Riemann hypothesis asserts that every nontrivial zero has real part .
This asserts only the shape of the asymptotics, with no numerical constants, so it remains valid however the explicit constants are later improved.
For every primitive character modulo and , uniformly in and :
The result itself. The formula shows that the zeros up to height number about , and that their mean spacing at height is . It is the normalisation behind pair-correlation statistics, the input that turns zero-free regions into error terms for the prime number theorem, and the bound that makes sums over zeros in the explicit formula converge. Explicit forms such as Backlund's and Hasanalizade–Shen–Wong's are what numerical work uses: they convert a verified count of zeros up to a height into rigorous statements about primes.
Formalizing it. All the targets are classical, proved theorems; none of them is open. What remains is a machine-checked development: the zero-counting function for Mathlib's riemannZeta, the asymptotic formula, its explicit and conditional forms, and the Dirichlet -function analogue. The platform already contains a related dyadic-window statement for that is conditional on Stirling-type hypotheses. This mission targets the unconditional cumulative count in its standard form.
The obvious approach counts zeros with the argument principle around the rectangle with vertices , , , , using the completed function . The contributions of the Gamma factor and of the right-hand edge are routine. The step that does not go through directly is the top edge: one must show that the change in along is . A naive bound on gives no control of the argument. The classical arguments bound the number of sign changes of on the segment (Backlund's trick via Jensen's formula), or use the Hadamard product with a local zero count. Both need growth estimates for in the strip, Stirling's formula for complex , and a careful treatment of that is the ordinate of a zero. For the explicit bounds, every one of these steps must be carried out with numerical constants. The conditional refinements need the Selberg-type analysis of .
riemannZeta, is DirichletCharacter.LFunction, primitivity is DirichletCharacter.IsPrimitive, and the Riemann hypothesis is Mathlib's RiemannHypothesis.zetaZeroCount) and (dirichletZeroCount) are finite sums of multiplicities (analyticOrderNatAt) over the zeros in the open critical strip, with imaginary part in and respectively. Zeros on the line are counted.finsum over an infinite set would be , so a solver must prove finiteness.Asymptotics.IsBigO / IsLittleO along Filter.atTop. The Lindelöf hypothesis is the one-sided form as , which is equivalent to the two-sided form by conjugate symmetry.Every closed oriented 3-manifold bounds a compact oriented 4-manifold, but asking for a bounding 4-manifold with the homology of a point turns this into one of the long-standing questions of 3/4-manifold topology. The question, recorded on the Open Problem Garden as an outstanding problem of ancient/folklore origin, is whether there is a complete and computable set of invariants that determines which (rational) homology 3-spheres bound (rational) homology 4-balls (Open Problem Garden).
The question organizes the homology cobordism group (integral homology spheres modulo homology cobordism): an integral homology sphere represents zero in exactly when it bounds a smooth integral homology ball. It is also tied to the slice-ribbon problem, listed on the Open Problem Garden as a related problem.
Timeline (as recorded in the source's bibliography).
A closed topological 3-manifold is a compact Hausdorff space locally homeomorphic to . Write and for singular homology. is an integral homology 3-sphere if for all , and a rational homology 3-sphere if the same holds with coefficients.
A smooth integral homology 4-ball is a compact smooth 4-manifold with boundary such that for all ; a rational homology 4-ball is defined with coefficients. bounds if the manifold boundary is homeomorphic to .
The Brieskorn manifold is an integral homology sphere when are pairwise coprime; is the Poincaré homology sphere . The lens space is the quotient of by the -action generated by , .
To speak of algorithms, a 3-manifold is presented by a finite simplicial complex , a list of simplices each given as a list of vertex labels in , with geometric realization . Every closed 3-manifold is triangulable (Moise).
A complete and computable set of invariants is, in particular, a decision procedure; conversely a decision procedure is itself a complete computable invariant. The goal is stated for integral homology spheres and integral homology balls (the title question).
A decision procedure would settle membership in the zero class of for every presented homology sphere. Without one, each new example requires an ad hoc construction (to show bounding) or an obstruction (to rule it out). The known obstructions — the Rokhlin invariant, Siebenmann's -invariant, the Ozsváth–Szabó -invariant and others — are spin or spin cobordism invariants and are not known to be complete.
None of the milestone results is formalized in Lean. Formalizing even the milestones requires substantial infrastructure (smooth 4-manifolds with boundary, intersection forms, Rokhlin's theorem, explicit handle constructions), which is reusable well beyond this mission.
The answer to the goal is unknown; a disproof (undecidability) would equally resolve the mission. On the obstruction side, every known invariant is a homology cobordism invariant that is computable for special families but not known to detect bounding in general. On the construction side, homology balls are produced by explicit handle decompositions with no general recipe. The topological category is no substitute: by Freedman's work every integral homology 3-sphere bounds a contractible topological 4-manifold, so the problem lives entirely in the smooth category.
A knot is a smooth simple closed curve in the -sphere . Since is the boundary of the -ball , one can ask whether bounds a smoothly embedded disc in ; if so, is called slice. Slice knots are the identity element of the smooth knot concordance group, so deciding which knots are slice is a central question of -dimensional topology. A more restrictive and more combinatorial notion is that of a ribbon knot: a knot bounding an immersed disc in whose only self-intersections are ribbon singularities (arcs of double points whose two preimages are an interior arc and an arc running across the disc from boundary to boundary). Every ribbon knot is slice: pushing the interior of a ribbon disc into removes the double points. In 1962 R. H. Fox asked for the converse ([F]). The Open Problem Garden lists this slice–ribbon problem as Outstanding (source): given a knot in which is slice, is it a ribbon knot?
Write for Euclidean -space (R4), , , and for the closed unit disc in the parameter plane (R2).
IsKnot γ). A map which is , -periodic, takes values in , is injective on , and has nowhere-vanishing velocity. The knot is the image .IsSliceDisk γ F). A map that is injective on with injective differential at every point of , maps the open disc into the open ball, maps the unit circle onto , and is transverse to along the boundary: for . A knot is slice (IsSlice γ) if it has a slice disc.IsRibbonImmersedDisk γ f, Fox's definition). A map that maps into with injective differential on , maps the unit circle injectively onto , has no triple points, has transverse double points, and whose double-point set in is a disjoint union of arcs with , each contained in the open disc and each running from the boundary circle through the open disc back to the boundary circle. A knot is ribbon (IsRibbon γ) if it bounds a ribbon disc.IsRibbonSliceDisk γ F). A slice disc on which the squared radial function is Morse in the open disc with no local maxima.IsMinimalOnDisk F). With , , , the vector is tangent to the surface at every interior point, i.e. the mean curvature vector of vanishes on the open disc.A further (non-milestone) sanity item asserts that the round unknot is a ribbon knot, which shows that the definitions are not vacuous.
A supporting (non-milestone) item isolates the maximum-principle step behind [H]: on a minimal disc, the radial function has no local maximum in the open disc.
A positive answer would make sliceness, a -dimensional property defined by the existence of an embedded disc in , equivalent to a -dimensional property that can be certified by a finite diagrammatic object (a ribbon presentation). A counterexample would exhibit a slice knot whose slice discs all need local maxima of the radial function; several proposed candidates (Gompf–Scharlemann–Thompson) are tied to the smooth -dimensional Poincaré conjecture and to Property 2R. The problem is closely related to the question of which homology -spheres bound homology -balls.
On the formal side no part of this theory is in Mathlib: there are no knots, no slice or ribbon discs, no Morse functions on surfaces and no minimal surfaces. The milestones (Fox's easy direction, the D/D equivalence, Hass's theorem) are classical theorems that have not been machine-checked; formalizing them builds the infrastructure any later attack needs.
Turning a slice disc into a ribbon disc requires removing the local maxima of the radial function on the disc. Cancelling a maximum against a saddle is possible only when the handles are in suitable position, and there is no known procedure that achieves this in general; the known positive results rely on classifying the rational homology balls bounded by branched double covers, using Donaldson's diagonalization theorem, which applies only to special families of knots.
Everything is stated in Euclidean coordinates: knots are periodic parametrisations , discs are maps whose restriction to is the disc in question. Smoothness is ; slice discs are required to be smooth up to the boundary and transverse to there (the standard notion of a properly embedded disc). The knot enters only through its image, so orientation and parametrization play no role. The problem is the smooth one; topologically locally flat slice discs are not allowed. Definitions under which the conjecture holds trivially (for example, a ribbon condition implied by the slice condition by definition) are excluded: the goal uses Fox's -dimensional ribbon discs, and the -dimensional characterisation is a separate milestone.
Contributions welcome: smooth embedded discs and their collars, Morse theory for functions on , the push-in construction, and minimal-surface tools (the maximum principle for on minimal surfaces).
The generalized Poincaré conjecture asks whether a closed -manifold with the homotopy type of the sphere must be the sphere. In the topological category (conclusion: homeomorphic) it is now known in every dimension: classically, by Smale (and Stallings, Newman), by Freedman (1982), and by Perelman (2003). In the smooth category (conclusion: diffeomorphic) it fails in general: Milnor (1956) found exotic smooth structures on , and Kervaire–Milnor showed that exotic spheres exist in many dimensions. The single case that remains completely open is the smooth one in dimension ; the Open Problem Garden rates it Outstanding.
All manifolds are Hausdorff, compact, without boundary and smooth (). The model sphere is with its standard smooth structure. Two spaces have the same homotopy type if there is a homotopy equivalence between them.
This is the conjecture exactly as stated in the source.
By Freedman's theorem a homotopy 4-sphere is already homeomorphic to , so the conjecture is equivalent to the statement that has no exotic smooth structure. It would complete the generalized Poincaré conjectures in the smooth category in the one dimension where the answer is unknown. A disproof would give the first exotic smooth structure on a closed simply connected 4-manifold with small homology.
The h-cobordism technology that settles dimensions (the Whitney trick) fails in dimension 4. Freedman's topological methods give a homeomorphism but no smoothing, and gauge-theoretic invariants (Donaldson, Seiberg–Witten) give no information on homotopy 4-spheres. Many candidate counterexamples (Gluck twists, Cappell–Shaneson spheres) have since been shown to be standard.
Manifolds use Mathlib's ChartedSpace (EuclideanSpace ℝ (Fin n)) M together with IsManifold (𝓡 n) ∞ M. The model with corners 𝓡 n has no boundary, and ∞ means (not analytic). The sphere is Metric.sphere (0 : EuclideanSpace ℝ (Fin (n+1))) 1 with Mathlib's standard smooth structure. A homotopy equivalence is ContinuousMap.HomotopyEquiv, and diffeomorphisms are Diffeomorph (≃ₘ^∞⟮𝓡 n, 𝓡 n⟯). Closedness is CompactSpace plus T2Space; second countability follows from compactness. The milestones are the known results the source cites: low dimensions, Perelman, Smale, Milnor's exotic spheres, Freedman, and the continuum of exotic 's. They also include the equivalent reformulation "there is no exotic ". Formalizing any of them requires substantial new manifold-topology infrastructure in Mathlib, and that work is welcome.
The Schoenflies problem asks whether a codimension-one sphere sitting smoothly inside a sphere can be knotted. In every dimension except one the answer is known to be "no"; the remaining case, a smooth -sphere in , is listed as an outstanding problem in the Open Problem Garden (source). It is one of the central open questions of smooth -manifold topology, closely tied to the existence of exotic smooth structures on the -ball and to the smooth -dimensional Poincaré conjecture.
Timeline.
For let be the unit sphere with its standard smooth structure, and let be the closed unit ball. In the Lean development is Sph n.
A smooth embedding is a map that is injective and whose differential is injective at every point (an injective immersion; since is compact this is an embedding). Its image is a smooth -dimensional submanifold of diffeomorphic to (Lean predicate IsSmoothEmbeddingSph n f).
By the Jordan–Brouwer separation theorem, has exactly two connected components, and is the frontier of each. Their closures are compact connected -manifolds with common boundary .
A subset is a smoothly embedded closed ball if it is diffeomorphic to (with the smooth structure inherited from ). Concretely, for a map that is injective on and has injective differential at every point of , boundary points included (Lean predicate IsSmoothClosedBallIn n K). The topological counterpart, homeomorphic to , is IsTopClosedBallIn n K.
For every smooth embedding and every point , writing for the connected component of containing ,
Equivalently: is unknotted.
The result itself. By milestone 2, always bounds two topological -balls. So a counterexample to the goal would produce an exotic smooth structure on that embeds in ; a proof would show that no exotic , if one exists, embeds in . The problem is related to, but independent of, the smooth -dimensional Poincaré conjecture. For example, the Poincaré conjecture could hold while carries an exotic smooth structure. The goal also completes the uniform statement "every smooth is unknotted" across all dimensions.
Formalizing it. The goal is open. Milestones 1–5 are classical theorems, and no existing machine-checked proof of them for smooth spheres is relied on here. Formalizing them is substantial independent work and would add basic infrastructure to Mathlib's manifold library: separation theorems, collars, and smoothing of balls.
The topological statement is known in every dimension (milestone 2), so the difficulty is purely smooth. In dimensions the passage from "homeomorphic to a ball" to "diffeomorphic to a ball" goes through the -cobordism theorem. That theorem fails in the smooth category in dimension , because the Whitney trick is unavailable. Freedman's topological methods do not control smooth structures. The naive approach is to apply the high-dimensional argument verbatim, and this breaks at exactly this step. Known partial results (Scharlemann) need strong restrictions on the embedding, such as genus bounds or few critical points of a height function.
EuclideanSpace ℝ (Fin (n+1)), with Mathlib's standard smooth manifold structure modelled on EuclideanSpace ℝ (Fin n). Smoothness means (ContMDiff … ∞), not analytic.mfderiv everywhere). This is equivalent because is compact.connectedComponentIn (Set.range f)ᶜ x for . The conclusion is required for every such , so for both sides of .mfderiv, which is not injective.Stochastic dual dynamic programming (SDDP) and related decomposition methods solve multistage stochastic programs by approximating each stage's recourse function from below by a maximum of affine cuts. Every cut needs a value and a slope: the value of a convex subproblem at a trial point, and a subgradient of that subproblem's optimal value as a function of the trial point. For linear subproblems the slope is a vector of dual multipliers. For convex subproblems in which the trial point enters the objective and the nonlinear constraints, the slope requires a formula for the subdifferential of the value function of a parametric convex program.
Vincent Guigues, in Convergence Analysis of Sampling-Based Decomposition Methods for Risk-Averse Multistage Stochastic Convex Programs (arXiv:1408.4439v4, SIAM J. Optim. 2016), states such a formula as Lemma 2.1 and announces it in the abstract and in contribution (C) as a result of independent interest. Earlier convergence proofs for convex SDDP (Girardeau, Leclère and Philpott, Math. Oper. Res. 2015) avoid the question by copying the trial point into new variables and linear constraints, so that only the classical formula for a value function of right-hand-side perturbations is needed. Lemma 2.1 removes that device.
This mission is the second in the series on Guigues' paper. The first mission formalizes the almost-sure convergence of the risk-averse algorithm (Theorem 4.1) and takes the subgradient property of cut slopes as part of its model, so the two missions are independent.
Write for Euclidean space with the scalar product , and pair by . Let , , , let , let be constraint functions on , and let and be nonempty, compact and convex. The value function (2.1) is
defined for every , with when . The solution set is and the active set is .
The subdifferential of an extended-real function at is , and the normal cone of a set at is . The Lagrangian dual (2.3) maximizes
over , ; its solution set is .
Assumption (H): is lower semicontinuous, proper and convex; each is convex and lower semicontinuous with values in ; and for some , where .
Assume (H) and the repaired Slater condition: every is real-valued (R1), and there is with , for all (R2), and (R3). For with , the set is nonempty and for every
If and the are real-valued, convex and differentiable, then under (R2)
Formula (2.4) yields cut slopes for SDDP applied to convex multistage programs directly from a primal solution and multipliers of the stage subproblem, without auxiliary copies of the state, and it is the source of the subgradient property used in the convergence analysis of the paper's Algorithm 1. The differentiable case is the form an implementation uses: any optimal dual pair gives a subgradient, and every subgradient arises this way.
For formalization, the result is a self-contained piece of finite-dimensional convex analysis: infimal projection, the subdifferential sum rule under a relative-interior condition, normal cones of intersections, of affine sets and of convex sublevel sets, and Lagrangian duality under Slater's condition. None of these steps is in Mathlib in the extended-real form needed here. No machine-checked proof of Lemma 2.1 or of its differentiable case exists. The platform has Shor's subgradient formula for value functions (ShorNonsmooth.Decomposition.value_function_convex_and_subgradient, subgradient_formula, subgradient_formula_differentiable, proved). Those statements cover real-valued data with inequality constraints only and prove one inclusion. They have no equality block , no set and no converse, so they are related to this mission but are not instances of it.
The printed lemma is false. Two steps of its proof fail. First, the formula for needs a strict Slater point: for , equals its own relative interior, but is not generated by . With , and , all printed hypotheses hold, , and no satisfies (2.4). Second, does not give : with , and , while . The repair (R1)–(R3) adds hypotheses and leaves every step of the printed proof valid.
The remaining work is the relative-interior calculus. The sum rule and the intersection formula for normal cones hold only under qualification conditions phrased with relative interiors, and the converse direction of (2.4) needs that the qualification passes from to . A proof that uses only interiors fails as soon as is lower-dimensional, which the hypotheses allow.
Vectors live in EuclideanSpace ℝ (Fin k). The product is the Lean product type, and subgradients and normal cones on it use the explicit pairing . No norm of the product is involved. Extended values are EReal. is an EReal infimum on all of , and is its subdifferential on , not relative to . An encoding of on only, or of relative to , would describe a different function, whose subdifferential is unbounded at boundary points of ; it is excluded. Subdifferentials require a finite value at the base point, so the equivalence cannot hold vacuously at a point where a function is . is Metric.cthickening ε X; relative interiors are intrinsicInterior ℝ. Indices are 0-based (Fin p, Fin q). The sums in (2.4) are written with explicit witnesses , indexed by the active set, which avoids the convention .
Repaired statements, each labelled "(repaired)" in its title:
The sum-rule milestone keeps (2.6) as a hypothesis, as the page states it. The dual-solution milestone reads "primal-dual solution" as , with zero duality gap, assumes only primal feasibility of for the converse (as the page does), and extends by zero outside the active set.
A complete development needs: the subdifferential sum rule for proper convex extended-real functions under a relative-interior condition; normal cones of intersections of convex sets with one affine set; normal cones of sublevel sets of finite convex functions under Slater's condition; existence of minimizers of lower semicontinuous functions on compact sets; and a zero-duality-gap (minimax) theorem for Lagrangians of convex programs over a compact convex set. These are reusable well beyond this mission. Contributions of any of these lemmas, in the generality of an arbitrary finite-dimensional inner product space, are welcome.
Multistage stochastic programs model sequential decisions under uncertainty: hydro-thermal scheduling, portfolio management and capacity planning are standard examples. Their dynamic programming equations involve recourse functions (cost-to-go functions) of the decision history, which cannot be computed exactly. Stochastic Dual Dynamic Programming (SDDP), introduced by Pereira and Pinto in 1991, approximates each recourse function from below by a maximum of affine cuts, built at trial points generated by simulating sampled scenarios. SDDP is the method of choice in the energy industry for long-horizon stochastic planning.
Two extensions motivate this mission. Risk-averse planning replaces the expectation at each stage by a coherent risk measure (for instance the Conditional Value-at-Risk), and many applications have convex but nonlinear stage problems. Guigues (2016) proves that the risk-averse sampling algorithm for convex stage problems converges almost surely.
Timeline.
There are stages with decisions and a given . A history is identified with the vector with its Euclidean norm. The random data are interstage independent (H1). For , takes values with probabilities , and is deterministic. A realization consists of a cost with values in , convex constraints and linear constraints . Together with a compact set , they define the feasible set .
The risk measure of stage is given in dual form,
The recourse functions satisfy and, for ,
The first-stage value is . Assumption (H2) requires convexity, lower semicontinuity and properness of the data, and fixes an such that the costs are finite and the feasible sets nonempty on the -fattening . It also asks for a relative-interior point of the nonlinear constraints.
Algorithm 1 keeps cutting-plane models , starting from . At iteration it computes decisions at every node of the scenario tree, by solving the stage problems with in place of . It then samples one scenario , with indices satisfying the independence assumption (H3), and adds at each sampled node one cut
Here attains the supremum in , and is a subgradient of .
Almost surely, for and every node of stage ,
Almost surely, moreover, , and every accumulation point of the first-stage decisions is an optimal solution of the first-stage problem.
Theorem 4.1 guarantees that the algorithm's lower bound converges to the true risk-averse optimal value, and that its first-stage decisions approach optimal ones. It covers nonlinear convex stages, where finite convergence arguments for polyhedral problems do not apply. It also covers every risk measure with a dual representation, including CV@R and its combinations with expectation. Practitioners rely on this to justify stopping rules based on the lower bound.
The result is proved on paper. To our knowledge neither Theorem 4.1 nor its risk-neutral counterpart (Girardeau–Leclère–Philpott, Theorem 3.1) has been machine-checked; the risk-neutral statements are posed, unproved, on this platform. A formalization would check a proof that combines convex analysis (value functions of convex programs, subgradient bounds, Lipschitz continuity on fattenings), cutting-plane bookkeeping and a probabilistic argument (strong law of large numbers along a predictable subsequence).
The cuts are built only along sampled scenarios, so at a given node the approximation is refined only at the iterations whose scenario passes through it. The obvious induction argument controls the error only along those iterations. Extending it to all iterations is the probabilistic core (4.29). It needs the samples to be independent of everything the algorithm has computed so far, and it needs a strong law of large numbers along the subsequence of iterations at which the error is still large. A second difficulty is passing from the current model to the previous one . This needs uniform Lipschitz bounds on the models (Lemmas 3.2, 3.5), which in turn rest on the fattening in (H2) and on the subgradient bound of Proposition 2.2.
PiLp 2), so fattenings, inner products and Lipschitz constants use the Euclidean norm on . Fattenings are closed thickenings.EReal, infima are on empty feasible sets, and weights are real numbers (with ). Limits of gaps are taken in EReal, so that convergence to forces the gaps to become finite.run_exists shows that under (H2), with closed , rules producing a run exist for every sample path.Multistage stochastic programs model decisions taken over time while uncertain data are revealed: generation scheduling in hydro-thermal power systems, capacity expansion, unit commitment, portfolio management. When the uncertainty is represented by a finite scenario tree, the problem becomes one very large deterministic program, and decomposition algorithms solve it stage by stage. For linear problems the standard methods are nested Benders decomposition and its sampling variant, stochastic dual dynamic programming (SDDP), introduced by Pereira and Pinto (1991). Both rely on the convexity of the value functions, which they approximate from below by linear cuts.
Many applications need integer decisions (on/off status of generators, investment choices), and integer variables destroy convexity. Zou, Ahmed and Sun (Math. Program. 175 (2019) 461–502) observed that when the state variables passed between stages are binary, exact convex polyhedral representations still exist on the binary points. They proposed stochastic nested decomposition (SND) and its stage-wise independent special case SDDiP, and identified three properties of cuts (valid, tight, finite) under which the algorithms converge. This mission formalizes that convergence theorem, Theorem 2 of the paper.
Timeline. Birge (1985) gave nested decomposition for multistage linear programs; Pereira and Pinto (1991) introduced SDDP. Philpott and Guan (2008) proved almost sure finite convergence of SDDP-type methods for linear problems, and Girardeau, Leclère and Philpott (2015) extended convergence to convex problems. Zou, Ahmed and Sun (2019) proved finite convergence with probability one for mixed integer problems with binary states and abstract valid, tight and finite cuts, and showed that their Lagrangian cuts have the first two properties.
Let be a scenario tree with stages , root , parent map and children . The nodes of the last stage are the scenarios. Node probabilities satisfy , , and before the last stage, and . Each node has a linear cost and a nonempty compact mixed integer polyhedral set (assumption (A1)). The state is binary, the local variables are general, and the root's parent state is fixed. The problem in local-copy form (2.1) is
Its value functions satisfy the recursion (2.3): over the nodal feasible set, with the expected cost-to-go function .
The SND algorithm keeps an under-approximation of each : the maximum of a lower bound and the aggregated cuts collected so far (3.2). Each iteration samples scenarios with replacement. In the forward step it solves the nodal problems from the root down, which yields the forward tree solution of (3.6). In the backward step, at every sampled node it generates one cut per child at the state and adds their aggregate to . Cuts are valid if on (3.4). They are tight if they equal the value of the child's updated nodal problem at (3.5). They are finite if only finitely many distinct cuts occur. Assumption (A3) requires the nodal solver to return the same optimal solution whenever it is given the same problem.
With sampling with replacement, valid, tight and finite cuts, and a solver satisfying (A3), the following holds with probability one:
Theorem 2 separates the convergence of nested decomposition from the choice of cuts. Any cut family with the three properties yields an exact algorithm for multistage stochastic integer programs with binary states. The paper verifies the properties for integer optimality cuts and, through its Theorem 3, shows that Lagrangian cuts from the local-copy reformulation are valid and tight. The convergence of SDDiP, the variant used in computations, follows from the same theorem, and binary expansion of general integer states extends the reach to mixed integer state spaces.
The result is proved in the paper; no machine-checked proof exists. A formal development would turn its informal points into checked statements: that the minima are attained, that the DP recursion is equivalent to the extensive form, and that the finiteness of cuts is global. It would also supply a reusable framework (scenario trees with node probabilities, cut-based approximations, sampled runs) for the convergence theory of SDDP-type methods.
No single step is deep; the difficulty is the interaction of the pieces. A tempting argument says the approximations stop changing, so the algorithm stops at an optimum. But a stalled run need not be optimal: if a node at which is inexact is never sampled again, nothing changes and the forward solution stays suboptimal. The proof must therefore combine three things: the deterministic finiteness of changes, an almost sure statement about sampling, and the exactness chain (3.8). That chain depends on tightness with respect to the updated approximation of the child, and it fails if tightness refers to the approximation from before the backward step. The equivalence between optimality for the DP recursion and for the extensive form (2.1), used without proof in Claim 1, also requires a backward induction over the tree.
The tree is the platform definition StochasticProg.Multistage.Tree H, with stage of the paper equal to stage = t − 1. Binary vectors are Fin d → Bool, embedded in . The copy variable is eliminated through . Minima are written as infima over sets that the standing assumptions make nonempty, bounded below and attained. Lean iterations are numbered from , and the run is infinite (stopping criteria and bounds play no role).
Readings of informal words. "Optimal solution of (2.1)" means a feasible tree solution of least cost among all feasible tree solutions. "After a finite number of iterations" means from some iteration on, in every iteration (∀ᶠ i in atTop). "With probability one" refers to a probability space carrying independent draws, per iteration, each with law . "Finite" cuts means one finite set for the whole run, as the proof uses it, not a different finite set per iteration. (A3) means the solver is a function of the node, the parent state and the approximation, and returns an optimal solution.
Added hypotheses, which the paper uses without stating them: ; every nodal problem is feasible for every binary parent state, which replaces (A2) (not used by Theorem 2); and the lower bounds under-estimate, , which is Algorithm 1's "initial under-approximation".
Trivializing formalizations are ruled out: tightness refers to the child's approximation after its own update, optimality is for the true extensive form and not relative to , and the probability statement is over independent sampling, not over a fixed sample sequence assumed to visit every scenario.
Contributions welcome: the attainment lemmas for nodal minima, the DP/extensive-form equivalence on trees, and the second Borel–Cantelli argument for repeated sampling. All of these are reusable for other SDDP-type convergence results.
A data center or cloud platform routes each incoming task to one of parallel servers. Sending each task to a server with the shortest queue, the join-the-shortest-queue (JSQ) policy, minimizes waiting in a strong sense, but the dispatcher must learn all queue lengths for every arrival. The power-of-d schemes cut this communication: the dispatcher samples servers and joins the shortest of them. Mukherjee, Borst, van Leeuwaarden and Whiting ask how large must be for the sampled scheme to perform as well as JSQ as . They answer at two scales. At the fluid scale (mission 1 of this series) suffices. At the diffusion scale of the Halfin–Whitt regime, the subject of this mission, suffices, and does not.
Timeline:
There are servers, each with a buffer of size that counts the task in service. Tasks arrive as a Poisson process of rate , and each needs a unit-mean exponential amount of work, served at unit rate. A task sent to a full server is discarded. Under JSQ(d) the dispatcher samples servers without replacement () and sends the task to a server with the shortest queue among them. For this is JSQ.
The state is the occupancy vector , where is the number of servers with at least tasks. The conventions are and for . With the servers ordered by nondecreasing queue length, the -th ordered server has queue length . An arrival at position raises by one when . A departure at position lowers by one when . JSQ(d) routes to the smallest position in a uniform -subset of .
In the Halfin–Whitt regime , the diffusion-scaled state is
Here is the scaled number of idle servers.
Let , and . Assume for large and . If , then in , where for and
Here is a standard Brownian motion and is the nonnegative nondecreasing regulator with . The goal also asserts that this solution is unique.
The goal follows from 1–3.
The result. Theorem 2.4 shows that queue-length queries per arrival already achieve diffusion-level optimality: over any finite horizon only servers are idle and only hold two or more tasks, exactly as under JSQ. With Theorem 2.5 it identifies as the minimal order of . The diffusion limit is also the input for the steady-state analyses of JSQ in this regime (Braverman; Banerjee and Mukherjee).
Formalizing it. The result is proved on paper; nothing in it is machine-checked. A formalization needs:
The Eschenfeldt–Gamarnik limit (milestone 2) is cited by the paper, not proved in it, so its formalization is a separate, substantial contribution.
JSQ(d(N)) cannot be compared with JSQ path by path. The same arrival is routed to different servers under the two schemes, so their occupancy vectors drift apart and do not stay ordered. The obvious generator-based diffusion argument for JSQ(d(N)) itself does not close either. The routing probabilities depend on the whole ordered queue-length profile through -type terms, and these do not reduce to a function of at scale unless is large enough.
The threshold is sharp: for the limit is different (Theorem 2.5). Any argument therefore has to use the growth rate quantitatively, controlling at scale over a finite horizon how often JSQ(d(N)) fails to make a near-shortest choice. A qualitative fluid-type argument cannot do this. A second difficulty is the limit itself: (2.4) is a reflected equation whose regulator enters two coordinates, so even its well-posedness needs a Skorokhod-type argument with feedback.
Lean conventions:
Q i is for , with Q 0 = N, and positions are . The initial vector Fin k → ℝ lists levels .b : ℕ∞ with 2 ≤ b; ⊤ is an infinite buffer.expMeasure (λ + N) interarrival times through the published renewalCount/partialSum. Its i.i.d. marks are arrivals, with probability and a uniform -subset, or departures at a uniform position. Marks are independent of the clock and of a random initial state. The model is therefore the paper's in law. Sampling is without replacement, so JSQ(N) is JSQ.IsBrownianReal.Trivializing formalizations are ruled out. The goal asserts the existence of the limit (Brownian motion, initial value and solution), not merely that every limit point solves (2.4). The system hypotheses are satisfiable: the mark law has total mass one, which is checked in Lean. The convergence is of the whole path, including the tail above level .
Infrastructure needed and welcome:
An agent whose preferences change over time cannot simply optimize once: a plan that is optimal today may be abandoned tomorrow by the agent's own "future selves". This is time inconsistency, and its standard source is non-exponential discounting, studied since Strotz (1955). The usual response, going back to Strotz and made rigorous in continuous time by Ekeland and Lazrak (2006), is to look for an equilibrium strategy: a strategy from which no future self wants to deviate. In continuous time "no incentive to deviate" is encoded through a first-order condition, which Huang and Zhou call a weak equilibrium.
Björk, Khapko and Murgoci (2017, Remark 3.5) observed that this first-order condition need not express the absence of an incentive to deviate: it only says that a derivative vanishes or is nonnegative, and a stationary point need not be a maximum. Huang and Zhou (Math. Oper. Res. 46(2), 2021; read here as arXiv:1809.09243v3) introduce a strong equilibrium, which requires the agent's payoff to be no better after any short deviation, and study the two notions for continuous-time Markov chains with controlled generators. This mission formalizes their main example (Example 4.3): a concrete two-state model in which a weak equilibrium fails to be strong, so that an agent in one state strictly gains from deviating on every short interval.
The state space is . A generator is a matrix whose -th row lies in . Admissible rows form sets , and the control space is . A payoff function gives the payment rate at time difference in state when row is in force. The expected payoff of using from state is
The concatenation uses on and afterwards. A generator is a weak equilibrium if for all , , and a strong equilibrium if for all there is with for every .
The paper's first-order and second-order quantities are
with the payoff computed with the time derivative in place of .
In the two-state model of §4, , , every generator is with , and , with the pseudo-exponential discount . Example 4.3 takes , , , , and for , for .
The statement is fully explicit and has no hypotheses.
Remark 4.1: for , , for all small . And (4.13): the equation has a unique solution , and is a strong equilibrium.
The example shows that the weak equilibrium concept, the standard one in the time-inconsistency literature since Ekeland and Lazrak, admits strategies that an agent would abandon: Remark 4.1 exhibits a deviation that strictly increases the payoff on every short interval. Together with (4.13), it shows that in one and the same model a weak-but-not-strong equilibrium and a strong equilibrium coexist, so the choice of equilibrium concept changes which strategies are predicted. The example is the paper's justification for introducing strong equilibria.
The result is proved in the paper, through the first-order characterization (Theorem 3.1), the second-order test (Proposition 3.3, resting on the second-order expansion Lemma 3.2) and explicit computations in the two-state model. None of it has been machine-checked. A formal proof would provide checked versions of Theorem 3.1 and Proposition 3.3 for finite-state chains, reusable for any other example, and an independent check of the arithmetic of Example 4.3, where the source contains at least one misprinted formula.
Both conjuncts of the goal concern the small- behaviour of , an integral of products of matrix exponentials. Weakness reduces to a first-order comparison by Theorem 3.1, but its proof needs the expansion (3.6) with an remainder controlled uniformly enough to pass under the integral over . Failure of strong equilibrium cannot be read off the first-order term: at the maximizer of is not unique, every ties at first order, and the decision moves to the second-order coefficient of Lemma 3.2, whose derivation needs a second-order expansion of the concatenated payoff. The regularity hypotheses of Lemma 3.2 and of (3.3) must also be verified for the example's discount function.
States are Fin N; the paper's state is index , so in the two-state model state 1 is 0 : Fin 2 and state 2 is 1 : Fin 2. Expectations are written through the transition matrices (NormedSpace.exp (t • Q)) and Fubini, exactly as the paper computes on p. 23; no Markov process is constructed. Payoffs are Bochner integrals over . The weak-equilibrium condition is written as "for every , eventually as the quotient is ", which is without a real-valued liminf. The norm in (2.3) is the sup norm, equivalent to the paper's Euclidean norm because (2.3) quantifies over every .
Standing assumptions: , continuity of in (2.2) and the integrability condition (2.3). Theorem 3.1 adds the shift bound (3.3)–(3.5); Proposition 3.3 assumes the conditions of Lemma 3.2, with the derivative tied to . The closed forms (4.3)–(4.4) assume (the page allows , but with a zero rate the payoff integral diverges); the algebraic identities (4.5)–(4.8) keep the page's ; Example 4.3 has , . Statement (4.11) gives and the argmax; the page's case formula for contains a misprint and is not used.
No trivializing reading is available: the goal has no hypotheses, is built from and the concatenation uses before and after , so neither conjunct holds by a junk value. Integrability of every payoff follows from (2.3) and is never assumed.
Theorem 3.1 and the second-order package are also drafted in the companion mission on existence of equilibria; they are restated here in the sub-namespace StrongWeakEq.TwoState. The goal needs the verification of (2.3), (3.3) and the Lemma 3.2 conditions for the example (convexity of gives (3.15)), the closed forms of for two-state generators, and the expansions of the paper. Contributions of proofs of the general results (Theorem 3.1, Proposition 3.3) are welcome independently of the example.
Algorithms for smooth nonlinear programming, such as augmented Lagrangian, interior point and sequential quadratic programming methods, do not stop at exact Karush–Kuhn–Tucker (KKT) points. They stop at points where the KKT conditions hold approximately. Sequential optimality conditions make this precise: they are properties of sequences with approximate multipliers, satisfied at every local minimizer without any constraint qualification, and verified by the iterates of practical methods. To conclude that a limit point is a KKT point, one still needs a condition on the constraints. Andreani, Martínez, Ramos and Silva (Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018, doi:10.1287/moor.2017.0879) identify, for each of several sequential conditions, the weakest such condition. They call it the weakest strict constraint qualification associated with that condition, and they place each one within the classical hierarchy of constraint qualifications.
This mission concerns the Complementary AKKT condition (CAKKT) of Andreani, Martínez and Svaiter (SIAM J. Optim. 20(6), 2010). CAKKT is strictly stronger than AKKT and is satisfied by the limit points of an augmented Lagrangian method under a weak Łojasiewicz-type hypothesis. The paper's §6.1 compares the associated weakest strict CQ, CAKKT-regularity, with Abadie's constraint qualification, one of the classical conditions of nonlinear programming. The answer is that CAKKT-regularity implies Abadie's CQ, and the converse fails.
Timeline:
Let be continuously differentiable, and let
For feasible , is the set of active inequalities. The polar of a set is .
Abadie's CQ holds at when .
An objective satisfies CAKKT at if there are , and with
For and , let be the set of vectors with and . The point is CAKKT-regular if is outer semicontinuous at :
The inclusion always holds, so the content of the goal is the reverse inclusion. The milestones are the statements the paper's proof uses, in attack order:
with the equivalence of the two formulations (4.12)–(4.13) and (4.14)–(4.15) of CAKKT as a milestone.
Theorem 6.4 places CAKKT-regularity in the classical hierarchy. Every point at which CAKKT forces KKT for all objectives also satisfies Abadie's CQ, and therefore Guignard's. The paper's Example 6.1 shows that Abadie's CQ does not imply CAKKT-regularity. A convergence theorem for an algorithm that produces CAKKT sequences therefore cannot be stated under Abadie's CQ alone. Together with Theorem 4.3, this fixes exactly what a CAKKT-based method needs from the constraints.
The results are proved in the paper. None of them, and none of the variational-analysis facts they rest on, is formalized on Prove2Me, and Mathlib has no regular or limiting normal cones of nonconvex sets. The work is to formalize the paper's proof together with the parts of Rockafellar–Wets it cites: Theorem 6.11 (gradients of smooth functions as normals), Proposition 6.5, and Theorems 6.26 and 6.28(b). The last is Clarke's theorem that the regular tangent cone of a closed set is the polar of its limiting normal cone. These facts are reusable well beyond this mission.
The inclusion is elementary. The reverse inclusion cannot be obtained from CAKKT-regularity at alone, because CAKKT-regularity is a statement about multiplier combinations, which live on the polar side. The argument therefore has to pass through normal cones at points near . At such points the active set may differ from , and the complementarity residual must be controlled uniformly. Returning from polars to cones requires the passage from the limiting normal cone to the tangent cone (milestone 7). That is a deep fact about closed sets in finite dimension; it is not a formal manipulation of cones. Equality of polars would only give Guignard's CQ.
is EuclideanSpace ℝ (Fin n), indices are Fin m and Fin p, and gradients are Mathlib's gradient. The objects are:
Constraints n m p of two index families. Every theorem assumes IsC1 (each and is , the paper's standing hypothesis) and feasibility of .tangentConeAt allows negative scalars and is not used). The regular normal cone is empty off the set. The limiting normal cone and outer semicontinuity use the sequential Painlevé–Kuratowski outer limit, and the outer limit in CAKKT-regularity is taken over pairs with .The following would trivialize the goal and are excluded:
A complete development needs Clarke's tangent–normal polarity for closed sets in , the existence of functions realizing regular normals, and a penalty argument for Lemma 6.2. Proofs of the general variational-analysis milestones (3 and 7) are especially welcome, since they serve any mission on nonconvex constraint sets.
Many service systems must match jobs to servers whose quality is not known in advance: crowdsourcing platforms routing tasks to worker types, wireless schedulers assigning users to channels, and switches in data networks. The scheduler learns server quality only by trying servers, and every poor assignment lets work pile up. The natural performance measure is therefore not the cumulative reward loss of classical bandits but the queue-regret: the expected excess backlog compared with a genie that knows the best assignment.
Krishnasamy, Sen, Johari and Shakkottai, Learning Unknown Service Rates in Queues: A Multiarmed Bandit Approach (Operations Research, 2021; arXiv:1604.06377), show that queue-regret has two regimes. In an early stage it grows like the regret of a bandit. In a late stage, once the queue regularly empties, past mistakes are forgotten at every empty instant and the queue-regret decays. This mission formalizes their upper bound for the late stage: a UCB scheduler with forced exploration, Q-UCB, has queue-regret of order .
A discrete-time switch has queues and servers. In every slot , queue receives an arrival and link offers a potential service , all independent and i.i.d. over slots. The scheduler picks a matching , an injective assignment of a server to every queue, and queue evolves as
The scheduler observes only past schedules and the services offered on scheduled links.
Write , for its maximizer, , and . Assumption 1: each queue has a unique best server and the best servers are distinct, so is the unique optimal matching. Assumption 2: for all . The genie queue always uses . Assumption 3: the system starts from the stationary law of . The queue-regret is
Q-UCB (Algorithm 1) explores in slot with probability , scheduling a uniformly random member of a fixed family of matchings that together cover all links. Otherwise it exploits: for each queue it picks the server with the largest index , with the empirical mean and the number of past assignments of link , and schedules a matching closest in Hamming distance to these choices. Fix and set
For every with , and ,
The constants are the paper's, stated exactly.
The theorem shows that a simple learning scheduler loses only in expected backlog in the late stage. Together with the paper's lower bound for consistent policies (Theorem 3), this places the optimal late-stage queue-regret within a polylogarithmic factor. The analysis method has two parts: a high-probability statement that the learner has locked onto the optimal matching, and a regenerative argument that converts it into a bound on queue length. It applies to other learning-in-queues problems in the same way.
All results are proved in the paper (§8.2). None of them has a machine-checked proof. The mission produces a formal model of the learning switch, including the algorithm with arbitrary tie-breaking, the coupled genie and the stationary start, and checks the explicit constants. These constants rely on numerical facts stated in the proofs, for example a positivity check for in Lemma 10(b) and the absorption of lower-order terms into , which a formal proof must verify.
The obvious argument says that UCB eventually identifies the best server, so the queue behaves like the genie's. This fails for two reasons. First, the regret is an expectation of a queue length, and a queue remembers every early mistake until it next empties. So one must bound the current regenerative cycle, and that bound itself depends on the queue length, which forces the recursion of Lemmas 13, 14, 16 and 17. Second, UCB's standard logarithmic-regret analysis bounds the expected number of sub-optimal pulls. It says nothing about whether a sub-optimal pull happens in a specific late window. Forced exploration at rate is what makes all indices concentrate at once, and Lemma 11 requires a union bound over every link, slot and sample count with explicit exponents.
Fin U and Fin K, and slots are . The genie shares arrivals, services and with the system. This coupling is implicit in the paper's proofs and does not change .The source is the arXiv v4 preprint; the paper's proofs are in its §8 and §9.
Large data centers and cloud platforms route each incoming job to one of parallel servers through a single dispatcher. The join-the-shortest-queue (JSQ) policy, which sends each job to a server with the fewest jobs, has strong optimality properties for identical exponential servers, but it needs the queue length of every server at every arrival, which is costly when is in the thousands. The power-of- scheme JSQ() polls only servers chosen at random and joins the shortest among them. For fixed it improves dramatically over random routing, which is the supermarket model of Mitzenmacher and of Vvedenskaya, Dobrushin and Karpelevich, but it does not match JSQ.
Mukherjee, Borst, van Leeuwaarden and Whiting (arXiv:1612.00723, Stochastic Systems 2018) ask how fast must grow for JSQ() to behave like JSQ in the large- limit. This mission concerns their fluid-scale answer: any growth suffices.
Timeline.
There are identical servers, each with a buffer of size counting the job in service. Jobs arrive as a Poisson process of rate and need independent unit-mean exponential service. A job sent to a full server is discarded. The occupancy vector is , where is the number of servers with at least jobs, with the convention . If the servers are listed in nondecreasing order of queue length, the -th ordered server holds jobs. A dispatch scheme picks an ordered position for each arrival, and the arrival raises by one (or is discarded if ).
The schemes are:
Two systems are S-coupled when they share the arrival clock and the departure clock of the -th ordered server for every .
The fluid-scaled state is . It lives in
which carries the distance. For let . The coefficients of (4.4) send all incoming work to level while the rate can be absorbed there, and the excess to level : if then ; otherwise , , and all other vanish.
Assume , and in . Then every subsequence of has a further subsequence converging weakly (Skorohod ) to a limit satisfying
The statement fixes no rate for , which is what makes it the right goal.
The milestones follow the paper's proof.
The result. Theorem 2.1 shows that on the fluid scale the optimality of JSQ costs nothing beyond queue inquiries per job, far fewer than . In particular the fluid limit is the same as that of JSQ, which is fluid-optimal. The coupling framework of §3 (the class CJSQ(), stack orderings, S-coupling) is not tied to JSQ(). The paper uses the same tools for the diffusion-scale Theorem 2.4, for batch arrivals and for the interchange of limits, Proposition 2.2.
Formalizing it. Proofs of the paper's results exist; no machine-checked version does. The mission produces:
The proof of Theorem 4.1 in the paper is sketched in places (the time-scale separation is argued "analogously" to Hunt and Kurtz), so a formal proof would also settle those steps.
The obvious argument would compare JSQ() directly with JSQ: the two disagree whenever the sampled servers miss every shortest queue. When a constant fraction of servers is idle this is rare, but when few servers share the minimum queue length the disagreement rate does not vanish, and a direct coupling fails. The paper instead passes through CJSQ() with , which is close to JSQ() for a suitable and sandwiched between JSQ and MJSQ().
The second difficulty is the topology. The sandwich controls tail sums , so the fluid limit of JSQ is needed in , not coordinatewise. With the state space is infinite-dimensional, and tightness requires uniform control of tails. Finally, the JSQ fluid limit itself involves a separation of time scales: the drift is discontinuous in and arises as an averaged stationary behaviour of a fast process.
ℕ →₀ ℕ with the paper's level index; coordinate holds . The buffer is with ; both finite and infinite are covered.ℕ → ℝ with . carries the distance, computed in .A formalization that states only "every limit point solves (2.1)", or that measures convergence coordinatewise, would be vacuous or weaker: it is ruled out by requiring the limit's existence and convergence.
Needed infrastructure. The development needs Poisson clocks and thinning, martingale bounds for counting processes, compactness in , tightness and Prokhorov's theorem on Polish spaces, and the Skorohod representation. The compactness and tightness criteria (Lemmas 4.6, 4.7) and the stack ordering (Proposition 3.1) are reusable on their own. Proofs of any milestone are welcome, as are proofs of Theorem 2.1 that bypass Theorem 4.1.
In the prophet inequality a gambler observes independent nonnegative random values with known laws one at a time and must decide irrevocably, after seeing each one, whether to stop and keep it. Her expected reward is compared with that of a prophet who knows all realizations and earns . When the values arrive in a fixed adversarial order the best guarantee is (Krengel, Sucheston and Garling, 1977; Samuel-Cahn, 1984). Prophet inequalities are the stopping-theoretic core of posted-price mechanisms in online auctions, where a guarantee for the gambler translates into a welfare or revenue approximation for sequential pricing.
The prophet secretary problem keeps arbitrary independent laws but lets the values arrive in a uniformly random order, as in the secretary problem.
An instance is a list of laws of independent nonnegative random variables , all continuous. A uniformly random permutation of , independent of the values, is the arrival order: at time the gambler sees .
The time threshold algorithm stops at the first time with . Its stopping time is and the gambler's reward is , written .
A blind strategy is a nonincreasing function . Given an instance, draw independently and uniformly from , let be the -th smallest, and choose thresholds by
The strategy is called blind because fixes the levels of the distribution of the maximum at which the gambler stops, independently of the instance and of . The deterministic blind strategy (Definition 3.1) uses in place of . A piecewise-constant strategy uses at most distinct levels.
There is a nonincreasing such that, for every and every continuous instance,
where is the stopping time of the blind strategy . One serves every instance.
Theorem 1.1 raised the guarantee for the prophet secretary problem from just above to , and it separates random-order arrival from adversarial arrival by more than the classical single-threshold analysis. The strategies are distribution-insensitive in a precise sense: the gambler needs only the distribution of the maximum, not the individual laws, and does not depend on . The milestones are general facts about multi-threshold stopping in random order (Lemmas 3.1, 3.3, 4.1, 4.2) that apply to any nonincreasing thresholds, not only to blind ones.
The result is proved in the paper, with one numerical step: Corollary 4.4 evaluates the bound of Lemma 4.3 at a specific vector found by optimization, which the paper does not print. No part of this argument has a machine-checked proof. The formalization would make the reduction from blind to deterministic strategies, the stopping-time estimates and the final numerical certificate explicit and checked. The paper also shows that no blind strategy guarantees more than (Theorem 1.2, outside this mission); any later improvement of the constant leaves this goal, which asserts only , intact.
The obvious argument fixes a threshold and bounds the probability that some value exceeds it; with one threshold this cannot beat , and with time-varying thresholds the events "the gambler has not stopped by time " and "value arrives at time " are dependent, because the arrival of at time removes from the earlier times. The union bound loses exactly the constant one is trying to gain. The analysis must therefore bound the law of the stopping time uniformly over all instances (Lemma 3.3), sharpen the conditional survival probability (Lemma 4.1) and the union bound (Lemma 4.2), and then pass to the limit of large instances. The final constant depends on a numerical optimization over levels, so the closing step is a certified evaluation of an explicit but long expression involving -th roots and logarithms.
All statements import one definitions file, BlindProphetSec.Blind.Setting.
μ : Fin n → Measure ℝ with IsProbabilityMeasure, NullSingletonClass (continuity, the paper's standing assumption of §1.2 and §3) and μ i (Set.Iio 0) = 0 (nonnegativity). Independence is built in: the values are the coordinates of Measure.pi μ. Indices and times are 0-based; the paper's time is j.val + 1.A trivializing formalization is ruled out: the strategy (and the vector of Corollary 4.4) is quantified before and the instance, the constants and are exact rationals, and expectations cannot collapse to through non-integrability.
A complete development needs order statistics of uniform samples, exchangeability arguments for uniformly random permutations, convergence of the padded deterministic strategies, and a certified numerical evaluation of . The random-order stopping vocabulary is reusable for other prophet secretary results, including the upper bound of the companion mission. Contributions to any milestone, including partial results such as Lemma 3.2 (), are welcome. The PDF used is the arXiv preprint, version 2 (arXiv:1807.07483v2, 12 March 2019); all labels and pages refer to it.
Stochastic dual dynamic programming (SDDP) and its relatives are the standard algorithms for multistage stochastic programs: hydro-thermal scheduling, energy storage and long-horizon capacity planning are solved with them in industry. They approximate each future cost function from below by a maximum of affine cuts, compute new cuts only at a few randomly chosen nodes of the scenario tree, and use the current approximations to simulate decisions forward. Whether such sampled cutting-plane schemes converge, and in what sense, decides whether their bounds can be trusted.
This mission formalizes the stochastic part (§3) of the 2015 paper. Mission 1 of the series covers its deterministic part (§2).
A finite scenario tree has nodes , root , parent map , children , leaves , and node probabilities with and . Every node carries a control multifunction , a cost and linear dynamics ; every node carries a compact convex stock set ; leaves carry final costs . The future cost functions are defined backwards by (20):
Assumptions ask for convex, lower semicontinuous, proper costs, convex compact-valued convex multifunctions , Lipschitz final costs, and an extended relatively complete recourse condition: feasibility and finite cost on a -neighbourhood of every .
The algorithm keeps approximations , starting from . At iteration it simulates the whole tree with , producing stocks and controls . Cuts are computed at the selected nodes by solving the stage problems (21) at their children and averaging optimal values and Lagrange multipliers with weights . Every approximation is then updated by (22), . The selections form a random process. It is τ-admissible (Definition 1) when, inside each block of iterations, cuts are computed backwards along the tree, and when the block indicators are i.i.d. in , independent of the past, and equal to with positive probability.
Under and a τ-admissible selection process, almost surely, for every non-leaf node and every node respectively,
The decisions become optimal for the true problem and the approximations become exact at the visited stocks. Nothing is claimed about exactness elsewhere in the state space.
The theorem covers in one statement CUPPS (1-admissible), DOASA and SDDP (-admissible), and many other sampling schemes, for stage problems that are convex rather than linear and for scenario trees without stagewise independence. It shows that the lower bound produced by these methods converges to the optimal value along the simulated trajectories.
The result is proved on paper. It is not formalized anywhere: no proof assistant library contains SDDP-type algorithms for convex stage problems. This mission makes the algorithm, the τ-admissibility notion and the convergence statement precise. Formalizing them corrects slips of the printed statements: the lower-bound property holds on the affine hull of only, the boundedness of the cut slopes concerns finite cuts only, and the theorem's two limits concern different node sets. The rest of the work is the formalization of the published proof.
The deterministic argument (mission 1) shows exactness at stage from exactness at stage along the whole iteration sequence. In the stochastic case a node is updated only at the random iterations at which it is selected, while its stock moves at every iteration. Exactness along the selected iterations (32) does not transfer to the others: a selection rule that updated a node only when its stock lay in a given region would leave the approximation inexact elsewhere. The proof has to show that the iterations at which the approximation is still -inexact are, by independence, selected with positive frequency. This requires the event " is -inexact" to be measurable with respect to the past selections, so the algorithm's choices among multiple minimisers and multipliers must be deterministic (footnote 6). It also requires the optional-skipping Lemma 5.4 and the strong law of large numbers. The first idea of conditioning on the stocks directly fails because the stocks depend on all past selections.
EuclideanSpace ℝ (Fin d), controls in EuclideanSpace ℝ (Fin p). Costs and value functions take values in EReal; convexity is epigraph convexity; off ; the initial approximation is . Limits are EReal limits, so convergence to forces the differences to be finite eventually.StochasticProg.Multistage.Tree (a finite rooted tree with stages) is referenced; leaves, ascendents and node probabilities are defined on it. Costs are indexed by the child node as in (19a) and (20).Vc k is the paper's .Bool-valued maps on a probability space; Definition 1 (i) holds on every path; (ii) is per node, i.i.d. in and independent of , with no independence across nodes.run_exists shows that runs exist for every selection path, and a sanity check shows and τ-admissibility are satisfiable, so the goal is not vacuous. Its conclusion mentions none of the proof's auxiliary objects.EReal-valued convex functions, are welcome.In distributed optimization a network of agents minimizes a sum of private functions while each agent talks only to its neighbours. Applications include federated and decentralized learning, sensor networks and multi-robot systems, where the data cannot be pooled at one site. Many of these networks are directed (communication links are one-way, for instance because transmission powers differ) and time-varying (links come and go). On such networks no doubly stochastic mixing matrix is available in general, and plain averaging drifts toward a weighted average instead of the true one. The push-sum protocol corrects this drift by carrying an auxiliary weight at every agent (Kempe, Dobra & Gehrke 2003; Nedić & Olshevsky 2015).
Y. Sun, A. Daneshmand and G. Scutari (arXiv:1905.02637v2) analyse SONATA, a gradient-tracking method in which each agent solves a strongly convex surrogate of its local problem instead of taking a gradient step, for composite problems (a convex, possibly nonsmooth regulariser and a convex constraint set). They prove linear convergence on undirected graphs (their Theorem 3.9, the companion mission of this series) and, in Section 4, for a push-sum version over time-varying digraphs (Theorem 4.5). This mission formalizes the second result.
Timeline. Gradient tracking with push-sum over time-varying digraphs appears in NEXT/SONATA (Di Lorenzo & Scutari 2016; Scutari & Sun 2019), where convergence was proved without rates for nonconvex problems. Linear rates for smooth unconstrained strongly convex problems over time-varying digraphs were obtained for Push-DIGing (Nedić, Olshevsky & Shi 2017). Sun, Daneshmand and Scutari (2019, revised 2020) extend the linear rate to the composite, constrained setting with surrogates, and require only the average , not every , to be strongly convex.
Problem (P). Agent holds ; the agents solve
Assumption A: is nonempty, closed and convex; each is twice differentiable on an open set and convex; on with ; is convex on . is the solution and .
Surrogates (Assumption C). Each agent has , on , with , -Lipschitz and -strongly convex on . Constants satisfy on (15); , .
Network (Assumption B′). At time the digraph has edge set ; is a link from to . There is an integer such that the union of the edge sets over every window is strongly connected.
Weights (Assumption E). is column stochastic, , if and for other .
Algorithm 3. From , , , each agent computes
then , and .
The analysis uses the weighted gap , the tracking error , and the consensus errors , measured against the -weighted averages.
If , there is such that for every , every run and every agent ,
The goal is qualitative: neither nor the rate is fixed, so it survives any improvement of the constants.
In attack order: the weighted tracking identity (74) and its consequence ; the bounds (p. 29); the per-agent descent inequality (Lemma I.1); the lower bound on the weighted step length (Lemma I.2); the tracking-error bound (Lemma I.3); the contraction (Proposition 4.1); the bound of by and (Proposition 4.3).
Theorem 4.5 gives a linear rate for distributed composite and constrained optimization over time-varying directed networks. Two features matter: the individual need not be strongly convex, and the surrogates cover proximal-gradient steps, DANE-type local solves and mirror-descent steps under one analysis. The rate depends on the surrogate-mismatch constants , which is the mechanism by which the paper shows that local computation helps when the are similar.
The result is proved in the paper; the proof of Theorem 4.5 refers to the undirected argument, and several of its supporting statements (Propositions 4.1 and 4.3) have their proofs omitted or relegated to the supplement, with consensus estimates quoted from Scutari & Sun (2019). To our knowledge none of it is machine-checked. A formalization produces a checked proof of the directed result together with reusable statements about push-sum weights over -strongly connected digraphs.
The obvious argument is to repeat the undirected proof with weighted averages. Two steps fail. First, the -weighted average is not the minimiser of , so consensus errors measured against it lose a constant (the 8 in Lemma I.3 instead of 4), and every passage between weighted and unweighted sums needs the bounds , which rest on a product-of-matrices argument over windows of length . Second, the matrices change with , so there is no single contraction factor; geometric decay of the consensus errors holds only over windows, and the coupling between the optimality gap, the consensus errors and the step lengths must be closed by a small-gain argument whose constants are uniform over the run. The step-size threshold must not depend on the starting point.
Points are EuclideanSpace ℝ (Fin d); stacked vectors are Fin m → ℝ^d with the Euclidean norm , never Lean's sup norm. The Hessian is the derivative of the gradient, and Loewner bounds are quadratic-form inequalities. Time is 0-based. A run is a relational predicate: is some minimizer of the subproblem, whose existence the paper takes for granted; is assumed to exist. The divisions by appear as in the paper and are genuine, since Assumption E keeps the weights positive. is convex on and locally convex on (positive semidefinite Hessian; need not be convex), , and are parameters: the statements hold for every valid choice. The graph sequence, , and the matrices come before ; the starting point and the run come after . The bounds on are stated for (the printed is at ), and positivity of is claimed only when or .
The following do not count as a formalization of the goal: an unsatisfiable run predicate (a sorry-free verification file exhibits a run satisfying every hypothesis), a chosen after the run, the bounds or a contraction factor assumed in place of Assumptions B′ and E, and dropping the normalisation.
Not posed: the explicit rate (Theorem III.1), the complexity corollaries, and the consensus estimates Lemma 4.2 and Proposition 4.4, whose constants come from Scutari & Sun (2019) (as printed, is negative). A complete development needs Taylor expansions with integral remainder along segments, first-order optimality for composite problems on convex sets, and products of column-stochastic matrices over strongly connected windows; the last is reusable for any push-sum method. Contributions to any milestone, and to the missing consensus estimates as auxiliary lemmas, are welcome.