4 papers
Duality theory in linear optimization and its extensions -- formally verified
Martin Dvorak, Vladimir Kolmogorov
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…
A Blueprint for the Formalization of Seymour's Matroid Decomposition Theorem
Ivan Sergeev, Martin Dvorak, Cameron Rampell +2
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…
The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale
Matthew Bolan, Joachim Breitner, Jose Brox +31
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 suc…
Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified
Martin Dvorak, Tristan Figueroa-Reid, Rida Hamadani +8
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 fa…