Composition direction of Seymour's theorem for regular matroids — Formally verified Dvorak, Martin ; https://orcid.org/0000-0001-5293-214X Figueroa-Reid, Tristan Hamadani, Rida Hwang, Byung-Hak Karunus, Evgenia Kolmogorov, Vladimir Meiburg, Alexander Nelson, Alexander Nelson, Peter Sandey, Mark Sergeev, Ivan ; https://orcid.org/0009-0004-9145-8785 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 info:eu-repo/semantics/preprint doc-type:preprint text http://purl.org/coar/resource_type/c_816b https://research-explorer.ista.ac.at/record/21398 Dvorak M, Figueroa-Reid T, Hamadani R, et al. Composition direction of Seymour’s theorem for regular matroids — Formally verified. <i>arXiv</i>. doi:<a href="https://doi.org/10.48550/arXiv.2509.20539">10.48550/arXiv.2509.20539</a> eng info:eu-repo/semantics/altIdentifier/doi/10.48550/arXiv.2509.20539 info:eu-repo/semantics/altIdentifier/arxiv/2509.20539 info:eu-repo/semantics/openAccess