A Blueprint for the Formalization of Seymour's Matroid Decomposition Theorem
Ivan Sergeev, Martin Dvorak, Cameron Rampell, Mark Sandey, Pietro Monticone
math.CO
Jan 3, 2026 · v1
TL;DR
A blueprint mapping the structural theory of regular matroids and Seymour's decomposition theorem to Lean declarations for an ongoing formalization.
Abstract
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 for the ongoing formalization effort and as a human-readable reference for the organization of the proof.
Problem
Seymour's matroid decomposition theorem, which characterizes regular matroids via decomposition into graphic, cographic, and R10 components, lacks a formal machine-checked proof.
Approach
The authors present a modular blueprint for formalizing the structural theory of regular matroids in Lean. They develop regularity via totally unimodular representations, prove regularity is preserved under 1-, 2-, and 3-sums, and establish regularity for graphic, cographic, and R10 matroids. The blueprint records logical structure, dependencies between results, and correspondence with Lean declarations.
Results
The blueprint covers the full logical structure of the decomposition theorem proof, with precise dependencies mapped to Lean declarations. It serves as both a formalization guide and a progress-tracking document for the ongoing Lean development.
