OPG-46613: $P_3$ -partitions of cubic 3-connected graphs

Open

CubicP3Partition.root_problem

by hao jia · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricscubic-graphsgraph-theoryp3-factor

Let $V$ be a finite vertex type and let $G$ be a finite simple graph on $V$ . Assume that every vertex of $G$ has degree three, deletion of any set of at most two vertices leaves a connected induced graph, $|V|\ge4$ , and the number of vertices is divisible by three. Then the vertices can be partitioned into noninduced paths of length two:

\operatorname{Cubic}(G)\land\operatorname{ThreeVertexConnected}(G)\land 3\mid |V| \quad\Longrightarrow\quad \operatorname{Nonempty}(\operatorname{P3Factor}(G)).

Equivalently, when $|V|=3k$ , the factor consists of $k$ pairwise vertex-disjoint three-vertex paths covering every vertex. This is the mission's open main goal; no candidate milestone is presented as a proof of it.

Preamble

import Definitions.Def_cubic_p3_partition_models

Formal statement

namespace CubicP3Partition

universe u

/-- The divisible-order form of the cubic three-connected P3-packing problem. -/
theorem root_problem {V : Type u} [Fintype V] (G : SimpleGraph V)
    (hCubic : Cubic G) (hConnected : ThreeVertexConnected G)
    (hOrder : 3 ∣ Fintype.card V) :
    Nonempty (P3Factor G) := by sorry

end CubicP3Partition

Source

UnsolvedMath, OPG-46613, https://www.unsolvedmath.com/problems/OPG-46613; see also A. Kelmans, https://arxiv.org/abs/0910.2766v2, p. 3, Problem 1.10, and pp. 7–8, Theorem 3.1 claim (z1).

Read-back

What the Lean code literally says, in plain math · gpt-5.6-luna

对宇宙 $u$ 中的任意有限类型 $V$ （带有 Fintype V 实例）和任意简单图 $G$ ，在三个显式假设下，定理声明存在一个自然数 $b$ 和双射 $Fin\,b×Fin\,3≃V$ ，使对每个 $i∈Fin\,b$ ， $place(i,0)$ 与 $place(i,1)$ 相邻且 $place(i,1)$ 与 $place(i,2)$ 相邻。第一个假设 hCubic 是对每个 $v∈V$ ， $G$ 中以 $v$ 为起点的邻居 subtype 的自然数基数等于 $3$ ；第二个假设 hConnected 是合取： $4≤Fintype.card V$ ，并且对每个有限子集 $S⊆V$ ，若 $S.card≤2$ ，则 $G$ 在满足 $v∉S$ 的 subtype 上的诱导图连通；第三个假设 hOrder 是 $3∣Fintype.card V$ ，即存在自然数 $k$ 使 $Fintype.card V=3·k$ 。 $S$ 的量化包括空集和所有大小为一或二的有限子集；除这三个假设、有限性实例和图 $G$ 外，没有其他前提。

Human review

Endorsed by Shuze Chen · Sep 7, 2026
Endorsed by hao jia · Sep 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

OPG-46613: P3P_3P3​-partitions of cubic 3-connected graphs

OPG-46613: $P_3$ -partitions of cubic 3-connected graphs