---
OA_place: repository
_id: '21400'
abstract:
- lang: eng
text: 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.
article_processing_charge: No
arxiv: 1
author:
- first_name: Ivan
full_name: Sergeev, Ivan
id: ca3c9187-9a72-11ee-a009-8af825d896b0
last_name: Sergeev
orcid: 0009-0004-9145-8785
- first_name: Martin
full_name: Dvorak, Martin
id: 40ED02A8-C8B4-11E9-A9C0-453BE6697425
last_name: Dvorak
orcid: 0000-0001-5293-214X
- first_name: Cameron
full_name: Rampell, Cameron
last_name: Rampell
- first_name: Mark
full_name: Sandey, Mark
last_name: Sandey
- first_name: Pietro
full_name: Monticone, Pietro
last_name: Monticone
citation:
ama: 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
apa: 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
chicago: 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.
ieee: I. Sergeev, M. Dvorak, C. Rampell, M. Sandey, and P. Monticone, “A blueprint
for the formalization of Seymour’s matroid decomposition theorem,” arXiv.
.
ista: 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.
mla: Sergeev, Ivan, et al. “A Blueprint for the Formalization of Seymour’s Matroid
Decomposition Theorem.” ArXiv, doi:10.48550/arXiv.2601.01255.
short: I. Sergeev, M. Dvorak, C. Rampell, M. Sandey, P. Monticone, ArXiv (n.d.).
corr_author: '1'
date_created: 2026-03-04T12:09:26Z
date_published: 2026-01-03T00:00:00Z
date_updated: 2026-03-09T15:14:18Z
day: '03'
department:
- _id: GradSch
- _id: VlKo
doi: 10.48550/arXiv.2601.01255
external_id:
arxiv:
- '2601.01255'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2601.01255
month: '01'
oa: 1
oa_version: Preprint
page: '18'
publication: arXiv
publication_status: submitted
related_material:
link:
- relation: supplementary_material
url: https://ivan-sergeyev.github.io/seymour/blueprint.pdf
status: public
title: A blueprint for the formalization of Seymour's matroid decomposition theorem
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: preprint
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2026'
...
---
OA_place: repository
_id: '21398'
abstract:
- lang: eng
text: Seymour's decomposition theorem is a hallmark result in matroid theory presenting
a structural characterization of the class of regular matroids. Formalization
of matroid theory faces many challenges, most importantly that only a limited
number of notions and results have been implemented so far. In this work, we formalize
the proof of the forward (composition) direction of Seymour's theorem for regular
matroids. To this end, we develop a library in Lean 4 that implements definitions
and results about totally unimodular matrices, vector matroids, their standard
representations, regular matroids, and 1-, 2-, and 3-sums of matrices and binary
matroids given by their standard representations. Using this framework, we formally
state Seymour's decomposition theorem and implement a formally verified proof
of the composition direction in the setting where the matroids have finite rank
and may have infinite ground sets.
acknowledgement: "We would like to dedicate the paper to the memory of Klaus Truemper,
whose monograph Matroid Decomposition [12]\r\nlaid the foundation for our entire
work."
article_processing_charge: No
arxiv: 1
author:
- first_name: Martin
full_name: Dvorak, Martin
id: 40ED02A8-C8B4-11E9-A9C0-453BE6697425
last_name: Dvorak
orcid: 0000-0001-5293-214X
- first_name: Tristan
full_name: Figueroa-Reid, Tristan
last_name: Figueroa-Reid
- first_name: Rida
full_name: Hamadani, Rida
last_name: Hamadani
- first_name: Byung-Hak
full_name: Hwang, Byung-Hak
last_name: Hwang
- first_name: Evgenia
full_name: Karunus, Evgenia
last_name: Karunus
- first_name: Vladimir
full_name: Kolmogorov, Vladimir
id: 3D50B0BA-F248-11E8-B48F-1D18A9856A87
last_name: Kolmogorov
- first_name: Alexander
full_name: Meiburg, Alexander
last_name: Meiburg
- first_name: Alexander
full_name: Nelson, Alexander
last_name: Nelson
- first_name: Peter
full_name: Nelson, Peter
last_name: Nelson
- first_name: Mark
full_name: Sandey, Mark
last_name: Sandey
- first_name: Ivan
full_name: Sergeev, Ivan
id: ca3c9187-9a72-11ee-a009-8af825d896b0
last_name: Sergeev
orcid: 0009-0004-9145-8785
citation:
ama: Dvorak M, Figueroa-Reid T, Hamadani R, et al. Composition direction of Seymour’s
theorem for regular matroids — Formally verified. arXiv. doi:10.48550/arXiv.2509.20539
apa: Dvorak, M., Figueroa-Reid, T., Hamadani, R., Hwang, B.-H., Karunus, E., Kolmogorov,
V., … Sergeev, I. (n.d.). Composition direction of Seymour’s theorem for regular
matroids — Formally verified. arXiv. https://doi.org/10.48550/arXiv.2509.20539
chicago: Dvorak, Martin, Tristan Figueroa-Reid, Rida Hamadani, Byung-Hak Hwang,
Evgenia Karunus, Vladimir Kolmogorov, Alexander Meiburg, et al. “Composition Direction
of Seymour’s Theorem for Regular Matroids — Formally Verified.” ArXiv,
n.d. https://doi.org/10.48550/arXiv.2509.20539.
ieee: M. Dvorak et al., “Composition direction of Seymour’s theorem for regular
matroids — Formally verified,” arXiv. .
ista: Dvorak M, Figueroa-Reid T, Hamadani R, Hwang B-H, Karunus E, Kolmogorov V,
Meiburg A, Nelson A, Nelson P, Sandey M, Sergeev I. Composition direction of Seymour’s
theorem for regular matroids — Formally verified. arXiv, 10.48550/arXiv.2509.20539.
mla: Dvorak, Martin, et al. “Composition Direction of Seymour’s Theorem for Regular
Matroids — Formally Verified.” ArXiv, doi:10.48550/arXiv.2509.20539.
short: M. Dvorak, T. Figueroa-Reid, R. Hamadani, B.-H. Hwang, E. Karunus, V. Kolmogorov,
A. Meiburg, A. Nelson, P. Nelson, M. Sandey, I. Sergeev, ArXiv (n.d.).
corr_author: '1'
date_created: 2026-03-04T11:56:29Z
date_published: 2025-09-23T00:00:00Z
date_updated: 2026-03-27T12:36:59Z
day: '23'
department:
- _id: GradSch
- _id: VlKo
doi: 10.48550/arXiv.2509.20539
external_id:
arxiv:
- '2509.20539'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2509.20539
month: '09'
oa: 1
oa_version: Preprint
page: '21'
publication: arXiv
publication_status: draft
related_material:
record:
- id: '21393'
relation: dissertation_contains
status: public
status: public
title: Composition direction of Seymour's theorem for regular matroids — Formally
verified
type: preprint
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2025'
...