[{"OA_place":"repository","date_created":"2026-03-04T12:09:26Z","author":[{"first_name":"Ivan","id":"ca3c9187-9a72-11ee-a009-8af825d896b0","last_name":"Sergeev","orcid":"0009-0004-9145-8785","full_name":"Sergeev, Ivan"},{"last_name":"Dvorak","orcid":"0000-0001-5293-214X","id":"40ED02A8-C8B4-11E9-A9C0-453BE6697425","first_name":"Martin","full_name":"Dvorak, Martin"},{"first_name":"Cameron","last_name":"Rampell","full_name":"Rampell, Cameron"},{"last_name":"Sandey","first_name":"Mark","full_name":"Sandey, Mark"},{"full_name":"Monticone, Pietro","last_name":"Monticone","first_name":"Pietro"}],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2601.01255"}],"publication_status":"submitted","_id":"21400","article_processing_charge":"No","related_material":{"link":[{"relation":"supplementary_material","url":"https://ivan-sergeyev.github.io/seymour/blueprint.pdf"}]},"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"}],"doi":"10.48550/arXiv.2601.01255","department":[{"_id":"GradSch"},{"_id":"VlKo"}],"citation":{"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>.","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>","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>","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>. .","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>.","short":"I. Sergeev, M. Dvorak, C. Rampell, M. Sandey, P. Monticone, ArXiv (n.d.)."},"page":"18","status":"public","corr_author":"1","title":"A blueprint for the formalization of Seymour's matroid decomposition theorem","day":"03","external_id":{"arxiv":["2601.01255"]},"oa":1,"oa_version":"Preprint","type":"preprint","publication":"arXiv","arxiv":1,"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","year":"2026","month":"01","date_published":"2026-01-03T00:00:00Z","language":[{"iso":"eng"}],"license":"https://creativecommons.org/licenses/by/4.0/","date_updated":"2026-03-09T15:14:18Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"}},{"department":[{"_id":"GradSch"},{"_id":"VlKo"}],"doi":"10.15479/AT-ISTA-21393","file_date_updated":"2026-03-04T09:03:37Z","abstract":[{"lang":"eng","text":"This thesis documents a voyage towards truth and beauty via formal verification of theorems. To this end, we develop libraries in Lean 4 that present definitions and results from diverse areas of MathematiCS (i.e., Mathematics and Computer Science). The aim is to create code that is understandable, believable, useful, and elegant. The code should stand for itself as much as possible without a need for documentation; however, this text redundantly documents our code artifacts and provides additional context that isn’t present in the code. This thesis is written for readers who know Lean 4 but are not familiar with any of the topics presented. We manifest truth and beauty in three formalized areas of MathematiCS.\r\n\r\nWe formalize general grammars in Lean 4 and use grammars to show closure of the class of type-0 languages under four operations; union, reversal, concatenation, and the Kleene star.\r\n\r\nOur second stop is the theory of optimization. Farkas established that a system of linear inequalities has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the inequalities. We state and formally prove several Farkas-like theorems over linearly ordered fields in Lean 4. Furthermore, we extend duality theory to the case when some coefficients are allowed to take “infinite values”. Additionally, we develop the basics of the theory of optimization in terms of the framework called General-Valued Constraint Satisfaction Problems, and we prove that, if a Rational-Valued Constraint Satisfaction Problem template has symmetric fractional polymorphisms of all arities, then its basic LP relaxation is tight.\r\n\r\nOur third stop is matroid theory. Seymour’s decomposition theorem is a hallmark result in matroid theory, presenting a structural characterization of the class of regular matroids. We aim to formally verify Seymour’s theorem in Lean 4. First, we build a library for working with totally unimodular matrices. We define binary matroids and their standard representations, and we prove that they form a matroid in the sense how Mathlib defines matroids. We define regular matroids to be matroids for which there exists a full representation rational matrix that is totally unimodular, and we prove that all regular matroids are binary. We define 1-sum, 2-sum, and 3 sum of binary matroids as specific ways to compose their standard representation matrices. We prove that the 1-sum, the 2-sum, and the 3-sum of regular matroids are a regular matroid, which concludes the composition direction of the Seymour’s theorem. The (more difficult) decomposition direction remains unproved.\r\n\r\nIn the pursuit of truth, we focus on identifying the trusted code in each project and presenting it faithfully. We emphasize the readability and believability of definitions rather than choosing definitions that are easier to work with. In search for beauty, we focus on the philosophical framework of Roger Scruton, who emphasizes that beauty is not a mere decoration but, most importantly, beauty is the means for shaping our place in the world and a source of redemption, where it can be viewed as a substitute for religion."}],"article_processing_charge":"No","_id":"21393","related_material":{"link":[{"description":"Full version of all definitions, statements, and proofs for Chapter 3.1 (Linear duality)","url":"https://github.com/madvorak/duality/tree/v3.5.0","relation":"software"},{"relation":"software","url":"https://github.com/madvorak/vcsp/tree/v8.2.0","description":"Full version of all definitions, statements, and proofs for Chapter 3.2 (Valued Constraint Satisfaction Problems)"},{"relation":"software","description":"Full version of all definitions, statements, and proofs for Chapter 4 (Seymour project)","url":"https://github.com/Ivan-Sergeyev/seymour/tree/v1.2.0"},{"relation":"software","url":"https://github.com/madvorak/chomsky/tree/v1.2.0","description":"Full version of all definitions, statements, and proofs for Chapter 5 (Theory of grammars)"},{"description":"Old version (Lean 3) of the project about grammars","url":"https://github.com/madvorak/grammars","relation":"software"},{"relation":"software","url":"https://github.com/madvorak/preliminaries/blob/main/Preliminaries.lean","description":"Demonstration of (minimal) requirements for selected algebraic classes used in my Ph.D. thesis"}],"record":[{"id":"13120","status":"public","relation":"part_of_dissertation"},{"status":"public","relation":"part_of_dissertation","id":"21398"},{"status":"public","relation":"part_of_dissertation","id":"20071"}]},"alternative_title":["ISTA Thesis"],"publication_identifier":{"issn":["2663-337X"],"isbn":["978-3-99078-074-9"]},"degree_awarded":"PhD","publication_status":"published","ddc":["511","000"],"has_accepted_license":"1","author":[{"full_name":"Dvorak, Martin","first_name":"Martin","id":"40ED02A8-C8B4-11E9-A9C0-453BE6697425","orcid":"0000-0001-5293-214X","last_name":"Dvorak"}],"OA_place":"repository","date_created":"2026-03-04T09:26:46Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"date_updated":"2026-03-27T12:37:00Z","language":[{"iso":"eng"}],"date_published":"2026-03-04T00:00:00Z","month":"03","year":"2026","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","supervisor":[{"last_name":"Kolmogorov","id":"3D50B0BA-F248-11E8-B48F-1D18A9856A87","first_name":"Vladimir","full_name":"Kolmogorov, Vladimir"},{"full_name":"Blanchette, Jasmin","last_name":"Blanchette","first_name":"Jasmin"}],"type":"dissertation","publisher":"Institute of Science and Technology Austria","oa_version":"Published Version","oa":1,"day":"04","title":"Pursuit of truth and beauty in Lean 4 : Formally verified theory of grammars, optimization, matroids","corr_author":"1","status":"public","page":"160","citation":{"chicago":"Dvorak, Martin. “Pursuit of Truth and Beauty in Lean 4 : Formally Verified Theory of Grammars, Optimization, Matroids.” Institute of Science and Technology Austria, 2026. <a href=\"https://doi.org/10.15479/AT-ISTA-21393\">https://doi.org/10.15479/AT-ISTA-21393</a>.","ista":"Dvorak M. 2026. Pursuit of truth and beauty in Lean 4 : Formally verified theory of grammars, optimization, matroids. Institute of Science and Technology Austria.","apa":"Dvorak, M. (2026). <i>Pursuit of truth and beauty in Lean 4 : Formally verified theory of grammars, optimization, matroids</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT-ISTA-21393\">https://doi.org/10.15479/AT-ISTA-21393</a>","ama":"Dvorak M. Pursuit of truth and beauty in Lean 4 : Formally verified theory of grammars, optimization, matroids. 2026. doi:<a href=\"https://doi.org/10.15479/AT-ISTA-21393\">10.15479/AT-ISTA-21393</a>","ieee":"M. Dvorak, “Pursuit of truth and beauty in Lean 4 : Formally verified theory of grammars, optimization, matroids,” Institute of Science and Technology Austria, 2026.","mla":"Dvorak, Martin. <i>Pursuit of Truth and Beauty in Lean 4 : Formally Verified Theory of Grammars, Optimization, Matroids</i>. Institute of Science and Technology Austria, 2026, doi:<a href=\"https://doi.org/10.15479/AT-ISTA-21393\">10.15479/AT-ISTA-21393</a>.","short":"M. Dvorak, Pursuit of Truth and Beauty in Lean 4 : Formally Verified Theory of Grammars, Optimization, Matroids, Institute of Science and Technology Austria, 2026."},"file":[{"success":1,"file_id":"21394","date_updated":"2026-03-04T08:56:15Z","file_name":"2026_Dvorak_Martin_Thesis.pdf","access_level":"open_access","relation":"main_file","creator":"mdvorak","date_created":"2026-03-04T08:56:15Z","file_size":1771231,"content_type":"application/pdf","checksum":"cface6dc18152680962b5361575f6e4f"},{"creator":"mdvorak","date_created":"2026-03-04T09:03:37Z","date_updated":"2026-03-04T09:03:37Z","file_id":"21395","access_level":"closed","file_name":"2026_Dvorak_Martin_Thesis.docx","relation":"source_file","file_size":864585,"checksum":"290ddfacfb7e07fb07e6f0b334e67c90","content_type":"application/vnd.openxmlformats-officedocument.wordprocessingml.document"}]},{"intvolume":"       209","acknowledgement":"We thank the anonymous reviewers for their careful reading of our manuscript and their many insightful comments and suggestions. Open access funding provided by Institute of Science and Technology (IST Austria).","author":[{"orcid":"0000-0001-5293-214X","last_name":"Dvorak","id":"40ED02A8-C8B4-11E9-A9C0-453BE6697425","first_name":"Martin","full_name":"Dvorak, Martin"},{"first_name":"Vladimir","last_name":"Kolmogorov","id":"3D50B0BA-F248-11E8-B48F-1D18A9856A87","full_name":"Kolmogorov, Vladimir"}],"date_created":"2021-09-27T10:48:23Z","OA_place":"publisher","ddc":["004"],"has_accepted_license":"1","publication_status":"published","article_processing_charge":"Yes (via OA deal)","_id":"10045","publication_identifier":{"eissn":["1436-4646"],"issn":["0025-5610"]},"keyword":["minimum 0-extension problem","metric labeling problem","discrete metric spaces","metric extensions","computational complexity","valued constraint satisfaction problems","discrete convex analysis","L-convex functions"],"OA_type":"hybrid","file_date_updated":"2025-04-16T09:36:08Z","abstract":[{"text":"Given a fixed finite metric space (V,μ), the {\\em minimum 0-extension problem}, denoted as 0-Ext[μ], is equivalent to the following optimization problem: minimize function of the form minx∈Vn∑ifi(xi)+∑ijcijμ(xi,xj) where cij,cvi are given nonnegative costs and fi:V→R are functions given by fi(xi)=∑v∈Vcviμ(xi,v). The computational complexity of 0-Ext[μ] has been recently established by Karzanov and by Hirai: if metric μ is {\\em orientable modular} then 0-Ext[μ] can be solved in polynomial time, otherwise 0-Ext[μ] is NP-hard. To prove the tractability part, Hirai developed a theory of discrete convex functions on orientable modular graphs generalizing several known classes of functions in discrete convex analysis, such as L♮-convex functions. We consider a more general version of the problem in which unary functions fi(xi) can additionally have terms of the form cuv;iμ(xi,{u,v}) for {u,v}∈F, where set F⊆(V2) is fixed. We extend the complexity classification above by providing an explicit condition on (μ,F) for the problem to be tractable. In order to prove the tractability part, we generalize Hirai's theory and define a larger class of discrete convex functions. It covers, in particular, another well-known class of functions, namely submodular functions on an integer lattice. Finally, we improve the complexity of Hirai's algorithm for solving 0-Ext on orientable modular graphs.\r\n","lang":"eng"}],"scopus_import":"1","department":[{"_id":"GradSch"},{"_id":"VlKo"}],"doi":"10.1007/s10107-024-02064-5","page":"279-322","citation":{"ama":"Dvorak M, Kolmogorov V. Generalized minimum 0-extension problem and discrete convexity. <i>Mathematical Programming</i>. 2025;209:279-322. doi:<a href=\"https://doi.org/10.1007/s10107-024-02064-5\">10.1007/s10107-024-02064-5</a>","apa":"Dvorak, M., &#38; Kolmogorov, V. (2025). Generalized minimum 0-extension problem and discrete convexity. <i>Mathematical Programming</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10107-024-02064-5\">https://doi.org/10.1007/s10107-024-02064-5</a>","chicago":"Dvorak, Martin, and Vladimir Kolmogorov. “Generalized Minimum 0-Extension Problem and Discrete Convexity.” <i>Mathematical Programming</i>. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/s10107-024-02064-5\">https://doi.org/10.1007/s10107-024-02064-5</a>.","ista":"Dvorak M, Kolmogorov V. 2025. Generalized minimum 0-extension problem and discrete convexity. Mathematical Programming. 209, 279–322.","mla":"Dvorak, Martin, and Vladimir Kolmogorov. “Generalized Minimum 0-Extension Problem and Discrete Convexity.” <i>Mathematical Programming</i>, vol. 209, Springer Nature, 2025, pp. 279–322, doi:<a href=\"https://doi.org/10.1007/s10107-024-02064-5\">10.1007/s10107-024-02064-5</a>.","short":"M. Dvorak, V. Kolmogorov, Mathematical Programming 209 (2025) 279–322.","ieee":"M. Dvorak and V. Kolmogorov, “Generalized minimum 0-extension problem and discrete convexity,” <i>Mathematical Programming</i>, vol. 209. Springer Nature, pp. 279–322, 2025."},"article_type":"original","file":[{"checksum":"25d9bd490719b45eca84f4d93a06c69f","content_type":"application/pdf","file_size":839510,"date_created":"2025-04-16T09:36:08Z","creator":"dernst","relation":"main_file","file_name":"2025_MathProgramming_Dvorak.pdf","file_id":"19578","access_level":"open_access","success":1,"date_updated":"2025-04-16T09:36:08Z"}],"status":"public","title":"Generalized minimum 0-extension problem and discrete convexity","corr_author":"1","quality_controlled":"1","oa_version":"Published Version","oa":1,"external_id":{"isi":["001176563300001"],"arxiv":["2109.10203"]},"day":"01","isi":1,"publisher":"Springer Nature","publication":"Mathematical Programming","type":"journal_article","volume":209,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","arxiv":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"date_updated":"2025-05-19T13:52:10Z","date_published":"2025-01-01T00:00:00Z","language":[{"iso":"eng"}],"month":"01","year":"2025"},{"publication":"arXiv","_id":"21399","article_processing_charge":"No","type":"preprint","publication_status":"submitted","language":[{"iso":"eng"}],"date_published":"2025-12-16T00:00:00Z","date_updated":"2026-03-12T08:36:21Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"doi":"10.48550/arXiv.2512.07087","year":"2025","department":[{"_id":"GradSch"},{"_id":"VlKo"}],"month":"12","abstract":[{"text":"We report on the Equational Theories Project (ETP), an online collaborative pilot project to explore new ways to collaborate in mathematics with machine assistance. The project successfully determined all 22 028 942 edges of the implication graph between the 4694 simplest equational laws on magmas, by a combination of human-generated and automated proofs, all validated by the formal proof assistant language Lean. As a result of this project, several new constructions of magmas satisfying specific laws were discovered, and several auxiliary questions were also addressed, such as the effect of restricting attention to finite magmas.","lang":"eng"}],"arxiv":1,"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","status":"public","citation":{"ista":"Bolan M, Breitner J, Brox J, Carlini N, Carneiro M, Doorn F van, Dvorak M, Goens A, Hill A, Husum H, Mejia HI, Kocsis ZA, Floch BL, Bar-on A, Luccioli L, McNeil D, Meiburg A, Monticone P, Nielsen PP, Osazuwa EO, Paolini G, Petracci M, Reinke B, Renshaw D, Rossel M, Roux C, Scanvic J, Srinivas S, Tadipatri AR, Tao T, Tsyrklevich V, Vaquerizo-Villar F, Weber D, Zheng F. The equational theories project: Advancing collaborative mathematical research at scale. arXiv, <a href=\"https://doi.org/10.48550/arXiv.2512.07087\">10.48550/arXiv.2512.07087</a>.","chicago":"Bolan, Matthew, Joachim Breitner, Jose Brox, Nicholas Carlini, Mario Carneiro, Floris van Doorn, Martin Dvorak, et al. “The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale.” <i>ArXiv</i>, n.d. <a href=\"https://doi.org/10.48550/arXiv.2512.07087\">https://doi.org/10.48550/arXiv.2512.07087</a>.","apa":"Bolan, M., Breitner, J., Brox, J., Carlini, N., Carneiro, M., Doorn, F. van, … Zheng, F. (n.d.). The equational theories project: Advancing collaborative mathematical research at scale. <i>arXiv</i>. <a href=\"https://doi.org/10.48550/arXiv.2512.07087\">https://doi.org/10.48550/arXiv.2512.07087</a>","ama":"Bolan M, Breitner J, Brox J, et al. The equational theories project: Advancing collaborative mathematical research at scale. <i>arXiv</i>. doi:<a href=\"https://doi.org/10.48550/arXiv.2512.07087\">10.48550/arXiv.2512.07087</a>","ieee":"M. Bolan <i>et al.</i>, “The equational theories project: Advancing collaborative mathematical research at scale,” <i>arXiv</i>. .","mla":"Bolan, Matthew, et al. “The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale.” <i>ArXiv</i>, doi:<a href=\"https://doi.org/10.48550/arXiv.2512.07087\">10.48550/arXiv.2512.07087</a>.","short":"M. Bolan, J. Breitner, J. Brox, N. Carlini, M. Carneiro, F. van Doorn, M. Dvorak, A. Goens, A. Hill, H. Husum, H.I. Mejia, Z.A. Kocsis, B.L. Floch, A. Bar-on, L. Luccioli, D. McNeil, A. Meiburg, P. Monticone, P.P. Nielsen, E.O. Osazuwa, G. Paolini, M. Petracci, B. Reinke, D. Renshaw, M. Rossel, C. Roux, J. Scanvic, S. Srinivas, A.R. Tadipatri, T. Tao, V. Tsyrklevich, F. Vaquerizo-Villar, D. Weber, F. Zheng, ArXiv (n.d.)."},"oa_version":"Preprint","day":"16","external_id":{"arxiv":["2512.07087"]},"oa":1,"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2512.07087","open_access":"1"}],"author":[{"last_name":"Bolan","first_name":"Matthew","full_name":"Bolan, Matthew"},{"first_name":"Joachim","last_name":"Breitner","full_name":"Breitner, Joachim"},{"first_name":"Jose","last_name":"Brox","full_name":"Brox, Jose"},{"full_name":"Carlini, Nicholas","last_name":"Carlini","first_name":"Nicholas"},{"full_name":"Carneiro, Mario","last_name":"Carneiro","first_name":"Mario"},{"last_name":"Doorn","first_name":"Floris van","full_name":"Doorn, Floris van"},{"full_name":"Dvorak, Martin","orcid":"0000-0001-5293-214X","last_name":"Dvorak","id":"40ED02A8-C8B4-11E9-A9C0-453BE6697425","first_name":"Martin"},{"full_name":"Goens, Andrés","last_name":"Goens","first_name":"Andrés"},{"first_name":"Aaron","last_name":"Hill","full_name":"Hill, Aaron"},{"full_name":"Husum, Harald","last_name":"Husum","first_name":"Harald"},{"full_name":"Mejia, Hernán Ibarra","first_name":"Hernán Ibarra","last_name":"Mejia"},{"first_name":"Zoltan A.","last_name":"Kocsis","full_name":"Kocsis, Zoltan A."},{"full_name":"Floch, Bruno Le","last_name":"Floch","first_name":"Bruno Le"},{"full_name":"Bar-on, Amir","first_name":"Amir","last_name":"Bar-on"},{"full_name":"Luccioli, Lorenzo","first_name":"Lorenzo","last_name":"Luccioli"},{"full_name":"McNeil, Douglas","last_name":"McNeil","first_name":"Douglas"},{"full_name":"Meiburg, Alex","first_name":"Alex","last_name":"Meiburg"},{"last_name":"Monticone","first_name":"Pietro","full_name":"Monticone, Pietro"},{"first_name":"Pace P.","last_name":"Nielsen","full_name":"Nielsen, Pace P."},{"full_name":"Osazuwa, Emmanuel Osalotioman","last_name":"Osazuwa","first_name":"Emmanuel Osalotioman"},{"first_name":"Giovanni","last_name":"Paolini","full_name":"Paolini, Giovanni"},{"last_name":"Petracci","first_name":"Marco","full_name":"Petracci, Marco"},{"full_name":"Reinke, Bernhard","first_name":"Bernhard","last_name":"Reinke"},{"full_name":"Renshaw, David","last_name":"Renshaw","first_name":"David"},{"first_name":"Marcus","last_name":"Rossel","full_name":"Rossel, Marcus"},{"full_name":"Roux, Cody","last_name":"Roux","first_name":"Cody"},{"full_name":"Scanvic, Jérémy","last_name":"Scanvic","first_name":"Jérémy"},{"last_name":"Srinivas","first_name":"Shreyas","full_name":"Srinivas, Shreyas"},{"last_name":"Tadipatri","first_name":"Anand Rao","full_name":"Tadipatri, Anand Rao"},{"full_name":"Tao, Terence","first_name":"Terence","last_name":"Tao"},{"last_name":"Tsyrklevich","first_name":"Vlad","full_name":"Tsyrklevich, Vlad"},{"full_name":"Vaquerizo-Villar, Fernando","first_name":"Fernando","last_name":"Vaquerizo-Villar"},{"full_name":"Weber, Daniel","last_name":"Weber","first_name":"Daniel"},{"first_name":"Fan","last_name":"Zheng","full_name":"Zheng, Fan"}],"title":"The equational theories project: Advancing collaborative mathematical research at scale","date_created":"2026-03-04T12:00:16Z","OA_place":"repository"},{"publication":"arXiv","_id":"21398","related_material":{"record":[{"id":"21393","status":"public","relation":"dissertation_contains"}]},"article_processing_charge":"No","type":"preprint","publication_status":"draft","date_published":"2025-09-23T00:00:00Z","language":[{"iso":"eng"}],"date_updated":"2026-03-27T12:36:59Z","doi":"10.48550/arXiv.2509.20539","year":"2025","month":"09","department":[{"_id":"GradSch"},{"_id":"VlKo"}],"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"}],"arxiv":1,"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","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.","status":"public","page":"21","citation":{"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>","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>","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>.","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>.","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.).","ieee":"M. Dvorak <i>et al.</i>, “Composition direction of Seymour’s theorem for regular matroids — Formally verified,” <i>arXiv</i>. ."},"oa_version":"Preprint","external_id":{"arxiv":["2509.20539"]},"day":"23","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2509.20539"}],"oa":1,"author":[{"full_name":"Dvorak, Martin","first_name":"Martin","id":"40ED02A8-C8B4-11E9-A9C0-453BE6697425","last_name":"Dvorak","orcid":"0000-0001-5293-214X"},{"full_name":"Figueroa-Reid, Tristan","first_name":"Tristan","last_name":"Figueroa-Reid"},{"full_name":"Hamadani, Rida","first_name":"Rida","last_name":"Hamadani"},{"full_name":"Hwang, Byung-Hak","first_name":"Byung-Hak","last_name":"Hwang"},{"last_name":"Karunus","first_name":"Evgenia","full_name":"Karunus, Evgenia"},{"id":"3D50B0BA-F248-11E8-B48F-1D18A9856A87","last_name":"Kolmogorov","first_name":"Vladimir","full_name":"Kolmogorov, Vladimir"},{"full_name":"Meiburg, Alexander","last_name":"Meiburg","first_name":"Alexander"},{"last_name":"Nelson","first_name":"Alexander","full_name":"Nelson, Alexander"},{"full_name":"Nelson, Peter","first_name":"Peter","last_name":"Nelson"},{"first_name":"Mark","last_name":"Sandey","full_name":"Sandey, Mark"},{"full_name":"Sergeev, Ivan","first_name":"Ivan","orcid":"0009-0004-9145-8785","last_name":"Sergeev","id":"ca3c9187-9a72-11ee-a009-8af825d896b0"}],"title":"Composition direction of Seymour's theorem for regular matroids — Formally verified","date_created":"2026-03-04T11:56:29Z","corr_author":"1","OA_place":"repository"},{"language":[{"iso":"eng"}],"date_published":"2024-09-12T00:00:00Z","date_updated":"2026-03-27T12:36:59Z","year":"2024","month":"09","arxiv":1,"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","publication":"arXiv","type":"preprint","oa_version":"Preprint","day":"12","external_id":{"arxiv":["2409.08119"]},"oa":1,"title":"Duality theory in linear optimization and its extensions -- formally  verified","corr_author":"1","article_number":"2409.08119","status":"public","citation":{"chicago":"Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization and Its Extensions -- Formally  Verified.” <i>ArXiv</i>, n.d. <a href=\"https://doi.org/10.48550/arXiv.2409.08119\">https://doi.org/10.48550/arXiv.2409.08119</a>.","ista":"Dvorak M, Kolmogorov V. Duality theory in linear optimization and its extensions -- formally  verified. arXiv, 2409.08119.","ama":"Dvorak M, Kolmogorov V. Duality theory in linear optimization and its extensions -- formally  verified. <i>arXiv</i>. doi:<a href=\"https://doi.org/10.48550/arXiv.2409.08119\">10.48550/arXiv.2409.08119</a>","apa":"Dvorak, M., &#38; Kolmogorov, V. (n.d.). Duality theory in linear optimization and its extensions -- formally  verified. <i>arXiv</i>. <a href=\"https://doi.org/10.48550/arXiv.2409.08119\">https://doi.org/10.48550/arXiv.2409.08119</a>","ieee":"M. Dvorak and V. Kolmogorov, “Duality theory in linear optimization and its extensions -- formally  verified,” <i>arXiv</i>. .","mla":"Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization and Its Extensions -- Formally  Verified.” <i>ArXiv</i>, 2409.08119, doi:<a href=\"https://doi.org/10.48550/arXiv.2409.08119\">10.48550/arXiv.2409.08119</a>.","short":"M. Dvorak, V. Kolmogorov, ArXiv (n.d.)."},"doi":"10.48550/arXiv.2409.08119","department":[{"_id":"GradSch"},{"_id":"VlKo"}],"abstract":[{"text":"Farkas established that a system of linear inequalities has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the inequalities. We state and formally prove several Farkas-like theorems over linearly ordered fields in Lean 4. Furthermore, we extend duality theory to the case when some coefficients are allowed to take \"infinite values\".","lang":"eng"}],"OA_type":"green","_id":"20071","article_processing_charge":"No","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"21393"}],"link":[{"relation":"software","url":"https://github.com/madvorak/duality/tree/v3.2","description":"full version of all definitions, statement, and proofs"}]},"keyword":["Farkas lemma","linear programming","extended reals","calculus of inductive constructions"],"publication_status":"draft","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2409.08119","open_access":"1"}],"author":[{"full_name":"Dvorak, Martin","first_name":"Martin","orcid":"0000-0001-5293-214X","last_name":"Dvorak","id":"40ED02A8-C8B4-11E9-A9C0-453BE6697425"},{"full_name":"Kolmogorov, Vladimir","id":"3D50B0BA-F248-11E8-B48F-1D18A9856A87","last_name":"Kolmogorov","first_name":"Vladimir"}],"date_created":"2025-07-23T11:21:52Z","OA_place":"repository","acknowledgement":"We would like to thank David Bartl and Jasmin Blanchette for frequent consultations. We would also like to express gratitude to Andrew Yang for the proof of Finset.univ sum of zero when not and to Henrik B¨oving for a help with generalization from extended rationals to extended linearly ordered fields. We would also like to acknowledge Antoine Chambert-Loir, Apurva Nakade, Ya¨el Dillies, Richard Copley, Edward van de Meent, Markus Himmel, Mario Carneiro, and Kevin Buzzard."},{"acknowledgement":"Jasmin Blanchette: This research has received funding from the Netherlands Organization\r\nfor Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).\r\n__\r\nWe thank Vladimir Kolmogorov for making this collaboration possible. We\r\nthank Václav Končický for discussing ideas about the Kleene star construction. We thank Patrick Johnson, Floris van Doorn, and Damiano Testa for their small yet very valuable contributions to our code. We thank Eric Wieser for simplifying one of our proofs. We thank Mark Summerfield for suggesting textual improvements. We thank the anonymous reviewers for very helpful comments. Finally, we thank the Lean community for helping us with various technical issues and answering many questions. ","intvolume":"       268","date_created":"2023-06-05T07:29:05Z","author":[{"full_name":"Dvorak, Martin","id":"40ED02A8-C8B4-11E9-A9C0-453BE6697425","last_name":"Dvorak","orcid":"0000-0001-5293-214X","first_name":"Martin"},{"first_name":"Jasmin","last_name":"Blanchette","full_name":"Blanchette, Jasmin"}],"has_accepted_license":"1","ddc":["000"],"publication_status":"published","related_material":{"record":[{"id":"21393","relation":"dissertation_contains","status":"public"}],"link":[{"relation":"software","url":"https://github.com/madvorak/grammars/tree/publish"}]},"_id":"13120","article_processing_charge":"No","alternative_title":["LIPIcs"],"publication_identifier":{"isbn":["9783959772846"],"eissn":["1868-8969"]},"scopus_import":"1","file_date_updated":"2023-08-07T11:55:43Z","abstract":[{"text":"We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant. We defined basic notions of rewrite rules and of words derived by a grammar, and used grammars to show closure of the class of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star. The literature mostly focuses on Turing machine arguments, which are possibly more difficult to formalize. For the Kleene star, we could not follow the literature and came up with our own grammar-based construction.","lang":"eng"}],"department":[{"_id":"GradSch"},{"_id":"VlKo"}],"doi":"10.4230/LIPIcs.ITP.2023.15","conference":{"end_date":"2023-08-04","start_date":"2023-07-31","location":"Bialystok, Poland","name":"ITP: Interactive Theorem Proving"},"citation":{"chicago":"Dvorak, Martin, and Jasmin Blanchette. “Closure Properties of General Grammars - Formally Verified.” In <i>14th International Conference on Interactive Theorem Proving</i>, Vol. 268. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. <a href=\"https://doi.org/10.4230/LIPIcs.ITP.2023.15\">https://doi.org/10.4230/LIPIcs.ITP.2023.15</a>.","ista":"Dvorak M, Blanchette J. 2023. Closure properties of general grammars - formally verified. 14th International Conference on Interactive Theorem Proving. ITP: Interactive Theorem Proving, LIPIcs, vol. 268, 15.","apa":"Dvorak, M., &#38; Blanchette, J. (2023). Closure properties of general grammars - formally verified. In <i>14th International Conference on Interactive Theorem Proving</i> (Vol. 268). Bialystok, Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.ITP.2023.15\">https://doi.org/10.4230/LIPIcs.ITP.2023.15</a>","ama":"Dvorak M, Blanchette J. Closure properties of general grammars - formally verified. In: <i>14th International Conference on Interactive Theorem Proving</i>. Vol 268. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:<a href=\"https://doi.org/10.4230/LIPIcs.ITP.2023.15\">10.4230/LIPIcs.ITP.2023.15</a>","ieee":"M. Dvorak and J. Blanchette, “Closure properties of general grammars - formally verified,” in <i>14th International Conference on Interactive Theorem Proving</i>, Bialystok, Poland, 2023, vol. 268.","short":"M. Dvorak, J. Blanchette, in:, 14th International Conference on Interactive Theorem Proving, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.","mla":"Dvorak, Martin, and Jasmin Blanchette. “Closure Properties of General Grammars - Formally Verified.” <i>14th International Conference on Interactive Theorem Proving</i>, vol. 268, 15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, doi:<a href=\"https://doi.org/10.4230/LIPIcs.ITP.2023.15\">10.4230/LIPIcs.ITP.2023.15</a>."},"file":[{"file_size":715976,"content_type":"application/pdf","checksum":"773a0197f05b67feaa6cb1e17ec3642d","creator":"dernst","date_created":"2023-08-07T11:55:43Z","success":1,"file_name":"2023_LIPIcS_Dvorak.pdf","file_id":"13982","access_level":"open_access","date_updated":"2023-08-07T11:55:43Z","relation":"main_file"}],"status":"public","article_number":"15","corr_author":"1","title":"Closure properties of general grammars - formally verified","oa":1,"day":"27","external_id":{"arxiv":["2302.06420"],"isi":["001515590500015"]},"quality_controlled":"1","oa_version":"Published Version","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","isi":1,"type":"conference","publication":"14th International Conference on Interactive Theorem Proving","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","arxiv":1,"volume":268,"month":"07","year":"2023","date_updated":"2026-03-27T12:36:59Z","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"language":[{"iso":"eng"}],"date_published":"2023-07-27T00:00:00Z"},{"quality_controlled":"1","oa_version":"Published Version","external_id":{"arxiv":["2106.11247"]},"day":"29","oa":1,"title":"Massively winning configurations in the convex grabbing game on the plane","status":"public","file":[{"date_created":"2021-06-28T20:23:13Z","creator":"mdvorak","relation":"main_file","access_level":"open_access","date_updated":"2021-06-28T20:23:13Z","file_name":"Convex-Grabbing-Game_CCCG_proc_version.pdf","success":1,"file_id":"9616","checksum":"45accb1de9b7e0e4bb2fbfe5fd3e6239","content_type":"application/pdf","file_size":381306},{"creator":"kschuh","date_created":"2021-08-12T10:57:21Z","access_level":"open_access","file_name":"Convex-Grabbing-Game_FULL-VERSION.pdf","date_updated":"2021-08-12T10:57:21Z","file_id":"9902","success":1,"relation":"main_file","file_size":403645,"checksum":"9199cf18c65658553487458cc24d0ab2","content_type":"application/pdf"}],"citation":{"ieee":"M. Dvorak and S. Nicholson, “Massively winning configurations in the convex grabbing game on the plane,” in <i>Proceedings of the 33rd Canadian Conference on Computational Geometry</i>, Halifax, NS, Canada; Virtual, 2021.","mla":"Dvorak, Martin, and Sara Nicholson. “Massively Winning Configurations in the Convex Grabbing Game on the Plane.” <i>Proceedings of the 33rd Canadian Conference on Computational Geometry</i>, Canadian Conference on Computational Geometry, 2021.","short":"M. Dvorak, S. Nicholson, in:, Proceedings of the 33rd Canadian Conference on Computational Geometry, Canadian Conference on Computational Geometry, 2021.","ista":"Dvorak M, Nicholson S. 2021. Massively winning configurations in the convex grabbing game on the plane. Proceedings of the 33rd Canadian Conference on Computational Geometry. CCCG: Canadian Conference on Computational Geometry.","chicago":"Dvorak, Martin, and Sara Nicholson. “Massively Winning Configurations in the Convex Grabbing Game on the Plane.” In <i>Proceedings of the 33rd Canadian Conference on Computational Geometry</i>. Canadian Conference on Computational Geometry, 2021.","ama":"Dvorak M, Nicholson S. Massively winning configurations in the convex grabbing game on the plane. In: <i>Proceedings of the 33rd Canadian Conference on Computational Geometry</i>. Canadian Conference on Computational Geometry; 2021.","apa":"Dvorak, M., &#38; Nicholson, S. (2021). Massively winning configurations in the convex grabbing game on the plane. In <i>Proceedings of the 33rd Canadian Conference on Computational Geometry</i>. Halifax, NS, Canada; Virtual: Canadian Conference on Computational Geometry."},"language":[{"iso":"eng"}],"date_published":"2021-06-29T00:00:00Z","license":"https://creativecommons.org/licenses/by-nd/4.0/","tmp":{"short":"CC BY-ND (4.0)","image":"/image/cc_by_nd.png","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode"},"date_updated":"2025-05-14T11:23:45Z","year":"2021","month":"06","arxiv":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication":"Proceedings of the 33rd Canadian Conference on Computational Geometry","type":"conference","publisher":"Canadian Conference on Computational Geometry","ddc":["516"],"has_accepted_license":"1","author":[{"full_name":"Dvorak, Martin","first_name":"Martin","last_name":"Dvorak","orcid":"0000-0001-5293-214X","id":"40ED02A8-C8B4-11E9-A9C0-453BE6697425"},{"full_name":"Nicholson, Sara","first_name":"Sara","last_name":"Nicholson"}],"date_created":"2021-06-22T15:57:11Z","conference":{"location":"Halifax, NS, Canada; Virtual","name":"CCCG: Canadian Conference on Computational Geometry","end_date":"2021-08-12","start_date":"2021-08-10"},"department":[{"_id":"GradSch"},{"_id":"VlKo"}],"file_date_updated":"2021-08-12T10:57:21Z","abstract":[{"lang":"eng","text":"The convex grabbing game is a game where two players, Alice and Bob, alternate taking extremal points from the convex hull of a point set on the plane. Rational weights are given to the points. The goal of each player is to maximize the total weight over all points that they obtain. We restrict the setting to the case of binary weights. We show a construction of an arbitrarily large odd-sized point set that allows Bob to obtain almost 3/4 of the total weight. This construction answers a question asked by Matsumoto, Nakamigawa, and Sakuma in [Graphs and Combinatorics, 36/1 (2020)]. We also present an arbitrarily large even-sized point set where Bob can obtain the entirety of the total weight. Finally, we discuss conjectures about optimum moves in the convex grabbing game for both players in general."}],"_id":"9592","article_processing_charge":"No","keyword":["convex grabbing game","graph grabbing game","combinatorial game","convex geometry"],"publication_status":"published"}]