The goal of this project is to formally verify Seymour's decomposition theorem for regular matroids in Lean 4.
Seymour's theorem is an important chapter of matroid theory. 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 representation and we prove that they form a matroid in the sense that Mathlib 4 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. This concludes the composition direction of the Seymour's theorem.
- 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
- You can find the blueprint on the GitHub Pages site
- Quick link to the dependency graph
- K. Truemper – Matroid Decomposition
- J. Oxley – Matroid Theory
- J. Geelen, B. Gerards – Regular matroid decomposition via signed graphs
- S. R. Kingan - On Seymour's decomposition theorem (arxiv, paper)
- H. Bruhn et al. - Axioms for infinite matroids (arxiv, paper)
- Imports Mathlib library
- Uses LeanProject template
- Uses Leanblueprint tool
- Uses do 75FD c-gen4 library