Seymour's decomposition theorem is a hallmark result in matroid theory that gives a structural characterization of the class of regular matroids. The aim of this project is to formally verify the proof of this theorem in Lean 4. This file contains a summary of our main results together with the key definitions they depend on. Currently, we formalized the statement of the theorem and the proof of its forward (composition) direction for matroids of finite rank and with potentially infinite ground sets. In the future, we would like to also formalize the proof of the backward (decomposition) direction, which we stated in this file.
You can find the blueprint of our formalization on the GitHub Pages site. The blueprint serves as an overview of the theoretical results underpinning the formalization, as well as the documentation of our implementation. The blueprint is also presented visually in the dependency graph.
In case you want to contribute to our project, you can read the contribution guidelines. We use GitHub Issues for tracking tasks, and the issues we think could be a good fit for newcomers are labeled with good first issue. Feel free to reach out on Zulip in case you have questions.
- 2024-10-15 project announced
- 2025-03-24 finished proof that every vector matroid is a matroid
- 2025-05-17 finished proof that the 2-sum of regular matroids is a regular matroid
- 2025-07-05 finished proof that the 3-sum of regular matroids is a regular matroid
- K. Truemper – Matroid Decomposition
- J. Oxley – Matroid Theory
- H. Bruhn, R. Diestel, M. Kriesell, R. Pendavingh, P. Wollan – Axioms for infinite matroids (arxiv, paper)