{"id":"palomar/PALOMAR-2026-10-21-000009","url":"https://github.com/jtraverso/nash-williams-lean/tree/2603197abdbf0a600ec663f6f046f70fbd209d4a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-21-000009-v1.json","repo":"https://github.com/jtraverso/nash-williams-lean","tags":["math.CO","msc:05C70","msc:05C35","graph-theory","triangle-decomposition","lean","formalization"],"score":0,"title":"The Nash–Williams triangle-decomposition theorem","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of the Nash–Williams theorem for large graphs proved by Delcourt and Postle: there is N such that every finite simple graph on n ≥ N vertices that is triangle-divisible (3 divides the number of edges and every degree is even) and has minimum degree at least 3n/4 has a triangle decomposition; together with Delcourt–Postle's fractional threshold (every graph with 3n ≤ 4δ has a fractional triangle decomposition) and their fractional stability theorem (with an additional order threshold). The proof follows their extremal/non-extremal case division but does not…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-21","reactions":{},"formalized":true,"formalizes":[{"title":"A Proof of Nash-Williams' Conjecture","identifier":"doi:10.48550/arXiv.2606.11178","relationship":"formalizes"},{"title":"Triangle decompositions I: Formalizing the Nash–Williams theorem in Lean","identifier":"","relationship":"formalizes"},{"title":"Triangle decompositions II: Robust absorption for typed triangles","identifier":"","relationship":"formalizes"}]}