Matroid Decomposition Theorem Verification
The goal of this project is to formally verify Seymour's decomposition theorem for regular matroids in Lean 4.
Blueprint
- You can find the blueprint on the GitHub Pages site
- Quick link to the dependency graph
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
- Used doc-gen4 tool
- Imports Mathlib library