Optimization

Every linear programming problem asks to minimize a linear cost $c'x$ over a polyhedron — a set of the form $P = \{x \in \mathbb{R}^n \mid Ax \ge b\}$, or in standard form $\{x \mid Ax = b,\ x \ge 0\}$. Chapter 2 of Bertsimas–Tsitsiklis develops the geometry of these feasible sets, and its central achievement is making the intuitive notion of a "corner point" rigorous. There are three natural candidates: the extreme point — a point of $P$ that cannot be written as a convex combination of two other points of $P$ (purely geometric, representation-independent); the vertex — the unique minimizer of some linear cost $c'y$ over $P$ (geometric, via supporting hyperplanes); and the basic feasible solution — a feasible point at which $n$ linearly independent constraints are active (algebraic, the object the simplex method actually computes with). This mission formalizes polyhedra, active constraints, vertices and basic (feasible) solutions, and proves the fundamental Theorem 2.3: for a nonempty polyhedron all three notions coincide. Around the capstone sit the supporting pillars: polyhedra are convex (Theorem 2.1), the characterization of points pinned down by $n$ linearly independent active constraints (Theorem 2.2), finiteness of the set of basic solutions (Corollary 2.1), and the basis-column characterization of basic solutions in standard form (Theorem 2.4) — the combinatorial engine behind the simplex method of Chapter 3 and the root of the entire series.

Motivation

Finding the quickest route between two points of a road network is among the oldest problems of operations research. It is the subproblem inside vehicle routing, network flow and many dynamic programs. Richard Bellman's four-page note On a routing problem (Quarterly of Applied Mathematics, 1958) treats it as a dynamic program. The minimal travel times satisfy a nonlinear system of equations, and that system can be solved by successive approximations that terminate after a number of steps bounded in advance. The iteration is now known as the Bellman–Ford method. A footnote added in proof records that Max Woodbury and George Dantzig had obtained the same scheme independently, and Ford's RAND report of 1956 describes a closely related labelling procedure.

Timeline.

• 1956. L. R. Ford Jr., Network flow theory (RAND P-923): a label-improving procedure for shortest paths.
• 1957. Bellman's Dynamic Programming (Princeton) states the principle of optimality used here.
• 1958. Bellman's note: the routing equation, its uniqueness, approximation in policy space with an (N − 1)-step bound, and a second, monotone increasing scheme.
• 1959. Dijkstra gives a label-setting method for nonnegative lengths.
• 1962. Floyd's Algorithm 97 computes all pairs of shortest distances.

Setting

There are $N$ cities, numbered $1, \dots, N$. Every two of them are linked by a direct road, and city $N$ is the destination. The travel time from $i$ to $j$ is a real number $t_{ij}$; the matrix $T = (t_{ij})$ need not be symmetric. Throughout, $t_{ij} > 0$ for $i \ne j$.

A route from $i$ to $N$ is a sequence of cities $i = c_0, c_1, \dots, c_m = N$ in which consecutive cities differ. Its stops are $c_1, \dots, c_{m-1}$, and its time is $\sum_{r<m} t_{c_r c_{r+1}}$. The minimal time $f_i$ (3.1) is the least time of a route from $i$ to $N$, and $f_N = 0$.

The routing equation (3.2) is the system

Approximation in policy space (§5) starts from the direct-route policy (5.2), $f_i^{(0)} = t_{iN}$, and iterates (5.1):

The second scheme (§7, (7.1)) starts instead from $\underline f_i^{(0)} = \min_{j\ne i} t_{ij}$ and uses the same step.

Formalization targets

Goal: convergence within $N - 1$ iterations

For every $k \ge N - 1$ the following hold. Each $f_i^{(k)}$ is the minimal time from $i$ to $N$, attained by a route. The vector $f^{(k)}$ solves (3.2). Every real solution of (3.2) equals $f^{(k)}$:

This is the claim of the Summary ("converges after at most $(N-1)$ iterations") and of the last sentence of §5. The paper's bound $N - 1$ is kept, although $N - 2$ also suffices.

Milestones

1. (3.2): the minimal times exist and satisfy the routing equation.
2. §4: (3.2) has at most one solution.
3. (5.4): $f^{(1)} \le f^{(0)}$.
4. §5, the sentence after (5.4): $f_i^{(k)}$ is the minimal time over routes with at most $k$ stops.
5. (5.5): $f^{(k+1)} \le f^{(k)}$ for all $k$.
6. §7: the scheme (7.1) increases, stays below the solution of (3.2) (7.2), and equals it from some index on.

Significance

The result. The note turns an enumeration over exponentially many paths into $N - 1$ rounds of $N$ minimisations each, with a bound fixed before the computation starts. The uniqueness theorem makes the routing equation a characterisation of the minimal times, not merely a property of them. This is the template for later correctness proofs of shortest-path and value-iteration algorithms. The monotone decrease (5.5) is the first instance of policy improvement: every iterate is the value of an actual routing policy.

Formalizing it. The results are classical and proved. What this mission adds is a machine-checked development against the paper's own objects. Routes, their times and minimal times are defined from scratch. The iteration is stated exactly as printed, apart from the corrected initial value at the destination. The (N − 1)-step termination is asserted as an equality, not a limit. Related platform items treat other methods and do not cover these statements. One is the label-correcting method (BertsekasDP.label_correcting_correctness_of_nonneg_arcs, BertsekasDP.label_correcting_terminates). Another is the stochastic shortest path problem under a termination assumption that fails for deterministic routing (BertsekasDP.ssp_main_theorem). There are also the generic candidate-list algorithm (BertsekasNetwork.generic_shortest_path_algorithm), Floyd's Algorithm 97 and Dijkstra's method.

Difficulty

The minimum in (3.2) may be attained at a $j$ whose own optimal route passes back through $i$. The routing equation is a fixed-point equation for an operator that is monotone but not a contraction in any fixed norm. The standard contraction argument for discounted dynamic programs therefore does not apply. Uniqueness has to use $t_{ij} > 0$ to exclude zero-time cycles: with $t_{12} = t_{21} = 0$, the system (3.2) has infinitely many solutions. The $N - 1$ bound depends on the at-most-$k$-stops reading of $f^{(k)}$ and on the fact that an optimal route never needs to revisit a city. Neither is visible from the recursion alone. For the scheme of §7, the page gives no bound on the number of iterations, and none holds uniformly in $t$.

Formalization scope

Cities are Fin (n + 1), so $N = n + 1$, with standing hypothesis $n \ge 1$. City $N$ is Fin.last n, and travel times are t : Fin (n + 1) → Fin (n + 1) → ℝ with $t_{ij} > 0$ for $i \ne j$. Diagonal entries are unconstrained and never used. No symmetry, triangle inequality or integrality is assumed. A route is a list of cities with distinct consecutive entries ending at $N$. Repeated cities are allowed; with positive times this changes no minimum. Minimal times are attained minima over routes (IsMinTime, IsMinTimeWithin), not real infima. The minimum in (3.2) is a Finset.inf' over all $j \ne i$, the destination included.

The paper's loose phrases are made explicit as follows.

• "Using an optimal policy" (3.1) becomes a minimum attained by a route and below every route.
• "Represents the minimum time for a path with at most one stop" becomes, for every $k$, a minimum over routes with at most $k + 1$ roads.
• "Converges after at most $(N - 1)$ iterations" becomes $f^{(k)} = f$ for every $k \ge N - 1$.
• "Only a finite number of iterations will be required" (§7) becomes $\exists K, \forall k \ge K$, $\underline f^{(k)} = f$.
• "The solution of (3.2)" in §7 becomes an arbitrary solution of (3.2), which milestones 1–2 show is the vector of minimal times.

Two printed slips are corrected. (5.2) is printed for $i = 1, \dots, N$, which would set $f_N^{(0)} = t_{NN}$, and with $t_{NN} > 0$ statements (5.4), (5.5) and the goal would be false. The formalization uses $f_N^{(0)} = 0$, the value the paper's own justification needs. (7.1) prints "$N = 1$" for $N - 1$. Section 6 (computational aspects) and the closing expectation of §7 that the first method converges faster are not formalized.

The goal cannot be satisfied trivially. The minimal times are defined from routes, not as a solution of (3.2) or as a limit of the iteration, so the goal connects the recursion to the routing problem itself.

The development needs only finite minima, lists and induction; nothing beyond core Mathlib. The route and minimal-time layer is reusable for other deterministic shortest-path results. Proofs of any milestone are welcome, as are proofs of the sharper bound $N - 2$.

Selected references

• R. Bellman, On a routing problem, Quarterly of Applied Mathematics 16(1) (1958), 87–90. https://doi.org/10.1090/qam/102435
• R. Bellman, Dynamic Programming, Princeton University Press, 1957.
• R. Bellman, The theory of dynamic programming, Bull. Amer. Math. Soc. 60 (1954), 503–515. https://doi.org/10.1090/S0002-9904-1954-09848-8
• L. R. Ford Jr., Network flow theory, RAND Corporation P-923, 1956. https://www.rand.org/pubs/papers/P923.html
• E. W. Dijkstra, A note on two problems in connexion with graphs, Numerische Mathematik 1 (1959), 269–271. https://doi.org/10.1007/BF01386390
• R. W. Floyd, Algorithm 97: Shortest path, Communications of the ACM 5(6) (1962), 345. https://doi.org/10.1145/367766.368168

Motivation

Sequential decisions often change the distribution of future states. A planner choosing an action today must account for both its immediate reward and the later rewards made possible by the resulting state. The mathematical question is whether an optimal rule can be chosen once and reused at every stage, even when a competing plan may randomize and use the entire observed history. In Discounted Dynamic Programming, Blackwell studies this question on general Borel state and action spaces, beyond the finite models in which a direct comparison of actions is available.

The paper distinguishes several strengths of optimality. For each distribution of the initial state, an approximately optimal stationary plan exists, but a single plan that is approximately optimal at every initial state need not exist in a general Borel problem. Essential countability of the actions restores uniform approximate stationary optimality; essential finiteness yields exact stationary optimality. These are different mathematical claims, and the mission keeps their different quantifiers visible. Blackwell 1965, pp. 227, 229, 232–234.

Setting

A state is an element $s$ of a nonempty standard Borel space $S$, and an action is an element $a$ of a nonempty standard Borel space $A$. The transition kernel $q(\cdot\mid s,a)$ gives a probability distribution for the next state after action $a$ in state $s$. The reward $r(s,a,s')\in\mathbb R$ may depend on that next state $s'$; it is bounded and Borel measurable. Future rewards are discounted by $\beta$ with $0\le\beta<1$. These are the objects of Blackwell’s Sections 2–3. Blackwell 1965, pp. 227–228.

A plan $\pi=(\pi_1,\pi_2,\ldots)$ assigns a probability distribution of actions to each possible history before a decision. At stage $n$, that history contains $n-1$ completed state-action pairs and the current state. Thus plans may randomize and depend on earlier states and actions. A Markov plan instead uses a Borel function $f_n:S\to A$ at each stage; a stationary plan uses the same function $f$ at every stage and is denoted $f^{(\infty)}$. Starting from state $s$, the plan has discounted expected return

Here $\sigma_n$ and $\alpha_n$ are the state and action at stage $n$. The comparison class for an optimal plan is all such plans, including randomized and history-dependent ones. Blackwell 1965, pp. 228–229.

Two actions are equivalent at state $s$ when they have the same reward $r(s,a,s')$ for every next state $s'$ and the same transition measure $q(\cdot\mid s,a)$. An action set is essentially countable by a Markov plan $(f_1,f_2,\ldots)$ if, for every $(s,a)$, one of the actions $f_n(s)$ is equivalent to $a$ at $s$. It is essentially finite by that plan if $S$ has a countable Borel partition $(S_n)$ such that, for $s\in S_n$, one of $f_1(s),\ldots,f_n(s)$ is equivalent to every action $a$ at $s$. A finite action set is a special case. Blackwell 1965, pp. 233–234.

Formalization targets

For a probability distribution $p$ on $S$ and $\varepsilon>0$, $(p,\varepsilon)$-optimality asks for a stationary $f$ with

Theorem 6(b) asserts that such an $f$ always exists. Under essential countability, Theorem 7(a) obtains a stronger, uniform $\varepsilon$-optimality statement: for every $\varepsilon>0$ there is a stationary $f$ with $I(\pi)(s)\le I(f^{(\infty)})(s)+\varepsilon$ for all $\pi,s$. Its other targets identify the optimal return with the fixed point of the operator $U_\pi u=\sup_nT_{f_n}u$ and with the unique bounded solution of the optimality equation $u=\sup_{a\in A}T_au$. Blackwell 1965, pp. 232–234.

The mission’s goal is Theorem 7(b). Under essential finiteness, it asks for a stationary $f$ with exact optimality:

The milestone list also includes the paper’s operator identity, approximate selection result, contraction criterion, generated-plan comparison, and upper-bound criterion. Each has its own source index and statement. Blackwell 1965, pp. 231–234.

Significance

The exact result says that, under a condition weaker than a globally finite action set, repeated use of one measurable state-based rule matches or exceeds the return of every adaptive randomized plan. It is a structural result about what information and randomization can add to discounted control. The preceding approximate results specify what can still be guaranteed when that condition is relaxed; Blackwell’s examples show that the distinctions cannot simply be ignored. Blackwell 1965, pp. 229–230, 234.

Blackwell proved these statements in 1965. The formalization work here is to give machine-checked proofs for the Borel-space model and its full comparison class, together with reusable definitions of history-dependent kernels, returns, stationary rules, and Bellman operators. The draft theorem statements compile as Lean declarations, but their proofs remain open. The milestone results are intended to make both the final theorem and its supporting measure-theoretic objects independently usable.

Difficulty

On an uncountable Borel action space, the pointwise supremum of available action values does not automatically come with a Borel action selector. Choosing a maximizing action separately at each state may fail to define a measurable rule, and a supremum need not be attained. Also, a Markov or stationary comparison cannot by itself certify optimality against plans that depend on full histories. These issues are real in the paper’s examples: general Borel problems may lack an $\varepsilon$-optimal plan, and a given plan need not be uniformly approximated by a Markov plan. Blackwell 1965, pp. 229–230.

Formalization scope

The Lean model uses nonempty StandardBorelSpace types for $S$ and $A$. “Baire function” is read as Borel measurable on these metrizable spaces. The problem stores a Markov transition kernel, a bounded measurable real reward on $S\times A\times S$, and $0\le\beta<1$; $\beta=0$ is included. A plan contains a probability kernel on each finite history, and the return is the actual absolutely convergent series of expected one-stage rewards. The first decision is indexed by $0$ in Lean, corresponding to the paper’s index $1$. The finite history law is assembled through kernel composition products, and a stationary rule is represented by deterministic kernels. The integrals and series therefore express the paper’s expected return, including the cases where the reward depends on the next state.

For the operator results, $M(S)$ means bounded and measurable real functions. The suprema defining $U_\pi$ and the optimal return are real suprema over nonempty families bounded by the reward and discount; they are used only in that setting. The abstract operator in Theorem 5 maps $M(S)$ into itself. The action equivalence predicate uses the paper’s explicit equality of reward functions and transition laws; the later “i.e.” phrasing on p. 234 is weaker when interpreted as equality of operators alone. A partition piece may be empty, and Lean’s piece $n$ corresponds to the paper’s $S_{n+1}$, with rules $f_1,\ldots,f_{n+1}$.

An optimality claim here always compares with every randomized history-dependent plan. Restricting that quantifier to Markov or stationary plans would trivialize the target. A complete development needs measure-theoretic facts about history laws and their bounded integrals, the discounted series, measurable partitions and selections, and the sup-norm contraction of bounded Borel functions. The history-law and bounded-function infrastructure can be reused outside this mission. Contributions to those foundations and to the numbered milestone theorems are welcome.

Selected references

• David Blackwell, Discounted Dynamic Programming, Annals of Mathematical Statistics 36(1), 226–235, 1965. DOI: 10.1214/aoms/1177700285.

Motivation

Dynamic programming (DP) solves sequential decision problems by backward recursion: compute the optimal cost of the last stage, then of the last two stages, and so on. For problems with finitely many states and controls and real-valued costs, the recursion obviously gives the optimal cost. Applications are rarely like that. Control spaces are continuous, costs can be unbounded or infinite, the criterion can be multiplicative (risk-sensitive exponential cost) or worst-case (minimax), and the set of policies is an infinite product of function spaces. In this setting the DP recursion can fail to produce the optimal cost.

Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996), Part I, separates the order-theoretic content of DP from the measure theory. It works with an abstract monotone mapping $H$ that covers deterministic, stochastic, multiplicative-cost and minimax problems at once, following Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15 (1977). Chapter 3 answers the finite-horizon questions: when does the DP algorithm give the $N$-stage optimal cost, and when do optimal or nearly optimal policies exist? This mission is the first of a series formalizing the book. Later chapters (contraction models, monotone increase and decrease models, the Borel models of Part II) are built on the model fixed here.

Setting

Let $S$ (states) and $C$ (controls) be sets, and for each $x\in S$ let $U(x)\subseteq C$ be a nonempty control constraint set. Write $R^*=[-\infty,\infty]$ and let $F$ be the set of all functions $J:S\to R^*$, ordered pointwise. A mapping $H:S\times C\times F\to R^*$ is given, subject to the Monotonicity Assumption: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$ for all $x\in S$, $u\in U(x)$.

A selector is a function $\mu:S\to C$ with $\mu(x)\in U(x)$ for all $x$. A policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ of selectors. Define

and let $T^k$ be the $k$-fold composition of $T$. A terminal function $J_0\in F$ with $J_0(x)>-\infty$ for all $x$ is fixed. The $N$-stage cost of $\pi$ and the $N$-stage optimal cost are

A policy is uniformly $N$-stage optimal if each tail $(\mu_i,\mu_{i+1},\dots)$ is $(N-i)$-stage optimal, and $N$-stage $\varepsilon$-optimal if $J_{N,\pi}(x)\le J^*_N(x)+\varepsilon$ where $J^*_N(x)>-\infty$ and $J_{N,\pi}(x)\le-1/\varepsilon$ where $J^*_N(x)=-\infty$.

The three conditions on $H$ used in the chapter are F.1 (continuity of $H$ along nonincreasing sequences $J_k$ with $H(x,u,J_1)<\infty$), F.2 (there is $\alpha>0$ with $H(x,u,J)\le H(x,u,J+r)\le H(x,u,J)+\alpha r$ for all $r>0$), and F.3 (a quantitative selection property with a constant $\beta>0$).

Formalization targets

Goal: Proposition 3.1

Under F.1, if $J_{k,\pi}(x)<\infty$ for all $x,\pi$ and $k=1,\dots,N$; or under F.2, if $J^*_k(x)>-\infty$ for all $x$ and $k=1,\dots,N$:

and under F.2, for every $\varepsilon>0$ there is $\pi_\varepsilon$ with $J^*_N\le J_{N,\pi_\varepsilon}\le J^*_N+\varepsilon$.

Milestones

• Proposition 3.3: $\pi^*$ is uniformly $N$-stage optimal iff $(T_{\mu^*_k}T^{N-k-1})(J_0)=T^{N-k}(J_0)$ for $k<N$. Needs monotonicity only.
• Corollary 3.3.1: a uniformly $N$-stage optimal policy exists iff every infimum $T^{k+1}(J_0)(x)=\inf_{u}H[x,u,T^k(J_0)]$ is attained, and then $J^*_N=T^N(J_0)$.
• Proposition 3.4: if $C$ is Hausdorff and every sublevel set $\{u\in U(x)\mid H[x,u,T^k(J_0)]\le\lambda\}$ is compact, then $J^*_N=T^N(J_0)$ and a uniformly $N$-stage optimal policy exists.
• Proposition 3.7: the minimax mapping $H(x,u,J)=\sup_{w\in W(x,u)}\{g+\alpha J[f]\}$ satisfies F.2 with constant $\alpha$.
• Proposition 3.6: the multiplicative mapping $H(x,u,J)=E\{g\,J[f]\mid x,u\}$ over a countable disturbance set satisfies F.1, and F.2 with constant $b$ when $0\le g\le b$.
• Proposition 3.2: under F.3 and the finiteness of $J_{k,\pi}$, $J^*_N=T^N(J_0)$ and, for $\varepsilon_n\downarrow0$, policies with $\{\varepsilon_n\}$-dominated convergence to optimality exist.
• Corollary 3.7.1(a): for minimax control with $J_0=0$ and $J^*_k>-\infty$, the DP algorithm gives $J^*_N$ and $N$-stage $\varepsilon$-optimal policies exist.

Significance

The identity $J^*_N=T^N(J_0)$ says that an infimum over an infinite-dimensional policy space equals $N$ nested one-dimensional infima. Every numerical use of finite-horizon DP depends on it, and so do the infinite-horizon results of later chapters, which pass to the limit in $T^N(J_0)$. Corollary 3.3.1 and Proposition 3.4 give the existence of optimal policies, and Propositions 3.6 and 3.7 verify the abstract hypotheses for two models outside standard expected additive cost.

These results are proved in the book; none of them is formalized. Mathlib has no abstract DP model, and the platform's finite-horizon results (Bertsekas, Dynamic Programming and Optimal Control, Prop. 1.3.1 and the minimax DP algorithm) assume finite disturbance and constraint sets and real costs. They are special cases, not this theory. The finite-horizon results of the 1977 paper (Lemma 3.1 here, on compact sublevel sets, and Corollary 3.1.1, the F.1′ case) are already posed on the platform and are not posed again.

Difficulty

The obvious argument interchanges the infimum over policies with the composition of operators: $\inf_\pi T_{\mu_0}(\cdots)=T(\inf_{\pi'}\cdots)$. The inequality $T^N(J_0)\le J^*_N$ follows from monotonicity alone. The reverse inequality is the content. Taking a near-minimizing selector at each stage requires either passing a limit inside $H$ (F.1) or bounding how errors at later stages propagate through $H$ (F.2, F.3). Both steps break at infinite values. With $J^*_k(x)=-\infty$ there may be no $\varepsilon$-optimal policy at all (Counterexample 4 of the book). Without F.1 or F.2 the identity itself fails (Counterexamples 1–3). A proof must therefore track separately the states where the optimal cost is $-\infty$, which is why F.3 and the definition of $\varepsilon$-optimality have two cases.

Formalization scope

The model is a structure Model S C with fields U, U_nonempty, H : S → C → (S → EReal) → EReal and the monotonicity proof. Policies are ℕ → Selector, with selectors as a subtype of S → C. $T^N$ is m.T^[N], and $(T_{\mu_0}\cdots T_{\mu_{N-1}})(J)$ is a recursion that applies $T_{\mu_{N-1}}$ first. All values lie in EReal. The book's convention $\infty-\infty=\infty$ never arises in Propositions 3.1–3.4, which only add real numbers to extended reals. The minimax and multiplicative mappings implement it explicitly (badd, and an expectation that returns $+\infty$ when the positive part diverges). Every theorem assumes $J_0>-\infty$ and $N\ge1$. Assumptions F.1–F.3 are predicates on the model. F.2 is also available with a named constant (F2With) so that Propositions 3.6 and 3.7 can carry the book's constants $b$ and $\alpha$.

$J^*_N$ is defined as an infimum over policies of the composed operators, never through $T$, so the goal is not true by definition. A formalization in which $J_{N,\pi}$ already contains an infimum over controls would make Proposition 3.1 hold by rfl, and this one rules that out.

Proving the goal needs elementary EReal order arithmetic, iterated infima over subtypes, and pointwise selection of near-minimizers via choice. Proposition 3.6 additionally needs monotone and dominated convergence for countable sums in ℝ≥0∞. The model and operator definitions are reusable by the later missions of the series (contraction, monotone increase and decrease models). Proofs of any milestone, and reusable EReal lemmas about shifting by real constants, are welcome.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press 1978; Athena Scientific 1996, Chapters 2–3. https://web.mit.edu/dimitrib/www/soc.html
• D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15(3) (1977) 438–464. https://doi.org/10.1137/0315031
• D. P. Bertsekas, Dynamic Programming and Stochastic Control, Academic Press 1976.
• D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific 2022. https://web.mit.edu/dimitrib/www/abstractdp_MIT.html

Motivation

Many selection problems assign a value to each subset of a finite collection: the coverage supplied by chosen facilities, the influence reached by chosen seeds, or the value of a coalition. A submodular set function has diminishing returns in the precise sense that the combined value of two sets, counting their overlap once, does not exceed the sum of their separate values. When the function is also monotone, taking more elements never hurts. The unconstrained problem studied here permits nonmonotone functions, so both accepting and rejecting an element can matter. The question is what a single pass through the elements can guarantee when the function is available through value queries. Buchbinder et al., FOCS 2012

The randomized algorithm in this mission attains an expected one-half approximation for every nonnegative submodular function. The paper presents this as tight in the value-oracle setting: it recalls the earlier result of Feige, Mirrokni and Vondrák that a fixed improvement beyond one-half requires exponentially many queries. The contribution here is therefore both the guarantee and a short adaptive rule that attains it in a linear number of iterations. The local proposal follows the FOCS 2012 version of the paper; its theorem numbering differs from the later SIAM Journal on Computing article. Buchbinder et al., §I.A and Theorem I.2

Setting

Let $\mathcal N$ be a finite ground set, and let $f:2^{\mathcal N}\to\mathbb R_{\ge0}$ assign a nonnegative real value to every subset. The unconstrained submodular maximization problem asks for the largest value $f(S)$ among all $S\subseteq\mathcal N$. Write $OPT$ for that value when no confusion arises, and $O$ for a set attaining it. Submodularity means

There is no monotonicity or normalization assumption: $f(\varnothing)$ and $f(\mathcal N)$ may both be positive. A value oracle returns $f(S)$ for a requested subset $S$. The paper's complexity claim counts such queries, assuming a query takes constant time. Buchbinder et al., §I and footnotes 1–2

Algorithm 2 visits the elements once in an arbitrary order $u_1,\ldots,u_n$. It keeps two sets, starting at $X_0=\varnothing$ and $Y_0=\mathcal N$. At step $i$, it measures the gain $a_i$ from adding $u_i$ to $X_{i-1}$ and the gain $b_i$ from removing $u_i$ from $Y_{i-1}$. It clips each gain at zero, giving $a'_i=\max(a_i,0)$ and $b'_i=\max(b_i,0)$. It adds $u_i$ to $X$ with probability $a'_i/(a'_i+b'_i)$ and otherwise removes it from $Y$. When both clipped gains vanish, the paper defines the add probability as one. After all elements have been processed, the two sets coincide, and the algorithm returns their common value. The state law is adaptive: its probability at step $i$ depends on the actual pair of sets produced by earlier choices. Buchbinder et al., Algorithm 2

Formalization targets

The main target is Theorem I.2 for this exact algorithm and for every enumeration of the ground set:

The milestone statements retain the paper's key local quantities. For a comparison optimum $O$, set $OPT_i=(O\cup X_i)\cap Y_i$. Lemma II.1 asserts $a_i+b_i\ge0$. The endpoint statement identifies $OPT_0=O$ and $OPT_n=X_n=Y_n$. Inequality (3) bounds the conditional loss in the positive-gain case; Lemma III.1 compares the expected change of $OPT_i$ with the expected combined change of $X_i$ and $Y_i$. The telescoped display keeps the initial endpoint values $f(\varnothing)$ and $f(\mathcal N)$ before using nonnegativity. Buchbinder et al., Lemmas II.1 and III.1, inequality (3), proof of Theorem I.2

A companion target is Theorem I.4 via its second proof. For two normalized monotone submodular utilities $f_1,f_2$, let $g(S)=f_1(S)+f_2(\mathcal N\setminus S)$. The maximum of $g$ is exactly the optimal welfare of a two-player partition. Algorithm 2 on $g$ is asked to satisfy

This is the paper's three-quarter guarantee in its welfare application. Buchbinder et al., Theorem I.4 and Proof (2)

Significance

The main theorem gives a specific randomized rule whose expected value is at least half the best subset value, even when accepting an element can lower the objective. It applies without restricting the cardinality or shape of the chosen subset. The welfare corollary shows that keeping the initial endpoint values in the analysis yields a stronger guarantee for the objective formed from two monotone players. Buchbinder et al., Theorems I.2 and I.4

This mission formalizes the statement of the algorithm, its intermediate state laws, its comparison set, and the paper's numbered proof targets. The algorithmic guarantee is proved in the source paper; the local Lean theorem files are open statements with sorry and do not yet give machine-checked proofs of these results. A completed development would supply a reusable formal model of an adaptive finite random process over pairs of subsets, as well as the specific submodular inequalities. The published Submodular and OPT definitions from the earlier Feige–Mirrokni–Vondrák formalization are reused here.

Difficulty

The two possible updates cannot be assessed independently. The probability of each choice depends on the current state, and the comparison set $OPT_i$ can gain or lose the processed element in a way that differs from the two algorithm sets. A bound on the expected value of $X_i$ alone does not control the movement of $OPT_i$. The proof must handle the clipped gains, including the case when both are zero, while preserving the exact joint law of $(X_i,Y_i)$. Buchbinder et al., proof of Lemma III.1

Formalization scope

The ground set is a finite Lean type; subsets are Finset X, and values are real numbers. An order is a list with no repeated elements that covers the type, including the empty type. The run is an explicit finite mass function on pairs of subsets after every prefix of the list. Expectation is a finite weighted sum, so it has no integrability exception. The transition clips the two real marginal gains and handles $0/0$ by assigning probability one to the add branch, exactly as Algorithm 2 specifies. The optimum is the published maximum over all subsets. No ratio divides by a possibly zero optimum.

The theorem fixes Algorithm 2 itself; an arbitrary process with nested sets or a process defined by its desired approximation property does not satisfy this scope. The Lean goal states the value bound and leaves the paper's linear-time claim outside the formal theorem. The algorithm uses four value evaluations per processed element in its printed rule; the Lean development represents those evaluations, not an implementation cost model. The statement that its two final sets coincide is a separate milestone.

The source's main-text decreasing-returns definition has an overbroad quantifier on the added element. This development uses the equivalent lattice inequality given in the paper's footnote, which permits nonmonotone functions. The proof of Lemma II.1 also has a set-index slip, and the proof of Theorem I.2 prints $F$ for $f$ in one display; neither slip is copied into a formal statement. The one-step inequality (3) is stated for any nested pair with the processed element in $Y\setminus X$, a generalization of the conditioned reachable states in the paper. Contributions proving the endpoint invariant, conditional inequality, one-step expected estimate, and final bound are all within scope.

Selected references

• Niv Buchbinder, Moran Feldman, Joseph Naor and Roy Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, Proceedings of the 53rd IEEE Symposium on Foundations of Computer Science, 2012. FOCS version used here.
• Niv Buchbinder, Moran Feldman, Joseph Naor and Roy Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM Journal on Computing 44(5), 2015. DOI: 10.1137/130929205. The cited statement indices above refer to the FOCS version.

Motivation

Many problems in optimization and numerical analysis reduce to finding a point in the intersection of finitely many closed convex sets: solving a system of linear equations or inequalities, reconstructing an image from projections, or finding a feasible point of a convex program. The classical methods for this convex feasibility problem project the current point onto one set at a time, in Euclidean distance: Kaczmarz (1937) for linear equations, Agmon and Motzkin–Schoenberg (1954) for linear inequalities, and the cyclic projection method for general convex sets studied by Gubin, Polyak and Raik (1967).

L. M. Bregman's 1967 paper replaces the Euclidean distance by a general function $D(x,y)$ satisfying a short list of axioms, and shows that the projection method still works. The functions $D(x,y)=f(x)-f(y)-\langle\nabla f(y),x-y\rangle$ built from a strictly convex $f$ are the ones now called Bregman divergences, and the paper is the origin of Bregman projections, of the row-action methods of Censor and collaborators, and indirectly of mirror descent. Its §2 uses the abstract result to solve convex programs with linear constraints by relaxation.

This mission formalizes §1 of the paper for the cyclic control, in which the sets are visited in a fixed round-robin order. A companion mission treats the remotest-set control of Theorem 2, and two further missions treat the convex-programming results of §2.

Setting

Let $X$ be a real linear topological space and $A_0,\dots,A_{m-1}$ closed convex subsets of $X$, with intersection $R=\bigcap_i A_i$. Let $S\subset X$ be a convex set with $S\cap R\ne\emptyset$, and let $D:S\times S\to\mathbb R$. The paper requires:

• I. $D(x,y)\ge 0$, with equality if and only if $x=y$.
• II. For every $y\in S$ and every $i$ there is a point $P_iy\in A_i\cap S$ minimizing $D(\cdot,y)$ over $A_i\cap S$; it is the $D$-projection of $y$ onto $A_i$.
• III. For every $i$ and $y\in S$, the function $z\mapsto D(z,y)-D(z,P_iy)$ is convex on $A_i\cap S$.
• IV. $D(\cdot,y)$ has derivative $0$ at the point $y$.
• V. For every $z\in R\cap S$ and real $L$, the sublevel set $\{x\in S\mid D(z,x)\le L\}$ is compact.
• VI. If $D(x^n,y^n)\to 0$, $y^n\to y^*\in\bar S$, and $\{x^n\}$ lies in a compact set, then $x^n\to y^*$.

The relaxation sequence with control $(i_n)$ starts at any $x^0\in S$ and sets $x^{n+1}=P_{i_n}x^n$. Under the cyclic control $i_n=n\bmod m$, the sets are projected onto in the order $A_0,A_1,\dots,A_{m-1},A_0,\dots$. A limiting point of $\{x^n\}$ is the limit of a convergent subsequence $x^{n_k}$.

The Lean development uses the namespace BregmanRelax.Cyclic: DConditions A S D P bundles conditions I–IV and VI together with the closedness and convexity of the sets, CondV S D Z is condition V for the points of $Z$, IsRelaxSeq S P i x is the relaxation sequence with control $i$, and cyclicControl hm is $n\mapsto n\bmod m$.

Formalization targets

Goal: Theorem 1 (p. 203)

Under conditions I–VI, with the cyclic control, every limiting point of every relaxation sequence lies in every set:

The statement is about every starting point $x^0\in S$ and every convergent subsequence. It does not assert that the whole sequence converges.

Milestones

1. Lemma 1 (pp. 201–202): for $z\in A_i\cap S$ and $y\in S$,

2. Lemma 2 (2) (p. 202): for any control and any $z\in R\cap S$, $\lim_{n\to\infty}D(z,x^n)$ exists.
3. Lemma 2 (3) (p. 202): for any control, $D(x^{n+1},x^n)\to 0$.
4. Lemma 2 (1) (p. 202): for any control, $\{x^n\}$ lies in a compact set.

Further result: Note 1, condition (1) (pp. 204–205)

For any control whose relaxation sequence has all its limiting points in $R$ (the cyclic control, by Theorem 1), if in addition $S$ is closed and $y\mapsto D(z_1,y)-D(z_2,y)$ is continuous on $S$ for all $z_1,z_2\in R\cap S$, then the relaxation sequence converges to a point of $R$.

Significance

Theorem 1 is the abstract convergence theorem behind cyclic Bregman projections. With $D(x,y)=\|x-y\|^2$ in a Hilbert space it gives the convergence of cyclic orthogonal projections onto finitely many closed convex sets in the weak topology (the paper's Example 1). With $D$ given by a Bregman divergence it gives the method that the paper's §2 turns into an algorithm for convex programs with linear equality and inequality constraints, including entropy maximization. Lemma 1, the generalized Pythagorean inequality, is used throughout the later literature on Bregman projections, mirror descent and online learning.

The results are proved in the paper and are classical. To our knowledge no machine-checked version exists: Mathlib has orthogonal projections onto closed convex sets in Hilbert spaces, but no Bregman projections and no convergence theorem for cyclic projection methods. A formalization supplies an axiomatic interface (conditions I–VI) that does not depend on any particular divergence, so special cases (Euclidean distance, Kullback–Leibler divergence, Bregman divergences of Legendre functions) can be obtained by checking the conditions.

Difficulty

There is no norm and no metric: $D$ is neither symmetric nor subject to a triangle inequality, and $X$ is only a topological vector space. The usual Fejér-monotonicity argument for Euclidean projections, which compares distances to a fixed point of $R$, works only one way in $D$. Convergence of a subsequence $x^{n_k}$ does not by itself say anything about the shifted subsequences $x^{n_k+1},\dots,x^{n_k+m-1}$, and these are needed to reach every set $A_i$. That step requires condition VI together with compactness, and condition VI has a compactness premise that has to be supplied separately. Throughout, convergence is in a general topology where "compact" and "sequentially compact" may differ.

Formalization scope

The formalization commits to the following readings, each recorded in the items' Formalization Notes.

• The projection is a map. $P:\iota\to X\to X$ is fixed, and condition II states that $P_iy$ is a minimizer. Condition III is stated for this map.
• Condition IV, one-sided. The paper asks for $\lim_{t\to0}D(y+tz,y)/t=0$ for every $z\in X$. The formalization assumes only the right-hand limit in the directions $w-y$ with $w\in S$, which is what the proofs use and what the paper's IV implies. Every theorem is therefore at least as strong as the paper's.
• Compactness is sequential. "Compact" in V, VI and Lemma 2 (1) is IsSeqCompact. The set of elements of $\{x^n\}$ being compact is read as $\{x^n\}$ lying in a sequentially compact set.
• Hausdorff space. The proof of Theorem 1 identifies two limits of one sequence, so T2Space X is assumed. $X$ is a real topological vector space (IsTopologicalAddGroup, ContinuousSMul ℝ).
• Limiting point means the limit of x ∘ φ for a strictly increasing φ : ℕ → ℕ.
• Index base. The sets are indexed by Fin m with $0<m$, and the cyclic control is $n\mapsto n\bmod m$, the paper's $i_n=(n\bmod m)+1$ shifted by one.
• Translation typos. Condition II is printed as "$D(x,y)=\min_{z\in A_i\cap S}D(z,x)$" with "$i\in T$". The formalization reads $\min_z D(z,y)$ and $i\in I$. In Lemma 2 (2) the faint set symbol is read as $R$, and $z$ is taken in $R\cap S$, as in the proof.
• Domain of $D$. $D$ is a total function X → X → ℝ; every condition constrains it on $S\times S$ only, and the standing assumption $S\cap R\ne\emptyset$ is an explicit hypothesis.

A trivializing formalization is ruled out: the hypotheses are satisfiable (a sorry-free local check takes $X=\mathbb R$, $D(x,y)=(x-y)^2$, two overlapping closed intervals and the clamp projections), the conclusion concerns every limiting point of every cyclic run, and the goal neither assumes convergence nor restricts the control.

Contributions welcome: proofs of the milestones, a proof of the goal, and instances of DConditions for concrete divergences (squared Euclidean distance in finite dimension, Bregman divergences of strictly convex differentiable functions). These instances are reusable by the companion missions of this paper.

Selected references

• L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Computational Mathematics and Mathematical Physics 7(3) (1967) 200–217. https://doi.org/10.1016/0041-5553(67)90040-7
• L. G. Gubin, B. T. Polyak, E. V. Raik, The method of projections for finding the common point of convex sets, USSR Computational Mathematics and Mathematical Physics 7(6) (1967) 1–24. https://doi.org/10.1016/0041-5553(67)90113-9
• T. S. Motzkin, I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954) 393–404. https://doi.org/10.4153/CJM-1954-038-x
• Y. Censor, A. Lent, An iterative row-action method for interval convex programming, Journal of Optimization Theory and Applications 34 (1981) 321–353. https://doi.org/10.1007/BF00934676

Motivation

Single-machine sequencing is the base case of deterministic scheduling theory. Many multi-machine and shop problems are analysed by reduction to it, and many bounds and approximation algorithms for harder models use it as a subroutine. A central objective class is the bottleneck or minmax objective. Each job carries a nondecreasing cost of its completion time, and the schedule is judged by its worst job. Maximum lateness, maximum tardiness and maximum weighted tardiness are all special cases.

Before 1973 the minmax problem was solved without precedence constraints. Jackson (1955) showed that ordering by due date minimizes maximum lateness. Moore (1968, Management Science 15(1)) gave a procedure for general nondecreasing deferral costs, and Lawler and Moore (1969) gave a related method. In Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5), 1973, Lawler showed that arbitrary precedence constraints can be added at no loss of efficiency. Jobs are chosen from last to first, by a single comparison of costs at a known time. The resulting $O(n^2)$ procedure is the standard algorithm for the problem written $1\,|\,\mathrm{prec}\,|\,f_{\max}$ in the classification of Graham, Lawler, Lenstra and Rinnooy Kan (1979). It is one of the first polynomial-time results for precedence-constrained scheduling that every survey of the field cites.

Setting

A finite, nonempty set $J$ of jobs is processed on a single machine, one job at a time and without interruption. Each job $j$ has a processing time $a_j \ge 0$ and a cost function $c_j : \mathbb{R} \to \mathbb{R}$ that is monotone nondecreasing. The value $c_j(t)$ is the cost incurred when $j$ is completed at time $t$.

The precedence constraints are an arbitrary relation $\prec$ on jobs: $i \prec j$ means that job $i$ is required to precede job $j$. A sequence $\pi = (\pi_1, \dots, \pi_n)$ lists every job of $J$ once. It observes the precedence constraints if $\pi_q \prec \pi_p$ never holds for positions $p < q$. The machine starts at time $0$ with no idle time, so the completion time of $\pi_m$ is $C_{\pi_m}(\pi) = a_{\pi_1} + \dots + a_{\pi_m}$. The maximum incurred cost of $\pi$ is

and a feasible $\pi$ is minmax optimal if $f_{\max}(\pi) \le f_{\max}(\pi')$ for every feasible $\pi'$.

For a set $P$ of jobs, $S(P)$ is the set of jobs of $P$ that are not required to precede any other job of $P$, and $T_P = \sum_{j \in P} a_j$. Lawler's rule builds a sequence from the last position to the first. With $P$ the jobs not yet placed, it chooses $k \in S(P)$ with $c_k(T_P) = \min_{j \in S(P)} c_j(T_P)$, places $k$ in the latest open position and removes it from $P$. Ties are broken arbitrarily. In Lean the objects are IsFeasible, lastEligible ($S$), IsMinmaxOptimal and IsLawlerSequence, in namespace LawlerPrec.MinMax. They are built on the published MooreLateJobs.Shared.completionTime and MooreLateJobs.MaxDeferral.maxCost.

Formalization targets

Goal: the rule is optimal

Every sequence $\pi$ that Lawler's rule can produce, under any tie-breaking, observes the precedence constraints and satisfies

This is the statement of §3 (p. 545), "An efficient algorithm for finding a minmax optimal sequence follows immediately from the theorem above". It contains no constants.

Milestones

1. §2 proof, third paragraph. Moving a job of $S(J)$ to the end of a feasible sequence keeps it feasible.
2. §2 proof, fourth paragraph, first sentence. After that move, no job other than $k$ completes later, and $k$ completes at $T = \sum_{j \in J} a_j$.
3. §2 proof, fourth paragraph. If $c_k(T) \le c_{k'}(T)$, where $k'$ is the last job of the feasible sequence, the move does not raise $f_{\max}$.
4. THEOREM (§2), p. 544. If some feasible sequence exists and $k \in S(J)$ minimizes $c_j(T)$ over $S(J)$, then some minmax optimal sequence has $k$ last.
5. §3, the reduction. A minmax optimal sequence of $J \setminus \{k\}$, followed by $k$, is minmax optimal for $J$.
6. §3, the procedure never stalls. If a feasible sequence exists, the rule produces a complete sequence. This shows the goal is not vacuous.

Significance

The result shows that $1\,|\,\mathrm{prec}\,|\,f_{\max}$ is solvable in polynomial time for every family of nondecreasing costs. The ordering of an optimal sequence depends on the costs only through their values at the $n$ partial sums $T_P$ along the way. The deadline problem is a corollary (§5): sequencing from last to first by latest deadline among the currently available jobs avoids tardiness whenever any sequence does. The last-to-first scheme is reused in later backward rules for $f_{\max}$ objectives. A formal statement of the rule, its feasibility and its optimality makes these extensions available for formal reuse.

The result is classical and its proof is short. No machine-checked proof of it is known to be in Mathlib. The work this mission asks for is a formal proof of the known exchange argument and of the induction that turns the Theorem into the algorithm's correctness. The induction needs the reduced problem's sets $S(P)$ and times $T_P$ to be the correct ones at each stage, which the definitions fix.

Difficulty

The exchange argument of §2 is elementary. The difficulty lies in stating the algorithm faithfully and carrying the induction. At each stage the eligible set $S(P)$ and the time $T_P$ must be recomputed on the remaining jobs, with constraints into already placed jobs ignored. The induction must also show that the rule's sequence is feasible, which is a conclusion and not an assumption.

A first attempt often proves only the Theorem, that some optimal sequence has $k$ last. That statement says nothing about a sequence built entirely by the rule, because an optimal sequence of $J$ with $k$ last need not restrict to an optimal sequence of $J \setminus \{k\}$. Optimality of the rule's whole sequence is the target, and milestone 5 isolates the corresponding step of the page.

Formalization scope

• Jobs form a type ι with decidable equality, and the job set is J : Finset ι.
• Processing times are a : ι → ℝ, costs are c : ι → ℝ → ℝ, and the precedence constraints are prec : ι → ι → Prop.
• A sequence is a duplicate-free list whose elements are exactly J. Positions are 0-based, and completion times are prefix sums (MooreLateJobs.Shared.completionAt).
• The relation prec is arbitrary: it is not assumed transitive, irreflexive or acyclic. A cycle among distinct jobs leaves no feasible sequence. A self-loop constrains nothing, both in feasibility and in $S$ (the "others" of the page exclude the job itself).

The standing assumptions of §1 appear as hypotheses wherever they are used: monotone nondecreasing $c_j$ for $j \in J$, and $J$ nonempty where the maximum is taken. Two hypotheses are added relative to the page and disclosed in each statement. Processing times are non-negative ($a_j \ge 0$), since they are durations and the exchange argument fails without them. The Theorem also assumes the existence of a feasible sequence, which its conclusion presupposes.

The rule is the property IsLawlerSequence of a finished sequence. At each position $m$, the job there lies in $S$ of the jobs in positions $0..m$ and minimizes the cost at their total processing time. Every tie-break is covered. The rule is not a deterministic function, and it is not an arbitrary choice function. Feasibility of the rule's output is part of the goal's conclusion, so the goal cannot be obtained by assuming it. A statement that compares the rule only with some sequence, or that asserts only that an optimal sequence exists, is weaker and is ruled out by the goal's form. Milestone 6 shows the goal's hypotheses are satisfiable whenever a feasible sequence exists.

The $n^2$ operation count of §4, the first-to-last rule of §5 and the deadline corollaries of §5 are not part of this mission. A development needs only finite lists and finsets from Mathlib. Lemmas about moving an element to the end of a duplicate-free list, and about prefix sums under that move, are reusable for other exchange arguments in single-machine scheduling.

Selected references

• E. L. Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5):544–546, 1973. https://doi.org/10.1287/mnsc.19.5.544
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1):102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• E. L. Lawler and J. M. Moore, A Functional Equation and its Application to Resource Allocation and Sequencing Problems, Management Science 16(1):77–84, 1969. https://doi.org/10.1287/mnsc.16.1.77
• J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
• R. L. Graham, E. L. Lawler, J. K. Lenstra and A. H. G. Rinnooy Kan, Optimization and Approximation in Deterministic Sequencing and Scheduling: a Survey, Annals of Discrete Mathematics 5:287–326, 1979. https://doi.org/10.1016/S0167-5060(08)70356-X

Motivation

A set function $f : 2^{\mathcal N} \to \mathbb R$ on a finite ground set $\mathcal N$ is submodular if it has diminishing returns, equivalently if $f(A) + f(B) \ge f(A \cup B) + f(A \cap B)$ for all $A, B \subseteq \mathcal N$. Cut functions of graphs and hypergraphs, coverage functions, entropy, and many facility-location and welfare objectives are submodular. Unconstrained Submodular Maximization (USM) asks, given a nonnegative submodular $f$ through a value oracle, for a set $S \subseteq \mathcal N$ of maximum value. It contains Max-Cut, Max-DiCut and Max Facility Location as special cases, and it is a subroutine in algorithms for constrained submodular maximization.

Timeline:

• Feige, Mirrokni and Vondrák (FOCS 2007; SIAM J. Comput. 2011) gave a uniformly random set achieving $1/4$ of the optimum, a deterministic local search achieving $1/3 - \varepsilon/n$, a randomized local search achieving $2/5$, and proved that no algorithm making polynomially many value queries achieves $1/2 + \varepsilon$.
• Oveis Gharan and Vondrák (SODA 2011) improved the ratio to about $0.41$ by simulated annealing; Feldman, Naor and Schwartz (ICALP 2011) to about $0.42$.
• Buchbinder, Feldman, Naor and Schwartz (FOCS 2012; SIAM J. Comput. 2015) gave the double greedy algorithms: a deterministic linear-time $1/3$-approximation (this mission) and a randomized linear-time $1/2$-approximation, matching the query lower bound.

Setting

Let $\mathcal N$ be a finite ground set and $f : 2^{\mathcal N} \to \mathbb R_{\ge 0}$ a nonnegative submodular function. Write $f(OPT) = \max_{S \subseteq \mathcal N} f(S)$, and let $OPT$ denote a set attaining it.

Algorithm 1 (DeterministicUSM) fixes an arbitrary order $u_1, \dots, u_n$ of $\mathcal N$ and maintains two solutions, starting from $X_0 = \emptyset$ and $Y_0 = \mathcal N$. In iteration $i = 1, \dots, n$ it computes

If $a_i \ge b_i$ it sets $X_i = X_{i-1} \cup \{u_i\}$, $Y_i = Y_{i-1}$; otherwise $X_i = X_{i-1}$, $Y_i = Y_{i-1} \setminus \{u_i\}$. A tie adds $u_i$. After $n$ iterations $X_n = Y_n$, which is the output.

The analysis uses the hybrid sets $OPT_i = (OPT \cup X_i) \cap Y_i$, which agree with $X_i$ and $Y_i$ on $u_1, \dots, u_i$ and with $OPT$ on $u_{i+1}, \dots, u_n$. In Lean, the run is state f l i, the state $(X_i, Y_i)$ after the first $i$ entries of the order l, and $OPT_i$ is optI O (state f l i).

Formalization targets

Goal: Theorem I.1

For every nonnegative submodular $f$ and every order of $\mathcal N$,

Milestones

1. Lemma II.1. For every $1 \le i \le n$, $a_i + b_i \ge 0$.
2. The hybrid sequence. $OPT_i$ agrees with $X_i, Y_i$ on $u_1, \dots, u_i$ and with $OPT$ on the rest; $OPT_0 = OPT$ and $OPT_n = X_n = Y_n$.
3. Lemma II.2. For every $1 \le i \le n$,

4. The telescoped display. $f(OPT_0) - f(OPT_n) \le [f(X_n) - f(X_0)] + [f(Y_n) - f(Y_0)] \le f(X_n) + f(Y_n)$.
5. Theorem II.3 (tightness). For every $\varepsilon > 0$ there is a nonnegative submodular $f$ with $f(OPT) > 0$ and an order on which $f(X_n) \le (1/3 + \varepsilon)\, f(OPT)$.

Significance

The result. Algorithm 1 is the deterministic member of the double greedy family. It makes one pass over the ground set with four value queries per element, and it guarantees $1/3$ of the optimum for every order, without the polynomial-but-large running time and the $\varepsilon/n$ loss of local search. Its analysis, which charges the decrease of $f(OPT_i)$ to the increases of $f(X_i)$ and $f(Y_i)$, is the template the paper then refines into the randomized $1/2$-approximation (Theorem I.2) and its continuous counterpart on the multilinear extension. Theorem II.3 shows that $1/3$ is the exact ratio of this algorithm, so the improvement to $1/2$ requires randomization (or a different deterministic rule) rather than a sharper analysis.

Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal statement of the algorithm as printed, a checked proof of its guarantee for every order, and a checked tight instance. The definitions of the run and of $OPT_i$ are the same objects the randomized and fractional analyses reason about, so a complete development here is the first step toward the paper's main theorem.

Difficulty

The individual inequalities are short; the difficulty lies in the bookkeeping. Each step needs the invariants $X_{i-1} \subseteq Y_{i-1}$ and $u_i \in Y_{i-1} \setminus X_{i-1}$, which follow from the order being an enumeration (no repetitions, every element present), and the identification of $OPT_i$ from $OPT_{i-1}$ in each branch of the algorithm. Summing Lemma II.2 needs a telescoping over the run defined as a fold. The naive idea of comparing $f(X_n)$ with $f(OPT)$ directly, without the hybrid sets, gives no bound: the greedy choices are made against $X$ and $Y$, not against $OPT$. For Theorem II.3 the difficulty is producing an explicit instance, checking that it is submodular and nonnegative, and tracing the run, including the ties, which the algorithm resolves by adding.

Formalization scope

• The ground set is a finite type X with decidable equality; subsets are Finset X; $f$ is real valued, Finset X → ℝ, and nonnegativity is the hypothesis ∀ S, 0 ≤ f S where the page uses it (the goal, the telescoped display and the tight example). Lemma II.1, Lemma II.2 and the hybrid-sequence milestone do not assume it.
• Submodularity is the lattice form $f(A) + f(B) \ge f(A \cup B) + f(A \cap B)$ of the paper's footnote 1, through the published definition NonmonotoneSubmod.Shared.Submodular. The paper's main-text sentence ("for every $A \subseteq B \subseteq \mathcal N$ and $u \in \mathcal N$") would force monotonicity when $u \in B \setminus A$ and is read as the footnote. $f(OPT)$ is the published NonmonotoneSubmod.Shared.OPT f, the maximum of $f$ over all subsets.
• The order $u_1, \dots, u_n$ is a list l with l.Nodup and ∀ x, x ∈ l; $u_i$ is l[i - 1]. Every statement quantifies over all such lists. No nonemptiness of $\mathcal N$ is assumed: for an empty ground set the goal reads $f(\emptyset) \le 3 f(\emptyset)$.
• The tie rule is line 5's $a_i \ge b_i$: ties add $u_i$.
• Where a milestone mentions an optimal solution, it takes a set O with ∀ S, f S ≤ f O.
• The goal is stated multiplied out, $f(OPT) \le 3 f(X_n)$, because $f(OPT)$ may be $0$.
• Trivializing formalizations ruled out. The paper's Theorem I.1 reads "there exists a deterministic linear time $(1/3)$-approximation algorithm"; without the running time that existential is satisfied by exhaustive search, so the goal is the guarantee of the printed Algorithm 1 for every order. Running time is not formalized: the algorithm evaluates $f$ on four sets per element, $n$ elements in all. Theorem II.3 requires $f(OPT) > 0$, without which $f \equiv 0$ would satisfy it.
• Needed infrastructure: elementary lemmas on List.foldl over List.take, on membership in the states of the run, and on telescoping sums over $1 \le i \le n$. A reusable lemma "the run keeps $X_i \subseteq Y_i$ and decides exactly $u_1, \dots, u_i$" would serve all three missions of this paper. Contributions of proofs of any milestone, of the goal from the milestones, and of the tight instance (e.g. the paper's five-vertex directed cut function) are welcome.