Matroid Decomposition Theorem Verification

Seymour's theorem is a key structural result about regular matroids. We aim to formally verify Seymour's theorem in Lean 4. You can read a formally verified summary of what we completed so far. It lists our main results together with the key definitions they depend on. Ultimately, we would like to prove the decomposition direction of the Seymour theorem, which we only stated but haven't started proving yet.

Timeline

• 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

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

• Imports Mathlib library
• Uses LeanProject template
• Uses Leanblueprint tool
• Uses doc-gen4 library