Graph Theory

Motivation

A perfect graph is one whose coloring problem has a particularly sharp answer on every induced subgraph: the fewest colors needed is exactly the size of its largest clique. This makes a local obstruction, a clique, certify the optimum number of colors throughout the graph. Claude Berge proposed in 1961 that perfection could be recognized by the absence of two kinds of induced odd cycles, one in the graph and one in its complement. The equivalence became known as the strong perfect graph conjecture. Chudnovsky, Robertson, Seymour, and Thomas proved it in their 2006 paper, which also proves a structural decomposition of the graphs under study. The paper connects this question to graph coloring, Shannon capacity, and linear and integer programming. Chudnovsky et al., pp. 51–54

The earlier complement theorem was proved by Lovász in 1972 and appears as Theorem 1.1 in the paper. The strong conjecture remained unresolved for roughly four decades; the authors' Theorem 1.2 settles it. Their proof places a second result, Theorem 1.3, beside the equivalence: a graph with no forbidden odd hole or antihole must either belong to a basic class or admit one of several specified decompositions. The graph classes and decompositions are therefore part of the statement of the route to the main result, not merely vocabulary for a proof. Chudnovsky et al., pp. 52–56

Setting

All graphs here are finite and simple. The complement $\overline G$ has the same vertices as $G$, and two distinct vertices are adjacent in $\overline G$ exactly when they are not adjacent in $G$. For a vertex set $X$, the notation $G|X$ means the induced subgraph on $X$. A clique is a set of pairwise adjacent vertices. Its largest possible size in a graph $H$ is $\omega(H)$, and $\chi(H)$ is the minimum number of colors in a proper vertex coloring of $H$.

A hole is an induced cycle of length at least four. An antihole of $G$ is a hole in $\overline G$. A graph is Berge if every hole and antihole has even length. Thus a perfect graph requires $\chi(G|X)=\omega(G|X)$ for every $X\subseteq V(G)$, while a Berge graph satisfies a restriction on induced cycles in both $G$ and $\overline G$. “Induced” matters: a cycle with a chord is not a hole. Chudnovsky et al., pp. 51–52

For the structural milestones, a basic graph is a bipartite graph, the complement of one, a line graph of a bipartite graph, the complement of such a line graph, or a double split graph. The latter consists of paired vertices $a_i,b_i$ and $c_j,d_j$ with the within-pair and between-pair adjacencies specified on pp. 52–53. A proper 2-join partitions the vertices into two sides with two prescribed complete cross-edge blocks, connected-component conditions on both sides, and a special odd-path condition. A proper homogeneous pair is a pair of vertex sets whose outside vertices split into four nonempty adjacency classes. A balanced skew partition has one side disconnected and the other disconnected in the complement, together with parity restrictions on induced paths and antipaths. Chudnovsky et al., pp. 52–54

Formalization targets

Theorem 1.2: perfection and the Berge property

The goal is the exact equivalence for every finite simple graph:

$$G\text{ is perfect}\quad\Longleftrightarrow\quad G\text{ is Berge}.$$

No order bound, chosen graph class, or decomposition hypothesis is attached to the goal. Chudnovsky et al., p. 52, 1.2

Structural and reduction milestones

Theorem 1.1 says that $G$ perfect implies $\overline G$ perfect. Theorem 1.5 says that a minimum imperfect graph, a Berge nonperfect graph with the smallest vertex count among all such graphs, cannot admit a balanced skew partition. Theorem 13.5 says that a recalcitrant graph—a Berge graph with the listed line-graph, double-split, 2-join, homogeneous-pair, and balanced-skew outcomes absent—has $G$ or $\overline G$ bipartite. Theorem 1.3 states the decomposition conclusion:

$$G\text{ Berge}\Longrightarrow G\text{ basic}\ \lor\ G\text{ or }\overline G\text{ has a proper 2-join}\ \lor\ G\text{ has a proper homogeneous pair}\ \lor\ G\text{ has a balanced skew partition}.$$

The milestone order records the two reduction results, the later structural capstone, and the decomposition statement it yields. The paper's other section results that establish 13.5 are posed in the remaining missions of this series. Chudnovsky et al., pp. 52, 54–55, 154

Significance

Theorem 1.2 gives a forbidden-induced-subgraph characterization of perfect graphs. Its cycle condition is intrinsic to the graph and its complement; its coloring condition quantifies over every induced subgraph. Together with Theorem 1.3, it ties a numerical property of colorings to explicit graph structures and separations. The complement theorem and the exclusion of decompositions for a minimum imperfect graph explain why the structural alternatives have the strength needed for the equivalence. Chudnovsky et al., pp. 52–56

The mathematical theorem was proved in the cited paper. This mission poses its statements in Lean and seeks machine-checked proofs; the draft theorem declarations are open targets. The definition layer is useful beyond this mission: induced holes, Berge graphs, perfection, balanced skew partitions, and the decomposition predicates can support the later missions without changing what each source statement means. No machine-checked proof of these draft targets is claimed here.

Difficulty

The forward implication can be tested on induced odd cycles, but that observation does not settle the converse. Excluding odd holes and antiholes does not give an immediate coloring of an arbitrary induced subgraph. The paper instead establishes a detailed account of what a Berge graph can look like when it is not in a basic class. The delicate point in turning this account into Theorem 1.2 is that each decomposition outcome must be incompatible with a minimum imperfect graph. Ordinary skew partitions are too broad for that role; the balanced parity conditions are part of the statement. The structural conclusion 13.5 collects restrictions established across many later sections, so formalizing its prerequisites is a substantial graph-theoretic task. Chudnovsky et al., pp. 52–56, 154

Formalization scope

Lean uses SimpleGraph V with finite vertices, decidable vertex equality, and the Mathlib complement, induced subgraph, chromatic number, clique number, bipartiteness, and line graph. A hole is a list in cyclic order whose adjacency relation agrees exactly with the cycle edges; a path is likewise listed in one orientation with exactly its consecutive edges. Antiholes and antipaths use the complement graph. The empty vertex set is connected, matching p. 54. The double split partition is encoded by an equivalence from the four indexed parts to the whole vertex type, making disjointness and coverage explicit. A minimum imperfect graph is globally minimal by vertex count, among all finite Berge graphs.

No hypothesis beyond the paper's finite, simple graph convention is added to the goal or numbered milestones. In particular, “Berge” includes holes in both $G$ and $\overline G$; “perfect” ranges over every induced subgraph; and the complement occurs only in those decomposition outcomes where the paper places it. A non-induced cycle or a missing complement condition would make the formal target different. The definitions and Lean proofs of the graph classes, their boundary cases, and the structural milestones are welcome contributions. Later missions pose the paper's intervening numbered results rather than duplicating them here.

Selected references

• Maria Chudnovsky, Neil Robertson, Paul Seymour, and Robin Thomas, The strong perfect graph theorem, Annals of Mathematics 164 (2006), 51–229. DOI 10.4007/annals.2006.164.51.

Motivation

List colouring asks for a proper colouring of a graph in which every vertex takes its colour from its own prescribed list. A graph is $k$-choosable if such a colouring exists for every assignment of lists of size $k$. Choosability is harder to guarantee than colourability: planar triangle-free graphs are 3-colourable (Grötzsch) but not all are 3-choosable (Voigt, 1995), and planar graphs are 4-colourable but not all 4-choosable (Voigt, 1993), while every planar graph is 5-choosable (Thomassen, 1994).

A long line of work asks which forbidden cycle lengths make a planar graph 3-colourable or 3-choosable, motivated by Steinberg's conjecture (every planar graph without cycles of lengths 4 and 5 is 3-colourable), which was disproved by Cohen-Addad, Hebdige, Král', Li and Salgado (arXiv:1604.05108).

Timeline.

• 1993–1995: Voigt constructs planar graphs that are not 4-choosable, and planar triangle-free graphs that are not 3-choosable.
• 1994: Thomassen proves that every planar graph is 5-choosable; in 1995 he proves that planar graphs of girth at least 5 (no cycles of lengths 3 and 4) are 3-choosable.
• 1996: Borodin proves that planar graphs without cycles of lengths 4 to 9 are 3-colourable; the proof also gives 3-choosability.
• 2005: Borodin, Glebov, Raspaud and Salavatipour prove 3-colourability when cycles of lengths 4 to 7 are forbidden.
• 2007: Voigt constructs a planar graph without cycles of lengths 4 and 5 that is not 3-choosable, so the list version of Steinberg's conjecture fails.
• 2013: Borodin's survey records as open, for more than fifteen years, whether excluding cycles of lengths 4 to 8 suffices for 3-choosability.
• 2018: Dvořák and Postle (arXiv:1508.03437, J. Combin. Theory Ser. B) answer the question positively. To do so they introduce correspondence colouring, now usually called DP-colouring, which has since become a standard tool.

Setting

All graphs are finite and simple. A list assignment $L$ gives each vertex $v$ a finite set $L(v)$ of colours; an $L$-coloring is a map $\varphi$ with $\varphi(v)\in L(v)$ for all $v$ and $\varphi(u)\ne\varphi(v)$ on every edge $uv$. $G$ is $k$-choosable if an $L$-coloring exists whenever $|L(v)|=k$ for all $v$.

Write $[k]$ for a set of $k$ colours. A $k$-correspondence assignment $C$ assigns to each edge $uv$ a partial matching $C_{uv}$ between $\{u\}\times[k]$ and $\{v\}\times[k]$. A $C$-coloring is a map $\varphi:V(G)\to[k]$ such that $(u,\varphi(u))$ and $(v,\varphi(v))$ are not matched in $C_{uv}$ for any edge $uv$. Ordinary colouring is the case where every $C_{uv}$ matches equal colours.

For a closed walk $W=v_0v_1\dots v_m$ ($v_m=v_0$), $C$ is inconsistent on $W$ if there are colours $c_0,\dots,c_m$ with $(v_i,c_i)(v_{i+1},c_{i+1})\in E(C_{v_iv_{i+1}})$ for every $i<m$ and $c_0\ne c_m$; otherwise it is consistent on $W$. $C$ is consistent if it is consistent on every closed walk. An edge $uv$ is straight if $C_{uv}$ only matches equal colours, and full if $C_{uv}$ is a perfect matching.

A plane graph is a graph with a fixed drawing in the plane without crossings; its faces are the connected components of the complement of the drawing, and a vertex is incident with a face if it lies in the face's closure. A graph is planar if it has such a drawing.

Formalization targets

Goal: Theorem 1 (p. 3)

$$\text{Every planar graph } G \text{ without cycles of lengths } 4 \text{ to } 8 \text{ is } 3\text{-choosable.}$$

Milestones

• Lemma 5 (p. 6): $G$ is $k$-choosable iff $G$ is $C$-colorable for every consistent $k$-correspondence assignment $C$.
• Lemma 7 (p. 10): if every cycle of a subgraph $H$ has full edges and $C$ is consistent on it, then renaming colours at the vertices of $H$ makes every edge of $H$ straight.
• Lemmas 10, 11, 12 (pp. 14–16): properties of a minimal counterexample to Theorem 8 — dense matchings, full triangles next to degree-three vertices, and every tetrad (a path of four degree-three vertices on a face whose end edges lie in triangles) meets the precoloured set.
• Theorem 8 (p. 11): for a plane graph $G$ without cycles of lengths 4 to 8, a set $S$ with $|S|\le 1$ or $S$ = all vertices of one face, $|S|\le 12$, and a 3-correspondence assignment $C$ consistent on closed walks of length 3, every $C$-coloring of $G[S]$ extends to a $C$-coloring of $G$.
• Theorem 6 (p. 7): every planar graph without cycles of lengths 4 to 8 is $C$-colorable for every 3-correspondence assignment $C$ consistent on every closed walk of length 3.

Theorem 8 implies Theorem 6 ($S=\emptyset$), and Theorem 6 with Lemma 5 implies Theorem 1.

Significance

The result. Theorem 1 settles Borodin's question and is still the best known forbidden-interval result for 3-choosability of planar graphs with triangles allowed. Theorem 6 is a strengthening in the correspondence setting, and Theorem 8, a precolouring-extension statement, is the form used for induction. The broader contribution is correspondence colouring itself: it allows reductions that identify vertices, which list colouring does not, and it has since been developed by Bernshteyn, Kostochka, Pron and many others as DP-colouring.

Formalizing it. The results are proved in the paper; none has a machine-checked proof. Mathlib has no planarity, no list colouring and no correspondence colouring. This mission produces the first formal definitions of $k$-choosability and correspondence colouring on the platform, the equivalence between list colouring and consistent correspondence colouring (Lemma 5), and a formal statement of the planar result, together with the paper's reduction lemmas as independent targets.

Difficulty

Lemma 5 and Lemma 7 are finite combinatorics. The main obstacle is Theorem 8. The natural list-colouring argument by reducible configurations fails: reductions for ordinary colouring identify two vertices, which is meaningless when their lists differ. Correspondence colouring removes that obstruction only when the identification does not create parallel edges or short cycles, and the main reduction (Lemma 12) needs consistency on triangles, which is why Theorem 6 carries that hypothesis. On the formal side, the proof uses planar topology: faces, the open disk bounded by a cycle, 2-connectedness of a minimal counterexample, and a discharging argument over faces that relies on Euler's formula. None of this exists in Mathlib.

Formalization scope

Conventions committed to in the Lean statements:

• Graphs are SimpleGraph V on a Fintype vertex type; the paper's graphs are finite and simple (p. 3).
• $k$-choosability quantifies over an arbitrary colour type α : Type and lists L : V → Finset α of cardinality exactly $k$.
• A $k$-correspondence assignment is a relation M u c v d on V × Fin k × V × Fin k that lives on edges, is symmetric, and is a partial matching. The paper's $[k]=\{1,\dots,k\}$ is Fin k.
• Consistency is defined on Mathlib closed walks G.Walk v v through getVert. The paper's example of Figure 1(a) (p. 5) was checked against this definition by a sorry-free local proof.
• Planarity and plane graphs use straight-line drawings in ℝ × ℝ: injective vertex positions, no vertex on a non-incident edge, and disjoint segments for edges with no common end. These are the clauses of the platform's OPG401.IsPlanar. By Fáry's theorem this is equivalent to planarity for finite simple graphs, and every plane graph has a straight-line drawing with the same faces. Faces are components of the complement of the drawing, incidence is membership in the closure, and the outer face is the unbounded face. Theorem 8 is stated for every drawing and any face, not only the outer one.
• "Renaming on vertices of $X$" between two 3-correspondence assignments is a permutation of $[k]$ at each vertex of $X$, the identity elsewhere. This is exactly the effect of the paper's sequences of single renamings.
• A target (p. 11) has its vertex type in Type. The measure $s(B)$ counts ordered pairs, which gives the same lexicographic order. A minimal counterexample is minimal among all targets of this kind.

Formalizations that would trivialize or change the problem are ruled out:

• a girth bound, which excludes triangles;
• lists drawn from a fixed 3-element palette (3-colourability);
• a planarity surrogate such as an edge bound;
• a correspondence that is not a matching;
• consistency without the closing condition $c_0\ne c_m$;
• consistency on all closed walks in Theorems 6 and 8.

Infrastructure needed and reusable beyond this mission: planar straight-line drawings and their faces (Euler's formula, the Jordan curve theorem for polygons), 2-connectivity and facial cycles, and a DP-colouring library (renaming, consistency, Lemma 5). Contributions to any of these are welcome. So are proofs of Lemma 5 and Lemma 7, which need no topology.

Selected references

• Z. Dvořák, L. Postle, Correspondence coloring and its application to list-coloring planar graphs without cycles of lengths 4 to 8, J. Combin. Theory Ser. B (2018); cited version arXiv:1508.03437v2 (2016). https://arxiv.org/abs/1508.03437
• O. V. Borodin, Colorings of plane graphs: a survey, Discrete Math. 313 (2013) 517–539.
• O. V. Borodin, Structural properties of plane graphs without adjacent triangles and an application to 3-colorings, J. Graph Theory 21 (1996) 183–186.
• O. V. Borodin, A. N. Glebov, A. Raspaud, M. R. Salavatipour, Planar graphs without cycles of length from 4 to 7 are 3-colorable, J. Combin. Theory Ser. B 93 (2005) 303–311.
• V. Cohen-Addad, M. Hebdige, D. Král', Z. Li, E. Salgado, Steinberg's conjecture is false, J. Combin. Theory Ser. B (2017). https://arxiv.org/abs/1604.05108
• C. Thomassen, Every planar graph is 5-choosable, J. Combin. Theory Ser. B 62 (1994) 180–181.
• C. Thomassen, 3-list-coloring planar graphs of girth 5, J. Combin. Theory Ser. B 64 (1995) 101–107.
• M. Voigt, List colourings of planar graphs, Discrete Math. 120 (1993) 215–219.
• M. Voigt, A not 3-choosable planar graph without 3-cycles, Discrete Math. 146 (1995) 325–328.
• M. Voigt, A non-3-choosable planar graph without cycles of length 4 and 5, Discrete Math. 307 (2007) 1013–1015.

Motivation

Tree-width measures how closely a graph resembles a tree. Graphs of bounded tree-width admit dynamic-programming algorithms for problems that are NP-hard in general (colouring, Hamiltonicity, and every property expressible in monadic second-order logic, by Courcelle's theorem), which is why the parameter is central to parameterized complexity and to combinatorial optimization on sparse networks. The question this mission addresses is structural: which excluded substructures force bounded tree-width?

The answer is the Excluded Grid Theorem of Robertson and Seymour: excluding a fixed graph $H$ as a minor bounds the tree-width if and only if $H$ is planar. The "only if" direction is easy, since grids are planar and have unbounded tree-width. The "if" direction is the content of Graph Minors. V. Excluding a Planar Graph (J. Combin. Theory Ser. B 41 (1986) 92–114). It is a cornerstone of the Graph Minors series that culminates in the Robertson–Seymour theorem (graphs are well-quasi-ordered by the minor relation), and it underlies polynomial-time minor testing for planar $H$ (Graph Minors XIII) and the Erdős–Pósa-type results of Sect. 8 of the same paper.

Timeline. Robertson and Seymour, Graph Minors V (1986): tree-width at most an explicit, iterated-exponential function of the grid size. Robertson, Seymour and Thomas, Quickly excluding a planar graph (JCTB 62, 1994): bound $2^{O(\theta^5)}$ for the $\theta$-grid. Chekuri and Chuzhoy (J. ACM 2016): the first polynomial bound. Chuzhoy and Tan (JCTB 2021): $O(\theta^9\,\mathrm{polylog}\,\theta)$.

Setting

Graphs are finite. A graph $H$ is a minor of $G$ if $H$ can be obtained by contraction from a subgraph of $G$; equivalently, there are nonempty, pairwise disjoint vertex sets $\beta(w)\subseteq V(G)$, one per vertex $w$ of $H$, each inducing a connected subgraph, such that every edge $ab$ of $H$ is matched by an edge of $G$ between $\beta(a)$ and $\beta(b)$.

A tree-decomposition of $G$ is a tree $T$ together with bags $X_t\subseteq V(G)$ ($t\in V(T)$) such that every vertex lies in some bag, both ends of every edge lie in a common bag, and $X_t\cap X_{t''}\subseteq X_{t'}$ whenever $t'$ lies on the path of $T$ between $t$ and $t''$. Its width is $\max_t(|X_t|-1)$, and the tree-width $\mathrm{tw}(G)$ is the least width of a tree-decomposition of $G$.

The $\theta$-grid has vertex set $\{v_{ij}: 1\le i,j\le\theta\}$, with $v_{ij}$ adjacent to $v_{i'j'}$ exactly when $|i-i'|+|j-j'|=1$. For even $\theta\ge 6$, $\mathcal F_\theta$ is the class of graphs with no minor isomorphic to the $\theta$-grid. Every planar graph $H$ is a minor of some even grid of size at least 6; $\theta(H)$ denotes the least such size.

The paper fixes explicit parameters. For $k\ge 2$: $\alpha(2,n)=n+1$ and $\alpha(k,n)=2^{n\theta^4}+\alpha(k-1,2^{n\theta^4}+n+1)$. Then $\theta_1=2\alpha(\theta^2/2,\theta^2/2)$; $\phi_{\theta_1}=\theta^2/2$ and $\phi_k=\phi_{k+1}2^{\phi_{k+1}\theta^2}$; $\theta_2=\phi_0+2\phi_1+\dots+2\phi_{\theta_1-1}+\phi_{\theta_1}$; $\theta_3=(\theta^2/2)^{\theta_2-1}$; $\theta_4=\theta_2\binom{\theta_3}{\theta_2}+\tfrac12\theta^2\binom{\theta_3}{\theta^2/2}$; $\theta_5=(\theta^2/2)^{\theta_4-1}$; $\theta_6=\theta_3\binom{\theta_5}{\theta_4}+\tfrac12\theta^2\binom{\theta_5}{\theta^2/2}$; $\theta_7=\alpha(\theta_5,\theta_6)$; $\theta_8=3\theta_5(3^{\theta_5}-1)/4$; $\theta_9=\theta_7(\theta_8+1)+1$.

Two auxiliary structures carry the argument. An $(m,n)$-web is a pair of families of paths $(A_1,\dots,A_m)$, $(B_1,\dots,B_n)$, each family vertex-disjoint, every $A_i$ meeting every $B_j$, and all $m+n$ paths pairwise edge-disjoint. An $(m,n)$-mesh is the same with arbitrary connected subgraphs in place of paths and without edge-disjointness.

Formalization targets

Goal: (2.1)

For every finite planar graph $H$ and every finite graph $G$,

$$H \not\preceq G \;\Longrightarrow\; \mathrm{tw}(G)\le\theta_9\bigl(\theta(H)\bigr).$$

Principal theorem: (7.3)

For even $\theta\ge 6$ and $G\in\mathcal F_\theta$,

$$\mathrm{tw}(G)\le\theta_9.$$

Intermediate targets

• Sect. 2: every planar graph is a minor of some even $\theta$-grid, $\theta\ge 6$.
• (3.2): $n$ disjoint connected subgraphs meeting each of $V_1,\dots,V_k$, or a hitting set of size $<\alpha(k,n)$.
• (4.1), (4.2), (4.4), (4.5), (4.6): no $(\theta_2,\theta_2)$-web in $G\in\mathcal F_\theta$.
• (5.1), (5.2), (5.3): no $(\theta_5,\theta_6)$-mesh in $G\in\mathcal F_\theta$.
• (6.2), (6.3), (6.4): weighted and unweighted balanced-cut lemmas valid for all graphs.
• (7.1), (7.2): separations of order $\le\theta_7$ splitting $V(G)$, or any $X\subseteq V(G)$, in ratio $1-\theta_8^{-1}$.

Significance

The theorem converts a qualitative exclusion (no $H$ minor) into a quantitative width bound, and it is the entry point of the structure theory of minor-closed classes: every minor-closed class excluding a planar graph has bounded tree-width, and hence all MSO-definable problems on it are solvable in linear time. It is used in the proof of the graph minor theorem, in minor testing, and in the Erdős–Pósa property for planar minors (Sect. 8 of the paper).

The result is proved and classical; to our knowledge it has not been machine-checked in any proof assistant, and Mathlib has no graph minors, tree-decompositions or Menger's theorem. A formalization produces reusable definitions (branch-set minors, tree-decompositions, separations, grids) and a checked proof of the paper's explicit bound. The goal is stated with the paper's constant $\theta_9$, not an optimized one; later improvements are stronger variants, not replacements.

Difficulty

The obvious attempt, building a tree-decomposition greedily from small separations, fails because nothing forces small balanced separations to exist. The whole argument supplies them: a graph without a large grid minor has no large mesh (5.3), and a graph with no large mesh has a balanced separation of bounded order (7.1). The step from no grid to no mesh goes through webs and spiders (Sect. 4) and relies on two results from Graph Minors I ((3.1) and (4.3) of the paper, cited without proof), which themselves depend on Menger's theorem. The balanced-cut lemmas (6.2)–(6.4) rest on Tutte's ordering of 2-connected graphs. None of this infrastructure exists in Mathlib.

Formalization scope

Graphs are Mathlib SimpleGraphs on finite types (Fintype V, DecidableEq V). The paper allows loops and multiple edges; for $G$ this changes nothing, since every notion used depends only on adjacency, and for $H$ in the goal it specializes the theorem to simple planar graphs. Minors use the branch-set model (IsMinor); planarity (IsPlanar) is the existence of a crossing-free drawing in $\mathbb R^2$, mirroring the platform's FourColor.IsPlanar. Tree-width is not defined as an infimum; "tree-width at most $w$" (TreewidthLE) is the existence of a tree-decomposition with all bags of size $\le w+1$ over a finite tree. $\theta(H)$ enters the goal as a hypothesis IsLeast {t | Even t ∧ 6 ≤ t ∧ IsMinor H (grid t)} θ, which is satisfiable for every planar $H$ by the Sect. 2 milestone, so the goal is not vacuous. Every statement of Sects. 3–7 that mentions $\theta$ carries the standing assumption "$\theta$ even, $\theta\ge 6$" as hypotheses. Rational bounds such as $(1-\theta_8^{-1})|V(G)|$ and $2(3^k-1)^{-1}|V(G)|$ are compared in $\mathbb Q$.

Two printed statements are corrected. (4.5) is printed for $0\le k<\theta_2$ and is stated for $0\le k<\theta_1$, the only range on which $\phi_{k+1},\psi_{k+1}$ are defined. (5.1) is false as printed for $p=1$, $q\ge 1$, so it carries the hypothesis "$p=1$ implies $q=0$"; the paper uses it only with $p=\theta^2/2$.

Needed infrastructure, reusable well beyond this mission: Menger's theorem, the Graph Minors I linkage results, Tutte's ordering of 2-connected graphs, and a library of lemmas for minors and tree-decompositions. Proofs of any milestone, of the cited results as separate theorems, and of basic API for the definitions are welcome.

Selected references

• N. Robertson, P. D. Seymour, Graph Minors. V. Excluding a Planar Graph, J. Combin. Theory Ser. B 41 (1986) 92–114. https://doi.org/10.1016/0095-8956(86)90030-4
• N. Robertson, P. D. Seymour, Graph Minors. I. Excluding a Forest, J. Combin. Theory Ser. B 35 (1983) 39–61. https://doi.org/10.1016/0095-8956(83)90079-5
• N. Robertson, P. D. Seymour, R. Thomas, Quickly Excluding a Planar Graph, J. Combin. Theory Ser. B 62 (1994) 323–348. https://doi.org/10.1006/jctb.1994.1073
• C. Chekuri, J. Chuzhoy, Polynomial Bounds for the Grid-Minor Theorem, J. ACM 63 (2016), Art. 40. https://doi.org/10.1145/2820609
• J. Chuzhoy, Z. Tan, Towards Tight(er) Bounds for the Excluded Grid Theorem, J. Combin. Theory Ser. B 146 (2021) 219–265. https://doi.org/10.1016/j.jctb.2020.09.010
• B. Courcelle, The Monadic Second-Order Logic of Graphs. I. Recognizable Sets of Finite Graphs, Information and Computation 85 (1990) 12–75. https://doi.org/10.1016/0890-5401(90)90043-H

Let $u_1, \dots, u_n$ be unit vectors in a Euclidean space such that among any three of them some two are orthogonal. How large can $\|u_1 + \dots + u_n\|$ be?

The answer is $\Theta(n^{2/3})$.

Attribution, which is commonly given wrong in both halves

Lovasz posed the question, as Problem 11.8 of Combinatorial Problems and Exercises (North Holland, 1979). Konyagin proved the $O(n^{2/3})$ upper bound in Systems of vectors in Euclidean space and an extremal problem for polynomials, Mat. Zametki 29 (1981) 63-74, doi:10.1007/BF01142512. Alon gave a matching lower bound in Explicit Ramsey graphs and orthonormal labelings, Electron. J. Combin. 1 (1994) R12, doi:10.37236/1192. The two together pin the exponent exactly.

Where the proof comes from

The hypothesis is a graph condition in disguise. Join $i$ to $j$ when $\langle u_i, u_j \rangle \ne 0$; then "among any three some two are orthogonal" says that graph is triangle-free.

The proof does not run through Ramsey counting, which is the natural first guess and does not reach the right exponent. It runs through the Lovasz theta function. Kashin and Konyagin bound $\theta = O(n^{1/3})$ for graphs of independence number less than 3, that is for complements of triangle-free graphs, and Cauchy-Schwarz turns that into the bound on the norm of the sum. The orthonormal labeling of a graph by unit vectors is not a coincidence of notation: it is the definition of $\theta$ that the argument uses.

What this mission will cost

State this honestly rather than discover it later. The Lovasz theta function, orthonormal graph labeling, and Shannon capacity are all absent from Mathlib. So the milestone chain that the upper bound needs cannot be written yet, and this proposal ships with exactly one milestone, which is Alon's lower bound.

google-deepmind/formal-conjectures contains an SDP-form definition of the theta function, with basic bounds such as lovaszThetaFunction_le_card since PR #6100 of 2026-09-18. The proof here needs the orthonormal-labeling form instead, so that file is a starting point rather than a foundation. Building the theta function, proving that the two forms agree, and getting the Kashin-Konyagin bound is the real content of this mission and is larger than the statement of the goal suggests.

The lower bound is the tractable half. It needs explicit Ramsey graphs and an orthonormal labeling of one, and it does not need $\theta$ at all.

Notes on the formalization

Both items are stated in Mathlib primitives alone, so the mission omits definition items. The triangle-free hypothesis is written as a condition on triples of indices rather than through SimpleGraph.CliqueFree 3, so that a reader auditing the statement does not have to unfold a graph construction to see what is assumed. Anyone proving it is free to build the graph and use the Mathlib predicate.

Why formalize the Four Color Theorem in Lean 4?

The Four Color Theorem links a short mathematical statement to a large collection of finite checks. For contributors to graph theory and proof assistants, it is a concrete test of whether abstract mathematics, executable verification, and a public theorem statement can share one auditable foundation. The proposed result is a complete Lean 4 formalization, reusing Mathlib and adapting the established proof architecture to Lean.

The mathematical result is established. Robertson, Sanders, Seymour, and Thomas gave a modern computer-assisted proof in 1997. Gonthier subsequently developed a Coq formalization covering both mathematical reasoning and computation, described in his 2005 report and 2008 Notices article. This mission is classified as ResearchPaper because it formalizes these published results. (RSST, Gonthier 2005, Gonthier 2008)

Graphs, drawings, and colors

The root Lean interface uses Mathlib's SimpleGraph: a finite vertex set with a symmetric, irreflexive adjacency relation. Edges in this representation carry no additional identities or multiplicities. The conventional statement also permits parallel edges. Already-proved local infrastructure uses Mathlib's Graph V E to erase parallel edges while preserving a genuine plane drawing and proper vertex colorings; only the actual vertex set must be finite. A proper vertex coloring assigns a color to every vertex and assigns different colors to adjacent vertices. Four available colors means at most four colors are used; there is no requirement that each color occur.

A planar drawing places distinct vertices at distinct points of the real plane and represents each edge by an injective continuous arc joining its endpoints. An arc contains no other vertex, and arcs of different undirected edges meet only at shared endpoints. Reversing the orientation of an edge reverses its parameterization. A graph is planar when such a drawing exists. This is a geometric condition independent of coloring and of the eventual configuration checkers. Gonthier discusses the graph-embedding formulation in Section 2, PDF p. 4 of the 2005 report.

Write $V$ for the vertex set, $G$ for its adjacency relation, and $C=\{0,1,2,3\}$ for the available colors. Empty graphs, isolated vertices, and disconnected graphs are included. The drawing is a witness to a hypothesis; the theorem does not impose coordinates, a prescribed embedding, or a straight-line representation.

Formalization target

For every finite loopless planar graph, establish

$$\forall\,G=(V,E),\qquad \operatorname{Planar}(G)\Longrightarrow \exists c:V\to C,\quad \forall v,w\in V,\ \{v,w\}\in E\Longrightarrow c(v)\ne c(w).$$

The draft Lean target is FourColor.four_color: for every finite vertex type and every SimpleGraph on that type, FourColor.IsPlanar G implies G.Colorable 4. Its graph formulation follows RSST's Section 1, PDF p. 2 of the author-hosted manuscript. The manuscript's PDF page numbers differ from the journal's pagination.

The exact unchanged root signature is:

FourColor.four_color.{u} :
  ∀ (V : Type u) [Finite V] (G : SimpleGraph V),
    FourColor.IsPlanar G → G.Colorable 4

This is an open target signature, not a completed proof. The existing FourColor.FinalAudit.multigraph_four_color_of_necessary_targets conditionally connects the mission obligations to the conventional finite loopless planar multigraph statement. Its drawing has distinct vertex positions and injective continuous arcs for each edge identity; erasing parallel edges is proved to preserve planarity and every proper-coloring constraint. This bridge adds no simplicity, connectedness, triangulation, or nonemptiness assumption to the conventional conclusion. The root target itself remains unchanged.

An equivalent combinatorial formulation is welcome only with the formally verified translations needed to recover this target. If equivalence is claimed, both directions must be proved under precisely stated conventions. In particular, a hypermap coloring theorem alone does not complete this mission.

The original seven structural milestones remain unchanged:

Milestone	Deliverable
1. Graph realization	Construct a planar plain hypermap whose faces represent exactly the nonisolated graph vertices and whose edge steps encode precisely adjacency.
2. Cubic normalization	Construct a plain cubic hypermap with six times as many darts, preserving planarity and bridgelessness and transporting a coloring back.
3. Minimal counterexample	Choose a least-dart counterexample within the planar, bridgeless, plain, precubic comparison class.
4. Counterexample structure	Prove cubicity, connectedness and minimum face arity five as consequences of minimality.
5. Charge conservation	Prove total face charge $120c$ for $c$ components under arbitrary rational dart transfers, and a positive-charge face when connected.
6. Elimination	Complete the source's reducibility and unavoidability analysis to exclude every minimal counterexample.
7. Hypermap theorem	Assemble four-colorability for all planar bridgeless hypermaps.

These correspond to Gonthier's reductions in Section 3, PDF pp. 6–9, and development in Sections 5.1–5.6 of the 2005 report. Exact locations and executable-reference declarations accompany each milestone. Milestones 2, 3 and 6 imply milestone 7; milestones 1 and 7 imply the graph target. Those two conditional implications have been checked in Lean against the exact proposed statements. Milestone 6 now has thirteen concrete supporting targets:

Core target	Deliverable
Catalogue geometry	Prove geometric admissibility of every one of the fixed 633 configurations.
Catalogue reducibility	Kernel-check reducibility of every fixed map and contract using the proved complete checker or a verified refinement.
Reflection	Prove that the explicit mirror preserves minimal counterexamples.
Geometric exclusion	Prove that a C-reducible configuration cannot occur in a minimal counterexample; this includes the Birkhoff and patching arguments.
Presentation soundness	Prove the concrete finite presentation checker's generic soundness as one route to coverage.
Seven coverage cases	Independently handle positive hubs of degrees 5, 6, 7, 8, 9, 10 and 11, allowing reflected occurrences and unbounded neighboring arities.
Transfer bound	Bound each directed transfer by five under the explicit absence-of-configurations hypothesis; proved arithmetic then excludes positive hubs of degree at least 12.

The fixed catalogue and fixed rules are shared by both branches. The local Lean assembly checks that reducibility, geometric exclusion, reflection, the transfer bound, the seven degree cases, and milestones 4–5 imply milestone 6. It then connects to the unchanged hypermap and graph targets. The generic presentation checker offers a sufficient route to the semantic degree targets; its ability to certify every source presentation is not presumed. That route also requires actual presentation certificates and proofs of acceptance for the degree cases. Generic soundness and catalogue geometry alone do not supply those witnesses. Direct proofs of the seven semantic coverage obligations remain valid. Catalogue geometry remains a separate, meaningful finite theorem.

Exact mission obligations

There are 21 open theorem targets: 20 supporting milestones and one root. Every name below has prefix FourColor.. All remain future mission work; the checked conditional assembly is not a proof of any of these targets.

#	Exact target name	Obligation
1	graph_realization	Realize a finite drawn graph by a planar plain hypermap with exact face/adjacency incidence.
2	cubic_normalization	Construct the sixfold plain cubic map with the stated preservation and coloring transport.
3	minimal_counterexample_exists	Select a least-dart counterexample in the precubic comparison class.
4	minimal_counterexample_structure	Derive cubicity, connectedness and face arity at least five from minimality.
5	charge_conservation	Prove total charge and existence of a positive face for a connected host.
6	catalogue_embeddable	Prove the fixed 633 entries satisfy configuration geometry.
7	catalogue_reducibility_certificates	Establish accepted reducibility certificates for every fixed entry.
8	mirror_minimal_counterexample	Preserve minimal-counterexample status under the specified mirror.
9	reducible_configuration_exclusion	Exclude a C-reducible occurrence from a minimal counterexample.
10	discharge_presentation_soundness	Prove generic soundness of the concrete finite presentation checker.
11	degree_5_coverage	Derive a catalogue occurrence, in either orientation, from a positive degree-5 hub.
12	degree_6_coverage	Establish the same semantic occurrence obligation for degree 6.
13	degree_7_coverage	Establish the same semantic occurrence obligation for degree 7.
14	degree_8_coverage	Establish the same semantic occurrence obligation for degree 8.
15	degree_9_coverage	Establish the same semantic occurrence obligation for degree 9.
16	degree_10_coverage	Establish the same semantic occurrence obligation for degree 10.
17	degree_11_coverage	Establish the same semantic occurrence obligation for degree 11.
18	discharge_transfer_bound	Bound each transfer by five under minimality and absence of catalogue occurrences in either orientation.
19	no_minimal_counterexample	Assemble the core argument to exclude all minimal counterexamples.
20	hypermap_four_color	Assemble four-colorability of every planar bridgeless hypermap.
21	four_color	Prove the unchanged finite planar graph root above.

The degree cases quantify over minimal counterexamples with the exact positive score defined by the fixed rules; neighboring degrees have no artificial upper bound. The dependency path uses 16 necessary input targets to derive targets 19, 20 and 21. Targets 6 and 10 support the optional presentation-certificate route. None of targets 19, 20 or 21 is assumed as a shortcut in this assembly.

What completion would provide

The theorem provides a uniform existence guarantee for all finite planar graphs, without a bound on their size. Its Lean development should also make reusable graph embeddings, finite combinatorial maps, coloring transports, and verified finite checkers available to later work.

The existing Rocq development is an executable reference for definitions, dependency structure, and proof behavior. It is not a proof import into Lean. The proposed contribution is a Lean development whose proof objects and computation are justified within Lean's documented foundations. A mechanically translated collection of scripts is not required; contributors should choose abstractions that work well with Mathlib.

Where the difficulty lies

Checking finitely many small graphs does not establish the theorem for arbitrary finite graphs. The development must justify why its finite computational tasks suffice, and must connect their results to the graph statement. The mathematical and computational obligations must meet at explicit, proved interfaces.

There is also a representation gap. The standard target concerns vertex colorings of graphs drawn in the plane, whereas the reference implementation's combinatorial core colors faces of planar bridgeless hypermaps. The latter endpoint is four_color_hypermap in combinatorial4ct.v. Correct treatment of duality, connected components, and isolated vertices is part of the work. Renaming a combinatorial predicate “planar” cannot establish that connection.

Formalization scope and acceptance criteria

Use Lean 4 with a supported, pinned Mathlib revision. The initial draft is checked against Lean v4.30.0 and Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f. Any later migration must preserve the statements and repeat the relevant checks. Reuse Mathlib's graph and coloring interfaces where appropriate, and develop missing infrastructure as reusable modules. The topological definition must not assume colorability, successful certificate verification, or the conclusion of an intermediate theorem.

The definition layer now provides plane drawings, finite permutation hypermaps, an exact graph/face incidence representation, minimal counterexamples, and rational face charges. Coloring equivalence across a face representation is proved for every positive number of colors, with isolated vertices handled explicitly. Exact Euler equality defines combinatorial planarity; geometric realization is a theorem obligation and cannot be assumed from the name.

The concrete core now defines configurations, ordered boundary traces, contracts, chromograms, Kempe closure, kernel preembeddings and reflected occurrences. The reference reducibility checker has proved soundness and completeness. All 633 maps, rings and contracts are literal data with kernel-validated table/index proofs. The 38 base entries and their 71 symmetrized entries are explicit, and the executable matcher has proved semantic correctness. These infrastructure results do not prove the catalogue's geometric validity, its reducibility, or unavoidability.

The production targets import FourColor.CompactCatalogue.configurations, a compact catalogue containing the same literal maps, rings and contracts. A generic verified decoder constructs validated entries without storing large evaluated proof terms in every import. A separate kernel-checked comparison proves exact ordered equality with the original catalogue, proves that every raw entry is accepted, and proves that none is dropped. The original certificate batches remain available for that audit but are excluded from production target imports. This representation change does not alter any of the 21 mathematical obligations.

Data provenance is pinned to Rocq commit c1d6b1cd5288bea4b067aac13cdde3c18dffe018. Independent fresh-source comparisons check all 633 configurations and every base/expanded rule entry against that snapshot, including actual evaluated Lean payloads. These comparisons establish source correspondence; they are not proofs of reducibility or unavoidability.

The duplicate-data gate rejects unexplained or unintended duplicates and permits verified source-mandated repetition encoding multiplicity or weight. The only repeated rule payload is drule1, deliberately listed twice: the source explains its two-point transfer in discharge.v, lines 17–24 and retains both copies in base_drules (line 145). The Lean rule-match count also counts both copies, preserving weight two. Thus there are 38 base entries with 37 distinct payloads, and 71 expanded entries with 70 distinct payloads. Both copies must remain. No configuration duplicates or other repeated rule payloads are permitted without separately verified source justification.

The reference reducibility evaluator is exponentially expensive. Contributors should implement verified compressed representations or efficient checkers, with acceptance implying the same semantic C-reducibility. Completeness of the reference checker then recovers the stated certificate-existence target. The presentation language is a transparent finite baseline; its generic soundness is an open target, and no completeness claim is made. Source-style quizzes/hubcaps or direct Lean proofs can close the same seven semantic coverage targets. This keeps performance choices separate from the mathematical endpoint.

All computational claims needed by the theorem must be established in Lean. External generators may prepare candidate data or certificates, but their output must be validated by a checker with proved correctness, and the resulting proof must be accepted by the Lean kernel. A recorded successful run of an external program is insufficient. The final theorem and its dependency closure must contain no sorry, admit, unproved custom axiom, or unsupported computational assumption. An axiom audit must identify only Lean/Mathlib's documented foundations. The current 37-declaration conditional/infrastructure audit uses only propext, Classical.choice and Quot.sound; it does not claim an unconditional Four Color proof. Python generators and runtime JSON extraction are outside the mathematical trust boundary and cannot discharge the 21 targets.

Completion requires a reproducible repository in which lake build succeeds from a clean environment and builds the final theorem. Pin toolchain, dependencies, source revisions, and certificate data; document regeneration and verification commands. Maintain a dependency map connecting Lean declarations to exact paper locations and Rocq declarations, and record justified differences in representation. The local multigraph adapter already justifies forgetting parallel-edge multiplicities and transports proper colorings. Any auxiliary restrictions such as connectedness or nonemptiness must be discharged before the root theorem. The current statement and conditional builds verify proposal infrastructure. Success requires proofs of the mission obligations and the final theorem in the reproducible clean build, with no unproved assumptions beyond the documented Lean/Mathlib foundations. All 21 targets remain open at proposal finalization. The submission snapshot records the repository base commit, exact working-file hashes, toolchain, Mathlib revision, payload hashes and audit report; it must not misrepresent uncommitted files as contents of the base commit.

Selected references

• Georges Gonthier, A Computer-Checked Proof of the Four Colour Theorem, technical report, 2005. Sections 2–5. Microsoft Research PDF.
• Georges Gonthier, Formal Proof—The Four-Color Theorem, Notices of the AMS 55(11), 1382–1393, 2008. Theorem 1 and the formalization architecture. AMS PDF.
• Gonthier and Rocq-community contributors, fourcolor, executable formalization, pinned to commit c1d6b1cd5288bea4b067aac13cdde3c18dffe018. Repository.
• Neil Robertson, Daniel Sanders, Paul Seymour, Robin Thomas, The Four-Colour Theorem, Journal of Combinatorial Theory, Series B 70(1), 2–44, 1997. DOI; author-hosted manuscript.

Motivation

Many production and computing systems run jobs on parallel machines that also draw on a shared, limited resource: tools, workers, memory, power. Adding such a resource to a scheduling problem can change its complexity entirely. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the three-field classification $\alpha\mid\beta\mid\gamma$ of Graham, Lawler, Lenstra and Rinnooy Kan by a resource field $res\lambda\sigma\rho$, and determined the complexity of every problem with unit-time jobs on identical or uniform machines under the makespan criterion. Their Fig. 2 separates the maximal polynomially solvable cases from the minimal NP-hard ones.

This mission formalizes the polynomial side. Two identical machines are easy under arbitrary resources (Theorem 1, due to Garey and Johnson, via maximum matching). Three identical machines with one resource are NP-hard in the strong sense (Theorem 4), and so are two uniform machines with unit resources (Theorem 3). What remains for uniform machines is settled by two algorithms: a sorting-and-shifting procedure for two uniform machines with one resource of arbitrary size (Theorem 5), and a bottleneck transportation problem for any number of uniform machines with one resource and 0–1 requirements (Theorem 6). The hardness results are the subject of the companion missions I and II.

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines $M_1,\dots,M_m$. Machine $M_i$ has speed $q_i>0$; every job has unit execution requirement, so it takes time $1/q_i$ on $M_i$. Identical machines ($P$) have $q_i=1$; uniform machines ($Q$) have arbitrary speeds. There are $l$ resources $R_h$ with positive integer sizes $s_h$, and job $J_j$ needs a nonnegative integer amount $r_{hj}$ of $R_h$ throughout its execution. The field $res\lambda\sigma\rho$ records restrictions: $\lambda$ bounds the number of resources, $\sigma$ their sizes, $\rho$ the requirements, a dot meaning "part of the input". So $res1{\cdot}{\cdot}$ is one resource with arbitrary size and requirements, and $res1{\cdot}1$ is one resource with requirements in $\{0,1\}$.

A schedule gives every job a machine $\mu(j)$ and a start time $S_j\ge0$; the job is executed during $[S_j,C_j)$ with $C_j=S_j+1/q_{\mu(j)}$. It is feasible if jobs on the same machine do not overlap and, at every time $t$, the jobs executed at $t$ use at most $s_h$ of each resource $R_h$. The makespan is $C_{\max}=\max_j C_j$. No precedence constraints occur in this mission.

Formalization targets

Goal: Theorem 5, correctness of the algorithm

For $Q2\mid res1{\cdot}{\cdot},\,p_j=1\mid C_{\max}$ with $q_1\ge q_2$: put all jobs on $M_1$ in order of nonincreasing $r_{1j}$, then repeatedly move the last job of $M_1$ to the earliest feasible time on $M_2$ after the jobs already there, as long as this strictly reduces $C_{\max}$. For every order with nonincreasing requirements, the resulting schedule $A$ is feasible and

$$C_{\max}(A)\le C_{\max}(\sigma)\quad\text{for every feasible schedule }\sigma.$$

Milestones for the goal

The paper's proof has two steps, both milestones. Call a schedule an (a)–(c) schedule when (a) $M_1$ runs its jobs back to back from time $0$ in nonincreasing $r_{1j}$, (b) $M_2$ runs its jobs in nondecreasing $r_{1k}$, and (c) every requirement on $M_1$ is at least every requirement on $M_2$.

1. The algorithm's schedule is feasible, is an (a)–(c) schedule, and is best among feasible (a)–(c) schedules.
2. Every feasible schedule can be transformed into a feasible (a)–(c) schedule with no larger $C_{\max}$.

Further results

• Theorem 1. For $P2\mid res{\cdot}{\cdot}{\cdot},\,p_j=1\mid C_{\max}$, with $G$ the graph joining two jobs when they can run together and $S$ a maximum matching of $G$, the optimal makespan is $n-|S|$.
• Theorem 6. For $Q\mid res1{\cdot}1,\,p_j=1\mid C_{\max}$ with the $s_1$ fastest machines listed first, the optimal makespan equals the optimal value of a bottleneck transportation problem that assigns jobs to slots (machine, position) with cost $k/q_i$, resource jobs only to the $s_1$ fastest machines.

Significance

Theorems 5 and 6 complete the classification of Fig. 2 for uniform machines: every special case of $Q\mid res{\cdot}{\cdot}{\cdot},\,p_j=1\mid C_{\max}$ not covered by the hardness theorems has a polynomial algorithm. Theorem 1 is the classical reduction of two-machine resource scheduling to maximum matching, the model case for later work on scheduling with conflict graphs.

The paper proves these results briefly: "clearly" for the first half of Theorem 5, "obviously" for Theorem 1, and a one-paragraph model for Theorem 6. The exchange argument of Theorem 5 is presented "in an informal way" through five steps that pass through fractional, preempted jobs. A machine-checked proof makes these arguments exact on a model with real start times. No formalization of these results is known, and the platform had no statement about resource-constrained scheduling on uniform machines before this mission.

Difficulty

With $q_1\ne q_2$ the job boundaries on the two machines are misaligned: a job on $M_2$ overlaps parts of several jobs on $M_1$, so the resource check cannot be done slot by slot, and discrete reasoning on integer time grids does not apply. The exchange argument of Theorem 5 must control the resource usage at every real time while jobs are moved between machines and reordered, and it has to end with a nonpreemptive schedule even though the paper's intermediate steps split jobs. For Theorem 1, the hard direction is the lower bound: a feasible schedule with arbitrary real start times must be converted into a matching, which is a statement about how unit jobs on two machines can overlap. For Theorem 6, one must show that restricting resource jobs to the fastest machines and to back-to-back positions loses nothing.

Formalization scope

• Model. Jobs, machines and resources are Fin n, Fin m, Fin l (0-based). Speeds are positive reals, sizes positive naturals, requirements naturals. Start times are nonnegative reals, execution intervals are half-open, and the resource constraint is checked at every real time. $C_{\max}=0$ for $n=0$. The model carries a precedence digraph for consistency with the companion missions; every statement here assumes it has no arcs.
• Implicit hypothesis. Theorems 1 and 5 assume every job fits alone ($r_{hj}\le s_h$), which the paper leaves unstated; without it no feasible schedule exists.
• The algorithm is a Lean definition following the page: the order is an argument (any nonincreasing order), "as early as possible" is the earliest start after $M_2$'s last job at which the resource constraint holds throughout, and the loop stops at the first move that does not strictly reduce $C_{\max}$.
• Optimality is always stated in full: feasibility plus a lower bound against every feasible schedule. No minimum is written as an infimum of a possibly empty set.
• Theorem 6 is stated with 0–1 slot assignments, the interpretation the paper gives to $x_{ijk}$; the page's constraint $\sum_{k=1}^{m}$ is read as $\sum_{k=1}^{n}$.
• Not formalized: the running times $O(ln^2+n^{5/2})$ (Theorem 1), $O(n\log n)$ (Theorem 5, including the phrase "This O(n log n) algorithm") and $O(n^3)$ (Theorem 6), which depend on a machine model the paper does not fix and, for Theorems 1 and 6, on cited matching and transportation algorithms.
• Ruled out: a formalization of the goal that proves optimality only against (a)–(c) schedules, against schedules with integer start times, or for one fixed tie-breaking order proves less than Theorem 5.

Contributions welcome: lemmas about step functions of resource usage on half-open intervals, a left-shifting lemma for unit-time schedules on two machines, and the exchange steps of Theorem 5 as separate lemmas.

Selected references

• J. Błażewicz, J.K. Lenstra, A.H.G. Rinnooy Kan, Scheduling subject to resource constraints: classification and complexity, Discrete Applied Mathematics 5 (1983) 11–24. https://doi.org/10.1016/0166-218X(83)90012-4
• M.R. Garey, D.S. Johnson, Complexity results for multiprocessor scheduling under resource constraints, SIAM Journal on Computing 4 (1975) 397–411. https://doi.org/10.1137/0204035
• R.L. Graham, E.L. Lawler, J.K. Lenstra, A.H.G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• S. Even, O. Kariv, An O(n^{2.5}) algorithm for maximum matching in general graphs, Proc. 16th IEEE FOCS (1975) 100–112. https://doi.org/10.1109/SFCS.1975.23

Motivation

Edge-colored tournaments combine a complete orientation with a finite palette. They are a natural setting for comparing local multicolor obstructions with global directed reachability. The question attributed to Sands, Sauer, and Woodrow asks whether three colors force one of two outcomes: a directed triangle whose three arcs all have different colors, or a single vertex that can reach every target along a monochromatic directed path.

The problem was recorded by the Open Problem Garden in 2008. A minimum-counterexample reduction was later restated by Georgakopoulos and Sprüssel in their study of three-colored tournaments. The available project computation excludes counterexamples through eleven vertices, but that package is explicitly candidate_only: it is bounded search evidence, not a proof of the unrestricted theorem.

Setting

A tournament is an orientation of a finite complete simple graph. For each pair of distinct vertices $u,v$, exactly one of $u\to v$ and $v\to u$ is present. Every directed arc receives one of three labeled colors.

A rainbow directed triangle is a cyclically oriented triangle

$$a\to b\to c\to a$$

whose three arc colors are pairwise distinct. A transitive three-vertex subtournament is not a directed triangle and is therefore not forbidden merely because its three arcs have different colors.

A vertex $s$ is a monochromatic source when, for every vertex $t$, there is some color $k$ and a directed $s$-to-$t$ path all of whose arcs have color $k$. The chosen color may depend on $t$; the theorem does not demand one common color for all targets. Length-zero reachability handles $t=s$.

The formal domain is nonempty finite tournaments. This nonemptiness convention is stated explicitly because an empty vertex type has neither a rainbow triangle nor a candidate source and would trivialize the negation of the intended question.

Formalization targets

Root theorem

For every nonempty finite tournament $T$ with a three-coloring of its arcs,

$$T\text{ has a rainbow directed triangle} \quad\lor\quad \exists s\in V(T)\ \forall t\in V(T),\ \text{$s$ reaches $t$ monochromatically}.$$

No compatibility is required between the colors of paths to different targets, and unused palette colors are permitted.

Finite order milestone

The first milestone freezes the exact bounded claim supported by the replay package:

$$1\le |V(T)|\le 11\text{ and no rainbow directed triangle} \quad\Longrightarrow\quad T\text{ has a monochromatic source}.$$

The statement includes all tournaments and all three-color arc assignments at those orders, not only one symmetry representative. The repository's observations report exhaustive search after a minimum-counterexample reduction, but the Lean theorem remains open until it has an accepted proof.

Significance

The root theorem would turn a local forbidden configuration into a global reachability certificate. Such a result clarifies how orientation and edge color interact: ordinary Gallai decompositions for undirected colored complete graphs cannot be imported unchanged, because the hypothesis forbids only rainbow cyclic triangles and allows rainbow transitive triples.

The formal development creates reusable definitions for colored directed reachability and exposes the direction of every relation. This matters in minimum-counterexample arguments, where an auxiliary arc $u\to_F v$ may encode that $v$ cannot reach $u$; reversing that convention invalidates the cycle reduction. A verified finite milestone would also provide a regression target for SAT, SMT, or exhaustive encodings without elevating their raw output to a universal theorem.

Difficulty

The classical Gallai theorem is not directly applicable. It assumes an undirected complete graph with no rainbow triangle of any orientation, whereas this problem permits a transitive triple with three distinct colors. A proposed partition must therefore control both arc colors and directions between parts.

The minimum-counterexample route yields a useful spanning cycle in an auxiliary nonreachability digraph. It does not itself bound the size of a counterexample. The order-eleven computation terminates because its domain is finite, but no induction from eleven to arbitrary order follows. A proof must add a structural theorem that survives all orientations and allows monochromatic paths of arbitrary length rather than treating reachability bits as independent physical arcs.

Formalization scope

Lean represents the tournament as a binary relation D with looplessness and exactly one orientation on each unordered pair. The coloring is a total function on ordered pairs, but only values on actual arcs are semantically used. Monochromatic reachability is the reflexive transitive closure of arcs of one fixed color. The root and finite theorem quantify over every nonempty finite vertex type.

The finite replay, its solver versions, hashes, and no-witness observations remain external candidate evidence. They do not close the milestone without a checkable certificate or a proof accepted by the platform. Contributions may formalize the minimum-counterexample cycle lemma, build an independently checked finite certificate, isolate a directed decomposition theorem, or prove the root. No contribution may replace a directed rainbow triangle by an undirected one, require the same path color for every target, or assume heredity of failure for arbitrary induced subtournaments.

Selected references

• Open Problem Garden, Monochromatic reachability versus rainbow triangles, posted 2008. https://www.openproblemgarden.org/op/monochromatic_reachability_vs_rainbow_triangles
• B. Sands, N. Sauer, and R. Woodrow, On monochromatic paths in edge-coloured digraphs, Journal of Combinatorial Theory, Series B 33 (1982), 271–275.
• A. Georgakopoulos and P. Sprüssel, On 3-coloured tournaments, 2009. https://arxiv.org/abs/0904.1967
• A. Trygub, Full Characterization of Color Degree Sequences in Complete Graphs Without Tricolored Triangles, 2023. https://arxiv.org/abs/2304.14579