Saved in:
| Main Authors: | , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2509.20539 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911174318096384 |
|---|---|
| author | Dvorak, Martin Figueroa-Reid, Tristan Hamadani, Rida Hwang, Byung-Hak Karunus, Evgenia Kolmogorov, Vladimir Meiburg, Alexander Nelson, Alexander Nelson, Peter Sandey, Mark Sergeev, Ivan |
| author_facet | Dvorak, Martin Figueroa-Reid, Tristan Hamadani, Rida Hwang, Byung-Hak Karunus, Evgenia Kolmogorov, Vladimir Meiburg, Alexander Nelson, Alexander Nelson, Peter Sandey, Mark Sergeev, Ivan |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_20539 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified Dvorak, Martin Figueroa-Reid, Tristan Hamadani, Rida Hwang, Byung-Hak Karunus, Evgenia Kolmogorov, Vladimir Meiburg, Alexander Nelson, Alexander Nelson, Peter Sandey, Mark Sergeev, Ivan Combinatorics Logic in Computer Science 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. |
| title | Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified |
| topic | Combinatorics Logic in Computer Science |
| url | https://arxiv.org/abs/2509.20539 |