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