Graph Theory

Motivation

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

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

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

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

Setting

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

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

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

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

Formalization targets

Goal

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

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

Supporting targets

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

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

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

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

Setting

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

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

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

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

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

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

Formalization targets

Main goal

For every finite simple graph $G$,

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

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

Literature and route milestones

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

Candidate boundary milestones

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

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

Formalization targets

The two-part OPG record

The source records both

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

and

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

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

Published first part

A milestone formalizes the stronger published statement

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

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

Universal bound

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

Selected references

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

Motivation

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

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

Setting

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

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

The asymptotic notation

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

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

Formalization targets

Erdős Problem 81

The root theorem is

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

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

Leading-coefficient milestone

The supporting target records the weaker uniform statement

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

Selected references

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

Motivation

A quantum LDPC code is a CSS code whose two check matrices $H_X$ and $H_Z$ have rows and columns of bounded weight, so that every check measures only a few qubits. Such codes are the main candidates for fault-tolerant quantum memories, because their checks are local, but a code is only useful together with a decoder: an efficient procedure that recovers the error, up to stabilizers, from its syndrome. For classical LDPC codes built from expander graphs, Sipser and Spielman showed in 1996 that a simple bit-flipping algorithm corrects a constant fraction of the minimum distance in linear time (Sipser–Spielman 1996). In the quantum setting the obvious analogue fails, and before this work no family of quantum LDPC codes was known to admit an efficient decoder correcting a number of adversarial errors proportional to its minimum distance.

Timeline.

• 1996: Sipser and Spielman, expander codes and their linear-time bit-flipping decoder.
• 2009: Tillich and Zémor introduce the hypergraph product, giving quantum LDPC codes of positive rate and minimum distance of order $\sqrt n$ (arXiv:0903.0566).
• 2015: Leverrier, Tillich and Zémor take the hypergraph product of an expanding biregular graph with itself and prove that a greedy generator-flipping decoder corrects every error of weight up to a constant fraction of the minimum distance (arXiv:1504.00822, FOCS 2015). This mission formalizes that result.

Setting

Let $G = (A \cup B, \mathcal E)$ be a finite bipartite graph, $n_A = |A|$, $n_B = |B|$, with $n_B \le n_A$, and write $a \sim b$ for adjacency. $G$ is $(\Delta_A, \Delta_B)$-biregular if every vertex of $A$ has $\Delta_A$ neighbours and every vertex of $B$ has $\Delta_B$. For $S \subseteq A$ let $\Gamma(S)$ be its neighbourhood. $G$ is $(\gamma_A, \delta_A)$-left-expanding if $|\Gamma(S)| \ge (1 - \delta_A)\Delta_A |S|$ for every $S \subseteq A$ with $|S| \le \gamma_A n_A$; right expansion is the same on the $B$ side, and left-right expanding means both. $\Gamma_u(S)$ denotes the unique neighbours of $S$, adjacent to exactly one vertex of $S$.

Let $H$ be the $n_B \times n_A$ binary biadjacency matrix of $G$. The quantum code $\mathcal Q_G$ has $n = n_A^2 + n_B^2$ qubits, indexed by $A^2 \cup B^2$ (written $\alpha a$ and $b\beta$), and check matrices

$$H_X = (\mathbb 1_{n_A} \otimes H,\ H^T \otimes \mathbb 1_{n_B}), \qquad H_Z = (H \otimes \mathbb 1_{n_A},\ \mathbb 1_{n_B} \otimes H^T),$$

with rows indexed by $A \times B$ and $B \times A$. The row $ba$ of $H_Z$ has support the Z-generator $g_{ba} = \{\alpha a : \alpha \sim b\} \cup \{b\beta : \beta \sim a\}$. An $X$ error is $e \in \mathbb F_2^{A^2 \cup B^2}$, its syndrome is $\sigma_X(e) = H_X e^T$, and $\mathcal C_Z^\perp$ is the space of sums of Z-generators. The weight $w(e_X, e_Z)$ of a quantum error counts the qubits where $e_X$ or $e_Z$ is nonzero.

The decoder. On a syndrome $s$, one iteration picks a vector $e_1$ whose support lies in some generator $g_{ba}$, such that $s_1 = s + \sigma_X(e_1)$ has $|s_1| < |s|$ and the ratio $(|s| - |s_1|)/|e_1|$ is maximal among all such vectors. It iterates on the current syndrome, fails if it gets stuck at a nonzero syndrome, and otherwise outputs the sum $e_O$ of the flipped vectors. The $Z$ decoder is the same with $H_X$ and $H_Z$ exchanged.

Formalization targets

Goal: Theorem 2

Assume $G$ is $(\Delta_A, \Delta_B)$-biregular and $(\gamma_A, \delta_A, \gamma_B, \delta_B)$-left-right expanding with

$$\delta_A < \tfrac16, \qquad \delta_B < \tfrac16,$$

and let $(e_X, e_Z)$ be a quantum error with

$$w(e_X, e_Z) < w_0 = \frac{1}{3(1 + \Delta_B)} \min(\gamma_A n_A, \gamma_B n_B).$$

Then on every run, the $X$ decoder on input $\sigma_X(e_X)$ never outputs a failure and its output satisfies $e_O + e_X \in \mathcal C_Z^\perp$. The $Z$ decoder on $\sigma_Z(e_Z)$ behaves symmetrically, with $e_O + e_Z \in \mathcal C_X^\perp$.

Milestones

In the paper's order of proof:

• Lemma 3, $|\Gamma_u(S_A)| \ge (1 - 2\delta_A)\Delta_A |S_A|$;
• Proposition 4, distance at least $\gamma_A n_A$ for the classical code;
• the distance half of eq. (3), $d_Q \ge \min(d, d^T)$, already posed on the platform;
• Corollary 5, $d_Q \ge \min(\gamma_A n_A, \gamma_B n_B)$;
• the column-weight bound $|\sigma_X(e)| \le \Delta_B |e|$;
• Lemma 7, existence of a critical generator;
• the displays (19), (22), (23), (24) of Appendix B;
• Lemma 8, a step of ratio at least $1/3$ inside a critical generator;
• Lemma 10, the $X$ half of the goal.

Significance

The result. Theorem 2 gives the first family of quantum LDPC codes with an efficient decoder that corrects a number of adversarial errors proportional to the minimum distance. Here that number is of order $\sqrt n$. The same analysis yields a robustness property: low-weight errors have syndromes of proportional weight (Corollary 9 of the paper). Later work on quantum expander codes builds on this analysis, for example on their decoding under random noise (arXiv:1711.08351) and on fault tolerance with constant overhead (arXiv:1808.03821).

Formalizing it. The result is proved on paper. As far as is known, it has no machine-checked proof. The mission produces a formal statement of the decoder and its correctness, and it also produces reusable pieces:

• unique-neighbour expansion;
• the distance of expander codes;
• the distance of hypergraph product codes, tied to an open item of the Tillich–Zémor mission;
• a generic formalization of greedy syndrome-weight decoding.

Difficulty

The obvious quantum analogue of Sipser–Spielman flips single qubits that lower the syndrome weight. It fails because of degeneracy: an error and its sum with a generator have the same syndrome. A small error can therefore look locally like a large one, and no single qubit need be worth flipping. The paper's decoder instead flips arbitrary patterns inside one generator. The difficulty is to show that some pattern always lowers the syndrome weight by a constant fraction of its size. The proof needs a combinatorial structure, the critical generator, whose existence uses unique-neighbour expansion on both sides of the graph, and a case analysis on its six parts. A second difficulty is that the decoder minimizes the syndrome weight, not the error weight, so the intermediate error can grow. Bounding that growth is what limits the guarantee to $w_0$ rather than the distance.

Formalization scope

• The graph is a relation adj : A → B → Prop on finite types, and $H$ = bipMatrix adj : Matrix B A (ZMod 2).
• The published TillichZemor.HGP.Setting is reused. The paper's $H_X$ is TillichZemor.HGP.hz H H and its $H_Z$ is hx H H; the X/Z names are swapped relative to the 2009 paper, and this is checked against eq. (5) in a sanity file.
• Qubits are (A × A) ⊕ (B × B), weights are hammingNorm, and $\mathcal C_Z^\perp$ is CodingTheory.dualCode of ker H_Z.
• Expansion constants are real and cardinalities are compared in $\mathbb R$. Distance statements are per-vector, so no $\infty$-valued minimum distance is cast to a real number.
• The decoder is defined once (Candidate, Step, Reach, DecodesCorrectly), generic in the syndrome and generator matrices. Its ratio is computed in $\mathbb Q$.
• Reach contains every state reachable under any tie-breaking. Correctness requires, at every reachable state, a further step while the syndrome is nonzero, and $e_O + e$ in the row space of the generator matrix once it is zero. Termination is automatic, because each step lowers a natural number.

Additions and omissions.

• The hypothesis $\Delta_A \ge 1$ is added throughout. With $\Delta_A = 0$ the expansion conditions are vacuous, $H = 0$, and every error is invisible.
• In Lemma 8 the vector $e_1$ is required to be nonzero. With $e_1 = 0$ the printed inequality reads $0 \ge 0$.
• Lemma 8 is posed in its first assertion only. The critical generator is taken with respect to a minimum-weight representative of the coset, as in Appendix B.
• The clauses "runs in time linear in the code length" and "letting $\Delta_A$, $\Delta_B$ be fixed and allowing $n_A, n_B$ to grow" are not formalized. The goal holds for every finite graph meeting the hypotheses.

Trivializing formalizations ruled out. The goal names the paper's own decoder, not "there exists a decoder", which a brute-force coset decoder would satisfy. It quantifies over every run, not a single favourable one. It asserts both never-failing and correctness, not partial correctness alone. It uses $H_X$ = hz H H, not the swapped matrix.

Welcome contributions. Proofs of the counting milestones (Lemma 3, Proposition 4, the column-weight bound, (19), (22)–(24)) are independent of one another. The distance bound of Tillich–Zémor, open on the platform, is the deepest dependency. Unique-neighbour expansion and the hypergraph-product distance bound are useful beyond this mission.

Selected references

• A. Leverrier, J.-P. Tillich, G. Zémor, Quantum expander codes, FOCS 2015; arXiv:1504.00822v1 (2015). https://arxiv.org/abs/1504.00822
• J.-P. Tillich, G. Zémor, Quantum LDPC codes with positive rate and minimum distance proportional to the square root of the blocklength, IEEE Trans. Inf. Theory 60(2), 2014; arXiv:0903.0566. https://arxiv.org/abs/0903.0566
• M. Sipser, D. A. Spielman, Expander codes, IEEE Trans. Inf. Theory 42(6), 1996. https://doi.org/10.1109/18.556667
• O. Fawzi, A. Grospellier, A. Leverrier, Efficient decoding of random errors for quantum expander codes, STOC 2018; arXiv:1711.08351. https://arxiv.org/abs/1711.08351
• O. Fawzi, A. Grospellier, A. Leverrier, Constant overhead quantum fault-tolerance with quantum expander codes, FOCS 2018; arXiv:1808.03821. https://arxiv.org/abs/1808.03821

Motivation

Many graph-colouring questions ask whether a proper colouring can be produced indirectly, from local data, instead of being assigned vertex by vertex. In the 1-2-3 Conjecture, the colours are produced by weighting the edges of a graph and colouring each vertex with the sum of the weights at it. Karoński, Łuczak and Thomason asked in 2004 whether weights from $\{1,2,3\}$ always suffice (J. Combin. Theory Ser. B 91 (2004)). The question started as a local version of the irregularity strength problem, where all vertices, not only adjacent ones, must receive different sums. It became one of the most studied problems on graph labellings. Surveys: Seamone (arXiv:1211.5122) and Grytczuk (DOI 10.1016/j.ejc.2020.103213).

Timeline.

• 2004: Karoński, Łuczak, Thomason state the conjecture and prove it for 3-colourable graphs.
• 2007: Addario-Berry, Dalal, McDiarmid, Reed and Thomason give the first finite bound, $k=30$; later $k=16$ (Addario-Berry et al.) and $k=13$ (Wang and Yu).
• 2010: Kalkowski, Karoński and Pfender reach $k=5$ (J. Combin. Theory Ser. B 100 (2010)).
• Before 2023: Przybyło proves the conjecture for $d$-regular graphs with $d\ge 10^8$ and for graphs with minimum degree $\delta(G)\ge C\log\Delta(G)$; Zhong proves it for graphs with minimum degree at least $0.99985|V|$ (references [20], [21], [31] of the paper).
• 2023: Keusch reaches $k=4$ with a maximum-cut and flow argument (Combinatorica 43 (2023), 651–658; reference [18] of the paper).
• 2024: Keusch proves the conjecture, $k=3$ (J. Combin. Theory Ser. B (2024), arXiv:2303.02611).

Setting

Let $G=(V,E)$ be a finite simple graph and write $N(v)$ for the neighbourhood of a vertex $v$. A $k$-edge-weighting is a function $\omega:E\to\{1,\dots,k\}$. The weighted degree of $v$ is

$$s_\omega(v)=\sum_{w\in N(v)}\omega(\{v,w\}).$$

Two adjacent vertices $v,w$ have a coloring conflict if $s_\omega(v)=s_\omega(w)$. The weighting is vertex-coloring if no edge is a coloring conflict, that is, if $s_\omega$ is a proper vertex colouring of $G$.

If $G$ has a connected component consisting of a single edge $\{v,w\}$ (a component isomorphic to $K_2$), then $s_\omega(v)=s_\omega(w)=\omega(\{v,w\})$ for every $\omega$, so no weighting is vertex-coloring. This is the only obstruction.

The proof uses a few further objects:

• for $W\subseteq V$, $\deg_W(v)=|N(v)\cap W|$;
• for disjoint $S,T\subseteq V$, the bipartite subgraph $G(S,T)$ with vertex set $S\cup T$ and the edges of $G$ between $S$ and $T$;
• a good R-B-partition (Definition 6): a partition $V=R\cup B$ with $R$ independent, $G(R,B)$ connected and $|B|$ even;
• a maximum cut $C=(S,T)$ and an auxiliary unit-capacity flow network $G_{C,F,\sigma}$ built from it (Lemma 4).

The Lean names are wdeg G ω v for $s_\omega(v)$, IsWeighting G k ω, IsVertexColoring G ω, NoK2Component G and IsGoodPartition G U R B.

Formalization targets

Goal: Theorem 1 (p. 2)

If no connected component of $G$ is isomorphic to $K_2$, then there is $\omega:E\to\{1,2,3\}$ with

$$\sum_{u\in N(v)}\omega(\{u,v\})\ne\sum_{u\in N(w)}\omega(\{u,w\})\qquad\text{for every edge }\{v,w\}\in E.$$

The connected case (p. 14)

Every finite connected graph with $|V|\ge 3$ has a vertex-coloring $\{1,2,3\}$-edge-weighting. This is the statement the case analysis of the proof establishes. Theorem 1 follows by treating each component separately.

Milestones along the proof

In the order the proof uses them:

• Lemma 2: an independent set $R$ with $G(R,V\setminus R)$ connected, alternating along a shortest path.
• Lemma 4: a flow of value $|F|$ in $G_{C,F,\sigma}$.
• Lemma 3: a weighting and odd designated colours $f$, proper on $G$, with $|s_\omega+h-f|=1$.
• Lemma 5: a bipartite weighting with prescribed parities on $R$ and exact weighted degrees on $B$, plus a second version with extra control along a fixed path.
• Lemmas 7, 8 and 9: the three basic situations in which a good R-B-partition of $G$, or of $G$ minus one vertex, yields a vertex-coloring weighting.
• Lemma 10: every connected graph of minimum degree at least $2$ has an edge whose removal, together with its two ends, leaves a connected graph.

Significance

The result. Theorem 1 settles a conjecture that was open for nineteen years. The constant is optimal: the triangle $K_3$ has no vertex-coloring $\{1,2\}$-weighting (two of its three edges get the same weight, and then two vertices tie), and deciding whether a vertex-coloring $\{1,2\}$-weighting exists is NP-complete (Dudek and Wajc, 2011). Theorem 1 also closes the sequence of upper bounds $30,16,13,6,5,4$ on the number of weights needed. Variants remain open: total weightings with vertex weights $\{1,2\}$ and edge weights $\{1,2\}$ (the 1-2 Conjecture), and list versions.

Formalizing it. The theorem is proved, in a 16-page paper. As far as is known it has no machine-checked proof. A formal proof would verify the case analysis at the end of the paper (pp. 11–14, about fifteen sub-cases with three auxiliary graphs), which is where errors in such arguments usually hide. The flow lemma is quoted from the 2023 paper and not reproved here. Formalizing it means proving an integral max-flow statement for a specific unit-capacity network, and the result can be reused for other flow-based weighting arguments.

Difficulty

The obvious approach is to fix the weights greedily, edge by edge or vertex by vertex. This fails because changing one edge weight changes two weighted degrees at once, so a repair at one vertex can create a conflict at a neighbour. With only three weights there is no room to absorb this. Every earlier bound above $3$ used the extra weight as slack.

The difficulty in the paper is parity. The construction needs the set $B$ of blue vertices to have even cardinality, and $|B|$ cannot always be made even. The proof therefore removes one or two vertices, applies one of three base lemmas, and re-inserts the vertices. That re-insertion may need one more round of weight changes along a path. Each sub-case has to keep track of parities, of exact weighted degrees on $B$, and of the connectivity of $G(R,B)$ simultaneously.

Formalization scope

Representation.

• Graphs are SimpleGraph V on a finite vertex type V with decidable adjacency. The paper's "graph" is a finite simple graph: weighted degrees are finite sums, and the proof uses a maximum cut and vertex orderings.
• An edge-weighting is a function ω : Sym2 V → ℕ on unordered pairs. IsWeighting G k ω requires $\omega(e)\in\{1,\dots,k\}$ for every edge $e$ of $G$; values on non-edges are unconstrained and never used.
• The weighted degree sums over G.neighborFinset v. Since $\{u,v\}=\{v,u\}$ in Sym2, the single sum equals both sides of Theorem 1's displayed inequality.
• "No component isomorphic to $K_2$" uses Mathlib's connected components and graph isomorphism. A sanity file proves it equivalent to "no edge both of whose ends have degree 1".
• $G(R,B)$ is Mathlib's G.between R B, induced on $R\cup B$ wherever that vertex set is not all of $V$.

Conventions that differ from the page. There are two, both disclosed in the item statements:

1. The vertex type is finite.
2. The flow of Lemma 4 is integral. The page says "an $s$-$t$-flow"; the paper uses integrality immediately afterwards, and the two versions are equivalent by the integrality theorem.

Lemma 5's condition $\alpha(v)\in\{2\deg(v)-1,2\deg(v),2\deg(v)+1\}$ is stated in $\mathbb Z$, and Lemma 3's $|s_\omega+h-f|=1$ is computed in $\mathbb Z$.

Ruled out. None of the following formalizations is faithful:

• weights allowed to be $0$, which deletes edges;
• weights constrained off the edges;
• the $K_2$ hypothesis strengthened to minimum degree at least $2$, or to connectivity;
• "adjacent vertices" replaced by "all pairs of vertices", which is the irregularity-strength problem.

Infrastructure. A complete development needs:

• spanning trees and parity arguments on trees (Lemma 5);
• depth-first search trees (Lemma 10);
• maximum cuts and an integral max-flow or augmenting-path argument for $G_{C,F,\sigma}$ (Lemma 4), together with path decompositions of unit flows (the proof of Lemma 3).

The flow and cut definitions are stated for arbitrary finite graphs and can be reused. Contributions are welcome at every level: proofs of individual lemmas, general flow-decomposition results, and the final case analysis.

Selected references

• R. Keusch, A Solution to the 1-2-3 Conjecture, J. Combin. Theory Ser. B, 2024. arXiv:2303.02611v4, DOI 10.1016/j.jctb.2024.01.002
• R. Keusch, Vertex-coloring graphs with 4-edge-weightings, Combinatorica 43 (2023), 651–658. Cited as [18] in arXiv:2303.02611v4.
• M. Karoński, T. Łuczak, A. Thomason, Edge weights and vertex colours, J. Combin. Theory Ser. B 91 (2004), 151–157. DOI 10.1016/j.jctb.2003.12.001
• M. Kalkowski, M. Karoński, F. Pfender, Vertex-coloring edge-weightings: towards the 1-2-3-conjecture, J. Combin. Theory Ser. B 100 (2010). DOI 10.1016/j.jctb.2009.06.002
• A. Dudek, D. Wajc, On the complexity of vertex-coloring edge-weightings, Discrete Math. Theor. Comput. Sci. 13 (2011), 45–50. Cited as [11] in arXiv:2303.02611v4.
• B. Seamone, The 1-2-3 Conjecture and related problems: a survey, 2012. arXiv:1211.5122
• J. Grytczuk, From the 1-2-3 Conjecture to the Riemann Hypothesis, European J. Combin. 91 (2021), 103213. DOI 10.1016/j.ejc.2020.103213

Motivation

Generalized Turán problems ask for the maximum number of copies of a fixed graph $H$ in an $n$-vertex graph that avoids a family $\mathcal F$ of forbidden subgraphs. The ordinary Turán number counts edges ($H = K_2$); Alon and Shikhelman (arXiv:1506.03397) started the systematic study of the general function $\mathrm{ex}(n, H, \mathcal F)$, building on earlier results of Erdős on cliques, Bollobás and Győri on pentagons in triangle-free graphs, and Győri and Li on triangles in graphs without a long odd or even cycle. Counting cycles in graphs with forbidden cycles is closely tied to extremal problems for Berge hypergraphs, and the constructions used are sparse hypergraphs of large girth.

Gerbner, Győri, Methuku and Vizer, Generalized Turán problems for even cycles (arXiv:1712.07079, J. Combin. Theory Ser. B, 2020), determine or bound $\mathrm{ex}(n, C_{\ell}, \mathcal F)$ for many cycle families. This mission covers one of their results in §6.2: the number of odd cycles $C_{2l+1}$ in a graph in which every shorter cycle is forbidden and, in addition, one longer odd cycle $C_{2k+1}$ is forbidden. Its companion (Theorem 17, a separate mission of this series) forbids a longer even cycle $C_{2k}$ instead, and there the paper obtains a sub-quadratic upper bound; with an odd extra cycle only a quadratic upper bound is proved.

Setting

All graphs are finite and simple. For an integer $a \ge 3$, $C_a$ is the cycle of length $a$. For a set $A$ of integers $a \ge 3$, write $\mathcal C_A = \{C_a : a \in A\}$; a graph is $\mathcal C_A$-free if it contains no $C_a$ with $a \in A$ as a (not necessarily induced) subgraph. The family $\mathcal C_{2l}$ consists of all cycles $C_3, C_4, \dots, C_{2l}$.

For graphs $H$ and $G$, $\mathcal N(H, G)$ is the number of copies of $H$ in $G$: subgraphs of $G$ isomorphic to $H$, counted without labelling. The generalized Turán number is

$$\mathrm{ex}(n, H, \mathcal F) = \max\{\mathcal N(H, G) : G \text{ has } n \text{ vertices and contains no member of } \mathcal F\}.$$

For a vertex $v$ of $G$, $N_i(v)$ is the set of vertices at distance exactly $i$ from $v$.

A hypergraph is a finite set of hyperedges (vertex sets); it is $r$-uniform if each hyperedge has $r$ vertices. A Berge cycle of length $j \ge 2$ is a sequence $v_1, h_1, v_2, h_2, \dots, v_j, h_j, v_1$ of distinct vertices and distinct hyperedges with $v_i, v_{i+1} \in h_i$ and $v_j, v_1 \in h_j$. The girth of a hypergraph is the length of its shortest Berge cycle; "girth at least $s$" means there is no Berge cycle of length $2, \dots, s-1$.

Formalization targets

Goal: Theorem 18

For all integers $k > l \ge 2$, as $n \to \infty$,

$$\Omega\big(n^{1+\frac{1}{2k+2}}\big) = \mathrm{ex}\big(n, C_{2l+1}, \mathcal C_{2l} \cup \{C_{2k+1}\}\big) = O(n^2).$$

Both the lower and the upper bound are part of the goal; the implied constants may depend on $k$ and $l$ only.

Milestones

1. Theorem 29 (Nešetřil–Rödl). For $r \ge 2$, $s \ge 3$ and all large $n$ there is an $r$-uniform hypergraph on $n$ vertices of girth at least $s$ with at least $n^{1+1/s}$ hyperedges.
2. The construction. Replacing each hyperedge of a $(2l+1)$-uniform hypergraph of girth at least $2k+2$ by a copy of $C_{2l+1}$ yields a graph with no cycle of length at most $2k+1$ other than $2l+1$, and with at least as many copies of $C_{2l+1}$ as hyperedges.
3. Cycles through a vertex. In a $\mathcal C_{2l} \cup \{C_{2k+1}\}$-free graph there is no edge inside $N_i(v)$ for $i < l$, every $C_{2l+1}$ through $v$ uses exactly one edge inside $N_l(v)$, and so the number of $C_{2l+1}$'s through $v$ is at most the number of edges inside $N_l(v)$.
4. Claim 19. In a $\mathcal C_{2l} \cup \{C_{2k+1}\}$-free graph the number of edges inside $N_l(v)$ is at most $C(k,l)\,|N_l(v)| \le C(k,l)\, n$.

The supporting published theorem erdos_gallai_path_conjecture (the Erdős–Gallai path theorem: a graph on $n$ vertices with no path of $m+1$ edges has at most $mn/2$ edges) is included as a reference item; the paper's proof of Claim 19 invokes it.

Significance

Theorem 18 shows that forbidding all cycles up to length $2l$ together with one odd cycle $C_{2k+1}$ still permits polynomially more than $n$ copies of $C_{2l+1}$, at least $n^{1 + 1/(2k+2)}$, and at most $O(n^2)$. Compared with Theorem 17, where an even cycle $C_{2k}$ is forbidden and the count is $O(n^{1+l/(l+1)})$, it isolates the role of the parity of the extra forbidden cycle. The authors conjecture that the true order is sub-quadratic (Conjecture 34, §8 of the paper), so the gap between the two exponents in Theorem 18 is a stated open question; a formal development of the known bounds is the base on which any improvement would be checked.

The result is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it produces: a reusable encoding of generalized Turán numbers for cycle families on top of Mathlib's copyCount; Berge cycles and the girth of uniform hypergraphs; distance layers $N_i(v)$; and a formal statement of the Nešetřil–Rödl existence theorem, which is used as a black box by many extremal constructions.

Difficulty

The upper bound requires careful bookkeeping of distance layers around a vertex in a graph without short cycles. The obvious estimate, bounding the copies of $C_{2l+1}$ through $v$ by the number of pairs of vertices of $N_l(v)$, gives only $|N_l(v)|^2$ per vertex and hence nothing better than the trivial bound overall; the content of Claim 19 is that forbidding the single cycle $C_{2k+1}$ makes the edge count inside $N_l(v)$ linear, and the parity of $2k+1$ is used essentially.

The lower bound rests on Theorem 29, a cited result that is not proved in the paper, and for which Mathlib has no supporting theory of uniform hypergraphs or Berge cycles. For the construction itself, the paper only asserts that the cycle-replacement graph has no short cycle other than the inserted $C_{2l+1}$'s; a cycle of the graph may wander through many hyperedges, and relating it to the girth of the hypergraph is the step a formal proof has to supply.

Formalization scope

• Vertices of an $n$-vertex graph are Fin n; graphs are SimpleGraph (Fin n). Cycles are Mathlib's SimpleGraph.cycleGraph, and $\mathcal N(H, G)$ is Mathlib's unlabelled copyCount.
• $\mathcal C_{2l} \cup \{C_{2k+1}\}$ is encoded as the set of lengths Set.Icc 3 (2 * l) ∪ {2 * k + 1}: every length $3, \dots, 2l$, not only $2l$.
• $\mathrm{ex}(n, H, \mathcal C_A)$ is the supremum of a nonempty finite set of natural numbers, hence a true maximum (checked in a sanity file).
• $N_i(v)$ uses the extended distance edist, so vertices of other components lie in no layer.
• Hypergraphs are Finset (Finset V); "girth at least $s$" is a predicate (no Berge cycle of length $2, \dots, s-1$), not an infimum, so a hypergraph without Berge cycles has every girth.
• $\Omega$ and $O$ are Mathlib's Asymptotics.IsBigO along atTop, with real exponents; both directions of the goal are stated.
• Claim 19's $O(\cdot)$ is a single constant chosen before $n$, the graph and the vertex. The milestone on cycles through $v$ uses the page's $\mathcal C_{2l} \cup \{C_{2k+1}\}$-freeness assumption.

A formalization that states only the upper bound, uses labelled copies, lets a constant depend on the graph, omits the short cycles $C_3, \dots, C_{2l-1}$ from the forbidden family, or defines $\mathrm{ex}$ by a supremum that can take a junk value, does not prove this theorem.

Contributions welcome: proofs of the milestones, a proof of Theorem 29, and general lemmas on breadth-first layers in graphs of large girth, which are reusable by the companion missions of this series.

Selected references

• D. Gerbner, E. Győri, A. Methuku, M. Vizer, Generalized Turán problems for even cycles, J. Combin. Theory Ser. B (2020); arXiv:1712.07079v3. https://arxiv.org/abs/1712.07079, https://doi.org/10.1016/j.jctb.2020.05.005
• N. Alon, C. Shikhelman, Many T copies in H-free graphs, J. Combin. Theory Ser. B 121 (2016). https://arxiv.org/abs/1506.03397
• J. Nešetřil, V. Rödl, On a probabilistic graph-theoretical method, Proc. Amer. Math. Soc. 72(2), 417–421 (1978). https://www.ams.org/journals/proc/1978-072-02/
• P. Erdős, T. Gallai, On maximal paths and circuits of graphs, Acta Math. Acad. Sci. Hungar. 10 (1959). https://doi.org/10.1007/BF02024498

Motivation

School and university timetabling is one of the oldest applications of combinatorial optimization. In his invited review An introduction to timetabling (European Journal of Operational Research, 1985), D. de Werra opens with the class–teacher model: classes meet teachers for a prescribed number of one-period lectures, and the lectures must be placed into periods or days so that no class and no teacher is overloaded. Every richer timetabling model of the review (preassignments, unavailabilities, course scheduling) is built on top of this one, and the review keeps returning to its graph-theoretic reading as an edge-colouring problem in a bipartite multigraph.

The model comes in three levels of demand. The daily problem asks for a clash-free timetable. The weekly problem asks for an assignment of lectures to days within daily load limits. The balanced weekly problem asks, in addition, that the load of every class and every teacher be spread as evenly as possible over the week, and that the lectures of each class–teacher pair be spread evenly too. The last one is the practical requirement that a teacher should not have all four lectures with one class on Monday.

Timeline (as cited in the review).

• 1916. D. König proves that a bipartite multigraph of maximum degree $\Delta$ can be edge-coloured with $\Delta$ colours. The review states it as Proposition 2.1, citing Berge's Graphes [1].
• 1975. D. de Werra, "A few remarks on chromatic scheduling" (reference [37] of the review), gives the balanced version: for every $p$ the edges of a bipartite multigraph can be $p$-coloured so that every node and every bundle of parallel edges is balanced. This is Proposition 2.3.
• 1978. D. de Werra, "Some comments on a note about timetabling" (INFOR, reference [38]), gives the weekly version with daily load limits, Proposition 2.2.
• 1985. The review collects the three results in matrix form as problems CT1, CT2 and CT3 and sketches a network-flow construction for CT3, citing Krarup [19].

Setting

There are $m$ classes $c_1,\dots,c_m$ and $n$ teachers $t_1,\dots,t_n$. The requirement matrix $R=(r_{ij})$ is an $m\times n$ matrix of nonnegative integers: $r_{ij}$ is the number of lectures class $c_i$ must have with teacher $t_j$. Write $r_{i\cdot}=\sum_j r_{ij}$ for the total load of class $c_i$ and $r_{\cdot j}=\sum_i r_{ij}$ for that of teacher $t_j$. For nonnegative integers $s$ and $p\ge1$, $\lfloor s/p\rfloor$ and $\lceil s/p\rceil$ are the floor and ceiling of the rational $s/p$.

A schedule over $p$ periods or days is an array $x=(x_{ijk})$ of nonnegative integers ($i\le m$, $j\le n$, $k\le p$) that places every lecture exactly once:

$$\sum_{k=1}^p x_{ijk}=r_{ij}\quad\text{for all } i,j. \tag{1}$$

• CT1 asks in addition that $x_{ijk}\in\{0,1\}$ and that $\sum_j x_{ijk}\le1$, $\sum_i x_{ijk}\le1$: no class and no teacher has two lectures in one period.
• CT2, given positive integers $a_i$, $b_j$, asks that $\sum_j x_{ijk}\le a_i$ and $\sum_i x_{ijk}\le b_j$ on every day $k$.
• CT3 asks that on every day $k$

$$\Big\lfloor \tfrac{r_{i\cdot}}{p}\Big\rfloor\le\sum_j x_{ijk}\le\Big\lceil \tfrac{r_{i\cdot}}{p}\Big\rceil,\quad \Big\lfloor \tfrac{r_{\cdot j}}{p}\Big\rfloor\le\sum_i x_{ijk}\le\Big\lceil \tfrac{r_{\cdot j}}{p}\Big\rceil,\quad \Big\lfloor \tfrac{r_{ij}}{p}\Big\rfloor\le x_{ijk}\le\Big\lceil \tfrac{r_{ij}}{p}\Big\rceil. \tag{8–10}$$

In the Lean development these are IsCT1 R p x, IsCT2 R p a b x and IsCT3 R p x, with the floor and ceiling written lo s p and hi s p and the totals rowSum R i, colSum R j.

Formalization targets

Goal: Proposition 2.3

$$\forall\,R\in\mathbb N^{m\times n},\ \forall\,p\ge1:\quad \exists\,x,\ \ x \text{ solves CT3 for } R \text{ over } p \text{ days}.$$

The statement fixes no constant: it asserts that perfectly balanced weekly timetables always exist.

Milestones

1. One balanced day (flow sketch, p. 153): for $p\ge1$ there is a matrix $y$ satisfying the bounds (8), (9), (10) at once.
2. The remaining days stay balanced (same sketch): if $p\ge2$ and $\lfloor s/p\rfloor\le y\le\lceil s/p\rceil$, then $\lfloor s/p\rfloor\le\lfloor (s-y)/(p-1)\rfloor$ and $\lceil (s-y)/(p-1)\rceil\le\lceil s/p\rceil$.
3. Proposition 2.1 (König): CT1 is solvable iff $r_{\cdot j}\le p$ and $r_{i\cdot}\le p$ for all $i,j$.
4. Proposition 2.2: CT2 is solvable iff $r_{\cdot j}\le p\,b_j$ and $r_{i\cdot}\le p\,a_i$.
5. Minimum number of days: CT2 is solvable over $p$ days iff $p\ge\max\big(\max_j\lceil r_{\cdot j}/b_j\rceil,\max_i\lceil r_{i\cdot}/a_i\rceil\big)$.
6. Figure 1: the printed timetable for $R=\begin{pmatrix}1&2&4\\3&0&2\end{pmatrix}$, $p=3$, solves CT3.

Significance

The result. Proposition 2.3 says that the balancing requirement costs nothing: whatever the requirement matrix, the week can be organised so that each class and each teacher has an essentially constant daily load and each class–teacher pair is spread evenly. It contains König's edge-colouring theorem (take $p$ at least the maximum degree, so every daily load is at most one) and the weekly Proposition 2.2 as special cases. Combined with Proposition 2.1 applied to each day, it reduces weekly timetabling to independent daily problems, which is the decomposition the review recommends ("one may start by solving the weekly problem … and then solve separately the resulting daily problems", p. 154). In graph language it is the existence of equitable edge colourings of bipartite multigraphs, a standard tool in scheduling and in the theory of edge colourings.

Formalizing it. All results of this mission are classical and proved in the literature; none of them is formalized on the platform. Mathlib contains Hall's marriage theorem but not König's edge-colouring theorem for bipartite multigraphs, and not balanced or equitable colourings. A complete development gives a machine-checked König edge-colouring theorem in matrix form, the matrix-rounding step with simultaneous row, column and entry bounds, and the balanced-colouring theorem itself.

Difficulty

Each family of constraints alone is easy: spreading a single number $r_{ij}$ evenly over $p$ days, or a single row total, is a matter of division with remainder. The difficulty is that one array must satisfy (1), (8), (9) and (10) simultaneously, so that the per-entry roundings must add up to correct roundings of every row total and every column total on every day. Rounding each entry independently breaks the row and column constraints, and greedy day-by-day choices can leave a remainder that no longer fits the bounds. The crux is integrality: the rational average $r_{ij}/p$ satisfies every bound on every day, but the problem asks for integers, and an integral one-day slice must round all entries, all row totals and all column totals consistently.

Formalization scope

Classes, teachers and days are Fin m, Fin n, Fin p; $R$ and $x$ are natural-number valued, which is the paper's "$x_{ijk}\ge0$ integer". Constraint (4) of CT1 is written $x_{ijk}\le1$. Floors and ceilings are Nat.floor and Nat.ceil of the rational quotient. In (8) and (9) they are applied to the row and column totals, never summed entrywise. The minimum number of days uses Finset.sup, whose empty value is $0$, and is stated as an equivalence ("solvable over $p$ days iff $p\ge p_{\min}$") rather than as an infimum.

Disclosed choices:

• The goal and the one-day milestone assume $p\ge1$; the paper's "for any $p$" means any number of days, and for $p=0$ Lean's division returns $0$.
• The remaining-days milestone assumes $p\ge2$ so that $p-1$ days remain.
• Propositions 2.1, 2.2 and the minimum-days statement hold for every $p$, including $p=0$, and assume nothing more than the page: $a_i,b_j$ positive.
• The edge-colouring and network-flow readings of the paper are stated in prose only; the formal statements are in matrix form, which is how the propositions are stated.

The formalization does not admit a trivial reading: CT3 requires all four constraint families at once, (1) is an equality, and the sanity checks show both that the Figure 1 data satisfy CT3 and that CT1 is not satisfiable for $R=(2)$ and $p=1$.

Useful infrastructure, reusable beyond this mission: integral flows with lower bounds, or total unimodularity of bipartite incidence matrices; König's edge-colouring theorem for bipartite multigraphs; floor and ceiling arithmetic for natural-number quotients. Proofs of any milestone, alternative proofs of the goal, and a sorry-free proof of the Figure 1 instance are all welcome.

Selected references

• D. de Werra, An introduction to timetabling, European Journal of Operational Research 19 (1985) 151–162. https://doi.org/10.1016/0377-2217(85)90167-5
• D. König, Über Graphen und ihre Anwendung auf Determinantentheorie und Mengenlehre, Mathematische Annalen 77 (1916) 453–465. https://doi.org/10.1007/BF01456961
• C. Berge, Graphes, Gauthier-Villars, Paris, 1983 (reference [1] of the review).
• D. de Werra, A few remarks on chromatic scheduling, in B. Roy (ed.), Combinatorial Programming: Methods and Applications, Reidel, Dordrecht, 1975, 337–342.
• D. de Werra, Some comments on a note about timetabling, INFOR 16 (1978) 90–92.
• J. Krarup, Chromatic optimisation: Limitations, objectives, uses, references, European Journal of Operational Research 11 (1982) 1–19.

Motivation

A Markov decision process with finitely many states and decisions, a discount factor $\beta\in(0,1)$ and the objective of minimizing expected discounted cost is the basic model of sequential decision making in operations research and reinforcement learning. It is solvable in polynomial time by linear programming. Papadimitriou and Tsitsiklis (Math. Oper. Res. 12(3), 1987) asked the finer question of whether it can be solved fast in parallel, and showed a sharp split: the general (stochastic) problem is P-complete (their Theorem 1), so it is unlikely to admit a polylogarithmic parallel algorithm, while the deterministic special case, where every transition probability is 0 or 1, is in NC (their Theorem 4).

The deterministic case is a shortest-path problem with a twist. Every policy traces a walk in a graph, and the cost of the walk counts its $t$-th arc with weight $\beta^t$. The paper's argument identifies the optimal discounted cost with the cost of a finite combinatorial object, a sigma, and computes it from discounted min-plus matrix products. This mission formalizes that identity.

Setting

A deterministic stationary Markov decision process consists of a finite set $S$ of $n$ states, an initial state $s_0\in S$, and for each state $s$ a finite nonempty set $D_s$ of decisions. Decision $i\in D_s$ costs $c(s,i)\in\mathbb R$ and leads with certainty to the state $\mathrm{next}(s,i)$. Equivalently, it is a directed graph on $S$ with an arc $s\to\mathrm{next}(s,i)$ of weight $c(s,i)$ for each decision; parallel arcs and loops are allowed.

A policy $\delta$ chooses a decision $\delta(s,t)\in D_s$ for every state $s$ and time $t=0,1,2,\dots$; it is stationary if $\delta(s,t)$ does not depend on $t$. From $s_0$ it produces the states $s_{t+1}=\mathrm{next}(s_t,\delta(s_t,t))$ and the discounted cost

$$J_\beta(\delta)=\sum_{t=0}^{\infty}\beta^t c\bigl(s_t,\delta(s_t,t)\bigr).$$

The optimal discounted cost is $J^*_\beta(s_0)=\inf_\delta J_\beta(\delta)$, the infimum over all policies $\delta(s,t)$.

A sigma is a walk $w_0=s_0,w_1,\dots,w_N$ along decisions $e_t\in D_{w_t}$ whose nodes $w_0,\dots,w_{N-1}$ are distinct and whose last node repeats an earlier one, $w_N=w_j$ with $j<N$: the walk from $s_0$ up to the first repetition of a node. It is a prefix of $j$ arcs followed by a cycle of $l=N-j\ge1$ arcs. Its discounted cost $c_\beta(P)$ is the discounted cost of the infinite walk that follows it and repeats its cycle forever.

In the min-plus semiring (addition is $\min$, multiplication is $+$, zero is $+\infty$), let $A_{uv}$ be the least cost of a decision from $u$ to $v$ ($+\infty$ if none), let $rA$ multiply every finite entry by $r$, and let

$$B_0=I,\qquad B_k=A\otimes\beta A\otimes\cdots\otimes\beta^{k-1}A ,$$

with $I$ the min-plus identity. The entry $(B_k)_{uv}$ is the least discounted cost $\sum_{t<k}\beta^t c_t$ of a $k$-arc walk from $u$ to $v$.

Formalization targets

Goal

For $0<\beta<1$,

$$J^*_\beta(s_0)=\min_{P\text{ sigma}}c_\beta(P)=\min\Bigl\{(B_k)_{s_0u}+\frac{\beta^{k}(B_l)_{uu}}{1-\beta^{l}}\;:\;u\in S,\ 0\le k\le n,\ 1\le l\le n,\ \text{both entries finite}\Bigr\},$$

with both minima attained. This is the claim on pp. 446–447 on which Theorem 4 rests. The algebraic expression is the corrected form of the paper's (see Formalization scope).

Milestones

1. The closed form of the cost of a sigma (p. 446): $c_\beta(P)=\sum_{t<j}\beta^tc_t+\frac{\beta^j}{1-\beta^l}\sum_{t<l}\beta^tc_{j+t}$.
2. A stationary optimal policy exists (§2, p. 444; cited on p. 446). The general finite stochastic statement is on the platform as BertsekasDP.discounted_main_theorem (Proved), and the deterministic case is stated in this mission's model.
3. The path of a stationary policy, cut at its first repeated node, is a sigma with the same discounted cost, and every sigma arises this way (p. 446).
4. The products $B_j$ are the cheapest discounted $j$-arc walks (p. 447).

Significance

The identity reduces an optimization over infinite objects, the time-dependent policies, to a minimum over finitely many closed-form expressions in matrix entries. Each $B_k$ is a product of $k$ min-plus matrices, and matrix products parallelize well; that is the source of the NC algorithm. The same reduction, with the discounting removed, underlies the minimum-mean-cycle characterization of the average-cost problem (mission II of this series), and the sigma structure reappears in the stationary finite-horizon analysis (mission IV).

On the formalization side, the result has been proved in the paper only as a short paragraph, which cites the existence of stationary optimal policies and leaves the algebra to the reader. Its printed formulas contain index slips (below). A machine-checked version fixes the exact constants. To our knowledge none of these statements has a formal proof. The existence of stationary optimal policies for finite discounted problems is formalized on the platform in Bertsekas's general stochastic setting.

Difficulty

The obvious argument says: an optimal policy may be taken stationary, a stationary deterministic policy produces an eventually periodic path, and an eventually periodic path is a sigma. The first step is the substantial one: the optimum is an infimum over all time-dependent policies $\delta(s,t)$, and a non-stationary policy can follow any walk at all, so this step is a statement about the whole dynamic program, not a combinatorial fact about a single walk. The second part of the goal adds a matching argument in the other direction: the expression ranges over arbitrary $k$-arc walks and closed $l$-walks, which need not be simple, so one must check that none of them beats the best sigma, and that the best sigma has $k\le n$ and $l\le n$. Finally, the discount factors must be tracked exactly; the printed formulas are off by one power of $\beta$ in two places.

Formalization scope

The Lean development lives in the namespace MDPComplexity.Discounted, with one definition file and five theorems. Conventions committed to:

• The model is stationary and deterministic. A DetMDP S has a finite state type, a nonempty finite decision type at each state (the paper says "a finite set $D_s$"; nonemptiness is implicit since a policy must choose a decision), a successor map and real costs.
• Policies are maps $\delta(s,t)$, time is $\mathbb N$ from $0$, and the optimum optDisc is the infimum over all such policies. Defining it over stationary policies or over sigmas would make the goal true by definition. That shortcut is ruled out, and the stationarity step is part of the content.
• Costs are tsums, which are junk ($0$) for non-summable series; every statement that sums costs assumes $0<\beta<1$, under which the series converge absolutely.
• A sigma is encoded as a lasso, $w_N=w_j$ with $j<N$. This includes $j=0$, a sigma whose cycle passes through $s_0$, which the printed form $(u_0,\dots,u_k,v_1,\dots,v_l,v_1)$ omits but the definition "a path from $u_0$ until the first repetition of a node" includes. The paper's $k$ is $j-1$.
• Corrected slips: (i) in the sigma display the cycle sum carries $\beta^{j-1}$, not $\beta^j$, for its $j$-th arc, and the indices are made consistent; (ii) the algorithm's expression is $\lambda+\beta^k\mu/(1-\beta^l)$ with $l\ge1$, not $\lambda+\beta^{k+1}\mu/(1+\beta^l)$ (one state with a loop of cost $1$ has optimum $1/(1-\beta)$, which the printed form misses); (iii) $B_0$, used but not defined, is the min-plus identity.
• Matrix entries are in Tropical (WithTop ℝ), so $+\infty$ is ⊤ and the product is Mathlib's matrix product over the tropical semiring.

Not formalized: membership in NC, the processor count $n^4$, the $\log^2 n+3\log n$ parallel time, and the P-completeness of the general problem. Mathlib has no parallel complexity classes. Only the identity that makes the algorithm correct is a target.

Contributions welcome: proofs of any milestone. A bridge from DetMDP to BertsekasSSPModel (taking decisions as controls and 0/1 transition rows) would let milestone 2 be derived from the platform's proved Proposition 7.3.1. A direct proof of the deterministic case is also welcome. The lasso and walk lemmas are reusable for the other missions of the series.

Selected references

• C. H. Papadimitriou and J. N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 441–450, 1987. https://doi.org/10.1287/moor.12.3.441
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, §7.3 (discounted problems, Proposition 7.3.1).
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, Ch. 6 (existence of stationary optimal policies for discounted models). https://doi.org/10.1002/9780470316887