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
- Quick link to the dependency graph
- Quick link to the documentation
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
- Imports Mathlib library