[{"related_material":{"link":[{"url":"https://ivan-sergeyev.github.io/seymour/blueprint.pdf","relation":"supplementary_material"}]},"tmp":{"short":"CC BY (4.0)","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)"},"corr_author":"1","article_processing_charge":"No","author":[{"id":"ca3c9187-9a72-11ee-a009-8af825d896b0","first_name":"Ivan","orcid":"0009-0004-9145-8785","last_name":"Sergeev","full_name":"Sergeev, Ivan"},{"last_name":"Dvorak","full_name":"Dvorak, Martin","id":"40ED02A8-C8B4-11E9-A9C0-453BE6697425","first_name":"Martin","orcid":"0000-0001-5293-214X"},{"full_name":"Rampell, Cameron","last_name":"Rampell","first_name":"Cameron"},{"full_name":"Sandey, Mark","last_name":"Sandey","first_name":"Mark"},{"full_name":"Monticone, Pietro","last_name":"Monticone","first_name":"Pietro"}],"department":[{"_id":"GradSch"},{"_id":"VlKo"}],"month":"01","oa":1,"doi":"10.48550/arXiv.2601.01255","date_created":"2026-03-04T12:09:26Z","title":"A blueprint for the formalization of Seymour's matroid decomposition theorem","oa_version":"Preprint","arxiv":1,"publication_status":"submitted","license":"https://creativecommons.org/licenses/by/4.0/","status":"public","page":"18","date_updated":"2026-03-09T15:14:18Z","publication":"arXiv","date_published":"2026-01-03T00:00:00Z","OA_place":"repository","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2601.01255"}],"year":"2026","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","day":"03","citation":{"chicago":"Sergeev, Ivan, Martin Dvorak, Cameron Rampell, Mark Sandey, and Pietro Monticone. “A Blueprint for the Formalization of Seymour’s Matroid Decomposition Theorem.” <i>ArXiv</i>, n.d. <a href=\"https://doi.org/10.48550/arXiv.2601.01255\">https://doi.org/10.48550/arXiv.2601.01255</a>.","ama":"Sergeev I, Dvorak M, Rampell C, Sandey M, Monticone P. A blueprint for the formalization of Seymour’s matroid decomposition theorem. <i>arXiv</i>. doi:<a href=\"https://doi.org/10.48550/arXiv.2601.01255\">10.48550/arXiv.2601.01255</a>","ista":"Sergeev I, Dvorak M, Rampell C, Sandey M, Monticone P. A blueprint for the formalization of Seymour’s matroid decomposition theorem. arXiv, <a href=\"https://doi.org/10.48550/arXiv.2601.01255\">10.48550/arXiv.2601.01255</a>.","apa":"Sergeev, I., Dvorak, M., Rampell, C., Sandey, M., &#38; Monticone, P. (n.d.). A blueprint for the formalization of Seymour’s matroid decomposition theorem. <i>arXiv</i>. <a href=\"https://doi.org/10.48550/arXiv.2601.01255\">https://doi.org/10.48550/arXiv.2601.01255</a>","mla":"Sergeev, Ivan, et al. “A Blueprint for the Formalization of Seymour’s Matroid Decomposition Theorem.” <i>ArXiv</i>, doi:<a href=\"https://doi.org/10.48550/arXiv.2601.01255\">10.48550/arXiv.2601.01255</a>.","ieee":"I. Sergeev, M. Dvorak, C. Rampell, M. Sandey, and P. Monticone, “A blueprint for the formalization of Seymour’s matroid decomposition theorem,” <i>arXiv</i>. .","short":"I. Sergeev, M. Dvorak, C. Rampell, M. Sandey, P. Monticone, ArXiv (n.d.)."},"language":[{"iso":"eng"}],"_id":"21400","abstract":[{"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.","lang":"eng"}],"external_id":{"arxiv":["2601.01255"]},"type":"preprint"},{"external_id":{"arxiv":["2509.20539"]},"_id":"21398","language":[{"iso":"eng"}],"abstract":[{"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.","lang":"eng"}],"publication_status":"draft","type":"preprint","citation":{"mla":"Dvorak, Martin, 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>.","ieee":"M. Dvorak <i>et al.</i>, “Composition direction of Seymour’s theorem for regular matroids — Formally verified,” <i>arXiv</i>. .","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.).","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. <i>arXiv</i>. <a href=\"https://doi.org/10.48550/arXiv.2509.20539\">https://doi.org/10.48550/arXiv.2509.20539</a>","ama":"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>","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, <a href=\"https://doi.org/10.48550/arXiv.2509.20539\">10.48550/arXiv.2509.20539</a>.","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.” <i>ArXiv</i>, n.d. <a href=\"https://doi.org/10.48550/arXiv.2509.20539\">https://doi.org/10.48550/arXiv.2509.20539</a>."},"day":"23","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","year":"2025","arxiv":1,"date_created":"2026-03-04T11:56:29Z","title":"Composition direction of Seymour's theorem for regular matroids — Formally verified","OA_place":"repository","date_published":"2025-09-23T00:00:00Z","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2509.20539","open_access":"1"}],"oa_version":"Preprint","doi":"10.48550/arXiv.2509.20539","oa":1,"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.","author":[{"id":"40ED02A8-C8B4-11E9-A9C0-453BE6697425","first_name":"Martin","orcid":"0000-0001-5293-214X","last_name":"Dvorak","full_name":"Dvorak, Martin"},{"first_name":"Tristan","last_name":"Figueroa-Reid","full_name":"Figueroa-Reid, Tristan"},{"full_name":"Hamadani, Rida","last_name":"Hamadani","first_name":"Rida"},{"last_name":"Hwang","full_name":"Hwang, Byung-Hak","first_name":"Byung-Hak"},{"first_name":"Evgenia","full_name":"Karunus, Evgenia","last_name":"Karunus"},{"full_name":"Kolmogorov, Vladimir","last_name":"Kolmogorov","id":"3D50B0BA-F248-11E8-B48F-1D18A9856A87","first_name":"Vladimir"},{"first_name":"Alexander","full_name":"Meiburg, Alexander","last_name":"Meiburg"},{"first_name":"Alexander","last_name":"Nelson","full_name":"Nelson, Alexander"},{"full_name":"Nelson, Peter","last_name":"Nelson","first_name":"Peter"},{"first_name":"Mark","full_name":"Sandey, Mark","last_name":"Sandey"},{"id":"ca3c9187-9a72-11ee-a009-8af825d896b0","first_name":"Ivan","orcid":"0009-0004-9145-8785","full_name":"Sergeev, Ivan","last_name":"Sergeev"}],"publication":"arXiv","date_updated":"2026-03-27T12:36:59Z","month":"09","department":[{"_id":"GradSch"},{"_id":"VlKo"}],"article_processing_charge":"No","corr_author":"1","status":"public","page":"21","related_material":{"record":[{"status":"public","id":"21393","relation":"dissertation_contains"}]}}]