Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The multi-secretary problem is the basic model of selecting under a budget from a stream of offers. Hiring a fixed number of candidates, accepting a fixed number of requests for a perishable resource, and admitting customers into a capacity-limited service all have this structure. Each item must be accepted or rejected on arrival, and the comparison point is the offline decision maker, who sees the whole sequence and keeps the best items. The gap between the two expected values is the regret.
A common class of heuristics in revenue management and online resource allocation does not react to the realised history. These policies fix in advance, period by period, a probability of accepting each type of item, and then follow it until the budget runs out; static bid-price and randomised-acceptance rules are of this kind (Talluri and van Ryzin 2004). Arlotto and Gurvich (arXiv:1710.07719v2, Theorem 1) show that when abilities take finitely many values, an adaptive policy has regret bounded uniformly in the horizon and the budget . Their Theorem 3 shows that the restriction to non-adaptive policies costs order over a wide range of budgets. Read together, these two results separate adaptive from non-adaptive control by an unbounded factor. This mission formalizes the non-adaptive half.
There are candidates with abilities , independent and identically distributed on values , with masses and . Write and . The budget is , with .
The offline value is
A non-adaptive policy is a matrix . At time , if budget remains and , the candidate is selected with probability , independently of everything else. The selection coins are then independent Bernoulli variables with . The policy selects until coins have come up. Its value is the expected total ability selected, and
The deterministic relaxation replaces the random counts by their means. Its value is
with solution . The index policy takes its probabilities from : .
For every , and there is such that, for all masses with and all with ,
The constant does not depend on the masses beyond , nor on or .
Theorem 3 is the lower half of the separation in Theorem 1 of the paper. The Budget-Ratio policy and the dynamic-programming policy have regret , uniformly in , while every non-adaptive policy has regret when lies strictly between and . The order of fluid and static randomised policies is therefore a property of the whole class, not of a poor choice inside it. Lemma 4 shows that the budget range cannot be removed: with a small budget a non-adaptive policy is as good as any.
The result is proved in the source but has not been machine-checked. A complete development would formalize, inside one finite probabilistic model: the binomial overshoot bound, a uniform anti-concentration estimate for Bernoulli sums, the structure of optimal non-adaptive policies, and the comparison with the offline sort. The source's proof of Theorem 3 also relies on a lemma that fails as printed (see Formalization scope), so a formal proof would close a real gap in the published argument.
The upper bound of order (Lemma 3) follows from a variance computation. The lower bound must hold for every non-adaptive policy, including time-varying ones, and the obvious argument does not cover them. That argument compares a policy with the index policy and shows the index policy loses . A policy can, however, differ from the index policy by order in its expected selection counts and still have regret of the same order. The step "small regret forces ", which the source uses, is exactly the step that fails.
What has to be shown is that the selection count of an optimal policy fluctuates by order , uniformly in the policy. A policy that runs out of budget early then misses top-value candidates late in the horizon, and one that keeps budget wastes slots. Both effects must be bounded below by a multiple of that is uniform over all masses with the same . Lemma 5 needs a normal approximation with an explicit, -independent error. Lemma 7 needs the existence of an optimal policy, which is a maximisation over a continuum of matrices.
The source is the arXiv preprint arXiv:1710.07719v2 (1 June 2018). Its printed page numbers equal the PDF page numbers.
a f : Fin m → ℝ. Lean index is the paper's index , so a 0 is the largest value and f (Fin.rev 0) is the mass of the smallest. The standing assumptions of Sec. 2 are IsValues a (strictly decreasing, positive) and IsMasses f (positive, summing to one).Contributions of any kind are welcome. Reusable pieces include binomial overshoot bounds, anti-concentration for sums of independent Bernoulli variables (for example via a Wasserstein normal approximation, which Mathlib lacks), and compactness arguments for optimal randomised policies.
A controlled Markov process (CMP), or Markov decision process, models a system that moves randomly between states while a controller chooses actions that influence both the cost incurred and the next state. When the planning horizon is long and no discounting is natural (queueing control, inventory, communication networks, maintenance), the criterion of interest is the long-run average cost. Average-cost problems are harder than discounted ones: the dynamic programming operator is no longer a contraction, and an optimal policy need not exist without structure.
The survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993)) organizes the theory by state space. For Borel state spaces and bounded costs, §6.1 follows Dynkin and Yushkevich and works with canonical triplets: a pair of bounded functions and a policy that make the policy optimal for every finite horizon with a fixed terminal cost. Theorem 6.3 is the statement that explains why this notion is the right one: a canonical triplet solves the average-cost problem.
Timeline. The notion of a canonical policy was introduced by Yushkevich (1973) and developed in Dynkin and Yushkevich's Controlled Markov Processes (1979, Chap. 7), which contains the substance of Theorem 6.3 (i)–(iii). Mandl (1974) introduced the discrepancy function that bears his name. The almost-sure statements (v)–(vi) are due to Georgin (1978). Coupled optimality equations for the multichain case go back to Howard (1960).
The model is a five-tuple . The state space and the action space are Borel spaces. For each state , is a nonempty compact set of admissible actions, and is measurable. is a transition kernel and a measurable one-stage cost, nonnegative on .
A policy chooses the action at time at random from a kernel that may depend on the whole history and charges only . The class of all such policies is . Each policy and initial state determine a law of the state–action process , with expectation .
For a horizon and a terminal cost ,
The average cost is and the optimal average cost is . The span of a bounded function is .
With the bounded measurable functions, a triplet with and is canonical if
A policy is strong average optimal if
Let be a canonical triplet and let be bounded on . Then for each :
The proof's milestones are: ; the decomposition ; part (i) on its own; and .
If is constant and is Mandl's discrepancy function, then for every and ,
and the running average converges to almost surely if and only if almost surely. Moreover is sample path average cost optimal. The intermediate milestones are on , the almost-sure limit under every policy, and almost surely under .
The result. Theorem 6.3 reduces the average-cost problem on a general Borel space to finding a canonical triplet. Once one is found, is the optimal average cost from every initial state, possibly state-dependent as in multichain models, and the canonical policy is optimal in a strong sense: its worst-case long-run performance is no worse than the best-case long-run performance of any competitor, at every finite horizon up to the additive constant . With constant , optimality also holds path by path. The rest of §6 of the survey looks for conditions on and that produce a canonical triplet, and those results rely on this theorem.
Formalizing it. The result is classical and proved; it has no machine-checked proof that we know of. Formalization requires measure-theoretic infrastructure for history-dependent policies on Borel spaces (Ionescu-Tulcea path measures, finite-horizon costs, infima over all admissible policies) together with a strong law for bounded martingale differences for parts (v)–(vi). Both are reusable for any average-cost result on general state spaces.
Parts (i)–(iii) are short on paper; the work is in making every quantity genuine. The infimum ranges over a class of kernels, and turning (6.4) into a usable inequality needs the family bounded below. The decomposition of needs integrability, which comes from the almost-sure confinement of the trajectory to , a consequence of admissibility under the path measure. Parts (v)–(vi) need the conditional expectation identity from the Markov structure of the path measure, and a martingale strong law. The tempting shortcut of restricting to stationary or Markov policies is not available: and every competitor are arbitrary history-dependent randomized policies.
Kernel.trajMeasure. is a Bochner integral and a real infimum; every theorem assumes bounded on , which makes both genuine.EReal, so no limit superior or inferior is a junk value. Part (iii) is the two equalities and .Contributions welcome: a.s. confinement of trajectories to , integrability lemmas for , the Markov property of trajMeasure in the form above, and a strong law for bounded martingale differences.
A controlled Markov process run under the long-run average cost criterion asks for a policy minimizing the asymptotic cost per stage. When every stationary policy induces a single recurrent class, the optimal average cost is a constant and is characterized by one equation, the average cost optimality equation (ACOE). In general it is not: under some policies the state process splits into several ergodic classes, different classes have different optimal costs, and the optimal average cost is a function of the initial state. This is the multichain case.
For finite models, Howard ([Dynamic Programming and Markov Processes, 1960, pp. 61–62]) introduced a pair of coupled equations for this situation: one for the gain function alone, and one, the ACOE, for together with a relative value function . Denardo and Fox (1968) developed the approach for finite multichain Markov renewal programs. For general Borel models, Yushkevich (1973) and Dynkin and Yushkevich (1979) introduced canonical triplets: a gain , a terminal cost and a policy such that is optimal for every finite horizon with terminal cost , and the optimal -stage cost is exactly . The survey of Arapostathis, Borkar, Fernández-Gaucherand, Ghosh and Marcus (SIAM J. Control Optim. 31 (1993), §6.1) states the link between the two notions as Theorem 6.2 and proves it on p. 317.
A controlled Markov process is a five-tuple :
A history is . An admissible policy is a sequence of stochastic kernels on with ; the class of all of them is . A stationary deterministic policy is a measurable map with . An initial state and a policy determine a probability measure on trajectories, with expectation . For a terminal cost and ,
denotes the bounded measurable real functions on . For and , the triplet is canonical if
Let , , and bounded on . Then is a canonical triplet if and only if, for all ,
and attains the infimum in both (6.6) and (6.7).
The result. Theorem 6.2 turns a statement about every finite horizon and every history-dependent randomized policy into two pointwise equations in and a pointwise selection condition on . A canonical policy is -stage optimal for every with terminal cost ; dividing (6.4) by shows that its average cost is . In the paper this is the entry point of Theorem 6.3, which shows that a canonical policy is strong average optimal and that is the optimal average cost, without any recurrence assumption. Equation (6.6) is the condition that makes behave as a constant in the optimization; when is constant it holds trivially, and Theorem 6.2 specializes to the bounded ACOE with a minimizing selector.
Formalizing it. The theorem is proved in the paper (and earlier by Yushkevich). This mission formalizes that proof on a general Borel model with history-dependent randomized policies and path measures built by the Ionescu-Tulcea theorem. Prove2Me has no formalization of the multichain coupled equations or of canonical triplets beyond finite models. The finite-horizon dynamic programming inequality of milestone 2, for policies that may use the whole history, is reusable in any finite-horizon or average-cost development on Borel spaces.
The algebra in the proof takes a few lines. The work is in two probabilistic facts that the paper uses without comment.
The first is the Markov decomposition of the -stage cost: conditioning on the first state–action pair turns the remaining stages into an -stage problem started from the next state. For a stationary policy the continuation is the same policy. For a history-dependent policy, the continuation is a policy that depends measurably on . Expressing this on the Ionescu-Tulcea measure is where the effort goes.
The second is the identity . On a Borel model, need not be measurable and the infimum need not be attained by a measurable selector. That is why the paper usually works with semicontinuous models (p. 288). Theorem 6.2 avoids the issue: only the inequality is needed, under the measurability that supplies, and the reverse direction is supplied by the given . A first attempt that proves the full identity for general Borel models runs into measurable selection problems that the theorem never needs.
BorelCMP S A has standard Borel S and Borel A, compact nonempty U x with measurable graph, a measurable cost c : S × A → ℝ with c ≥ 0 on K, and a Markov kernel P. c and P are total on S × A; only values on K enter. No continuity of c or P is assumed: Theorem 6.2 does not use Assumptions 2.2, 2.3 or 6.1.Policy M is the paper's : history-dependent, randomized, with admissibility . StationaryPolicy M is (measurable with ). The infimum ranges over all of Policy M. Restricting it to stationary policies would make sufficiency trivial and necessity false, and is not what the paper states.Kernel.trajMeasure at the first step, the shifted (continuation) policy and its measurability in the first state–action pair, and bounded-convergence bookkeeping for the Bochner integrals. These are reusable for every finite-horizon statement on this model. Proofs of the milestones are welcome independently. So are alternative proofs of the goal that bypass milestone 2 and argue directly with the canonical policy.In most control problems the controller does not see the state of the system. It sees noisy observations, remembers its past controls, and must act on that record. Inventory systems with delayed or inaccurate counts, maintenance of machines whose wear is only inspected, target tracking, and medical treatment planned from test results all have this form. The standard device for such problems is to replace the hidden state by a summary of the record, most often the conditional distribution of the state given the observations, and to solve a dynamic program whose state is that summary.
For finite or countable spaces this reduction goes back to Åström (1965) and Striebel (1965), who introduced the conditional distribution of the state as a "sufficient statistic" for control. Chapter 10 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996) carries it out for Borel state, control and observation spaces, with universally measurable policies and costs that are only lower semianalytic. In that generality the measurability of the reduced model is the whole difficulty, and the chapter isolates exactly what a summary must satisfy for the reduction to be exact.
The imperfect state information model (ISI) of Definition 10.3 has a nonempty Borel state space , control space and observation space ; a discount factor ; a lower semianalytic cost ; a Borel state transition kernel ; Borel observation kernels and ; and a horizon . The initial state has distribution , , and then , . The controller knows the information vector and must choose , where the constraint set is analytic.
A policy consists of universally measurable stochastic kernels that respect the constraints (Definition 10.4). Together with it determines probability measures on the histories , the cost
and the optimal cost (Definition 10.5). Assumption asks that the expected discounted negative part of the cost be finite for every policy and initial distribution; asks the same of the positive part.
A statistic is a sequence of Borel maps into nonempty Borel spaces. It is sufficient for control (Definition 10.6) if (a) the constraints can be read off from it, with analytic; (b) the conditional law of given is a Borel kernel , for every and every policy; and (c) the conditional expectation of given is a lower semianalytic function . The perfect state information model (PSI) of Definition 10.7 has states , constraints , costs and transitions ; its cost and optimal cost at are and . The initial distribution of is
A Markov (PSI) policy acts in (ISI) through .
Under or ,
and a Markov (PSI) policy that is optimal, -optimal or weakly --optimal for (PSI) is respectively optimal, optimal at , or -optimal at for (ISI); under an -optimal (PSI) policy is -optimal for (ISI). Here is weakly --optimal if when and otherwise, and -optimal if (Definition 10.8).
Proposition 10.3 says that an imperfect-information problem loses nothing by being solved in the reduced model: the optimal cost is the -average of the reduced optimal cost, and good reduced policies are good original policies. Combined with Proposition 10.6, every (ISI) model has such a reduction, so the finite-horizon dynamic programming theory of Chapter 8 (existence of -optimal policies, the dynamic programming algorithm) transfers to partially observed problems on Borel spaces. Proposition 10.4 turns this into a structural statement about the original problem: nearly optimal controllers need to retain only the statistic.
These results are proved in the book. None of them is formalized: the platform's related results (Bäuerle–Rieder's partially observable models with observation densities, and the linear-quadratic-Gaussian separation theorem) work in different models and do not cover universally measurable policies, analytic constraints, or lower semianalytic costs. A machine-checked version makes the conditional-expectation bookkeeping of the reduction explicit, and the definitions of this mission (universal measurability, lower semianalytic functions, the book's extended integral, history measures built from universally measurable kernels) are reusable by every other chapter of the book.
The obvious argument says: replace the state by the statistic, observe that costs and transitions depend only on the statistic, and conclude. In the Borel setting each step is a measurability claim that the naive argument does not supply. The conditions of Definition 10.6 are almost-everywhere statements about conditional distributions under every pair , while the reduced model needs genuine kernels; the policies are only universally measurable, so integrals and compositions must be taken with respect to completions; the costs take the values , so interchanging sums and integrals requires the finiteness assumptions and ; and the inequality requires producing, from an arbitrary history-dependent (ISI) policy, a Markov (PSI) policy with the same cost, which the naive argument does not do.
EReal with the book's convention written out explicitly (badd, bsum, extIntegral); Mathlib's EReal subtraction () is never used where both terms can be infinite.ProbabilityMeasure C that are measurable for the completion of every probability measure. History measures are characterized by their values on rectangles. Families indexed by the stage are indexed by all of ; only stages are constrained.Contributions are welcome on any milestone. Basic facts that a full development needs, such as composition of universally measurable maps (Proposition 7.44), measurability of integrals against universally measurable kernels (Proposition 7.46), and existence of the history measures (Proposition 7.45), can be posed and proved as supporting lemmas; they are reusable across the book.
A single-server queue in which customers arrive according to a renewal process and are served in exponentially distributed times is the system GI/M/1. Observed just before successive arrivals, its queue length is a Markov chain on , the imbedded chain introduced by D. G. Kendall (Kendall 1953, Ann. Math. Statist. 24, pp. 338–354). Whether this chain settles into a statistical equilibrium, keeps returning to the empty state without one, or drifts off to infinity is the first question asked about the queue, and every later quantity (stationary queue lengths, waiting-time distributions) presupposes the answer.
F. G. Foster's 1953 paper (Foster 1953) answers it for GI/M/1 and for M/G/1 by a different route from Kendall's direct analysis: it first proves general criteria, stated in terms of solutions of linear equations and inequalities in the transition matrix, for a countable Markov chain to be ergodic, recurrent or transient, and then checks them on the two queueing matrices. The criteria are of independent use; one of them (Theorem 2 of the paper) is now known as Foster's criterion, the starting point of the drift (Lyapunov-function) method for stability of Markov chains and queueing networks.
Timeline. Kendall (1951, J. Roy. Statist. Soc. B 13) studied queue-length processes directly, including a recurrence argument for M/G/1 that Foster's §3 reproduces; Kendall (1953) introduced the imbedded-chain method and, for GI/M/1, proved by it that is sufficient for ergodicity (Foster 1953, p. 359); Foster (1953) proved the full classification, ergodic iff and recurrent iff , by the general criteria. This mission treats the GI/M/1 half; a companion mission treats M/G/1.
A transition matrix on the states is an array of nonnegative reals whose rows sum to . For a state , is the probability that the chain started at returns to at some later step. The chain is recurrent if for every , transient if for every , and ergodic (recurrent-nonnull, positive recurrent) if moreover every mean recurrence time is finite. Foster's general theorems concern an irreducible chain (every state reachable from every state), assumed aperiodic for simplicity.
The GI/M/1 chain is described by a sequence of positive numbers with : is the probability that exactly services are completed between two arrivals. With the tails ,
that is , for , and for . In Lean this matrix is gim1Matrix a. The traffic parameter is defined through its inverse,
the mean number of service completions per interarrival interval (rhoInv a, and rho a ).
Together: ergodic for , recurrent-null for , transient for . The statement carries no constants and leaves the sequence free apart from positivity and normalization.
Milestones 2–4 are stated for a general irreducible aperiodic chain.
The classification tells exactly when the GI/M/1 queue is stable: the stationary distribution of the imbedded chain, which is geometric, exists precisely in the ergodic case , and for the queue grows without bound. Theorems 1 and 4 are general tools, reusable for any countable chain: Theorem 1 characterizes ergodicity by summable invariant vectors, Theorem 4 characterizes transience by bounded harmonic functions off one state. Theorem 7 is the extinction criterion of branching processes and recurs throughout applied probability.
All of these results are proved in the literature (Foster 1953; Feller's textbook for Theorem 7 and a version of Theorem 4). As far as a search of the platform shows, none of them has a machine-checked proof; the platform holds related special cases for the G/M/1 queue with a specific interarrival law (QueueingFundamentals.GM1.unique_root_unit_interval, open), but not the general lemma or the classification. A formalization would provide the general criteria as reusable library results and the first verified stability classification of a non-Markovian queue's imbedded chain.
The matrix is explicit, but none of the three properties is a finite computation: ergodicity and recurrence are statements about return times over all horizons, so each direction must go through an existence or nonexistence statement about infinite systems of equations. For the converse directions the obvious argument fails: exhibiting a candidate solution such as shows nothing until it is known that ergodicity forces every such solution to be summable, and showing that no bounded nonconstant solution of (7) exists when requires control of all solutions, not of one. The general criteria themselves rest on limit theorems for and on interchanging infinite sums, and the infinite-mean case has to be carried along everywhere.
QueueingFundamentals_Foundations_MarkovChain: TransitionMatrix (entries p, nonnegativity, rows summing to via HasSum), returnProb, meanRecurrenceTime, Irreducible, Aperiodic, PositiveRecurrent. "Ergodic" is PositiveRecurrent. IsRecurrent and IsTransient are defined state by state from returnProb; their complementarity for irreducible chains is a theorem, not a definition.TransitionMatrix whose entries equal gim1Matrix a; such a matrix exists for every admissible (rows sum to ), so the statement is not vacuous.ℝ≥0∞), with : an infinite mean gives , and that chain is ergodic.HasSum or Summable), so that a divergent series cannot satisfy an equation or inequality vacuously. In Theorem 1's sufficiency half the may be of either sign. In Theorem 7 the distribution is renamed to avoid a clash with .Infinite horizon dynamic programming asks for the least expected cost of controlling a stochastic system forever, and for a policy attaining it. On finite or countable state spaces the theory has been classical since Bellman, Blackwell (1965) and Strauch (1966). Many models in operations research, inventory control, queueing and economics have continuous states and controls, however, and there the Bellman equation raises a question the countable theory never meets: the optimal cost need not be Borel-measurable, so its expectation under the transition law, which the equation requires, may not be defined.
Bertsekas and Shreve (1978) settled this question by working with lower semianalytic cost functions and universally measurable policies. In that framework the optimal cost is always measurable enough to be integrated, and the optimality equation holds with no continuity or compactness assumption. Chapter 9 of their book treats the infinite horizon model under the three classical cost structures: nonnegative costs (P), nonpositive costs (N), and bounded discounted costs (D).
Timeline:
An infinite horizon stochastic optimal control model (SM) is an eight-tuple . The state space , the control space and the disturbance space are nonempty Borel spaces, that is, spaces homeomorphic to Borel subsets of complete separable metric spaces. The control constraint assigns to each state a nonempty set , and the set is analytic. The disturbance kernel is a Borel stochastic kernel and the system function is Borel. The discount factor is , and the one-stage cost is lower semianalytic: each sublevel set is analytic. The state moves by , with transition kernel .
A policy chooses at random from a universally measurable stochastic kernel concentrated on ; is the set of all policies. A policy is Markov if each depends only on , and it is stationary if, moreover, for all . Writing for the law of started from , the cost of and the optimal cost are
For , the dynamic programming operators are
The three cases are (P) on ; (N) on ; (D) and on for some real .
Under each of (P), (N) and (D),
The optimality equation is the basic structural fact of infinite horizon control. Corollary 9.12.1 uses it to construct optimal stationary policies from minimizers in the equation. The existence results for -optimal policies (Propositions 9.19 and 9.20), the convergence analysis of value iteration in Section 9.5, and the reduction of imperfect state information problems in Chapter 10 all build on it. It holds for arbitrary Borel models, with no continuity or compactness assumption.
All results of the mission were proved in 1978. None of them has a machine-checked proof: Mathlib has stochastic kernels and the Ionescu-Tulcea construction for measurable kernels, but no theory of lower semianalytic functions, universally measurable kernels, or dynamic programming on Borel spaces. A formal development would fix the measurability bookkeeping on which the textbook proofs rest and supply a reusable substrate for the stochastic control papers that cite this book.
Under (D), is a contraction on bounded functions, and its fixed point is the limit of value iteration. That argument, however, gives a fixed point only within a fixed class of measurable functions. Showing that this fixed point equals requires knowing that belongs to the class and that history-dependent randomized policies do no better. Under (P), value iteration can converge to the wrong limit (Example 1 of the chapter: while ). Even when each is Borel, may fail to be (Example 2). So cannot be obtained as a limit of the finite horizon equations, and the natural class of Borel functions is not closed under the partial minimization that defines .
The book's route lifts (SM) to a deterministic model on the space of probability measures , where no measurability restriction is needed, and transfers the results back. Making this transfer rigorous requires that the cost of a randomized policy be a measurable functional of its law, and that the infimum over policies preserve lower semianalyticity.
The draft fixes the following conventions.
AnalyticSet. A set is universally measurable if it is null-measurable for every probability measure.EReal. The book's convention is implemented explicitly, because Mathlib's EReal sets . The integral of an extended-real function is with the same convention.The goal admits a trivializing formalization that this draft rules out. is not defined as a fixed point of , nor as the limit of ; it is the infimum of the costs of all policies, which under (P) can differ from that limit.
A complete development needs universally measurable kernels and their compositions on product spaces, measurability of for universally measurable integrands, the measurable selection theorem of Jankov and von Neumann, and the closure of lower semianalytic functions under partial infimum. These are the subject of the series' mission on Chapter 7, and they are reusable for any stochastic control model on Borel spaces. Contributions are welcome at any level: these foundations, the Markov reduction (Proposition 9.1), or the case-by-case arguments.
Finite-horizon stochastic control on general state and control spaces — inventory levels, queue lengths, positions, beliefs — cannot be written down without measure theory, and the measure theory turns out to be the hard part. The dynamic programming (DP) recursion "start from zero and minimise one stage at a time" is easy to state, but on uncountable spaces the minimisation in each step produces functions that need not be Borel-measurable, and the infimum over policies has to be taken over a class large enough to contain near-minimisers. Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978; Athena reprint 1996) resolved this by working with universally measurable policies and lower semianalytic costs. Chapter 8 is the finite-horizon core of that theory, and the infinite-horizon results of Chapter 9 and the imperfect-information reduction of Chapter 10 are built on it.
Timeline. Blackwell (1965) treated discounted problems on Borel spaces with bounded costs and Borel policies, where ε-optimal Borel policies may fail to exist. Strauch (1966) studied positive and negative models. Blackwell, Freedman and Orkin (1974) introduced analytic sets and analytically measurable policies into DP. Bertsekas and Shreve (1978, Chapters 7–8) gave the universally measurable finite-horizon theory formalized here, including the unbounded-cost assumptions (F⁺)/(F⁻).
A finite horizon stochastic optimal control model is a nine-tuple . The state space , control space and disturbance space are nonempty Borel spaces (topological spaces homeomorphic to Borel subsets of complete separable metric spaces). The constraint is nonempty and is analytic in . Disturbances are drawn from a Borel stochastic kernel , the system moves by with Borel, the discount factor is a positive real, the one-stage cost is lower semianalytic ( is analytic for every real ), and is the horizon. The state transition kernel is .
A set is universally measurable if it is measurable for the completion of the Borel σ-algebra under every probability measure. A policy chooses from a universally measurable stochastic kernel concentrated on ; it is Markov if depends on only, and nonrandomized if every is a point mass. denotes all policies and the Markov ones. A policy and an initial distribution determine a probability measure on state–control paths, and the -stage cost and optimal cost are
Assumption (F⁺) requires , and (F⁻) requires , for every policy, initial state and stage, where is the marginal of on the -th pair. The DP operators are
under (F⁺) or (F⁻), where . The goal leaves the horizon, the discount factor and the sign of unrestricted beyond (F⁺)/(F⁻), and it compares an infimum over all history-dependent randomized policies with a pointwise recursion.
In attack order: Lemma 8.1 (the cost of a Markov policy equals ), Proposition 8.1 and Corollary 8.1.1 (Markov policies suffice), Lemma 8.2 (an ε-optimal universally measurable kernel for one application of ), Lemma 8.3 (under (F⁺), ), Lemma 8.4 (monotone and bounded convergence for ). Two consequences of the goal complete the chapter's existence theory: Corollary 8.2.1 ( is lower semianalytic) and Proposition 8.3 (ε-optimal nonrandomized Markov policies under (F⁺); nonrandomized semi-Markov and randomized Markov ones under (F⁻)).
Proposition 8.2 says the DP algorithm computes the true optimal cost of the Borel model, with no restriction to Markov or nonrandomized policies and with costs that may be unbounded in either direction. Corollary 8.2.1 identifies the regularity of the value function — lower semianalytic, possibly not Borel (Example 1 of Chapter 8) — and Proposition 8.3 turns the recursion into near-optimal policies. These results are the base case for the infinite-horizon theory of Chapter 9 (positive, negative and discounted models are analysed as limits of finite-horizon problems) and for the sufficient-statistic reduction of Chapter 10.
All results here are proved in the book. None is formalized: the platform has finite-state, finite-action DP theorems and Borel models with Borel-measurable policies, but no universally measurable policies, no lower semianalytic costs and no Ionescu-Tulcea construction for universally measurable kernels. The mission poses the finite-horizon Borel theory, with reusable infrastructure: the universal σ-algebra, universally measurable kernels, iterated path integrals representing integration against the induced path measure, and the operator calculus on extended-real functions with the convention .
The obvious argument fails at measurability. On countable spaces, Proposition 8.2 follows from the Part I argument: induct on , choose near-minimising controls state by state, assemble them into a policy. On Borel spaces, a pointwise choice of near-minimisers is not a policy unless it is measurable, and is generally not Borel even when and are; Borel policies are too few for -optimal ones to exist. The book's way out needs the selection theorem for lower semianalytic functions (Proposition 7.50), integration of universally measurable functions against universally measurable kernels (Propositions 7.45–7.46), and care with infinite values: without (F⁺) or (F⁻), the integral of the stage sum and the sum of the stage integrals can disagree, and Lemma 8.1 fails.
Lean conventions:
[TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [IsBorelSpace X] [Nonempty X]. IsBorelSpace is the book's Definition 7.7.EReal. Addition inside costs and integrands uses the book's convention (badd), not Mathlib's, which gives . Integrals are with (extInt).universalSigma). Kernels are universally measurable in the sense of Lemma 7.28(b).pathInt).A trivializing formalization is excluded by construction. is the infimum over all policies in , not over Markov or nonrandomized ones. is the integral of the stage sum against the path measure, never the operator composition of Lemma 8.1, so the goal does not collapse to the Part I result.
A complete development needs:
This infrastructure is reusable for the infinite-horizon Borel models (Chapter 9), for the imperfect-information reduction (Chapter 10), and for papers that cite this book. Contributions of these supporting lemmas as separate theorems are welcome.
Abstract dynamic programming, in the form developed by Denardo (1967) and Bertsekas (1977), studies sequential decision problems through a single monotone mapping : the cost of using control at state when the future is valued by the function . Chapters 2–5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), analyze this model when policies are arbitrary selectors and is defined on all extended-real functions on .
That generality breaks down as soon as the state and control spaces are uncountable. A stochastic control problem on Borel spaces needs measurable policies, so that the expected cost is an integral rather than an outer integral, and the functions on which acts must be measurable for the same reason. Chapter 6 of the book introduces a generalized abstract model in which the policies are drawn from a prescribed class and is only defined on a prescribed class of functions. The examples on p. 94 are the models of Part II: universally measurable policies with lower semianalytic costs (Chapters 8–9), analytically measurable policies (Section 11.2), and the semicontinuous models of Definitions 8.7–8.8. Chapter 6 is the bridge that lets the abstract results of Part I be invoked for these models.
The data are a state space , a control space , nonempty constraint sets , and three restricted classes: sets of functions , where is the set of all functions , and a set of selectors with . The mapping is monotone: in implies . For and ,
A policy is a sequence with every ; their set is . Given with , the -stage and infinite-horizon costs are
and the optimal costs are and . For a stationary policy write .
Five standing conditions tie the classes together: A.1 (every control is the value of some ), A.2 ( is closed under and under adding constants), A.3 ( is closed under every , , and under adding constants), A.4 (-minimizing selectors for , , exist in ), and A.5 ( and are closed under pointwise limits). Assumption asks for a closed subset of the space of bounded real functions with the sup norm , containing and invariant under on and under on , such that every exists and is real, each is -Lipschitz on , and every -fold composition is a -contraction on for some .
Under A.1–A.5 and : is the unique fixed point of in , with and ; each , , is the unique fixed point of in ;
a stationary is optimal iff ; and for every some stationary policy in satisfies .
In attack order:
The other results of Sections 6.2–6.3 are posed in the mission as separate theorems:
Proposition 6.4 is the statement that makes value iteration, Bellman's equation and stationary -optimal policies available for discounted problems whose admissible policies are restricted, for instance to measurable ones. Without it, each measurable model would need its own fixed-point argument. The finite-horizon Propositions 6.1–6.3 play the same role for the dynamic programming algorithm , and their hypotheses (, exact selection) are exactly what Chapters 7–8 verify for universally measurable policies.
The book states Propositions 6.4 and 6.5 without proof (p. 97), referring to the proofs of Chapter 4; Propositions 6.1–6.3 are justified by "nearly verbatim repetition" of Chapter 3. A formalization therefore supplies proofs that are only indicated in print, and checks that A.1–A.5 really suffice for each step of the Chapter 3–4 arguments. None of these results has a machine-checked proof that we know of; the companion missions of this series formalize the unrestricted special case (, ) of Chapters 3 and 4.
The Chapter 4 proof of Proposition 4.2 applies the contraction mapping theorem to on . Here the obvious transcription fails at two points. First, maps into itself but only maps into itself, so the fixed-point theorem must be applied on two different sets, and these are closed only because of A.5. Second, every argument that picks a near-minimizing selector at each state must produce a selector in : pointwise choices are no longer allowed, and A.1, A.4 and the exact selection assumption are the only sources of admissible selectors. Proofs of Chapter 3–4 that build a policy state by state cannot be copied.
Functions on are S → EReal. is a total Lean function, but monotonicity is assumed only on and every statement evaluates only at functions of . is limUnder; Assumption makes the limit exist. is Mathlib's ; a bound between extended-real functions means both are real everywhere and , which is how the book's convention reads a norm of a difference. No statement adds values of opposite infinite sign, so Mathlib's EReal addition agrees with the book's wherever it is used. and are infima over only, the -optimality notions keep the book's two-case form at , and is a positive integer.
The chapter collapses to Chapters 3–4 if or is built in; here , and are arbitrary and constrained only by A.1–A.5, and is never defined as a fixed point.
A complete development needs the -step contraction mapping theorem on a closed subset of , monotonicity lemmas for and , and the restricted-class versions of Propositions 3.1–3.4 and 4.1–4.4. These are reusable for the Borel models of Chapters 8–9. Proofs of any milestone, and sorry-free lemmas about the Assumption contraction, are welcome.
The maximum flow problem asks how much of a commodity can be shipped from a source to a sink through a network whose arcs have limited capacities. L. R. Ford, Jr. and D. R. Fulkerson's 1956 paper Maximal Flow Through a Network proved the minimal cut theorem: the largest flow value equals the smallest total capacity of a set of arcs that separates source from sink. That theorem is formalized in the companion mission Maximal Flow Through a Network I.
The second section of the same paper treats a special class of networks, those that remain planar after an arc from source to sink is added. For these networks the paper shows that one particular source–sink chain crosses every minimal separating set exactly once. This structural fact turns the minimal cut theorem into a simple computing procedure: repeatedly push as much flow as possible along such a chain and delete the arcs it saturates. The paper notes that G. Dantzig had conjectured, before the minimal cut theorem was proved, that this procedure yields a maximal flow on planar networks. The same "uppermost path" idea underlies later algorithms for maximum flow in planar graphs with source and sink on a common face (Itai and Shiloach, 1979).
The statement is short and purely combinatorial in its conclusion, but its hypothesis is topological. This mission isolates that theorem.
A network has a finite set of vertices and a finite set of arcs. Each arc joins two distinct end vertices, written and ; arcs carry no direction, and two arcs may join the same pair of vertices. Two distinct vertices are distinguished, the source and the sink , and each arc carries a positive capacity (capacities play no role in the target below).
A chain joining and is a set of distinct arcs that can be arranged as with , , and the vertices pairwise distinct; each arc may be traversed in either direction. The empty set is the null chain from to .
A set of arcs is a disconnecting set if every chain joining and contains an arc of . A disconnecting set none of whose proper subsets is disconnecting is a cut.
The network is ab-planar if the graph of , together with one additional arc joining and , can be drawn in the plane without crossings: vertices go to distinct points of ; each arc, including the added arc , goes to an injective continuous path between the points of its end vertices; no arc passes through a vertex other than its ends; and two distinct arcs meet only at endpoints of both. In Lean the drawing is the structure ABPlaneDrawing N, and is ab-planar when Nonempty (ABPlaneDrawing N). The section's standing assumption is that no arc of already joins and .
If is ab-planar, no arc of joins and , and some chain joins and , then
This is FordFulkerson56.Planar.ab_planar_exists_chain_meeting_each_cut_once. "Precisely once" is exact cardinality one, neither "at least once" (true of every chain) nor "at most once".
For every network , every cut and every arc , there is a chain joining and with . No planarity is involved; the statement is what the minimality of a cut provides to the proof.
In the "gas, water, electricity" graph with the arc removed, every chain joining and meets some cut in three arcs. This network is not ab-planar, so the example shows that the planarity hypothesis of Theorem 2 cannot be dropped.
Theorem 2 and the minimal cut theorem together give the paper's procedure for planar networks: if meets every cut once, then imposing a flow on lowers the value of every cut by exactly , so the minimal cut value, and hence the maximal flow value, drops by . Saturated arcs can then be deleted and the step repeated. Without the "exactly once" property the reduction could overshoot the cut structure, and the greedy step would not be justified. The theorem is also one of the earliest instances of the link between planarity and cut structure that later underlies planar duality arguments for minimum cuts.
The result has been known since 1956 and is not open. No machine-checked version is recorded on the platform, and Mathlib, at the pinned revision, has neither planar graphs nor the Jordan curve theorem. A formal proof would be the first formalized statement about source–sink planar networks in this library, and the counterexample item records, as a checkable fact, that the hypothesis is necessary.
The conclusion is combinatorial while the hypothesis is a drawing in . The paper's proof normalises the drawing (the added arc on the outer boundary, the graph in a vertical strip with on the left line and on the right), selects the "top-most" chain from to , and argues that a chain meeting a cut below the top-most chain must cross another such chain. Each of these steps rests on plane topology: the existence of the outer region, the meaning of "top-most", and the fact that two chains with interleaved endpoints on a boundary must intersect, which is a form of the Jordan curve theorem.
The naive purely combinatorial route fails: the analogous statement for arbitrary networks is false (Fig. 2), so any argument has to use the drawing somewhere. Replacing the drawing by a combinatorial embedding (rotation systems, faces) is possible but then requires proving that the two notions agree, which is again Jordan-curve territory.
Conventions committed to in the Lean statements:
V, E with decidable equality. Arcs are undirected, may be parallel, and have two distinct end vertices. Source and sink are distinct, capacities are positive (structure Network).Finset E that is the arc set of some arrangement as a simple path (IsChainWalk, IsChain); the null chain is allowed.IsDisconnecting and IsCut quantify over all chains joining source and sink; a cut is a disconnecting set no proper subset of which is disconnecting.none : Option E, with injective Paths in ℝ × ℝ as arcs.Hypotheses of the goal: hno_ab, the standing assumption of §2 (no arc joins and , p. 403); hconn, that some chain joins and . The second is not stated in the paper; its proof starts from "the chain joining a and b which is top-most", which presupposes one, and without it the statement is false (if and are disconnected, the empty set is a cut and no chain exists).
The drawing structure is satisfiable (a three-vertex path network has an explicit drawing), so the planarity hypothesis is not vacuous; and it covers the added arc and all crossings, so minus is not ab-planar and the goal is not refuted by the paper's own example. A formalization that dropped the arc from the drawing, or quantified over disconnecting sets instead of cuts, would state a false theorem and is ruled out.
A complete development needs basic plane topology for paths in (a Jordan-curve-type separation lemma for simple closed curves, or an equivalent statement about crossing paths in a strip), together with combinatorial lemmas about chains (concatenation and shortcutting of chains at a common vertex). The topological lemmas are reusable well beyond this mission. Proofs through a combinatorial embedding are welcome, provided the equivalence with ABPlaneDrawing is proved.
A robust Markov decision process (robust MDP) evaluates a policy against the worst transition kernel and reward in an uncertainty set around a nominal model . It is the standard model for planning when the dynamics are estimated from data (Iyengar 2005; Nilim and El Ghaoui 2005; Wiesemann, Kuhn and Rustem 2013). Its Bellman update contains an inner optimization over the uncertainty set at every state, which makes robust planning costly when the sets are not -rectangular.
Derman, Geist and Mannor (arXiv:2110.06267, NeurIPS 2021) show that, for -rectangular ball uncertainty sets, this inner optimization can be replaced by an explicit penalty that depends both on the policy and on the value function. The resulting twice regularized (R²) MDPs have Bellman operators with no inner optimization over models. The first mission of this series formalizes the robust–regularized equivalence (Theorem 4.1 of the paper). This mission formalizes Section 5: the R² Bellman operators are monotone and contracting under a bound on the transition radius, and the greedy policy of the R² optimal value is optimal.
Let and be finite nonempty sets of states and actions, a discount factor, a transition kernel and a reward. A policy assigns to each state a probability distribution on . For write and
All norms below are -norms, ; is the sup norm.
Fix nonnegative radii for each state. The R² regularizer is , and the R² Bellman operators are
A policy is greedy for when .
Assumption 5.1 (bounded radius). For each there is with
and . The R² value function of a policy and the R² optimal value are the fixed points of and .
Under Assumption 5.1, and every have unique fixed points; a greedy policy for exists, and every such policy satisfies
every optimal policy is greedy; and when for all the greedy policy is unique, hence the unique optimal R² policy.
Theorem 5.1 is the R² counterpart of the fundamental theorem of discounted dynamic programming: optimal R² values are achieved by stationary policies obtained by a single greedy step. Together with the contraction of Proposition 5.1 (iii) it justifies the R² modified policy iteration algorithm of the paper, whose greedy step is a projection onto the simplex rather than a robust max–min problem. Combined with the first mission of the series, which identifies the robust value of an -rectangular ball-constrained MDP with the optimum of an R²-regularized program, it gives a route to robust planning at the cost of regularized planning.
The results are proved in the paper (App. C), partly by reference to Geist, Scherrer and Pietquin (2019) for the optimality operator. No machine-checked proof of any of them exists; this mission produces the first. Prop. 2.1 is a general fact of convex analysis (Danskin-type smoothness of a conjugate on the simplex) that is reusable for any regularized MDP or entropy-regularized game.
The R² evaluation operator is not affine: the value regularizer is concave in and decreases as grows. Monotonicity therefore does not follow from the positivity of as in the standard case; it requires the second bound of Assumption 5.1, which compares the variation of with the minimal nonnegative bilinear form of . Likewise the contraction modulus is not but , because the regularizer is -Lipschitz between the and sup norms. The optimality step of the classical proof uses linearity of when comparing values of policies; here only monotonicity and contraction are available. Uniqueness of the greedy policy rests on strict concavity on the simplex, which holds only when the regularization weight is positive.
States and actions are finite nonempty types; transitions are arrays P₀ : S → A → S → ℝ with the published predicate IsTransitionKernel; value functions are S → ℝ with the pointwise order. The -norm is an explicit l2norm (Mathlib's norm on S → ℝ is the sup norm, used only for ). is the real supremum over the simplex (attained), and the inner minimum of Assumption 5.1 is the real infimum over nonnegative -unit vectors; the witnesses are explicit. Greedy policies are a predicate, never a function, and the R² value functions are not defined by choice: the goal asserts their existence and uniqueness and speaks about the fixed points.
Disclosed deviations from the page. Assumption 5.1 is a hypothesis of Theorem 5.1 (its proof assumes it). The uniqueness clause of Theorem 5.1 additionally assumes for all : with one state, two actions, zero reward and zero radii every policy is greedy and optimal. Proposition 2.1 assumes continuous on the simplex, without which the maximum need not be attained, and strong convexity is Mathlib's StrongConvexOn for some modulus (norm-independent in finite dimension). Proposition 5.1 (ii) is false as printed and is not drafted: with one state, one action, , , , , , , one has , and , give . Remark 5.1, Algorithm 1 and the variant of App. C.1 are out of scope. The inner minimum of Assumption 5.1 is whenever some , forcing ; this is the assumption as printed.
A formalization in which is the sup norm, the inner minimum ranges over all unit vectors (making the assumption unsatisfiable), or the value functions are postulated rather than shown to exist would be trivial or wrong; the drafted statements avoid all three. Contributions welcome: Prop. 2.1 as a general convex-analysis lemma, Banach fixed-point plumbing for S → ℝ with the sup norm, and the strict concavity of on the simplex.
A disjunctive normal form (DNF) is a disjunction of terms, each term a conjunction of Boolean literals. An unambiguous DNF has pairwise disjoint terms: no Boolean assignment satisfies two different terms. This restriction makes several tasks easy. In particular, the cited open-problem entry records polynomial-time algorithms for weighted satisfiability on unambiguous DNFs and for unweighted falsifiability. The unresolved boundary is weighted falsifiability: can one find a high-weight assignment outside the union of the terms, without enumerating all assignments?
This question is relevant to the complexity of negating compact representations of Boolean functions. Amarilli's entry observes that, since unambiguous DNFs are d-DNNFs, a polynomial-time negation procedure for d-DNNFs would yield a polynomial-time solution to weighted falsifiability on unambiguous DNFs by applying weighted satisfiability to the negated representation. Conversely, if weighted falsifiability for unambiguous DNFs—or even for d-DNNFs—is NP-hard, then, unless , d-DNNFs cannot be negated in polynomial time. These are implications stated by the source, not results established by this mission.
The question appears on Albertine Amarilli's open-problem list. The entry cites a Theoretical Computer Science Stack Exchange question by Mikaël Monet and credits him with helping prepare the entry. It records two partial tractability results: weighted satisfiability with binary weights, and weighted falsifiability when the variable weights are unary. The entry gives no date for when the problem was posed or last seen open, so this description does not assign one. The linked discussion is useful context, not a novelty or resolution certificate.
Let be exactly the variables occurring in the DNF. The formal input declares this finite universe by its size ; validity requires every declared variable to occur in at least one literal. An input DNF is a finite list of terms, and each term is a finite list of signed variable indices. An assignment is a function . A positive literal is true when ; a negative literal is true when . A term is true when all its literals are true, and the DNF is true when at least one term is true. Thus the empty DNF is false and an empty term is true.
The input also contains one positive integer weight for each variable and a positive threshold . The weight of an assignment is
The DNF is valid for this problem when every literal index is below and every pair of distinct terms is mutually unsatisfiable. The decision question is whether there exists an assignment that falsifies the DNF and has weight at least .
For valid unambiguous DNF inputs with positive binary-encoded weights and threshold, the decision problem asking whether a satisfying assignment has weight at least has a deterministic polynomial-time algorithm. This is the weighted-satisfiability baseline recorded in the source entry. It is a separate result from the goal below.
For the same valid DNF model, when each variable weight is encoded in unary, weighted falsifiability has a deterministic polynomial-time algorithm. The threshold remains binary-encoded in this formalization. The source entry records this unary-weight restriction as tractable.
For arbitrary positive binary-encoded variable weights and a positive binary-encoded threshold, determine whether one fixed deterministic Turing machine and one polynomial time bound decide weighted falsifiability for every valid input. The machine must be correct on all valid instances; its running-time bound is uniform and measured in the length of the explicit input code. No witness output is required.
The two partial results are reference points, not assumptions from which the goal is claimed to follow. The goal is the open binary-weight case; it must not be replaced by the satisfiability problem or by the unary-weight restriction.
Input, semantics, validity, and serialization definitions
├── binary-weight weighted satisfiability (source baseline)
├── unary-weight weighted falsifiability (source baseline)
└── binary-weight weighted falsifiability (open goal)
Each branch shares the same finite DNF model and correctness predicates. The arrows indicate required definitions and scope, not a claim that either partial theorem implies the open goal.
A positive result would give a uniform algorithm for finding whether a disjoint union of Boolean subcubes omits any sufficiently heavy point, even when weights are represented compactly in binary. A negative complexity result would identify a sharp obstruction to efficient complement-related operations on these representations. The exact-weight version (asking for weight exactly ) is a different problem and is outside this mission's scope; the goal here is specifically weight at least .
Formalizing the question fixes the universe of variables, signed-literal semantics, unambiguity condition, threshold direction, input encoding, and computational model. It also makes the unary and satisfiability baselines comparable to the binary-weight goal without treating a finite search or a candidate implementation as a complexity proof. No solution is supplied or presumed here.
The direct search over all assignments is exponential in . Counting satisfying assignments is enough to settle ordinary falsifiability, but a weighted threshold partitions assignments by exponentially many possible total weights when the weights are binary. The unary dynamic program therefore does not by itself give a polynomial bound in the binary input length. Conversely, solving weighted satisfiability on the DNF does not answer whether a heavy assignment lies outside it. The task is to settle that gap without silently replacing binary magnitude by unary size.
The Lean model uses Input, an explicit variable count, a list of signed-index terms, a weight list, and a threshold. validInput requires exactly one positive weight per variable, positive weights and threshold, in-range literal indices, that every declared variable occurs in the formula, and pairwise unsatisfiable distinct terms. The finite assignment type is Fin n → Bool; unused variables remain part of the input. The decision predicate is existential and exact.
The binary code includes the variable count, every list count and delimiter, all signed indices, all weights, and the threshold. Natural-number payloads use canonical binary digits with an explicit unary length prefix. The unary-weight code changes only the variable-weight payloads to unary; formula data and threshold remain binary. The complexity statements use Mathlib's bundled deterministic Turing.TM2ComputableInPolyTime model, with a single machine and polynomial bound in the chosen code length. This formalization does not claim refinement to JSON, CPython, or any runtime implementation. Human review should check the encoding/decoder round-trip and the source correspondence before launch.
The reusable definitions are the finite DNF semantics, weighted assignment score, validity predicate, binary/unary encoders, and exact decision predicates. Formalizing the two cited partial results is part of the mission's milestone path; neither is evidence that the binary-weight goal is solved.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's earlier values ( down to ) came from Schnirelmann's method with every constant written out. Those arguments stall near because the medium range relies only on a Chebyshev lower bound for . This entry adds the small-shift idea of Riesel and Vaughan, which removes that bottleneck without any zeta-zero input.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in.
Let and . We show , then conclude with Mann's theorem as in the entry. Write for the scale.
The argument stays elementary: no prime number theorem and no zeros of or -functions. New reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Already proved on the platform: Schnir.sieve_ineq, Schnir.G_lower, Schnir.pi_lower, Schnir.basis_of_density. Mathlib supplies the Chebyshev bounds (Chebyshev.psi_ge', Chebyshev.theta_le_log4_mul_x) and the Λ² sieve framework (Mathlib.NumberTheory.SelbergSieve).
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's earlier values ( down to ) came from Schnirelmann's method with every constant written out. Those arguments stall near because the medium range relies only on a Chebyshev lower bound for . This entry adds the small-shift idea of Riesel and Vaughan, which removes that bottleneck without any zeta-zero input.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in.
Let and . We show , then conclude with Mann's theorem as in the entry. Write for the scale.
The argument stays elementary: no prime number theorem and no zeros of or -functions. New reusable components:
The Lean statement is the campaign template verbatim with in place of the value. Already proved on the platform: Schnir.sieve_ineq, Schnir.G_lower, Schnir.pi_lower, Schnir.basis_of_density. Mathlib supplies the Chebyshev bounds (Chebyshev.psi_ge', Chebyshev.theta_le_log4_mul_x) and the Λ² sieve framework (Mathlib.NumberTheory.SelbergSieve).
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's first proved value, , came from Schnirelmann's method with every constant written out. This entry records a sharper value, , from the same elementary circle of ideas.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in. The argument proves the stronger statement that every odd is a sum of exactly primes; the at-most form for all odd follows.
It follows the companion entry, with every parameter pushed to the limit of the same tools. Let and . We show :
About is the floor of this method: the medium range relies on the Chebyshev constant , which forces the sieve threshold below and so inflates the sieve coefficient.
The bound is far weaker than Tao's or Helfgott's , but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization. Reusable components:
The Lean statement is the campaign template verbatim with in place of the value. All the ingredients above except the moment bound and the final assembly are already proved on the platform (Schnir.sieve_ineq, Schnir.G_lower, Schnir.pi_lower, Schnir.basis_of_density).
Iterative methods for optimization and equation solving on a smooth constraint set (orthogonal matrices, fixed-rank matrices, spheres, Stiefel and Grassmann manifolds) compute an update vector in the tangent space at the current iterate and then have to return to . The Riemannian exponential map does this along geodesics, but computing it means solving an ordinary differential equation. The notion of retraction, introduced by Adler, Dedieu, Margulies, Martens and Shub (IMA J. Numer. Anal., 2002) and developed in the book of Absil, Mahony and Sepulchre (Princeton, 2008), captures what such a return map needs for Newton's method to keep its local quadratic convergence and for gradient methods to converge: smoothness, , and first-order agreement with the exponential.
Absil and Malick (SIAM J. Optim., 2012; HAL hal-00651608v2) give a general recipe for building retractions on submanifolds of a Euclidean space: move tangentially from to , then come back to along a prescribed family of admissible directions. This mission formalizes that recipe, Theorem 4.2 of the paper ("retractors give retractions"), together with the two lemmas its proof rests on.
Let be a Euclidean space of dimension (in the paper's examples, with the Frobenius inner product). A set is a submanifold of dimension if around every it is a coordinate slice: there are an open neighbourhood of and a diffeomorphism of onto an open subset of with . Throughout, .
The tangent space is the linear subspace of of tangent directions of at , the normal space is its orthogonal complement, and the tangent bundle is .
A map from to is a retraction around (Definition 2.1) if, on a neighbourhood of in , it is of class , satisfies , and has derivative at . It is a retraction on if this holds around every point.
A retractor (Definition 4.1) is a map , defined on a neighbourhood of the zero section of , with values in the Grassmann manifold of -dimensional linear subspaces, such that for every . Given , set and let
The theorem asserts both that the point-to-set map is single-valued near the zero section and that it is a retraction there.
Near there is one and only one smallest with ; ; and is a retraction around , hence on .
On a neighbourhood of the zero section, for a unique linear depending on .
If and for all , then for all .
Theorem 4.2 reduces the construction of a retraction to the choice of a smooth field of subspaces transverse to the tangent space at . The orthographic retraction () and the projective retraction () are both instances, as are the gnomonic, orthographic and stereographic projections on the sphere. Theorem 4.9 then certifies, by a check at only, that a retraction agrees with the exponential to second order, which matters for the superlinear convergence of Riemannian trust-region and Newton methods. Lemma 4.7 goes beyond an earlier result on tangential parameterizations (reference [28, Th. 3.4] of the paper) by giving regularity jointly in , not only in (Remark 4.4 of the paper).
The results are proved in the paper. None of them is machine-checked: Mathlib has the implicit function theorem and smooth manifolds, but no embedded submanifolds of a Euclidean space with their tangent and normal bundles, no retractions, and no smooth Grassmannian-valued maps. The work here is to formalize the known proof and to build this layer, which every later mission of this series (projective, spectral, fixed-rank and Stiefel retractions) also needs.
The statement is an implicit-function argument, but the obvious one does not apply directly. The unknown lives in the normal space , which moves with , and ranges over the tangent bundle, a submanifold of rather than an open set of a vector space. The equation has to be read in charts of the bundle, which costs one derivative; the uniqueness given by the implicit function theorem holds only locally in , and turning it into "the smallest ", or "the nearest point of ", requires excluding far-away intersection points. For a general retractor, the subspace also moves, and has to be written as a graph over the normal space with a dependence before a second implicit-function argument applies.
is a finite-dimensional real inner product space E, is Module.finrank ℝ E, and are natural numbers with and (the latter inside the submanifold definition). The coordinate slice uses an open partial homeomorphism E → EuclideanSpace ℝ (Fin n), in both directions, with 0-based coordinates. is the span of Mathlib's tangent cone (chart-free), its orthogonal complement. Retractions and retractors are total maps on constrained only on with open; "of class on a subset of " is ContDiffOn on that set. A Grassmannian-valued map is when its orthogonal projector is, and the dimension of is part of the definition. The set-valued uses the published nearest-point predicate RandomGradFree.Nonsmooth.IsMetricProjection. In Lemma 4.8, is extended by on so that it is an operator on . Theorem 4.9 assumes , the standing assumption of the definition of second-order retractions (display (2.3)), and reads the page's "" as for all .
The goal is not satisfied by exhibiting some retraction: it requires the nearest-point set to equal a singleton (so it is nonempty) and that very to be a retraction. Theorem 4.9 requires the curve to be twice differentiable, so a junk second derivative of does not satisfy it.
A complete development needs: finite-rank facts for tangent spaces of slices (), smoothness of , charts of and of the Whitney sum , ContDiffOn on submanifolds, and local orthonormal frames of a smooth field of subspaces. All of these are reusable beyond this mission. Contributions to any of them, and proofs of the two lemmas, are welcome.
Many optimization algorithms are discretizations of a continuous-time descent: the gradient flow for smooth objectives, and its nonsmooth analogue, the subgradient dynamical system, for objectives with kinks or constraints. A basic question about such a flow is whether a bounded trajectory actually converges, rather than merely accumulating on a continuum of critical points, and how fast. For real-analytic this was settled by Łojasiewicz through his gradient inequality, which forces bounded gradient trajectories to have finite length. Without some such structure the answer is negative: there are smooth functions whose bounded gradient trajectories spiral forever around a circle of critical points.
Bolte, Daniilidis and Lewis (SIAM J. Optim. 17 (2007) 1205–1223) extended the Łojasiewicz inequality to nonsmooth subanalytic functions, possibly taking the value , by replacing with the least norm of a limiting subgradient. Section 4 of the paper turns this inequality into convergence results for subgradient trajectories of convex and lower- functions. This mission formalizes that section. The same "Łojasiewicz argument" later became the Kurdyka–Łojasiewicz framework behind convergence proofs for proximal, alternating and splitting algorithms (Attouch–Bolte 2009; Bolte–Sabach–Teboulle 2014).
Timeline. Łojasiewicz (1963, 1984) proved the gradient inequality for real-analytic functions and finite length of bounded analytic gradient trajectories. Kurdyka (Ann. Inst. Fourier 1998) extended it to functions definable in an o-minimal structure. Kurdyka, Mostowski and Parusiński (2000) proved Thom's gradient conjecture for analytic functions. Bolte, Daniilidis and Lewis (2007) gave the nonsmooth subanalytic version and the trajectory results formalized here.
Let with domain . The Fréchet subdifferential is the set of with . The limiting subdifferential is the set of limits of with and . The nonsmooth slope is , equal to when , and is the set of critical points.
The standing assumptions of Section 4 are:
A trajectory of the subgradient system is an absolutely continuous curve , , with for almost every and for every . It is maximal if it admits no extension to a longer interval. The Łojasiewicz inequality holds around with exponent if is bounded near , with and . A Łojasiewicz exponent at is any such .
Under –, every bounded maximal trajectory is defined on and converges to a critical point . For every Łojasiewicz exponent at there are and such that for
and for , for all large . The constants are existential, so the goal survives any later sharpening of them.
Theorem 4.5 says that for convex or lower- subanalytic objectives, including constrained problems through indicator functions of subanalytic sets, the subgradient flow never oscillates indefinitely: bounded trajectories converge to one critical point. Theorem 4.7 adds rates that depend only on the Łojasiewicz exponent at the limit: exponential at , polynomial above it, finite time below it. These are continuous-time templates for the convergence analyses of proximal and splitting methods under the Kurdyka–Łojasiewicz property.
On the formalization side, the results are proved on paper but, to our knowledge, not formalized in any proof assistant. A development would provide reusable infrastructure: a Lean notion of a trajectory of a differential inclusion on , a chain rule for along absolutely continuous curves, and a comparison lemma for the differential inequality . The analysis of Section 4 uses subanalyticity only through inequality (20), so Theorems 4.5 and 4.7 can be attacked with (20) as an imported milestone, independently of the subanalytic geometry.
Compactness gives cluster points of a bounded trajectory, and the decrease of gives convergence of . Neither gives convergence of . The usual first idea, that forces convergence, fails, since square-integrable speed allows infinite length. The difficulty is to control rather than . That needs a lower bound on the slope in terms of the function gap near the cluster point, which is exactly what (20) supplies, plus a trapping argument showing the tail of the trajectory stays in the ball where (20) holds. In the nonsmooth setting the chain rule itself is nontrivial: is differentiable almost everywhere with derivative for every , which relies on for convex and lower- functions. Global existence on (Corollary 4.1(iii)) must also be established before any asymptotic statement makes sense.
Space is EuclideanSpace ℝ (Fin n). Functions take values in EReal; "bounded from below" by a real number excludes . The limiting subdifferential is the published NonconvexSplitting.Shared.LimitingSubdiff, and convexity is the published MoreauProx.Characterization.EConvex (convex epigraph). The slope is valued in . The Łojasiewicz inequality is encoded as for near and every , which is the bounded ratio under the paper's conventions. Times are real numbers and . Curves are functions whose values outside are irrelevant. "Absolutely continuous on " means absolutely continuous on every compact . Velocities appear only "for almost every ". Lengths are lower Lebesgue integrals in , never Bochner integrals (which would vanish for a non-integrable speed).
Two trivializations are ruled out. Maximality is a hypothesis and is a conclusion: assuming would narrow the theorem, and dropping maximality would make it false. Rates are claimed for every Łojasiewicz exponent at the limit, not for one chosen exponent. Corollary 4.1(iii) is stated as "defined on with ", because the printed would fail for any trajectory with nonzero limit.
Needed infrastructure: absolutely continuous curves and their a.e. derivatives (Mathlib's AbsolutelyContinuousOnInterval), chain rules for convex and lower- functions, existence and uniqueness for monotone differential inclusions (Brézis), and an ODE comparison principle. Contributions to any of these are reusable well beyond this mission.
This mission formalizes A. Connes, J. Feldman and B. Weiss, An amenable equivalence relation is generated by a single transformation, Ergodic Theory Dynam. Systems 1 (1981) 431–450 (doi:10.1017/S014338570000136X).
A countable group acting on a measure space partitions it into countable orbits, and much of ergodic theory studies actions only through this orbit equivalence relation. The simplest relations are those of a single transformation, the orbits of an action of . Connes, Feldman and Weiss characterize exactly which relations are of this kind, up to null sets: the amenable ones, those carrying an invariant mean. Since the orbit relation of any action of a countable amenable group is amenable, every such action is orbit equivalent to an action of . The same theorem gives the uniqueness of Cartan subalgebras in hyperfinite von Neumann algebras.
On this platform it is the missing link in the Lodha–Moore mission, which passes between Lodha and Moore's definition of a -amenable relation (an orbit relation of off a null set) and the invariant-mean definition of the Monod bundle: one direction is proved, the other (LodhaMoore.isMuAmenable_of_isAmenableRel) is this mission's goal in Lodha and Moore's language.
Timeline.
is a standard Borel space with a -finite measure . A discrete measured equivalence relation (IsDiscreteMeasured μ R) is a Borel equivalence relation whose classes are countable and for which is quasi-invariant: the saturation of a null Borel set is null.
carries the measure , the counting measure on the class of (relMeasure), and the module , the density of against its image under (module). A partial transformation of is a Borel bijection between Borel subsets of whose graph lies in (Monod.PartialTransformation).
is amenable (Monod.IsAmenableRel) when it has a left invariant mean: a positive normalized map from bounded functions on to bounded functions on with for every partial transformation (Definitions 5–6). is of type I (IsTypeI) when, off a null saturated set, its quotient is a standard Borel space, and hyperfinite (IsHyperfinite) when, off a null set, it is a countable increasing union of type I equivalence relations (Definition 1). A finite subequivalence relation (IsFiniteSubrelation) is a Borel that is an equivalence relation with finite classes on .
For amenable there are a non-singular Borel automorphism of and a null set with
The result. Theorem 10 turns amenability, which is usually easy to check, into hyperfiniteness, which is the structure one wants: for instance, the action of on the projective line, or of any discrete group on with amenable, is generated by a single transformation. On this platform it closes the open direction, LodhaMoore.isMuAmenable_of_isAmenableRel, and with it Lodha and Moore's Theorem 2.1.
Formalizing it. No machine-checked proof of the theorem exists, in Mathlib or elsewhere as far as a search finds; Mathlib has no theory of countable Borel equivalence relations. A complete development builds that theory from the descriptive set theory Mathlib has.
The theorem is about relations without a group. The obvious route, through a countable group generating and an amenability of that group, is unavailable: the orbit relation of a nonamenable group, such as acting on the projective line, can be amenable, and there is no group whose Følner sets one could use. The Følner sets of Lemma 8 have to be produced from the invariant mean on the relation itself, which needs duality between and and convexity arguments. Underneath, even the basic facts used in §§1–3 (that is a countable union of graphs of Borel automorphisms, that is a measure, that saturations of Borel sets are Borel) rest on the Lusin–Novikov uniformization theorem, which is not in Mathlib. It is published here as standalone theorems: a Borel set with countable sections is a countable union of Borel graphs, and a countable-to-one Borel map is injective on countably many Borel pieces covering its domain.
All statements carry the hypotheses of §1: standard Borel (StandardBorelSpace), -finite, a Borel equivalence relation with countable classes and quasi-invariant. Lemmas 8 and 9 take a probability measure, as the paper's proof of Lemma 9 does. “Up to a null set” is read as “off a -null Borel set of points”, which by quasi-invariance agrees with the paper's -null sets. Amenability is the published Monod definition, an invariant mean on bounded measurable functions modulo null sets; it is not trivial (the relation of for a countable dense subring of is not amenable, Monod.not_isAmenableRel_mob).
The definitions are in the definition bundle ConnesFeldmanWeiss. Reusable beyond this mission: the Feldman–Moore theorem and the basic theory of countable Borel equivalence relations, both welcome as standalone theorems.
What is left out. Proposition 7 and Corollary 11 need the von Neumann algebra of a relation and its Cartan subalgebras, which Mathlib does not have. The final part of the paper (Lemma 15 to Corollary 21) treats relations with uncountable classes through transverse functions, including foliations; it is a different setting with its own definitions.
Nguyen and Tang study the irreversible catalytic network , , a simple reaction–diffusion system with both a positive and a boundary equilibrium (catalyst used up). They settle every mass regime but one and leave it as a conjecture (AIM problem 416).
Timeline. 2021: Fellner–Morgan–Tang give global classical solutions with uniform bounds. 2026: Nguyen–Tang prove convergence for and and local results in between, conjecturing global attraction there.
On a bounded connected smooth domain with and :
with homogeneous Neumann conditions and strictly positive compatible initial data. The masses , are conserved. The equilibria are the positive one and the boundary one .
If , every classical solution converges uniformly on to the positive equilibrium (no rate required).
This is the last open regime of Nguyen–Tang's stability analysis. Strict positivity is essential: with the solution stays away from the positive equilibrium.
For there is no positive lower bound on , so entropy dissipation can degenerate near the boundary equilibrium (), and the local results do not exclude trajectories approaching it.
is EuclideanSpace ℝ (Fin n) and is Mathlib's Laplacian. The domain is for a function with on ; the Neumann condition is the derivative within in the direction . Solutions are continuous on and for , and convergence is TendstoUniformlyOn. The goal quantifies over classical solutions; their existence is proved in the literature (Fellner–Morgan–Tang; Nguyen–Tang, Theorem 2.1) but is not part of this statement.
Gustafson, Meinert and Melcher construct axisymmetric saddle points of the micromagnetic energy of a spherical shell in two ways (a heat flow, and continuation from an explicit solution at ). Their Remark 3.18 conjectures that a single uniqueness statement identifies the two; it is problem 241 of the AIM open problem list.
Timeline. 2016: Kravchuk et al. propose the model. 2025: Gustafson–Meinert–Melcher construct the saddle points and state the conjecture.
For anisotropy the energy of is . An axisymmetric field with profile is critical exactly when
The hemispheric class adds , , .
For every there is exactly one smooth profile in that solves (2.6) and induces a smooth map . The statement may be proved or disproved.
Uniqueness would identify the two constructions as one saddle branch; a counterexample would give further degree-zero critical points of .
(2.6) is singular at both poles and is a two-point boundary condition, so standard ODE uniqueness does not apply, and the paper's comparison arguments only control solutions in the wedge . Numerical evidence (shooting) finds at , besides , a second solution in the class with (similarly at ), which leaves the wedge.
Profiles are functions ; all conditions, and the uniqueness, are imposed on only (values outside are unconstrained, so uniqueness on would be trivially false). Smoothness is ContDiffOn ℝ ∞ on . "Induces a smooth map" means the field extended to as a function of is there; this excludes profiles with a cone singularity at a pole. The paper's uses piecewise profiles; by its Corollary 2.7 it has the same solutions.
A Costas array is a permutation matrix in which the difference vectors between distinct dots are pairwise distinct; such arrays are frequency-hopping patterns for sonar and radar (Costas, 1984). Rubio and Torres ask whether their -dimensional version can stay Costas in every window of its periodic extension, and conjecture that this happens only in the smallest order.
Timeline. 1984: Taylor proves that 2D periodic Costas arrays have order . 2023: Rubio–Torres prove the odd-order and 3D cases, give examples, and state Conjecture 1.
Let , , with all sides , and a bijection; the dots are . The array is Costas if the difference vectors between distinct dots are distinct, and periodic Costas if moreover, after repeating the dots periodically over , the dots inside every translate have distinct difference vectors.
Conjecture 1: if and defines a periodic Costas array, then
equivalently every . The condition is a normalization ( swaps the boxes).
A proof would give the multidimensional analogue of Taylor's theorem; a counterexample would give periodic distinct-difference patterns of non-power-of-two order.
The Rubio–Torres counting argument needs a bound that is available only when is one-dimensional, which is why it stops at . Computational evidence: an exhaustive window check reports that the array with dots is periodic Costas, which would disprove the conjecture.
A point of is a pair ; boxes are 1-based; is a total function whose values off are unused. Differences are plain integer vectors (not reduced modulo the sides), windows range over all , and and sides are part of the definition, so no degenerate case holds vacuously.
Many estimation procedures in statistics, and most stochastic optimization models in operations research, have the same shape: a decision or parameter is chosen to minimize an expected loss under a distribution that is not known. In practice is replaced by an estimate built from the information available at stage (an empirical measure, a smoothed or parametric fit, a Bayesian posterior), and the minimizer of the estimated problem is used in place of the true one. The basic question is whether this is justified: do the estimated solutions converge to a true solution, and the estimated optimal values to the true optimal value, as information accumulates?
For maximum likelihood this is Wald's consistency theorem (Wald 1949); Huber extended it to M-estimators under non-standard conditions (Huber 1967). Both settings are unconstrained, or constrained to an open set, and assume finite-valued criteria. Constrained least squares, and Huber regression with inequality constraints, variance-component models with Heywood cases, and two-stage stochastic programs with recourse all lead instead to criteria that take the value off a closed feasible set and are only lower semicontinuous in .
J. Dupačová and R. Wets (IIASA WP-86-41, 1986; journal version Ann. Statist. 16 (1988)) proved consistency in this generality by combining epi-convergence of functions with the theory of measurable multifunctions and normal integrands. This mission formalizes their §3.
is a Polish space with its Borel -field and is a probability measure on it. The integrand is , and the true problem is to minimize
with the convention that whenever is not bounded above by a summable function. The effective domain of a function is , and .
Information arrives on a probability space with an increasing sequence of -fields . Each sample yields probability measures on , and is -measurable for every Borel : the estimate at stage uses only stage- information. The estimated problem minimizes
A sequence epi-converges to if, at every , along every sequence , and along some sequence .
The standing hypotheses are Assumption 3.4: with closed and nonempty; is continuous for ; is lower semicontinuous; and is locally lower Lipschitz on with a bounded continuous modulus . Assumption 3.5 asks that, for -almost every , converge in distribution to , that be uniformly tight along for each , and that for all .
Let be compact, suppose -a.s. for every , and suppose . Then there are -measurable selections of with
The goal does not assume that has a unique global minimizer, and it does not assume convexity.
In attack order:
The result separates two things: the statistical input, which is only convergence in distribution of plus a tightness condition, and the variational output, which is convergence of optimal values and solutions. It therefore applies to any estimator that converges weakly almost surely: empirical measures, kernel estimates, parametric fits. It also covers constrained and nonsmooth problems: the feasible set enters through off , and only lower semicontinuity in is required. Asymptotic distribution results for constrained estimators, such as the second part of the same paper and the subsequent literature on sample average approximation, start from this consistency.
The theorem is proved on paper. To the best of current knowledge none of it is machine-checked. Mathlib has weak convergence of probability measures, lower semicontinuity and extended-real integrals. It does not have epi-convergence, Effros-measurable multifunctions, normal integrands or the Kuratowski–Ryll-Nardzewski selection theorem. A formal proof produces these as reusable components. It also has to supply the details that the paper's proof of Theorem 3.8 leaves as a sketch.
Pointwise convergence is not enough to move minimizers to the limit, and uniform convergence fails because is off and need not be bounded. Epi-convergence is the right notion. Proving it needs a liminf inequality along moving points under moving measures . That combines Fatou's lemma, the lower Lipschitz bound and the tightness condition, and the integrands are extended-real-valued, so care is needed.
The second difficulty is measurability. The exceptional null set lies in but not in , so "-measurable" has to be understood on a full-measure set in the trace -field. The paper's argument for Theorem 3.8 appeals to continuity of in the epi-topology, and it remarks itself that Theorem 3.7 gives this only along sequences satisfying Assumption 3.5. A solver will have to rebuild this step, for example through the normal-integrand structure of .
EuclideanSpace ℝ (Fin n) with its Euclidean norm.EReal-valued. Every expectation is the mission's expect: when , and otherwise, both computed as Lebesgue integrals of -valued functions. A Bochner integral, which would assign to non-integrable functions, is never used for or .Pν k and 𝔽 k are the paper's and , and is a separate argument.The hypotheses are not vacuous. A sorry-free check verifies all of them, including those of the goal, for with Dirac measures. Defining the expectation through a Bochner integral, or dropping (which makes every all of ), would trivialize or change the statements; the definitions above rule both out.
Contributions are welcome on any milestone. Proposition 3.1 (Kuratowski–Ryll-Nardzewski for -valued multifunctions) and Proposition 3.3 (deterministic epi-convergence facts) are independent of the probabilistic setting and reusable beyond this mission.
The Pontryagin maximum principle is the basic first-order necessary condition of optimal control: along an optimal control, the control value at almost every time extremizes a Hamiltonian built from the dynamics and an adjoint vector. The classical statement presupposes that an optimal control exists. For many problems none does: the set of trajectories is not closed, or the cost does not attain its infimum, and the classical principle then says nothing.
Ekeland's 1974 paper On the Variational Principle (DOI 10.1016/0022-247X(74)90025-0) proves a general result about lower semicontinuous functions on complete metric spaces (its Theorem 1.1, now called Ekeland's variational principle) and closes with an application to control theory in §7 (pp. 348–351): for every terminal-cost problem satisfying mild regularity and growth conditions, there are ε-optimal controls that satisfy the maximum principle up to ε, whether or not an optimal control exists. The argument equips the measurable controls with the metric "measure of the set where two controls differ", which has since become a standard device in nonsmooth and approximate optimal control. For the classical theory, Ekeland refers to the treatise of Pallu de la Barrière (Optimal Control Theory, Saunders, 1967).
Fix , a horizon , an initial state , and a nonempty compact metrizable space of control values, with its Borel σ-algebra. A control is a measurable map . The dynamics are a map , and the state obeys
A trajectory of (Lean: IsTrajectory f x₀ T u x) is a function continuous on with for all . The standing hypotheses are:
fx) are continuous on ;The terminal cost is given by a function , and the problem is to minimize over all controls. The adjoint vector along a pair (Lean: IsAdjoint fx g T u x p) solves the linear equation
where is the transpose. The control distance (Lean: ctrlDist T u₁ u₂) is
and the needle variation of a control at with value (Lean: needle T uε u₀ t₀ τ) equals on and elsewhere.
For every there is a control with trajectory and adjoint vector such that
The result. Theorem 7.1 decouples the maximum principle from existence of optimal controls. Any minimizing sequence can be replaced by one consisting of controls that satisfy the necessary condition up to a vanishing error, so approximate extremals are available for numerical schemes and for limiting arguments (relaxation, convergence of extremals) in problems without compactness or convexity of the velocity sets. The same scheme, a complete metric on controls plus Ekeland's principle plus needle variations, underlies later proofs of the maximum principle with state constraints and in nonsmooth settings.
Formalizing it. The theorem has a published proof, which the paper sketches in four pages and partly defers to classical results (local existence for measurable controls, differentiability of trajectories with respect to needle variations). Neither Mathlib nor the platform contains this theorem or a maximum principle for measurable controls with time-dependent dynamics; the nearest platform items assume an exact optimum, a running cost and globally Lipschitz autonomous dynamics. A formalization requires a Carathéodory theory of ODEs in Lean, the complete metric space of controls, and a rigorous version of the classical first-variation computation. Each of these is useful well beyond this paper.
The obvious argument fails at its first step: a minimizing sequence of controls has no convergent subsequence in any useful sense, because measurable controls with values in are not compact in the metric and their weak limits are relaxed controls, which are not controls. Ekeland's principle avoids compactness, but it needs a complete metric space on which the cost is lower semicontinuous. Completeness of (Lemma 7.2) and continuity of the cost (Lemma 7.3) both require care. Continuity must hold for trajectories driven by merely measurable controls, which converge only in measure. The needle derivative (Lemma 7.4) holds only at times where the trajectory satisfies the state equation in the classical sense, which is almost every time but not every time.
ℝ → K with Measurable u; only values on matter. Trajectories and adjoint vectors are functions ℝ → EuclideanSpace ℝ (Fin n), continuous on and solving the integral form of their equation. The paper uses the same form in (7.13). A definition that asks for a derivative at every time would be unsatisfiable for discontinuous controls and would make the goal vacuous; the integral form avoids this.f and fx on univ ×ˢ univ ×ˢ Icc 0 T together with HasFDerivAt (fun y => f y u t) (fx x u t) x. Hypothesis (b) is ∃ c, … with the order of arguments ; the page prints in (b), a slip.ContinuousLinearMap.adjoint, and is gradient g x.⨅; (7.4) and (7.15) are stated as "for every control with trajectory ".[Nonempty K] in the goal and milestone 5. With empty no control exists and the existential statements would be false.Welcome contributions include Carathéodory existence and uniqueness for ODEs with measurable time dependence, Gronwall-type estimates for absolutely continuous functions, the complete metric space of measurable maps under the disagreement measure, and differentiability of flows with respect to initial data.
The classical Lagrange multiplier rule and its inequality-constrained form, the Karush–Kuhn–Tucker (KKT) conditions, are necessary conditions satisfied at a minimizer of a constrained problem. In finite dimensions, a continuous function bounded below on a closed bounded feasible set attains its minimum, so the rule describes an actual point. In an infinite-dimensional Banach space this fails: closed bounded sets are not compact, minimizing sequences need not converge, and a smooth function bounded below on a smooth constraint set can have no minimizer at all. The multiplier rule then has nothing to describe.
Ekeland's 1974 paper On the Variational Principle (DOI) introduced a principle (its Theorem 1.1) that replaces "a minimizer exists" with "near every almost-minimizer there is a point that strictly minimizes a slightly perturbed function". Section 3 of the paper uses this to prove that, for a problem with finitely many smooth equality and inequality constraints satisfying a linear-independence regularity condition, nearly optimal feasible points satisfy the KKT conditions up to a small error, with no compactness and no existence of a minimizer. This is the first appearance of what is now called an approximate or asymptotic KKT condition, a notion central to the convergence theory of nonlinear programming algorithms.
Let be a real Banach space with dual (continuous linear functionals) and dual norm . Let be Fréchet-differentiable, with derivative , and let be (continuously Fréchet-differentiable). Fix and consider
The feasible set is (3.2). At the saturated constraints are (3.3). The regularity assumption (3.4) is: for every , the derivatives , , are linearly independent in .
In the Lean development these are EkelandVP.Constraints.feasibleSet p G and EkelandVP.Constraints.IsRegular p G, with constraints indexed by Fin m.
Assume (3.4), , and that is bounded below on (3.5). Then for every there are and with
An additional item states Corollary 3.4 (p. 333), the one-constraint case: if , and is bounded below on , then for every there are with and with .
The result. Theorem 3.1 is an existence theorem for approximate KKT points that needs neither compactness nor attainment of the infimum. It shows that every bounded-below problem with regular constraints has a sequence of feasible points whose objective values converge to the infimum and along which the KKT residual tends to zero. This is the property that later work calls approximate KKT or asymptotic KKT (AKKT) and uses as a stopping criterion and as a sequential optimality condition for nonlinear programming. Corollary 3.4 is the corresponding nonlinear eigenvalue statement: on a regular level set, is approximately proportional to at almost-minimizing points.
Formalizing it. The result is classical and proved in the paper; to our knowledge no machine-checked version exists. Mathlib has the Fréchet derivative, the implicit function theorem for strictly differentiable maps, Banach–Alaoglu and the Hahn–Banach separation theorems, but no Ekeland principle in this form, no Lyusternik-type tangent-curve theorem for mixed equality–inequality constraints, and no Farkas lemma in a dual Banach space. Each milestone is a reusable piece of nonlinear optimization theory in Banach spaces.
The obvious argument, "take a minimizer and apply the Lagrange multiplier rule", fails at the first step because no minimizer need exist. The variational principle supplies a point that minimizes on , but that function is not differentiable at , so the multiplier rule cannot be applied to it directly either. Two further gaps remain. Linearized feasible directions (those satisfying the derivative conditions on the active constraints) need not be directions along which one can actually move inside ; closing this gap requires the regularity assumption and completeness of , and must keep the active inequality constraints nonnegative, not just the equalities. And the resulting first-order inequality, which holds only up to , must be turned into an approximate multiplier representation in , an infinite-dimensional dual space in which the usual finite-dimensional Farkas lemma does not apply as stated.
[NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V]. is V →L[ℝ] ℝ with the operator norm; is fderiv ℝ F v.G : Fin m → V → ℝ, 0-based: the paper's constraint is Lean index , an equality constraint iff its index is . p ≤ m is assumed in the goal.ContDiff ℝ 1; is Differentiable ℝ F (Fréchet-differentiable everywhere).BddBelow (F '' 𝒞) and "" is " for all ". A real infimum over an empty or unbounded set would be a junk value.Contributions welcome: a general Ekeland principle with the strict-minimizer conclusion, a Lyusternik–Graves tangent-curve theorem for maps with surjective derivative onto , and a closedness result for finitely generated cones in .
Many sequential decision problems ask a learner to choose, round after round, a combination of items: a set of ads out of , a path in a network, a matching. After each choice the learner sees the loss of the items it used, not of those it did not. This is online combinatorial optimization with semi-bandit feedback. It contains the classical adversarial multi-armed bandit (choose one of arms) and is a standard model in online advertising, routing and ranking.
Chapter 5 of Bubeck and Cesa-Bianchi's monograph arXiv:1204.5721v2 treats this problem with one algorithm, Online Stochastic Mirror Descent (OSMD). Every regret bound in the chapter comes from a single mirror-descent inequality, specialized through the choice of a convex "regularizer". The chapter's capstone, Theorem 5.7, shows that a polynomial regularizer gives pseudo-regret with no logarithmic factor. For this is the minimax-optimal rate of the adversarial bandit, first attained by the INF strategy of Audibert and Bubeck (2009). The semi-bandit version is due to Audibert, Bubeck and Lugosi (2014).
Vectors live in . The arm set is a nonempty with for every , and . An oblivious adversary fixes loss vectors . In round the learner plays a random arm , pays , and observes . The pseudo-regret is
A Legendre function on , for a nonempty open convex , is a continuous that is strictly convex and on and whose gradient norm tends to at . Its Bregman divergence is , and its Legendre–Fenchel transform is .
Online Mirror Descent with learning rate and vectors starts at . It then sets and . OSMD uses a random estimate of the loss. In the semi-bandit case it plays with and uses
A -potential is a convex, , increasing with , and . It defines the Legendre function on . With this is the negative entropy.
For every -potential and non-negative unbiased estimates,
For with , the estimate (5.5) and ,
Theorem 5.7 is the sharpest semi-bandit bound in the monograph. It shows that removing the factor of the exponential-weights analysis (Theorem 5.6) is a matter of the regularizer, not of a new algorithm. The same OSMD template gives the Euclidean-ball bound of Theorem 5.8 and is reused for bandit convex optimization in Chapter 6. Lemma 5.1, Lemma 5.2 and Theorem 5.3 are the standard mirror-descent toolkit, used throughout online learning and optimization.
All results of the chapter are proved in the book. Lemmas 5.1 and 5.2 are cited from Cesa-Bianchi and Lugosi (2006). None of them is formalized on Prove2Me. The published mirror-descent bound of Bandit Algorithms XII treats linear losses with a comparator inside and Euclidean-space vectors; it is not Theorem 5.3. The mission adds a machine-checked version of the whole chain, from Legendre duality to the explicit constant , with two of the printed statements corrected (below).
The pathwise mirror-descent inequality is a telescoping argument, but several of its steps rest on convex analysis that Mathlib does not package. One is the existence and interior location of Bregman projections onto a set that touches the boundary of . Another is the differentiability of on the open dual space and the identity . A third is the closed form of for a potential defined through an improper integral of .
The probabilistic step is not a martingale argument. Only conditioning on the current iterate is available. The estimate (5.5) divides by , so its integrability and unbiasedness have to be derived from the fact that the iterates stay in the open orthant. Finally, the explicit constant requires a Hölder step, , and the matching bound .
Vectors are Fin d → ℝ. The arm set is a Set of vectors with coordinate sum , and is convexHull ℝ C. Rounds are , sums run over Finset.Icc 1 n, and index is unused. A randomized run is a family of measurable processes on a probability space, with the deterministic OMD recursion holding on every sample path. is the coordinatewise conditional expectation given , which is exactly what the book's proofs use. Losses are oblivious, so is stated as "for every , ". is valued in EReal, and is evaluated only on the open dual space, where is finite. Wherever an expectation of a possibly non-integrable quantity appears on a right-hand side, its integrability is assumed: the book's bound is then and trivial, while Lean's integral would be .
Corrections and instantiations, each labelled in the item's Formalization Note:
A trivializing formalization would let , or the estimate be junk values: an OSMD step at , a Lean division , or a regret written as a real infimum over an unbounded set. Here every run is the book's algorithm on the open orthant, and each bound is stated against every comparator in .
Reusable beyond this mission: the Legendre/Bregman layer, the OMD run predicate and the -potential layer. Proofs of Lemmas 5.1 and 5.2 in this generality would be welcome additions to the library.
An integer linear program is usually attacked through its linear programming relaxation , which drops the integrality constraint. Two questions follow at once. How far can an optimal solution of the relaxation be from an optimal integer solution? And how many rounds of rounding-based cutting planes are needed before the relaxation describes the integer points exactly? Branch-and-bound, cutting-plane methods and the parametric analysis of integer programs all depend on the answers.
W. Cook, A.M.H. Gerards, A. Schrijver and É. Tardos, Sensitivity theorems in integer linear programming (Math. Programming 34 (1986) 251–264), answer both in terms of the number of variables and the largest subdeterminant of the constraint matrix, independently of the right-hand side.
Timeline.
All matrices, vectors and polyhedra are rational. Let be an integral matrix. A square submatrix of order , where , keeps rows and columns of . The quantity is the largest over all such submatrices . So , and whenever . Norms are and .
For write . An optimal solution of is a point of maximizing . For it is an integral point of maximizing among the integral points of . A rational polyhedron is a set with , rational. The integer hull is the convex hull of the integral points of .
If for all , with integral and rational, then every integral point of satisfies the Chvátal cut . The Chvátal closure is the set of points satisfying all Chvátal cuts. Set and . Then for all . The Chvátal rank of is the least with . The Chvátal rank of the matrix is the supremum of the Chvátal ranks of over all integral vectors .
In particular, every integral matrix has finite Chvátal rank, and the bound does not depend on or on .
The result. Theorem 10 shows that the number of Gomory–Chvátal rounding rounds needed for is controlled by alone. It is the first general finite bound on the Chvátal rank of a matrix. Earlier, the matrices of Chvátal rank 0 had been characterized by Hoffman and Kruskal: they are the matrices whose transpose is unimodular. Some classes of rank 1 had also been characterized (Edmonds–Johnson, Gerards–Schrijver). The proximity results of §2 are used on their own. They bound the work needed to solve an integer program from an LP optimum, and they show that the optimal value of an integer program changes at most affinely with . They are also the standard starting point for the later proximity literature.
Formalizing it. All results are proved in the paper. As far as is known, none of them has a machine-checked proof: the Prove2Me corpus holds no Chvátal rank bound, and its existing proximity theorems concern a different bound, the bound with the largest entry. This mission asks for Lean proofs of the paper's statements with the constants exactly as printed. It also builds a reusable layer over : polyhedra, LP and IP optimality, integer hulls, the Chvátal closure and the Chvátal rank.
The proximity theorems need a conic decomposition into integral generators with entries bounded by . That requires Cramer's rule bounds on cone generators and Carathéodory's theorem, and neither is in Mathlib in this form for rational polyhedral cones.
Theorem 7 needs finite generation of integral cones with explicit coefficient bounds, together with LP duality.
The Chvátal-rank part is harder. The obvious induction on the value of a valid inequality fails, because the value gap is not bounded independently of until Theorem 7 and Corollary 2 bound it by . Theorem 8 itself rests on a flatness theorem for lattice-free polyhedra (Lenstra; Grötschel–Lovász–Schrijver), which the paper cites without proof. It also needs Schrijver's lemma that for faces , and invariance under unimodular affine maps. None of these is in Mathlib.
Fin n → ℚ, is Matrix (Fin m) (Fin n) ℤ cast to , and a polyhedron is a finite system of rational inequalities.A complete development needs the following:
The LP, cone and Chvátal-closure layers are reusable beyond this mission. Proofs of any milestone are welcome, and so is groundwork such as polyhedrality of the Chvátal closure or the flatness theorem, submitted as separate theorems.