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.
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?
In a stochastic multi-armed bandit a player repeatedly chooses one of distributions ("arms") and observes a reward drawn from it; the goal is to collect as much reward as possible, which amounts to pulling suboptimal arms as rarely as possible. Lai and Robbins (1985) showed that any reasonable strategy must pull a suboptimal arm at least times up to horizon , where is a Kullback–Leibler divergence between arm and the best arm, and Burnetas and Katehakis (1996) extended the bound to general models. Strategies matching this rate are called asymptotically optimal.
The popular UCB algorithms of Auer, Cesa-Bianchi and Fischer (2002) use Hoeffding-type confidence bounds and are not asymptotically optimal outside special cases. Cappé, Garivier, Maillard, Munos and Stoltz (Ann. Statist. 41(3), 2013; arXiv:1210.1136) analyse kl-UCB, which replaces the Hoeffding radius by a Kullback–Leibler confidence region, and prove a finite-horizon bound whose leading term is exactly the Lai–Robbins constant. This mission formalizes that result for one-parameter exponential families (Theorem 1), the main-text steps of its proof skeleton, and its two corollaries for bounded rewards.
Timeline: Lai and Robbins (1985) lower bound and asymptotically optimal index policies; Agrawal (1995) sample-mean based index policies; Auer, Cesa-Bianchi and Fischer (2002) finite-time analysis of UCB1; Garivier and Cappé (2011) kl-UCB for bounded rewards; Cappé et al. (2013) the unified analysis formalized here.
A canonical exponential family is given by a dominating measure on and a function , with densities . The parameter set is the natural parameter space , assumed to be an open interval (the family is regular), and is twice differentiable. The mean of is , an increasing function, so is determined by its mean in the open interval . The divergence (11) is
extended by continuity to the closure , possibly with the value .
There are arms with laws and means ; . At each round the player picks an arm based on the past and receives a reward drawn from . is the number of pulls of arm in rounds , and the mean of the rewards obtained from arm so far.
kl-UCB (Algorithm 2) with a nondecreasing exploration function pulls each arm once and then, for , pulls an arm maximizing the index
With for and , for every suboptimal arm and every horizon ,
where and is the derivative in the first argument.
Corollary 1 (p. 17, kl-UCB with the Bernoulli divergence for arbitrary rewards in ) and Corollary 2 (p. 18, UCB with radius ), stated as separate theorems.
Theorem 1 shows that kl-UCB is asymptotically optimal in every regular one-parameter exponential family (Bernoulli, Poisson, Gaussian with known variance, exponential, Gamma with known shape), and it does so with an explicit bound valid at every horizon, not only in the limit. Corollary 2 improves the constants of the classical UCB1 analysis, and Corollary 1 shows that the Bernoulli kl-UCB index is uniformly better than UCB for all bounded rewards.
The result is proved in the paper; its proofs are in the supplemental article (DOI 10.1214/13-AOS1119SUPP, Appendix A), not in the main text. No machine-checked version exists. The platform has a formal analysis of a Bernoulli KL-UCB variant with another exploration function (Lattimore–Szepesvári's Theorem 10.6), which is a different statement. The formalization adds the general exponential-family index, the random-sample-size deviation bound (13) and the full finite-time constant.
The obvious argument bounds by a union bound over the possible values of , which costs a factor and destroys the logarithmic rate. The deviation bound (13) has to control an empirical mean whose number of summands is chosen by the algorithm itself, losing only a factor over the fixed-sample Chernoff bound; this is the step that needs the strategy to be non-anticipating. The second-order terms depend on the curvature of between and , measured by and , and the explicit constants must be tracked through every step. The empirical mean can be an endpoint of (Bernoulli rewards at small sample sizes), where is only defined as a limit.
The rewards are a stack (the -st reward of arm ), mutually independent and i.i.d. per arm, the representation of §2.2; this is the platform's RegretBandits.Stochastic.IsStochasticBandit, and the law of is pinned to . Arms are Fin K. The exponential family is the platform's OptimalBAI.OptProportions.ExpFamily (with , i.e. strict convexity, which the page derives); the natural-parameter-space condition is a separate hypothesis. A run of kl-UCB is a pathwise predicate: rounds pull every arm once and later rounds pull an argmax of the index, ties broken by any rule. The arm choices are measurable and non-anticipating (a measurable function of the arms and rewards already observed). The index (12) is a real supremum over a set containing the empirical mean, so it is never a junk value, and the divergence at an empirical mean on the boundary of is computed in . Statement (13) is made for : at its printed right-hand side is .
A trivializing formalization is ruled out: the run predicate forces both initialization and argmax, the index sets are nonempty and bounded, the reward stack is independent under the probability measure, and the Bernoulli divergence is never evaluated at or .
A complete development needs exponential-family calculus (convex conjugate of , continuity of up to the boundary), Chernoff bounds for exponential families, a peeling/maximal inequality for random sample sizes, and the counting arguments of §3.1. The deviation bound and the counting arguments are reusable for every index policy on the platform.
Sparse graphs with small nontrivial eigenvalues, expanders, are basic objects in combinatorics and theoretical computer science. They are used in error-correcting codes, derandomization, sorting networks, and the analysis of random walks. The Alon–Boppana bound says that a -regular graph on vertices has a nontrivial eigenvalue of absolute value at least (Alon 1986; Nilli 1991). Graphs that reach are Ramanujan graphs.
The classical explicit Ramanujan graphs of Lubotzky, Phillips and Sarnak (1988) and Margulis exist only for degrees with prime, and only for very sparse sequences of vertex counts. Constructions with for every degree came from Mohanty, O'Donnell and Paredes (STOC 2020, arXiv:1909.06988), but their graphs also do not have every number of vertices. Alon (arXiv:2003.11673, Combinatorica 41, 2021) asked for near-Ramanujan graphs of every degree and every large size. Theorem 1.3 of that paper answers this up to : for every , every and every large with even there is an explicit -graph with .
A -graph is a -regular simple graph on vertices in which every nontrivial eigenvalue of the adjacency matrix has absolute value at most . The trivial eigenvalue is , with the constant eigenvector . Equivalently, every eigenvalue of with an eigenvector , , satisfies .
Distances are graph distances, and they are between components. The -neighbourhood of a vertex is . The -neighbourhood of an edge is , and is the set of vertices at distance exactly from . A set contains no cycle if the subgraph induced on it is a forest. A ball contains at most one cycle if its induced subgraph has at most as many edges as vertices.
The construction starts from a -regular graph on a vertex set and a set . Write for the set of neighbours of , and let be a perfect matching on . Then is the subgraph induced on , is the graph of matching edges , and .
Let , , . Suppose is an -graph in which the -neighbourhood of every vertex contains at most one cycle, and . Then for every with even and ,
The hypotheses on are what Theorem 3.3 (Mohanty–O'Donnell–Paredes) supplies, and that theorem is not formalized.
Theorem 1.3 shows that the size restrictions of algebraic Ramanujan constructions cost nothing spectrally: up to an arbitrarily small , the Alon–Boppana bound is attained by explicit graphs on every admissible vertex count. The deletion method is local. It turns any near-Ramanujan graph whose short cycles are sparse into graphs of all nearby sizes, so it applies to future constructions as well. Lemma 3.2 is a self-contained delocalization statement in the tradition of Kahale 1995: eigenvectors of eigenvalues at least in absolute value cannot concentrate near tree-like edges.
The result is proved on paper. To our knowledge none of it is formalized; Mathlib has adjacency matrices, extended graph distance and acyclicity, but no theory of expanders. A complete development would give machine-checked versions of a delocalization lemma, of the greedy selection of far-apart vertices away from short cycles, and of the variational eigenvalue bound for induced subgraphs. It would also check two points the paper passes over. The proof of Theorem 1.3 treats only positive eigenvalues . And its claim that the -neighbourhood of a matching edge is cycle-free fails when two deleted vertices are at distance exactly . This mission states the corrected forms (see Formalization scope).
The spectral bound for does not follow from interlacing alone. Deleting vertices is harmless, since by (9) the quadratic form of is controlled by . But the added matching contributes up to to , which can be as large as for an eigenvector concentrated on . The obvious estimate therefore gives only . Closing the gap requires showing that an eigenvector of a large eigenvalue spreads its mass over the layers around each matching edge (Lemma 3.2). That in turn needs those neighbourhoods to be trees in and pairwise disjoint, which is where Lemma 3.1's choice of is used. The combinatorial part, tracking distances and cycles in when mixes edges of with matching edges, is the main formalization burden.
SimpleGraphs with real adjacency matrices adjMatrix ℝ. The (n, d, λ) predicate requires IsRegularOfDegree d, symmetry, row sums , and for every eigenpair with , . Distances use the extended SimpleGraph.edist, never dist (which is across components). Cycle conditions are on induced subgraphs, and "at most one cycle" on a ball is . Deleted vertices are a Finset U; the new graph lives on the subtype {v // v ∉ U}. The matching is a fixed-point-free involution of .Many problems in machine learning and statistics are regularized empirical risk minimization: minimize an average of loss terms, one per data point, plus a regularizer such as . When is large, a full gradient costs component gradients, so stochastic gradient methods that touch one per step are preferred. Variance-reduced methods (SVRG, SAGA) correct the stochastic gradient with a periodically recomputed full gradient and reach the rates of full-gradient descent at the cost of stochastic steps; accelerated full-gradient methods (Nesterov) improve the rate from to on convex problems.
Combining the two directly was open until Allen-Zhu's Katyusha (arXiv:1603.05953, STOC 2017, JMLR 2018). Before it, accelerated stochastic rates were obtained either for special structure (accelerated coordinate and dual methods, which need strong convexity or dual access) or through reductions such as Catalyst and APPA, which wrap a non-accelerated method in an outer proximal-point loop and lose logarithmic factors. Katyusha adds a third momentum term, the Katyusha momentum, that pulls each iterate back to the snapshot point, and obtains the accelerated rate directly. This mission concerns the paper's second main result: the variant Katyusha (Algorithm 2) for objectives that are convex but not strongly convex.
Problem (1.1) of the paper is
where , each component is convex and -smooth, , and the regularizer is convex. A point minimizes .
Katyusha runs epochs of iterations each (the paper takes ). It keeps three sequences , and a snapshot , all starting at , and fixes . Epoch uses the weight and the step , computes once, and performs, for :
At the end of the epoch the new snapshot is the average . The output is . Throughout, and .
The paper states ; the explicit form above is what its proof in Appendix C.1 establishes.
Theorem 4.1 gives the accelerated rate for non-strongly convex composite finite sums with a direct method: error after stochastic gradient evaluations, a factor better than the of non-accelerated variance-reduced methods such as SAGA (Remark 4.2). The non-strongly convex case covers -regularized and unregularized convex losses, where no strong-convexity parameter is available to tune a linear-rate method.
The result is proved in the paper; no machine-checked proof of Katyusha or Katyusha is known to exist. The mission produces a formal statement of the algorithm and its rate with explicit constants, and a formal chain of the paper's intermediate inequalities. A SAGA mission on this platform states SAGA's non-accelerated rate for the same problem class, so the two results become directly comparable in Lean.
Each step uses only convexity, smoothness and the optimality of proximal points, but the steps interlock. The variance of cannot be bounded by as in SVRG's analysis without losing acceleration; the paper's bound (Lemma 2.4) leaves a linear term that is cancelled only by the specific weight of the Katyusha momentum (Lemmas 2.6–2.7). Without strong convexity the per-epoch inequalities do not contract, so the proof must telescope across epochs with epoch-dependent weights : the coefficients of produced by epoch must dominate those consumed by epoch , and the snapshot term must be charged to the previous epoch's iterates. Getting the boundary epoch (whose snapshot is ) and the last epoch right is where the constants come from.
The Lean development works on EuclideanSpace ℝ (Fin d) with components indexed by Fin n (). Gradients are given functions tied to by HasGradientAt; -smoothness is the Lipschitz bound on them with ; convexity is ConvexOn ℝ Set.univ. and are the published SAGA.Convex.fAvg and SAGA.Convex.gradAvg. The regularizer is real-valued and convex, so extended-valued regularizers such as indicator functions of constraint sets are not covered. The two arg-min steps are evaluated through a map assumed to return a proximal point of (the published SAGA.Convex.IsProxPoint) for every positive step; for real-valued convex such points exist and are unique, so the hypothesis is satisfiable. is assumed to minimize (without strong convexity a minimizer need not exist). Randomness is modelled by finite sequences of indices: the expectation is the uniform average over all index sequences (SAGA.Convex.expectIdx), with the indices split into epochs by Mathlib's finProdFinEquiv.
Conventions committed to:
A trivializing formalization is ruled out: the prox map, the gradients and are all tied to , and by hypotheses that a quadratic instance satisfies, and the expectation averages over every index sequence rather than a chosen one. The iteration count stated "in other words" after Theorem 4.1 is not a target.
Contributions welcome: proofs of the milestones in any order; general lemmas about proximal points of convex functions (the three-point inequality behind Lemma 2.5) and the co-coercivity of convex -smooth functions (behind Lemma 2.4) are reusable beyond this mission.
A graph is perfect if every induced subgraph has chromatic number equal to its clique number. Berge conjectured in 1961 that a graph is perfect exactly when it contains no odd hole and no odd antihole. Chudnovsky, Robertson, Seymour and Thomas proved this strong perfect graph theorem in 2006 (Ann. of Math. 164 (2006), 51–229). Perfect graphs matter beyond graph theory: for them the stable set polytope is described by clique inequalities, so maximum weight stable set and colouring problems become polynomially solvable linear programs (Grötschel, Lovász and Schrijver).
The proof reduces the theorem to a decomposition statement (1.3 of the paper): every Berge graph is basic or admits one of a few decompositions. That statement is in turn proved in twelve steps, listed as 1.8.1–1.8.12. Each step excludes one kind of configuration from a Berge graph without the decompositions. This mission is step 1.8.5, restated as 13.4: it deals with Berge graphs that contain a long odd prism but no appearance of . It is the only step of the proof that needs proper 2-joins in the complement and proper homogeneous pairs.
All graphs are finite and simple; is the complement of . A path is an induced subgraph which is a path, and its length is its number of edges. An antipath is a path of . A hole is an induced cycle of length at least , and an antihole is the complement of a hole of . is Berge if every hole and antihole of has even length.
A prism consists of two disjoint triangles , and three paths from to , such that the only edges between different paths are the triangle edges. It is long if some has length , even if all three lengths are even, and odd otherwise.
A subdivision of a graph replaces every edge of by a track, these tracks being disjoint except at their ends. appears in if is isomorphic to an induced subgraph of for some bipartite subdivision of , where is the line graph.
The decompositions in the conclusion (pp. 53–54):
The intermediate objects come from Sections 11–13 of the paper:
Let be Berge with no appearance of in or in , and suppose contains a long odd prism as an induced subgraph. Then
In the order of the paper's argument:
13.4 removes long prisms from the analysis. Combined with 10.6 (the even prism), it shows that a recalcitrant graph contains no long prism in or , which places it in the class (p. 154). The later steps (double diamonds, odd wheels, pseudowheels, wheels) all assume this. The step-connected strip and staircase method developed here is also the paper's model for growing a maximal structure and then classifying how the rest of the graph attaches to it.
The theorem has been proved since 2006; no machine-checked proof of it or of any of its steps is known. The proof of 13.4 also cites these results of the same paper, which are posed in other missions of this series:
The difficulty is the volume of case analysis behind every statement. The paper does not prove the exact analogue of the even-prism result 10.6. It warns (p. 127) that it does not know whether that analogue holds, and adds the two extra outcomes instead. The obvious first idea is to take a long odd prism and analyse attachments to it as in Section 10. The paper does not get the result that way (p. 127): it replaces two of the three paths by a maximal step-connected strip. Controlling how every remaining vertex or connected set attaches to such a strip is what the breaker results do. Maximality is also delicate. "Strongly maximal" refers to staircases of the complement, so and must be handled in one framework.
Graphs are SimpleGraph V on a Fintype vertex type with decidable equality. is Gᶜ.
G.induce X, so is connected. Anticonnectedness is the same notion in Gᶜ.Every hypothesis of the paper is kept. "No appearance of " is in and in for the goal, and in for the milestones. The goal also keeps "Berge", "no even prism" and "no 1-/2-breaker" where the page has them. 12.1's "exactly one" is an exclusive disjunction. 11.4 is a non-existence statement.
A formalization with non-induced paths, with the complement dropped from "one of ", or with a strip, staircase or breaker predicate that no graph satisfies would make the targets empty or false. The definitions here are checked against a concrete graph: the 8-vertex prism with path lengths is a long odd prism, and it carries a staircase. Contributions are welcome: proofs of the milestones, and reusable material on induced paths, holes and line graphs of subdivisions.
Two-stage adaptive optimization models decisions taken in two steps: a first-stage decision is fixed before an uncertain right-hand side is revealed, and a second-stage decision is chosen after it, as a function of . The objective protects against the worst in an uncertainty set . Computing an optimal fully adaptable solution is intractable in general (Feige, Jain, Mahdian and Mirrokni, IPCO 2007), so practitioners restrict the second stage to affine policies , introduced in robust optimization by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 2004). An optimal affine policy is computed by a single convex program, but its cost may exceed the adaptive optimum.
Bertsimas and Goyal (Math. Program. Ser. A, 2012) quantify this loss. Earlier, Bertsimas, Iancu and Parrilo (Math. Oper. Res. 2010) proved affine policies optimal for a class of one-dimensional multistage problems. The present paper shows that affine policies are optimal when is a simplex (Theorem 1), that they can lose a factor in general (Theorem 3), and — the subject of this mission — that when the first-stage constraint matrix is nonnegative they never lose more than (Theorem 4). Nonnegative first-stage matrices occur in network design, facility location, capacity planning and other covering problems.
Let , , , , and let be convex, compact and full-dimensional. The problem is
where the minimum is over first-stage vectors and arbitrary maps . The problem is assumed feasible. The value is the same minimum restricted to affine second stages , which must still satisfy on .
For each coordinate put and fix a maximizer with (display (38)). The scaled sum of over an index set is .
Algorithm (Fig. 1 of the paper) starts with and . While some has scaled sum over larger than , it picks a maximizer of that scaled sum, adds to the running vector on the coordinates of , and moves to every coordinate whose running value has reached . It returns the number of iterations , the vectors , their sum , and the partition .
In the -uncertain variant (60)–(63), only right-hand sides are uncertain and the remaining are fixed at ; all data are nonnegative. Its values are and .
If entrywise, then a feasible affine solution exists and
Theorem 4 is an upper bound on the price of restricting to affine policies, and Theorem 3 of the same paper shows it is tight up to a constant factor: for every there are instances with where the gap is . Together they settle the order of the approximation ratio of affine policies for covering-type two-stage problems. Theorem 5 refines the bound to when only of the right-hand sides are uncertain, which is the regime of many applications. The construction is also the template for the paper's Theorem 6, a -approximation for general obtained from a single dominating simplex.
The results are proved in the paper. To the knowledge of this mission, none of them has a machine-checked proof. Formalizing them produces a reusable model of two-stage adaptive linear programs with affine policies, a verified analysis of a greedy covering procedure (Algorithm ), and an explicit-constant version of an statement.
The obvious attempt scales the fully adaptable solution at the extreme points linearly in : . This is feasible at cost factor only when the scaled sums stay below on (condition (39)); in general they can reach , and the linear rule then costs a factor . The difficulty is to handle the coordinates where has large scaled mass. Algorithm isolates them, and the delicate point is the iteration count: each round must add scaled mass above , while the total scaled mass that can be absorbed before every coordinate leaves is at most . A formal proof must also track the algorithm's state through its recursion, because the argmax choices are not unique and the statements must hold for every run.
Vectors are Fin m → ℝ with the componentwise order, indices are 0-based, and matrices are Matrix (Fin m) (Fin n) ℝ. Nonnegativity of a matrix is stated entrywise. and are infima of the set of worst-case cost bounds achieved by feasible solutions; the goal and Theorem 5 assert the existence of a feasible affine solution, which rules out the trivializing reading in which is the infimum of an empty set (Lean's junk value ) and the inequality holds for free. The goal does not mention , or Algorithm ; these appear only in milestones.
and are given with their defining properties ( is the greatest value of on , and with ). Algorithm is encoded as a recursion on a choice sequence , with step 2(d) read as . A complete run requires the loop test and the argmax property at each iteration and the failure of the loop test at the end. The milestones on the constructed policy are stated for every feasible and every cost bound , so that no attainment of the optimum is assumed.
Standing assumptions of (1) carried by the goal: ; convex, compact, with nonempty interior; feasibility. Milestones drop the ones they do not use. Theorem 5 carries compactness and full-dimensionality of , which §5.1 does not repeat but its proof uses through Theorem 4. Lemma 11 assumes that is finite, since the paper's inequality is between extended reals.
A complete development needs: finite-dimensional linear programming facts (existence of optimal solutions is not needed), compactness arguments for the argmax in Algorithm , and manipulation of finite sums over Finset. The model of (1) and the analysis of Algorithm are reusable by the companion mission on Theorem 6. Contributions of proofs of any milestone, and of supporting lemmas about the recursion of Algorithm , are welcome.
Two-stage adaptive optimization models decisions made in two steps: a first-stage decision is fixed before an uncertain parameter is revealed, and a second-stage (recourse) decision may then depend on the realized value. In the robust version, the uncertain parameter ranges over an uncertainty set and the objective is the worst-case cost. Such models arise in capacity planning, network design and inventory problems with uncertain demand, where the demand is the right-hand side of the constraints.
Computing an optimal fully adaptable second-stage policy is intractable in general: the recourse is an arbitrary function of the uncertain parameter. The standard tractable surrogate, introduced by Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 99, 2004), restricts the recourse to an affine policy , whose optimization is a finite convex program. Practitioners report that affine policies often perform well, which raises the question of when they are optimal and how much they can lose.
Bertsimas and Goyal (Math. Program. Ser. A, 2012) answer this for problems with an uncertain right-hand side. Their Theorem 1 shows that affine policies are optimal when the uncertainty set is a simplex, that is, the convex hull of affinely independent points of . Their Theorem 2, the subject of this mission, shows that this is almost tight: one additional extreme point can make the best affine policy almost twice as expensive as the optimum.
Let , , , and let be an uncertainty set. The problem is
Here is the first-stage decision and is the second-stage policy; all inequalities between vectors are componentwise. The value is the same minimum restricted to affine policies with and ; an affine policy must still satisfy for every . Always .
The instance of (6) is defined for and an even integer . It has , , , , and
where , is the -th unit vector for , has entries in its first coordinates and in the others, and has in its first coordinates and in the others. Thus is generated by nonzero points. The last two are also extreme points when ; for or they lie in the convex hull of .
For a permutation of , write . A set is permutation-invariant with respect to if (Definition 2), and is the set (10) of permutations with .
Together with Theorem 1 of the same paper, Theorem 2 delimits exactly where affine policies are optimal for right-hand-side uncertainty: for a simplex they are, and with one more nonzero extreme point the gap can approach . The ratio is measured against the fully adaptable optimum, which is the quantity a practitioner gives up by choosing affine recourse. Later sections of the paper push the same construction to for sets with polynomially many extreme points and prove a matching upper bound; Theorem 2 is the simplest member of this family and isolates the mechanism.
The result is proved in the paper; to our knowledge it has not been machine-checked. The mission produces a formal model of two-stage adaptive linear optimization with uncertain right-hand side, the values and , and a verified lower-bound instance. The symmetrization statement (Lemma 3) is an instance of a general principle, that a convex problem invariant under a group has an invariant optimum, which is reusable well beyond this paper.
The upper bound requires a feasible policy, which can be written down. The lower bound on is a statement about all affine policies, an dimensional family, and cannot be checked policy by policy. The obvious attempt, testing an arbitrary affine policy against a few extreme points, fails because an asymmetric policy can trade cost between coordinates. The argument needs an optimal policy that is symmetric, which in turn needs both the existence of an optimal affine solution (attainment of a minimum over a non-compact set of policies) and the invariance of the instance under the permutations of and the swap of the two halves. Without the attainment step, a contradiction for every policy of cost at most yields only , not the strict inequality.
Vectors are Fin m → ℝ with the componentwise order, matrices are Matrix (Fin m) (Fin n) ℝ, is B *ᵥ x and is d ⬝ᵥ y. Indices are 0-based: the paper's coordinate is index , so "" is (i : ℕ) < m / 2, with natural-number division (exact since is even). is x ∘ τ for τ : Equiv.Perm (Fin m).
and are the infima of the sets of real numbers for which some feasible (respectively feasible affine) solution satisfies for all . This epigraph form avoids a supremum of a possibly unbounded function; on an infeasible instance the infimum would be Lean's junk value , which is why Lemma 1 also asserts the existence of the feasible solution of cost . Optimal solutions are stated by IsOptimalAff: feasible, with worst-case cost bounded by every bound achieved by any feasible affine solution. Affine policies must be nonnegative on , as in (1).
The instance is concrete, so the standing assumptions of (1) (nonnegative costs, compact convex full-dimensional , feasibility) are properties of the data rather than hypotheses. The goal adds no hypothesis to the page: , even and . For the statement is easy but still true. The three Claims are stated for any feasible affine solution with constant intercept and worst-case cost at most , which is exactly what the paper's proof uses about the symmetric optimal solution under its contradiction hypothesis (12). Lemma 1 drops the unused hypothesis . Definition 2 prints ""; the formalization reads as the set .
Replacing by the cost of one particular affine policy, stating the goal with , or bounding only policies with constant intercept would not be Theorem 2, and is ruled out: the goal compares the two optimal values with a strict inequality.
A complete development needs convex hulls of finite point sets in Fin m → ℝ, the existence of a minimizer for the affine problem (a linear program in with infinitely many constraints indexed by , reducible to the extreme points), averaging of optimal solutions over a permutation group, and elementary estimates with . Contributions of general lemmas on attainment of semi-infinite linear programs and on symmetrization of convex programs are welcome.
Sparse graphs whose adjacency spectrum is concentrated near zero, expanders, are used throughout theoretical computer science: in error-correcting codes, derandomization, sorting and routing networks, and the construction of pseudorandom objects (Hoory, Linial and Wigderson, survey). The best possible spectral expansion for a -regular graph is governed by the Alon–Boppana bound , and graphs attaining it, Ramanujan graphs, were constructed explicitly by Lubotzky, Phillips and Sarnak (LPS 1988) and by Margulis. These constructions exist only for special degrees ( with prime) and special numbers of vertices (orders of or ). Applications often need a graph of a prescribed size .
N. Alon's paper Explicit expanders of every degree and size (arXiv:2003.11673v1; Combinatorica 41, 2021) shows how to obtain explicit near-Ramanujan graphs on exactly vertices. This mission formalizes the spectral core of its Theorem 1.2: a Ramanujan graph on vertices can be enlarged to vertices, with degree raised by one, while the nontrivial eigenvalues stay within a constant factor of optimal.
Let be a finite set of vertices. A -graph is a -regular graph on vertices whose adjacency matrix satisfies for every nontrivial eigenvalue , that is, every eigenvalue other than the top eigenvalue of the constant vector . For a symmetric with , the nontrivial eigenvalues are those with an eigenvector satisfying . Graphs may carry loops, at most one per vertex, and a loop adds one to the degree: it is a diagonal entry of .
Fix an integer and let be an -graph on , a -regular Ramanujan graph. Let be new vertices and let be pairwise disjoint sets of vertices each. Put and . The graph on is obtained from by joining each to every vertex of and adding one loop at each vertex of . Its adjacency matrix is
where is the adjacency matrix of (zero on ), that of the stars joining to , and the diagonal matrix of the loops. Every vertex of has degree .
The paper states for ; its proof gives , which is stronger, and the error term it produces is . The goal is parametrised by , and the sets , so it does not depend on how and are chosen.
With the Lubotzky–Phillips–Sarnak graph on vertices for the largest suitable prime with , and , the distribution of primes in arithmetic progressions gives , and the goal yields an explicit -graph with for every sufficiently large . This is within a factor of about of the Ramanujan bound , for every number of vertices, by an elementary modification of an existing graph. The statement is useful independently of LPS: any Ramanujan graph, or any graph with a bound on its nontrivial eigenvalues, can be padded to a nearby size in the same way.
The result is proved in the paper. No formalization of it, of the notion, or of the variational characterization of nontrivial eigenvalues for regular graphs exists on the platform. The mission produces a checked version of the spectral argument, and the variational characterization (milestone 1) is a general fact about symmetric matrices with constant row sums that applies to any spectral expander argument.
The vertices of and lie in the old graph , whose spectrum is controlled, but the new vertices of are not; and a vector orthogonal to on need not be orthogonal to the constant vector on . Bounding by applying the Ramanujan bound for to restricted to therefore fails: the restriction has a component along the trivial eigenvector of , whose eigenvalue is large. The argument must show that this component is small, of order , and must balance the star edges between and against the loops on so that every vertex class gets the same coefficient. The naive bound added to for and for gives a constant larger than ; the stated constant needs the weighted estimate.
On the Lean side, milestone 1 concerns the spectrum of a symmetric matrix on the invariant subspace , while Mathlib states the spectral theorem for the whole space.
SimpleGraph with adjMatrix.An -graph is a -regular graph on vertices in which every eigenvalue of the adjacency matrix other than the top eigenvalue has absolute value at most . Graphs of this kind with small compared with are expanders. They are used in derandomization, error-correcting codes, sorting networks and many other constructions in theoretical computer science. A Ramanujan graph achieves , which is asymptotically optimal.
The classical explicit Ramanujan graphs of Lubotzky, Phillips and Sarnak (LPS, 1988) exist only for special vertex counts, such as for a prime or the size of a quaternion group modulo . N. Alon, in Explicit expanders of every degree and size (arXiv:2003.11673, 2020; Combinatorica 41, 2021), asks for explicit -graphs with for every degree and every number of vertices . His Proposition 1.1 builds such graphs out of LPS graphs, and one ingredient is purely arithmetic. If the available vertex counts of an LPS family are dense enough, so that for every large one is within a factor of , then a few vertices can be added or removed while keeping the spectral bound.
This mission formalizes that ingredient, Lemma 2.2 of the paper (p. 7). It concerns the vertex counts of the LPS graphs for two fixed primes and all exponents . With fixed, the construction needs no large primes, which is why Proposition 1.1 is strongly explicit for every fixed degree.
Fix natural numbers . For natural numbers define the LPS vertex count
When are distinct primes congruent to modulo and , this is the number of vertices of the LPS Cayley graph (§2.3, p. 6). Lemma 2.2 itself only requires to be distinct primes. Both fractions are integers, because is a product of three consecutive integers.
The proof uses the real number , and the fractional part , written in the paper.
For distinct primes there is a function with such that for all sufficiently large there are integers with
Equivalently, the ratio between consecutive elements of tends to . The statement fixes no rate for , matching the paper's .
The result. Lemma 2.2 is the step of Proposition 1.1 that turns a family of Ramanujan graphs with sparse vertex counts into a family whose vertex counts approximate every large up to a factor . The deviation from can then be absorbed by the general packing argument of §2.1 of the paper. Without it, the construction would have to search for large primes depending on , and the result would be explicit but not strongly explicit.
The formalization. The lemma is proved in the paper, in one paragraph. To our knowledge no machine-checked proof exists, and the platform has no statement of it. The only related platform item is the irrationality of , the case , of milestone 1. Formalizing the lemma requires a quantitative inhomogeneous step that the paper leaves implicit ("implying the desired result"). Its last sentence also contains a misprint that the formalization corrects (see below). The Diophantine milestones 1–3 are reusable for any argument about the multiplicative density of , for instance the ratio of consecutive elements of .
Each milestone is short. The difficulty is in making the paper's last sentence ("implying the desired result") into a proof. Taking or large separately does not work: changing or by one multiplies by or , a fixed factor larger than , so the values obtained by varying one exponent leave gaps of a constant ratio. The bound must hold for every large , not just along a subsequence, and the exponents must stay positive throughout. Milestone 2 is the classical fact that the multiples of an irrational number are dense modulo . It needs a pigeonhole argument, not just the irrationality.
Real.log, and the fractional part is Int.fract.IsLittleO along atTop) and, eventually in , with . This is equivalent to the form "for every , every large has with ". The paper's proof yields the second form, with the factor for arbitrary .Int.fract and a pigeonhole or Dirichlet-approximation argument for milestone 2, and real exponentiation and asymptotics for the goal. Contributions of alternative proofs of milestone 2, for instance via Mathlib's Dirichlet approximation theorem, are welcome.Large-scale nonsmooth convex problems, such as minimising a Lipschitz convex function over a probability simplex with millions of coordinates, are routinely solved by first-order methods that use one subgradient per iteration. The classical projected subgradient method reaches accuracy after iterations, where and are measured in the Euclidean norm; on the simplex this hides a factor of order in the dimension. Nemirovski and Yudin's mirror descent algorithm (MDA) replaces the Euclidean geometry by one adapted to the feasible set and, on the simplex, reduces the dimension dependence to .
Beck and Teboulle (Oper. Res. Lett. 31 (2003) 167–175, doi:10.1016/S0167-6377(02)00231-6) showed that mirror descent is a projected subgradient method in which the squared Euclidean distance is replaced by a Bregman-type distance . This viewpoint gives a short convergence proof, and with the entropy as it yields a fully explicit method on the simplex, the entropic mirror descent algorithm (EMDA), the same multiplicative update that underlies exponentiated-gradient and Hedge-type algorithms in online learning.
Timeline. Nemirovski and Yudin (1983) introduce mirror descent with a rate on the simplex. Ben-Tal, Margalit and Nemirovski (SIAM J. Optim. 12 (2001)) analyse MDA with the potential , , whose conjugate requires a one-dimensional root-finding at each step. Beck and Teboulle (2003) derive MDA as a nonlinear projected subgradient method (SANP), prove its efficiency estimate for an arbitrary norm, and show that the entropy gives the same rate with a closed-form update.
Let be with an arbitrary norm , and the dual norm. The problem is under Assumption A: is closed and convex; is convex on and Lipschitz there, ; has a minimiser ; and a subgradient can be computed at every .
Let be strongly convex with parameter and differentiable. The distance-like function (3.10) is
The subgradient algorithm with nonlinear projections (SANP, (3.11)) starts from and sets, with step sizes ,
With this is the projected subgradient method.
On the unit simplex take the entropy (5.27), with . SANP becomes the entropic descent algorithm (EDA):
If is convex and -Lipschitz on for , with subgradients satisfying , and the EDA is started at with step for a horizon , then
For any norm, any -strongly convex and any SANP run,
and with the optimal constant step this gives .
The milestones follow the paper's proof: the three-point identity (Lemma 4.1), the optimality condition (4.16), the lower bound , the one-step inequality (4.21), Theorem 4.1(a), Proposition 4.1 (optimal step), Theorem 4.2 and its version with an upper bound on ; then for the simplex, the 1-strong convexity of for (Proposition 5.1(a), Remark 5.1), the bound (Proposition 5.1(c)), and the identification of the EDA with SANP.
The result shows that for nonsmooth convex minimisation over the simplex an explicit first-order method attains accuracy in iterations, with measured in the dual norm. The general estimate of Theorem 4.2 applies to any norm and any strongly convex potential, and is the template for later analyses of mirror descent, its stochastic and online variants, and mirror-prox methods.
Formalizing the paper produces a norm-agnostic, machine-checked proof of the mirror descent efficiency estimate, in which subgradients are dual-space objects and the dual norm is explicit, and a verified link between the entropy, the geometry and the multiplicative-weights update. To our knowledge none of these statements is formalized; existing formal developments of online mirror descent work in Euclidean space with Legendre potentials and bound regret for linear losses, which is a different statement.
The algebra of Theorem 4.1 is short, but it rests on facts that are not available off the shelf. The first-order optimality condition (4.16) must be derived for a minimiser over a convex set without assuming the set has interior (the simplex has none in ). The bound must be obtained from the chord definition of strong convexity for an arbitrary norm. On the simplex, strong convexity of the entropy with respect to is a form of Pinsker's inequality, and it must hold on the closed simplex, where the entropy is not differentiable at the boundary. Finally, the EDA must be shown to be the exact minimiser of the SANP subproblem over , which is a Gibbs variational principle. A tempting shortcut, working throughout in Euclidean space, fails: it changes the dual norm of the subgradients from to and the strong convexity constant of the entropy, and loses the rate.
Sections 3–4 live in a general real normed space; a subgradient is a continuous linear functional, is its value at , and is the operator norm. is the Fréchet derivative. Iterates are indexed from . A SANP run is a predicate on sequences: each step size is positive, each iterate lies in , is differentiable there, and the next iterate minimises the SANP objective. This encodes the paper's standing assumption that SANP is well defined, and replaces " has nonempty interior" and "". Section 5 works on as functions with explicit and sums; is the relative interior, and the entropy formula is evaluated on only. "" is stated as the existence of with .
Added hypotheses, each disclosed in the item: a bound on the oracle (used by the proofs of Theorems 4.1(b), 4.2 and 5.1, not implied by the Lipschitz condition for subgradients relative to ); in Proposition 4.1, without which the proposition as printed is false; in the step sizes. The step sizes of (4.23) and of the EDA are constant over a fixed horizon , which is what the proof chooses; Theorem 5.1 is stated with , since the free index in the printed bound (5.28) cannot be bound, and is what the proof yields.
Trivializing formalizations are ruled out: is never evaluated where fderiv is a junk value (the run requires differentiability at every iterate), the SANP step is never chosen by Classical.epsilon, the bound of Theorem 5.1 is not stated with a maximum of over the run, and the step is not an anytime schedule .
A complete development needs first-order optimality conditions over convex sets, strong convexity and Bregman distances in normed spaces, Pinsker-type inequalities for finite distributions, and the Gibbs variational principle. These are reusable beyond this mission; proofs of any milestone, and general lemmas that serve several of them, are welcome.
A linear program is solved with data that, in practice, is rarely known exactly: coefficients come from measurements, estimates or forecasts. Robust optimization asks for a solution that remains feasible for every realization of the data in a prescribed uncertainty set, and among those the one with the best guaranteed objective value. Ben-Tal and Nemirovski introduced this framework for linear programming in Robust solutions of uncertain linear programs (Oper. Res. Lett. 25, 1999), following their treatment of robust convex optimization (Math. Oper. Res. 23, 1998) and Soyster's earlier work on inexact linear programming (Oper. Res. 21, 1973). The robust counterpart has since become the starting point of a large literature on uncertainty sets, budgets of uncertainty and adjustable policies.
A natural first objection is that the robust counterpart might be needlessly conservative: by demanding feasibility for all realizations simultaneously, it could be infeasible, or have a worse value, even when every individual realization is perfectly well behaved. This mission formalizes the paper's answer (§2.2): under two structural hypotheses, the robust counterpart is no worse than the worst realization.
Fix and write a linear program in the homogeneous form (6)
where is a real matrix and is componentwise. Every linear program can be put in this form. The matrix is uncertain: it is only known to lie in an uncertainty set of matrices. Each gives an instance with feasible set and optimal value ; the family of instances is . The robust counterpart (7) is
and its optimal value is . Since does not change when is replaced by its closed convex hull, the paper assumes throughout that is convex and closed.
Let be the set of all realizations of the -th row, the projection of onto the data of the -th constraint. The uncertainty is constraint-wise if : the rows vary independently. The Boundedness Assumption asks for a convex compact set that contains the feasible set of every instance.
If the uncertainty is constraint-wise and the Boundedness Assumption holds, then
The milestones follow the paper's proof: the row-wise description (8) of robust feasibility; the inclusion of in every instance's feasible set; the reduction of the semi-infinite system (8) on to a finite subsystem; the statement that the finite system (10) then has no solution at all; the Farkas certificate (11); the construction of one infeasible instance from it; and part (i) alone, which part (ii) uses for an augmented program.
The §2.2 example (every instance has optimal value 1, the robust counterpart is infeasible), and the two invariance remarks: is unchanged under passing to the closed convex hull of (§2.1) or to the product of its projections (§2.2).
Proposition 2.1 says that, for constraint-wise uncertainty, robustness costs nothing beyond what the worst realization already costs: the robust counterpart is feasible exactly when every instance is, and its optimal value equals the worst instance value. The §2.2 example shows the hypothesis cannot be dropped: there, correlated uncertainty in two rows makes every instance solvable with value 1 while the robust counterpart is infeasible. Together with the invariance of under passing to the product of projections, this explains why row-wise (constraint-wise) uncertainty sets are the standard modelling choice in robust linear optimization.
The result is proved in the paper; no machine-checked version is known to exist. Formalizing it produces a reusable development of semi-infinite linear systems: the compactness reduction to finite subsystems, a homogeneous Farkas alternative, and the row-averaging argument that uses convexity and the product structure of .
The robust counterpart has a continuum of constraints, one for each , so Farkas' Lemma cannot be applied to it directly. The step that requires care is passing from infeasibility of this semi-infinite system to infeasibility of a single instance. Compactness yields only finitely many instances whose joint system has no solution in ; those instances are in general all feasible individually, and the infeasible instance has to be manufactured from their rows. Without constraint-wise uncertainty the manufactured matrix need not lie in , which is exactly what the §2.2 example exploits. Part (ii) needs the optimal values of the instances to be attained on compact feasible sets, which is where the Boundedness Assumption enters again.
Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, and is 0 ≤ A *ᵥ x in the componentwise order. The -th row of is A i and is a ⬝ᵥ x. The projections are the images of under , not free sets, and constraint-wise uncertainty is the inclusion (the reverse inclusion always holds). The Boundedness Assumption keeps both convexity and compactness of , as on the page.
Optimal values are infima: is the greatest lower bound (IsGLB) of over , and (9) states that is the least upper bound (IsLUB) of the set of real optimal values of the instances. No real sInf/sSup is used, so no junk value can make the statement true.
The goal carries the paper's standing assumption that is convex and closed, and one disclosed addition: is nonempty. The paper takes this for granted; without it part (i) fails for and the supremum in (9) ranges over the empty set. The goal does not assume that the robust counterpart or any instance attains its optimum, and it does not mention finite subsystems, multipliers or the averaged matrix; those appear only in the milestones. A formalization in which the uncertainty sets are arbitrary sets with , or in which optimal values are taken as sInf without boundedness, would not be faithful and is ruled out.
A complete development needs: compactness arguments for families of closed half-spaces, a Farkas alternative for homogeneous systems with one normalizing equation, and elementary convexity of linear images. These pieces are general and reusable beyond robust optimization. Proofs of the milestones, alternative arguments (for instance via LP duality for part (ii)) and proofs of the companion statements are welcome.
Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets equipped with a rank function, or equivalently a family of independent sets, obeying a few postulates abstracted from the linear dependence of the columns of a matrix. The obvious first question about such an abstraction is whether it is genuinely more general than its model, that is, whether there are matroids that do not arise from any matrix. Section 16 of the paper answers it with a seven-element example, now called the Fano matroid , and proves that no real matrix corresponds to it.
The question has had a long life. Representability of matroids over a given field is a central theme of matroid theory: Tutte (1958) characterized the matroids representable over the field with two elements by a single excluded minor, the four-point line , and the regular matroids by three excluded minors, , and its dual; and Seymour's decomposition of regular matroids (1980) rests on the same objects. Whitney's §16 is the starting point of this line: the first proof that the abstract postulates admit matroids outside linear algebra over .
Timeline:
Let be an matrix with columns . For a set of columns, let be the rank of the submatrix formed by those columns. Regarding the columns as abstract elements gives a matroid on with rank function : the matroid of . A matroid corresponds to if it is the matroid of , with elements matched to columns.
A circuit of a matroid is a minimal dependent set. For a circuit of the matroid of , there are numbers with for every row , and exactly for ; the set of such vectors is written when only the support condition is meant. Stacking one such row per circuit gives the circuit matrix of , determined up to nonzero factors on its rows.
A fundamental set of circuits of a matroid with nullity ( the number of elements) is a family of circuits with such that the elements can be ordered with and for ; it is strict if for every .
The matroid of §16 has elements ; its bases (maximal independent sets) are all three-element sets except
The number of rows is arbitrary; the existence clause makes the non-existence statement non-vacuous.
The result. The theorem separates the abstract notion of matroid from linear dependence over : some matroids are not real-representable. It also exhibits that representability depends on the field, because the same matroid is the matroid of a matrix over the integers mod 2 (milestone 8). Everything later written about representability over particular fields, excluded-minor characterizations, and the gap between abstract and linear matroids starts from this distinction. Theorem 32 is of independent interest: it translates statements about circuits of a represented matroid into the vanishing of minors of a normalised circuit matrix.
Formalizing it. The result is classical and its proof is short on paper, but it is not formalized in Mathlib, which has matroids (Matroid, circuits, ranks) but no column matroid of a matrix with a rank-of-submatrix characterization, no circuit matrix, and no Fano matroid. The mission produces those objects and the bridge lemmas (Theorem 29, Lemmas 10–11, Theorem 32) that connect matroid circuits with linear algebra of the circuit matrix. No machine-checked proof of the non-representability of the Fano matroid over in Lean is known to the curators.
The obvious attempt is a direct search: suppose a real matrix has as its matroid and derive a contradiction from the seven dependent triples. This does not work as stated. Each rank condition is a determinantal (nonlinear) condition on the entries, the number of rows is unbounded, and a representation is determined only up to row operations and column scalings, so there is no finite case check and no single linear computation that settles the question. The contradiction has to come from an argument that is invariant under these symmetries, and the milestones (circuit vectors determined up to scaling, fundamental sets spanning, circuits detected by minors) are what such an argument needs to be stated in. The field also matters: the argument must use that in , since over a field of characteristic 2 the statement is false (milestone 8).
Matroids whose ground set is the whole (finite) type. The Fano matroid lives on Fin 7, Whitney's element being k - 1; the seven triples are written out literally. Matrices are Matrix (Fin m) ι K; "the matroid of " means: ground set everything, and the rank M.eRk N of every finite set of columns equals Matrix.rank of the column submatrix.Fin t with , and determinants are of square submatrices in the paper's row and column order.Reusable beyond this mission: the matroid of a matrix over a field, the circuit matrix, fundamental sets of circuits, and the Fano matroid. Contributions welcome: proofs of the milestones, and a proof of the goal by any route, including one that does not go through Theorem 32.
Whitney's 1935 paper introduced matroids as an abstraction of linear dependence among the columns of a matrix. Most of the paper works over the real numbers; its appendix asks which matroids arise from matrices of integers mod 2, that is, matrices with entries 0 and 1 in which rank and dependence are computed over the two-element field. These are today's binary matroids. They include the cycle matroids of graphs (Whitney closes the paper by noting that graphs correspond to mod-2 matrices with exactly two ones in each column) and they are the setting of several later structure theorems: Tutte's excluded-minor characterization of binary matroids (Tutte 1958), Seymour's decomposition of regular matroids (Seymour 1980) and Seymour's theory of binary clutters and max-flow min-cut (Seymour 1977), which underlies parts of combinatorial optimization.
Whitney's answer is an intrinsic postulate, (C*), on the circuits of the matroid, stated without reference to any matrix, and a constructive representation theorem (Theorem 37): a matroid satisfying (C*) is the matroid of a mod-2 matrix, and the matrix is unique once the columns of one base are fixed.
A matroid on elements is given by its independent sets; its circuits are its minimal dependent sets, its rank is the size of a base, and its nullity is . Here is a Mathlib Matroid (Fin n) whose ground set is all of Fin n.
Subsets of the elements are added mod 2: a sum of finitely many sets is the set of elements lying in an odd number of them (for two sets, the symmetric difference). A cycle is a sum mod 2 of circuits; the empty sum is the null cycle . A set is a true sum of sets that have no common elements and whose union it is. Postulate (C*) requires that each cycle be a true sum of circuits.
With , a family is a strict fundamental set of circuits with respect to if , each is a circuit, and contains but no other .
For a matrix over the integers mod 2 with columns , columns are independent (mod 2) if no non-null subset of them sums to the zero column. The matroid corresponding to has the column indices as elements and these independent sets.
Let satisfy (C*), with elements and base . For every matrix mod 2 (any number of rows) whose columns are independent mod 2,
Milestone 7 and the goal together characterize binary matroids as the matroids satisfying (C*).
The result. Theorem 37 and the p. 532 claim give an intrinsic, matrix-free description of the matroids representable over the two-element field, and Theorem 36 parametrizes all of them by arbitrary subsets of a base. Uniqueness in Theorem 37 says that a binary representation is determined by the columns of one base; in modern terms, binary matroids are uniquely representable over GF(2) up to row operations. Every later theory of binary matroids, including graphic and cographic matroids, Tutte's excluded-minor theorem and Seymour's decomposition, starts from this equivalence.
Formalizing it. The results are proved in the paper and in textbooks (e.g. Oxley, Matroid Theory, Ch. 9) but, at the Mathlib revision used here, there is no notion of a matroid represented by a matrix over a field, and no binary-matroid theory. On Prove2Me, the existing binary objects (SeymourMFMC.Binary.*) are binary clutters defined through blockers, not matroids represented by mod-2 matrices. This mission produces the representation predicate for mod-2 matrices, the cycle space of a matroid, and the equivalence between (C*) and binary representability.
Writing down candidate columns is not the hard part; showing that the matroid of the completed matrix is itself, and not merely a matroid sharing some of its circuits, is. Whitney's example at the end of §9 exhibits two different matroids with a common strict fundamental set, so agreement on fundamental circuits does not by itself identify a matroid; any argument must use (C*) on both the given matroid and the matroid of the matrix. A naive comparison of independent sets column by column does not close this gap. Uniqueness likewise depends on the independence mod 2 of the prescribed columns: without it, different completions can give the same matroid.
Matroid (Fin (r + q)) with ground set Set.univ; Whitney's is k - 1, his is the range of Fin.castAdd q, and is Fin.natAdd r (i - 1). Writing removes natural-number subtraction; is not a free parameter, since is required to be a base.sumMod2); cycles are sums over finite sets of circuits; true sums are unions over finite pairwise-disjoint sets of circuits; (C*) is SatisfiesCStar on the circuit family {C | M.IsCircuit C}. These definitions take the circuit family as a parameter, so that the (C₂) milestone is posed for an arbitrary family of sets, as Whitney poses it.Matrix (Fin m) (Fin n) (ZMod 2) with any ; independence mod 2 of columns is LinearIndepOn (ZMod 2) of the columns (the rows of the transpose). IsMatroidOf M A compares all independent sets, not only bases.Contributions welcome: the general fact that the matroid of a vector family over a field exists (a reusable Matroid.ofFun-style construction over any field), the cycle-space lemmas, and proofs of the milestones in any order.
Many problems in imaging, signal processing and statistics are convex minimizations of the form
where is smooth, and are nonsmooth but have computable proximity operators, and is a bounded linear operator, for example a discrete gradient in total-variation denoising. Primal–dual splitting methods solve such problems using only , the proximity operators of and , and applications of and , without ever inverting or computing the proximity operator of .
Condat's 2013 paper (JOTA 158(2):460–479; final author's version HAL hal-00609728v5) introduced Algorithms 3.1 and 3.2, which handle all three kinds of terms at once, allow relaxation and summable errors, and contain earlier methods as special cases. Together with the closely related work of Vũ (Adv. Comput. Math. 2013), it is the standard reference for the "Condat–Vũ" algorithm.
Timeline. Chambolle and Pock (2011) proved convergence of their primal–dual algorithm, without a smooth term and without relaxation, under (J. Math. Imaging Vis. 40). He and Yuan (2012) interpreted it as a proximal point algorithm in a modified metric (SIAM J. Imaging Sci. 5). Condat (2013) added the smooth term , relaxation and errors (Theorem 3.1), and, for , proved weak convergence for relaxation parameters up to (Theorem 3.2), the result of this mission.
Let and be real Hilbert spaces and a bounded linear operator with adjoint and operator norm . Write for the proper, lower semicontinuous, convex functions . For , the conjugate is , the proximity operator is , and the subdifferential is .
Fix , and . The primal–dual inclusion (6) asks for with
then minimizes and solves the dual problem. The paper assumes this inclusion has a solution.
Given , relaxation parameters and error terms , , Algorithm 3.1 iterates, from any ,
Algorithm 3.2 exchanges the roles: it computes from first, then using .
Suppose and , , and
Then for every run of Algorithm 3.1, and for every run of Algorithm 3.2, there is a solution of (6) with and weakly.
Remark 3.2 (the goal with affine, , instead of ) and Theorem 5.2 (the version with composite terms and condition ).
The result. Theorem 3.2 covers the Chambolle–Pock algorithm with relaxation and summable errors, in arbitrary real Hilbert spaces. Over-relaxation often speeds the method up in practice, and the error terms justify inexact proximity operators. Theorem 5.2 extends it to any finite number of composite terms by full splitting. The convergence statement makes no reference to a Lipschitz constant, so it applies whenever the problem has no smooth part.
Formalizing it. The result is proved on paper; no machine-checked version of Theorem 3.2, of the Krasnosel'skii–Mann lemma with errors, or of the proximal point algorithm under the condition is known to exist. A formal proof would supply reusable pieces of monotone-operator theory in Hilbert spaces: weak convergence of Fejér-type iterations, the change of metric induced by a positive operator, and maximal monotonicity of sums with a skew operator.
The algorithm is not a fixed-point iteration of a nonexpansive map in the original inner product: the coupling between the primal and dual steps breaks nonexpansiveness. The difficulty is to find a metric in which it becomes one, to show this metric is equivalent to the original one (which is where , strictly, is needed), and to transfer maximal monotonicity, zeros and summability of the errors to the new metric. Weak convergence in infinite dimension also requires an Opial-type argument rather than compactness. Mathlib provides inner product spaces, the operator norm and adjoints, but neither maximal monotone operators nor resolvents nor Krasnosel'skii–Mann iteration theory.
The spaces are real Hilbert spaces (InnerProductSpace ℝ and CompleteSpace). Functions valued in are EReal-valued, with the published IsProperClosedConvex. The conjugate is an EReal supremum, so can take the value . Proximity operators enter as maps with the published IsProx property; the subdifferential is the published IsSubgradient. The product with the inner product is WithLp 2 (X × Y). Weak convergence is for all . "" means partial sums tend to , and "" means summability of a nonnegative series.
Standing assumptions are hypotheses: , and (6) has a solution. With the smoothness assumption on is automatic. The paper's assumption that (1) has a minimizer follows from the solvability of (6) and is not stated. The goal is a conjunction over the two algorithms, and the limit is chosen after the run.
The condition is strict, , and relaxation is open, . A goal quantifying over no run, assuming the limit exists, or fixing before the initial point would be a different and weaker statement. Proofs of the milestones, of Theorem 5.2 via the product-space identities (49)–(52), and general results on monotone operators are welcome.
Hassler Whitney's 1935 paper On the Abstract Properties of Linear Dependence introduced matroids: finite sets of elements carrying an abstract rank function that behaves like the rank of a set of vectors. Part II of the paper opens with the decomposition of a matroid into components. The question it answers is basic to every later use of matroids: when does a matroid split into independent pieces, and how can the pieces be recognized?
For the matroid of a graph (elements = edges, rank = number of vertices minus number of connected pieces spanned) the components are the 2-connected blocks of the graph, and Whitney's theorem recovers the classical fact that two edges lie in a common block exactly when they lie on a common cycle. Whitney had studied separability of graphs in Non-separable and planar graphs (1932), and footnote 11 of the 1935 paper points out that the theorem identifies König's "Glieder" of a graph with components. Matroid connectivity built on this notion runs through later structure theory: Tutte's higher connectivity, Seymour's decomposition of regular matroids, and the matroid minors project all start from the separation of a matroid into components.
A matroid on a finite ground set is given here by Mathlib's Matroid structure, with rank function for (Mathlib's M.eRk X) and circuits, the minimal dependent sets (M.IsCircuit). Whitney treats every subset as a matroid in its own right, a submatroid, with the rank function of restricted to subsets of . For sets he writes for the union, for the number of elements of , and
for the nullity of .
Rank is subadditive: . A submatroid is separable if it can be divided into two disjoint groups , each containing at least one element, with
and non-separable otherwise. Every single element is non-separable. A component of is a maximal non-separable part of : a nonempty non-separable set contained in no strictly larger non-separable subset of .
For two distinct elements of ,
Components are defined by the rank function, circuits by dependence; the goal asserts that the two descriptions agree.
The result. Theorem 19 makes the component decomposition computable from circuits alone and shows that "lying on a common circuit" is an equivalence relation on distinct elements, a fact that is not evident from the circuit axioms. Theorem 18 adds that the decomposition is the unique one with additive rank. Together they are the starting point of matroid connectivity: the direct-sum decomposition of a matroid, the reduction of many matroid problems (representability, duality of components, Whitney's own Theorems 24–26 on duals of components) to the connected case, and the higher-connectivity theory that followed.
Formalizing it. The results are classical and proved in the paper; nothing here is open. To our knowledge Mathlib at the pinned revision has no notion of matroid connectivity or components, so this mission produces the first machine-checked development of Whitney's §10: the rank-based definition of separability, the disjoint decomposition into components, the circuit characterization, and the ear-type construction of non-separable matroids (Theorem 17). These are reusable for any later formalization of matroid connectivity, including Whitney's results on duals of components.
The two directions of Theorem 19 rest on different machinery. That two elements on a common circuit lie in one component follows from the rank theory (Theorems 13 and 16). The converse is the substantial direction: a component is defined by the failure of rank additivity, which only says that every division of the component is crossed by some circuit (Lemma 9). It does not directly give one circuit through two prescribed elements. Combining circuits that cross different divisions into a single circuit through both and requires the circuit elimination property together with a minimality argument over subsets of the component; the naive attempt of chaining overlapping circuits from to gives a connected chain of circuits, not one circuit.
Matroid α with [M.Finite]; Whitney's matroids are finite. A submatroid is a subset M.E with the rank M.eRk restricted to its subsets; results that Whitney states for "a matroid " are stated for subsets of an ambient finite matroid, which is the same statement applied to the submatroid .ℕ∞-valued M.eRk, finite on a finite matroid, so (10.1) is an equation of natural numbers. Nullity is computed in as the number of elements minus the rank.IsSeparable M X requires two nonempty, disjoint groups with union and additive rank; without nonemptiness every set would be separable. IsNonSeparable M X adds M.E. IsComponent M K requires nonempty, non-separable, and maximal; nonemptiness excludes the empty set, which is vacuously non-separable.Matroid.IsCircuit.M.eRk and circuit elimination (both in Mathlib), the relation between circuits of M ↾ X and circuits of M inside (Matroid.restrict_isCircuit_iff), and finiteness arguments for maximal non-separable sets. Proofs of the milestones, alternative proofs of the goal, and lemmas relating components to Mathlib's direct sums of matroids are all welcome.Many problems in imaging, signal processing and statistics take the form
where and are convex functions whose proximity operators can be computed cheaply, is a linear operator such as a finite-difference gradient, and is smooth. Total-variation denoising, the lasso with a structured penalty, and constrained least squares are of this type. Because is generally not proximable even when is, practical methods split the problem so that each step uses only , , and , without inverting any operator.
L. Condat (J. Optim. Theory Appl. 158 (2013)) introduced a relaxed, inexact primal–dual iteration of this kind; B. C. Vũ (Adv. Comput. Math. 38 (2013)) studied the same structure for monotone inclusions. With the iteration is exactly the method of Chambolle and Pock (J. Math. Imaging Vis. 40 (2011)). They proved convergence in finite dimension assuming , and no errors. He and Yuan (SIAM J. Imaging Sci. 5 (2012)) extended this to a constant relaxation under the same other hypotheses (Condat, §3.1.1). Condat's paper proves three convergence theorems. This mission is the third: in finite dimension and with , the iterates converge under the step-size condition , equality included. Equality matters in practice: one can set and tune a single parameter, as in the Douglas–Rachford method.
Let and be real Hilbert spaces and a bounded linear operator with adjoint and operator norm . Write for the proper, lower semicontinuous, convex functions , and let , . The Fenchel conjugate is , the proximity operator is , and the subdifferential is .
The primal–dual inclusion (6) asks for with
A solution gives a minimiser of the primal problem and a solution of its dual.
Algorithm 3.1 chooses , , relaxation parameters , error terms and an initial estimate , then iterates
Algorithm 3.2 swaps the roles of the primal and dual variables: the dual step comes first, and the primal step uses . Section 5 extends both to (Algorithms 5.1 and 5.2), with the inclusion (48) in place of (6).
Let , be finite-dimensional, , , and assume (6) has a solution. If
then for every run of Algorithm 3.1, and for every run of Algorithm 3.2, converges to a solution of (6).
With the operator (20) and the error-free step of Algorithm 3.1:
Remark 3.2 (Theorem 3.3 with affine, i.e. in (2)) and Theorem 5.3 (the analogue for composite terms, with (i) replaced by ) are included as draft theorems.
Theorem 3.3 is the convergence guarantee behind the common practice of running the Chambolle–Pock iteration and its relaxed variants at the critical step size . It covers relaxation parameters up to and summable errors in both proximity operators. It applies directly to the discrete models of imaging and statistics, which are finite-dimensional. Theorem 5.3 extends it to any finite number of composite terms in parallel.
None of the statements of this paper is formalized on the platform. Machine-checked convergence proofs for primal–dual splitting are not available in Mathlib. The mission would produce the first ones, together with two standalone tools of general use: the inexact Krasnosel'skii–Mann theorem (Lemma 4.1), and Polyak's recursive-inequality lemma (Lemma 4.6), which is a standard tool for stochastic and inexact iterations.
The usual proof treats the iteration as a proximal-point or forward–backward step in the space with the inner product . That argument needs strictly positive, which is exactly what fails when : then has a nontrivial kernel, is only a seminorm, and weak convergence in the -geometry says nothing about the components of in . The proof replaces the iteration by its "shadow" on , uses that factors through , and recovers the full iterates through continuity of and a recursive inequality. The last step requires strong convergence of the shadow sequence, which is where finite dimension enters. Infinite-dimensional versions require different arguments and are not claimed here.
Spaces are real inner product spaces with CompleteSpace; the goal and Theorem 5.3 add FiniteDimensional. Functions in take values in EReal and satisfy the published predicate IsProperClosedConvex (never , finite somewhere, lower semicontinuous, convex epigraph). The conjugate is an EReal supremum. Proximity operators are maps , satisfying the published minimisation predicate IsProx for and ; such maps exist and are unique for functions. The subdifferential is the published IsSubgradient. Runs of the algorithms are predicates on pairs of sequences with arbitrary initial point, and the limit is chosen after the run. "" for a series is divergence of its partial sums, "" is summability of a nonnegative series, and convergence in the goal is norm convergence.
The standing assumptions of pp. 3–4 are hypotheses: , and (6) has a solution. The paper's other standing assumption, that problem (1) has a minimiser, follows from the second and is omitted. In the milestones, the operators and are plain maps on . The projector is not built: "" is stated as "", which is equivalent because is self-adjoint. Each milestone drops finite dimension, so it is stated at least as strongly as on the page.
The strict inequality would make the goal a corollary of the weaker Theorem 3.2 with an extra finite-dimensional upgrade. The goal keeps . Weak convergence in place of norm convergence, an chosen after , or a solution of (6) fixed before the run would each weaken the theorem, and all are excluded.
Useful infrastructure includes: firm nonexpansiveness of for EReal-valued functions; -ness of the conjugate and Moreau's identity; maximal monotonicity of plus a skew operator; and the inexact Krasnosel'skii–Mann theorem. All of it can be reused for Theorems 3.1 and 3.2 of the same paper, and for Douglas–Rachford and three-operator splitting. Proofs of individual milestones are welcome independently of the goal.
A graph is perfect if every induced subgraph has chromatic number equal to its clique number. Perfect graphs are the graphs for which colouring and clique problems behave as linear programs do: the stable-set polytope of a perfect graph is described by its clique inequalities, so maximum weight stable sets and minimum colourings can be computed in polynomial time (Grötschel, Lovász & Schrijver 1988). In 1961 Berge conjectured that a graph is perfect exactly when it has no odd hole and no odd antihole. Chudnovsky, Robertson, Seymour and Thomas proved this, the strong perfect graph theorem, in Ann. of Math. 164 (2006).
The proof is a decomposition theorem: every Berge graph is basic or admits one of a few decompositions. The paper reaches it through twelve steps, 1.8.1–1.8.12 (p. 59), each handling graphs that contain a certain configuration. This mission poses step 1.8.3, Theorem 9.6. It handles Berge graphs that contain the line graph of a bipartite subdivision of , all such line graphs being degenerate.
All graphs are finite and simple. denotes the complement of . A hole is an induced cycle of length at least , an antihole is a hole of , and is Berge if all its holes and antiholes have even length. A path is always an induced path, and an antipath is a path of . The length of either is its number of edges.
Line graphs and appearances. The line graph has vertex set , two edges adjacent when they share an end. is a subdivision of if it arises from by replacing every edge by a track (a path, not necessarily induced), these tracks disjoint except for their ends. appears in if, for some bipartite subdivision of , is isomorphic to an induced subgraph of ; is then an appearance of . For the appearance is degenerate if some 4-cycle of contains the four vertices of degree three. A -enlargement is a 3-connected graph with a proper subgraph isomorphic to a subdivision of . An appearance is overshadowed if some branch of of odd length , with ends , has a vertex of nonadjacent to at most one edge at and at most one edge at .
Knots and striations. A knot is formed by two paths with ends and two antipaths with ends . They are pairwise disjoint and of length , is anticomplete to , is complete to , and the ends are joined in a prescribed twisted pattern (pp. 107–108). A degenerate appearance of is a knot. A strip is a family of paths ("rungs") from to through ; an antistrip is a strip of . A striation is made of strips and antistrips. All rungs and antirungs are odd, the strips are pairwise anticomplete, the antistrips pairwise complete, and every strip is parallel or co-parallel to every antistrip, with enough "twists" between them (p. 112). A striation is maximal if no striation has a strictly larger vertex set. The paper defines when a set of vertices is local for a knot or striation and when it resolves one.
Outcomes. A double split graph has its vertices partitioned into () and (). Each is an edge and each a nonedge, distinct pairs are anticomplete and distinct pairs complete to each other, and every and are joined by exactly two disjoint edges. A skew partition of has disconnected and disconnected. It is balanced if no odd path joins nonadjacent vertices of through and no odd antipath joins adjacent vertices of through . A proper 2-join is a partition of whose only cross edges are complete joins – and –, with the side conditions of p. 53.
Let be Berge, with every appearance of in and in degenerate and no induced subgraph of isomorphic to . Then
9.3–9.5 assume that no -enlargement appears in or and that no appearance of in or is overshadowed. An optional, non-milestone item poses 9.7 (p. 118): a Berge graph with an appearance of is a line graph or the complement of one, a double split graph, or admits a proper 2-join (in or ) or a balanced skew partition.
9.6 is the step of the proof that produces double split graphs, one of the five basic classes. In the main argument it follows step 1.8.1 (5.1, nondegenerate appearances of ) and is combined with it in 9.7. Through 9.7 it gives the first half of 13.5: every recalcitrant graph belongs to the class and so contains no appearance of in or .
The theorem has been proved since 2006. We know of no machine-checked proof of the strong perfect graph theorem or of any of its steps. Mathlib has line graphs and graph embeddings but no subdivisions, appearances or decompositions of Berge graphs. This mission produces a faithful Lean statement of step 1.8.3 and of the four lemmas its proof rests on, together with Lean definitions of knots, strips and striations.
The obvious approach would take a degenerate appearance of and study how each remaining vertex attaches to it, as §§5–6 do for nondegenerate appearances. This does not close. A degenerate appearance can be read as a line graph or as its complement, so the analysis of a vertex in and in has to be run at once. Single vertices can also be absorbed into larger structures that the line-graph analysis does not see. The proof grows the appearance to a maximal striation and classifies attachments to it, and the hard steps are 9.4 and 9.5. Their proofs need 9.3 in every case, and they use maximality to refute configurations that would let the striation grow.
Graphs are SimpleGraph V on a Fintype with decidable equality. Every object is defined as on the page, in the namespace StrongPerfectGraph.DoubleSplit.
SimpleGraph.lineGraph; "isomorphic to an induced subgraph" is an induced embedding ↪g. Subdivisions and enlargements range over graphs on Fin k.Fin m, Fin n.Dropping the bars of the complement would make the theorem false or vacuous. So would reading "path" as a non-induced path, or encoding a decomposition so that it always exists. The statements use the complement explicitly, induced paths throughout, and the full definitions of p. 53–54.
The proof of 9.6 also uses results of the same paper that are posed in other missions of this series. These are 2.1, 2.2, 4.1 and 4.2, posed in mission II (skew partitions), and 5.3, 5.8, 6.1 and 7.5, posed in mission III (line graphs). They are not posed again here. The bridge 9.2 between knots and line graphs, whose proof the paper omits as obvious, is not posed either. Proofs of 9.1, of 9.3, and reusable lemmas about knots and striations are welcome.
In 1935 Hassler Whitney asked which properties of linear dependence among the columns of a matrix can be stated without reference to the matrix at all. His answer, On the Abstract Properties of Linear Dependence (American Journal of Mathematics 57, 1935), introduced the matroid: a finite set together with a rank function obeying three short postulates. The notion now underlies combinatorial optimization (the greedy algorithm is optimal exactly on matroids, and matroid intersection and partition generalize bipartite matching and arborescence packing), graph theory (graphic and cographic matroids), coding theory and the study of linear representations over finite fields.
A defining feature of the subject is that the same structure can be axiomatized in several apparently unrelated ways: by rank, by independent sets, by bases, by circuits. Each axiom system is convenient for different arguments, and passing between them, a so-called cryptomorphism, is routine in practice. Whitney's paper is where these equivalences first appear. Part I, §§2–4 and §6 (pp. 510–514), derives the basic properties of rank from the rank postulates, deduces from them the postulates for independent sets, and shows that the two systems are equivalent. This mission formalizes that first equivalence.
Let be a finite set of elements . Following Whitney, write for , for the union and for the intersection of subsets; is the number of elements of .
A rank system is a function on the subsets of satisfying
The nullity of is , and is independent when . The increment of (3.1) is , written when .
An independence system is a predicate "independent" on the subsets of satisfying
From an independence system one recovers a rank by letting be the number of elements in a largest independent subset of . In the Lean development these objects are IsRankSystem, nullity, Delta, indepOfRank, IsIndepSystem and rankOfIndep, all in the namespace WhitneyMatroid.RankIndep.
Both translations and both round trips are part of the goal: Whitney's conclusion is not only that each system implies the other but that "the definitions of the rank and the independence or dependence of any subset of agree under the two systems".
The equivalence makes the rank function and the family of independent sets two descriptions of one object. Every later result of Whitney's paper, and of matroid theory generally, moves between them without comment: the circuit postulates of §5 and §8, the base postulates of §7 and the duality of §§11–13 are all phrased through rank or independence as convenient. Theorem 3 is the submodularity of rank, the property that connects matroids to submodular function minimization and polymatroids; here it is derived from the purely local postulates (R₁)–(R₃), which constrain the rank only under the addition of one or two elements.
On the formal side, Mathlib defines Matroid through independent sets (with constructors from other axiom systems) and proves submodularity of its rank; the platform has submodularity for Mathlib matroids (FamousTheorems.matroid_rank_submodular_7a). Neither starts from Whitney's local rank postulates. What this mission adds is a machine-checked derivation of the global properties of rank from (R₁)–(R₃) and of Whitney's original equivalence, stated for his own postulates, so that the later missions of this series, which work from the same postulates, rest on a verified foundation. The result itself has been settled since 1935; the open work is the formal proof.
The postulates (R₂) and (R₃) are local: they speak about adding at most two elements to a set. Monotonicity and the bound follow by adding elements one at a time, but the submodular inequality relates arbitrary sets, and nothing in (R₃) mentions more than two new elements. The gap between the local and the global statement is the substance of Lemmas 3, 4 and Theorem 3, and the deduction of (I₂) depends on it.
In the converse direction the rank is defined as a maximum over independent subsets, while (I₂) only augments a set from an independent set with exactly one element more; (R₃) for the derived rank is a statement about three sets that are not given in that form. The round trips are where the two halves meet, and each depends on the global properties of the first half rather than on the postulates alone.
Elements form a type α with [Fintype α] [DecidableEq α]; subsets are Finset α, and the matroid is the whole type. Ranks, nullities and increments take values in ℤ, so differences never truncate; Whitney allows any number, but (R₁) and (R₂) force nonnegative integers. Postulate (I₂) is stated in Whitney's form with N'.card = N.card + 1, not the general augmentation for . Postulates (R₂), (R₃) keep their hypotheses . Lemmas 3, 4 and Theorem 3 are stated for arbitrary subsets ; Lemma 1's monotonicity for arbitrary , the form in which the paper uses it. rankOfIndep is the supremum of cardinalities over the independent members of the powerset.
The paper takes for granted that the empty set is independent in system (I). Without that hypothesis, the predicate declaring nothing independent satisfies (I₁) and (I₂) vacuously, the supremum defining the rank returns , and the round trip fails; the goal therefore assumes independent in part 2 and proves it in part 1. A formalization in terms of Mathlib's Matroid would make the goal a restatement of library facts, since Mathlib's matroids are independence systems by construction; the goal is deliberately about the postulates as predicates on functions and on families of sets.
A complete development needs only finite set combinatorics (Finset.card, induction on finite sets, Finset.sup). The derived lemmas (monotonicity, submodularity, (I₂)) are reusable for any later work from Whitney's rank postulates, including the circuit-postulate equivalence of the companion mission. A bridge from rank systems to Mathlib's Matroid (via IndepMatroid.ofFinset) would be a welcome addition but is not part of the goal. Proofs of the milestones in any order are welcome; Theorem 3 and the §4 deduction are the natural first targets.
Mathlib.Data.Matroid (matroids via independent sets; IndepMatroid.ofFinset). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matroid/Basic.htmlMany convex optimization models combine a smooth loss, a nonsmooth penalty whose proximity operator is easy to compute, and a second penalty applied after a linear map. Imaging models, for example, often place a data-fitting term on the image and a regularizer on its transformed coefficients. The resulting objective has the form . Condat's primal–dual method evaluates the smooth gradient and two proximity operators separately, without requiring a proximity operator for the composite . Condat, 2013 establishes weak convergence with relaxation and summably weighted computational errors. This mission targets its main positive-smoothness theorem, Theorem 3.1, in the final author's version.
The theorem matters when a computed gradient or proximal point is inexact, as is common when a proximal subproblem is itself solved numerically. Its conditions account for these errors directly rather than treating the displayed algorithm as exact. It also gives one parameter regime for two orders of updating the primal and dual variables. These two algorithms share an objective and a solution inclusion, but have distinct recursions.
Let and be real Hilbert spaces and let be bounded linear, with adjoint . The smooth term is convex and differentiable. Its gradient is -Lipschitz when for all . The nonsmooth terms and are proper, lower semicontinuous, convex functions with values in . Such functions form the class . An infinite value may encode a constraint.
For a convex function , its proximity operator minimizes over , where . The Fenchel conjugate is . A subgradient obeys for every . The sought primal–dual solution satisfies
Algorithms 3.1 and 3.2 maintain sequences and . Algorithm 3.1 updates the primal proximity step before the dual one; Algorithm 3.2 reverses that order. Each uses positive step sizes , positive relaxation weights , and errors , and in the gradient and the two proximal evaluations. Their full recursions are part of the Lean setting, so a run is determined by its initial pair. The paper specifies the problem in §2 and both algorithms in §3.
The goal is Theorem 3.1 on p. 5. Suppose , the primal–dual solution set is nonempty, and . Set
For , the theorem assumes
Under these conditions, both sequences of each algorithm converge weakly to the components of a primal–dual solution. The solution may depend on the initial pair and on the run. The milestone list includes Lemmas 4.1 and 4.3–4.5, the strict positivity claim for the block operator , estimate (29), and the error-free optimality inclusions (22) and (44), ordered as preliminary results followed by the two algorithm-specific claims. These targets match the results stated in §4 of the source version.
The result supplies a convergence guarantee for a composite objective under an explicit coupling condition on , , and . It permits relaxation weights that vary with and errors that are summable only after weighting by those same relaxation values. The dual conclusion is substantive: convergence of the primal sequence alone would not give convergence of the dual certificate produced by the algorithm. The weak topology is appropriate in general Hilbert spaces; norm convergence would assert more than the paper proves.
The theorem is proved in the 2013 paper. The present formalization task is to give its statement and the selected operator lemmas machine-checked proofs in Lean. Related platform definitions for proximal maps, monotone operators, nonexpansive maps, subgradients and weak convergence already exist; the paper-specific convergence theorem and its selected milestones are new targets in this proposal. The resulting definitions and abstract Lemmas 4.1, 4.3–4.5 can be reused in later operator-splitting developments.
The displayed recursions involve three errors, two proximal evaluations, a linear map and its adjoint, and two different update orders. A direct estimate on does not by itself control the coupled dual variable, while a bound on only the combined objective value would not establish weak convergence of either iterate. The relaxation condition permits weights without a fixed positive lower bound, so a convergence argument cannot replace the stated divergent series by a simpler constant-step assumption. The abstract lemmas must also retain the endpoints and present in the source.
Lean uses complete real inner-product spaces for and , a continuous linear map for , and EReal for , and their conjugates. The conjugate supremum is taken in EReal. The paper's class and proximity maps use published definitions; the latter are parameters constrained to be the actual proximal minimizers. Positive step sizes and proper closed convex data ensure such maps exist and are unique. The subgradient predicate explicitly requires a finite value at the base point; this follows from the source's properness assumptions when a subgradient exists.
Both algorithms are represented by recursion predicates on every natural-number index, with all error terms present. The goal quantifies over every run and chooses its weak limit afterwards. Divergence to means finite partial sums tend to atTop; a finite weighted error sum means the corresponding nonnegative real sequence is summable. These choices prevent a default value of an infinite sum from satisfying the hypotheses. The nonempty solution set is an explicit standing assumption from p. 4 and implies the earlier nonempty-primal-minimizer assumption. A condition that made all runs impossible, or one that discarded either the primal or dual conclusion, would not represent Theorem 3.1.
The block operator is represented through its quadratic form ; is recorded for Algorithm 3.2. The complete development will need the abstract iteration lemmas, proximal optimality conditions, block-metric estimates, and the links from each algorithm's inclusion to the solution set. Contributions proving those results, or building reusable Hilbert-space operator infrastructure needed by them, are in scope. The several-composite-functions extension in Theorem 5.1 is reserved for separate work.
The conditional logit model assigns to an alternative in a finite choice set the probability , where is a "representative utility" built from observed attributes of the alternative and the decision maker. It is the workhorse of discrete choice econometrics, transportation demand forecasting, marketing and revenue management, where it underlies multinomial logit assortment and pricing models. Its appeal for applied work is computational; its appeal for economics is that it can be read as the aggregate behaviour of a population of utility maximizers. This mission formalizes the result that makes that reading exact: Lemmas 1 and 2 of D. McFadden, Conditional logit analysis of qualitative choice behavior (1974), which show that, under a mild regularity condition, logit choice probabilities arise from random utility maximization exactly when the idiosyncratic taste shocks follow the extreme value (Gumbel) distribution.
Timeline:
An individual faces alternatives with representative utilities . The utility of alternative is , where the taste shocks are independent and identically distributed with a common law on and distribution function . The individual chooses the alternative of highest utility, so the selection probability of is (Equation (2) of the paper)
computed under the product law of the shocks. The logit formula (Equation (12)) is . The extreme value law (Equation (13)) is .
A law is translation complete if for every function of bounded total variation on with , the condition for every real forces outside a Lebesgue-null set. Laws whose characteristic function never vanishes, the extreme value law among them, are translation complete (footnote 5 of the paper).
In Lean the law is μ : Measure ℝ with [IsProbabilityMeasure μ], is ProbabilityTheory.cdf μ, the selection probability is selProb μ V i for V : Fin J → ℝ, and the logit formula is logitProb V i.
Fix a universe of alternatives with a representative utility map onto the real line. For a translation complete law normalized by ,
The normalization only fixes the location of the shocks: without it the conclusion is the one-parameter family of Lemma 2 below.
The result separates two readings of the logit formula. Lemma 1 shows that it is consistent with utility maximization; Lemma 2 shows that, within the class of i.i.d. additive random utility models with translation complete shocks, the extreme value law is the only one consistent with it. Consequences drawn from the random utility reading, such as the log-sum formula for expected maximum utility used in welfare analysis, therefore apply to logit models without further distributional assumptions inside that class. The same reading supports the interpretation of multinomial logit demand in assortment optimization and revenue management.
Both lemmas are proved in the paper and in later textbooks; neither is open. As far as a search of the Prove2Me catalog shows, neither has a machine-checked proof. The mission provides Lean statements of the random utility model with i.i.d. shocks, of translation completeness and of the extreme value law that later discrete choice formalizations can reuse.
Lemma 1 is a computation with the extreme value density; its formal cost lies in passing from the product-measure probability (2) to the iterated integral (3) and evaluating an improper integral. Lemma 2 is harder. The natural first idea is to differentiate the logit identity in the utilities and solve a differential equation for ; this requires a density, which Lemma 2 does not assume. Without a density, the only handle on is the logit identity itself, an equality of integrals against that holds for every utility vector; turning such integral identities into pointwise information about is where the hypothesis of translation completeness enters, and it yields statements only outside a Lebesgue-null set, so one-sided continuity of distribution functions is needed to recover identities at every point. A second subtlety is that the paper's (14) is written with while the event (2) is strict, so with a general law the integrals involve left limits of .
Alternatives are indexed by Fin J; the model is indexed by the utility vector, so the individual attributes and alternative attributes enter only through . The shocks have joint law Measure.pi (fun _ => μ), which is what "independently identically distributed" means; a general joint law is not allowed. The event in (2) uses strict inequalities, and the selection probability is defined for every law, with no density. Translation completeness quantifies over BoundedVariationOn h Set.univ with limits at both ends; such are bounded and measurable, so the integrals are genuine, and "measure zero" is Lebesgue measure.
Lemma 2's hypothesis is stated on every finite subset of the paper's alternative universe, with a surjective utility map. Distinct alternatives may have the same utility. The printed proof uses equal-utility alternatives, which surjectivity alone need not supply; proving the stated theorem requires an additional continuity argument. A trivializing formalization is ruled out: the selection probability is a genuine product-measure probability, and the hypotheses of the goal are met by the extreme value law, which is translation complete with .
A complete development needs: Fubini for Measure.pi over Fin J split at one coordinate; the Gumbel density and the improper integral ; the facts that bounded-variation functions are bounded and measurable and that distribution functions are right-continuous with left limits. The integral representation (milestone 1) and the Gumbel computations are reusable in any random utility formalization. Proofs of the milestones, of the footnote-5 fact that the extreme value law is translation complete, and alternative proofs of Lemma 2 are welcome.
A perfect graph is a finite simple graph in which every induced subgraph has chromatic number equal to its largest clique size. This equality gives a structural reason that a clique lower bound on the number of colours is attainable for every induced part of the graph. Berge proposed a forbidden-subgraph description of perfect graphs: a graph should be perfect exactly when it has neither an odd hole nor an odd antihole. Chudnovsky, Robertson, Seymour and Thomas proved that statement in The strong perfect graph theorem, Annals of Mathematics 164 (2006), Theorem 1.2. Their proof separates possible configurations in a Berge graph and shows that each either belongs to a controlled class or admits a decomposition.
This mission isolates the even-prism step, Theorem 10.6 of that paper. A prism is one of the configurations that can appear in a Berge graph even though odd holes and antiholes do not. The step matters because its conclusion leaves only a specific nine-vertex graph or one of two decompositions that the larger proof handles elsewhere. It is the result identified as step 1.8.4 in the authors’ outline (paper, pp. 59 and 124).
All graphs here are finite and simple. A path means an induced path; a single vertex is allowed as a path of length zero. A hole is an induced cycle with at least four vertices, and an antihole is a hole in the complementary graph. A graph is Berge if every hole of and of its complement has even length.
A prism has two disjoint triangles, and , joined by three pairwise vertex-disjoint induced paths from to . Between distinct paths, the only edges are those in and those in . The prism is even when all three have even length. “ contains an even prism” means that such paths exist as an induced configuration in ; may have other vertices. “ is an even prism” means the paths cover every vertex of (paper, pp. 93 and 119).
An appearance of is an induced copy in of the line graph of a bipartite subdivision of the four-vertex complete graph. It is nondegenerate if no four-cycle of contains all four branch vertices. Only appearances in are excluded in this mission; appearances in are allowed by the hypotheses (paper, pp. 72, 74–75).
A proper 2-join partitions the vertices into two sides with specified, nonempty attachment sets. The cross edges are exactly the two complete attachment pairs; every component of either side meets both of its attachment sets. If a side is itself a path between singleton attachment sets, that path has odd length at least three. A balanced skew partition divides the vertices into and so that is disconnected, is disconnected in the complement, and two path parity conditions hold: no odd path crosses between nonadjacent vertices of , and no odd antipath crosses between adjacent vertices of (paper, pp. 53–54).
The numbered milestones are Theorems 7.2–7.4 and 10.5. They assert common parity of the three prism paths, common neighbours of an anticonnected set at both end triangles, preservation of two neighbours under replacement of one even prism path, and the balanced skew partition forced by a major vertex. A vertex is major when it is adjacent to at least two vertices of each end triangle. These milestones match the paper’s statements on pp. 93 and 123 (paper).
For a Berge graph with no nondegenerate appearance of in ,
The first case describes the entire graph, not just an induced nine-vertex subgraph. The statement fixes all outcomes exactly as in Theorem 10.6, p. 124.
Theorem 10.6 removes even prisms from the unresolved part of the strong perfect graph theorem’s structural argument. If the graph is larger than the exceptional prism and has no nondegenerate appearance, the theorem supplies a proper 2-join or a balanced skew partition. Subsequent results can work with those decompositions instead of treating arbitrary attachments to a prism (paper, §10 and the outline at 1.8.4).
The mathematical result is proved in the 2006 paper. The work here is to give its graph objects and statements machine-checkable meanings, then formalize the known proof. This proposal contains open Lean theorem statements and sorry-free definitions; the proof obligations remain for solvers. The definitions of induced paths, holes, subdivisions, and decomposition predicates can also support other steps of this paper. The Roussel–Rubio lemma and the balanced-skew-partition results of §§2–4 are proved in the same paper and posed in mission II of this series. The prism-attachment result 10.4 is posed in mission VI, where it is used most directly.
An outside connected set can attach to several parts of a prism without containing a single major vertex. Its attachments need not be local to one path or one triangle, so checking vertices one at a time does not decide which decomposition exists. The paper’s §10 distinguishes several attachment patterns; the evenness of the paths and the exclusion of a nondegenerate appearance restrict them, but do not themselves give a 2-join or skew partition by a one-line parity argument. The larger proof must also account for attachments throughout the graph while preserving the full definitions of both decomposition outcomes (paper, pp. 119–127).
Lean represents a graph as SimpleGraph V with a finite vertex type. The prism is three lists of vertices, each an induced path; the lists are disjoint, and the cross-edge condition admits exactly the two end triangles. Reversing a list changes its orientation but not the underlying graph configuration. A hole uses a cyclic list with the closing edge; Berge checks holes in both and . Connectivity is reachability in an induced graph, so the empty vertex set is connected as the paper says. A subdivision uses six tracks on a finite carrier, with all its vertices and edges accounted for; the appearance uses an induced graph embedding of its line graph. The exception checks that the prism covers the whole graph and that .
These encodings require genuinely induced paths and the paper’s nondegenerate appearance condition. Dropping either would change the theorem. The proper 2-join includes component reachability and the odd-path special case; the balanced skew partition includes both path parity clauses. The nine-vertex graph formed by two triangles and three two-edge paths has a separate sorry-free Lean witness, so the exceptional outcome is nonvacuous. Useful contributions include the numbered prism lemmas, attachment analysis for 10.6, and reusable results about finite induced paths and graph subdivisions.
Linear programming, with , is the basic model of operations research, and the complexity of solving it is a central question of algorithm theory. Interior-point methods follow the central path: primal–dual pairs with and for every , as the path parameter decreases to . A classical short-step method needs iterations, each solving a linear system with the matrix , for a total of roughly operations or more.
Cohen, Lee and Song (J. ACM 68(1), 2021; arXiv:1810.07896) showed that linear programs can be solved in time (for the current values of the matrix multiplication exponent and its dual ), matching the cost of multiplying two matrices. The analysis has two halves: a data structure that maintains the projection matrix lazily, and the stochastic central path method, which replaces each Newton step by a sparse random step and proves that the iterates still stay close to the central path. This mission formalizes the second half.
Timeline: Karmarkar's projective method (1984) gave the first polynomial interior-point method; Renegar (1988) gave the path-following bound; Vaidya (1989) reduced the per-iteration cost with low-rank updates; Lee and Sidford (2014–2015) reduced the iteration count to ; Cohen, Lee and Song (STOC 2019, J. ACM 2021) reached ; van den Brand (2020) derandomized the result.
Vectors are in and products, quotients and roots of vectors are coordinatewise. For and vectors , means for all ; for a scalar is defined likewise. The number of variables is and has full row rank .
The potential is , evaluated at with ; it is small exactly when every is close to .
StochasticStep (Algorithm 1) takes positive , a direction , a sampling parameter and the output of a data structure with . It rescales to , (), draws a sparse vector with independent coordinates, with probability and otherwise, and computes the step through the projection . The draw is repeated until and are at most ; the output is .
Main (Algorithm 2) sets , , , , starts at , and in each iteration sets , takes the direction
runs StochasticStep, and falls back to a deterministic ClassicalStep whenever .
For every iteration , almost surely Assumption 4.1 holds for the input of iteration (in particular and ), almost surely the resampling loop of iteration succeeds with positive probability, and
The paper writes ; its proof gives the constant .
Lemma A.1 (variance of a product), Lemma 4.12 (properties of ), Lemma 4.2 (explicit step), Lemma 4.3 and Claim 4.7 (moments and success probability of the sampled step), Lemma 4.8 (moments of ), and Lemma 4.13:
Lemma 4.14 is what makes the randomized method usable: the iterates stay in the -neighbourhood of the central path along the whole run, and the expensive fallback is rare enough that its expected cost, , is negligible. The paper's cost bound (Lemma 4.16) and its main theorem rest on it. The same potential-based "stochastic central path" analysis was reused in later solvers, for instance for empirical risk minimization (Lee, Song and Zhang, COLT 2019).
The result is proved in the paper; no machine-checked version exists. A formalization pins down the probabilistic model that the paper leaves implicit (independence of the sampled coordinates, the law of the resampling loop, a data structure and fallback that see only the past) and checks the constants, several of which are tight against printed slack (Remark 4.4).
The running-time claims of the paper (Theorem 2.1's expected time , Lemma 4.16, Section 5) are not part of this mission: they live in an arithmetic cost model that Lean does not have. The accuracy guarantee of Theorem 2.1 (Lemma A.6, ClassicalStep from [57]) is also outside the mission.
The obvious argument would bound each quantity under the product law of the sparse direction. But StochasticStep resamples, so the step actually taken is distributed according to that law conditioned on a success event, and expectations and variances shift. A second difficulty is that is controlled only in expectation, while Assumption 4.1 must hold surely at every iteration; this is reconciled by the deterministic ClassicalStep fallback, which caps at , and by an induction over iterations of under the trajectory law. Claim 4.7 needs a Bernstein inequality, which Mathlib does not yet provide.
Coordinates are Fin n, vectors Fin n → ℝ, a Matrix (Fin d) (Fin n) ℝ with A.rank = d, and the natural logarithm. is written out as ; is stated coordinatewise. The sampled direction has law Measure.pi of two-point laws; the step taken by StochasticStep has that law conditioned (ProbabilityTheory.cond) on the success event, and every , of Lemmas 4.3, 4.8 and 4.13 is under this conditioned law. mp.Query is replaced by its value ; the data structure and ClassicalStep are arbitrary measurable functions , of the history with the only properties the paper uses. The trajectory is Mathlib's Ionescu-Tulcea measure, with kernels equal to the step law of Main. is the number of variables of the program the loop runs on.
Deviations from the page, all recorded in the items: Assumption 4.1 is used with instead of the printed , because Main sets to exactly that value; is instantiated as , the constant of the paper's proof; the conclusions of Lemma 4.14 are stated for every iteration index rather than while ; at the second term of is . No hypothesis is imposed.
A trivializing formalization is ruled out: every statement that integrates against the conditioned law also concludes that this law is a probability measure (so it cannot be the zero measure), the goal concludes that each resampling loop succeeds with positive probability, the oracles , cannot see the coins of the current iteration, and the goal is about the whole iterated process from the initial point, not one step from an arbitrary law.
Contributions welcome: a Bernstein inequality for bounded independent sums, conditional-law lemmas for cond of Measure.pi, and Markov-kernel measurability for the step law; these are reusable beyond this mission.
The neutral theory of molecular evolution holds that much of the genetic variation observed at the molecular level is caused by selectively neutral mutations rather than by selection. To test it against data one needs the distribution of allele frequencies that a neutral model predicts, and in practice that distribution has to be compared with a sample from the population, never with the whole population. Ewens (Ewens 1972) derived the equilibrium distribution of allele counts under the infinite alleles model, now called the Ewens sampling formula; it underlies classical tests of neutrality and appears throughout combinatorics and probability as the law of the cycle type of an Ewens-distributed random permutation and of the Chinese restaurant process.
Chapter 7 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979) obtains the infinite alleles model as a limit of the reversible migration processes of Chapters 2 and 6, and uses reversibility to answer questions about allele ages and fixation. The mission formalizes the finite, combinatorial results of that chapter.
Timeline. Kimura and Crow (1964) introduced the infinite alleles model. Ewens (1972) found its equilibrium sampling distribution (7.6). Kingman (1978, J. London Math. Soc.) characterized the consistency of random partitions under sampling, the property Theorem 7.1 asserts for the Ewens family. Kelly (1979, Chapter 7) derived (7.6) as a limit of reversible migration processes, and the consistency and the allele-age results from the reversibility of a labelled population process.
A population consists of individuals, each carrying an allelic type. Its description is , where is the number of allelic types carried by exactly individuals, so that
For a real parameter , the Ewens distribution on descriptions is
where is the binomial coefficient for real . In the infinite alleles model, individuals die at rate , each death is followed by the birth of an offspring of a uniformly chosen survivor, and the offspring is a mutant of an entirely new type with probability ; then (7.6) is the equilibrium distribution with (7.5).
A random sample of size without replacement is a uniformly random -element subset of the labelled individuals, each of the subsets being equally likely; the sample has a description in the same sense.
The number of individuals carrying one given allele performs a random walk on with intensities
An allele is quasi-fixed when it is the only allele present ().
If and the population description is distributed as , then a random sample of size drawn without replacement has description with probability , the same being used for both sizes:
The results. Consistency under sampling is what makes the Ewens formula usable as a statistical model: the predicted distribution for an observed sample does not depend on the unknown population size, only on . Kelly deduces from it the sufficiency of the number of alleles in a sample for and the heterozygosity (Exercises 7.1.5, 7.1.8). The formula (7.9) gives the equilibrium frequency of the oldest allele, and Theorem 7.9 gives the quasi-fixation probability from which the mean time between quasi-fixations follows (Corollary 7.10).
Formalizing them. All four results are classical and proved; none has a machine-checked proof on the platform or in Mathlib as of this writing. The mission produces a reusable formal Ewens distribution over integer partitions, a definition of sampling without replacement by counting labelled subsets, and an absorption probability for an explicit birth–death walk. Proofs independent of Kelly's process argument are welcome.
The book's proof of Theorem 7.1 is a process argument: in a population whose size fluctuates between and , a drop in size acts as a random deletion, and the truncated equilibrium (7.7) restricted to each size gives and . Turning that into a statement about finite sets requires the equilibrium of a truncated reversible process, which is not available here, so a formal proof must either build that process or find a direct combinatorial route. A direct route has to relate, for each description of the sample, the number of -subsets of a labelled population with a given description to products of binomial coefficients, and sum the result against (7.6); the bookkeeping over partitions is where the work lies. Theorem 7.9 needs a solution of the first-step equations of a non-symmetric walk and the identification of that solution with a hitting probability defined as a limit.
Nat.Partition n, with the multiplicity of the part ; the product in (7.6) runs over . The real binomial coefficient is the published definition AppliedComb.GenFun.binomReal.Fin M with allelic types Fin M → ℕ; the description of a labelled set is computed from the labelling. The sampling probability is times the number of -subsets whose restricted labelling has the given description. It is not defined by a formula on descriptions, and a definition that removed individuals one at a time in proportion to class sizes (the book's proof route) is ruled out as a definition because it presupposes the reduction the proof must supply.Contributions of general partition and sampling lemmas (counting subsets with a given description, the generating function identity ) are reusable beyond this mission.
A graph is perfect if every induced subgraph has chromatic number equal to its clique number, and Berge if no induced subgraph is an odd cycle of length at least five (an odd hole) or the complement of one (an odd antihole). Berge conjectured in 1961 that the two classes coincide. Chudnovsky, Robertson, Seymour and Thomas proved this, the strong perfect graph theorem, in Ann. of Math. 164 (2006), 51–229. Perfect graphs matter beyond graph theory. A graph is perfect exactly when its stable-set polytope is defined by clique inequalities (Chvátal; Lovász), so the theorem characterizes the graphs on which the stable-set and colouring integer programs are solved by their linear relaxations.
The proof is a structure theorem. Every Berge graph is basic (bipartite, the complement of a bipartite graph, the line graph of a bipartite graph or its complement, or a double split graph), or it admits a proper 2-join, a proper homogeneous pair or a balanced skew partition. The proof splits into twelve steps (1.8.1–1.8.12, p. 59), each about Berge graphs that contain a particular configuration. This mission is the first step, statement 5.1 of the paper. It covers Berge graphs that contain a large line graph, and it takes up Sections 5–8 (pp. 72–107).
All graphs are finite and simple. For a graph , is its complement. A path is an induced path, and its length is its number of edges. A track is a path in the conventional, not necessarily induced, sense. A set is connected if is connected, and anticonnected if is connected.
The line graph of a graph has vertex set , and two edges are adjacent when they share an end. is a line graph if for some graph . A subdivision of a graph replaces each edge of by a track from to , the tracks being disjoint except for their ends. A branch-vertex is a vertex of degree at least . A branch is a maximal track whose internal vertices are not branch-vertices. is 3-connected if it has more than three vertices and no set of at most two vertices disconnects it.
For a bipartite subdivision of , is degenerate if some 4-cycle of passes through its four vertices of degree three. A graph appears in if is isomorphic to an induced subgraph of for some bipartite subdivision of .
Two decompositions occur in the conclusion. A skew partition is a partition of with not connected and not anticonnected. It is balanced if no odd path joins two nonadjacent vertices of through , and no odd antipath joins two adjacent vertices of through . A proper 2-join is a partition of with nonempty disjoint such that:
The development needs further objects, each defined on its page: saturating edge sets and major vertices (pp. 77, 81), overshadowed appearances (p. 85), -enlargements (p. 75), and -strip systems with their rungs (p. 98).
Let be Berge and let be a bipartite subdivision of such that is nondegenerate and is an induced subgraph of . Then
The proposal also contains 5.2 (p. 73, step 1.8.2: Berge graphs containing ) and 5.3 (p. 74) as theorems without milestones.
5.1 is the line-graph step of the decomposition theorem. It turns "contains a substantial line graph" into "is a line graph or decomposes". The later steps of the proof start from the complementary case, where no such appearance exists (degenerate appearances in §9, prisms in §§10–13). The strip-system technique of §8 can be reused: it assembles all alternative rungs of a line-graph appearance and analyses how the rest of the graph attaches to it.
The strong perfect graph theorem is proved, but to our knowledge no proof assistant has a machine-checked proof of it. This mission formalizes one of its twelve structural steps. Several results of the same paper that the proof of 5.4 uses are posed in other missions of this series and are not posed here:
The statements 5.5, 5.6, 5.8, 8.3, 8.4 and 8.5 are also used in the proof. They are open to solvers as further lemmas.
Knowing that contains some appearance of is not enough to make a line graph or to decompose it. Vertices outside the appearance can attach to it in many ways. Each such pattern has to be shown to be impossible in a Berge graph, or to yield a larger appearance of a bigger graph , or to yield a decomposition. The first idea, analysing one outside vertex at a time, fails for two reasons. Connected sets of "minor" vertices can attach non-locally even when each vertex alone attaches locally (5.8). And anticonnected sets of "major" vertices are what produce the skew partitions (6.1). The small cases make things harder: , and degenerate subdivisions of are basic in several ways at once, so the theorem fails for them without the nondegeneracy hypothesis.
Graphs are SimpleGraph V on a Fintype. is Gᶜ. is Mathlib's H.lineGraph on H.edgeSet. " is an induced subgraph of " is an induced embedding H.lineGraph ↪g G, and "" says that this embedding is surjective. Paths and holes are vertex lists with the induced-adjacency condition. Tracks are vertex lists with consecutive vertices adjacent; their adjacency is not induced. Subdivisions carry an injection of and one track per edge of . These tracks are internally disjoint, avoid internally, and cover every vertex and every edge of . "3-connected" includes the paper's convention of more than three vertices. "", "" mean isomorphism. Existentially quantified graphs ( in an appearance, the enlargement , the graph of which is a line graph) live on Fin n.
The standing assumptions are those of each statement: is Berge and is 3-connected. In 7.1 the two edges are taken distinct, as the conclusion requires. "Up to symmetry" in 6.1 becomes an existential choice of the labelling of the 4-cycle and of the order of .
The formalization would be trivial if paths were allowed to be non-induced, if the complement bars in 5.4 and 6.1 were dropped, or if a "subdivision" could share internal track vertices or carry extra vertices or edges. The definitions rule out all three. A sorry-free check shows that is a subdivision of itself and is not bipartite.
Reusable infrastructure: tracks, branches, subdivisions, 3-connectivity, appearances and strip systems. Contributions are welcome on the graph-theoretic lemmas 5.3 and 7.1, which do not need Berge graphs, and on the Berge-specific milestones in the order listed.
Many optimization problems in statistics, signal processing and control are posed over sets of matrices with a constraint that makes them curved: matrices of fixed rank, matrices with orthonormal columns, symmetric matrices with a prescribed spectrum. Algorithms on such sets ("optimization on manifolds") compute a step in the tangent space at the current point, as in a vector space, and then need a rule that brings the point back to the set. A retraction is such a rule; the notion was introduced by Adler, Dedieu, Margulies, Martens and Shub for Newton's method on Riemannian manifolds (IMA J. Numer. Anal. 2002) and is the basic building block of the algorithms in Absil, Mahony and Sepulchre's monograph (Princeton, 2008). Any retraction preserves the local convergence of Newton's method, so the choice among retractions is about cost and convenience.
The most natural candidate is to project back onto the manifold: take the nearest point. Absil and Malick (SIAM J. Optim. 2012; preprint HAL hal-00651608) show in §3.1 that this projective retraction is always a valid retraction of maximal smoothness, and then compute it for fixed-rank, spectral and Stiefel manifolds. The underlying fact, that the nearest-point map onto a submanifold is locally single-valued and , is classical (the paper cites Lewis and Malick, Math. Oper. Res. 2008); the paper gives a short proof through the inverse function theorem on the normal bundle. This mission formalizes §3.1: that lemma and the resulting retraction.
Let be a Euclidean space, a finite-dimensional real inner product space, of dimension (in the paper's examples, with the Frobenius inner product). A set is a submanifold of class and dimension around if and there are an open neighbourhood of and a diffeomorphism from onto an open subset of with
The tangent space is the linear subspace of spanned by the tangent cone of at , and the normal space is . The tangent bundle and normal bundle are and , subsets of . denotes the orthogonal projector onto .
The projection of onto is the set of nearest points,
which may be empty (if is not closed) or contain several points (if is not convex).
A map from to is a retraction around (Definition 2.1) if on some neighbourhood of in it is of class , satisfies , and for .
The formal retraction predicate includes and a local submanifold chart at ; this ensures that its base point lies on .
For a submanifold () around , the map
is single-valued near in , and this single value is a retraction around .
The projective retraction is the reference retraction on an embedded submanifold: it exists for every submanifold, it has the maximal smoothness allowed by the tangent bundle, and it is the one practitioners compute first (truncated SVD for fixed-rank matrices, polar factor for the Stiefel manifold). Section 4 of the paper shows that it is moreover second order and generalizes it to projections along arbitrary smooth fields of transverse subspaces; Lemma 3.1 is the model of that argument. Lemma 3.1 on its own is a basic tool well beyond retractions: local single-valuedness and smoothness of the nearest-point map underlies the local convergence analysis of alternating projections on manifolds and the theory of prox-regular sets.
All statements here are proved results. No machine-checked proof of them is known to exist: Mathlib has the inverse function theorem, tangent cones and orthogonal projections onto subspaces, but no embedded submanifolds of a Euclidean space with their normal bundle and no nearest-point map onto non-convex sets. The mission produces these statements in Lean and invites proofs of them.
The obvious argument writes the nearest point as a critical point of on and applies the implicit function theorem. Two things break. First, existence: is not assumed closed, so a nearest point exists only because is locally closed near and points of far from are farther from than is. Second, uniqueness: critical points are not unique in general, and the implicit function theorem only describes critical points near a given one. Uniqueness needs a quantitative argument that every nearest point of lies in the region where on the normal bundle is injective. Finally, the normal bundle is itself only a manifold, whose tangent space at must be identified before the inverse function theorem applies; this is milestone (3.3).
The ambient space is any type E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]; is Module.finrank ℝ E, and are natural numbers with stated as a hypothesis (so that in ℕ is honest). The paper's standing assumption " is a submanifold of class () and dimension " enters only as the local hypothesis IsSubmanifoldAt k d M xbar, exactly as Lemma 3.1 and Proposition 3.2 state it ("around "). The chart is an OpenPartialHomeomorph onto EuclideanSpace ℝ (Fin n), in both directions, with 0-based coordinates. No closedness of is assumed, because the paper does not assume it.
The projection is the platform predicate IsMetricProjection M x z ( and for all ); single-valuedness is stated as equality of the set of such with a singleton, which asserts existence and uniqueness. A formalization that only states "some selection is ", or uses (satisfied by the empty set), would drop the main claim and is ruled out. The tangent space is the span of Mathlib's tangentConeAt; "class on a neighbourhood in " is ContDiffOn on with open; is a HasFDerivAt statement on the normed space ; is Submodule.starProjection.
A complete development needs: the tangent space of a slice submanifold equals the image of the chart's derivative, the normal bundle as a manifold, an inverse function theorem on it, and compactness of for small . These are reusable for the other missions of this series (fixed-rank, spectral and Stiefel manifolds, and the retractor construction of Section 4), and contributions of such general lemmas as intermediate theorems are welcome.
Networks of queues model systems in which jobs visit a sequence of service stations: items in a manufacturing job-shop, packets in a communication network, patients moving between hospital departments. The open migration process of Chapter 2 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979), and the job-shop networks of Jackson (Jackson 1963) route a customer leaving a queue at random, independently of where he has been. That rules out the most common situation in practice: an item that has passed machines 1 and 3 must next go to machine 4, while an item that has passed machines 2 and 3 must go to machine 5.
Section 3.1 of the book removes this restriction. Customers are divided into types, a type fixes a deterministic route through the queues, and a stochastic routing rule is recovered by using one type per possible route. Within each queue, the order of service is described by two position-dependent functions, which cover first-come first-served -server queues, last-come first-served, processor sharing and service in random order. Theorem 3.1 states that, for every such network, the equilibrium distribution is a product of explicit single-queue factors. This is the result behind the "Kelly network" and "Kelly-type queue" terminology of later work (Kelly 1975; Baskett, Chandy, Muntz, Palacios 1975).
There are customer types and queues. Customers of type enter the system in a Poisson stream of rate and visit the queues in that order before leaving; two successive stages of a route are at different queues.
Queue holds its customers in positions . Each customer needs an exponentially distributed amount of service with unit mean. The queue supplies total service effort at rate , with for ; a proportion goes to the customer in position . An arriving customer takes position with probability . For each , and are probability vectors on .
The class of the customer in position of queue is , his type and the stage of his route. The state of queue is and the state of the network is . Its transition rates , displays (3.1)–(3.6), are the sums of the intensities of all events taking to : a departure from the system (intensity ), a move from position of queue to position of the next queue (intensity ), and an arrival into position of the first queue of a route (intensity ).
With if and otherwise, set
If every series defining converges, then
is positive, sums to over all network states, and satisfies the equilibrium equations
Theorem 3.1 gives the full joint law of a network in which routes carry memory, and its corollaries turn it into usable performance formulas: each queue behaves, in its marginal law and as seen by arriving customers, like an isolated queue fed by a Poisson stream of rate , even though the actual arrival stream at queue is not Poisson. Mean sojourn times along a route then follow from Little's result. Theorem 3.2 identifies the reversed process as a network of the same kind; it is the source of the departure-stream results (Corollary 3.3) and of the arrival theorem (Corollary 3.5). Lemma 3.13 isolates the condition (3.26) under which state-dependent arrival rates preserve the product form (Theorem 3.14).
The results are classical and proved in the book. None of them has a machine-checked proof: the Prove2Me catalogue holds the rate-level theorems for migration processes (Chapter 2 of Kelly–Yudovina), and open targets for the BCMP and Jackson models, which have different state descriptions. This mission adds a formal model of the position-structured multiclass network itself, with the summation over coinciding transitions that (3.2), (3.4) and (3.6) require, and product-form, reversal and arrival-theorem statements over it.
The obvious first attempt, detailed balance, fails: and differ in general, because a customer's route cannot be run backwards inside the same network ( is usually when ). The equilibrium equations therefore involve, for each state, all its predecessors at once. The rates are themselves sums over coinciding transitions, so a statement about individual events does not transfer to the rates without accounting for which positions lead to the same successor state. In Lean this brings in insertion into and deletion from position lists, the relabelling of stages, and the normalization of a product over a countable space of -tuples of lists, reorganized by queue length together with the identity .
Fin I, queues Fin J; the book allows countably many types with . A network state is a function assigning to each queue a list of classes with ; the state space is countable and all sums over it are tsum/HasSum.KellyStochasticNetworks.FullBalance). The existence of the Markov process, irreducibility and non-explosion are not formalized. "The reversed process" (Theorem 3.2) is read through the reversed rates ; "the probability he finds" (Corollary 3.5) is read as a ratio of equilibrium arrival fluxes; quasi-reversibility is its rate characterization (3.8), (3.10).tsum, which Lean sets to for a divergent series; every theorem assumes the series converges, the book's "none of is zero".Infrastructure that a complete development needs: list insertion/deletion lemmas for position bookkeeping, sums of products over , and a bijection-of-events argument for summed rates. The quasi-reversibility predicate and the reversed-rate apparatus are reusable for the closed networks of §3.4 and the symmetric queues of §3.3. Contributions are welcome on any milestone, in any order.