Composition direction of Seymour's theorem for regular matroids

preprint Composition direction of Seymour's theorem for regular matroids — Formally verified draft Martin Dvorak author 40ED02A8-C8B4-11E9-A9C0-453BE66974250000-0001-5293-214X Tristan Figueroa-Reid author Rida Hamadani author Byung-Hak Hwang author Evgenia Karunus author Vladimir Kolmogorov author 3D50B0BA-F248-11E8-B48F-1D18A9856A87 Alexander Meiburg author Alexander Nelson author Peter Nelson author Mark Sandey author Ivan Sergeev author ca3c9187-9a72-11ee-a009-8af825d896b00009-0004-9145-8785 GradSch department VlKo department 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. 2025 eng arXiv 2509.2053910.48550/arXiv.2509.20539 https://research-explorer.ista.ac.at/record/21393 Dvorak M, Figueroa-Reid T, Hamadani R, et al. Composition direction of Seymour’s theorem for regular matroids — Formally verified. arXiv. doi:<a href="https://doi.org/10.48550/arXiv.2509.20539">10.48550/arXiv.2509.20539</a> 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. <a href="https://doi.org/10.48550/arXiv.2509.20539">https://doi.org/10.48550/arXiv.2509.20539</a>. M. Dvorak et al., “Composition direction of Seymour’s theorem for regular matroids — Formally verified,” arXiv. . 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. <a href="https://doi.org/10.48550/arXiv.2509.20539">https://doi.org/10.48550/arXiv.2509.20539</a> 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, 2509.20539. Dvorak, Martin, et al. “Composition Direction of Seymour’s Theorem for Regular Matroids — Formally Verified.” ArXiv, 2509.20539, doi:<a href="https://doi.org/10.48550/arXiv.2509.20539">10.48550/arXiv.2509.20539</a>. 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.). 213982026-03-04T11:56:29Z2026-07-29T12:56:51Z