Graph Theory

Motivation

Many planning problems combine a discrete choice with a continuous one. A robot moving through a cluttered room chooses which free regions to traverse and where exactly to cross between them; a vehicle chooses a sequence of operating modes and a trajectory within each mode. Marcucci, Umenberger, Parrilo and Tedrake (arXiv:2101.11565, SIAM J. Optim. 2024, doi:10.1137/22M1523790) abstract this as the shortest-path problem in a graph of convex sets (SPP in GCS): a shortest-path problem in which each vertex is not a point but a convex set, and the length of an edge depends on where in its two sets the path enters and leaves. The paper shows that the problem is NP-hard even in simple cases, and then gives a mixed-integer convex formulation that is exact and whose convex relaxation is strong in practice. That formulation underlies the GCS motion planners developed later by the same group.

Setting

A graph of convex sets consists of a finite directed graph $G = (\mathcal V, \mathcal E)$, a source vertex $s$, a target vertex $t \neq s$, a nonempty compact convex set $\mathcal X_v \subseteq \mathbb R^n$ for each vertex $v$, and for each edge $e = (u,v)$ an edge length $\ell_e : \mathbb R^n \times \mathbb R^n \to \mathbb R_{\ge 0}\cup\{\infty\}$, which is proper, closed and convex. No symmetry or triangle inequality is assumed. An $s$-$t$ path is a sequence $p = (v_0,\dots,v_K)$ of distinct vertices with $v_0 = s$, $v_K = t$ and $(v_k, v_{k+1}) \in \mathcal E$; $\mathcal E_p$ is the set of its edges. The SPP in GCS (2.1) is

$$\operatorname{SPP}(G) := \inf\Big\{ \sum_{e=(u,v)\in\mathcal E_p} \ell_e(x_u,x_v) : p \text{ an } s\text{-}t\text{ path},\ x_v \in \mathcal X_v \text{ for } v \in p \Big\}.$$

The perspective of a set $\mathcal X$ is the closed cone $\tilde{\mathcal X} := \operatorname{cl}\{(x,\lambda) : \lambda \ge 0,\ x \in \lambda\mathcal X\}$ (Definition 4.1). The perspective of a function $f$ is $\tilde f(x,\lambda) := \inf\{\sigma : (x,\sigma,\lambda) \in \widetilde{\operatorname{epi} f}\}$, the function whose epigraph is the perspective of the epigraph of $f$ (Definition 4.4). For $\lambda > 0$ it equals $\lambda f(x/\lambda)$.

With $\mathcal E^{\mathrm{in}}_v$ and $\mathcal E^{\mathrm{out}}_v$ the edges entering and leaving $v$, the MICP (5.5) has a flow $y_e \in \{0,1\}$ and two vectors $z_e, z'_e \in \mathbb R^n$ per edge:

$$\begin{aligned} \text{minimize}\ & \textstyle\sum_{e\in\mathcal E}\tilde\ell_e(z_e,z'_e,y_e)\\ \text{s.t.}\ & \textstyle\sum_{\mathcal E^{\mathrm{out}}_s} y_e = 1,\ \sum_{\mathcal E^{\mathrm{in}}_t} y_e = 1,\ \ \sum_{\mathcal E^{\mathrm{out}}_v} y_e \le 1,\ \ \sum_{\mathcal E^{\mathrm{in}}_v}(z'_e,y_e) = \sum_{\mathcal E^{\mathrm{out}}_v}(z_e,y_e)\ \ (v\ne s,t),\\ & (z_e,y_e)\in\tilde{\mathcal X}_u,\ (z'_e,y_e)\in\tilde{\mathcal X}_v,\ y_e\in\{0,1\}\ \ (e=(u,v)\in\mathcal E). \end{aligned}$$

Its optimal value is $\operatorname{MICP}(G)$. The paper derives (5.5) from a biconvex program (5.2), the shortest-path LP (5.1) together with vertex positions $x_v \in \mathcal X_v$ and the bilinear constraints $z_e = y_e x_u$, $z'_e = y_e x_v$. Lemma 5.4 turns every valid linear inequality on the flows at a vertex into a valid perspective constraint.

Formalization targets

Goal: Theorem 5.7 (p. 10)

Under the standing assumptions of §2 and the assumption of p. 7 that no edge enters $s$ and no edge leaves $t$,

$$\operatorname{MICP}(G) = \operatorname{SPP}(G).$$

Both sides are infima in the extended reals and equal $+\infty$ when there is no $s$-$t$ path.

Milestones

1. Remark 4.2 (p. 5): for bounded closed $\mathcal X$, $\tilde{\mathcal X} = \{(x,\lambda): \lambda\ge0,\ x\in\lambda\mathcal X\}$.
2. Remark 4.5 (p. 6): $\tilde f(x,\lambda) = \lambda f(x/\lambda)$ for $\lambda>0$, $\tilde f = \infty$ for $\lambda<0$, $\tilde f(0,0)=0$ for proper closed convex $f$.
3. Lemma 5.4 (p. 9): a valid inequality $\sum_{e\in\mathcal E_v} c_e y_e + d \ge 0$ for (5.2) lifts to the valid constraint $\big(\sum_{\mathcal E^{\mathrm{in}}_v} c_e z'_e + \sum_{\mathcal E^{\mathrm{out}}_v} c_e z_e + d x_v,\ \sum_{\mathcal E_v} c_e y_e + d\big)\in\tilde{\mathcal X}_v$.
4. Remark 5.5 (p. 9): the equality version of Lemma 5.4.
5. Path and cycles (proof of Theorem 5.7): binary flows satisfying (5.5b)–(5.5d) form the vertex-disjoint union of an $s$-$t$ path and cycles.
6. Simplification of (5.5e) (proof of Theorem 5.7): $y_e = 0$ forces $z_e = z'_e = 0$ at cost $0$; $y_e = 1$ forces $z_e\in\mathcal X_u$, $z'_e\in\mathcal X_v$ at cost $\ell_e(z_e,z'_e)$.
7. Flow along the path (proof of Theorem 5.7): for consecutive path edges $e, f$, $z'_e = z_f$.

A companion item states the recovery part of Theorem 5.7 (second and third sentences): an optimal MICP solution yields an optimal path and optimal positions $x_u = z_e$, $x_v = z'_e$.

Significance

Theorem 5.7 is what makes (5.5) usable: it says that the mixed-integer program, whose only nonconvexity is $y_e\in\{0,1\}$, solves the SPP in GCS exactly. The SPP in GCS is NP-hard by Theorem 3.1, so exactness is the most one can ask of a polynomial-size formulation, and dropping integrality gives a convex program whose value is a lower bound for branch and bound. The perspective construction of Lemma 5.4 is a general recipe, closely related to the reformulation-linearization technique, for convexifying products of flows and positions.

On the formal side, the paper's proof is half a page and leaves several points to the reader: why the integer flows decompose into a path and cycles, why the closure in the perspective cone disappears for compact sets, and why the perspective function vanishes at the origin. A machine-checked proof makes these steps explicit. The result has not been formalized before, and the mission also produces reusable statements about perspectives of sets and functions in extended-real arithmetic and about the decomposition of unit $s$-$t$ flows with degree bounds.

Difficulty

The inequality $\operatorname{MICP}(G) \le \operatorname{SPP}(G)$ is the routine half: a path and its positions give a feasible point of (5.5) of the same cost. The other half requires reading a path out of an arbitrary feasible point. Integer flows satisfying (5.5b)–(5.5d) need not be a path: they may also contain disjoint cycles, and the degree constraint (5.5c) is what prevents a cycle from sharing a vertex with the path (Example 5.10 shows the value drops without it). The cost of a cycle must be shown to be nonnegative, and the perspective constraints must be shown to collapse to $z_e = z'_e = 0$ on zero-flow edges. That step uses compactness of $\mathcal X_v$. For unbounded sets the zero slice of $\tilde{\mathcal X}_v$ is the recession cone, and the argument fails. The cost at zero flow is $\tilde\ell_e(0,0,0)$, defined by a closure, and its value $0$ uses properness and convexity of $\ell_e$, not just the formula $\lambda\ell_e(\cdot/\lambda)$.

Formalization scope

• $\mathbb R^n$ is Fin n → ℝ. Edge lengths and all optimal values are EReal; optimal values are infima (⨅/sInf), equal to $+\infty$ on an empty feasible set. Attainment is not assumed.
• The graph is a structure with a finite edge set E : Finset (V × V) over a finite vertex type, a source, a target, sets X v and lengths ℓ e. The standing assumptions of §2 ($s\ne t$; $\mathcal X_v$ nonempty, compact, convex; $\ell_e \ge 0$ proper closed convex) are the predicate IsGCS. The assumption $|\mathcal E^{\mathrm{in}}_s| = |\mathcal E^{\mathrm{out}}_t| = 0$ of p. 7 is the separate predicate NoInSNoOutT, a hypothesis of the goal, of the path-and-cycles milestone and of the recovery item.
• Paths are duplicate-free vertex lists from $s$ to $t$ along edges; $\mathcal E_p$ is the list of consecutive pairs.
• The perspective of a function is Definition 4.4's infimum over the closed perspective cone of the epigraph. The formula $\lambda f(x/\lambda)$ is not used as a definition: in Lean it would evaluate to $0$ at $\lambda = 0$ for every argument and erase the content of (5.5e). The integrality constraint $y_e \in\{0,1\}$ is part of the feasible set; without it the goal is false (§9.4 reports relaxation gaps).
• Disclosed additions: Lemma 5.4 and Remark 5.5 assume no self-loop at $v$, which the page's partition of $\mathcal E_v$ into incoming and outgoing edges presupposes. The recovery item takes the $s$-$t$ path contained in $\{e : y_e = 1\}$, since the page's claim that this set is itself a path fails when an optimal solution carries a zero-length cycle.
• Needed infrastructure: closures of cones over compact sets, extended-real infima, and the combinatorics of unit flows on finite digraphs. Proofs of any milestone, and reusable lemmas on perspectives, are welcome.

Selected references

• T. Marcucci, J. Umenberger, P. A. Parrilo, R. Tedrake, Shortest Paths in Graphs of Convex Sets, SIAM Journal on Optimization 34(1), 2024; arXiv:2101.11565v5. https://arxiv.org/abs/2101.11565
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (perspectives and recession cones, §8). https://doi.org/10.1515/9781400873173
• R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows: Theory, Algorithms, and Applications, Prentice Hall, 1993 (flow decomposition, shortest-path LP).
• T. Marcucci, M. Petersen, D. von Wrangel, R. Tedrake, Motion Planning around Obstacles with Convex Optimization, Science Robotics 8(84), 2023. https://doi.org/10.1126/scirobotics.adf7843

Motivation

The spectral radius of a graph, the largest eigenvalue of its adjacency matrix, measures how densely and how unevenly the edges of the graph are distributed. Asking which graph in a class maximizes it is a spectral analogue of the extremal question "which graph in the class has the most edges". For planar graphs the question has a long history in spectral graph theory, going back at least to Schwenk and Wilson. It also arose in geography, where the spectral radius serves as a measure of the connectivity of planar networks. To compare real networks with a theoretical upper bound, geographers wanted the planar graph of maximum spectral radius (arXiv:1606.01916v2, p. 3).

Timeline, as recorded by Tait and Tobin (pp. 1–3):

• 1978, Schwenk and Wilson: early study of the eigenvalues of planar graphs.
• 1991, Boots and Royle, and independently 1993, Cao and Vince: conjecture that the planar graph on $n \ge 9$ vertices of maximum spectral radius is $P_2 + P_{n-2}$ (Conjecture 1 of the paper). The conjecture is false for $n \in \{7, 8\}$, so some lower bound on $n$ is necessary (p. 2).
• 1988–2000: successive improvements of the upper bound on the spectral radius of planar graphs, by Hong (1988, 1995, 1998), Cao and Vince (1993), Guiduli (1996) and Ellingham and Zha (2000). These bounds do not identify the extremal graph.
• 2010, Dvořák and Mohar: an upper bound on the spectral radius of planar graphs of given maximum degree.
• Guiduli and Hayes were reported by Ellingham and Zha to have proved the conjecture for large $n$. The preprint never appeared (p. 3).
• 2017, Tait and Tobin: proof of the conjecture for all sufficiently large $n$ (Theorem 15).

Setting

All graphs are finite and simple. A graph on $n$ vertices has vertex set $\{0, 1, \dots, n-1\}$. Its adjacency matrix $A(G)$ is the $n \times n$ real matrix with entry $1$ in position $(u, w)$ when $u \sim w$ and $0$ otherwise. Its eigenvalues are real, and the largest is the spectral radius $\lambda_1(G)$.

A graph is planar if it can be drawn in the plane with vertices as distinct points and edges as simple arcs joining their ends, such that an arc meets no vertex other than its ends and two arcs meet only at common ends.

For graphs $G$ and $H$ on disjoint vertex sets, the join $G + H$ is the graph on the union of the two vertex sets that keeps every edge of $G$ and of $H$ and adds every edge between a vertex of $G$ and a vertex of $H$. Write $K_2$ for a single edge, $P_m$ for the path on $m$ vertices, and $K_2 + P_{n-2}$ for their join: two adjacent vertices, both joined to every vertex of a path on the remaining $n - 2$ vertices. The paper also writes it $P_2 + P_{n-2}$.

A planar graph $G$ on $n$ vertices is a planar spectral maximizer if $\lambda_1(G') \le \lambda_1(G)$ for every planar graph $G'$ on the same $n$ vertices.

The milestones refer to a leading eigenvector $\mathbf v$ of a maximizer, scaled so that every entry is positive and the largest entry is $1$, and to a vertex $x$ with $\mathbf v_x = 1$. For a parameter $\varepsilon > 0$ they use the sets $L = \{z : \mathbf v_z > \varepsilon\}$ and $S = V(G) \setminus L$, the edge counts $e(X)$ (edges inside $X$) and $e(X, Y)$ (edges between $X$ and $Y$), and a second vertex $w$ with $\mathbf v_w > 1 - 24\varepsilon$ that is adjacent to all but $94\varepsilon n$ vertices of $S$.

Formalization targets

Goal: Theorem 15

$$\exists N_0\ \forall n \ge N_0\ \forall G \text{ on } n \text{ vertices}: \quad G \text{ is a planar spectral maximizer} \iff G \cong K_2 + P_{n-2}.$$

The threshold $N_0$ is not fixed. The paper proves the statement only for $n$ beyond an unspecified bound, and the conjecture's bound $n \ge 9$ remains open. The equivalence encodes "the unique maximizer is $K_2 + P_{n-2}$": every maximizer is isomorphic to it, and it is itself a maximizer.

Milestones, in the order of the proof

1. If $H$ is a proper spanning subgraph of a connected graph $G$, then $\lambda_1(H) < \lambda_1(G)$ (§1.2, already proved on the platform).
2. A planar graph on $n \ge 3$ vertices has no $K_{3,3}$ subgraph and at most $3n - 6$ edges, and each of its bipartite subgraphs has at most $2n - 4$ edges (p. 8).
3. Lemma 8: $\sqrt{2n-4} < \lambda_1 < \sqrt{6n}$.
4. The counts $|L| \le 3\sqrt{2n-4}/\varepsilon$, $e(S, L) \le 2n - 4$, $e(S) \le 3n - 6$, $e(L) \le 9\sqrt{2n-4}/\varepsilon$ (p. 8).
5. Lemma 9: $\sum_{z \in L} \mathbf v_z \le \varepsilon\sqrt{2n-4} + 18/\varepsilon$ and $\sum_{z \in S} \mathbf v_z \le (1 + 3\varepsilon)\sqrt{2n-4}$.
6. Eq. (7): $\sum_{y \sim u,\, y \in S} \mathbf v_y \ge (\mathbf v_u - \varepsilon)\sqrt{2n-4} - 18/\varepsilon$ for $u \in L$.
7. Lemma 10: $\mathbf v_z > 1/\sqrt{6n}$ for every vertex $z$.
8. $|\{y \in S : y \not\sim x\}| \le 14\varepsilon n$ (p. 10).
9. Lemma 11: a vertex $w \in L$, $w \ne x$, with $\mathbf v_w > 1 - 24\varepsilon$ and $|\{y \in S : y \not\sim w\}| \le 94\varepsilon n$.
10. Lemma 12: $\mathbf v_u < 1/10$ for every $u \notin \{x, w\}$.
11. Lemma 13: $x \sim w$.
12. Lemma 14: every vertex other than $x$ and $w$ is adjacent to both.
13. A planar graph with two distinct vertices adjacent to all other vertices is a spanning subgraph of $K_2 + P_{n-2}$ (proof of Theorem 15, p. 13).

Significance

The result. Theorem 15 settles the Boots–Royle / Cao–Vince conjecture for all large $n$. It identifies the planar graph of maximum spectral radius exactly, so the theoretical upper bound that the geographic application asks for is $\lambda_1(K_2 + P_{n-2})$. Along the way, Lemmas 8–14 describe the eigenvector of the extremal graph: two vertices carry almost all of the eigenvector weight, and every other entry is below $1/10$. The same method proves the outerplanar analogue (Theorem 7, the companion mission of this series).

Formalizing it. The theorem is proved on paper and has no machine-checked proof. Formalizing it needs several pieces that are absent from Mathlib or the platform and are reusable: the edge bound $3n - 6$ and the bipartite bound $2n - 4$ for topologically planar graphs, the non-planarity of $K_{3,3}$ and $K_5$ and of their subdivisions, Rayleigh-quotient comparison of spectral radii, and the face structure of maximal planar graphs. Each milestone is a self-contained target.

Difficulty

Counting edges does not separate the candidates. A maximizer can be taken to be a maximal planar graph, so it has exactly $3n - 6$ edges. Every maximal planar graph on $n$ vertices has the same number of edges, and the standard lower bound $\lambda_1 \ge 2|E|/n$ is the same for all of them. The extremal graph is pinned down only through its eigenvector. One has to show that the weight concentrates on two vertices, which are then forced to be adjacent to each other (Lemma 13) and to every other vertex (Lemma 14). Lemma 13 is the step specific to planarity. It uses the triangular faces of a maximal planar graph to find an edge switch that keeps the graph planar. In the formal setting, planarity is topological, so every planarity fact of the argument (the edge counts, the $K_{3,3}$ and $K_5$ obstructions, the faces of a triangulation) has to be derived from the drawing.

Formalization scope

• Graphs are SimpleGraph (Fin n). "$G$ is $K_2 + P_{n-2}$" is a graph isomorphism G ≃g bookPath n, where bookPath n lives on Fin 2 ⊕ Fin (n - 2). It is not an equality on a fixed labelling.
• $\lambda_1$ is the published WangKangXue.SpectralTuran.specRad, the largest eigenvalue of the real adjacency matrix.
• Planarity is the published topological RobertsonSeymour1986.GM5.IsPlanar: a drawing by simple arcs. It is not replaced by $K_5$/$K_{3,3}$-minor-freeness or by an edge count, either of which would change the class the maximum ranges over.
• Extremality is IsSpecMax IsPlanar G: $G$ is planar and $\lambda_1(G') \le \lambda_1(G)$ for every planar $G'$ on Fin n. Every milestone from Lemma 8 to Lemma 14 assumes it. These lemmas are false for an arbitrary planar graph, so a statement that drops the hypothesis, or replaces it by a property implying the conclusion, is not acceptable.
• The eigenvector is universally quantified: every $\mathbf v$ with $A\mathbf v = \lambda_1 \mathbf v$, all entries positive, all entries at most $1$, and every $x$ with $\mathbf v_x = 1$. Such a vector exists because the maximizer is connected (Perron–Frobenius). A statement that only asserts the existence of some eigenvector is weaker and is ruled out.
• Quantifiers. "For $n$ sufficiently large" is $\exists N\ \forall n \ge N$, and $N$ may depend on $\varepsilon$. Milestones 4–8 hold for every $\varepsilon > 0$. Lemmas 11–14 hold for $0 < \varepsilon < \varepsilon_0$ with an unspecified $\varepsilon_0$, because the paper chooses $\varepsilon$ small. The quantifier on $\varepsilon$ is always outermost, so $\varepsilon$ never depends on $n$ or $G$. Lemmas 12–14 hold for every vertex $w$ satisfying the conclusion of Lemma 11 (the predicate IsSecondHub), with the constants $24$ and $94$.
• Added hypotheses. $n \ge 3$ in the planar facts and in Lemma 8, where the paper's standing "$n$ large enough" is needed only to that extent. The page names the vertex of Lemma 12 $v$, the same letter as the eigenvector; it is renamed $u$. Lemma 14's set $A$ is stated in unfolded form.
• Infrastructure that a complete development needs: Euler's formula for topologically planar graphs, the non-planarity of $K_{3,3}$ and $K_5$, Perron–Frobenius for connected graphs, and the Rayleigh quotient. Proofs of the planar facts (milestone 2) are reusable well beyond this mission. Contributions toward any of them are welcome.

Selected references

• M. Tait and J. Tobin, Three conjectures in extremal spectral graph theory, J. Combin. Theory Ser. B (2017). Preprint arXiv:1606.01916v2. https://arxiv.org/abs/1606.01916, DOI https://doi.org/10.1016/j.jctb.2017.04.006
• B. N. Boots and G. F. Royle, A conjecture on the maximum value of the principal eigenvalue of a planar graph, Geographical Analysis 23(3) (1991), 276–282.
• D. Cao and A. Vince, The spectral radius of a planar graph, Linear Algebra Appl. 187 (1993), 251–257.
• A. J. Schwenk and R. J. Wilson, On the eigenvalues of a graph, in: Selected Topics in Graph Theory, Academic Press, 1978, 307–336.
• Hong Yuan, A bound on the spectral radius of graphs, Linear Algebra Appl. 108 (1988), 135–139.
• M. N. Ellingham and X. Zha, The spectral radius of graphs on surfaces, J. Combin. Theory Ser. B 78(1) (2000), 45–56.
• Z. Dvořák and B. Mohar, Spectral radius of finite and infinite planar graphs and of graphs of bounded genus, J. Combin. Theory Ser. B 100(6) (2010), 729–739.

Bibliographic data as given in the bibliography of Tait and Tobin (pp. 21–23).

Motivation

The spectral radius $\lambda_1(G)$ of a graph $G$, the largest eigenvalue of its adjacency matrix, is a standard measure of how densely and how centrally a graph is connected. A classical theme of spectral graph theory asks, for a natural family of graphs, which member of the family on $n$ vertices maximizes $\lambda_1$. For planar graphs this question was raised by geographers comparing road and transport networks, and for outerplanar graphs it was posed by Cvetković and Rowlinson in their 1990 survey of the largest eigenvalue of a graph, where they relate it to the study of subfamilies of Hamiltonian graphs.

Conjecture (Cvetković–Rowlinson, 1990). The outerplanar graph on $n$ vertices of maximum spectral radius is $K_1 + P_{n-1}$.

Timeline:

• 1990. Cvetković and Rowlinson state the conjecture (Linear and Multilinear Algebra 28).
• 1990. Rowlinson makes partial progress, on the index of certain outerplanar graphs (Ars Combinatoria 29).
• 1993. Cao and Vince work on the spectral radius of planar graphs and the related conjecture (Linear Algebra Appl. 187).
• 2001. Zhou, Lin and Hu study the spectral radius of Hamiltonian planar and outerplanar graphs (Tsinghua Science and Technology 6).
• 2017. Tait and Tobin prove the conjecture for all sufficiently large $n$ (arXiv:1606.01916, J. Combin. Theory Ser. B, doi:10.1016/j.jctb.2017.04.006), Theorem 7.

This mission formalizes Section 2 of Tait and Tobin.

Setting

All graphs are finite and simple. An $n$-vertex graph $G$ has vertex set $V(G) = \{0, \dots, n-1\}$, adjacency matrix $A(G)$, and spectral radius $\lambda_1(G)$, the largest eigenvalue of the real symmetric matrix $A(G)$. Write $d_u$ for the degree of a vertex $u$ and $N(u)$ for its neighbourhood.

A plane drawing of $G$ places the vertices at distinct points of $\mathbb R^2$ and each edge as a simple arc between its ends; an arc passes through no other vertex, and two arcs meet only at a common end. The union of the vertex points and arcs is a compact set, so its complement has exactly one unbounded connected component, the outer face. A graph is outerplanar if it has a plane drawing in which every vertex lies on the boundary of the outer face.

The join $G + H$ of two graphs is their disjoint union together with all edges between them. The fan $K_1 + P_{n-1}$ is a single vertex joined to every vertex of a path on $n-1$ vertices; it is outerplanar and has $2n-3$ edges.

An outerplanar graph $G$ on $n$ vertices is a spectral maximizer if $\lambda_1(G') \le \lambda_1(G)$ for every outerplanar graph $G'$ on the same $n$ vertices.

Several milestones refer to a Perron vector: an eigenvector $\mathbf v$ of $A(G)$ for $\lambda_1$ with all entries positive, normalized so that its maximum entry is $1$, together with a vertex $x$ with $\mathbf v_x = 1$. For a connected graph such a vector exists by the Perron–Frobenius theorem.

Formalization targets

Goal: Theorem 7

There is $N$ such that for every $n \ge N$ and every graph $G$ on $n$ vertices,

$$G \text{ is an outerplanar spectral maximizer} \iff G \cong K_1 + P_{n-1}.$$

The forward direction is the paper's Theorem 7; the converse says that the fan is the maximizer, as the conjecture reads. The threshold $N$ is left unspecified, as in the paper.

Milestones

The milestones follow the proof in Section 2, in order:

1. a strict subgraph of a connected graph has strictly smaller $\lambda_1$ (already proved on the platform);
2. an outerplanar graph on $n \ge 2$ vertices has at most $2n-3$ edges and no $K_{2,3}$ subgraph;
3. Lemma 3: for $n \ge 3$ a spectral maximizer has $\lambda_1 > \sqrt{n-1}$;
4. Lemma 4: $d_u > \mathbf v_u n - 11\sqrt n$ for every vertex $u$;
5. Lemma 5: for $n$ large, $d_x > n - 11\sqrt n$ and $\mathbf v_u < C_1/\sqrt n$ for every $u \ne x$, with an absolute constant $C_1$;
6. Lemma 6: for $n$ large, $\sum_{z\in B}\mathbf v_z < C_2/\sqrt n$, where $B = V(G)\setminus(N(x)\cup\{x\})$;
7. for $n$ large, $B = \emptyset$: $x$ is adjacent to every other vertex;
8. an outerplanar graph with a vertex adjacent to all others is a spanning subgraph of $K_1 + P_{n-1}$.

Significance

The theorem settles, for all large $n$, a conjecture that had been open since 1990 and had resisted several partial attacks. The same paper settles, in the same framework, the planar analogue (the Boots–Royle and Cao–Vince conjecture, $K_2 + P_{n-2}$) and a conjecture on spectral irregularity. The outerplanar case is the shortest of the three.

On the formal side, the result is proved on paper but has no machine-checked proof. Completing the mission produces a formal theory of outerplanar plane drawings (edge bound, $K_{2,3}$-freeness, outerplanarity of the fan), eigenvector estimates for extremal graphs, and the full extremal theorem. The edge bound and the $K_{2,3}$ exclusion are reusable for any later work on outerplanar or series–parallel graphs. Determining the exact threshold $N$, or proving the statement for every $n \ge 2$, would be a strengthening beyond the paper.

Difficulty

There are two separate difficulties. The first is topological: the facts about outerplanar graphs that the spectral argument uses (at most $2n-3$ edges, no $K_{2,3}$ subgraph, no cycle in $G - x$ when $x$ dominates, outerplanarity of the fan) are folklore on paper but require a Jordan-curve-type argument about plane drawings, of which Mathlib currently contains very little. The second is spectral: the edge-switching step that proves $B = \emptyset$ compares $\lambda_1$ of two graphs through the Rayleigh quotient, and needs a positive Perron vector and the variational characterization of the largest eigenvalue for symmetric matrices. A purely combinatorial edge-maximization argument does not work: the fan is not the only outerplanar graph with $2n-3$ edges, so maximizing the number of edges does not identify the spectral maximizer.

Formalization scope

• Graphs are SimpleGraph (Fin n); $\lambda_1$ is the published WangKangXue.SpectralTuran.specRad, the largest eigenvalue of G.adjMatrix ℝ.
• Outerplanarity is topological: a published RobertsonSeymour1986.GM5.PlaneDrawing with every vertex point in the closure of the unbounded component of the complement of the drawing. It is not replaced by a forbidden-minor characterization; such characterizations are theorems about outerplanarity, and would change which graphs compete in the maximization.
• Extremality is IsSpecMax IsOuterplanar G: $G$ is outerplanar and no outerplanar graph on the same vertex set has larger $\lambda_1$. It is never weakened to a comparison with the fan.
• "$G$ is $K_1 + P_{n-1}$" is a graph isomorphism G ≃g fan n, with the fan on Fin 1 ⊕ Fin (n - 1).
• Perron-vector statements quantify over every positive eigenvector for $\lambda_1$ with maximum entry $1$ and every vertex $x$ with $\mathbf v_x = 1$; existential quantification over $\mathbf v$ would be weaker.
• "For some absolute constant" is an existential quantifier placed before the threshold, the graph and the vector; "for $n$ sufficiently large" is ∃ N, ∀ n ≥ N.
• Added hypotheses, each forced by a degenerate case: $n \ge 2$ for the edge bound (the bound $2n-3$ is negative below), $n \ge 3$ for Lemma 3 (it fails for $n = 2$, where the maximizer $K_2$ has $\lambda_1 = 1 = \sqrt{n-1}$).

A complete development needs the Perron–Frobenius theorem for symmetric nonnegative matrices and the Rayleigh quotient characterization of $\lambda_1$, both of general use; the theory of outerplanar drawings; and the counting arguments of the lemmas. Contributions to any of these layers are welcome, as are independent proofs of the outerplanar facts from the drawing definition.

Selected references

• M. Tait and J. Tobin, Three conjectures in extremal spectral graph theory, J. Combin. Theory Ser. B (2017), https://doi.org/10.1016/j.jctb.2017.04.006; preprint arXiv:1606.01916v2, https://arxiv.org/abs/1606.01916
• D. Cvetković and P. Rowlinson, The largest eigenvalue of a graph: a survey, Linear and Multilinear Algebra 28 (1990), 3–33.
• P. Rowlinson, On the index of certain outerplanar graphs, Ars Combinatoria 29 (1990), 221–225.
• D. Cao and A. Vince, The spectral radius of a planar graph, Linear Algebra Appl. 187 (1993), 251–257.
• J. Zhou, C. Lin and G. Hu, Spectral radius of Hamiltonian planar graphs and outerplanar graphs, Tsinghua Science and Technology 6 (2001), 350–354.

Why reaction-network balance matters

A stochastic reaction network tracks the counts of chemical species as reactions occur. Different species and reaction rates may grow at different powers of a large system-size parameter. Kang and Kurtz's model-reduction paper uses these powers to identify candidate time scales and combinations of species that can remain bounded. Before a reduced model can be justified, the dominant reactions that increase a combination must be compared with those that decrease it. Condition 3.2 makes that comparison.

Checking the condition for every nonnegative linear combination is a large task even for a finite network: the weights range over a continuum, and changing a weight can change which reactions increase or decrease the combination. The paper's Lemma 3.4 relates this task to the directed graph of species. It says that combinations supported on different strongly connected components can be checked component by component. This mission formalizes that result and the claims in its proof that carry the reduction.

The network and its graph

There are finitely many species $S_i$ and finitely many indexed reactions $k$. Reaction $k$ consumes $\nu_{ik}$ molecules of species $i$ and produces $\nu'_{ik}$ molecules of that species. The stoichiometric change is $\zeta_{ik}=\nu'_{ik}-\nu_{ik}$. Species $i$ has a nonnegative scaling exponent $\alpha_i$, and reaction $k$ has a real exponent $\beta_k$. The effective reaction exponent is $\rho_k=\beta_k+\sum_i\nu_{ik}\alpha_i$.

For a vector of nonnegative weights $\theta$, the scalar $\theta\cdot\zeta_k$ is the change in its linear combination when reaction $k$ occurs. Write $\Gamma^+_\theta$ for reactions with positive change and $\Gamma^-_\theta$ for reactions with negative change. The balance equation equates the largest $\rho_k$ on these two sets. If that equation fails, the time-scale inequality permits a chosen exponent $\gamma$ only when it is no larger than $\gamma_\theta$, the largest $\alpha_i$ on the support of $\theta$ minus the largest $\rho_k$ on $\Gamma^+_\theta\cup\Gamma^-_\theta$. Condition 3.2 is the disjunction of these two alternatives.

The species graph has an edge $S_i\to S_j$ when one reaction consumes $S_i$ and produces $S_j$. Its strongly connected components are the maximal sets of species that can reach one another by directed paths. A single species is a component when it shares no larger mutual-reachability class. A nonnegative vector supported in one such component is a component-level test vector.

Formalization targets

The goal is Lemma 3.4, p. 15. Suppose $\theta=\sum_{j=1}^m\theta^j$, each $\theta^j$ is nonnegative and supported within one maximal strongly connected component, and distinct pieces belong to distinct components. For fixed $\gamma$, the lemma asserts all three implications:

$$\begin{aligned} \bigl(\forall j,\;\mathrm{Cond}_{3.2}(\gamma,\theta^j)\bigr)&\Longrightarrow\mathrm{Cond}_{3.2}(\gamma,\theta),\\ \bigl(\forall j,\;\mathrm{Balance}(\theta^j)\bigr)&\Longrightarrow\mathrm{Balance}(\theta),\\ \bigl(\forall j,\;\gamma\le\gamma_{\theta^j}\bigr)&\Longrightarrow\gamma\le\gamma_\theta. \end{aligned}$$

The companion consequence on the same page quantifies over all nonnegative vectors: if any one of these properties holds for every vector supported in a strongly connected subgraph, then it holds for every vector. The milestones mirror the paper's proof: a chain of component pieces cannot revisit a piece; under Condition 3.2 the maximal positive exponent either satisfies the time-scale bound or is bounded by the maximal negative exponent; and the two uniform cases yield their respective alternatives.

What the result establishes

Lemma 3.4 replaces a global family of tests with tests inside individual strongly connected components. In the paper this narrows the balance checks needed before the authors study separated time scales and reduced stochastic models. The uniform balance and uniform time-scale clauses matter separately: the first preserves equality of dominant positive and negative exponents, while the second preserves the same admissible $\gamma$ across a sum of pieces. The general Condition 3.2 clause allows different pieces to satisfy different alternatives.

The mathematical result was proved in the 2010 arXiv preprint and published in 2013; it is not an open conjecture. This proposal supplies Lean statements and a reusable finite reaction-network vocabulary, with proofs left for solvers. The local sanity file checks the empty-maximum and zero-vector behavior without using sorry. The draft theorem files compile as statements, but their six proofs are not yet machine checked.

Where the reasoning is difficult

The obvious inequality for a sum says that a reaction increasing $\theta$ increases at least one piece. It does not say that the piece's dominant increasing reaction also increases the sum: contributions from other pieces can cancel it. Consequently, taking a maximum separately on each piece does not directly give the balance equation for the sum. The graph restriction is decisive because a sequence of compensating reactions would otherwise be able to cycle among pieces. The milestones isolate that no-repetition property and the two inequalities the paper obtains from it.

Formalization scope

Species, reactions, and pieces are represented by Fin s, Fin r, and Fin m; these are zero-based versions of the paper's one-based indices. The stoichiometric coefficients are natural numbers, the changes $\zeta_k$ and all scaling exponents are real, and $\alpha_i\ge0$. Following the standing restriction on p. 5, each reaction consumes at most two molecules. The paper's $\rho_k$ is computed from $\beta_k$, $\nu_k$, and $\alpha$, not supplied independently.

For a reaction set $A$, $\max_{k\in A}\rho_k$ uses WithBot ℝ, so the maximum of an empty set is $-\infty$, as the paper explicitly uses on p. 17. The support maximum in $\gamma_\theta$ is an ordinary real maximum when relevant. The value $\gamma_\theta$ is represented in EReal: when $\Gamma^+_\theta\cup\Gamma^-_\theta$ is empty, it is $+\infty$ and the time-scale inequality holds for every real $\gamma$. Subtraction is performed in the reals before conversion to EReal. Thus zero vectors do not acquire a spurious bound from a default-valued maximum or extended-real subtraction.

An edge uses positive consumption and positive production in the same indexed reaction, matching the wording on pp. 4 and 15. Mutual reachability defines a component. Each piece is required to lie in one component, and different pieces in different components. These conditions prevent splitting a single component into separately balanced pieces, which would make the goal false. An empty family of pieces is permitted; its sum is zero. The definition file is useful for the other balance results in the paper, while the graph and component lemmas can support later work on reaction-network decomposition.

Selected references

• Hye-Won Kang and Thomas G. Kurtz, Separation of time-scales and model reduction for stochastic reaction networks, arXiv:1011.1672v1, 2010, especially §2 and §§3.2–3.4, pp. 4–17. Preprint.
• Hye-Won Kang and Thomas G. Kurtz, Separation of time-scales and model reduction for stochastic reaction networks, Annals of Applied Probability 23(2), 2013. DOI. The numbered statements in this mission follow the pinned 2010 preprint.

Motivation

An expander graph has many edges leaving each small vertex set. This condition is useful when a graph must remain connected after local losses, and it also constrains the cycles that can occur. Knowing that one long cycle exists leaves open how many different lengths its cycles can have. For example, a bipartite graph has no odd cycle, so expansion alone does not make every length available. The question here is quantitative: how large must the set of available lengths be in terms of the graph's order and expansion parameter? Friedman and Krivelevich answered it with a lower bound whose dependence on the expansion parameter is polynomial up to a logarithm. Their Theorem 2 is the target of this mission. Friedman and Krivelevich, Cycle lengths in expanding graphs, pp. 2–3

The same paper separates two questions. Theorem 1 says that cycle lengths are well spread over a range, but its resulting lower bound on their number has a much smaller dependence on the expansion parameter. Theorem 2 obtains a stronger count without claiming that those lengths form an interval. This distinction matters: counting many available lengths and prescribing an arbitrary length are different demands on a graph. The paper's third theorem studies the latter demand under a different graph condition. Friedman and Krivelevich, pp. 2–4

Setting

Let $G=(V,E)$ be a finite simple graph with $n=|V|$ vertices. A simple graph has no loops or parallel edges. For a vertex set $U\subseteq V$, its external neighborhood is

$N_G(U)=\{v\in V\setminus U:\text{$v$ is adjacent to some vertex in $U$}\}.$

The graph is an $\alpha$-expander if $\alpha>0$ and, for every $U\subseteq V$ with $|U|\le\lceil n/2\rceil$,

$$|N_G(U)|\ge\alpha|U|.$$

The ceiling is part of the paper's formal Definition on p. 2. It matters at odd $n$, where the largest tested set has $(n+1)/2$ vertices. A related $(k,\alpha)$-expander uses the same inequality for every $U$ with $|U|\le k$; here $k$ may be real and the size of $U$ is still an integer. This broader notion appears in the supporting long-path lemma. Friedman and Krivelevich, pp. 1–2, 4

A cycle is a closed path with no repeated vertex apart from its starting and ending vertex. Its length is its number of edges, hence at least three. Write

$L(G)=\{\ell\in\mathbb N:\text{$G$ contains a cycle of length $\ell$}\}.$

The quantity $|L(G)|$ counts lengths, rather than the number of cycles. Two cycles of the same length contribute just one element. Since a simple cycle visits distinct vertices, $L(G)$ is finite and its cardinality is an ordinary natural number. Friedman and Krivelevich, p. 2

Formalization targets

The goal is the polynomial lower bound from Theorem 2. There is one absolute constant $c>0$ such that, for each $0<\alpha\le1$ and every sufficiently large $n$, every $\alpha$-expander $G$ on $n$ vertices satisfies

$$|L(G)|\ge c\,\frac{\alpha^3}{\log_2(2/\alpha)}\,n.$$

The paper writes $\Omega(\alpha^3/\log(1/\alpha))n$. The denominator above records the endpoint convention used in this mission; it agrees up to an absolute factor for $\alpha\le1/2$. The constant $c$ is uniform across all $\alpha$, graph orders, and graphs. The threshold for $n$ may depend on $\alpha$. Friedman and Krivelevich, p. 3, Theorem 2

Four intermediate targets reproduce claims used by the paper. Lemma 2.5 gives a path of a prescribed length from a prescribed start vertex when every $k$-vertex set has enough external neighbors and the start vertex's component is large enough. In the proof of Theorem 2, deleting $\lfloor\alpha n/4\rfloor$ vertices leaves a path of length $\lceil\alpha n/4\rceil-1$. The chosen integer

$$k(\alpha)=2\left\lceil\frac{\log_2(3/\alpha)}{\log_2(1+\alpha/2)}\right\rceil+1$$

has order at most $\log_2(2/\alpha)/\alpha$ with an absolute constant. Finally, the paper's set $X_0$ of path vertices connected to the deleted set by short paths satisfies $|X_0|\ge\alpha^2n/12$ once the rounding-sensitive small cases are excluded. These are the milestone statements, in the order in which they enter the target. Friedman and Krivelevich, pp. 6, 13–14

Significance

The theorem guarantees linearly many distinct cycle lengths for every fixed positive expansion parameter, and gives an explicit polynomial-scale dependence on that parameter. A long cycle alone proves only that one length occurs. Even a statement placing cycles near many target lengths can lose substantial strength in its dependence on $\alpha$. The count in Theorem 2 supplies a separate guarantee for graph families where the expansion parameter varies. It does not imply that every length in an interval occurs. Friedman and Krivelevich, p. 3

The result is proved in the cited paper. The formalization target is a machine-checked proof of that known statement and its selected intermediate claims. The reusable output includes an exact interface for external vertex expansion, simple cycle lengths, and the prescribed-start path lemma. The local Lean statements currently compile as open targets; they do not supply machine-checked proofs of the claims.

Difficulty

Expansion gives large neighborhoods and forces connectedness, but these facts do not by themselves distinguish cycle lengths. A tempting first argument finds a long cycle and then treats its subpaths as shorter cycles; the subpaths do not close into cycles without additional edges. A second temptation is to count cycles rather than lengths: a graph may have many cycles while all of them share only a few lengths. The central challenge is to obtain a family of cycles whose lengths can be certified as different while keeping the graph's expansion parameter visible in the count. The proof also has integer rounding at the scale $\alpha n$, where claims written for large graphs can fail on small ones. Friedman and Krivelevich, pp. 13–14

Formalization scope

Graphs are SimpleGraph (Fin n) for the goal and proof-specific milestones; the general path lemma allows any finite vertex type. Vertex sets are Set V, with Set.ncard for finite cardinality. An $\alpha$-expander tests every set up to $\lceil n/2\rceil=(n+1)/2$ in natural-number arithmetic. Cycles use SimpleGraph.Walk.IsCycle, and paths use Walk.IsPath; their length is the number of edges. This rules out a two-edge closed walk being counted as a cycle. The formal development also uses the explicit $k(\alpha)$ and the paper's $X_0$, including its condition on the internal vertices of a short connecting path.

All logarithms are binary. The shifted $\log_2(2/\alpha)$ replaces $\log_2(1/\alpha)$ only inside asymptotic bounds, because the latter vanishes at $\alpha=1$. The constant in the lower bound precedes $\alpha$ in the quantifier order. The goal includes $n\ge n_0(\alpha)$, a necessary disclosed addition: the two-vertex complete graph is an $\alpha$-expander for $\alpha\le1$ but has no cycle. The $X_0$ milestone adds $\alpha n\ge12$ to make the paper's suppressed rounding valid; otherwise the initial vertex set can be empty. The deletion milestone states the path claim for any deleted set of the indicated size, since the displayed estimate uses only that size. A formal proof needs finite graph paths, component sizes, vertex neighborhoods, and cardinality estimates. Contributions to these general lemmas are useful beyond this mission. No claim is discharged by letting an asymptotic constant depend on $\alpha$, by counting closed walks, or by exploiting division by zero.

Selected references

• L. Friedman and M. Krivelevich, Cycle lengths in expanding graphs, arXiv:1912.11011v2, 2020; published in Combinatorica 41 (2021). arXiv; DOI.

Motivation

The paper of Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (2016) has an algorithmic headline. This mission concerns one of its finite graph lemmas, Lemma 2.9. The lemma translates a condition phrased separately for every connected component into a condition on three vertex sets. A reader of graph decompositions encounters both forms: components express what remains connected after deleting vertices, while a small fixed number of parts gives a compact way to state constraints on a partition. Lemma 2.9 identifies exactly when the two forms agree for the half-balance threshold. The same result appears again in the paper as Lemma 6.2, where the authors use it in a later section.

The result does not require a tree decomposition or a treewidth hypothesis. It holds for every finite graph. That generality makes it a useful standalone target: the definitions of deletion, connected components, and the weighted three-partition can be reused wherever graph separators are studied. The mission follows the published SIAM article, with printed page 328 for the main lemma and pages 363–364 for its restatement and the supporting combinatorial observation.

Setting

Let $G$ be a finite simple graph with vertex set $V(G)$. Let $S$ and $X$ be subsets of its vertices. The deleted graph $G\setminus X$ retains precisely the vertices outside $X$ and the edges joining them. Two remaining vertices are in the same connected component when a walk joins them without passing through any vertex of $X$. Write $C_X(u)$ for the vertex set of the component containing $u\notin X$. This interpretation follows the paper's notation on page 320.

A balanced $S$-separator is a set $X$ for which each component of $G\setminus X$ contains at most half the vertices of $S$:

$$|C_X(u)\cap S|\le\frac{|S|}{2}\qquad\text{for every }u\in V(G)\setminus X.$$

The paper introduces this phrase on page 321. Here balance is a property of $X$ relative to $S$; it imposes no bound on the size of $X$. The denominator counts all vertices of $S$, including any that lie in $X$.

A three-part partition of $V(G)\setminus X$ is a triple $(M_1,M_2,M_3)$ of pairwise disjoint sets whose union is $V(G)\setminus X$. A part may be empty. Two parts have no edge between them if no edge of $G$ joins a vertex of one to a vertex of the other. Since the graph is undirected, checking the three unordered pairs of distinct parts covers the requirement for every $i\ne j$.

Formalization targets

Lemma 2.9: balanced separators and three parts

The goal is the equivalence stated on page 328, also restated as Lemma 6.2 on page 363:

$$X\text{ is a balanced }S\text{-separator} \quad\Longleftrightarrow\quad \begin{gathered} V(G)\setminus X=M_1\mathbin{\dot\cup}M_2\mathbin{\dot\cup}M_3,\\ \text{no edge joins distinct }M_i,\\ |M_i\cap S|\le |S|/2\quad(i=1,2,3). \end{gathered}$$

The equivalence is the target, including both directions. It applies even when $S$ or $V(G)\setminus X$ is empty. It does not include a bound on $|X|$.

Lemma 6.3: three bounded sums

The main supporting result on page 363 says that nonnegative integers $a_1,\ldots,a_p$ with total $q$ and $a_i\le q/2$ can be divided into three classes, each with sum at most $q/2$. The milestone list also records the paper's merge inequality and its assertion that a component cannot cross between parts having no edge between them. These are the specific claims used in the published discussion of Lemma 2.9.

Significance

Lemma 2.9 lets a componentwise balance condition be represented by three sets whose coverage, disjointness, edge separation, and cardinalities can be inspected directly. It gives an exact equivalence, so the three-part formulation loses no balanced separators and introduces none that fail the original definition. That is the mathematical content needed when a later argument represents a separator by a bounded number of regions rather than by a list of all its components. The result is already proved in the 2016 paper; the open work in this mission is a machine-checked formalization of that known result and its cited supporting claims.

Formalizing the equivalence also establishes reusable interfaces for vertex deletion and component membership in a finite simple graph. A future development can state a separator condition using IsBalancedSSep, or use the three-part conclusion without redefining what a component of $G\setminus X$ means. The independent integer-partition lemma has uses whenever indivisible nonnegative weights, each no larger than half the total, must be grouped into three bounded classes. Nothing in that statement depends on graphs.

Difficulty

There may be arbitrarily many components of $G\setminus X$, although the conclusion permits only three parts. Simply assigning all components to one part can violate the half bound, while splitting a component between different parts may create forbidden edges. A component's weight is the number of its vertices in $S$, and those weights can be uneven or zero. The theorem has to accommodate all such patterns without changing the threshold $|S|/2$. In the converse direction, the absence of edges between the three parts must control entire walks, not only their first edge; ordinary connectivity in $G$ would allow a walk through $X$ and would describe the wrong components.

Formalization scope

The Lean development uses SimpleGraph V with V : Type, [Fintype V], and [DecidableEq V]. Vertex sets are Finset V. The shared walk-based AvoidReach G X u v requires every vertex on a walk to lie outside $X$, including both endpoints; avoidComp G X u collects the vertices reachable in this way. It is used only for $u\notin X$ when quantifying over components. This shared definition matches the paper's $G\setminus X$. The graph itself need not have decidable adjacency, since the statements concern propositions rather than computations.

Half bounds are written as $2c\le |S|$ or $2c\le q$ in natural-number arithmetic. This is equivalent to the paper's rational half bound and avoids any interpretation of natural-number division. The three parts may be empty, so $X=V(G)$ is a genuine boundary case. The set $S$ may meet $X$; the right-hand denominator remains $|S|$. The graph may have no vertices. There is no treewidth parameter or size condition on $X$: adding one would change Lemma 2.9 and can make its reverse implication false. Nor may components be computed using connectivity in the original graph, where paths through deleted vertices could merge them.

The required infrastructure is finite graph walks, finite sets, cardinalities, sums over finite index types, and the three original claims in the milestone list. The graph-component definitions and the integer grouping theorem are reusable beyond this mission. Contributions that prove any milestone or the full equivalence under exactly these conventions are in scope.

Selected references

• H. L. Bodlaender, P. G. Drange, M. S. Dregi, F. V. Fomin, D. Lokshtanov and M. Pilipczuk, A c^k n 5-approximation algorithm for treewidth, SIAM Journal on Computing 45(2):317–378, 2016. DOI: 10.1137/130947374.

Motivation

A cycle cover of a graph is a collection of cycles that together use every edge at least once. Covering the edges of a network by closed tours appears in routing and inspection problems (the Chinese postman problem is the closed-walk version), and the minimum total length of a cycle cover is a classical extremal parameter of bridgeless graphs. Alon and Tarsi (Covering multigraphs by simple circuits, SIAM J. Algebraic Discrete Methods 6, 1985, pp. 345–350; reference [2] of the paper) conjectured that every bridgeless graph with $m$ edges has a cycle cover of length at most $7m/5$ (Conjecture 7.1 of the paper).

The question is closely tied to cycle double covers (CDCs): families of cycles covering every edge exactly twice. The Cycle Double Cover Conjecture of Szekeres and Seymour asserts that every bridgeless graph has one, and it suffices to prove it for cubic graphs. Brinkmann, Goedgebeur, Hägglund and Markström (Generation and properties of snarks, arXiv:1206.6690v3, 2013; J. Combin. Theory Ser. B 103, 2013) generated all snarks on up to 36 vertices and tested these conjectures on them. Section 7 of their paper derives cycle-cover bounds from double covers. For colourable cubic graphs (those with a proper 3-edge-colouring) the argument gives the bound $4m/3$, and the authors conjecture (Conjecture 7.4) that $4m/3 + o(m)$ holds for all snarks. This mission formalizes the colourable bound and the chain of statements behind it.

Setting

All graphs are finite and simple. A graph is cubic if every vertex has degree 3. It is colourable if its edges can be coloured with three colours so that edges sharing a vertex receive different colours.

A cycle is a 2-regular connected graph. Inside a graph $G$ a cycle is recorded by its edge set $C = \{v_1v_2, \dots, v_{\ell-1}v_\ell, v_\ell v_1\}$, with $v_1, \dots, v_\ell$ distinct and $\ell \ge 3$; its length is $|C| = \ell$. A 2-regular subgraph of $G$ is an edge set $D$ such that every vertex lies on none or exactly two edges of $D$: a union of vertex-disjoint cycles, possibly empty and not necessarily spanning. A 2-factor is a spanning 2-regular subgraph. An even subgraph is an edge set $S$ such that every vertex lies on an even number of edges of $S$.

A cycle double cover of $G$ is a multiset of cycles such that every edge lies in exactly two of them. It is a $k$-CDC if the cycles can be coloured with $k$ colours so that cycles sharing an edge get different colours. Each colour class is then an even subgraph, and following the paper the $k$-CDC is written as a family $D_0, \dots, D_{k-1}$ of even subgraphs with every edge in exactly two of them, counted with multiplicity.

A cycle cover of $G$ is a set $\mathcal F$ of cycles of $G$ such that every edge lies in at least one of them, and its length is $\ell(\mathcal F) = \sum_{C \in \mathcal F} |C|$. Throughout, $m$ denotes the number of edges of $G$.

Formalization targets

Goal: the $4m/3$ bound (§7, p. 24)

For every colourable cubic graph $G$ with $m$ edges there is a cycle cover $\mathcal F$ with

$$\ell(\mathcal F) \le \frac{4m}{3}.$$

Equivalently, the shortest cycle cover of $G$ has length at most $4m/3$.

Milestones

1. Cycle decompositions (§5, p. 15). An edge set $S$ is an even subgraph of $G$ if and only if it is the union of pairwise edge-disjoint cycles of $G$.
2. Proposition 5.3 (p. 15). If $G$ is a colourable cubic graph and $D$ is any 2-regular subgraph of $G$, then $G$ has a 4-CDC $(D_0, D_1, D_2, D_3)$ with $D_0 = D$.
3. Lemma 7.2 (p. 24). If a cubic graph $G$ has a 2-regular subgraph $C$ and a CDC $\mathcal D$ with $C \in \mathcal D$, then $G$ has a cycle cover $\mathcal F$ with

$$\ell(\mathcal F) \le 2m - |C|.$$

Significance

The bound $4m/3$ is far below the Alon–Tarsi bound $7m/5$ and is attained up to lower-order terms on the snarks the paper enumerates (Corollary 7.3, which rests on a computer search and is not part of this mission). It isolates the colourable case of Conjecture 7.4, so any proof of that conjecture must at least reproduce it. Proposition 5.3 is a strong form of the Strong Cycle Double Cover Conjecture for colourable cubic graphs: every 2-regular subgraph, not only every cycle, is a colour class of a 4-CDC. Lemma 7.2 is the general device that turns a double cover containing a long 2-regular subgraph into a short cycle cover; the paper applies it again with long cycles of snarks.

On the formal side, none of these objects exists in Mathlib or on the platform: there is no cycle double cover, no cycle cover, and no decomposition of even graphs into cycles (Veblen's theorem). Mathlib has walks, cycles as walks (Walk.IsCycle), Eulerian trails and the predicate IsCycles, but the step from an even edge set to a family of edge-disjoint cycles is missing. The results of this mission are all proved in the paper or classical; none has a machine-checked proof.

Difficulty

The arithmetic of the goal is immediate once the pieces exist: a 3-edge-colouring of a cubic graph on $n$ vertices consists of three perfect matchings, two of which form a 2-factor with $n = 2m/3$ edges, and $2m - 2m/3 = 4m/3$. The work lies elsewhere.

First, Veblen's theorem must be formalized: an even edge set is a union of edge-disjoint cycles. This requires extracting a cycle (a walk with no repeated vertex) from a nonempty even edge set and inducting on the number of edges; the bookkeeping between walks, their edge lists and finite edge sets is where formal proofs of this kind spend their effort. Lemma 7.2 needs it, because the colour classes of a CDC are even subgraphs, while a cycle cover consists of cycles.

Second, Proposition 5.3 needs the passage from a proper 3-edge-colouring (a colouring of the line graph) to three perfect matchings and to the three 2-factors formed by pairs of colours, and then a parity check that the symmetric differences with $D$ are even and cover every edge exactly twice. A tempting shortcut fails: the three pairwise unions of colour classes already form a 3-CDC, but a prescribed 2-regular subgraph $D$ need not be one of its classes.

Formalization scope

Graphs are SimpleGraph V on a finite type V with decidable equality and decidable adjacency. Cubic is G.IsRegularOfDegree 3. Colourable is G.lineGraph.Colorable 3, a proper vertex colouring of the line graph, never a vertex colouring of G. Edges are Sym2 V, and every subgraph is recorded by its finite edge set. A cycle is the edge set of a closed walk satisfying Walk.IsCycle, of length its number of edges. A $k$-CDC is a function Fin k → Finset (Sym2 V) of even edge sets with every edge of G in exactly two indices, so repeated and empty classes count correctly. A cycle cover is a Finset of cycles covering every edge, of length ∑ C ∈ F, C.card.

"The shortest cycle cover has length at most $X$" is stated as "some cycle cover has length at most $X$"; the two agree because a finite graph has finitely many cycle covers. Bounds are kept in $\mathbb N$ without subtraction or division: the goal is $3\,\ell(\mathcal F) \le 4m$, and Lemma 7.2 is $\ell(\mathcal F) + |C| \le 2m$. Lemma 7.2 is stated for a CDC given as a family of even subgraphs, the form in which the paper applies it (with $C$ a 2-factor that is a colour class of a 4-CDC); a CDC of single cycles is a special case. The cubic hypothesis of Lemma 7.2 is kept as printed although the argument does not use it.

The bound becomes trivial if a "cycle" is weakened to an even edge set or to the edge set of a closed walk, since then the single set $E(G)$ is a cover of length $m \le 4m/3$. The cycles here are genuine cycles of G.

Out of scope: Corollary 7.3 (the cycle-cover lengths of all snarks on at most 36 vertices) and every other statement resting on the exhaustive enumeration, Conjectures 7.1 and 7.4, and the Strong Cycle Double Cover material of §5.1 and §6.

Reusable infrastructure: cycles as edge sets, even subgraphs, $k$-CDCs, cycle covers and Veblen's theorem are general graph-theoretic objects, useful well beyond this paper (for flows, the Cycle Double Cover Conjecture, and Eulerian subgraph arguments). Proofs of Veblen's theorem and of the passage from a 3-edge-colouring to perfect matchings are particularly welcome.

Selected references

• G. Brinkmann, J. Goedgebeur, J. Hägglund, K. Markström, Generation and properties of snarks, arXiv:1206.6690v3, 2013; J. Combin. Theory Ser. B 103 (2013). https://arxiv.org/abs/1206.6690
• N. Alon, M. Tarsi, Covering multigraphs by simple circuits, SIAM J. Algebraic Discrete Methods 6 (1985), no. 3, 345–350; MR 791163. Cited as [2] in https://arxiv.org/abs/1206.6690

Motivation

Excluding a fixed clique should force independent sets larger than those guaranteed by average degree alone. The source asks for the full logarithmic improvement uniformly across graph sizes. The source is OpenAI's September 2026 manuscript.

Setting

An independent set contains no adjacent pair. Write $n$ for the number of vertices, $d=2|E|/n$ for average degree, and $α(G)$ for the largest independent-set size. A graph is clique-free of order $r$ when it contains no $r$ pairwise adjacent vertices.

Formalization targets

$$\forall r\ge4\ \exists c_r>0:\quad \alpha(G)\ge c_r\frac{n\log d}{d}\qquad(d\ge2,\ G\text{ is }K_r\text{-free}).$$

For every natural number r ≥ 4, there is a real constant c > 0 such that the following holds for every finite simple graph G on a vertex type V (a Fintype). Here the average degree d(G) is defined as 2|E(G)|/|V|, twice the number of edges divided by the number of vertices (as a real number). If G contains no clique of size r (it is r-clique-free) and d(G) ≥ 2, then the independence number α(G), the maximum size of an independent set, satisfies α(G) ≥ c · |V| · log(d(G)) / d(G), where log is the natural logarithm of real numbers. The constant c may depend on r but not on G.

The goal is OAI.CliqueFreeLog.logarithmic_independence_bound.

Significance

The bound improves the general inverse-degree scale by a factor of natural logarithmic size. The constant may depend on the forbidden clique but must work for every input graph. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

The condition forbids ordinary cliques rather than imposing bounded complexity on every neighborhood. Estimates using maximum degree alone do not establish the stated average-degree bound.

Formalization scope

The representation is Mathlib SimpleGraph on a finite type. Real.log is the natural logarithm and the hypothesis $d\ge2$ keeps its argument and the denominator positive. The empty graph is excluded by that hypothesis.

The shared definitions are supplied by CliqueFreeLog. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, A logarithmic independence bound for clique-free graphs, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

A spanning subgraph in which every vertex has degree two may split into several cycles. Barnette’s question asks when planarity, bipartiteness, and connectivity force those vertices onto one cycle. The source is OpenAI's September 2026 manuscript.

Setting

A cubic graph has degree three at every vertex. A bipartite graph has two vertex classes with every edge crossing between them. A Hamiltonian cycle visits all vertices exactly once before returning to its starting point. Planarity is represented by a drawing using injective continuous edge arcs in the real plane.

Formalization targets

$$G\text{ finite, simple, cubic, bipartite, planar, and 3-vertex-connected}\ \Longrightarrow\ G\text{ has a Hamiltonian cycle}.$$

Every finite simple graph with decidable vertex equality and adjacency has a Hamiltonian cycle if each vertex has degree three, the vertices can be partitioned into two classes with every edge joining different classes, the graph is planar, and it is three-vertex-connected. Here planarity means that vertices can be placed at distinct points of the real plane and edges drawn as injective continuous arcs whose interiors contain no vertices and whose interiors are disjoint for distinct undirected edges; reversing an edge reverses its arc. Three-vertex-connectivity means that the graph has at least four vertices and remains connected after deletion of any set of at most two vertices. The conclusion is the existence of one closed cycle visiting every vertex exactly once before returning to its starting vertex.

The goal is OAI.Barnette.main.

Significance

A proof would turn the source’s Hamiltonicity claim into a result available for arbitrary finite graphs satisfying these exact hypotheses. It would also provide a reusable bridge between geometric embeddings and combinatorial walks. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Degree constraints do not guarantee that a spanning cycle cover is connected. The target requires a single cycle and must handle unrestricted face sizes, so verifying local degree conditions is insufficient.

Formalization scope

The published goal unfolds MainStatement. Three-vertex-connectivity requires at least four vertices and connectedness after deletion of any set of at most two vertices. The Hamiltonian object is a closed graph walk satisfying the cycle and vertex-coverage conditions. Stronger edge-avoidance conclusions from the paper are not attached as targets.

The shared definitions are supplied by BarnetteHamiltonian. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Paired states and Hamiltonian cycles in cubic bipartite planar graphs, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Graph homomorphism inequalities compare the frequency of a fixed pattern with what edge density predicts. The mission asks for one finite host graph violating the proposed bound for a specified bipartite pattern. The source manuscript presents the surrounding research claim.

Setting

The pattern H is the incidence graph between thirteen points and twenty-two explicitly listed triples, giving thirty-five vertices and sixty-six edges. Homomorphism density counts all edge-preserving maps, including noninjective maps, divided by the number of all vertex maps.

Formalization target

Construct a positive-size finite simple host G with at least one edge such that

$$t(H,G)<p(G)^{66},\qquad p(G)=\frac{2|E(G)|}{|V(G)|^2}.$$

The selected formal target is OAI.SidorenkoCounterexample.main.

Significance and status

The counterexample uses the exact supplied pattern rather than an unspecified bipartite graph. A finite host makes the density comparison an ordinary finite counting statement. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

The required strict inequality concerns all homomorphisms, not only embeddings. The host must have an edge so the assertion cannot be replaced by a zero-density degeneracy.

Formalization scope

H is built from the published table of twenty-two triples. Hosts use Fin size, and both graph counts and real density normalizations are fixed. The manuscript’s forcing-conjecture consequence is not an attached formal target.

Selected references

• OpenAI, A counterexample to Sidorenko's conjecture, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

List coloring permits each vertex to have different allowable colors. The mission asks whether the size of the largest clique minor still controls the required list size up to a universal linear factor. The source manuscript presents the surrounding research claim.

Setting

A clique minor of order t is represented by disjoint connected vertex sets, with an edge between every pair. The Hadwiger number h(G) is the largest possible t. The list chromatic number is the least k for which every assignment of at least k colors per vertex admits a proper selection.

Formalization target

Prove one integer C≥1 works for every finite nonempty simple graph:

$$\chi_{list}(G)\le C\,h(G).$$

The constant is chosen before the graph, the vertex type and all color lists.

The selected formal target is OAI.LinearListHadwiger.main_theorem.

Significance and status

The assertion controls list coloring rather than only a common-color-set chromatic number. It is a linear-factor statement, without coefficient-one optimality. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

A coloring from one chosen palette need not respect independently assigned lists. The proof must cover arbitrary color types and list assignments.

Formalization scope

The definitions use finite graph vertex types, arbitrary finite color sets, induced-subgraph connectivity and natural-number infima/suprema. Nonemptiness of the vertex type is explicit. Only the main inequality and its definition block are attached.

Selected references

• OpenAI, A linear list-coloring bound in terms of the Hadwiger number, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

A planar prime walk can go around a gap that would block a walk on a line. The Gaussian moat problem therefore asks for an obstruction to every possible bounded-step route through distinct Gaussian primes. The source manuscript presents the surrounding research claim.

Setting

A Gaussian prime is an irreducible element of ℤ[i]. For D ∈ ℝ, two distinct primes are adjacent when their Euclidean distance is at most D. A component contains every prime reachable by a finite path.

Formalization target

Prove the conjunction

$$\text{no injective infinite D-step prime walk exists},\qquad\forall D\;\exists B\;\forall p,\ |\operatorname{component}_D(p)|\le B.$$

The second clause also bounds the length of every finite injective D-step prime chain by B and asserts component finiteness.

The selected formal target is OAI.GaussianMoat.fullMain.

Significance and status

The same B must work for every starting prime at a fixed step bound. The theorem makes no numerical claim about this bound. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Showing that each component is finite does not give a uniform bound across starting points. Every route in two dimensions and primes on the axes remain within the quantification.

Formalization scope

The formal graph uses Mathlib Gaussian integers and complex Euclidean distance. Step bounds range over all real numbers. MainEndpoint and UniformEndpoint are both mandatory clauses of fullMain. Only that published target and its definitions are supplied.

Selected references

• OpenAI, Bounded-Step Walks on Gaussian Primes, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

How efficiently can the edges of a graph be split into cycles? Some single edges must be allowed, since a forest has no cycles at all, and a tree on $n$ vertices already needs $n-1$ single-edge parts. The Erdős–Gallai cycle decomposition conjecture asserts that this is essentially the only obstruction: every graph on $n$ vertices can have its edge set partitioned into $O(n)$ simple cycles and single edges. Equivalently, every graph with all degrees even partitions into $O(n)$ cycles. The problem is a basic question about edge decompositions, and the partial bounds $O(n\log n)$, $O(n\log\log n)$ and $O(n\log^*n)$ trace several decades of progress on it.

This mission asks for a formal proof of the linear bound, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1966 — Erdős, Goodman and Pósa record the problem and an $O(n\log n)$ bound, distinguishing covers from edge-disjoint partitions (Canad. J. Math. 1966).
• 1968 — Lovász: every graph on $n$ vertices partitions into at most $\lfloor n/2\rfloor$ paths and cycles (On covering of graphs, 1968).
• 1985 — Pyber shows that $n-1$ cycles and edges suffice to cover (not partition) every graph (Combinatorica 1985).
• 2014 — Conlon, Fox and Sudakov prove $O(n\log\log n)$ in general and linear bounds for random graphs and graphs of linear minimum degree (RSA 2014).
• 2015–2021 — Asymptotically sharp counts for random graphs (Korándi–Krivelevich–Sudakov, CPC 2015); $(3/2+\delta)n$ for dense graphs (Girão–Granet–Kühn–Osthus, J. LMS 2021).
• 2024 — Bucić and Montgomery prove $O(n\log^*n)$ (Adv. Math. 2024).
• 2025 — Akbari, Aloni, Beikmohammadi and Clow prove $n-1$ for maximum degree at most four (arXiv:2509.01901).
• September 2026 — The OpenAI preprint claims the linear bound (Theorem 1.1, p. 1).

Setting

A finite simple graph $G$ has vertex set of size $n$ and edge set $E(G)$ of unordered pairs of distinct vertices. A cycle is a closed walk of length at least $3$ with no repeated vertices except the endpoints; its edge set is the set of edges it traverses. A cycle-and-edge decomposition of $G$ into $k$ parts is a family $E_1,\dots,E_k$ of pairwise disjoint subsets of $E(G)$ with union $E(G)$, where each $E_i$ is either the edge set of a cycle of $G$ or a single edge of $G$. Parts may share vertices; isolated vertices need not be covered; for an edgeless graph $k=0$ is allowed.

Formalization targets

Goal: Theorem 1.1 (p. 1)

There is an absolute constant $C>0$ such that for every $n$ and every simple graph $G$ on $n$ vertices,

$$G\ \text{has a cycle-and-edge decomposition into at most } Cn \text{ parts}.$$

The value of $C$ is left unspecified, which keeps the goal stable under future improvements of the constant (the best possible constant is at least $3/2$, by complete bipartite examples).

Significance

The result itself. The order $n$ is optimal (trees). The theorem implies that every Eulerian graph (all degrees even) partitions into $O(n)$ cycles (Corollary 1.2, p. 2), and via known equivalences it gives the sharp $\Delta(G)/2+\delta n$ cycle bound for Eulerian graphs satisfying a large-cut condition. It removes the last iterated-logarithm loss from the Bucić–Montgomery bound.

Formalizing it. The statement uses only Mathlib's SimpleGraph.Walk.IsCycle and edge sets, so it is a clean combinatorial target. A complete development needs Lovász's path-cycle decomposition theorem, the Aharoni–Haxell hypergraph matching theorem, expansion and routing lemmas, and binomial tail bounds; all are reusable in extremal graph theory. No machine-checked proof of any $o(n\log n)$ bound is known.

Difficulty

Covering is easy (Pyber's $n-1$ bound), but a cover does not yield a partition: deleting repeated edges can break cycles into many paths. For partitions, the standard strategy decomposes the graph into expanding pieces at a sequence of scales, and paying a cost proportional to the full order at every scale accumulates a factor from the number of scales — this is where the $\log\log n$ and $\log^*n$ losses come from. The preprint (Introduction, pp. 2–3) charges the work on a prefix of scales to a single expanding layer and saves a fixed fraction of vertices by identifying pairs, then lifts quotient cycles back with reserved edge-disjoint routes (Lemma 3.1, p. 5); keeping a separate assignment for each original edge throughout is what makes the induction close.

Formalization scope

• Graphs are SimpleGraph (Fin n) for arbitrary n (including 0 and edgeless graphs).
• CycleOrSingleEdge G s: either $s$ is p.edgeSet for some p : G.Walk v v with p.IsCycle (Mathlib cycles have length at least $3$), or $s=\{e\}$ for an edge $e\in G$.
• EdgeDecomposition G k: parts indexed by Fin k, each a cycle or single edge, pairwise disjoint, with union G.edgeSet.
• MainStatement: $\exists C>0,\ \forall n\ \forall G,\ \exists k,$ EdgeDecomposition G k $\wedge\ k\le Cn$.
• Trivializations are ruled out: parts must be nonempty edge sets of the required shape and must exactly partition the edge set, so the count $k$ is a genuine count.

Selected references

• OpenAI, A linear cycle-and-edge decomposition of every graph, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-linear-cycle-and-edge-decomposition-of-every-graph-September-24-2026/main.pdf
• P. Erdős, A. W. Goodman, L. Pósa, The representation of a graph by set intersections, Canad. J. Math. 18 (1966). https://doi.org/10.4153/CJM-1966-014-3
• L. Lovász, On covering of graphs, Theory of Graphs (Proc. Colloq. Tihany, 1966), 1968.
• L. Pyber, An Erdős–Gallai conjecture, Combinatorica 5 (1985). https://doi.org/10.1007/BF02579444
• D. Conlon, J. Fox, B. Sudakov, Cycle packing, Random Structures Algorithms (2014). https://doi.org/10.1002/rsa.20574
• D. Korándi, M. Krivelevich, B. Sudakov, Decomposing random graphs into few cycles and edges, Combin. Probab. Comput. (2015). https://doi.org/10.1017/S0963548314000844
• A. Girão, B. Granet, D. Kühn, D. Osthus, Path and cycle decompositions of dense graphs, J. London Math. Soc. (2021). https://doi.org/10.1112/jlms.12455
• M. Bucić, R. Montgomery, Towards the Erdős–Gallai cycle decomposition conjecture, Adv. Math. (2024). https://doi.org/10.1016/j.aim.2023.109434
• R. Aharoni, P. Haxell, Hall's theorem for hypergraphs, J. Graph Theory 35 (2000). https://doi.org/10.1002/1097-0118(200010)35:2<83::AID-JGT2>3.0.CO;2-V
• S. Akbari, J. Aloni, A. Beikmohammadi, A. Clow, Tight bounds for cycle-edge decompositions and covers, arXiv:2509.01901 (2025). https://arxiv.org/abs/2509.01901v2

Motivation

When does the Erdős–Rényi random graph $G(n,p)$ contain a copy of a prescribed graph $H$? A necessary condition is visible from first moments: if some subgraph $F\subseteq H$ has expected copy count below a constant, then $H$ is unlikely to appear. Kahn and Kalai conjectured in 2007 that this elementary obstruction determines the containment threshold up to a logarithmic factor, uniformly over all target graphs, including spanning ones such as perfect matchings, Hamilton cycles or cubes (CPC 2007). Their abstract conjecture for general increasing families (the "first" conjecture) was proved by Park and Pham; the graph-specific "second" conjecture compares the threshold with the smaller, purely subgraph-count-based graph expectation threshold, and is not implied by the abstract theorem.

This mission asks for a formal proof of the second Kahn–Kalai conjecture with explicit constants, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1960–1981 — Erdős and Rényi's evolution of random graphs (1960) and perfect matchings (1966); Bollobás determines thresholds for fixed subgraphs (Math. Proc. Camb. Phil. Soc. 1981).
• 2007 — Kahn and Kalai state both conjectures (CPC 2007).
• 2010 — Talagrand introduces fractional expectation thresholds (STOC 2010).
• 2021 — Frankston, Kahn, Narayanan and Park prove $p_c=O(q_f\log\ell)$ (Annals 2021), building on the sunflower methods of Alweiss–Lovett–Wu–Zhang (Annals 2021).
• 2022–2025 — Mossel, Niles-Weed, Sun and Zadik obtain a single-log bound for a modified graph threshold (arXiv:2209.03326) and a Bayesian proof of the spread lemma (RSA 2025).
• 2024 — Park and Pham prove the abstract Kahn–Kalai conjecture (JAMS 2024).
• 2025 — Dubroff, Kahn and Park prove $p_c=O(p_E\log^3n)$ and special cases (arXiv:2508.14269, arXiv:2510.02005).
• 2026 — Tran reduces the loss to $O(\log^2(2e(H)))$ and proves the conjecture for trees and other classes (arXiv:2609.20546); the OpenAI preprint claims the general case (Theorem 1.1, p. 1).

Setting

For finite simple graphs $G,F$ let $N(G,F)$ be the number of subgraphs of $G$ isomorphic to $F$ (ordinary, non-induced copies). $G(n,p)$ is the random graph on $[n]$ with each of the $\binom n2$ edges present independently with probability $p$. For a graph $H$ with at least one edge and at most $n$ vertices,

$$p_c(n,H)=\inf\{p\in[0,1]:\ \Pr[N(G(n,p),H)>0]\ge\tfrac12\},$$ $$p_E(n,H)=\inf\{p\in[0,1]:\ \mathbb E\,N(G(n,p),F)\ge\tfrac12\ \text{for every subgraph }F\subseteq H\}.$$

The first is the containment threshold, the second the graph expectation threshold; always $p_E\le p_c$. Write $h=e(H)$ for the number of edges.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every $n\ge2$ and every finite simple graph $H$ with $h\ge1$ edges and at most $n$ vertices,

$$p_c(n,H)\ \le\ \min\bigl\{1,\ 2048\,e^{50}\,p_E(n,H)\,(1+\log_2 h)\bigr\},\qquad p_c(n,H)\ \le\ 6144\,e^{50}\,p_E(n,H)\log_2 n .$$

The constants are explicit and universal; $H$ may vary with $n$.

Significance

The result itself. The bound says that, up to a universal constant times $\log h$, the only obstruction to containing $H$ is a subgraph with too few expected copies. The logarithm cannot be removed: for a perfect matching $p_E=\Theta(1/n)$ while $p_c=\Theta(\log n/n)$, because isolated vertices must disappear. This settles the problem left by the abstract Park–Pham theorem, whose bound is in terms of the possibly larger integral expectation threshold of the family of graphs containing $H$.

Formalizing it. Both thresholds are finite, explicit optimization problems over Bernoulli product measures on the edges of $K_n$, so the statement is fully elementary. Mathlib has SimpleGraph.copyCount but no random-graph or threshold theory; the spread-family resampling lemma and the tree covering theorem would be reusable for other threshold results (Park–Pham, Frankston–Kahn–Narayanan–Park). No machine-checked proof of any Kahn–Kalai-type theorem is known.

Difficulty

The abstract theorem compares $p_c$ with the integral expectation threshold of the family $\mathcal F_H$ of edge sets containing a copy of $H$, and covers of $\mathcal F_H$ may be much cheaper than the copies of a single subgraph, so it does not give a bound in terms of $p_E$. Previous graph-specific approaches lost extra logarithms because each conditional extension step paid the sampling cost again. The preprint (Section 1.2, pp. 3) builds a tree of nested subgraph extensions with geometrically growing, pairwise disjoint labels along each path, and must reuse one random set at every level of the tree while keeping the spread property under conditioning (Theorem 3.1, p. 6).

Formalization scope

• $G(n,p)$ is encoded as a Bernoulli product weight on Finset (Edge n), where Edge n is the type of non-diagonal Sym2 (Fin n); expectations and probabilities are finite sums, defined for every real $p$ but used only on $[0,1]$.
• expectedCopies and containmentProbability use Mathlib's copyCount of the graph built from the edge set; both are ordinary (non-induced) copies.
• criticalThreshold and expectationThreshold are sInf over $p\in[0,1]$; the sets are nonempty (they contain $p=1$ when $H$ has at most $n$ vertices), so the infima are the true thresholds. The expectation constraint ranges over all H.Subgraphs, including subgraphs with isolated vertices, whose constraints are automatically satisfied.
• $H$ is a SimpleGraph on an arbitrary finite type V with Fintype.card V ≤ n, 2 ≤ n and at least one edge; logTwo is $\log x/\log 2$.
• The constants $2048e^{50}$ and $6144e^{50}$ are hard-coded, as in the source.

Selected references

• OpenAI, The second Kahn–Kalai conjecture, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-second-Kahn-Kalai-conjecture-September-24-2026/paper.pdf
• J. Kahn, G. Kalai, Thresholds and expectation thresholds, Combin. Probab. Comput. 16 (2007), 495–502. https://doi.org/10.1017/S0963548307008474
• J. Park, H. T. Pham, A proof of the Kahn–Kalai conjecture, J. Amer. Math. Soc. 37 (2024), 235–243. https://doi.org/10.1090/jams/1028
• K. Frankston, J. Kahn, B. Narayanan, J. Park, Thresholds versus fractional expectation-thresholds, Ann. of Math. 194 (2021), 475–495. https://doi.org/10.4007/annals.2021.194.2.2
• R. Alweiss, S. Lovett, K. Wu, J. Zhang, Improved bounds for the sunflower lemma, Ann. of Math. 194 (2021), 795–815. https://doi.org/10.4007/annals.2021.194.3.5
• M. Talagrand, Are many small sets explicitly small?, STOC 2010. https://doi.org/10.1145/1806689.1806693
• E. Mossel, J. Niles-Weed, N. Sun, I. Zadik, On the second Kahn–Kalai conjecture, arXiv:2209.03326 (2022). https://arxiv.org/abs/2209.03326v1
• E. Mossel, J. Niles-Weed, N. Sun, I. Zadik, A Bayesian proof of the spread lemma, Random Structures Algorithms 66 (2025), e70008. https://doi.org/10.1002/rsa.70008
• Q. Dubroff, J. Kahn, J. Park, On the "second" Kahn–Kalai conjecture, arXiv:2508.14269 (2025). https://arxiv.org/abs/2508.14269v1
• T. Tran, Fractional expectation thresholds and the "second" Kahn–Kalai conjecture, arXiv:2609.20546 (2026). https://arxiv.org/abs/2609.20546v2
• B. Bollobás, Threshold functions for small subgraphs, Math. Proc. Cambridge Philos. Soc. 90 (1981), 197–206. https://doi.org/10.1017/S0305004100058655