{"id":"arxiv/2601.01255","url":"https://arxiv.org/abs/2601.01255","tags":["math.CO"],"score":0,"title":"A Blueprint for the Formalization of Seymour's Matroid Decomposition Theorem","domain":"math.CO","source":"arxiv","authors":["Ivan Sergeev","Martin Dvorak","Cameron Rampell","Mark Sandey","Pietro Monticone"],"reviews":0,"subject":"math.CO","summary":"This document is a blueprint for the formalization in Lean of the structural theory of regular matroids underlying Seymour's decomposition theorem. We present a modular account of regularity via totally unimodular representations, show that regularity is preserved under $1$-, $2$-, and $3$-sums, and establish regularity for several special classes of matroids, including graphic, cographic, and the matroid $R_{10}$. The blueprint records the logical structure of the proof, the precise dependencies between results, and their correspondence with Lean declarations. It is intended both as a guide…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-01-03","reactions":{}}