Matroid Decomposition Theorem Verification
The goal of this project is to formally verify Seymour's decomposition theorem in Lean 4.
Blueprint
You can find the blueprint on the GitHub Pages site
References
- 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)
Used tools and projects
- Uses LeanProject template
- Uses leanblueprint tool