Graph Theory

Motivation

A strongly regular graph with parameters $(n,k,\lambda,\mu)$ is a finite simple graph on $n$ vertices in which every vertex has exactly $k$ neighbours, every pair of adjacent vertices has exactly $\lambda$ common neighbours, and every pair of non-adjacent vertices has exactly $\mu$ common neighbours. For most parameter tuples the elementary counting and integrality conditions already decide existence; the interesting cases are those that survive every known feasibility test and still resist construction. The tuple $(99,14,1,2)$ is the smallest such case in the family $\lambda = 1$, $\mu = 2$, and its existence has been open for more than fifty years. John Horton Conway offered $1000 for a resolution, as one of five problems posed at the 2014 DIMACS conference on Challenges of Identifying Integer Sequences (Conway, Five $1,000 Problems (Update 2017)).

Timeline of the problem and of what is known about it:

• 1969/1971 — the parameter set is raised by Norman Biggs in his Southampton lectures (Finite Groups of Automorphisms, LMS Lecture Note Series 6, p. 111).
• 1973 — Berlekamp, van Lint and Seidel construct a strongly regular graph with parameters $(243,22,1,2)$ as the coset graph of the perfect ternary Golay code, settling one of the five feasible parameter tuples in this family.
• 1975 — the existence question appears as Problem 7 (attributed to J. J. Seidel) in R. K. Guy's problem list, The Geometry of Metric and Linear Spaces, Springer LNM 490, pp. 237–238; Conway had worked on it by then.
• 1984 — H. A. Wilbrink, On the $(99,14,1,2)$ strongly regular graph, shows that such a graph cannot be vertex-transitive: no group of automorphisms can act transitively on its 99 vertices.
• 1988 — Brouwer and Neumaier, A remark on partial linear spaces of girth 5 with an application to strongly regular graphs, Combinatorica 8, 57–61.
• 2004 — Makhnev and Minakova, On automorphisms of strongly regular graphs with $\lambda=1$, $\mu=2$, Discrete Math. Appl. 14(2), and 2011 — Behbahani and Lam, Strongly regular graphs with non-trivial automorphisms, Discrete Math. 311, 132–144: further restrictions on the possible automorphism groups.
• 2014/2017 — Conway's prize offer publicises the problem.

No graph with these parameters has been found, and no non-existence proof is known.

Setting

Fix a finite vertex set $V$ and a simple graph $g$ on $V$ (irreflexive, symmetric adjacency $\mathrm{Adj}$). For vertices $v,w$ write $N(v) = \{u : \mathrm{Adj}(v,u)\}$ for the neighbourhood of $v$ and $N(v)\cap N(w)$ for the set of common neighbours. The graph $g$ is strongly regular with parameters $(n,k,\lambda,\mu)$, written $\mathrm{IsSRGWith}\ g\ n\ k\ \lambda\ \mu$, when

• $|V| = n$;
• $|N(v)| = k$ for every vertex $v$;
• $|N(v)\cap N(w)| = \lambda$ whenever $v$ and $w$ are adjacent;
• $|N(v)\cap N(w)| = \mu$ whenever $v \neq w$ are non-adjacent.

The case $\lambda = 1$ says that every edge lies in exactly one triangle — equivalently, the neighbourhood of each vertex induces a perfect matching, so such graphs are locally linear. The case $\mu = 2$ says that every non-adjacent pair is the pair of opposite corners of exactly one $4$-cycle. Conway's problem asks for $(n,k) = (99,14)$ with these two local conditions.

Counting paths of length two from a fixed vertex gives $k(k-\lambda-1) = (n-k-1)\mu$, which for $\lambda=1$, $\mu=2$ reduces to $2n = k^2 + 2$; with $k = 14$ this yields $n = 99$. Writing $A$ for the adjacency matrix, $I$ for the identity and $J$ for the all-ones matrix, strong regularity is equivalent to the matrix identity $A^2 = kI + \lambda A + \mu(J - I - A)$, which for $(99,14,1,2)$ reads $A^2 + A = 12I + 2J$; the eigenvalues of $A$ other than $k=14$ are then $3$ and $-4$, and integrality of their multiplicities ($54$ and $44$) is one of the feasibility conditions that $(99,14,1,2)$ passes.

Formalization targets

Goal

$$\exists\ \alpha,\ \exists\ g \text{ a simple graph on } \alpha,\quad \mathrm{IsSRGWith}\ g\ 99\ 14\ 1\ 2 .$$

The goal is Mathlib's own proof_wanted conway_99 in Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean, stated verbatim: existence of a finite type carrying a strongly regular graph with parameters $(99,14,1,2)$. A resolution in either direction is welcome — a proof settles the existence half, and a proof of the negation settles the non-existence half; the platform records the two as proof and disproof of the same statement.

Supporting targets

$$2n = k^2 + 2, \qquad k \text{ even}, \qquad k \in \{2,4,14,22,112,994\}$$

for every strongly regular graph with $\lambda = 1$, $\mu = 2$: the counting identity, local linearity, and the integrality restriction that cuts the family down to five non-degenerate parameter tuples.

$$\exists\, g,\ \mathrm{IsSRGWith}\ g\ 9\ 4\ 1\ 2, \qquad \exists\, g,\ \mathrm{IsSRGWith}\ g\ 243\ 22\ 1\ 2$$

the two members of the family that are known to exist: the $3\times 3$ rook's graph (the Paley graph on $9$ vertices) and the Berlekamp–van Lint–Seidel graph.

$$|E(g)| = 693, \qquad |\{\text{triangles of } g\}| = 231, \qquad A^2 + A = 12I + 2J, \qquad g \text{ not vertex-transitive}$$

structural consequences for a hypothetical $99$-graph, the last one being Wilbrink's theorem.

Significance

A $(99,14,1,2)$ graph, if it exists, is a locally linear graph of maximal density in its parameter range and a partial linear space of girth $5$ with $99$ points and $231$ lines of size $3$; its existence would also produce new association schemes and new examples for the general classification of strongly regular graphs. A non-existence proof would be the first case in this family ruled out by anything other than the classical feasibility conditions, and would say something new about how far local conditions ($\lambda=1$, $\mu=2$) constrain global structure.

Nothing in this mission is presently formalized. Mathlib defines SimpleGraph.IsSRGWith, proves the counting identity IsSRGWith.param_eq, the complement rule IsSRGWith.compl, and the matrix identity IsSRGWith.matrix_eq, and records the $99$-graph problem as a proof_wanted. The supporting targets are of three kinds: results that are proved in the literature and only need formalizing (existence at $(9,4,1,2)$ and $(243,22,1,2)$; Wilbrink's non-vertex-transitivity; the integrality restriction on $k$); routine consequences that supply reusable infrastructure (edge and triangle counts, the spectral identity, evenness of $k$); and the goal itself, which is open mathematics.

Difficulty

The obvious approaches fail for concrete reasons. Exhaustive search is out of range: the graph has $693$ edges among $\binom{99}{2} = 4851$ pairs, and no isomorph-free generation of locally linear graphs on $99$ vertices is feasible. Algebraic constructions are blocked by Wilbrink's theorem — the graph cannot be vertex-transitive, so it is not a Cayley graph and cannot be produced by the group-theoretic constructions that yield most known strongly regular graphs, including the two that work at $(9,4,1,2)$ and $(243,22,1,2)$. On the non-existence side, every classical feasibility test (the counting identity, integrality of the eigenvalue multiplicities, the Krein conditions, the absolute bound) is passed by $(99,14,1,2)$, so a proof of non-existence needs an argument that does not factor through the parameters alone.

Formalization scope

All statements are phrased with Mathlib's SimpleGraph.IsSRGWith on a Fintype vertex type with DecidableRel adjacency, and use Fintype.card, SimpleGraph.edgeFinset, SimpleGraph.cliqueFinset 3 (triangles as $3$-cliques), SimpleGraph.adjMatrix over $\mathbb{Z}$, and graph isomorphisms g ≃g g for automorphisms. The goal quantifies over α : Type together with a Fintype α instance, so the vertex set is finite by construction and the empty type does not satisfy the cardinality clause; the statement is therefore not vacuously satisfiable. Note that Mathlib's definition constrains $\lambda$ only through pairs that are actually adjacent and $\mu$ only through pairs that are actually distinct and non-adjacent, so degenerate small graphs (the one-vertex graph, $K_3$) do satisfy IsSRGWith with $\lambda = 1$, $\mu = 2$; the supporting statements carry the cardinality hypotheses ($0 < n$, $1 < n$) that exclude them where needed, and the degenerate degree $k = 2$ is listed explicitly in the classification of feasible degrees.

Infrastructure a complete development needs, and which is reusable beyond this mission: interface lemmas for counting common neighbours in a strongly regular graph; the spectral theory of the adjacency matrix (multiplicities of the two non-principal eigenvalues, and their integrality), which is the missing ingredient for the classification of feasible degrees; a Lean construction of the perfect ternary Golay code and its coset graph, for the $(243,22,1,2)$ case; and decision procedures for strong regularity of an explicitly given small graph, for the $(9,4,1,2)$ case. Contributions to any of these are welcome, as are partial non-existence results (for instance, restrictions on automorphisms of prime order) submitted as separate statements.

Selected references

• N. Biggs, Finite Groups of Automorphisms: Course Given at the University of Southampton, October–December 1969, London Mathematical Society Lecture Note Series 6, Cambridge University Press, 1971, p. 111.
• E. R. Berlekamp, J. H. van Lint, J. J. Seidel, A strongly regular graph derived from the perfect ternary Golay code, in: A Survey of Combinatorial Theory, North-Holland, 1973, pp. 25–30.
• R. K. Guy, Problems, in: The Geometry of Metric and Linear Spaces, Springer Lecture Notes in Mathematics 490, 1975, pp. 233–244 (Problem 7, J. J. Seidel, pp. 237–238). doi:10.1007/BFb0081147
• H. A. Wilbrink, On the $(99,14,1,2)$ strongly regular graph, in: Papers dedicated to J. J. Seidel, EUT Report 84-WSK-03, Eindhoven University of Technology, 1984, pp. 342–355. PDF
• A. E. Brouwer, A. Neumaier, A remark on partial linear spaces of girth 5 with an application to strongly regular graphs, Combinatorica 8 (1988), 57–61. doi:10.1007/BF02122552
• A. A. Makhnev, I. M. Minakova, On automorphisms of strongly regular graphs with $\lambda=1$, $\mu=2$, Discrete Mathematics and Applications 14 (2004), no. 2. doi:10.1515/156939204872374
• M. Behbahani, C. Lam, Strongly regular graphs with non-trivial automorphisms, Discrete Mathematics 311 (2011), 132–144. doi:10.1016/j.disc.2010.10.005
• J. H. Conway, Five $1,000 Problems (Update 2017), OEIS. PDF

Motivation

A $P_3$-packing in a graph is a collection of pairwise vertex-disjoint paths on three vertices. Determining the largest such packing is NP-hard even in restricted graph classes, so structural hypotheses that force an optimal packing are of independent interest in graph factor theory. The present question asks whether 3-vertex-connectivity and cubicity force the strongest possible packing whenever the vertex count permits a perfect partition.

A. Kelmans attributes the broader packing problem to 1984. In Problem 1.10 of Packing 3-vertex Paths in Cubic 3-connected Graphs, the question is whether every cubic 3-connected graph $G$ satisfies $\lambda(G)=\lfloor |V(G)|/3\rfloor$. Theorem 3.1 of that paper proves that the divisible-order factor statement is equivalent to several apparently stronger deletion and prescribed-edge statements; it does not prove the open claim itself. OPG-46613 records the divisible-order form targeted here.

A 2026 candidate analysis in the Vibe Mathing problem repository investigated a tempting sufficient route: find a perfect matching whose complementary 2-factor has every cycle length divisible by three. Candidate C01 explains why that condition would yield a $P_3$-factor. Candidate C02 gives an explicit proposed family $H_q$ of order $18+12q$ that has $P_3$-factors but is claimed not to satisfy the stronger matching condition. These candidate claims have computational and partial Lean checks, but no complete Lean kernel proof; they are milestones here, not declarations that the original problem or the candidate family has already been formally established.

Setting

All graphs are finite and simple. A graph is cubic when every vertex has exactly three neighbors. It is 3-vertex-connected here when it has at least four vertices and deleting any set of at most two vertices leaves a connected induced graph.

A $P_3$-factor is represented by a natural number $b$, together with a bijection

$$\operatorname{Fin}(b)\times\operatorname{Fin}(3)\simeq V(G),$$

such that, in every block, positions $0$ and $1$ are adjacent and positions $1$ and $2$ are adjacent. The path is not required to be induced: an ambient edge between positions $0$ and $2$ is allowed because the two selected path edges still form a copy of $P_3$.

A 2-factor is a spanning 2-regular subgraph. It is called divisible when every one of its connected components has order divisible by three. A divisible matching complement is a perfect matching $M$ such that the relative complement $G\setminus M$ is a divisible 2-factor.

The explicit graph $H_q$ is defined on $\operatorname{Fin}(18+12q)$. Its first nine vertices form the fixed Petersen-minus-one-vertex brick from C02; the remaining vertices form the stated cycle-and-opposite-chord brick with three joining edges. The full adjacency relation is part of the Lean definition rather than an external data file.

Formalization targets

Main goal

For every finite simple graph $G$,

$$\bigl(G\text{ cubic}\bigr)\land \bigl(G\text{ 3-vertex-connected}\bigr)\land 3\mid |V(G)| \quad\Longrightarrow\quad G\text{ has a }P_3\text{-factor}.$$

This is the OPG-46613 target. Cubicity forces the order to be even, so within this domain divisibility by three is equivalent to divisibility by six.

Literature and route milestones

The mission also formalizes the $(z1)\Leftrightarrow(z8)$ part of Kelmans's Theorem 3.1: the divisible-order factor claim is equivalent to the assertion that deleting any specified 3-vertex path leaves a $P_3$-factor. Two route lemmas state that divisible 2-factors split into $P_3$-factors and that, in cubic graphs, divisible 2-factors are equivalent to divisible perfect-matching complements.

Candidate boundary milestones

The C02 milestones ask first for the complete 18-vertex statement and then for the full family:

$$\forall q\in\mathbb N,\quad H_q\text{ is cubic and 3-vertex-connected, has a }P_3\text{-factor, and has no divisible matching complement}.$$

This separates a sufficient method from the root conclusion. It is not a counterexample to OPG-46613 because every $H_q$ in the proposed family explicitly satisfies the desired $P_3$ conclusion.

Significance

A proof of the main goal would settle the divisible-order form of a long-standing path-packing problem. Through Kelmans's equivalences it would also control several deletion and prescribed-edge variants for cubic 3-connected graphs. A disproof would require a graph satisfying all domain hypotheses but lacking a $P_3$-factor; the C02 family does not claim this.

Formalizing the candidate boundary is useful even before the root is resolved. It turns a route exclusion into a checkable theorem and prevents a search campaign from silently assuming that every relevant graph possesses a divisible complementary 2-factor. The definitions of noninduced $P_3$-factors, vertex connectivity by deletion, perfect matchings, 2-factors, and component-order divisibility are intended to be reusable in later graph-factor work.

Difficulty

The perfect-matching route is attractive because the complement of a perfect matching in a cubic graph is 2-regular. The obstruction is that its cycles need not have lengths divisible by three. The C02 candidate family is designed to expose exactly that gap: a persistent 5-cycle is claimed to occur in every complementary 2-factor even though an unrelated $P_3$-factor exists. Consequently, proving the main theorem cannot simply assume that a favorable perfect matching always exists.

The formal difficulty is also semantic. Connectivity must mean vertex connectivity, the complement must be relative to $G$ on the same vertex set, component sizes must refer to the 2-factor rather than the ambient graph, and $P_3$ must remain noninduced. Weakening any of these points can create a materially different or vacuous theorem.

Formalization scope

The development targets Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Graphs use SimpleGraph on finite vertex types. Degree is the cardinality of the actual neighbor subtype. Three-vertex-connectivity explicitly quantifies over all finite deletion sets of cardinality at most two and includes a four-vertex order guard.

The main theorem is universe-polymorphic and does not hard-code a finite graph enumeration. The $H_q$ family includes $q=0$. The factor structure uses a bijection, so disjointness and coverage cannot be discharged by duplicate or omitted vertices. Ambient chords do not invalidate a block, while both required consecutive adjacencies must be genuine graph edges. The candidate family statements remain open theorem goals ending in sorry; the shared definition module itself is sorry-free.

Welcome contributions include proofs of the model lemmas, the finite $H_0$ statement, the general C02 family, Kelmans's equivalence, or decompositions of the root theorem into faithful reusable lemmas. Numerical enumeration alone is supporting evidence and should not be presented as a kernel proof.

Selected references

• A. Kelmans, Packing 3-vertex Paths In Cubic 3-connected Graphs, arXiv:0910.2766v2, 2011, Problem 1.10 (p. 3) and Theorem 3.1 (pp. 7–8). https://arxiv.org/abs/0910.2766v2
• UnsolvedMath, OPG-46613: P3-partitions of cubic 3-connected graphs. https://www.unsolvedmath.com/problems/OPG-46613
• Vibe Mathing, C01: divisible-cycle implication and a 30-vertex obstruction, fixed repository revision 14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a. https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c01/proof.md
• Vibe Mathing, C02: an 18-vertex obstruction and an infinite family with P3-factors, fixed repository revision 14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a. https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c02/proof.md

Motivation

An obstacle representation turns a graph into a visibility system: vertices are points in the plane, and nonedges are blocked by polygonal obstacles. The obstacle number asks for the minimum number of obstacles needed. OPG-37357 records two different questions for planar graphs. The first asks whether one obstacle can ever be insufficient. The second asks whether some universal constant bounds the ordinary obstacle number of every planar graph.

The status of the two parts is different. Berman, Chappell, Faudree, Gimbel, Hartman, and Williams proved in 2017 that explicit planar graphs, including the icosahedron and their graphs $X_4$ and $X_6$, have ordinary obstacle number two. Thus the first question has a published positive answer. The universal-constant question remains the research target here. A separate invariant called planar or plane obstacle number requires a crossing-free visibility drawing; results for that invariant must not be substituted for the ordinary obstacle number used by this mission.

Setting

A finite simple graph $G$ has a $k$-obstacle drawing when its vertices are placed injectively as points in $\mathbb R^2$ and there are $k$ pairwise disjoint closed connected polygonal obstacles such that

$$uv\in E(G) \quad\Longleftrightarrow\quad [p(u),p(v)]\text{ meets no obstacle}.$$

Graph vertices lie outside every obstacle. The ordinary obstacle number $\operatorname{obs}(G)$ is the least such $k$. The drawing itself may contain crossings between visible graph edges; planarity is a property of the abstract input graph, not an extra constraint on the obstacle drawing.

The Lean model represents a polygonal obstacle as a connected finite union of closed filled triangles. This gives a compact polygonal region with exact real-coordinate segment incidence. Straight-line planarity of the abstract graph is represented separately.

Formalization targets

The two-part OPG record

The source records both

$$\exists\text{ finite planar }G,\ \operatorname{obs}(G)>1$$

and

$$\exists k\in\mathbb N\ \forall\text{ finite planar }H, \ \operatorname{obs}(H)\le k.$$

The first assertion is known in the literature and appears as a published-result milestone. The second is open and is therefore the mission's main theorem. Together they preserve the two-part source without presenting the whole record as unresolved.

Published first part

A milestone formalizes the stronger published statement

$$\exists\text{ finite planar }G, \qquad \operatorname{obs}(G)\le2 \quad\text{and}\quad \operatorname{obs}(G)\not\le1.$$

This captures ordinary obstacle number exactly two without hard-coding one graph before its adjacency data and lower-bound certificate are formalized.

Universal bound

The open milestone asks for a single natural number $k$, chosen before the graph, that works for every finite planar graph. The number of obstacle corners is not bounded by this theorem; only the number of connected polygonal obstacles is.

Significance

The published first part establishes that planarity alone does not force a one-obstacle representation. The second part asks whether planar graphs nevertheless have uniformly bounded visibility complexity. A positive answer would produce a common finite obstacle budget independent of graph order; a negative answer would require a family of planar graphs with unbounded ordinary obstacle number.

Formalization is especially useful because several nearby notions differ by one word but have different known bounds: ordinary versus plane obstacle number, arbitrary polygonal versus convex obstacles, and fixed-placement versus freely chosen drawings. The mission's definitions make those choices explicit and provide reusable segment-obstacle semantics for later geometric graph formalizations.

Difficulty

A finite combinatorial graph does not come with a canonical visibility drawing. Even when one starts with an arbitrary connected blocking set, replacing it by one bounded simple polygon requires compactness, component, incidence, and polygonal-neighborhood arguments. Conversely, lower bounds must quantify over every possible placement and obstacle, not merely refute a selected coordinate drawing.

Counting results for unrestricted graphs do not automatically preserve planarity. Bounds for planar obstacle number impose a crossing-free drawing and therefore answer a different question. The known two-obstacle examples close only the existential first part and give no universal $k$.

Formalization scope

All graph vertex types are finite. Obstacles are closed connected polygonal regions represented by finite triangle unions; they are pairwise disjoint and avoid graph vertices. Visibility uses the full closed segment, so tangency or boundary contact blocks a nonedge. The planarity witness is independent of the obstacle drawing. Empty and one-vertex graphs remain in the universal quantifier and should be handled without division or nonemptiness assumptions.

The repository's fixed-placement polygonization argument and finite arrangement code are candidate_only. They may motivate supporting lemmas, but they neither prove the unrestricted obstacle-drawing completeness theorem nor settle the universal bound. Contributions are welcome on exact geometry primitives, the published two-obstacle construction and lower bound, conversions between connected blockers and polygonal obstacles, and the universal root. A proof for the plane invariant, convex invariant, one fixed drawing, or a finite order cutoff must be labeled at that narrower scope.

Selected references

• L. W. Berman, G. G. Chappell, J. R. Faudree, J. Gimbel, C. Hartman, and G. I. Williams, Graphs with Obstacle Number Greater than One, JGAA 21(6), 2017. https://doi.org/10.7155/jgaa.00452
• J. Gimbel, P. Ossona de Mendez, and P. Valtr, Obstacle Numbers of Planar Graphs, Graph Drawing 2017. https://arxiv.org/abs/1706.06992
• M. Balko, S. Chaplick, R. Ganian, S. Gupta, M. Hoffmann, P. Valtr, and A. Wolff, Bounding and Computing Obstacle Numbers of Graphs, SIAM Journal on Discrete Mathematics 38(2), 2024. https://arxiv.org/abs/2206.15414
• Open Problem Garden / UnsolvedMath, OPG-37357. https://www.unsolvedmath.com/problems/OPG-37357

Motivation

An edge partition into cliques compresses the adjacency structure of a graph into complete pieces without allowing any edge to be counted twice. Erdős Problem 81 asks for the asymptotically sharp upper bound on the number of pieces needed when the graph is chordal. Chordal graphs have strong elimination structure, but that structure does not make the partition parameter additive under arbitrary edge deletion, and obtaining a linear error term remains substantially stronger than identifying the leading quadratic coefficient.

Erdős, Ordman, and Zalcstein studied clique partitions of chordal graphs in 1993. Their examples already exhibit the $n^2/6$ scale, while their general upper estimate had a larger quadratic coefficient. Later dense-packing results of Haxell–Rödl and Yuster compare fractional and integer triangle packings with an $o(n^2)$ gap. The project candidate combines that interface with chordal elimination arguments to formulate a uniform $n^2/6+o(n^2)$ milestone. It does not supply the $O(n)$ remainder asked for by the root.

Setting

A finite simple graph is chordal when it has no induced cycle of length greater than three. The Lean definition uses the equivalent perfect-elimination form: vertices admit an injective ranking such that the later neighbors of every vertex form a clique.

An edge partition into cliques is a finite family $\mathcal P$ of complete vertex sets such that every edge of $G$ belongs to exactly one member of $\mathcal P$. Members may share vertices but may not share edges. Write $\operatorname{cp}(G)$ for the minimum possible number of pieces.

The asymptotic notation

$$\frac{n^2}{6}+O(n)$$

means that there are constants $C>0$ and $n_0\ge1$, chosen independently of $G$ and $n$, such that every chordal $n$-vertex graph with $n\ge n_0$ has a clique partition with at most $n^2/6+Cn$ pieces.

Formalization targets

Erdős Problem 81

The root theorem is

$$\exists C>0\ \exists n_0\ge1\ \forall n\ge n_0\ \forall G\text{ chordal on }n\text{ vertices}, \qquad \operatorname{cp}(G)\le \frac{n^2}{6}+Cn.$$

The quantifier order is essential: $C$ and $n_0$ are universal and cannot depend on the graph.

Leading-coefficient milestone

The supporting target records the weaker uniform statement

$$\forall\varepsilon>0\ \exists n_0\ \forall n\ge n_0\ \forall G\text{ chordal on }n\text{ vertices}, \qquad \operatorname{cp}(G)\le \left(\frac16+\varepsilon\right)n^2.$$

This is the precise $n^2/6+o(n^2)$ form. It is not equivalent to the root: choosing $\varepsilon=1/n$ is invalid because the cutoff may depend on the fixed value of $\varepsilon$.

Significance

The root would determine the clique-partition extremum for chordal graphs up to a linear remainder, matching the scale of the complete-split examples that motivate the coefficient $1/6$. It would refine a leading-order asymptotic theorem into a uniform estimate strong enough to distinguish second-order behavior.

Formalization creates a clean interface among perfect elimination orderings, exact edge partitions, fractional edge-and-triangle decompositions, and integer triangle packings. It also forces the proof to distinguish a partition from a cover and original graph order from the order of any auxiliary hypergraph. These definitions can support other decomposition problems on chordal and split graphs.

Difficulty

Perfect elimination does not by itself give the sharp partition count. Greedily taking maximal cliques may overlap in edges or accumulate too many singleton pieces. Similarly, a fractional edge-and-triangle partition can achieve the right leading coefficient while integer rounding loses $o(n^2)$ pieces; the root requires that loss to be only $O(n)$.

The dense-packing theorem has quantifiers of the form “for every fixed $\varepsilon>0$ there exists $N(\varepsilon)$.” It therefore yields a uniform subquadratic error but no linear error. Any proof of the root must add a chordal-specific rounding or extremal reduction rather than treating the general packing theorem as if its $\varepsilon$ could vary with $n$.

Formalization scope

Graphs are finite and simple. Chordality is encoded by existence of a perfect-elimination ranking, including disconnected and edgeless graphs. A clique piece is a finite vertex set that spans a complete subgraph. Exactness means every actual edge occurs in exactly one piece; no nonedge can occur inside a piece. Bounds are compared in $\mathbb R$ so the displayed asymptotic expressions retain their conventional form, while the number of parts remains a natural number.

The candidate derivation of the leading coefficient imports finite linear-programming duality and the Haxell–Rödl/Yuster fixed-triangle packing approximation. It is candidate_only, not an admitted result or kernel proof. Contributions may formalize the perfect-elimination lemmas, the fractional compression, the uniform packing interface, complete-split lower examples, or the root linear rounding theorem. A result for edge-and-triangle pieces only, a fractional partition, or one fixed order must not be presented as the unrestricted integer clique-partition theorem.

Selected references

• P. Erdős, E. T. Ordman, and Y. Zalcstein, Clique Partitions of Chordal Graphs, Combinatorics, Probability and Computing 2(4), 1993. https://doi.org/10.1017/S0963548300000808
• P. E. Haxell and V. Rödl, Integer and Fractional Packings in Dense Graphs, Combinatorica 21, 2001. https://doi.org/10.1007/s004930170003
• R. Yuster, Integer and fractional packing of families of graphs, 2003. https://arxiv.org/abs/math/0305350
• Erdős Problems, Problem 81. https://www.erdosproblems.com/81

Motivation

Expander graphs are sparse graphs in which every set of vertices has many neighbours. Families of them with bounded degree and expansion bounded away from zero are a basic tool of theoretical computer science: they are the main component of the sorting network of Ajtai, Komlós and Szemerédi (AKS 1983), the building block of superconcentrators and other graphs with strong connectivity properties, and an ingredient of many later constructions in coding theory, derandomization and complexity.

Expansion is hard to certify. Checking that every set of vertices has many neighbours means looking at exponentially many sets, and computing the exact expansion of a graph is coNP-complete. A spectral quantity, by contrast, is computable in polynomial time. N. Alon's paper Eigenvalues and expanders (Combinatorica 6 (1986) 83–96) proves that for regular bipartite graphs the two notions are equivalent: a graph is a strong expander if and only if the second-smallest eigenvalue of its Laplacian is bounded away from 0, with explicit constants in both directions. This is a discrete counterpart of Cheeger's inequality for Riemannian manifolds.

Timeline.

• 1983: Ajtai, Komlós and Szemerédi use bounded-degree bipartite expanders to build sorting networks of depth $O(\log n)$.
• 1984: Tanner (SIAM J. Alg. Disc. Meth. 5) bounds the neighbourhood size of a set in a regular bipartite graph by its second eigenvalue, the direction "eigenvalue gap implies expansion".
• 1985: Alon and Milman (J. Combin. Theory Ser. B 38) prove isoperimetric inequalities for graphs in terms of $\lambda(G)$ and introduce enlargers.
• 1986: Alon proves the converse direction, "expansion implies an eigenvalue gap" (Lemma 2.4 and Theorem 3.4 of the paper).

Setting

All graphs are finite and simple. For a graph $G = (V, E)$ and a set $X \subseteq V$, $N(X) = \{v \in V : vx \in E \text{ for some } x \in X\}$ is the set of neighbours of $X$; it may meet $X$.

The Laplacian of $G$ is $Q_G = \mathrm{diag}(d(v))_{v \in V} - A_G$, where $A_G$ is the 0–1 adjacency matrix and $d(v)$ the degree of $v$. It is symmetric with eigenvalues $0 = \lambda_0 \le \lambda_1 \le \dots \le \lambda_{n-1}$, counted with multiplicity, and $\lambda(G) = \lambda_1$ is its second-smallest eigenvalue. It is positive exactly when $G$ is connected.

• An $(n, d, c)$-magnifier is a graph on $n$ vertices with maximal degree $d$ in which every $X \subseteq V$ with $|X| \le n/2$ satisfies $|N(X) - X| \ge c|X|$.
• An $(n, d, \varepsilon)$-enlarger is a graph on $n$ vertices with maximal degree $d$ and $\lambda(G) \ge \varepsilon$.
• A bipartite graph $G = (I, O; E)$ has inputs $I$, outputs $O$ and edges only between $I$ and $O$. It is a strong $(n, d, c)$-expander if $|I| = |O| = n$, the maximal degree is $d$, and for every $X \subseteq I$

$$|N(X)| \ge \Bigl(1 + c\Bigl(1 - \frac{|X|}{n}\Bigr)\Bigr)|X|.$$

Formalization targets

Goal: Theorem 3.4

Let $G = (I, O; E)$ be a $d$-regular bipartite graph with $|I| = |O| = n$ and $\lambda = \lambda(G)$.

1. If $G$ is a strong $(n, d, c)$-expander then

$$\lambda \ge \frac{c^2}{1024 + 2c^2}.$$

2. If $\lambda \ge \varepsilon$ then $G$ is a strong $(n, d, c)$-expander with

$$c = \frac{2d\varepsilon - \varepsilon^2}{d^2}.$$

Milestones, in the order of the paper

• Lemma 2.2 (Alon–Milman, already on the platform): for disjoint sets $A, B$ at distance $\varrho > 1$, $b \le (1-a)/(1 + (\lambda/d)a\varrho^2)$.
• Corollary 2.3: every $(n, d, \varepsilon)$-enlarger is an $(n, d, 2\varepsilon/(d+2\varepsilon))$-magnifier.
• Eq. (2.1): if $f$ is an eigenvector of $Q_G$ for $\lambda(G)$ and $g$ its positive part, then $\sum_{uv \in E}(g(u)-g(v))^2 \le \lambda \sum_v g^2(v)$.
• Lemma 2.4: every $(n, d, c)$-magnifier has $\lambda(G) \ge c^2/(4 + 2c^2)$.
• Lemma 3.1: a strong $(n, d, c)$-expander is a $(2n, d, c/16)$-magnifier.
• Proof of Lemma 3.3, spectrum: the two largest eigenvalues of $C^TC$, with $C$ the $I \times O$ biadjacency matrix, are $d^2$ and $(d - \lambda)^2$.
• Proof of Lemma 3.3, Tanner's bound: $|N(X)| \ge d^2|X| / \bigl(\alpha(d^2 - (d-\lambda)^2) + (d-\lambda)^2\bigr)$ with $\alpha = |X|/n$.
• Lemma 3.3: a $d$-regular bipartite graph is a strong $(n, d, (2d\lambda - \lambda^2)/d^2)$-expander.

Part (1) of the goal combines Lemmas 3.1 and 2.4; part (2) follows from Lemma 3.3.

Significance

The result. Theorem 3.4 makes expansion of regular bipartite graphs checkable in polynomial time up to a constant-factor loss. A random regular bipartite graph can be generated and its expansion certified by computing one eigenvalue. Lemma 2.4 is one of the first discrete Cheeger inequalities. Together with Corollary 2.3 it shows that magnifiers and enlargers are the same graphs up to the constants, and it underlies the later theory of spectral expanders, including the Alon–Boppana bound and Ramanujan graphs.

The formalization. The results are proved in the paper. The work is to formalize the known proofs. That includes Tanner's eigenvalue bound, which the paper only cites, and a max-flow min-cut argument, for which Mathlib has no general theorem. No machine-checked version of Lemma 2.4, Lemma 3.1, Lemma 3.3 or Theorem 3.4 is known to exist. Lemma 2.2 is already stated and proved on the platform as part of the Alon–Milman mission.

Difficulty

The direction "eigenvalue gap implies expansion" is a variational argument on the spectrum of $C^TC$. The converse is the hard one. A first attempt bounds $\lambda(G)$ from below by testing the Rayleigh quotient on indicator vectors of sets. That only gives upper bounds on $\lambda$: any one test vector does. A lower bound has to control every vector orthogonal to the constants at once. The paper first reduces to the positive part of an eigenvector (Eq. (2.1)). It then turns the combinatorial expansion of the graph into an analytic inequality for that function, using a network flow whose existence comes from the max-flow min-cut theorem. Step (ii) of the flow conditions printed on p. 87 is false as stated: the arcs $(u, u)$ of the network absorb part of the flow. The flow argument has to be repaired before it can be formalized.

Lemma 3.1 has its own obstacle: one-sided expansion of inputs must be converted into expansion of arbitrary vertex sets that mix inputs and outputs. This needs the strong form of expansion; for ordinary expanders the lemma is false.

Formalization scope

Graphs are SimpleGraph V on a Fintype. A bipartite graph lives on the sum type I ⊕ O, and IsIOBipartite forbids edges inside I and inside O. Cardinalities $|N(X)|$ are Set.ncard. "Maximal degree $d$" is read as G.maxDegree ≤ d; every statement is monotone in $d$ or fixes $d$ by regularity (G.IsRegularOfDegree d). The condition $|X| \le n/2$ is written $2|X| \le n$ in $\mathbb{N}$. All constants are real, and every subtraction and division is taken in $\mathbb{R}$.

Reused published items:

• $\lambda(G)$ is AlonMilman.Diameter.lambda1, the second-smallest eigenvalue of G.lapMatrix ℝ, which is $0$ by convention on fewer than two vertices.
• $N(X)$ is AKSSorting.Core.neighbours.
• Lemma 2.2 is AlonMilman.Diameter.theorem_2_5, which carries Alon–Milman's standing hypotheses that $G$ is connected and $n \ge 2$; outside them the inequality is trivial.

The page omits a few degenerate cases, and the following hypotheses are added for them. Each is necessary, with a counterexample recorded in the item's statement:

• $n \ge 1$ and $c \ge 0$ in Theorem 3.4 (1);
• $\varepsilon > 0$ in Theorem 3.4 (2);
• $n \ge 2$ and $c \ge 0$ in Lemma 2.4;
• $n \ge 2$ in Lemma 3.1 and in the $C^TC$ statement;
• $d \ge 1$ in Lemma 3.3;
• $\varepsilon \ge 0$ in Corollary 2.3.

Eq. (2.1) is stated in multiplied form, so no quotient by $\sum g^2$ appears.

The closing sentences of Theorem 2.5 and Theorem 3.4 ("Thus … one can prove efficiently …") are not formalized. Read as implications between expanders they reduce to monotonicity in $c$, because $c' \le c$; their content is algorithmic.

Several encodings would trivialize the mission and are excluded:

• a $\lambda$ other than the published second-smallest Laplacian eigenvalue, in particular one defined as the best constant of a quotient;
• expansion or magnifier conditions with a negative constant in a hypothesis;
• $|X| \le n/2$ with truncating natural-number division.

Contributions are welcome:

• Tanner's bound in Lean, which is reusable for any regular bipartite graph;
• a max-flow min-cut theorem for finite networks;
• the corrected flow lemma behind Eqs. (2.2)–(2.3);
• the spectral facts about $\lambda(G)$ for bipartite graphs ($\lambda \le d$ for $n \ge 2$, and $\lambda = d - \sigma_2(C)$).

Selected references

• N. Alon, Eigenvalues and expanders, Combinatorica 6 (1986) 83–96. https://doi.org/10.1007/BF02579166
• N. Alon and V. D. Milman, λ₁, isoperimetric inequalities for graphs, and superconcentrators, J. Combin. Theory Ser. B 38 (1985) 73–88. https://doi.org/10.1016/0095-8956(85)90092-9
• R. M. Tanner, Explicit concentrators from generalized N-gons, SIAM J. Algebraic Discrete Methods 5 (1984) 287–293. https://doi.org/10.1137/0605030
• M. Ajtai, J. Komlós and E. Szemerédi, Sorting in c log n parallel steps, Combinatorica 3 (1983) 1–19. https://doi.org/10.1007/BF02579338

Motivation

Several classical theorems of combinatorial optimization say that a family of sets arising from a graph packs: the maximum number of pairwise disjoint members equals the minimum size of a set meeting every member. König's theorem on bipartite graphs, Menger's theorem, the max-flow min-cut theorem of Ford and Fulkerson, Edmonds' branching theorem and the Lucchesi–Younger theorem all have this form (Seymour 1977, (1.1)–(1.5)). In the capacitated version (weights on elements, integral flows) the max-flow min-cut theorem says more: the packing property survives every deletion and replication of elements. Clutters with this stronger property are called Mengerian. For each $0$–$1$ matrix they are exactly the systems whose covering linear program and its dual have integral optima for every integral weight vector, which is why the notion matters to integer programming and polyhedral combinatorics.

Seymour's paper answers the question for the class of binary clutters, the clutters coming from binary matroids, which includes path collections, cut collections and odd-circuit collections of graphs. Earlier, Gallai's theorem implied that ports of regular matroids are Mengerian (Seymour 1977, p. 200); combined with Tutte's excluded-minor characterization of regular matroids, this showed that binary clutters without $Q_6$ or $b(Q_6)$ minors are Mengerian. Seymour shows that the second excluded minor is unnecessary, so a single small clutter is the only obstruction.

Setting

All sets are finite. A clutter $\mathbf L$ is a finite collection of finite sets, no member of which is contained in another; $\emptyset$ and $\{\emptyset\}$ are the two trivial clutters. Its ground set is $E(\mathbf L)=\bigcup_{A\in\mathbf L}A$. The blocker $b(\mathbf L)$ is the collection of minimal subsets of $E(\mathbf L)$ that meet every member of $\mathbf L$, and $\tau(\mathbf L)$ is the minimum cardinality of a member of $b(\mathbf L)$.

$\mathbf L$ is Mengerian if $\mathbf L=\{\emptyset\}$, or if for every weight map $w:E(\mathbf L)\to\mathbb Z^+$ there is an integral packing $q:\mathbf L\to\mathbb Z^+$ with $\sum_{A\ni x}q(A)\le w(x)$ for each $x\in E(\mathbf L)$ and

$$\sum_{A\in\mathbf L}q(A)=\min_{B\in b(\mathbf L)}\sum_{x\in B}w(x).$$

For a set $Z$, the deletion is $\mathbf L\setminus Z=\{A\in\mathbf L:A\cap Z=\emptyset\}$ and the contraction $\mathbf L/Z$ is the collection of minimal members of $\{A-Z:A\in\mathbf L\}$ (minimal, not minimal nonempty). A minor of $\mathbf L$ is any clutter obtained by a finite sequence of deletions and contractions.

A clutter is binary if $|A\cap B|$ is odd for all $A\in\mathbf L$ and $B\in b(\mathbf L)$; this is condition (3.2)(ii) of the paper, which is equivalent to being a port of a binary matroid. Finally

$$Q_6=\{\{1,3,5\},\{1,4,6\},\{2,3,6\},\{2,4,5\}\},$$

the triangles of $K_4$ with its edges labelled $1,\dots,6$.

For the structure theory, a circuit of a binary clutter is a minimal nonempty $C\subseteq E(\mathbf L)$ with $|C\cap B|$ even for every $B\in b(\mathbf L)$; $x$ and $y$ are parallel when $\{x,y\}$ is a circuit, and the point $\langle x\rangle$ is the parallel class of $x$. With $mb(\mathbf L)=\{B\in b(\mathbf L):|B|=\tau(\mathbf L)\}$, $\mathbf L$ is critical if $E(mb(\mathbf L))=E(\mathbf L)$. In a critical binary clutter, $x\to y$ means that every member of $mb(\mathbf L)$ containing $x$ contains $y$ while $y\notin\langle x\rangle$, and $y$ is initial if no $x$ has $x\to y$. MBC abbreviates "Mengerian binary clutter".

Formalization targets

Goal: Seymour's theorem (p. 209)

For every binary clutter $\mathbf L$,

$$\mathbf L\ \text{is Mengerian}\iff \mathbf L\ \text{has no minor isomorphic to } Q_6 .$$

Milestones

In the order the proof uses them:

• (2.3) Every minor of a Mengerian clutter is Mengerian.
• Section 1, p. 193. $Q_6$ is not Mengerian. With (2.3) this is the "only if" direction.
• (3.6)(i) Circuits of a binary clutter have at least two elements.
• (3.6)(iii) If $Z\subseteq E(\mathbf L)$ meets every member of $b(\mathbf L)$ evenly, then $Z$ is a disjoint union of circuits. If it meets every member oddly, then $Z$ is a disjoint union of circuits and one member of $\mathbf L$.
• (4.3) In a critical MBC, $x\to y$ implies $y\not\to x$.
• (4.4) In a critical MBC, $x\to y$ gives a circuit $C\ni x,y$ with $|C|\ge3$, $z\to y$ for $z\in C-\{y\}$, and $|B-(C-\{y\})|\ge\tau(\mathbf L)-1$ for $B\in b(\mathbf L)$.
• (4.5) In a critical MBC, a non-initial $x$ lies on a circuit $C$ with $|C|\ge3$ whose other elements are initial and point to $x$, and $|B\cap(C-\{x\})|\le1$ for $B\in mb(\mathbf L)$.
• (4.6) A nontrivial critical MBC has a member consisting of initial elements.
• (5.1) A binary clutter with six elements $x_1,y_1,x_2,y_2,x_3,y_3$ whose only circuits are the three sets $\{x_i,y_i,x_j,y_j\}$, together with a member $A$ that meets each pair $\{x_i,y_i\}$ once and satisfies a minimality condition, has a $Q_6$ minor.

Significance

The theorem is an excluded-minor characterization of the max-flow min-cut property. For binary clutters it decides exactly when the covering system $Mx\ge1$, $x\ge0$ has integral optimal primal and dual solutions for every integral cost vector, and it identifies $Q_6$ as the single obstruction. Its matroid form (the Corollary, p. 220) states that for a matroid $M$ the port $\Omega(M)$ is Mengerian for every element $\Omega$ if and only if $M$ is binary and has no $F_7^*$ minor. Consequences discussed in the paper include the two-commodity setting of (3.5): the clutter of minimal edge sets joining $s$ to $s'$ or $t$ to $t'$ is Mengerian exactly when the graph does not reduce to the configuration of its Figure 2. The theorem is also a basis for later work on ideal and Mengerian clutters, such as Cornuéjols' book Combinatorial Optimization: Packing and Covering (SIAM, 2001).

The result has been proved since 1977. To our knowledge no machine-checked proof exists. Mathlib at the pinned revision has matroids but no clutters, blockers, clutter minors, or matroids representable over GF(2). This mission builds that layer. The minor-closedness of the Mengerian property (2.3), the parity decomposition (3.6)(iii) and the structure theory of critical Mengerian binary clutters (4.3)–(4.6) are results in their own right and are useful beyond the main theorem.

Difficulty

The "only if" direction is short: minors of Mengerian clutters are Mengerian, and $Q_6$ fails with unit weights. The "if" direction is, in the author's words, "very much harder". A natural first idea is to show directly, by LP duality, that the covering polyhedron of a $Q_6$-free binary clutter is integral. This does not work: integrality of the polyhedron is the weak max-flow min-cut property, and $Q_6$ itself has that property while not being Mengerian, so no argument that sees only fractional optima can separate the two cases. The paper's proof works with a minimal counterexample and derives the $Q_6$ minor from the structure of critical Mengerian binary clutters in Section 4; its intermediate claims (5.2)–(5.39) hold only for that minimal counterexample, which is why they are not milestones here.

Formalization scope

Elements form a type α with decidable equality. A clutter is L : Finset (Finset α) with the clutter axiom as a hypothesis, $E(\mathbf L)$ is the union of members, and deletion and contraction take an arbitrary finite set $Z$. Weights $w$ and packings $q$ are $\mathbb N$-valued. The minimum in the Mengerian condition is expressed as "some $B\in b(\mathbf L)$ of least weight has weight equal to the packing value", never as an infimum. $\{\emptyset\}$ is Mengerian by the paper's convention, and $\tau(\{\emptyset\})$, which the paper leaves undefined, has the junk value $0$ in Lean; every item reading $\tau$ excludes $\{\emptyset\}$ or is vacuous there. "Minor" is the reflexive–transitive closure of single deletions and contractions. "Has a $Q_6$ minor" means that some minor equals the image of $Q_6$ (on Fin 6, with the paper's labels shifted down by one) under an injective relabelling Fin 6 ↪ α. Binary clutters are defined by (3.2)(ii); the paper defines them as ports of binary matroids and quotes (3.2) [15, 28] for the equivalence, and Mathlib has no GF(2)-representable matroids at this revision. Circuits are defined intrinsically, which makes (3.6)(ii) hold by definition.

Four readings would change the theorem and are ruled out: real-valued packings $q$ (the weak max-flow min-cut property, which $Q_6$ has, so the goal would be false), a non-minimal blocker or one not restricted to $E(\mathbf L)$, dropping the $\{\emptyset\}$ exception, and reading "$Q_6$ minor" as literal equality instead of isomorphism.

A complete development needs the blocker calculus ((2.1), (2.2), cited from [28] with proofs omitted), the parity theory of binary clutters, and the replication operation $\mathbf L_w$. The clutter layer (blocker, minors, Mengerian, binary, circuits) is reusable for later work on ideal clutters, Lehman's theorem and the Corollary's matroid form. Proofs of any milestone, of the helper facts $b(b(\mathbf L))=\mathbf L$, (2.1) and (2.2), and of the equivalences in (3.2) are welcome.

Selected references

• P. D. Seymour, The Matroids with the Max-Flow Min-Cut Property, J. Combin. Theory Ser. B 23 (1977) 189–222. https://doi.org/10.1016/0095-8956(77)90031-4
• J. Edmonds and D. R. Fulkerson, Bottleneck extrema, J. Combin. Theory 8 (1970) 299–306. https://doi.org/10.1016/S0021-9800(70)80083-7
• L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canad. J. Math. 8 (1956) 399–404. https://doi.org/10.4153/CJM-1956-045-5
• G. Cornuéjols, Combinatorial Optimization: Packing and Covering, CBMS-NSF Regional Conf. Ser. in Appl. Math. 74, SIAM, 2001. https://doi.org/10.1137/1.9780898717105

Motivation

Many polytopes of combinatorial optimization have exponentially many facets, yet linear optimization over them is tractable because they are projections of simpler convex sets: affine slices of a nonnegative orthant (linear programming) or of the cone of positive semidefinite matrices (semidefinite programming). The size of such a representation, the number of variables of the extended formulation, is the natural measure of how compactly a polytope can be optimized over. Yannakakis (Expressing combinatorial optimization problems by linear programs, JCSS 1991) characterized polyhedral representations through nonnegative factorizations of the slack matrix. Gouveia, Parrilo and Thomas (arXiv:1111.3164, Mathematics of Operations Research 2013) extended the characterization to lifts into arbitrary closed convex cones, in particular to cones of positive semidefinite matrices.

The stable set polytope of a graph is the standard test case. For a perfect graph on $n$ vertices it is a linear image of an affine slice of the cone of $(n+1)\times(n+1)$ positive semidefinite matrices (Lovász's theta body construction, stated in the paper as Theorem 5.1 with a citation to Lovász & Schrijver, SIAM J. Optim. 1991); this is the reason the maximum weight stable set problem is solvable in polynomial time on perfect graphs. The question addressed by this mission is whether a smaller matrix size could suffice. Theorem 5.2 of Gouveia–Parrilo–Thomas answers it: for every graph on $n$ vertices, matrices of size $n$ do not suffice.

Setting

Let $G$ be a graph with vertex set $V = \{1,\dots,n\}$. A set $S \subseteq V$ is stable if no edge joins two of its elements, and its incidence vector $\chi_S \in \{0,1\}^n$ has $(\chi_S)_i = 1$ exactly when $i \in S$. The stable set polytope is

$$\mathrm{STAB}(G) = \mathrm{conv}\{\chi_S : S \text{ stable}\} \subseteq \mathbb R^n .$$

Let $\mathcal S^k_+$ be the cone of $k \times k$ real symmetric positive semidefinite matrices, with the trace inner product $\langle A, B\rangle = \mathrm{tr}(AB)$, under which it is self-dual. For a closed convex cone $K$, a set $C$ has a $K$-lift if $C = \pi(K \cap L)$ for an affine subspace $L$ and a linear map $\pi$; the lift is proper if $L$ meets the interior of $K$.

For a polytope $P$ with vertices $p_1,\dots,p_v$ and facet inequalities $h_1(x) \ge 0, \dots, h_f(x) \ge 0$, the slack matrix is the nonnegative $v\times f$ matrix $(h_j(p_i))$. A $K$-factorization of a nonnegative matrix $M$ assigns $a^i \in K$ to each row and $b^j \in K^*$ to each column with $\langle a^i, b^j\rangle = M_{ij}$. In Lean the objects are stab, HasPSDLift, HasConeLift, HasProperConeLift, IsSlackMatrix, HasConeFactorization and HasPSDFactorization in the namespace ConeLifts.StableSet.

Formalization targets

Goal: Theorem 5.2

For every $n \ge 1$ and every graph $G$ on $n$ vertices,

$$\neg\ \exists\, L,\ \pi:\quad \mathrm{STAB}(G) = \pi(\mathcal S^n_+ \cap L).$$

The statement excludes all lifts, proper or not, and holds for every graph, perfect or not.

Milestones

1. Theorem 3.3 (first sentence). If a full-dimensional polytope $P$ with the origin in its interior has a proper $K$-lift, then every slack matrix of $P$ admits a $K$-factorization.
2. Rows of the submatrix. The origin and $e_1,\dots,e_n$ are vertices of $\mathrm{STAB}(G)$.
3. Columns of the submatrix. For $n \ge 1$, each $\{x \in \mathrm{STAB}(G) : x_i = 0\}$ is a facet, and some facet does not contain the origin.
4. The core lemma. For every $s \in \mathbb R^n$ the block matrix

$$S' = \begin{pmatrix} 1 & 0_n \\ s & I_n\end{pmatrix}$$

has no $\mathcal S^n_+$-factorization.

Significance

Theorem 5.2 shows that the semidefinite representation of $\mathrm{STAB}(G)$ for perfect graphs has the smallest possible matrix size: $n+1$ cannot be lowered to $n$. As Remark 5.3 of the paper notes, the same argument shows that no polytope in $\mathbb R^n$ with a vertex at which it locally looks like the nonnegative orthant has an $\mathcal S^n_+$-lift. It is also an instance of the factorization method: a statement about all possible semidefinite representations is reduced to a finite obstruction on a small submatrix of the slack matrix.

The theorem is proved in the paper. To the best of our knowledge no machine-checked proof of it, of the factorization theorem for cone lifts, or of any positive semidefinite lower bound for a polytope exists in Mathlib or on this platform. A formalization produces reusable statements about positive semidefinite factorizations, slack matrices and lifts, and a verified instance of the general lower-bound technique.

Difficulty

The step from lifts to factorizations is where the direct argument fails. Theorem 3.3 applies only to proper lifts and only to polytopes with the origin in their interior, while the goal concerns all lifts of a polytope that has the origin as a vertex. Applying Theorem 3.3 to $\mathrm{STAB}(G)$ and an arbitrary lift therefore does not match its hypotheses, and the printed proof does not spell out how the two gaps are closed (see Formalization scope). Theorem 3.3 itself is a consequence of the general factorization theorem of the paper (Theorem 2.4), whose proof rests on conic duality. The core lemma about $S'$ is a statement about every family of $2(n+1)$ positive semidefinite matrices, so it cannot be settled by any finite search.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); vertex $i+1$ of the paper is i : Fin n; graphs are SimpleGraph (Fin n) and stability is SimpleGraph.IsIndepSet. Vertices of a polytope are Set.extremePoints ℝ. $\mathcal S^k_+$ is the set of real $k\times k$ matrices satisfying Matrix.PosSemidef (which includes symmetry), and the ambient space of a positive semidefinite lift is all $k \times k$ matrices; this does not change which sets have lifts, because a lift in the symmetric matrices extends linearly and a lift in all matrices restricts to them. Positive semidefinite factorizations require both factor families to be positive semidefinite and use $\mathrm{tr}(A_iB_j)$.

Reading decisions: the goal assumes $n \ge 1$, the paper's meaning of "a graph with $n$ vertices", since for $n = 0$ the polytope $\{0\}$ is the image of $\mathcal S^0_+$ and the printed statement fails. Milestone 3 also assumes $n \ge 1$, and so does Milestone 1 (Theorem 3.3): in $\mathbb R^0$ the point $\{0\}$ has a proper lift to the whole space $\mathbb R^m$, whose dual cone $\{0\}$ cannot factor the slack matrix $(1)$. In Milestone 4 the column $*_n$ is an arbitrary real vector. The slack matrices of Theorem 3.3 are encoded through the identification on p. 9 of the paper: rows are vertices of $P$, columns are extreme points $y$ of the polar $P^\circ = \{y : \langle x, y \rangle \le 1\ \forall x \in P\}$, the canonical entry is $1 - \langle p, y\rangle$, and every slack matrix is the canonical one with positively scaled columns. Facets in Milestone 3 are nonempty proper exposed faces of dimension one less than the polytope.

The goal must not be weakened to proper lifts, and lifts must use equality $\mathrm{STAB}(G) = \pi(\mathcal S^n_+ \cap L)$ with $\pi$ linear and $L$ affine; with inclusion, or with arbitrary maps, the statement becomes trivial or false. The core lemma is meaningful only with both factor families positive semidefinite; without that requirement $S'$ factors trivially.

Beyond the milestones, a complete proof of the goal needs two facts the paper uses without stating them as claims of this proof: (a) an $\mathcal S^n_+$-lift that is not proper is a proper lift to a face of $\mathcal S^n_+$ (p. 5), every face of $\mathcal S^n_+$ is isomorphic to some $\mathcal S^r_+$ with $r \le n$ (Example 4.2, p. 12), and an $\mathcal S^r_+$-factorization yields an $\mathcal S^n_+$-factorization; (b) lifts are preserved by affine maps (Proposition 2.9, pp. 6–7), and translating a polytope changes its slack matrices only by positive column scalings, which is how Theorem 3.3 applies to $\mathrm{STAB}(G)$, whose origin is a vertex rather than an interior point. Stating (a) and (b) as separate lemmas is welcome.

Needed infrastructure: positive semidefinite matrices and the trace pairing, the face structure of $\mathcal S^n_+$, invariance of lifts under affine maps, and conic duality for Theorem 3.3. All of these are reusable beyond this mission. Contributions welcome: proofs of the milestones, the bridging facts (a) and (b), and alternative routes to the goal.

Selected references

• J. Gouveia, P. A. Parrilo, R. R. Thomas, Lifts of Convex Sets and Cone Factorizations, Mathematics of Operations Research 38(2):248–264, 2013. arXiv:1111.3164v2. https://arxiv.org/abs/1111.3164
• M. Yannakakis, Expressing combinatorial optimization problems by linear programs, Journal of Computer and System Sciences 43(3):441–466, 1991. https://doi.org/10.1016/0022-0000(91)90024-Y
• L. Lovász, A. Schrijver, Cones of matrices and set-functions and 0-1 optimization, SIAM Journal on Optimization 1(2):166–190, 1991. https://doi.org/10.1137/0801013

Motivation

The stable set problem (vertex packing) asks for a largest set of pairwise non-adjacent nodes of a graph. It is NP-hard, and its polyhedral study, the description of the stable set polytope $\mathrm{STAB}(G)$ by linear inequalities, is one of the most studied topics of polyhedral combinatorics. Classes of valid inequalities (clique, odd hole, odd antihole, wheel constraints) and the graph classes they describe exactly (perfect, $t$-perfect, $h$-perfect graphs) organize much of that literature; see Grötschel, Lovász and Schrijver, Geometric Algorithms and Combinatorial Optimization (Springer, 1988).

Lovász and Schrijver (SIAM J. Optim. 1(2), 1991) introduced a general lift-and-project procedure for 0–1 programs: lift a relaxation $K$ into a space of matrices, impose linear conditions that every 0–1 point satisfies, and project back. One round of their operator $N$ gives a tighter relaxation $N(K)$ that still contains every 0–1 point of $K$; $n$ rounds give the 0–1 hull. The procedure is an ancestor of the Sherali–Adams and Lasserre hierarchies, and the stable set problem is its first test case. This mission formalizes the paper's exact description of what one round of $N$ does to the fractional stable set polytope: it adds precisely the odd hole constraints.

Setting

Let $G = (V, E)$ be a finite graph with no isolated nodes, $n = |V|$. Vectors of $\mathbb{R}^{V \cup \{0\}}$ have a distinguished coordinate $x_0$; $\mathbb{R}^V$ sits inside as the hyperplane $H_0 = \{x_0 = 1\}$, via $x \mapsto (1, x)$.

• $\mathrm{FRAC}(G) \subseteq \mathbb{R}^V$ is the solution set of the nonnegativity constraints $x_i \ge 0$ ($i \in V$) and the edge constraints $x_i + x_j \le 1$ ($ij \in E$).
• $\mathrm{FR}(G) \subseteq \mathbb{R}^{V\cup\{0\}}$ is the cone given by $x_i \ge 0$ and $x_i + x_j \le x_0$; it is the cone spanned by the vectors $(1, x)$ with $x \in \mathrm{FRAC}(G)$.
• $Q$ is the cone spanned by the 0–1 vectors with $x_0 = 1$. For a convex cone $K$, its polar cone is $K^* = \{u : u^{\mathsf T}x \ge 0 \ \forall x \in K\}$.
• $M(K) = M(K, Q)$ is the set of $(n+1)\times(n+1)$ matrices $Y = (y_{ij})$ that are symmetric, satisfy $y_{ii} = y_{0i}$ for $i \in V$, and satisfy $u^{\mathsf T} Y v \ge 0$ for all $u \in K^*$, $v \in Q^*$.
• $N(K) = \{Y e_0 : Y \in M(K)\}$, and $N(G) = \{x \in \mathbb{R}^V : (1, x) \in N(\mathrm{FR}(G))\}$.
• A set $C \subseteq V$ is an odd hole if it induces a chordless cycle of odd length $|C| \ge 3$ (triangles included). Its odd hole constraint is $\sum_{i \in C} x_i \le \frac12(|C| - 1)$.

Formalization targets

Goal: Theorem 2.3 (p. 178)

For every finite graph $G$ without isolated nodes,

$$N(G) = \Big\{x \in \mathbb{R}^V : x_i \ge 0\ (i \in V),\ \ x_i + x_j \le 1\ (ij \in E),\ \ \sum_{i \in C} x_i \le \tfrac12(|C|-1)\ (C \text{ an odd hole})\Big\}.$$

Milestones, in the order the proof uses them

1. Lemma 1.3 (p. 171): for a convex cone $K \subseteq Q$ and $i \in V$, $N(K) \subseteq (K \cap H_i) + (K \cap G_i)$, with $H_i = \{x_i = 0\}$, $G_i = \{x_i = x_0\}$.
2. Lemma 2.2 (p. 178): if both the deletion and the contraction of some node $v$ give inequalities valid for $K$, then $a^{\mathsf T}x \le b$ is valid for $N(K)$.
3. Part (1) of the proof of Theorem 2.3 (p. 178): for an odd hole $C$ and $i \in C$, the deletion and contraction of $i$ in the odd hole constraint are valid for $\mathrm{FRAC}(G)$.
4. Observation of Section 2.b (p. 177): every $Y \in M(\mathrm{FR}(G))$ has $y_{ij} = 0$ for $ij \in E$.
5. Part (2) of the proof of Theorem 2.3 (p. 178): $x \in N(G)$ if and only if some nonnegative symmetric $Y$ with $y_{00} = 1$, $y_{i0} = y_{ii} = x_i$ satisfies $x_i + x_j + x_k - 1 \le y_{ik} + y_{jk} \le x_k$ for all $i, j, k$ with $ij \in E$.
6. Lemma 2.4 (p. 178): a system $a(ij) \le y_i + y_j \le b(ij)$, $y \ge 0$, $y|_U = 0$ on a graph is infeasible if and only if a walk with a negative alternating sum of one of four types exists.

Significance

Theorem 2.3 gives a complete description of one round of $N$ on the stable set problem: the only new constraints are the odd hole constraints. Consequences:

• For $t$-perfect graphs (those for which nonnegativity, edge and odd hole constraints describe $\mathrm{STAB}(G)$), $N(G) = \mathrm{STAB}(G)$.
• It is the base case for the paper's bounds on the $N$-index of stable set inequalities (Theorem 2.13), and it contrasts with the semidefinite operator $N_+$, which after one round already satisfies clique, odd antihole and wheel constraints.
• Lemma 2.4 is a combinatorial feasibility criterion for systems with two variables per inequality, useful beyond this paper.

The result has been proved since 1991. At the time of drafting, Prove2Me holds no formalization of it or of any part of the Lovász–Schrijver construction, and Mathlib has none. The mission produces a formal account of the $N$ operator on the stable set polytope and a formal proof of the walk criterion for two-variable systems.

Difficulty

The inclusion of $N(G)$ in the odd hole system is a short argument once Lemma 1.3 is available. The reverse inclusion is the substance: given $x$ satisfying all odd hole constraints, one must exhibit a lifted matrix $Y$. A direct appeal to Farkas' lemma yields a certificate with no visible relation to odd cycles; the difficulty is to show that every obstruction to solvability of the matrix system forces a violated odd hole constraint, which is what Lemma 2.4 and the analysis of its four walk types accomplish. Case (d) of that analysis needs the odd hole constraints; the other cases need only the edge constraints. Lemma 2.4 itself is called folklore on the page and is stated without proof there.

A further point: Lemma 2.4 is stated for lower bounds $0 \le a$, while the lower bounds that arise from the matrix system, $x_i + x_j + x_k - 1$, can be negative.

Formalization scope

• Coordinates of $\mathbb{R}^{V\cup\{0\}}$ are indexed by Option V, with none the coordinate $x_0$. Graphs are Mathlib SimpleGraphs on a finite type $V$ with decidable adjacency. Every statement about a graph carries the paper's standing assumption that $G$ has no isolated nodes (∀ v, ∃ w, G.Adj v w).
• $M$ is defined by condition (iii), never by its rewritings. Lemma 1.3 and Lemma 2.2 take the cone $K$ closed, a hypothesis the paper leaves tacit (its cones are polyhedral); for a non-closed $K$ Lemma 1.3 is false. $\mathrm{FR}(G)$ is polyhedral, so the goal needs no such hypothesis.
• $\mathrm{FR}(G)$ is defined by its constraints; this agrees with the cone over $\mathrm{FRAC}(G)$ because $G$ has no isolated nodes.
• Lemma 2.2 is stated in cone form: $K$ is any closed convex cone inside $\mathrm{FR}(G)$, and validity is read on the slice $x_0 = 1$. The paper's extra hypothesis $\mathrm{STAB}(G) \subseteq K$ is dropped, which strengthens the lemma.
• Deletion and contraction of a node are coefficient vectors on the same graph (coefficients set to $0$), not inequalities on the subgraphs $G - v$ and $G - \Gamma(v) - v$.
• Odd holes are chordless odd cycles including triangles; triangles are needed, as $\tfrac12\mathbf 1$ satisfies all other constraints on a triangle.
• The matrix system of part (2) is stated as an equivalence; the page uses one direction.
• Lemma 2.4 uses edge values on unordered pairs and strict inequalities, exactly as printed.

A trivializing formalization is ruled out: the goal is the set equality for every graph without isolated nodes, not the existence of a lifted matrix and not a single graph.

Not formalized here: the semidefinite operator $N_+$, the operator $\hat N$, algorithmic statements (Theorems 1.6, 2.1, Corollary 2.5), and the set-function results of Section 3.

Reusable beyond this mission: the matrix cone layer ($Q$, $M$, $N$), the stable-set cones, and the two-variable feasibility criterion of Lemma 2.4. Contributions of any of the milestones, and of general facts about polar cones of polyhedral cones in this setting, are welcome.

Selected references

• L. Lovász and A. Schrijver, Cones of matrices and set-functions and 0–1 optimization, SIAM Journal on Optimization 1(2) (1991) 166–190. https://doi.org/10.1137/0801013
• M. Grötschel, L. Lovász and A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4
• H. D. Sherali and W. P. Adams, A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems, SIAM Journal on Discrete Mathematics 3(3) (1990) 411–430. https://doi.org/10.1137/0403036

Motivation

A matching in a graph is a set of edges no two of which share a node. Given a real weight on every edge, the maximum-weight matching problem asks for a matching of largest total weight. It is one of the basic problems of combinatorial optimization: assignment, pairing and scheduling problems reduce to it, and it is the standard example of a combinatorial problem that is solvable in polynomial time although it is not obviously a linear program.

For bipartite graphs the problem is a linear program in disguise: the polytope cut out by nonnegativity and the node-degree inequalities has only 0–1 vertices (the Birkhoff–von Neumann theorem in the square case; Mathlib has it as extremePoints_doublyStochastic). For general graphs this fails already on a triangle, where the vector with every coordinate $1/2$ satisfies all degree inequalities but is not a combination of matchings. Edmonds' 1965 paper (DOI 10.6028/jres.069b.013) adds one family of inequalities, one for each odd set of nodes, and proves that the resulting polyhedron has exactly the matching vectors as its vertices. The companion paper Paths, trees, and flowers gives the cardinality algorithm on which the weighted algorithm of §7 is built.

Timeline:

• 1931: König and Egerváry prove the min–max theorems for bipartite matching; 1946: Birkhoff shows that the doubly stochastic matrices are the convex hull of the permutation matrices (the bipartite perfect-matching polytope).
• 1947: Tutte characterizes graphs with a perfect matching.
• 1965: Edmonds, Paths, trees, and flowers: the blossom algorithm for maximum-cardinality matching.
• 1965: Edmonds, this paper: Theorem (P) (the matching polyhedron) and Theorem (M) (blossom-shrinking optimality certificates), with a weighted matching algorithm.

Setting

Let $G$ be a finite graph with node set $V$ and edge set $E$; each edge meets two different nodes, its ends. Real variables $x_e$ correspond to the edges $e\in E$. The polyhedron $C\subseteq\mathbb R^E$ is the set of vectors $x$ satisfying

1. $x_e\ge 0$ for every edge $e$;
2. $\sum_{e \text{ meets } v} x_e\le 1$ for every node $v$;
3. $\sum_{e \text{ has both ends in } S} x_e\le r$ for every set $S$ of $2r+1$ nodes, $r$ a strictly positive integer.

The matching vectors $P$ are the vectors with every component $0$ or $1$ that satisfy (2); they are the incidence vectors of matchings. For edge weights $c\in\mathbb R^E$, the linear form (4) is $W(c,x)=\sum_e c_e x_e$.

The dual program has a variable $y_v$ for each node and $z_S$ for each odd set $S$ ($|S|=2r_S+1$, $r_S\ge1$). Its objective is (5) $U(y,z)=\sum_v y_v+\sum_S r_S z_S$, subject to (6) $y,z\ge0$ and (7) $y_{v_1}+y_{v_2}+\sum_{S\ni v_1,v_2}z_S\ge c_e$ for every edge $e$ with ends $v_1,v_2$. For a matching $M$, conditions (8)–(10) are the complementary slackness conditions: $y_v=0$ at nodes not covered by $M$, equality in (7) on $M$, and every odd set with $z_S>0$ contains exactly $r_S$ edges of $M$.

A blossom sequence $\{G_i\}_{i=0}^n$ (Theorem (M)) starts from $G_0=G$ with matching $M_0=M$ and repeatedly shrinks an odd circuit $B_i$ (a blossom, $2a_i+1$ edges of which $a_i$ are matched) to a single node, carrying node weights $w(v^i)$ and edge weights $w(e^i)$ that obey conditions (a)–(k) of p. 127.

In the Lean development these are Graph, IsMatching, incidence, matchingPolyhedron ($C$), matchingVectors ($P$), W, U, DualFeasible ((6)–(7)), CompSlack ((8)–(10)) and BlossomSequence, all in the namespace EdmondsMatching65.Polyhedron.

Formalization targets

Goal: Theorem (P)

$$\operatorname{ext}(C)=P.$$

The vertices (extreme points) of $C$ are exactly the matching vectors of $G$. Hence the maximum weight of a matching equals $\max\{W(c,x):x\in C\}$ for every $c$.

Milestones

1. $P\subseteq\operatorname{ext}(C)$ (§2, p. 126).
2. If for every $c$ some 0–1 point of $C$ maximizes $W(c,\cdot)$ over $C$, then $\operatorname{ext}(C)=P$ (§2, p. 126).
3. Weak duality: $W(c,x)\le U(y,z)$ for $x\in C$ and $\langle y,z\rangle$ satisfying (6)–(7) (§3, p. 126).
4. If $M$ is a matching and $\langle y,z\rangle$ satisfies (6)–(10), then $W(c,\chi^M)=U(y,z)$ (§3, p. 127).
5. A blossom sequence for $M$ yields $\langle y,z\rangle$ satisfying (6)–(10) (§5, pp. 127–128).
6. For every $c$ some maximum matching has a blossom sequence (§6, p. 128).
7. Theorem (M): a matching is maximum if and only if a blossom sequence for it exists (§4, p. 127).
8. For every $c$ there are a matching $M$ and $\langle y,z\rangle$ satisfying (6)–(10) (§3, p. 127).

Significance

The result. Theorem (P) turns maximum-weight matching in general graphs into a linear program over an explicitly described polyhedron, and Theorem (M) with the §5 translation gives a short certificate of optimality for every maximum matching. Together they established the template of polyhedral combinatorics: describe the convex hull of the combinatorial objects by inequalities, and prove the description through linear programming duality and an algorithm. The matching polytope underlies the analysis of the weighted blossom algorithm, separation over odd-set inequalities (Padberg–Rao), and many later integrality results; Edmonds' own §8 states the extension to degree-constrained subgraphs.

Formalizing it. The theorem has been proved since 1965 and appears in every text on combinatorial optimization; this mission asks for a machine-checked proof of the polytope statement for general finite graphs, including parallel edges, together with the duality certificate and the blossom-sequence characterization. The prove2me platform has a proved form of Edmonds' perfect matching polytope theorem on complete graphs in convex-decomposition form (MetricTSP.pm_polytope_decomposition), a different polytope with a different conclusion; nothing states Theorem (P) or Theorem (M).

Difficulty

The inclusion $P\subseteq\operatorname{ext}(C)$ and weak duality are routine. The difficulty is the reverse inclusion: showing that no fractional point of $C$ is a vertex. The bipartite argument (a fractional point has a cycle of fractional edges along which it can be perturbed both ways) breaks on odd cycles: perturbing along an odd circuit violates a degree inequality, and the odd-set inequalities that cut off the half-integral points are exponentially many and overlap. The paper's route needs, for every weight vector, an optimal matching together with a dual solution satisfying (6)–(10), and the existence of that certificate is the substance of the weighted matching algorithm: the blossom sequence of Theorem (M) must be constructed, and the translation (11)–(16) from node and edge weights of the contracted graphs to $\langle y,z\rangle$ must be verified through the whole shrinking history.

Formalization scope

• The graph is a finite node type V, a finite edge type E and an end map ends : E → Sym2 V with no loops. Parallel edges are allowed: the contracted graphs of Theorem (M) have them, and Theorem (P) holds for multigraphs; simple graphs are the case of an injective end map.
• Vectors are E → ℝ, one coordinate per edge. Vertices are Mathlib's Set.extremePoints ℝ. Odd sets carry an explicit r : ℕ with 1 ≤ r and |S| = 2r + 1; even sets and singletons carry no inequality.
• Edge weights are arbitrary reals; matchings need not be perfect and may be empty. No connectivity, no parity of |V|.
• The dual variable z is a function on all node sets of which only odd sets are read.
• A contracted graph Gᵢ is a partition of V into blocks; an edge of G is an edge of Gᵢ when its ends lie in different blocks. Each Mᵢ must be a matching of Gᵢ, and all of (a)–(k) appear as fields of BlossomSequence; a sequence missing any of them would make milestone 6 trivial or milestone 5 false.
• A trivializing formalization is ruled out: coordinates indexed by node pairs (Sym2 V → ℝ) leave non-edge coordinates free and give a polyhedron with no extreme points, and the goal is stated as equality of extreme points, not as a convex-hull identity or as the existence of a dual certificate.
• Needed infrastructure: extreme points of polyhedra as unique maximizers of linear forms, finite LP weak duality over these index sets, and the weighted blossom algorithm (or another proof of milestone 8). The polyhedral lemmas are reusable for other integrality results; contributions on any milestone are welcome.

Selected references

• J. Edmonds, Maximum Matching and a Polyhedron With 0,1-Vertices, J. Res. Nat. Bur. Standards Sect. B 69B (1965), 125–130. https://doi.org/10.6028/jres.069b.013
• J. Edmonds, Paths, Trees, and Flowers, Canad. J. Math. 17 (1965), 449–467. https://doi.org/10.4153/CJM-1965-045-4
• W. T. Tutte, The Factorization of Linear Graphs, J. London Math. Soc. 22 (1947), 107–111. https://doi.org/10.1112/jlms/s1-22.2.107
• M. W. Padberg, M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Math. Oper. Res. 7 (1982), 67–80. https://doi.org/10.1287/moor.7.1.67
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Chapter 25.