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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A matching pairs up nodes of a graph along its edges, each node being used at most once. Finding a largest matching is the model problem of combinatorial optimization: the obvious linear relaxation is not integral on non-bipartite graphs, and the methods developed for it (augmenting paths, odd-circuit shrinking, polyhedral descriptions) became standard across the field. A good algorithm for this problem needs a way to know when to stop, which means a short certificate that a given matching cannot be enlarged.
The history of that certificate is short. Tutte (1947) characterized the graphs with a perfect matching. Berge (1957) proved that a matching is maximum exactly when it has no augmenting path, and Berge (1958) stated the min-max formula for the maximum size of a matching, which is equivalent to Tutte's theorem. Edmonds (1965) introduced the shrinking of odd circuits and gave the first polynomial-time algorithm.
This mission formalizes §5.1 of Cook, Cunningham, Pulleyblank and Schrijver, Combinatorial Optimization (Wiley, 1998), pp. 127–133, where the formula is proved through odd-circuit shrinking.
A graph has finite sets of nodes and edges, each edge having an unordered pair of ends. Loops and parallel edges are allowed. A matching is a set of non-loop edges such that no node is incident with two edges of . A node incident with no edge of is -exposed. The maximum size of a matching is , and is the least number of exposed nodes.
For , the graph is obtained by deleting and all edges incident with it, and is the number of connected components of with an odd number of nodes. A circuit is a closed path with distinct edges and distinct inner nodes, of length at least one; a loop is a circuit of length one.
For an odd circuit , the graph is obtained by shrinking : the nodes of are replaced by one new node , the edges with both ends in are removed, and every other edge keeps its identity with any end in moved to the new node. An odd circuit is tight if . A node is inessential if some maximum matching misses it, and essential otherwise.
The goal asserts that both optima exist and coincide.
In the order of the source:
The formula gives every instance a certificate: a matching and a set with prove each other optimal. It gives a good characterization of the maximum matching problem, it specializes to König's theorem on bipartite graphs, and it is the starting point of the Gallai–Edmonds structure theory.
The theorem is classical and proved. What this mission adds is a machine-checked min-max formula. Tutte's theorem is formalized in Mathlib as SimpleGraph.tutte, and on the platform as FamousTheorems.tutte_theorem; Berge's augmenting path theorem is BergeMatching.Core.theorem_1; the odd-set-cover form of matching duality is PathsTreesFlowers.Duality.matching_duality_theorem. All of those concern other forms of the result, and the first two concern simple graphs. The formula in the form above, and the shrinking statements on graphs with parallel edges, are not on the platform.
The obvious certificate fails. In a bipartite graph a node cover of the size of a maximum matching exists, but an odd circuit of length has maximum matching size and minimum cover size . So the upper bound has to count odd components, and showing that it is attained is the entire content of the theorem.
Shrinking does not simply reduce the problem either: inequality (5.2) can be strict, since not every odd circuit is tight. The relation between and is an equality only for special circuits. Passing between and also changes the type of the nodes, which a formal development has to carry through.
The graph is CombOpt.TutteBerge.Multigraph V E, with ends : E → Sym2 V, and every theorem assumes [Finite V] [Finite E]. Sets of nodes and edges are Set, and cardinalities are Set.ncard and Nat.card. The Mathlib SimpleGraph type cannot be used throughout, because Proposition 5.4 says , which requires the edges of to be edges of , and has parallel edges.
G.shrink S, with node type Option {v // v ∉ S}, the new node being none, and edge type the subtype of E outside .G.toSimple, so Mathlib's SimpleGraph.oddComponents applies.ℚ after casting, so nothing truncates. Counting identities in ℕ are written with addition.A definition of oc under which every component counted, or matchings allowed to contain loops, would change the theorem; the definitions above exclude both.
The multigraph layer (paths, circuits, deletion, shrinking) is reusable by the T-join and matching-polytope missions of this series. Bridges to SimpleGraph are welcome, in particular a transfer of SimpleGraph.tutte and BergeMatching.Core.theorem_1 along Multigraph.toSimple, as are proofs of the Tutte–Berge formula by other routes than the book's.
Mathlib/Combinatorics/SimpleGraph/Tutte.lean. https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Combinatorics/SimpleGraph/Tutte.leanInteger programming asks for the best integral point of a polyhedron, and the standard way to attack it is to describe the convex hull of those integral points by linear inequalities. A simple rule produces such inequalities: if is an integral vector and holds on a polyhedron , then is an integer at every integral point of , so also holds there. This rounding rule underlies Gomory's cutting-plane algorithm and much of polyhedral combinatorics; Edmonds' blossom inequalities for matchings arise from a single round of it.
The history runs as follows.
This mission formalizes the statements of §6.7 of Cook, Cunningham, Pulleyblank and Schrijver, the tenth mission in a series on that book.
Work in . A polyhedron is the solution set of a finite linear system; it is a rational polyhedron if some rational system defines it, and a polytope if it is bounded. For , a Gomory–Chvátal cutting plane for is an inequality
The closure is the set of all vectors of satisfying every Gomory–Chvátal cut for . The iterates are and , and the integer hull is the convex hull of the integral vectors in . Since no cut removes an integral vector of ,
Given a system and nonnegative reals for which is integral, the inequality is derived from the system. A cutting-plane proof of is a sequence of inequalities, each derived from the system together with the earlier inequalities of the sequence, whose last inequality is .
For every rational polytope there is an integer with
The least such is the Chvátal rank of . The statement asserts finiteness only and fixes no bound on .
The theorem turns the rounding rule into a complete method: the linear description of the integer hull of a rational polytope can in principle be reached by rounding alone, without any other integrality argument. Theorem 6.32 is an integer analogue of Farkas' Lemma, giving a finite certificate that a rational polytope has no integral vector. Chvátal rank is also a measure of difficulty: the fractional matching polytope has rank 1, and rank bounds are a standard tool for comparing relaxations and proof systems.
All these results are proved in the literature. None of them has a machine-checked proof on the platform; the related items CookSensitivity.ChvatalRank.chvatalIter_eq_empty_of_no_integer_point and chvatalIter_subset_halfspace are explicit-bound statements over and are open. A completed mission provides cutting-plane proofs, closures and integer hulls in as reusable objects for later work on integer programming and polyhedral combinatorics.
The natural idea is induction on dimension: push inward by rounding, and handle the face where it is tight by the induction hypothesis. The obstacle is that a cut for a face is not a cut for the polytope. On a face, an inequality may be derived using equations, whose multipliers have no sign, and a negative multiplier does not give a derivation from the system defining . Theorem 6.34 has a separate obstacle: the definition quantifies over infinitely many inequalities, with real multipliers and real right-hand sides, and nothing in that definition shows that finitely many are enough.
Fin n → ℝ. The polyhedron is the published definition RobustToDynamics.polyhedron. The published CookSensitivity_ChvatalRank_ChvatalClosure is not reused because it lives in , while the book's sets, multipliers and right-hand sides are real.A complete development needs Farkas' Lemma in several forms, faces of rational polyhedra and their description by subsystems, dimension of polytopes, and finiteness of the set of integral points of a polytope. The polyhedral layer and the cutting-plane calculus are reusable beyond this mission. Contributions are welcome at every milestone, and intermediate lemmas on faces and on derivations under rescaling of systems are useful in their own right.
A matching in a graph is a set of edges no two of which share an end. Finding a matching of maximum total weight is one of the basic problems of combinatorial optimization: it models pairing tasks (assigning workers, pairing pen movements of a plotter, the postman and T-join problems of the same book) and it sits inside many algorithms as a subroutine. The standard way to understand such a problem is to describe the convex hull of its feasible solutions by linear inequalities. Once that description is known, the combinatorial problem is a linear program, and linear programming duality gives a min-max theorem that certifies optimality.
For matchings this description is a theorem of Edmonds (Edmonds 1965). It was the first complete linear description of a combinatorially defined polytope whose naive relaxation is not integral, and it introduced the blossom inequalities that every later work on matching polyhedra builds on. This mission formalizes the statement in the form of Cook, Cunningham, Pulleyblank and Schrijver, Combinatorial Optimization (Wiley, 1998), Chapter 6, together with the general polyhedral results of §6.1 to §6.3 that the book develops for it.
Timeline:
A graph has a finite node set , a finite edge set , and for each edge an unordered pair of ends. Parallel edges are allowed; a loop is an edge whose two ends coincide. For , the cut is the set of edges with one end in and one end outside , and is the set of edges with both ends in ; . For and , .
A matching has the characteristic vector , with for and otherwise. The matching polytope is
and the system (6.7) is
A polyhedron is the solution set of finitely many linear inequalities; a polytope is a bounded polyhedron. An inequality is valid for if every point of satisfies it. A face of is for a valid inequality with meeting , together with and ; a proper face is a face other than and ; a facet is a maximal proper face; a vertex is a point with a face. The dimension of a set is one less than the largest size of an affinely independent subset, so . An inequality induces the face .
Both inclusions are asserted. The printed theorem says "for any graph"; it fails for a graph with a loop (one node with one loop: , but (6.7) only says ), so the goal assumes loopless and allows parallel edges.
The theorem makes maximum-weight matching a linear program over (6.7). Combined with LP duality it gives the min-max formula for weighted matching that the blossom algorithm certifies, and it is the template for the other polyhedral results of the book: T-joins (Chapter 5), b-matchings (Exercise 6.8), and the matroid polytopes of Chapter 8. Theorems 6.10, 6.11, 6.17 and Corollary 6.19 are the general facts that turn "the convex hull is described by these inequalities" into a method: show that every facet of the hull is induced by one of the listed inequalities.
Status: all results here are classical and proved in the literature. Formal status on Prove2Me: the inclusion "" of the perfect matching polytope theorem for loopless multigraphs with an even number of nodes is proved (OAI.MatchingEntropy.LooplessGraph.constraint_subset_polytope_aux), in another vocabulary; the matching polytope theorem, its facet argument, and the face/facet theory of §6.2–6.3 in the book's vocabulary are not formalized there. Mathlib has convex hulls, affine independence and Carathéodory's theorem but no polyhedra, faces or facets at the pinned revision.
The inclusion is a counting argument. The converse is the content. The natural first attempt, showing that every vertex of the polytope defined by the degree constraints is integral, fails: on an odd circuit the vector is a vertex of . The blossom inequalities cut these points off, but the argument that no other fractional vertices remain needs either the weighted blossom algorithm or the facet argument of the book, which requires the facet theory of §6.3 (Proposition 6.16, Theorem 6.17) and a combinatorial exchange of alternating paths between two matchings (the case leading to (6.9)).
Graphs are finite multigraphs: Graph V E with ends : E → Sym2 V; parallel edges are distinct elements of E; a loop has a diagonal pair of ends. The goal, Theorem 6.3 and (6.9) assume G.IsLoopless. Vectors live in ι → ℝ for a finite type ι (E for ); w ⬝ᵥ x is ; convexHull ℝ is Mathlib's convex hull, equal to the book's conv.hull on finite sets. Dimension is integer valued with . A proper face is neither nor . In (6.9), the inequality (6.8) is assumed valid for , as the proof uses.
The goal is a set equality; stating only "" would drop the theorem. Every definition is the book's (pp. 199–214), one declaration per module, in the namespace CombOpt.MatchingPolytope. The polyhedral layer (polyhedron, polytope, face, facet, vertex, dimension, minimal system) is independent of graphs and is reusable for later chapters on integral polyhedra and total unimodularity. Contributions welcome: proofs of any milestone, and the auxiliary facts the book leaves as exercises (Proposition 6.7, Proposition 6.15, Exercise 6.2).
A minimum spanning tree (MST) of a connected graph with edge costs is a cheapest set of edges that connects all nodes and contains no circuit. It is the prototype of a combinatorial optimization problem solved exactly by a greedy rule, and it opens Chapter 2 of Cook, Cunningham, Pulleyblank and Schrijver's Combinatorial Optimization (Wiley, 1998). The chapter proves that Kruskal's and Prim's algorithms are correct and then ends with a theorem of Edmonds (Edmonds 1971): the MST problem is a linear program. The characteristic vector of any MST is an optimal solution of an explicit linear program with one constraint for every nonempty set of nodes. This is the book's first instance of its central theme, that a good algorithm comes with a linear-programming description whose optimal solutions are integral, and the same linear program reappears in Chapter 7 as the subtour relaxation of the traveling salesman problem.
This mission is the first of a series formalizing the book's capstone theorems.
A graph has a finite set of nodes, a finite set of edges, and for every edge an unordered pair of ends. Parallel edges (equal ends) and loops (an edge whose two ends coincide) are allowed. A path from to is a sequence in which the ends of are and ; it is simple if its nodes are distinct. A circuit is a closed path with distinct edges, distinct nodes and ; a loop is a circuit of length 1 and two parallel edges form a circuit of length 2.
For , the spanning subgraph is connected if any two nodes are joined by a path with edges in , and is a forest if it has no circuit. A spanning tree is a set with a connected forest. For real costs (negative costs allowed), an MST is a spanning tree minimizing .
For , the cut is the set of edges with one end in and one in , and is the set of edges with both ends in . For , .
Kruskal's Algorithm starts from , repeatedly adds to a least-cost edge such that is still a forest, and stops when is a spanning tree.
Let be an MST of for the costs , , and let be its characteristic vector. Then is an optimal solution of
The goal leaves the costs completely free (any signs, any ties) and the graph arbitrary (loops and parallel edges included).
The result. Theorem 2.8 says that the polytope cut out by (2.2)–(2.4) has, for every cost vector, an optimal vertex that is the characteristic vector of a spanning tree. Consequently the optimal value of the linear program equals the MST cost, the LP gives a certificate of optimality for an MST through LP duality, and the system (2.2)–(2.4) is the starting point for the spanning-tree polytope and, through matroid theory (Chapter 8 of the book), for Edmonds' matroid polytope theorem. In Chapter 7 the same constraints give the subtour lower bound for the traveling salesman problem.
Formalizing it. All results here are classical and fully proved in the book. What this mission adds is a machine-checked development for multigraphs with loops and parallel edges, with paths and circuits defined exactly as in the book. Existing formal developments of MST correctness (in Mathlib and on this platform) work with simple graphs; the LP characterization of Theorem 2.8 has, as far as a search of the platform shows, no formal statement. Theorem 2.6 is stated for the nondeterministic algorithm, so it covers every tie-breaking rule at once.
The milestones are elementary but bookkeeping-heavy: paths are sequences with repeated nodes and edges, and the passage from a path to a simple path or a circuit (needed in Lemma 2.1 and Lemma 2.7) is where most of the work sits. Theorem 2.8 is not a counting argument. Feasibility of is easy; optimality requires comparing with every fractional feasible point. The book's proof replaces (2.2) by the equivalent family indexed by edge sets and then builds an explicit dual solution from the order in which Kruskal's Algorithm scans the edges, so it needs LP weak duality or complementary slackness together with the structure of the components of the prefixes of that order. A proof by enumerating vertices of the polytope does not work directly, because integrality of the vertices is itself the content of the theorem.
A graph is a structure with ends : E → Sym2 V over finite types V and E; it is not Mathlib's SimpleGraph. Paths are an inductive type Graph.Walk with lists of edges and nodes; spanning subgraphs, forests and spanning trees are given by edge sets Finset E. Costs and LP variables are real. (2.2) is imposed for every nonempty , which gives the same feasible set as the printed since the case is implied by (2.3). Optimality is stated as feasibility plus for every feasible ; no infimum is used.
Lemma 2.2 and Theorem 2.8 assume nonempty. For the graph with no nodes the empty edge set is a spanning tree with edges, so both printed statements fail there; this is the only correction. Loops are kept: (2.2) with forces on a loop at , so a loop of negative cost cannot lower the LP value, and the statement is not trivialized.
Contributions welcome: proofs of the milestones, a reusable library of multigraph paths and circuits, LP duality on finite index sets for the goal, and alternative proofs of Theorem 2.8 (for example through the Prim order or matroid greedy arguments).
A mail carrier must walk every street of a district and return to the post office, and wants to walk as little as possible. Kwan Mei-Ko posed this Chinese postman problem in 1962. Edmonds observed that the extra streets to be walked a second time form a set of edges whose odd-degree nodes are exactly the odd-degree nodes of the street graph, and generalized the question to -joins: edge sets with a prescribed set of odd-degree nodes. The same object describes shortest paths in undirected graphs with negative edge costs but no negative circuits (), negative-circuit detection (), and, through planar duality, maximum cuts in planar graphs and via minimization in VLSI layout.
The central polyhedral fact is that the minimum cost of a -join is the optimal value of an explicit linear program. Edmonds and Johnson (Matching, Euler tours and the Chinese postman, Math. Programming 5 (1973)) proved it for nonnegative costs with the -cut relaxation. For costs of arbitrary sign, a relaxation with the additional "-twisted" cut constraints is exact. This mission formalizes Section 5.4 of Cook, Cunningham, Pulleyblank and Schrijver, Combinatorial Optimization (Wiley, 1998), which proves both statements (Theorems 5.28 and 5.30), together with Edmonds' perfect-matching linear program (Theorem 5.13) on which the proof rests.
Timeline:
A graph has finite node and edge sets, each edge having an unordered pair of ends; parallel edges and loops (both ends equal) are allowed. For , the cut is the set of edges with one end in and one end in ; . A loop lies in no cut. For and , , and .
Let with even. A -join is a set with
A set is -odd if is odd, and then is a -cut. The two linear programs are
A perfect matching is a set of edges such that every node is an end of exactly one of them. Edmonds' linear program (5.13) minimizes subject to for every node, for every odd set whose cut is not a star , and .
For every graph , every with even, and every ,
Both sides are taken in the extended reals; if has no -join both sides are .
Theorem 5.30 says that the polytope described by (5.37) is the convex hull of the characteristic vectors of -joins, seen through every linear objective. It gives a polynomial-size certificate of optimality for -joins with negative costs, hence for shortest paths in undirected graphs with negative edges, for maximum cuts in planar graphs, and for the postman problem. It is the base of the book's follow-up results on -factors and the "-join polytope" (Theorems 5.31, 5.32 and 6.5). Theorem 5.13 is Edmonds' perfect-matching theorem in linear-programming form.
All results here are classical and proved. The matching-polytope inclusion behind Theorem 5.13 is machine-checked on the platform for loopless multigraphs (OAI.MatchingEntropy.LooplessGraph.constraint_subset_polytope_aux), and Edmonds–Johnson's postman polyhedron for odd-degree terminals in an integer model (ChinesePostman.Polyhedron.postman_polyhedron). No machine-checked proof of the -join theorems in the form stated here (arbitrary , multigraphs, arbitrary costs) is known. This mission produces the -join layer on multigraphs and the two LP equalities.
The inequality "" in Theorems 5.28 and 5.30 is elementary: characteristic vectors of -joins are feasible (milestones 5, 6, 8). The reverse inequality needs a dual solution of the same value, and the obvious attempt fails. Rounding an optimal fractional of (5.33) does not work, since its vertices are not integral in general; the book instead reduces the case to minimum-weight perfect matching on the complete graph with shortest-path distances, uses Theorem 5.13 there, and reduces general to by attaching zero-cost pendant edges. For negative costs, (5.33) is unbounded and cannot be used directly; the proof replaces by , by with the odd nodes of the negative edges, and transports an optimal dual of (5.33) through complementary slackness to a dual of (5.37). Each step needs LP duality and an exact combinatorial correspondence.
Graphs are CombOpt.TJoin.Graph V E with ends : E → Sym2 V over finite types, allowing loops and parallel edges; it is not a SimpleGraph. Cuts are Finsets of edges, and loops are in no cut, so a loop never affects -join parity and occurs in (5.37) only in . All optimal values are infima in EReal: the minimum cost of a -join is when none exists, and the LP values are when infeasible. The equality then also asserts that the LP is infeasible exactly when no -join exists. Constraints over "-cuts" and over "" are listed through the node sets that define them. Costs are real and of arbitrary sign in Theorem 5.30. Every theorem assumes even, as the book does.
Theorem 5.13 is stated for loopless graphs: with a loop of negative cost, (5.13) is unbounded while the minimum-weight perfect matching is finite. A formalization that fixed , nonnegative costs, simple graphs, or that assumed a -join exists would not be the theorem.
A complete development needs parity counting on cuts, path decompositions of edge sets, LP duality and complementary slackness for finite systems (on the platform: MatousekLP.Duality.duality_theorem), and Edmonds' matching theorem. The -join layer (cuts, joins, path packings) is reusable for the postman problem, planar maximum cut and -matching missions. Proofs of the milestones, alternative proofs of Theorem 5.28 through the Edmonds–Johnson primal–dual algorithm, and integrality refinements (Seymour's Theorem 5.29) are welcome.
Many combinatorial optimization problems (bipartite matching, maximum flow, shortest paths, transportation and assignment problems) can be written as integer programs
whose constraint matrix has a special structure. Integer programming is hard in general, but linear programming is not. For a whole class of matrices the two coincide: dropping the constraint changes nothing, because the polyhedron of the linear relaxation has integral vertices. Total unimodularity is the property of that guarantees this for every integral right-hand side , and the Hoffman–Kruskal theorem says it is the only such property.
This mission is Section 6.5 of W. J. Cook, W. H. Cunningham, W. R. Pulleyblank and A. Schrijver, Combinatorial Optimization (Wiley, 1998), together with the facts from §6.2 and §6.4 it rests on.
Timeline.
All vectors live in . A polyhedron is a set for a real matrix and (equations and sign constraints are allowed, as pairs of inequalities). An inequality is valid for if every point of satisfies it; if moreover and , the hyperplane is supporting. A face of is the intersection of with a supporting hyperplane; by convention and are faces too (IsFace). A minimal nonempty face is a nonempty face containing no other nonempty face (IsMinimalNonemptyFace).
A rational polyhedron is integral if every nonempty face contains an integral vector, a point of (IsIntegralPolyhedron). For a polyhedron with vertices, such as one inside , this says every vertex is integral.
A matrix is totally unimodular if every square submatrix has determinant , or (Mathlib's Matrix.IsTotallyUnimodular). In particular every entry is or . For an matrix of full row rank, a basis is a nonsingular submatrix formed by columns, and is unimodular if it is integral and every basis has determinant (IsUnimodular).
For an integral matrix ,
The result. Hoffman–Kruskal turns integrality of a family of polyhedra into a purely algebraic property of one matrix, and the property is checkable on many matrices that arise in practice: incidence matrices of bipartite graphs and of directed graphs, network matrices, interval matrices. Each of these yields at once a min-max theorem (König's theorem, max-flow min-cut with integral flows, Birkhoff's theorem on doubly stochastic matrices) and a polynomial-time algorithm through linear programming. The converse direction shows that no weaker matrix condition can serve the same purpose for all integral right-hand sides. Theorem 6.26 removes the nonnegativity constraints and is the version used for flow polyhedra with arbitrary bounds.
Formalizing it. All results are classical and fully proved in the book; none of them has a machine-checked proof on this platform. Mathlib defines total unimodularity and proves basic closure properties, but has no notion of the faces of a polyhedron, of integral polyhedra, or of the Hoffman–Kruskal and Veinott–Dantzig theorems. Related platform items prove one-directional or vertex-only variants for other systems (box-constrained polyhedra, LP optimality with a TU matrix); this mission states the two-sided characterizations with the book's face-based definition of integrality.
The "if" directions are linear algebra once vertices are understood: a vertex of is a basic solution , and Cramer's rule makes it integral when . The obstacle is the polyhedral layer: connecting the book's definition of a face (supporting hyperplanes) to subsystems of tight inequalities (Proposition 6.6) and to minimal faces as affine subspaces (Proposition 6.7), which requires linear programming duality or an equivalent argument. Without it, "every nonempty face contains an integral vector" cannot be reduced to a statement about square subsystems.
The "only if" directions need the right test vectors: to show a basis has determinant it is not enough to look at one ; one must choose with an integral shift making the vertex nonnegative, and then use that every column of is integral. A first attempt that only uses unit vectors fails because the corresponding polyhedra may be empty or the basic solution infeasible.
Vectors of are Fin n → ℝ, matrices are Matrix (Fin m) (Fin n) R, and on vectors is the pointwise order. Integral matrices have entries in ℤ and act on through their real cast; an integral vector is the cast of a Fin n → ℤ. Ranks and inverses are those of real matrices. A subsystem of is a finite set of row indices. Integrality is defined through faces exactly as on p. 219, not through vertices, so Theorem 6.26 covers polyhedra without vertices. Unimodularity includes full row rank, as in the book's definition, and allows an arbitrary finite column index so that (Matrix.fromCols A 1) is covered. Every integral is quantified in the characterizations, including those that make the polyhedron empty; the empty polyhedron is integral. The degenerate sizes and are included and the statements remain true there.
A complete development needs: the face lattice of a polyhedron and its description by tight subsystems (Propositions 6.6–6.7), vertices as basic solutions, Cramer's rule over , and the slack-variable reduction from inequality to equality form. The polyhedral layer (faces, minimal faces, integral polyhedra) is reusable by every later mission of this series on integral polyhedra (matching, matroid and matroid-intersection polytopes, Chvátal closures). Contributions of these intermediate lemmas, and of further TU examples such as incidence matrices of bipartite graphs, are welcome.
Many combinatorial problems reduce to one question: can a prescribed amount of material be routed through a network without breaking any arc limit? Transportation problems, assignment and scheduling constraints, and the feasibility phase of minimum-cost flow all take this form. Hoffman's circulation theorem (Hoffman, 1960) answers it with a certificate: if no feasible routing exists, a single set of nodes witnesses the failure.
This mission is the third of a series on W. J. Cook, W. H. Cunningham, W. R. Pulleyblank and A. Schrijver, Combinatorial Optimization (Wiley, 1998, DOI). It covers §3.2 and §3.3 of the book, printed pp. 38–42 and 54–55.
The historical line is short. Ford and Fulkerson (1956) and, independently, Kotzig proved the max-flow min-cut theorem. Gale (1957) gave the feasibility condition for prescribed node demands and capacities. Hoffman (1960) treated upper and lower bounds on the arcs.
A digraph has a finite node set and a finite arc set ; each arc has a tail and a head, and loops and parallel arcs are allowed. For , the cut is the set of arcs with tail in and head outside , and , so is the set of arcs entering . For , the net flow into is
A circulation is a vector with at every node. An -flow satisfies off , has value , and is feasible for capacities when . For a set of arcs, . A vector of bounds is integral when its finite components are integers. A path may repeat nodes and traverses each arc forward or in reverse; it is -incrementing when forward arcs have and reverse arcs have ; an -augmenting path is an -incrementing path from to .
Let and with . There is a circulation with if and only if
and if and are integral, there is an integral such circulation if and only if the same condition holds.
The theorem turns the existence of a circulation into a finite family of cut inequalities, and its integral clause gives integer solutions with no additional condition. Together these yield the feasibility tests behind transportation problems, and they are the entry point to the minimum-cost flow chapter of the book, which starts from a feasible flow. Corollary 3.16 is the form used for uncapacitated transshipment.
All these results are proved in the literature and in the book. What is new here is their machine-checked form at the book's generality. The platform already has formal proofs of narrower statements: FlowsNetworks.Feasibility.circulation_theorem assumes finite on a digraph without parallel arcs and has no integrality clause, FlowsNetworks.Feasibility.supply_demand_theorem has no integrality clause, and LinearOptimization.max_flow_min_cut requires positive capacities and no loops. This mission states infinite bounds on both sides, negative bounds, loops, parallel arcs and zero capacities, and it states the integral clauses as separate equivalences.
The necessity of the condition is a short summation; the difficulty lies in sufficiency. The obvious first idea is to apply a max-flow theorem with finite capacities, and this does not apply as it stands: the bounds may be negative or infinite, and with infinite capacities a maximum flow need not exist at all, which is why Theorems 3.5 and 3.7 carry that hypothesis. Theorem 3.15 as printed has finite capacities, whereas Theorem 3.17 has infinite upper bounds, so the goal is not literally a special case of it. The integral clause is a second obstacle: it does not follow from the real statement, since rounding a real circulation breaks conservation.
Nodes and arcs are finite types, with tail head : E → V, so that parallel arcs and loops are present. Flows are real vectors E → ℝ. Capacities of the flow results have type ℝ≥0∞, which is the book's range of "nonnegative real numbers or "; the bounds of the goal have type EReal, with hypotheses and . Because of these hypotheses, no sum in the goal mixes and , so the EReal convention for that sum never applies. In Theorem 3.15 capacities are finite and nonnegative, as printed.
Theorems 3.5 and 3.6 carry the hypothesis , a correction recorded on each item: for there is no -cut, and the one-node path would be augmenting for every flow. A path is a list of arcs with a direction flag, and a loop counts as forward as in the book. The goal is not trivialized by its conventions: every hypothesis is satisfiable (a verification file gives instances), and the integral clause is stated as its own equivalence, not as a consequence of the real one.
A complete development needs summation identities over cuts and a treatment of infinite bounds. The flow definitions are reusable by the minimum-cost flow chapter of the series. Contributions of any milestone, and proofs by any route, are welcome.
Many service systems face a finite population of customers whose arrival times follow a time-of-day pattern: a clinic between opening and closing, a polling station on election day, a concert venue before the show. Such a system never reaches a steady state, and its arrivals are not a Poisson process with a posited rate function. Chakraborty and Honnappa (arXiv:1906.06740v1) study the RS queue, a mechanistic model of this transitory traffic: each of potential customers samples an arrival epoch from a distribution and independently decides to turn up with probability . The queue length is then neither stationary nor Markov, so the strong approximations available for Markovian nonstationary queues (Mandelbaum–Massey 1995 and its extension to Markovian service networks by Mandelbaum, Massey and Reiman, 1998) do not apply.
Earlier work on the queue (the case ) proved functional laws of large numbers and central limit theorems (Honnappa–Jain–Ward, arXiv:1412.2321; Queueing Systems 80, 2015). The paper proves a functional strong approximation: on one probability space, the queue length stays within of an explicit reflected Gaussian process, almost surely and uniformly in time.
Fix . Customer samples an epoch with distribution function supported on , and a turn-up indicator . With , the arrival process is . Under Assumption 2.1, for all ; under Assumption 2.5, with .
Service requirements are iid with law , whose moment generating function is finite near , with mean and standard deviation . A single non-idling FCFS server works at rate . The offered load is , the remaining workload is with the reflection map , the busy time is the time in the workload is positive, and with the truncated renewal process the queue length is
The approximating objects are a Brownian bridge and standard Brownian motions , :
There is a version of the model — iid , iid Bernoulli, iid , Brownian motions common to all , Brownian bridges , with the three blocks independent — such that
for every positive sequence . One statement covers both arrival assumptions.
The milestones follow the proof: the KMT embeddings of the random walk (Theorem 3.1) and of the uniform empirical process with one bridge (Theorem 3.2 with Remark 8.3); their consequences at a random index (Proposition 5.1) and for a general distribution (Proposition 5.2, Corollary 5.4); one version carrying all three couplings (§2.2); Lévy's modulus of continuity (corrected Proposition 4.12); the arrival embedding (Theorem 2.8); Lipschitz continuity of the running infimum (Lemma 6.2); the renewal embedding (Lemma 7.1); and the queue as a reflection, (117)–(118). The remaining steps of the proof (the fluid limit of the completed jobs at rate and Brownian motion evaluated at the completed fraction) are not milestones: the paper states them only as conditional tail bounds ((130)–(132), p.41) on a route that does not reach the goal's rate, and their pathwise forms are not statements of the paper.
The result gives a sample-path description of a nonstationary, non-Markovian queue: every functional law of large numbers and central limit theorem for the scaled queue length follows from it, including those of the literature, with an explicit rate. The approximating process separates the macroscopic time dependence (, ) from the mesoscopic Gaussian fluctuations, which makes it usable for staffing and capacity questions over a finite horizon.
The result is proved in the paper; nothing in it is machine-checked. Formalizing it would add to the platform the KMT strong embeddings, the Brownian bridge and its use in empirical-process couplings, Lévy's modulus of continuity, and the first strong approximation of a queue. Several printed statements along the way are false as printed (see the scope section), so a checked proof also settles which form of each is true.
The obvious route composes the paper's tail bounds with the Borel–Cantelli lemma. It fails twice. First, the tail bound for Brownian motion at a random time (Proposition 4.12) is false, and it is applied where the random time depends on the same Brownian motion. Second, a tail bound at scale of the form does not sum, so Borel–Cantelli loses a power of . What works is pathwise: all couplings are driven by three fixed Gaussian paths, whose suprema on compacts are finite, so every time fluctuation is at most ; Lévy's modulus at that distance gives . The busy time is a further difficulty: the identity "queue length equals the reflection of " needs an argument on càdlàg paths, and it holds only up to runs of zero service requirements.
Samples of size are indexed by Fin n; the arrays are triangular, with no constraint across . Time is real, ; Brownian motion is Mathlib's IsBrownianReal with time in , evaluated at and . The busy time is the Lebesgue measure of . Infima in and are over of functions bounded below there. "Almost surely " means: for almost every there is with the bound for all and .
The goal asserts one and one for all ; letting them vary with would reduce the almost-sure bound to tightness. The laws and the block independence are part of the conclusion, so no degenerate coupling satisfies it.
The goal departs from the printed theorem in three declared ways: is centred at (the printed Assumption 2.5 centring is false); the rate is asserted for every positive (the printed else-clause is false as stated); and both assumptions are one statement. Milestones correct Theorem 3.1's index typo, Proposition 4.12, Lemma 7.1's range, (117)–(118) for zero services, and replace the tails (130)–(132) by pathwise bounds.
Needed infrastructure: Brownian bridges as Gaussian processes, KMT (Theorems 3.1, 3.2, reusable well beyond this mission), quantile transforms, Lévy's modulus, and the Skorokhod reflection on càdlàg paths. Proofs of any milestone are welcome; the KMT theorems and Lévy's modulus are the most reusable.
The minimum-cost flow problem is the common roof over shortest paths, maximum flows, transportation and assignment problems, and transshipment. It asks for the cheapest way to move a commodity through a directed network so that every node receives its prescribed net amount and no arc carries more than its capacity. Its central structural fact is integrality: when the data are integers, an optimal flow can be taken integral, so the integer program is solved by its linear relaxation. This is why integer flows (numbers of trucks, of workers assigned, of disjoint paths) can be computed with linear programming and network algorithms.
This mission formalizes §4.1 of Cook, Cunningham, Pulleyblank and Schrijver, Combinatorial Optimization (Wiley, 1998), together with the feasibility theorem 3.18 of §3.3 on which the integrality proof rests. It is the fifth mission of a series on the book; the series uses the book's own graph conventions (multigraphs, loops allowed, infinite capacities).
A digraph has finite node set , finite arc set , and for each arc a tail and a head ; loops and parallel arcs are allowed. For and , the net flow into is
For , is the set of arcs leaving and ; for a vector on arcs, .
Given demands with , capacities with , and costs , the minimum-cost flow problem is
A vector is integral when its finite components are integers. For the reduced cost of an arc is . The dual of (4.1) is
with no variable when .
A circuit is a closed path in the underlying undirected multigraph, with distinct arcs, distinct nodes , and ; an arc is forward if it goes from to and reverse otherwise. A circuit is -incrementing if forward arcs have and reverse arcs have ; its cost is . A dicircuit is a circuit all of whose arcs are forward.
If and are integral and (4.1) has an optimal solution, then
The costs are arbitrary reals.
Theorem 4.5 says that the minimum-cost integral flow problem is no harder than (4.1): integrality comes for free. Special cases include integral maximum flows, integral transportation and assignment solutions, and the existence of integral shortest-path solutions of the transshipment program. Theorems 4.1–4.4 are the optimality and existence criteria used by the primal (cycle-cancelling), primal–dual and network simplex algorithms of Chapter 4, and Theorem 3.18 is the common generalization of Gale's supply–demand theorem and Hoffman's circulation theorem.
All of these results are classical and proved in the book. What this mission adds is machine-checked statements and, once solved, proofs in the book's generality: multigraphs with loops and parallel arcs, infinite capacities, lower bounds equal to , and real (not only rational) data. Related items already on the platform treat simple digraphs, loopless networks, circulations without demands, or finite bounds without the integral clause, so none of them states these theorems.
Every result here is classical, so the difficulty is in the substrate, not in a missing idea. The usual first argument for Theorem 4.5 is total unimodularity of the node–arc incidence matrix plus "an LP with an optimum attains it at a vertex". Neither piece is available in this form: Mathlib has Matrix.IsTotallyUnimodular but not the incidence matrix of a multigraph with loops, nor the vertex theory of polyhedra with some upper bounds absent. The book's own route needs a different missing piece, the integral half of Theorem 3.18 with mixed finite and infinite bounds. In both routes the infinite values of and enter every cut sum and every complementary slackness condition, and the integral clause of Theorem 3.18 is a separate claim from its real-valued form, not a corollary of it.
Nodes and arcs are finite types V, E; a digraph is a pair of functions tail head : E → V, so loops and parallel arcs are present. Capacities and bounds are EReal, with ⊤ for and ⊥ for ; the standing assumptions and are explicit hypotheses. "Optimal" means the minimum of over feasible flows is attained at ; no infimum is taken. The dual variables are indexed by the arcs of finite capacity. Integrality of a flow, demand or potential is "every component is an integer"; integrality of a bound is "every finite component is an integer".
One correction is made. Under the book's definition an arc of a path is forward when it goes from to , so a loop is always forward, and Theorem 4.2 then fails on a single loop with positive cost carrying positive flow. Circuits here record an orientation per arc and allow a loop to be traversed in reverse, which matches the auxiliary digraph the book's proof uses.
The statements are not trivial in a degenerate way: optimality quantifies over all feasible flows, the cut conditions range over every subset of , and the integral clauses assert existence of integer-valued vectors, not of real ones.
Reusable parts: the multigraph flow layer (net inflow, cuts, extended-real bounds), the oriented circuit, and the dual of (4.1). Welcome contributions include a proof of Theorem 3.18 via the max-flow min-cut theorem, LP-duality proofs of Theorem 4.1 using published complementary slackness results, and shortest-path (potential) proofs of Theorems 4.2–4.4.
Financial intermediaries often need access to two markets at once. A dealer that funds bond inventory in the repo market cannot operate without access to the collateral market, and the reverse also holds. Aymanns, Georg and Golub (SSRN 2881814; Operations Research, doi:10.1287/opre.2023.2439) model this coupling as a participation game on a multilayer network. Each agent stays active only if it has an active counterparty in every market. Their question comes from macroprudential stress testing. A regulator who knows only the degree distributions of the trading networks wants to know whether activity degrades gradually as a shock grows, or collapses all at once.
The single-layer version of this question is classical directed percolation. The giant out-component of a random digraph shrinks continuously to zero at a critical removal fraction (Cooper and Frieze, Combinatorics, Probability and Computing 13:319–337, 2004). Buldyrev et al. (Nature 2010) observed that interdependent networks instead fail abruptly. The paper proves the analogous discontinuity for the equilibrium of an economic game on two independent random directed networks with finitely many agents.
There are agents and two markets and . A network is a set of directed links. The link means that supports , and no agent links to itself. Each agent is shocked independently with probability , so is the shock size. Given the shocked set and the set of active agents, the best response (4) makes active exactly when and has at least one active in-neighbour in each market. The maximal equilibrium is the largest fixed point of this map, and the activity is the fraction of agents active in it.
The networks are random. For each market , a joint degree distribution gives the fraction of agents with in-degree and out-degree , with mean degree . A well-behaved degree tuple assigns in- and out-degrees to the agents for every . Its empirical law converges to , its second moments are , and its maximum degree is at most (Assumptions A.1, A.2). and are drawn independently and uniformly among simple loopless digraphs with these degrees. The two markets' degree labels are asymptotically independent. Assumption 4.5 requires , so asymptotically every agent has an in-link in both markets.
The analytic objects are defined from . Let be the in-degree law of the origin of a random link, and . Let be the smallest root in of , and set . The coupled map is , with greatest fixed point , and the limit activity is .
For all satisfying Assumption 4.5 there exist and with the following property. For every pair of well-behaved tuples with independent labels:
The constants depend only on the laws. does not depend on , which is what makes the transition discontinuous. No value of is hard-coded.
The result separates coupled markets from single ones. In one market (Proposition 4), activity vanishes continuously as the shock grows. With two complementary markets, activity drops from a fixed positive level to zero, so a stress test that extrapolates from small shocks misses the collapse.
The paper's argument is not a complete proof. Its reduction from random graphs to the fixed point (Lemmas 3–6) is a branching-process heuristic. Its analytic part assumes a tangency point that need not exist. Several printed statements are false. The degree convention of (9) is reversed. Lemma 3 uses a mutual giant component that can be large while activity is zero. The activity formula of Lemma 6 counts support through one market only. Continuity fails for the point-mass law , and Lemma 10's concavity contradicts its own flatness clause. The milestones state corrected versions, each with its counterexample in the item's differences list. No part of this result has a machine-checked proof. The Galton–Watson extinction criterion (Lemma 4) is an open goal on the platform (GaltonWatson.extinction_criterion). It is not restated here, because the definitions take the smallest root directly.
The deterministic analysis (milestones 5–8) needs only monotonicity and the fact that vanishes below . The hard part is milestones 3 and 4, which identify the activity of finite random networks with . Single-network results do not transfer. The mutual giant component of Definition 4.5, the intersection of the two giant out-components, does not control the mutually stable set. Removing an agent in one layer removes its support in the other, so the giant components must be recomputed jointly, and the obvious one-pass bound fails. The upper bound needs a concentration argument with summable tails for uniform simple digraphs with unbounded degrees. The lower bound needs a two-layer peeling process followed to a fixed point. At itself, where jumps, nothing is claimed.
Agents are Fin n and networks are Finset (Fin n × Fin n). The best response (4) is the primitive, with independent Bernoulli shocks. The cost distribution of Assumption 4.2 is not used, since as printed it is not a distribution function. In , is the in-degree. Probabilities and expectations are explicit finite sums over the uniform graph sets and the shocked set. "Almost surely " is read as convergence of the expectation together with summable tails. Assumption A.2(2) is imposed only for large , since it fails at . Assumption 4.6 is not assumed.
A trivial formalization is excluded. precedes and both constants precede the tuples, so a continuous decay to zero does not satisfy the goal. Verification files prove that the hypotheses are satisfiable (the -regular law and its constant tuple), and that the uniform graph set is nonempty in an example. They also check the running -regular example: solves with , the tangency point at which the planning computation places .
Needed infrastructure: uniform random digraphs with given degrees and the configuration model, local weak convergence or branching-process coupling for two independent layers, concentration for such graphs, and generating-function facts. These are reusable well beyond this paper. Contributions to any milestone, or to general lemmas about random digraphs with given degrees, are welcome.
The global minimum cut problem asks, for a finite undirected graph with nonnegative edge capacities, for a partition of the nodes into two nonempty sides that is crossed by edges of least total capacity. With unit capacities the optimal value is the edge-connectivity of the graph, a basic measure of network reliability; with general capacities the problem appears in network design, in clustering, and as the separation routine for subtour elimination constraints in cutting-plane methods for the traveling salesman problem (Chapter 7 of the source).
A minimum cut separating two fixed nodes can be found by one maximum flow computation, so a global minimum cut can be found with flow computations. The result formalized here shows that flows are not needed at all.
Timeline.
A graph has a finite node set , a finite edge set , and for each edge an unordered pair of ends. Parallel edges (several edges with the same ends) and loops (an edge whose two ends coincide) are allowed. Each edge has a capacity , and for we write .
For , the cut is the set of edges with one end in and the other in ; a loop lies in no cut. For a node , . A cut separates nodes , and is a -cut, if exactly one of lies in . Two optimal values are used:
For distinct nodes , the graph is obtained by identifying with : its nodes are for a new node ; its edges are those of that do not have both ends in , with every end or replaced by ; capacities are kept. Parallel edges arise naturally.
A legal ordering of is an ordering of all nodes such that, with ,
Each is attached to the earlier nodes by at least as much capacity as any later node. The Lean development uses the names CapGraph, CapGraph.delta, Separates, CapGraph.minCutValue (), CapGraph.globalMinCut (), CapGraph.identify (), CapGraph.IsLegalOrdering and CapGraph.IsMinCut.
For a graph with nonnegative capacities and at least two nodes, and any legal ordering ,
Equivalently . The graph need not be connected.
The result. Theorem 3.36 identifies, for any legal ordering, a pair of nodes together with a minimum cut separating them, without solving a flow problem. Combined with the identity of milestone 2, it yields the node identification minimum cut algorithm: compute a legal ordering (in the time of Prim's algorithm), record , replace by , and repeat until one node remains; the smallest recorded value is . This is the standard deterministic flow-free algorithm for global minimum cuts in capacitated graphs and the basis of edge-connectivity computations in multigraphs.
Formalizing it. The theorems are proved in the source; nothing is open. To the knowledge of this mission, neither Mathlib nor the Prove2Me library contains minimum cuts of capacitated multigraphs, node identification or legal orderings. The mission produces a checked statement of the correctness core of the Nagamochi–Ibaraki / Stoer–Wagner algorithm for multigraphs with loops and parallel edges, and reusable definitions of cuts, minimum cut values and node identification for capacitated multigraphs.
The obvious attempt compares directly with an arbitrary -cut and tries to bound the capacity of edge by edge; the legal ordering inequalities compare only the capacities into prefixes , not into the side , and a direct exchange argument does not close. The legal ordering condition is not preserved by arbitrary modifications of the graph, and the natural reductions change the node and edge types; relating cuts, the ordering condition and across such graphs is where most of the formal work lies. The statement must also hold for disconnected graphs, so connectivity cannot be used as a crutch.
A graph is CapGraph V E with ends : E → Sym2 V and u : E → ℝ, over finite types V, E; loops and parallel edges are allowed and are not a SimpleGraph. Cuts are Finset E, node sets Finset V, and every subset (including and ) defines a cut. Optimal values and live in WithTop ℝ as minima of finite families, with : and for a graph with one node, so the identity of milestone 2 holds also when . An ordering is a bijection Fin n ≃ V, 0-based (). The node set of is Option {a // a ≠ v ∧ a ≠ w} (none is the new node ) and its edge set is the subtype of edges of not having both ends in ; edge sets of are compared with those of through the inclusion.
The book poses the problem with and connected . Theorem 3.36 and the non-adjacent bounds are stated for ; the identity and Lemma 3.37 for arbitrary real capacities. Negative capacities are never admitted where they would change the statement: Theorem 3.36 fails for them.
A trivializing reading is excluded: the goal quantifies over all separating sets , and the legal ordering condition is the book's inequality for all (verified satisfiable on a three-node path in the sanity checks).
Needed infrastructure: deletion of an edge and of a node from a CapGraph with the induced legal ordering, and the comparison of cut capacities under deletion and node identification. These lemmas are reusable for the Gomory–Hu tree and random contraction results of §3.5.2. Contributions of such lemmas, decompositions by proof sketch, and proofs of the milestones are welcome.
Reflected Brownian motion (RBM) in a polyhedral cone arises as the heavy-traffic limit of open queueing networks (Reiman, 1984). Sensitivities of its stationary distribution to the drift, the covariance and the directions of reflection are relevant in those applications. There are few results on them. Dieker and Gao (2014) treat orthants with M-matrix reflection, perturbing the drift only in the direction . They conjecture that sensitivities of the stationary distribution can be expressed through the stationary distribution of the joint process of the RBM and its derivative process, and they verify this in dimension one. Lipshutz and Ramanan affirm the conjecture for a general simple polyhedral cone, with the drift, the covariance and the reflection directions all depending on the parameter.
Fix a cone with linearly independent unit normals . Write for the indices of the faces containing , and let be an open parameter set. For there are continuously differentiable directions of reflection with , a drift , and a positive definite covariance . Let be the matrix with columns , and let be the cone generated by .
Given a -dimensional Brownian motion , an RBM is a continuous adapted process in with
where each increment of the constraining process over lies in the cone generated by . Let . A derivative process along is an RCLL adapted process with , the subspace orthogonal to the normals of the faces at , and
where the increments of lie in the corresponding linear span. The joint process lives on , which is not closed in .
Under the geometric Assumptions 2.2, 2.4, 2.5, the Hölder Assumption 2.12 and the stability Assumption 3.4, for a continuously differentiable with bounded continuous Jacobian and , for almost every ,
Here has the stationary law of the joint process.
The milestones are the cited foundations (Theorems 2.8, 2.13, 3.5 and Corollary 2.16), the contraction results (Lemma 4.20 and Proposition 4.25), the Feller Markov property (Theorem 3.2), repeated visits to all faces (Proposition 6.1), the pathwise and Lyapunov estimates (Lemma 7.5, Proposition 7.3, Corollary 7.4), the asymptotic coupling criterion and uniqueness (Theorems 8.1 and 8.2), existence and uniqueness of the stationary distribution (Theorem 3.6), and the limits (9.1) with the dominator of Lemma 9.1.
The formula reduces a derivative of a stationary quantity to a stationary expectation, which is potentially useful for numerical algorithms that compute sensitivities. It covers perturbations of the drift, the covariance and the reflection matrix at once. Along the way the paper proves that the joint process is Feller Markov, that it is ergodic despite its degeneracy, and that its stability is uniform in the parameter.
Formalizing it would bring oblique reflection in polyhedral cones to the platform: the extended Skorokhod problem, the derivative problem and derivative processes. All statements are pathwise and need no stochastic integral. Theorems 2.8, 2.13, 3.5, 8.1 and Corollary 2.16 are quoted by the paper from other sources, so a complete proof must rebuild parts of those works. All of these results are proved in the literature, and a search of the platform found no machine-checked proof of them. The orthant results on the platform (HarrisonReimanRBM, GJNSteadyState) concern a narrower setting and different statements.
The obvious argument differentiates under the expectation at a finite time and lets . That needs a bound on the derivative process uniform in time, but the equation for has no dissipative drift: its driving term grows linearly. Stability comes only from the boundary, where the process is projected into . A single projection is only nonexpansive in the norm of the set , and a contraction appears only after the RBM has visited every face. The second difficulty is uniqueness: the joint process has dimension and is driven by a -dimensional Brownian motion, so it is degenerate and irreducibility arguments are not available. Its state space is not complete either, which rules out the textbook versions of the tools.
The development uses E J := EuclideanSpace ℝ (Fin J) with and time in ℝ≥0. One filtered probability space satisfying the usual conditions is fixed. Brownian motion is stated by Gaussian increments independent of the past, which is equivalent by Lévy's characterization, since quadratic variation is not available. The norm of is gauge, Hausdorff continuity uses Metric.hausdorffDist, and is fderivWithin ℝ f G, with having unique derivatives. Measures on are measures on the product that give the complement of measure zero. is defined as the square root of , so its smoothness is a fact and not an assumption.
Processes are universally quantified subject to Definitions 2.1 and 2.10, and the stationary laws subject to Definition 3.3, so no result holds by taking arbitrary processes. The goal also asserts integrability of and , so the identity cannot hold through a junk value of a Bochner integral. Almost-every stays as printed, and the cone, the reflection matrix and the perturbation are general: no orthant, M-matrix or drift-only restriction.
Proposition 4.25 is stated for , because the printed is false; the item records a counterexample. The Skorokhod and derivative problems, the contraction theory and the asymptotic coupling criterion are reusable beyond this mission. Contributions on any milestone, or on supporting lemmas such as Propositions 4.5, 4.15 and 4.16, are welcome.
Many problems in statistics, signal processing and machine learning minimize a smooth function over a set defined by smooth equations, subject to : orthogonality constraints (the Stiefel manifold), unit-norm constraints (spheres and oblique manifolds), fixed-rank and symplectic constraints. Riemannian optimization treats the feasible set as a manifold and moves along it with retractions and vector transports, which have to be designed and implemented for each manifold (Absil, Mahony & Sepulchre 2008). Exact penalty methods avoid that geometry, but the classical smooth exact penalty of Fletcher (1970) needs second derivatives of just to evaluate its gradient.
Xiao, Liu & Toh (arXiv:2203.10319v3) propose the constraint dissolving function (CDF), an unconstrained smooth function whose gradient needs only . They prove that, near the feasible set and above an explicit penalty threshold, the CDF and the constrained problem have the same stationary points and the same local minimizers. Any unconstrained solver can then be applied to the CDF directly. The paper later appeared in Mathematics of Operations Research (2024); this mission follows the arXiv v3 numbering throughout.
Let and , and let be the feasible region of (OCP). The transposed Jacobian has the gradients as columns. Assumption 1.1 asks that and be locally Lipschitz and that LICQ hold on : has full column rank for .
A constraint dissolving operator is a map with locally Lipschitz Jacobian such that and for every (Assumption 1.2). For the unit sphere one can take . The CDF with penalty parameter is
Around a feasible point the paper introduces local constants (§2.3, p.7). These are:
From these it builds a radius , two closed balls around , and the threshold
The Lean development uses the same names: transJac, cdf, rhoX, MXA, LXb, epsX, omegaBarRadius, betaX, Ainf.
For every , every and every :
The condition in the second implication corrects the printed statement: can be , and with the implication fails.
Theorem 3.18 makes the CDF an exact penalty for local minimization. With a penalty parameter above , unconstrained local minimization of near finds exactly the constrained local minimizers. Together with Theorem 3.10, this lets convergence and complexity results for unconstrained methods transfer to Riemannian optimization without retractions (§3.3 of the paper). The bounds of Lemmas 3.1–3.4 also justify the post-processing step used to restore feasibility.
The results are proved in the paper, and to our knowledge none of them has a machine-checked proof. Formalizing them yields a checked exact-penalty theorem with explicit constants. It also yields reusable infrastructure: an error bound for LICQ-regular equality constraints, nearest-point arguments for the zero set of a smooth map, and fixed-point iteration estimates near a manifold.
The obvious argument for the first implication of the goal compares with at a nearby feasible point. No such point is directly available: Lean has no projection onto , and the paper's projection argument needs the first-order optimality condition at a nearest point. That condition requires a Lagrange multiplier theorem under LICQ. The paper instead uses , whose existence (Lemma 3.4) is a quantitative contraction argument: one must show that the iterates never leave . The printed proof of the goal also applies Proposition 3.13 at the minimizer with the constants of , although the hypothesis concerns . A correct proof reruns the estimates with the constants of on a small ball around inside .
The step in the proof of Proposition 3.13 bounds along a segment where does not apply directly, and needs a separate argument. Every constant in the statements has to be tracked exactly, since the threshold is explicit.
EuclideanSpace ℝ (Fin n). Transposed Jacobians are adjoints of Fréchet derivatives, with the operator norm, and is the infimum of over unit . Theorems that use assume .sSups over the closed ball . They are finite under the assumptions, and no boundedness hypothesis is added. is the largest satisfying the two linear constraints. This is the printed minimum with , so an affine constraint (where ) does not collapse to a point; a proved sanity check confirms on such an instance.Welcome contributions are a Lagrange multiplier rule for nearest points of under LICQ, Lipschitz-on-compact lemmas for locally Lipschitz maps, and proofs of the milestones in order.
Simulation models of service systems, supply chains and financial products depend on input parameters that are themselves estimated from data, such as arrival rates or demand distributions. When a decision maker compares candidate designs by simulation, this input uncertainty means that the best design may differ from one plausible parameter value to the next. Kim, Kim and Song (arXiv:2207.07533, Operations Research, 2025) propose to select the most probable best (MPB): the design that is optimal with the largest probability under a distribution on the parameter.
Finding the MPB is a nested ranking-and-selection problem: an inner problem identifies the best design at each parameter, and an outer problem compares how often each design wins. The question the paper answers is how to split a simulation budget among all design–parameter pairs so that the probability of selecting the wrong MPB decays as fast as possible. The paper relaxes the exact large-deviations rate of this probability into a tractable max–min problem, (20), and characterizes its solutions by a short system of equations, Theorem 3. Its sequential sampling algorithms are plug-in versions of that system.
This follows the optimal computing budget allocation (OCBA) line of work for classical ranking and selection, in particular the large-deviations analysis of Glynn and Juneja (Proceedings of the 2004 Winter Simulation Conference, pp. 577–585), whose pairwise rate is the building block below.
There are solutions and parameters with probabilities , . The conditional mean of solution at is (smaller is better), and its simulation output has standard deviation .
An allocation is a point of the -simplex: is the fraction of the budget spent on . The pairwise rate is
if both ratios are positive, and otherwise. The relaxed OCBA problem is
A feasible is optimal for (20) if and only if
Both directions, every feasible allocation, every and .
Theorem 3 replaces an optimization over the simplex by a system that can be checked, and tracked, coordinate by coordinate. That is what makes the paper's sequential algorithms possible: each step samples the pair whose condition is most violated, and the consistency theorems of the paper (Theorems 4, 5 and 7) say that the sampling ratios converge to a solution of this system. The third condition is the qualitative finding: unlike classical ranking and selection, where every optimal ratio is positive, the MPB receives no budget at parameters where it is not the conditional optimum.
The result is proved in the paper. It has not been formalized. A machine-checked version gives a verified reference point for the nested ranking-and-selection model, the balance weights and the max–min KKT argument, and it checks three steps of the published proof that are misprinted (see Formalization scope). Theorem 3 itself is unaffected by these misprints.
The objective is a minimum of finitely many concave functions, which is not differentiable where two terms tie, and each term is not differentiable where an allocation ratio vanishes. The standard route rewrites (20) in epigraph form (EC.14) and applies KKT under Slater's condition. That route needs positivity of the optimal ratios first, so that the nonnegativity multipliers vanish and the rates are differentiable. Positivity is not automatic: the MPB's ratios at adversarial parameters are zero at every optimum, and when the conditional optimum's ratio at such a parameter is zero too, because it enters no term of the objective. A proof that assumes interior optima, or applies a smooth KKT theorem on all of , fails at exactly these coordinates.
The converse direction must rule out a degenerate solution of the system with on . Global balance and the zero ratio together exclude it only because the allocation lies on the simplex.
The Lean development uses the namespace MPBSelect. Solutions are Fin k, parameters Fin B, and an allocation is α : Fin k → Fin B → ℝ. A structure Problem k B carries , , , and , with fields for , , , assumption (i) (distinct means at each ), the strict-argmin property of , the strict-argmax property of (assumption (ii)), and . is a standard deviation: the paper's Model (4) has variance . is defined with an explicit if for its zero branch. The minimum over is Finset.inf', and is proved nonempty, so no junk value enters. is the real formula (17) and is only evaluated on .
The goal is stated for every feasible allocation and with all three conditions. A version restricted to , to interior allocations, to one direction, or to "some optimal allocation satisfies the conditions" would be a different and weaker theorem.
Three proof steps carry a declared correction. Positivity on all of and the condition (EC.20) "for all " both fail for : with , , , , the printed KKT system has no solution. The milestones restrict both to parameters at which has a pair; for that is every parameter. The printed partial derivative of has where belongs in the denominator ( against the true at ); the ratio of the two partials, which is all that (EC.22) uses, is unaffected.
A complete development needs concavity of the harmonic-mean function on the closed quadrant, a KKT theorem for a concave program with a linear equality constraint, differentiable at the point, and finite-sum manipulations. Mathlib supplies ConcaveOn, HasDerivAt and Finset.inf'. A reusable lemma on concavity of extended by to the closed quadrant would be welcome, as would a KKT sufficiency lemma for max–min problems.
Many problems in statistics, signal processing and operations research have the composite form : a smooth convex loss plus a convex, possibly nonsmooth term that encodes a regularizer or a constraint. First-order methods use only ; high-order (tensor) methods also use the derivatives and minimize a regularized Taylor model at each step. The question is how fast such a method can be.
For -th order methods on functions with Lipschitz -th derivative, the best possible worst-case rate is after iterations (Arjevani, Shamir & Shiff 2019; Nesterov 2021). Known accelerated tensor methods reached only .
Timeline.
Let be convex and times differentiable, with -Lipschitz -th derivative: , in the tensor operator norm. Let be proper closed convex, , the set of minimizers of (assumed nonempty), and the distance from the starting point to .
For the regularized Taylor model at is
The -subdifferential is . A triple is a -approximate solution of if and .
Algorithm 2 keeps weights , with , and the point . At each iteration it finds a step size and a -approximate solution at such that
(or a small-residual alternative that ends the run), sets and . The parameters satisfy , , and .
For every and every such that the step producing satisfies (3.7),
The goal keeps the paper's explicit constant.
The theorem shows that the rate is attained for composite problems at every order , so the lower bound for -th order methods is tight. At it gives a second-order method with rate for nonsmooth composite objectives, with inexact subproblem solutions. The A-HPE inequality (Lemma 3.1) and the Taylor gradient bound (Lemma 2.1) are general tools: the first underlies a family of accelerated proximal methods, the second every regularized tensor method.
The result is proved in the paper (with the correction below) but not formalized anywhere. The mission formalizes the A-HPE analysis, which the paper quotes from Monteiro and Svaiter without proof, a Taylor estimate for gradients at every order , and the bootstrapping argument from (3.13) to the closed-form growth of . A Lean proof would also confirm the explicit constant.
The classical estimate-sequence argument gives Nesterov's and no better: it discards the term of (3.3). The improvement needs that term together with the lower half of (3.7), which ties to a step length that itself depends on through . Converting the summed bound into growth of requires Hölder's inequality and an induction on exponents whose limit must be taken. Inequality (3.3) is the heart of the A-HPE theory and is not proved in the paper. At general , the gradient of the model must be identified, including the regularizer , and the Taylor remainder must be bounded with iteratedFDeriv.
is EuclideanSpace ℝ (Fin n). is ContDiff ℝ d f with the Lipschitz bound on iteratedFDeriv ℝ d f in the multilinear operator norm, and . and take values in EReal; proper closed convex means never , somewhere finite, lower semicontinuous and with convex epigraph. Gradients are Mathlib's gradient. is ⨅ x, F x and is Metric.infDist to the nonempty set of minimizers. A run of an algorithm is a family of sequences related by its steps for the iterations ; , and are computed from them with . The algorithm's STEP 2 stopping test is part of a run of Algorithm 2.
Correction. STEP 3 allows a step that satisfies only the small-residual alternative instead of (3.7). The printed Theorems 3.3 and 3.4 fail at such a step. A one-dimensional quadratic example satisfies every assumption, yet exceeds the printed bound, which is below . Every corrected item therefore assumes (3.7) at the step producing . Earlier steps satisfy it automatically, since an alternative-only step triggers the stopping test. The A-HPE framework is formalized without its exact stopping test , which Algorithm 2 replaces by an approximate one. The goal is stated for ; the paper's formula also holds at . The milestones on require , because their constants contain .
No hypothesis of the goal is vacuous: a one-step run with , , satisfies all of them (checked in Lean). The goal concerns the actual iterates of Algorithm 2 and the gap , not abstract sequences satisfying (3.13).
Needed infrastructure: Taylor's theorem with integral remainder for iteratedFDeriv along a segment, the calculus of , -subdifferential sum rules, and Hölder's inequality for finite sums (Real.inner_le_Lp_mul_Lq). The Taylor gradient bound and the A-HPE estimates are reusable beyond this mission. Contributions to any milestone, or to general lemmas they rely on, are welcome.
A manufacturer that sources from several suppliers faces a recall problem. When a defect is reported and the source cannot be traced, every unit on the shelf is recalled, including goods from suppliers who did nothing wrong. A shared ledger that records provenance changes this: only the defective batch needs to be recalled. A Walmart case study reports tracing times falling from seven days to 2.2 seconds, and the same record can also tell consumers more about the product.
Whether such a system is worth its cost depends on who keeps the gains. In a companion paper, the same authors show that under Bertrand competition among manufacturers the gains are competed away to consumers and the incremental welfare from adoption is zero (Iyengar, Saleh, Sethuraman, Wang, Economics of Permissioned Blockchain Adoption, Management Science 69(6), 2023). The paper formalized here, Iyengar, Saleh, Sethuraman and Wang, Blockchain Adoption in a Supply Chain with Manufacturer Market Power (SSRN 3950580), studies the opposite market structure, a single manufacturer that sets prices on both sides, and reaches the opposite conclusion.
There are homogeneous suppliers, one manufacturer of type , and a unit mass of consumers of types , with types uniform and independent. A consumer values the good at and has an outside option worth . Consumers do not see . Each receives a signal equal to with probability , where in the regime without blockchain (NB) and , , in the regime with blockchain (B). A consumer buys when the conditional expected utility given type and signal, minus the price, is at least . Demand is the resulting purchase probability.
The manufacturer places an order : a consumer price , a supplier price , and a set of suppliers, each producing a quantity . A supplier exerts effort at unit cost , and its whole batch is good with probability . Without blockchain any defect recalls everything, so the no-recall probability is . With blockchain only the defective batch is recalled, so it is . A symmetric effort maximizes a supplier's profit per unit given that the others exert the same effort, and a supplier accepts when the profit at that effort is strictly positive.
The manufacturer's random profit sums over the accepting suppliers whose batch is not recalled, with batches independent. Its objective is the mean-variance utility , . At an adoption cost , an equilibrium has suppliers responding after every order, the order optimal in each regime, and adoption exactly when the incremental welfare is at least .
There is a number , independent of the cost, such that for every an equilibrium exists and every equilibrium satisfies
The statement holds for every , every in the stated ranges, and without the paper's Assumption 1, which only the later comparative statics use.
The theorem says that the manufacturer always gains from traceability. The gain is explained by the decomposition the paper gives afterwards: a lower profit variance from diversification across suppliers, and a higher expected profit. It separates the monopolist case from the competitive one, where the same technology yields no gain. The solution also shows that adoption changes the sourcing structure, from a single supplier to all of them.
The result is proved in the paper; no machine-checked proof is known. This mission adds a three-layer supply chain game with recalls, Bayesian consumers and mean-variance utility, and it records two corrections of printed statements: the set of symmetric efforts at , , and the uniqueness claim for the cubic , which holds on and not on the real line.
The proof in the paper looks short because Proposition 3.1 carries the work, and the obstacle is exhaustiveness. The optimality condition ranges over every order, including and without blockchain, where the supplier fixed point has several solutions, and including , where . The naive reduction to maximizing on the good region is valid only after every other order is shown to give utility at most , under every symmetric supplier response. The variance computation over independent batches must produce the factor , and the strict preference for all suppliers needs .
Types and signals are Bool, suppliers are Fin N, and is the paper's normalization. Probabilities are finite weighted sums on Fin N → Bool. Everything is real-valued, and is quantified after .
The conventions follow the paper's proofs. The consumer conditions on type and signal, as on p.31. Demand is the purchase probability of a generic consumer, because the continuum integral (8) is not literally definable under independent signals. The supplier objective is per unit. The manufacturer's strategy does not depend on its type. The supplier stage is formalized as in the proof: a symmetric fixed point with exponent , assuming that all of produce, with acceptance then evaluated at that effort. An equilibrium requires a symmetric response after every order and leaves its selection free, so the printed selection is one case. The number precedes .
A trivializing formalization defines as or the supplier response as the printed formula; here demand is the Bayes quotient, supplier behaviour is the arg max, and comes from the random profit, so , and the printed efforts enter only as milestones. The existence clause rules out a vacuous goal.
The development needs only Mathlib: Real.sqrt, Real.rpow, StrictConcaveOn, HasDerivAt, and finite sums. The independent-Bernoulli module is reusable. Proofs of the milestones in any order are welcome, and the utility computations are the natural place to start.
Bayesian persuasion (Kamenica and Gentzkow, 2011) studies a sender who knows the state of the world and commits to a randomized signaling policy before a receiver acts. In the classical model the sender may send as many distinct messages as the receiver has actions, and by the revelation principle an optimal policy simply recommends an action. In many applications the channel is narrower than the action set: a recommender shows out of items, a platform has a fixed number of badges, a regulator can publish one of a few grades. With signals the sender can no longer point at every action, and which actions to bundle under one message becomes the core of the problem.
Gradwohl, Hahn, Hoefer and Smorodinsky (arXiv:2007.12489, published in Mathematics of Operations Research, 2022) study this limited-communication model algorithmically. Aybas and Turkel (arXiv:1910.13547) had shown that optimal schemes exist with signals and that the sender loses at most a fraction of utility when one signal is removed. Dughmi and Xu (arXiv:1503.05988) studied symmetric schemes for algorithmic persuasion with unrestricted signals. The mission formalizes the paper's structural result for symmetric instances: the characterization of an optimal scheme by a common slope on Pareto frontiers.
There are actions and a finite type set . A state is drawn with probability . A type carries a value pair : the receiver gets and the sender gets if takes action . The instance is symmetric if whenever is a permutation of . Types within a state of positive probability are assumed distinct.
A -signal scheme sends signal in state with probability , where . Write
for the joint utilities of signal and action . The receiver best responds to each signal and breaks ties in favour of the sender, so the sender's utility is . A scheme is optimal if no -signal scheme gives a larger . A direct scheme recommends an action with each signal; it is persuasive if following the recommendation is a best response. The quantity is the best the receiver gets from a fixed action.
For a direct scheme recommending action with signal , let be the set of types of the first actions and its probability. The recommendation point lies in the convex hull of . A point collection assigns to each a point in that hull, with and . For , is -Pareto (Definition 1) if every is on the Pareto frontier of , the line of slope through is tangent to that frontier, and .
For every symmetric instance there are an optimal -signal scheme and a slope such that is direct and persuasive with recommendations from , its recommendation points are -Pareto, and
The type set, the prior, the values and are arbitrary; no independence or special distribution is assumed.
Theorem 1 replaces an optimization over all randomized maps from to by a one-parameter family: guess the common slope , then each frontier contributes at most one segment, and the remaining choice is a linear program in the positions on those segments. This is the basis of the paper's Slope-Algorithm, which computes an optimal scheme in polynomial time given oracles for the probabilities of frontier segments, and of the polynomial-time oracles for IID, random-order and prophet-secretary distributions. It also underlies the paper's tight comparison between limited and unlimited signaling in symmetric instances.
The result is proved in the paper; it has not been machine-checked. The mission produces a finite, self-contained formal model of persuasion with limited signals and sender-favourable tie-breaking, which other limited-communication results can reuse, together with formal statements of each step of the characterization.
The obvious argument fails at two points. First, Lemma 2's exchange argument in the paper moves pairs of points along their frontiers until all share a slope, and does not argue that this terminates, so a complete proof has to supply a terminating argument. Second, optimality in Theorem 1 is against all -signal schemes with the receiver's tie-broken best response, not only against direct persuasive ones. Closing the circle needs Lemma 1, the realization of an -Pareto collection by a scheme (Lemma 4), and the fact that for symmetric schemes the obedience constraints collapse to one inequality (Lemma 3), whose "if" direction uses the symmetry of both the instance and the scheme.
The Lean development fixes the following conventions. All actions share one Fintype of types T; states are Fin n → T; the prior is a weight function q ≥ 0 with total mass 1; values ρ, ξ : T → ℝ are arbitrary. Signals are Fin k, and action j ∈ [k] is Fin.castLE hkn j. The receiver's response is formalized with the unnormalized sums and above, so a null signal involves no division and imposes no constraint; ties are broken toward the sender by taking the largest over the receiver's maximizers. For a direct scheme, and in §3 (recommendation points, Lemmas 2–4) are the utilities when the receiver follows the recommendation; Theorem 1 and Lemma 1 additionally state that this equals the best-response utility for the scheme they produce. sums over states whose first types form the Finset , and every condition on a point collection is imposed for the sets with . Points are in with the receiver coordinate first. A point is on the Pareto frontier of if it lies in the convex hull and no hull point is strictly larger in both coordinates, which keeps the horizontal and vertical end segments of the paper's picture (p.6); corresponds to slope if for every hull point . Symmetric schemes are stated through cross-multiplied equalities of conditional type distributions, not through permutation-equivariance of .
A statement in which -Pareto conditions were required for every set of types, including the empty set, would make every -Pareto condition unsatisfiable and the sender-optimality clause vacuous; the guard rules this out, and a two-action example with an explicit -Pareto collection has been checked. Optimality is never restricted to direct, persuasive or symmetric schemes.
Needed infrastructure: convex hulls in (Mathlib's convexHull), finite sums, permutations of Fin n, and an existence argument for an optimal scheme (compactness of the direct persuasive polytopes). The model definitions are reusable for the paper's other results (independent instances, approximation schemes), which are not part of this mission. Proofs of any milestone, and alternative proofs of Lemma 2, are welcome.
Percolation games were introduced by Garnier and Ziliotto (arXiv:2110.12227, published in Mathematics of Operations Research, 2022) as discrete toy models for the stochastic homogenization of non-convex Hamilton–Jacobi equations. In homogenization one asks whether a control or game problem in a random, spatially varying environment behaves, over long horizons, like a problem in a deterministic averaged environment. For convex Hamiltonians (one controller) this is classical; for non-convex Hamiltonians, which arise from two-player zero-sum differential games, homogenization can fail (Ziliotto, Comm. Pure Appl. Math. 2017; Feldman–Souganidis, J. Math. Pures Appl. 2017). Percolation games keep the two-player structure and the random environment but replace the continuum by the lattice , and ask the corresponding question about the limit value of a repeated game: does the value of the -stage game converge as , and to a deterministic constant?
The limit value question is central in the theory of zero-sum stochastic games (counterexamples to its existence by Vigeral, Dyn. Games Appl. 2013, and Ziliotto, Ann. Probab. 2016). Percolation games are stochastic games with infinitely many states, deterministic transitions and a random payoff field, a class for which none of these general results applies.
Fix , finite nonempty action sets (Player 1) and (Player 2), and a transition function . A probability space carries a payoff field , , that is uniformly bounded.
Given (known to both players) and an initial state , at each stage Player 1 chooses ; then Player 2, knowing , chooses ; Player 1 receives from Player 2, and the state moves to . A strategy for Player 1 maps the past and the current state to an action; a strategy for Player 2 also receives . The -stage payoff and value are
Write for the random variable and .
The game is oriented (Definition 2.1) if there is with for every : the state's coordinate along strictly increases, whatever the players do. It is i.i.d. (Definition 2.2) if the site vectors , , are independent and identically distributed.
In an i.i.d., oriented percolation game there is a constant such that, for every , almost surely; there are such that for all , and ,
and for some and all , . The constants depend on the game, never on , or .
Theorem 2.3 gives a deterministic limit value for a class of zero-sum stochastic games with infinitely many states in a random environment, with a quantitative rate: fluctuations of order up to a logarithm, as for sums of independent variables. In the homogenization picture it says that the oriented, i.i.d. discrete game homogenizes. Theorem 2.4 of the same paper shows that orientation alone does not suffice: there is an oriented game on with an ergodic but non-i.i.d. payoff field whose value oscillates between and . Together they locate the dividing line.
The result is proved on paper; it has no machine-checked proof. The mission produces a formal model of percolation games (plays, history-dependent strategies, values), the existence of the value for finite perfect-information games of this form, and a complete formal proof of Theorem 2.3. Two printed statements in the proof need repair, and the formal versions fix them: the concentration bound (3.2) is false as printed (it lacks the factor of the two-sided Azuma inequality and the number of martingale steps), and the cube must be symmetric around the origin, without which the concatenation step and the first inequality of (3.3) fail. Neither repair affects Theorem 2.3, whose constants are existential.
The obvious route, subadditivity of pathwise followed by a subadditive ergodic theorem, fails: after stages the game restarts from a state chosen by the players, not from a fixed site, so there is no pathwise subadditive inequality. The paper's argument replaces it by two separate controls. Concentration: is a function of independent site vectors in which each hyperplane is visited at most once, so the Doob martingale over hyperplanes has increments and Azuma gives Gaussian concentration. Convergence of the mean: concentration and a union bound over the polynomially many possible restart states give near-subadditivity of with an error term , which the de Bruijn–Erdős lemma, not Fekete's lemma, handles. Formally, the delicate parts are the strategy concatenation (shifting histories and restarting optimal strategies), the measurability of , and the conditional-independence step behind (3.1).
is Fin d → ℤ. Strategies are pure and history-dependent, indexed from stage with histories Fin m → ℤ^d × I × J; Player 2's strategy receives Player 1's current action. The value is ⨆ σ, ⨅ τ, gamma … over all strategies; for finite only finitely many histories are reachable in stages, so the supremum and infimum are of finite families for every payoff function, and milestone 1 proves they are attained and equal to the min–max. The play depends on the strategies and the transition only, never on the payoffs.
The i.i.d. hypothesis is: every is measurable, the site vectors are mutually independent (iIndepFun) and identically distributed (IdentDistrib). The paper's model also carries an ergodic measure-preserving -action and a stationarity condition; these are dropped, since i.i.d. sites already have a translation-invariant law and the proof uses nothing more. "Uniformly bounded" is one bound for all . Expectations are Bochner integrals and probabilities are measures of sets; is bounded and measurable (milestone 2), so neither convention is degenerate. A trivializing encoding, a value that is a junk constant, is ruled out by the sanity checks in the development: with one action each and the value is the path average, and for it is .
A complete development needs: backward induction for the finite perfect-information game, a translation-equivariance lemma for values, the Doob martingale over hyperplanes with a conditional-independence argument, Azuma's inequality (available on the platform as ModernOnlineLearning.OnlineToBatch.theorem_3_9), Borel–Cantelli, and the de Bruijn–Erdős lemma, which is not in Mathlib and is reusable on its own. Contributions to any milestone are welcome, including alternative proofs of the de Bruijn–Erdős lemma.
A structured bandit is a repeated decision problem in which a learner picks a decision from a set and observes a noisy reward. The set can be large or continuous: a dosage, a price vector, a path in a graph. Treating each decision separately costs regret of order , which is useless when is large relative to the horizon . The learner must generalize across decisions through a function class that is assumed to contain the true mean reward. Knowing that the mean reward is in is not enough on its own: in Example 4.1 of the notes, a class of needle functions has , yet regret of order is unavoidable. A guarantee therefore needs a second complexity measure, one that says how much is learned about one decision from others.
The eluder dimension of Russo and Van Roy (NeurIPS 2013) is such a measure. It was introduced to analyse optimistic algorithms and posterior sampling for general function classes, and it remains the standard yardstick for optimism beyond linear models. This mission is number XI in the formalization of Foster and Rakhlin's lecture notes (arXiv:2312.16730), and it covers §4.1.1 and §4.1.2.
Let be an arbitrary set of decisions. In each round the learner selects and observes , drawn from a fixed model . The mean reward is , and regret is , with a maximizer of . The learner knows a finite class with .
Generalized UCB forms the empirical minimizer of the square loss on the first rounds, keeps every function whose empirical loss is within of it, in a confidence set , and plays a maximizer of the upper confidence bound .
A sequence is -elusive for if for each some has and . The first layer of the dimension is the length of the longest such sequence. The eluder dimension is its monotone version, floored at one, maximized over the class:
With probability at least ,
with one absolute constant. The goal fixes no constant, so it survives any sharpening of the argument.
The theorem has no dependence on . For linear models the eluder dimension is of order , which recovers the LinUCB rate up to logarithms, and for generalized linear models with link derivative in it gains a factor . It also shows the limits of the approach: a single ReLU neuron has eluder dimension exponential in (Li et al.). The result is the reference point against which the Decision-Estimation Coefficient of the later chapters is compared.
The result is proved in the literature, so nothing here is open. The eluder dimension has no prior formal treatment on the platform. The mission contributes that definition, in a form usable for any class, together with a combinatorial lemma that makes no reference to probability, and a concentration statement for least-squares confidence sets under an arbitrary adaptive algorithm that the contextual and reinforcement-learning chapters can reuse. The platform's FoundationsRL.Bandits.optimism_lemma is stated for finitely many decisions, so it does not carry over to this setting.
The obvious argument stops at (4.7). The confidence set constrains a function on the decisions already played, while the regret is charged at the new decision , and in general good fit on the past says nothing about a new point. The eluder dimension bounds the number of rounds on which the two can disagree, but its definition has a single scale: squared error on the past and a surprise of . The confidence sets have a fixed radius which is much larger than for small widths. The central step is Lemma 12, which must control the count of large widths at every scale at once, and the elliptical-potential argument for linear models has no analogue for a general class.
The confidence sets themselves need a concentration inequality for dependent data: the decisions are chosen adaptively, so the square loss differences do not form an independent sequence.
Decisions live in an arbitrary type with no finiteness assumption. The class is a Set of real functions, F.Finite in the goal and arbitrary in Lemma 12. The dimension takes values in ℕ∞, with edimRaw for the underlined quantity and edimFstar, edim for the two layers built from it. The bound is stated in ℝ≥0∞, so it is vacuous, not false, when the dimension is infinite. The argmax over is presupposed by the source's notation, so a run of the algorithm has the maximizer as a hypothesis, and the regret comparator is a supremum. The first clause of (4.9) is strict and the second is not. Rounds are numbered from , as in the notes. The width of Lemma 12 is extended-real valued, because a real supremum would return a junk value on an unbounded class.
The conditional law of the reward is stated on measurable sets for an arbitrary filtration. The constant in the goal is existential and quantified before the types, so it cannot depend on , or . A trivializing reading, in which regret is measured against a fixed decision rather than the best one, or in which the supremum in the width collapses, is ruled out by these conventions.
Contributions are welcome on the eluder-dimension combinatorics, which are reusable beyond this mission, and on the concentration lemma, whose martingale argument also serves the contextual form of Lemma 10.
Many learning systems serve several populations at once: a recommender serves user segments, a clinical dosing rule serves patient subgroups, an online marketplace serves customer types. When these populations share the same unknown options, the exploration one population performs also informs the others. A policy that minimizes total regret decides who bears that exploration cost, and it can load the whole cost onto one group. Baek and Farias (arXiv:2106.02553v2) make this precise with the axiomatic bargaining framework of Nash (1950): each group's utility is the regret it saves relative to learning on its own, and a fair policy maximizes the Nash social welfare, the sum of the logarithms of these savings. Their Theorem 1 shows that regret-optimal policies such as KL-UCB give some group zero savings, so they are maximally unfair in this sense. Their Theorem 3, the goal of this mission, shows that a different policy, PF-UCB, attains the largest welfare any consistent policy can reach.
A grouped -armed bandit has a finite set of groups and arms . Group can pull only the arms ; is the set of groups connected to arm . At each time a group arrives, independently, with probability ; the decision maker sees , pulls an arm and observes a reward drawn from , where has distinct entries and is unknown. Write , , and . The group regret of a policy is
The disagreement point of group is , the regret of the KL-UCB policy on the single-group instance , in which every other group can only pull a null arm of mean . The utility gain and the Nash social welfare are
with for .
With , the arms optimal for no group, and , the welfare bound is the value of the concave program (13):
Here is the share of the exploration of arm carried by group . PF-UCB solves the same program at the empirical means, takes the optimal solution of smallest Euclidean norm , and at time pulls an arm that has the highest UCB for some group and that has pulled at most times; if there is none, it pulls the greedy arm.
for every instance: every finite group and arm set, every bipartite graph , every arrival law with , every with distinct entries, and every tie-breaking rule of the policies.
In the order of the proof in Appendix E:
Theorem 2 of the paper bounds for every consistent policy, so Theorem 3 makes PF-UCB the Nash solution: it is proportionally fair across groups in every instance. It also makes the fairness question quantitative. The same program measures the price of fairness, the share of the regret reduction lost to fairness, which the paper bounds in Theorem 4. Theorem 9 gives an exact asymptotic description of the group regrets: who explores which arm, and at what rate.
The result is proved in the paper; nothing in this mission is open mathematics. No part of it is machine-checked. A complete formalization would give the first verified asymptotic analysis of a grouped (contextual) bandit policy, and it produces reusable components: a grouped bandit model with fixed action sets, KL-UCB for Gaussian rewards with the exploration level, change-of-measure lower bounds of Lai–Robbins type, and a stability result for minimum-norm solutions of a parametric concave program. Shorter proofs of any milestone, and a proof of Proposition 1 by reduction to a published KL-UCB analysis, are welcome.
The welfare is a sum of logarithms of liminfs, so the goal needs exact first-order constants: every group's regret must be pinned to times the right constant, not bounded by it. Two parts of the argument resist the obvious approach.
First, the program (13) need not have a unique optimal solution, and PF-UCB tracks the minimum-norm one. Proposition 3 says the minimum-norm solutions at nearby parameters are close. This is not a consequence of continuity of the optimal value, and it fails for an arbitrary choice of optimal solutions. The proof in the paper goes through a polytope-distance argument whose uniform bound needs care where the constraint matrix loses rank.
Second, the paper's proofs of Lemma 9 and Proposition 2 cite each other: Proposition 2 uses Proposition 9, which assumes log-consistency, and Lemma 9's proof of log-consistency uses Proposition 2. A formal proof has to break this circle, for example by a direct proof that PF-UCB is log-consistent.
The probability space is explicit: i.i.d. arrivals with law , one i.i.d. reward stack per arm, and an i.i.d. uniform draw per step for the policy's randomization. The reward of a pull is the next unused entry of the arm's stack, as on p.6. A policy is one rule for every ; it sees the past groups, arms and rewards, the arriving group and its draw. Lean step is paper time .
The committed conventions are these.
The minimum-norm solution is defined by choice; the first milestone states that it exists and is unique, so the definition is the intended object. An -valued welfare (with ) or a Bochner expectation of a non-measurable regret would trivialize the goal; both are ruled out by the choices above.
Prizes and patents reward the first innovator to fill a market niche. How generous the reward should be depends on how often useful ideas arrive, and a policy maker rarely knows that rate. Basov, Erkal, Minehart and Scotchmer (SSRN 4628270, 2024; published in Management Science, doi:10.1287/mnsc.2023.03362) model ideas as scarce: they arrive at the times of a Poisson process, each to a different person, and an idea that is not used is lost. A reward then works as a screen. Ideas whose cost is below the reward are developed, and the rest are discarded. The planner trades the cost of the innovation against the delay before it arrives.
The question is how this trade-off changes over time when the arrival rate of ideas is unknown. Each period in which the reward goes unclaimed is evidence that ideas are scarce. The paper shows that the optimal reward rises with the delay and that expected welfare falls. The model belongs to the family of optimal stopping and real-options problems with Bayesian learning (compare Mason and Välimäki, 2011, with two possible arrival rates). Here the planner's belief is a whole density on , and the paper shows that one scalar state variable still suffices.
A niche, once filled, has social value , where is the discount rate. Each idea has an R&D cost drawn from a continuous cost density on its support , with distribution function . Throughout, . At time the planner offers a reward . An idea that arrives at time is developed exactly when its cost is at most , which happens with probability .
Ideas arrive at an unknown rate . The planner's prior is a density on , and Assumption 1 requires to be continuous and bounded, to have finite moments of every order, and to satisfy . The cumulative innovation incentive is a sufficient statistic: given that no innovation has occurred, the posterior is with . Its moments are .
The expected welfare of a reward policy from state is
The value function is , taken over all admissible policies. It satisfies the Hamilton–Jacobi–Bellman equation
There is an optimal feedback reward . It is the unique solution of
it is and strictly increasing, is strictly decreasing, and
The statement holds for every cost density and every prior satisfying Assumption 1. It assumes no parametric family.
Theorem 3 gives the shape of the optimal reward. It starts low, rises monotonically, and tends to the full social value . The rate is governed only by and the cost distribution below . Theorem 4 says that a planner who learns sets a lower reward than one who treats today's expected rate as known. The difference is the option value of the information in an unclaimed reward. These results underlie the paper's legal interpretations, such as rewards that grow with delay and the comparative statics in the cost distribution (Theorem 6).
Formalization adds three things on top of the paper. First, the moment calculus of Lemma 2 is a reusable result about exponential tilting of densities on . Second, the identification of the value function with the HJB solution and the derivation of (22) and (24) are carried out with a fixed policy class and solution concept. Third, the statements fix the welfare functional precisely: as printed, (16) multiplies by , which already contains that factor. The mission uses the functional that is the limit of the Bellman recursion (17), which the paper's own derivation uses, and the HJB milestone states that limit. None of these results has been machine-checked. The paper's proofs are informal at the limit .
The obvious route is to write down the HJB equation and read off the policy, and it skips the hard part. The paper passes from discrete time to the HJB equation in one sentence. In continuous time one needs a verification argument: every bounded differentiable solution of the HJB equation bounds the welfare of every admissible policy, and it is attained along closed-loop paths. The value function must also be shown to be differentiable before (21) can be written. A second difficulty is monotonicity. Equation (24) alone does not rule out a reward that first falls. The argument combines Lemma 3, which needs the strict Cauchy–Schwarz inequality behind Lemma 2 (iii), with a limit argument at infinity. The rate constant (not , the naive rate) comes from l'Hôpital's rule applied to (24) together with . The latter is a Laplace-type asymptotic that depends on being continuous and positive at .
The Lean development lives in the namespace ScarceIdeas. States are , and every derivative is taken within . Policies are open-loop functions of time with values in , measurable on . The value is the real supremum of the welfare over all of them. An optimal reward is a feedback rule whose closed-loop paths exist from every state, and every such path attains . The moments are defined by the quotient (31). The naive reward is the root of (56). is stated as a limit of . "Increases" and "decreases" are strict.
The value function is a supremum, not a solution of the HJB equation or of (22). Defining it by either would make the goal circular. Optimality is measured against all admissible policies, not a restricted class. Changing a feedback rule at a single state changes no closed-loop welfare. For that reason the goal pins the optimal reward pointwise through (22), and "unique solution to (22)" means uniqueness of the root at each state.
A complete development needs: differentiation under the integral sign for Laplace-type integrals, and their asymptotics at infinity; the strict Cauchy–Schwarz inequality for integrals; a verification theorem for a one-dimensional infinite-horizon discounted control problem with a bounded state-dependent hazard; and comparison arguments for scalar ODEs. The moment lemma and the verification theorem are reusable beyond this mission. Contributions toward either, and toward any milestone, are welcome.
Search engines sell the ad slots next to their results in position auctions: advertisers bid, the highest bidder gets the top slot, the second highest the next one, and so on. A slot higher on the page is clicked more often, and the ratio of click rates between slots is described by a vector of relative position values. The textbook truthful mechanism, Vickrey–Clarke–Groves (VCG), computes its prices from this vector. The auctioneer does not know the true vector; it can only estimate it, and the bidding language of a real auction (one number per bidder) cannot express the bidder's own view of it.
Dütting, Fischer and Parkes (arXiv:1602.07593v4) ask which mechanisms still reach an efficient outcome, with slots assigned in order of value, when the mechanism uses a misspecified estimate. Their answer for complete information is that the non-truthful generalized second price (GSP) auction used in practice is at least as robust as the VCG mechanism run on the same estimate.
Timeline. Varian (2007) and Edelman, Ostrovsky and Schwarz (2007) characterized the envy-free ("symmetric", "locally envy-free") equilibria of GSP when the auctioneer uses the true position values, and showed that one of them reproduces the VCG outcome. Dütting, Fischer and Parkes treat the case of an estimate α different from the true vector β: Theorem 1 (complete information) and Theorem 2 (Bayes–Nash equilibrium of the first price variant). The preprint was posted in 2016 and appeared in Mathematics of Operations Research in 2024.
There are k positions and n ≥ k bidders. Let be the set of vectors with positive, non-increasing entries, extended by for . The true relative values are , and bidder values position at with . The auctioneer uses an estimate .
A bid profile is . An allocation is a ranking of the bidders in non-increasing order of bids, with ties resolved by . Write for the -th highest bid, and for . The bidder in position pays
and its utility in position at price is . For these are the VCG and GSP auctions.
An equilibrium is a profile in which no bidder gains by raising or lowering its bid and being assigned a different position (§3.1, p.8). Moving bidder to position leaves the other bidders in their order, and the mechanism charges its price for position on the new order. The equilibrium is efficient if also orders the values. A profile is envy-free (22) if no bidder prefers another bidder's position at that bidder's current price.
For every , every and every :
The values are not sorted, ties are allowed in , and , and the rankings are existential on both sides.
The milestones are stated in the paper's sorted frame (, bidder in position ):
The theorem compares the two mechanisms over all misspecifications at once. For every pair where the α-VCG mechanism can support an efficient outcome, so can the α-GSP mechanism. §3.1 of the paper shows that the converse fails. Running the "truthful" mechanism therefore buys no robustness, which is one argument for the non-truthful auctions used in practice. The proof also goes through an envy-free α-VCG profile and a map to α-GSP bids that keeps the payments, which describes the α-GSP equilibrium explicitly.
The result is proved on paper. As far as the platform's catalog shows, no part of it, and no position auction model, has a machine-checked proof. The mission produces the model (rankings, both payment rules, deviations, envy-freeness), which other work on sponsored search auctions can reuse, and a checked version of an argument whose statement needed correcting (next section).
The obvious approach compares the equilibrium conditions of the two mechanisms inequality by inequality, as the paper does for three positions in §3.1. In general the α-GSP conditions are not implied term by term: a bidder moving up in the α-GSP auction pays the bid of the occupant it displaces, not a sum of externalities. The paper instead passes through envy-freeness, which depends only on allocation and payments. The work is index-heavy: telescoping sums over positions, a recursively defined profile (26), and boundary positions beyond and beyond , where , and the order statistics are . The goal is stated for arbitrary rankings and unsorted values, so a relabelling to the sorted frame is also needed.
The equilibrium notion. On p.6 the paper defines a Nash equilibrium with deviations to every real bid under a fixed tie-breaking rule, and efficiency as " whenever ". With that definition Theorem 1 is false. Take , , , , . The α-VCG profile has no ties and is an efficient Nash equilibrium. An efficient α-GSP equilibrium would need . Bidder 3 must not take position 2, which gives , so . Bidder 1 must not drop to position 2, which gives . With this forces , a contradiction. The paper's proof uses the position-deviation conditions (23)–(24) of p.11. Under that notion, with ties resolved by the ranking (Lemma 2 produces the tie ), the argument is sound. Here the α-GSP profile is an efficient equilibrium.
Bidders are Fin n, and positions are 0-based ranks Fin n (rank is position ). Ranks are unassigned positions, worth and priced at . Rankings are Equiv.Perm (Fin n). and are functions on that are positive and non-increasing below and from on. Bids in rank order are padded with . Bids and values are non-negative. The equilibrium is the position-deviation equilibrium in both the hypothesis and the conclusion of Theorem 1; it is the mission's one declared correction. In Lemmas 1 and 2, positive vectors in are relaxed to non-negative sorted ones.
Efficiency is part of both sides of the goal. Dropping it, or replacing the deviation price with the current price of the target position (which is envy-freeness), would change the theorem. The sanity file checks that the example above behaves as described. In the model, is an efficient α-VCG equilibrium, is an efficient α-GSP one, and is not an equilibrium.
Everything is finite: sums over ranks, one permutation, real inequalities. No library beyond Mathlib is needed. Proofs of any milestone are welcome, as are a general relabelling lemma that reduces arbitrary rankings to the sorted frame and a proof of the strengthening that keeps the ranking fixed.
In Multiway Cut one is given an edge-weighted graph and terminals, and must delete a minimum-weight set of edges so that no two terminals remain connected. Equivalently, one labels every vertex by a terminal, each terminal by itself, and pays for the edges whose endpoints get different labels. The problem is APX-hard for every fixed (Dahlhaus et al., 1994), and it is a standard test case for rounding geometric relaxations.
Timeline of the approximation ratio obtained by rounding the simplex relaxation:
An instance consists of a finite vertex set , a finite edge set of pairs , weights , and distinct terminals . A feasible labeling is with ; its cost is the total weight of the edges with .
The simplex relaxation embeds every vertex as a point of the simplex , with , and minimizes . A rounding maps the points to labels at random:
The transformation of the paper sorts the coordinates of as , forms the vectors , sets
for an explicit symmetric matrix (display (5.3) of the paper, nonzero only in its first three rows and columns and in ), and puts the values back in the original coordinate order. The cut density of a rounding at an edge that moves mass between the -th and -th largest coordinates (an -edge) is the limiting separation probability per unit .
With and the matrix (5.3), for every , every instance and every feasible embedding : both branches label the terminals correctly almost surely, and
hence for every feasible when is an optimal embedding.
The theorem shows that the barrier of Sharma and Vondrák concerns only coordinate-wise transformations: a transformation that couples the coordinates through their sorted order reaches with the two original ingredients and a proof checkable by hand. The approach (choose a feasible transformation, then bound the density by a sum of absolute values of linear forms) is a template for other partitioning relaxations.
The result is proved in the paper; nothing here is open. No part of it has a machine-checked proof. Formalizing it checks a long case analysis (the proof of Lemma 5.4 spans pp.8–11) and the reduction from cut density to the approximation ratio, which the paper calls "easy to show" and which, read with the lim sup of Definition 2.1, needs a correction (see below).
The obvious route, "bound the cut density and conclude by the Karger et al. argument", fails as stated: a bound on a pointwise does not control the separation probability of a long edge, because a labeling can jump between nearby points in a way invisible to every one-sided limit. The mission therefore states the per-edge bound with a remainder uniform over all edges, and the reduction with that hypothesis. Proving the uniform remainder for Algorithm 3 requires following along an edge exactly, not only its derivative.
The second obstacle is Lemma 5.4: removing the absolute values in (5.2) needs the chain of prefix-sum dominations of Observation 5.1 and Lemma 5.3, then a case analysis over and with exact rational arithmetic. The exponential-clocks bound (Lemma 2.1) needs the competing-exponentials computation and a coupling of two argmins.
Coordinates and terminals are Fin k, indexed from ; is stdSimplex ℝ (Fin k). The clocks' law is Measure.pi of expMeasure 1; the argmin runs over the support of by cross-multiplication (Lean's would otherwise let a zero coordinate win). CKR's law is the average over permutations of Lebesgue measure on . Probabilities are measures of events (outer measures), never integrals of indicators, so non-measurability cannot make a bound vacuous; expected costs are . "" is the eventual form "for every , eventually ratio ". The transformation uses Mathlib's Tuple.sort; its value does not depend on how ties are sorted. The matrix (5.3) is defined for every by its entry formula.
A trivializing formalization is excluded: the goal keeps the terminal clause (otherwise labeling everything costs nothing), and constants , and the matrix entries are fixed.
A complete development needs: the competing-exponentials law , the CKR union bound, the subdivision of a segment of into order-preserving steps, and exact rational arithmetic for the case analysis. The first three are reusable for any analysis of simplex-relaxation roundings. Proofs of individual milestones, and of the reduction (p.4) independently of this algorithm, are welcome.
Many allocation procedures used in practice — school choice, university admissions, course allocation — are run as one-shot direct mechanisms: every participant submits a full ranking, and an algorithm such as deferred acceptance or top trading cycles computes the assignment. Sequential alternatives, in which participants repeatedly pick one option from a menu, may see their pick rejected, and are then offered a smaller menu, have been proposed and studied for college admissions; the iterative deferred acceptance mechanism is the leading example (Bó and Hakimov, Games and Economic Behavior 135, 2022), and laboratory evidence finds more truthful behaviour under it than under its direct counterpart (Bó and Hakimov, The Economic Journal 130, 2020). Two questions arise: which allocation rules can be run this way at all, and when is it in every participant's interest to pick truthfully?
Bó and Hakimov, Pick-an-Object Mechanisms (arXiv:2012.01025v4) answer both questions for a general class of sequential procedures, and the answer is a pair of characterizations. This mission formalizes them.
is a finite set of agents and a finite set of object types containing the null object . Each agent has a strict preference over all of ; objects ranked below are unacceptable, and means or . A rule maps every preference profile to an allocation . There is no capacity constraint: feasibility is whatever the rule produces. A rule is individually rational if and strategy-proof if no agent gains by reporting another preference.
A choice history is a sequence of menus and choices ; a collective history has one per agent, and is the one in which no agent has chosen yet. A menu function assigns every agent a menu at every collective history, subject to two rules:
The pick-an-object (PAO) mechanism of runs in periods. If every menu is empty, it stops and each agent receives her last choice. Otherwise every agent with a non-empty menu picks one element, and the history grows. A straightforward agent always picks her most-preferred element of the menu. sequentializes if, for every profile , straightforward play from ends at .
The lower contour set is the set of profiles such that, for each agent , has the same objects strictly above as , in the same order. A rule satisfies monotonic discoverability if for every allocation and profile , either , or some agent has for every .
A strategy chooses an element of the current menu as a function of the agent's own choice history. Straightforward strategies form a perfect ex-post equilibrium of if, at every collective history that can produce (under arbitrary past choices) and for every profile , no agent gains by deviating to any other strategy from on. A rule is pick-an-object implementable in perfect ex-post equilibrium if some sequentializes it with straightforward strategies forming such an equilibrium.
For every individually rational rule :
and, if is PAO-implementable in perfect ex-post equilibrium, straightforward strategies form a perfect ex-post equilibrium of every menu function that sequentializes .
Theorem 1 says exactly which rules a PAO mechanism can run, and shows that the restriction is real: not every rule can be sequentialized, because a rejected choice can never be offered again. Proposition 1 of the paper (not part of this mission) places deferred acceptance, top trading cycles and the Boston mechanism inside the class. Theorem 2 adds incentives: among sequentializable rules, the strategy-proof ones are exactly those for which truthful picking is a best response after every history, against every deviation, for every preference profile — and this holds in every PAO mechanism for the rule, not in a specially designed one. For a designer this means the choice of menus can be made for simplicity or transparency without affecting incentives.
On the formal side, the mission produces a reusable model of sequential menu mechanisms for ordinal object allocation (histories, menu functions, an executable run, strategies, perfect ex-post equilibrium), which the platform does not have; existing items cover strategy-proofness of fixed algorithms (top trading cycles, deferred acceptance) and obviously strategy-proof mechanisms for scheduling. The paper's results are proved on paper only; none is machine-checked. The printed proof of Theorem 1's "if" direction relies on a canonical mechanism (§3.3) that does not sequentialize every monotonically discoverable rule (a two-agent serial dictatorship already fails), so a complete formal proof must supply a different witness.
The equilibrium part is the hard one. Perfect ex-post equilibrium is required at every history, including histories in which agents have already made arbitrary non-truthful choices. Strategy-proofness of speaks only about complete reports from , so it does not directly compare two continuations after such a history. The bridge is Lemma 1: every history of the mechanism must be rationalized by preferences (the tuples ), the continuations under truthful and deviating play must be re-expressed as straightforward play from the beginning under modified profiles, and the comparison must be made through recursive dominance. Keeping the same in both representations is essential and is where a careless argument breaks.
For Theorem 1, the natural first idea — elicit the whole preference profile with menus and then assign — is not available: menus must shrink and the agent keeps her last pick, so information about lower-ranked objects can only be obtained by permanently rejecting her current choice. The "only if" direction must turn this informational constraint into monotonic discoverability. The "if" direction needs a menu function that rejects only choices that are no longer attainable.
Object types are Option Obj for a finite type Obj, with none the null object. A strict preference is a ranking Option Obj ≃ Fin (card (Option Obj)) (rank is best), so every strict linear order is represented exactly once. Allocations are arbitrary maps . Histories are lists of (menu, choice) pairs, oldest first. The run is the -fold iterate of one period of the mechanism; with menus that strictly shrink, this is enough for the procedure to stop from any history, and a stopped history is a fixed point. Strategies are functions of the agent's own history and current menu that pick from every non-empty menu. The collective histories of are an inductive predicate: and everything reachable from it under arbitrary choices from the offered menus. The menu-shrinking constraint is not imposed at histories other than in which some agent has never faced a menu, which the mechanism never produces.
The lower contour set is corrected. The display on p.12 constrains only pairs of objects strictly above ; with it, the one-agent rule " iff " on is individually rational and sequentialized by the single menu , but fails Definition 3 at , , , so Theorem 1 would be false. The formalization uses the reading stated in the sentence under the display (same objects above , in the same order). Likewise, the canonical mechanism of §3.3 is not used as the witness for Theorem 1 and is not part of the formalization.
Restricting perfect ex-post equilibrium to histories generated by straightforward play, or allowing a deviation to "choose" an object outside the menu, would change the equilibrium notion; neither is done.
Needed infrastructure: finite permutations and rankings, list and finset manipulation, induction over reachable histories, and a determinism and termination analysis of the run. The model definitions and the representation of outcomes after arbitrary histories (Lemma 1) are reusable for other sequential mechanisms. Proofs of any milestone, a formal proof that the run's period bound suffices, and alternative witnesses for Theorem 1 are welcome.
When independent firms pool resources, they can share not only a deterministic profit but a random one, chosen through a joint decision. Cooperative models for operations management usually value such payoffs in expectation or by a concave utility, and then bargain over the expected values. Gutjahr, Kovacevic and Wozabal (author manuscript) replace this with coherent acceptability functionals in the sense of Artzner et al. (1999), the class that contains expectation and the Average Value-at-Risk, and ask which sharing rule follows from axioms alone. The classical axioms of Nash (1950) are stated for deterministic utility pairs. The relevant comparison for this mission is the splitting axiom of Hougaard (2009), which the paper carries from deterministic allocation to random payoffs.
Fix a probability space, an exponent , and a compact topological space of decisions. An instance for a finite nonempty player set consists of endowments , a profit for each decision , with continuous into with the weak topology, and coherent acceptability functionals , that is, monotone, positively homogeneous, super-additive and translation invariant. Write . The set of feasible acceptability allocations is
and is the maximum of over the same constraints, which is problem (8). A bargaining solution selects a point of for each instance. It is asked to satisfy PAR (Pareto optimality), SYM (equal treatment when all values agree and is permutation invariant) and STR (a player who splits into copies, each with endowment , receives the same total).
On the class of admissible instances, those with all for which the maximum in (8) exists, put
The goal has four clauses: (a) rule (9) is a bargaining solution; (b) a bargaining solution agreeing with (9) satisfies PAR, SYM, STR and CONT; (c) a bargaining solution with PAR, SYM, STR agrees with (9) wherever the are natural multiples of one positive real; (d) a bargaining solution with PAR, SYM, STR, CONT agrees with (9) everywhere. CONT requires to be continuous along scalings with .
The milestones are: Proposition 2 (the polytope (7)), Proposition 1 (compactness, as an equivalence with attainment), Lemma 5 ( does not depend on the endowments), invariance of and of the class under splitting, the identity under PAR, the commensurable case (clause (c)), the converse (clauses (a), (b)), and two counterexamples.
The result gives a sharing rule for risk-averse partners with a closed form: the shares depend only on the values , and the decision enters only through . So a joint decision can be separated from the division of the surplus, which is what makes the rule usable in stochastic optimization models.
The theorem has been published, but the formalization adds more than a check, because the printed statement is false in two ways, and the mission records both as machine-readable counterexamples. Nothing in this mission has a previous machine-checked proof on the platform. The two-player Nash theorem there uses different axioms and yields a different solution.
The obvious route from rational to real values fails. The printed proof treats by splitting and symmetry and then appeals to the continuity of the right-hand side of (9). That continuity says nothing about , and SYM only compares equal values while STR only divides a value by an integer, so two players with are never connected. The second obstacle is structural: Axiom STR splits one player at a time, the player type changes at every step, and no relabelling invariance of is assumed.
Corrections. Two corrections to the printed Theorem 1 are part of the statement. First, CONT is added to the characterization, and clause (c) keeps what the printed axioms give; the witness is a rule that differs from (9) at , and meets PAR, SYM, STR at every admissible instance. Second, the class requires the maximum in (8) to exist: on with the uniform probability there is a feasible instance, with , where it does not exist, is not compact, and no rule can satisfy PAR. Proposition 1 and Proposition 2 are restated accordingly. Lemma 4 of the paper is false and is not used.
Representation. is Lp ℝ p μ with p : ℝ≥0∞, 1 ≤ p (so is admitted), and is a map X → Lp ℝ p μ. Functionals are real-valued. No continuity of , no bound and no dual representation is assumed. Player sets are finite nonempty types and a rule is a family over all of them, because Axiom 3 changes the player set. A split player set is {j // j ≠ i} ⊕ Fin ℓ with ℓ : ℕ+. The real is a sSup and equals the maximum exactly on attained instances; every item mentioning assumes attainment.
Non-triviality. Clause (a) shows that the hypotheses of (c) and (d) can be met, so neither is vacuous, and the class is not empty: it contains every instance with constant endowments and expectations whose total does not exceed a constant profit. Defining through , or adding an axiom that depends only on , would assume part of the conclusion; neither happens here.
Infrastructure. The development needs coherent functionals on Lp, the polytope description of , and the split and scaling operations on instances. Coherent acceptability on is reusable for other risk-averse models. Contributions that connect these definitions to Average Value-at-Risk are welcome.