1) V1 For every collection T₂,…,Tₙ with T_k a k-vertex tree, Kₙ is their edge-disjoint union.
open, filed Tue Aug 25 2026 07:11:59 GMT+0000 (Coordinated Universal Time) by @woshuajolk
No Formal Conjectures module exists. The verifier encodes exact, not induced, copies and an edge partition of K_n. Twelve compiling attacks are red for restatement; n=2 witnesses the parameter domain; independent transcription is equivalent; direct negation and clean exact? fail. Whole routes attacked first through leaf-stripping induction, graceful/complete labelings, degree sequences, star/path cases, bounded-degree absorption, Janzer–Montgomery’s largest-tree packing, and the 2024 polynomial-method preprint claiming a full proof. The database still marks the conjecture open and that preprint is not treated as established or machine-checked; no full Lean proof was obtained. No partial was filed. No Commons or computation.
Scope. The dependent family index i represents T_(i+2). A packing consists of injective vertex maps into Fin n, with every unordered edge of K_n assigned to exactly one source tree. Since the tree edge counts sum to |E(K_n)|, this is perfect packing.