---
OA_place: repository
_id: '21400'
abstract:
- lang: eng
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.
article_processing_charge: No
arxiv: 1
author:
- first_name: Ivan
full_name: Sergeev, Ivan
id: ca3c9187-9a72-11ee-a009-8af825d896b0
last_name: Sergeev
orcid: 0009-0004-9145-8785
- first_name: Martin
full_name: Dvorak, Martin
id: 40ED02A8-C8B4-11E9-A9C0-453BE6697425
last_name: Dvorak
orcid: 0000-0001-5293-214X
- first_name: Cameron
full_name: Rampell, Cameron
last_name: Rampell
- first_name: Mark
full_name: Sandey, Mark
last_name: Sandey
- first_name: Pietro
full_name: Monticone, Pietro
last_name: Monticone
citation:
ama: Sergeev I, Dvorak M, Rampell C, Sandey M, Monticone P. A blueprint for the
formalization of Seymour’s matroid decomposition theorem. arXiv. doi:10.48550/arXiv.2601.01255
apa: Sergeev, I., Dvorak, M., Rampell, C., Sandey, M., & Monticone, P. (n.d.).
A blueprint for the formalization of Seymour’s matroid decomposition theorem.
arXiv. https://doi.org/10.48550/arXiv.2601.01255
chicago: Sergeev, Ivan, Martin Dvorak, Cameron Rampell, Mark Sandey, and Pietro
Monticone. “A Blueprint for the Formalization of Seymour’s Matroid Decomposition
Theorem.” ArXiv, n.d. https://doi.org/10.48550/arXiv.2601.01255.
ieee: I. Sergeev, M. Dvorak, C. Rampell, M. Sandey, and P. Monticone, “A blueprint
for the formalization of Seymour’s matroid decomposition theorem,” arXiv.
.
ista: Sergeev I, Dvorak M, Rampell C, Sandey M, Monticone P. A blueprint for the
formalization of Seymour’s matroid decomposition theorem. arXiv, 10.48550/arXiv.2601.01255.
mla: Sergeev, Ivan, et al. “A Blueprint for the Formalization of Seymour’s Matroid
Decomposition Theorem.” ArXiv, doi:10.48550/arXiv.2601.01255.
short: I. Sergeev, M. Dvorak, C. Rampell, M. Sandey, P. Monticone, ArXiv (n.d.).
corr_author: '1'
date_created: 2026-03-04T12:09:26Z
date_published: 2026-01-03T00:00:00Z
date_updated: 2026-03-09T15:14:18Z
day: '03'
department:
- _id: GradSch
- _id: VlKo
doi: 10.48550/arXiv.2601.01255
external_id:
arxiv:
- '2601.01255'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2601.01255
month: '01'
oa: 1
oa_version: Preprint
page: '18'
publication: arXiv
publication_status: submitted
related_material:
link:
- relation: supplementary_material
url: https://ivan-sergeyev.github.io/seymour/blueprint.pdf
status: public
title: A blueprint for the formalization of Seymour's matroid decomposition theorem
tmp:
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)
short: CC BY (4.0)
type: preprint
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2026'
...
---
OA_place: repository
_id: '21393'
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."
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Martin
full_name: Dvorak, Martin
id: 40ED02A8-C8B4-11E9-A9C0-453BE6697425
last_name: Dvorak
orcid: 0000-0001-5293-214X
citation:
ama: 'Dvorak M. Pursuit of truth and beauty in Lean 4 : Formally verified theory
of grammars, optimization, matroids. 2026. doi:10.15479/AT-ISTA-21393'
apa: 'Dvorak, M. (2026). Pursuit of truth and beauty in Lean 4 : Formally verified
theory of grammars, optimization, matroids. Institute of Science and Technology
Austria. https://doi.org/10.15479/AT-ISTA-21393'
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. https://doi.org/10.15479/AT-ISTA-21393.'
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.'
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.'
mla: 'Dvorak, Martin. Pursuit of Truth and Beauty in Lean 4 : Formally Verified
Theory of Grammars, Optimization, Matroids. Institute of Science and Technology
Austria, 2026, doi:10.15479/AT-ISTA-21393.'
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.'
corr_author: '1'
date_created: 2026-03-04T09:26:46Z
date_published: 2026-03-04T00:00:00Z
date_updated: 2026-03-27T12:37:00Z
day: '04'
ddc:
- '511'
- '000'
degree_awarded: PhD
department:
- _id: GradSch
- _id: VlKo
doi: 10.15479/AT-ISTA-21393
file:
- access_level: open_access
checksum: cface6dc18152680962b5361575f6e4f
content_type: application/pdf
creator: mdvorak
date_created: 2026-03-04T08:56:15Z
date_updated: 2026-03-04T08:56:15Z
file_id: '21394'
file_name: 2026_Dvorak_Martin_Thesis.pdf
file_size: 1771231
relation: main_file
success: 1
- access_level: closed
checksum: 290ddfacfb7e07fb07e6f0b334e67c90
content_type: application/vnd.openxmlformats-officedocument.wordprocessingml.document
creator: mdvorak
date_created: 2026-03-04T09:03:37Z
date_updated: 2026-03-04T09:03:37Z
file_id: '21395'
file_name: 2026_Dvorak_Martin_Thesis.docx
file_size: 864585
relation: source_file
file_date_updated: 2026-03-04T09:03:37Z
has_accepted_license: '1'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
page: '160'
publication_identifier:
isbn:
- 978-3-99078-074-9
issn:
- 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
link:
- description: Full version of all definitions, statements, and proofs for Chapter
3.1 (Linear duality)
relation: software
url: https://github.com/madvorak/duality/tree/v3.5.0
- description: Full version of all definitions, statements, and proofs for Chapter
3.2 (Valued Constraint Satisfaction Problems)
relation: software
url: https://github.com/madvorak/vcsp/tree/v8.2.0
- description: Full version of all definitions, statements, and proofs for Chapter
4 (Seymour project)
relation: software
url: https://github.com/Ivan-Sergeyev/seymour/tree/v1.2.0
- description: Full version of all definitions, statements, and proofs for Chapter
5 (Theory of grammars)
relation: software
url: https://github.com/madvorak/chomsky/tree/v1.2.0
- description: Old version (Lean 3) of the project about grammars
relation: software
url: https://github.com/madvorak/grammars
- description: Demonstration of (minimal) requirements for selected algebraic classes
used in my Ph.D. thesis
relation: software
url: https://github.com/madvorak/preliminaries/blob/main/Preliminaries.lean
record:
- id: '13120'
relation: part_of_dissertation
status: public
- id: '21398'
relation: part_of_dissertation
status: public
- id: '20071'
relation: part_of_dissertation
status: public
status: public
supervisor:
- first_name: Vladimir
full_name: Kolmogorov, Vladimir
id: 3D50B0BA-F248-11E8-B48F-1D18A9856A87
last_name: Kolmogorov
- first_name: Jasmin
full_name: Blanchette, Jasmin
last_name: Blanchette
title: 'Pursuit of truth and beauty in Lean 4 : Formally verified theory of grammars,
optimization, matroids'
tmp:
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)
short: CC BY (4.0)
type: dissertation
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2026'
...
---
OA_place: publisher
OA_type: hybrid
_id: '10045'
abstract:
- lang: eng
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"
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).
article_processing_charge: Yes (via OA deal)
article_type: original
arxiv: 1
author:
- first_name: Martin
full_name: Dvorak, Martin
id: 40ED02A8-C8B4-11E9-A9C0-453BE6697425
last_name: Dvorak
orcid: 0000-0001-5293-214X
- first_name: Vladimir
full_name: Kolmogorov, Vladimir
id: 3D50B0BA-F248-11E8-B48F-1D18A9856A87
last_name: Kolmogorov
citation:
ama: Dvorak M, Kolmogorov V. Generalized minimum 0-extension problem and discrete
convexity. Mathematical Programming. 2025;209:279-322. doi:10.1007/s10107-024-02064-5
apa: Dvorak, M., & Kolmogorov, V. (2025). Generalized minimum 0-extension problem
and discrete convexity. Mathematical Programming. Springer Nature. https://doi.org/10.1007/s10107-024-02064-5
chicago: Dvorak, Martin, and Vladimir Kolmogorov. “Generalized Minimum 0-Extension
Problem and Discrete Convexity.” Mathematical Programming. Springer Nature,
2025. https://doi.org/10.1007/s10107-024-02064-5.
ieee: M. Dvorak and V. Kolmogorov, “Generalized minimum 0-extension problem and
discrete convexity,” Mathematical Programming, vol. 209. Springer Nature,
pp. 279–322, 2025.
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.” Mathematical Programming, vol. 209, Springer Nature,
2025, pp. 279–322, doi:10.1007/s10107-024-02064-5.
short: M. Dvorak, V. Kolmogorov, Mathematical Programming 209 (2025) 279–322.
corr_author: '1'
date_created: 2021-09-27T10:48:23Z
date_published: 2025-01-01T00:00:00Z
date_updated: 2025-05-19T13:52:10Z
day: '01'
ddc:
- '004'
department:
- _id: GradSch
- _id: VlKo
doi: 10.1007/s10107-024-02064-5
external_id:
arxiv:
- '2109.10203'
isi:
- '001176563300001'
file:
- access_level: open_access
checksum: 25d9bd490719b45eca84f4d93a06c69f
content_type: application/pdf
creator: dernst
date_created: 2025-04-16T09:36:08Z
date_updated: 2025-04-16T09:36:08Z
file_id: '19578'
file_name: 2025_MathProgramming_Dvorak.pdf
file_size: 839510
relation: main_file
success: 1
file_date_updated: 2025-04-16T09:36:08Z
has_accepted_license: '1'
intvolume: ' 209'
isi: 1
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
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 279-322
publication: Mathematical Programming
publication_identifier:
eissn:
- 1436-4646
issn:
- 0025-5610
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Generalized minimum 0-extension problem and discrete convexity
tmp:
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)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 209
year: '2025'
...
---
OA_place: repository
_id: '21399'
abstract:
- lang: eng
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.
article_processing_charge: No
arxiv: 1
author:
- first_name: Matthew
full_name: Bolan, Matthew
last_name: Bolan
- first_name: Joachim
full_name: Breitner, Joachim
last_name: Breitner
- first_name: Jose
full_name: Brox, Jose
last_name: Brox
- first_name: Nicholas
full_name: Carlini, Nicholas
last_name: Carlini
- first_name: Mario
full_name: Carneiro, Mario
last_name: Carneiro
- first_name: Floris van
full_name: Doorn, Floris van
last_name: Doorn
- first_name: Martin
full_name: Dvorak, Martin
id: 40ED02A8-C8B4-11E9-A9C0-453BE6697425
last_name: Dvorak
orcid: 0000-0001-5293-214X
- first_name: Andrés
full_name: Goens, Andrés
last_name: Goens
- first_name: Aaron
full_name: Hill, Aaron
last_name: Hill
- first_name: Harald
full_name: Husum, Harald
last_name: Husum
- first_name: Hernán Ibarra
full_name: Mejia, Hernán Ibarra
last_name: Mejia
- first_name: Zoltan A.
full_name: Kocsis, Zoltan A.
last_name: Kocsis
- first_name: Bruno Le
full_name: Floch, Bruno Le
last_name: Floch
- first_name: Amir
full_name: Bar-on, Amir
last_name: Bar-on
- first_name: Lorenzo
full_name: Luccioli, Lorenzo
last_name: Luccioli
- first_name: Douglas
full_name: McNeil, Douglas
last_name: McNeil
- first_name: Alex
full_name: Meiburg, Alex
last_name: Meiburg
- first_name: Pietro
full_name: Monticone, Pietro
last_name: Monticone
- first_name: Pace P.
full_name: Nielsen, Pace P.
last_name: Nielsen
- first_name: Emmanuel Osalotioman
full_name: Osazuwa, Emmanuel Osalotioman
last_name: Osazuwa
- first_name: Giovanni
full_name: Paolini, Giovanni
last_name: Paolini
- first_name: Marco
full_name: Petracci, Marco
last_name: Petracci
- first_name: Bernhard
full_name: Reinke, Bernhard
last_name: Reinke
- first_name: David
full_name: Renshaw, David
last_name: Renshaw
- first_name: Marcus
full_name: Rossel, Marcus
last_name: Rossel
- first_name: Cody
full_name: Roux, Cody
last_name: Roux
- first_name: Jérémy
full_name: Scanvic, Jérémy
last_name: Scanvic
- first_name: Shreyas
full_name: Srinivas, Shreyas
last_name: Srinivas
- first_name: Anand Rao
full_name: Tadipatri, Anand Rao
last_name: Tadipatri
- first_name: Terence
full_name: Tao, Terence
last_name: Tao
- first_name: Vlad
full_name: Tsyrklevich, Vlad
last_name: Tsyrklevich
- first_name: Fernando
full_name: Vaquerizo-Villar, Fernando
last_name: Vaquerizo-Villar
- first_name: Daniel
full_name: Weber, Daniel
last_name: Weber
- first_name: Fan
full_name: Zheng, Fan
last_name: Zheng
citation:
ama: 'Bolan M, Breitner J, Brox J, et al. The equational theories project: Advancing
collaborative mathematical research at scale. arXiv. doi:10.48550/arXiv.2512.07087'
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. arXiv. https://doi.org/10.48550/arXiv.2512.07087'
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.” ArXiv, n.d. https://doi.org/10.48550/arXiv.2512.07087.'
ieee: 'M. Bolan et al., “The equational theories project: Advancing collaborative
mathematical research at scale,” arXiv. .'
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, 10.48550/arXiv.2512.07087.'
mla: 'Bolan, Matthew, et al. “The Equational Theories Project: Advancing Collaborative
Mathematical Research at Scale.” ArXiv, doi:10.48550/arXiv.2512.07087.'
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.).
date_created: 2026-03-04T12:00:16Z
date_published: 2025-12-16T00:00:00Z
date_updated: 2026-03-12T08:36:21Z
day: '16'
department:
- _id: GradSch
- _id: VlKo
doi: 10.48550/arXiv.2512.07087
external_id:
arxiv:
- '2512.07087'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2512.07087
month: '12'
oa: 1
oa_version: Preprint
publication: arXiv
publication_status: submitted
status: public
title: 'The equational theories project: Advancing collaborative mathematical research
at scale'
tmp:
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)
short: CC BY (4.0)
type: preprint
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2025'
...
---
OA_place: repository
_id: '21398'
abstract:
- lang: eng
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.
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."
article_processing_charge: No
arxiv: 1
author:
- first_name: Martin
full_name: Dvorak, Martin
id: 40ED02A8-C8B4-11E9-A9C0-453BE6697425
last_name: Dvorak
orcid: 0000-0001-5293-214X
- first_name: Tristan
full_name: Figueroa-Reid, Tristan
last_name: Figueroa-Reid
- first_name: Rida
full_name: Hamadani, Rida
last_name: Hamadani
- first_name: Byung-Hak
full_name: Hwang, Byung-Hak
last_name: Hwang
- first_name: Evgenia
full_name: Karunus, Evgenia
last_name: Karunus
- first_name: Vladimir
full_name: Kolmogorov, Vladimir
id: 3D50B0BA-F248-11E8-B48F-1D18A9856A87
last_name: Kolmogorov
- first_name: Alexander
full_name: Meiburg, Alexander
last_name: Meiburg
- first_name: Alexander
full_name: Nelson, Alexander
last_name: Nelson
- first_name: Peter
full_name: Nelson, Peter
last_name: Nelson
- first_name: Mark
full_name: Sandey, Mark
last_name: Sandey
- first_name: Ivan
full_name: Sergeev, Ivan
id: ca3c9187-9a72-11ee-a009-8af825d896b0
last_name: Sergeev
orcid: 0009-0004-9145-8785
citation:
ama: Dvorak M, Figueroa-Reid T, Hamadani R, et al. Composition direction of Seymour’s
theorem for regular matroids — Formally verified. arXiv. doi:10.48550/arXiv.2509.20539
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. arXiv. https://doi.org/10.48550/arXiv.2509.20539
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.” ArXiv,
n.d. https://doi.org/10.48550/arXiv.2509.20539.
ieee: M. Dvorak et al., “Composition direction of Seymour’s theorem for regular
matroids — Formally verified,” arXiv. .
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, 10.48550/arXiv.2509.20539.
mla: Dvorak, Martin, et al. “Composition Direction of Seymour’s Theorem for Regular
Matroids — Formally Verified.” ArXiv, doi:10.48550/arXiv.2509.20539.
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.).
corr_author: '1'
date_created: 2026-03-04T11:56:29Z
date_published: 2025-09-23T00:00:00Z
date_updated: 2026-03-27T12:36:59Z
day: '23'
department:
- _id: GradSch
- _id: VlKo
doi: 10.48550/arXiv.2509.20539
external_id:
arxiv:
- '2509.20539'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2509.20539
month: '09'
oa: 1
oa_version: Preprint
page: '21'
publication: arXiv
publication_status: draft
related_material:
record:
- id: '21393'
relation: dissertation_contains
status: public
status: public
title: Composition direction of Seymour's theorem for regular matroids — Formally
verified
type: preprint
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2025'
...
---
OA_place: repository
OA_type: green
_id: '20071'
abstract:
- lang: eng
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".
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.
article_number: '2409.08119'
article_processing_charge: No
arxiv: 1
author:
- first_name: Martin
full_name: Dvorak, Martin
id: 40ED02A8-C8B4-11E9-A9C0-453BE6697425
last_name: Dvorak
orcid: 0000-0001-5293-214X
- first_name: Vladimir
full_name: Kolmogorov, Vladimir
id: 3D50B0BA-F248-11E8-B48F-1D18A9856A87
last_name: Kolmogorov
citation:
ama: Dvorak M, Kolmogorov V. Duality theory in linear optimization and its extensions
-- formally verified. arXiv. doi:10.48550/arXiv.2409.08119
apa: Dvorak, M., & Kolmogorov, V. (n.d.). Duality theory in linear optimization
and its extensions -- formally verified. arXiv. https://doi.org/10.48550/arXiv.2409.08119
chicago: Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization
and Its Extensions -- Formally Verified.” ArXiv, n.d. https://doi.org/10.48550/arXiv.2409.08119.
ieee: M. Dvorak and V. Kolmogorov, “Duality theory in linear optimization and its
extensions -- formally verified,” arXiv. .
ista: Dvorak M, Kolmogorov V. Duality theory in linear optimization and its extensions
-- formally verified. arXiv, 2409.08119.
mla: Dvorak, Martin, and Vladimir Kolmogorov. “Duality Theory in Linear Optimization
and Its Extensions -- Formally Verified.” ArXiv, 2409.08119, doi:10.48550/arXiv.2409.08119.
short: M. Dvorak, V. Kolmogorov, ArXiv (n.d.).
corr_author: '1'
date_created: 2025-07-23T11:21:52Z
date_published: 2024-09-12T00:00:00Z
date_updated: 2026-03-27T12:36:59Z
day: '12'
department:
- _id: GradSch
- _id: VlKo
doi: 10.48550/arXiv.2409.08119
external_id:
arxiv:
- '2409.08119'
keyword:
- Farkas lemma
- linear programming
- extended reals
- calculus of inductive constructions
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.48550/arXiv.2409.08119
month: '09'
oa: 1
oa_version: Preprint
publication: arXiv
publication_status: draft
related_material:
link:
- description: full version of all definitions, statement, and proofs
relation: software
url: https://github.com/madvorak/duality/tree/v3.2
record:
- id: '21393'
relation: dissertation_contains
status: public
status: public
title: Duality theory in linear optimization and its extensions -- formally verified
type: preprint
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2024'
...
---
_id: '13120'
abstract:
- lang: eng
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.'
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. "
alternative_title:
- LIPIcs
article_number: '15'
article_processing_charge: No
arxiv: 1
author:
- first_name: Martin
full_name: Dvorak, Martin
id: 40ED02A8-C8B4-11E9-A9C0-453BE6697425
last_name: Dvorak
orcid: 0000-0001-5293-214X
- first_name: Jasmin
full_name: Blanchette, Jasmin
last_name: Blanchette
citation:
ama: 'Dvorak M, Blanchette J. Closure properties of general grammars - formally
verified. In: 14th International Conference on Interactive Theorem Proving.
Vol 268. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2023. doi:10.4230/LIPIcs.ITP.2023.15'
apa: 'Dvorak, M., & Blanchette, J. (2023). Closure properties of general grammars
- formally verified. In 14th International Conference on Interactive Theorem
Proving (Vol. 268). Bialystok, Poland: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.4230/LIPIcs.ITP.2023.15'
chicago: Dvorak, Martin, and Jasmin Blanchette. “Closure Properties of General Grammars
- Formally Verified.” In 14th International Conference on Interactive Theorem
Proving, Vol. 268. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
https://doi.org/10.4230/LIPIcs.ITP.2023.15.
ieee: M. Dvorak and J. Blanchette, “Closure properties of general grammars - formally
verified,” in 14th International Conference on Interactive Theorem Proving,
Bialystok, Poland, 2023, vol. 268.
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.'
mla: Dvorak, Martin, and Jasmin Blanchette. “Closure Properties of General Grammars
- Formally Verified.” 14th International Conference on Interactive Theorem
Proving, vol. 268, 15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2023, doi:10.4230/LIPIcs.ITP.2023.15.
short: M. Dvorak, J. Blanchette, in:, 14th International Conference on Interactive
Theorem Proving, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023.
conference:
end_date: 2023-08-04
location: Bialystok, Poland
name: 'ITP: Interactive Theorem Proving'
start_date: 2023-07-31
corr_author: '1'
date_created: 2023-06-05T07:29:05Z
date_published: 2023-07-27T00:00:00Z
date_updated: 2026-03-27T12:36:59Z
day: '27'
ddc:
- '000'
department:
- _id: GradSch
- _id: VlKo
doi: 10.4230/LIPIcs.ITP.2023.15
external_id:
arxiv:
- '2302.06420'
isi:
- '001515590500015'
file:
- access_level: open_access
checksum: 773a0197f05b67feaa6cb1e17ec3642d
content_type: application/pdf
creator: dernst
date_created: 2023-08-07T11:55:43Z
date_updated: 2023-08-07T11:55:43Z
file_id: '13982'
file_name: 2023_LIPIcS_Dvorak.pdf
file_size: 715976
relation: main_file
success: 1
file_date_updated: 2023-08-07T11:55:43Z
has_accepted_license: '1'
intvolume: ' 268'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
publication: 14th International Conference on Interactive Theorem Proving
publication_identifier:
eissn:
- 1868-8969
isbn:
- '9783959772846'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
quality_controlled: '1'
related_material:
link:
- relation: software
url: https://github.com/madvorak/grammars/tree/publish
record:
- id: '21393'
relation: dissertation_contains
status: public
scopus_import: '1'
status: public
title: Closure properties of general grammars - formally verified
tmp:
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)
short: CC BY (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 268
year: '2023'
...
---
_id: '9592'
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.
article_processing_charge: No
arxiv: 1
author:
- first_name: Martin
full_name: Dvorak, Martin
id: 40ED02A8-C8B4-11E9-A9C0-453BE6697425
last_name: Dvorak
orcid: 0000-0001-5293-214X
- first_name: Sara
full_name: Nicholson, Sara
last_name: Nicholson
citation:
ama: 'Dvorak M, Nicholson S. Massively winning configurations in the convex grabbing
game on the plane. In: Proceedings of the 33rd Canadian Conference on Computational
Geometry. Canadian Conference on Computational Geometry; 2021.'
apa: 'Dvorak, M., & Nicholson, S. (2021). Massively winning configurations in
the convex grabbing game on the plane. In Proceedings of the 33rd Canadian
Conference on Computational Geometry. Halifax, NS, Canada; Virtual: Canadian
Conference on Computational Geometry.'
chicago: Dvorak, Martin, and Sara Nicholson. “Massively Winning Configurations in
the Convex Grabbing Game on the Plane.” In Proceedings of the 33rd Canadian
Conference on Computational Geometry. Canadian Conference on Computational
Geometry, 2021.
ieee: M. Dvorak and S. Nicholson, “Massively winning configurations in the convex
grabbing game on the plane,” in Proceedings of the 33rd Canadian Conference
on Computational Geometry, Halifax, NS, Canada; Virtual, 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.'
mla: Dvorak, Martin, and Sara Nicholson. “Massively Winning Configurations in the
Convex Grabbing Game on the Plane.” Proceedings of the 33rd Canadian Conference
on Computational Geometry, 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.
conference:
end_date: 2021-08-12
location: Halifax, NS, Canada; Virtual
name: 'CCCG: Canadian Conference on Computational Geometry'
start_date: 2021-08-10
date_created: 2021-06-22T15:57:11Z
date_published: 2021-06-29T00:00:00Z
date_updated: 2025-05-14T11:23:45Z
day: '29'
ddc:
- '516'
department:
- _id: GradSch
- _id: VlKo
external_id:
arxiv:
- '2106.11247'
file:
- access_level: open_access
checksum: 45accb1de9b7e0e4bb2fbfe5fd3e6239
content_type: application/pdf
creator: mdvorak
date_created: 2021-06-28T20:23:13Z
date_updated: 2021-06-28T20:23:13Z
file_id: '9616'
file_name: Convex-Grabbing-Game_CCCG_proc_version.pdf
file_size: 381306
relation: main_file
success: 1
- access_level: open_access
checksum: 9199cf18c65658553487458cc24d0ab2
content_type: application/pdf
creator: kschuh
date_created: 2021-08-12T10:57:21Z
date_updated: 2021-08-12T10:57:21Z
file_id: '9902'
file_name: Convex-Grabbing-Game_FULL-VERSION.pdf
file_size: 403645
relation: main_file
success: 1
file_date_updated: 2021-08-12T10:57:21Z
has_accepted_license: '1'
keyword:
- convex grabbing game
- graph grabbing game
- combinatorial game
- convex geometry
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nd/4.0/
month: '06'
oa: 1
oa_version: Published Version
publication: Proceedings of the 33rd Canadian Conference on Computational Geometry
publication_status: published
publisher: Canadian Conference on Computational Geometry
quality_controlled: '1'
status: public
title: Massively winning configurations in the convex grabbing game on the plane
tmp:
image: /image/cc_by_nd.png
legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
short: CC BY-ND (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2021'
...