A blueprint for the formalization of Seymour's matroid decomposition theorem

Sergeev, Ivan; Dvorak, Martin; Rampell, Cameron; Sandey, Mark; Monticone, Pietro

A blueprint for the formalization of Seymour's matroid decomposition theorem

Sergeev I, Dvorak M, Rampell C, Sandey M, Monticone P. A blueprint for the formalization of Seymour’s matroid decomposition theorem. arXiv, 10.48550/arXiv.2601.01255.

Download (ext.)

https://doi.org/10.48550/arXiv.2601.01255 [Preprint]

DOI

10.48550/arXiv.2601.01255

Preprint | Submitted | English

Author

Sergeev, Ivan^ISTA ; Dvorak, Martin^ISTA ; Rampell, Cameron; Sandey, Mark; Monticone, Pietro

Corresponding author has ISTA affiliation

Department

Graduate School
Kolmogorov Group

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 R10. 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.

Publishing Year

2026

Date Published

2026-01-03

Journal Title

arXiv

Page

IST-REx-ID

21400

Cite this

Sergeev I, Dvorak M, Rampell C, Sandey M, Monticone P. A blueprint for the formalization of Seymour’s matroid decomposition theorem. arXiv. doi:10.48550/arXiv.2601.01255

Sergeev, I., Dvorak, M., Rampell, C., Sandey, M., & Monticone, P. (n.d.). A blueprint for the formalization of Seymour’s matroid decomposition theorem. arXiv. https://doi.org/10.48550/arXiv.2601.01255

Sergeev, Ivan, Martin Dvorak, Cameron Rampell, Mark Sandey, and Pietro Monticone. “A Blueprint for the Formalization of Seymour’s Matroid Decomposition Theorem.” ArXiv, n.d. https://doi.org/10.48550/arXiv.2601.01255.

I. Sergeev, M. Dvorak, C. Rampell, M. Sandey, and P. Monticone, “A blueprint for the formalization of Seymour’s matroid decomposition theorem,” arXiv. .

Sergeev I, Dvorak M, Rampell C, Sandey M, Monticone P. A blueprint for the formalization of Seymour’s matroid decomposition theorem. arXiv, 10.48550/arXiv.2601.01255.

Sergeev, Ivan, et al. “A Blueprint for the Formalization of Seymour’s Matroid Decomposition Theorem.” ArXiv, doi:10.48550/arXiv.2601.01255.

All files available under the following license(s):

Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):