A Blueprint for the Formalization of Seymour's Matroid Decomposition Theorem

TL;DR

This paper provides a detailed plan for formalizing Seymour's matroid decomposition theorem in Lean, focusing on the structural properties of regular matroids and their preservation under certain operations.

Contribution

It introduces a modular approach to regularity via totally unimodular representations and maps out the logical structure for formal proof development.

Findings

Regularity preserved under 1-, 2-, and 3-sums

Established regularity for graphic, cographic, and R_{10} matroids

Blueprint guides formalization and clarifies proof dependencies

Abstract

This document is a blueprint for the formalization in Lean of the structural theory of regular matroids underlying Seymour's decomposition theorem. We present a modular account of regularity via totally unimodular representations, show that regularity is preserved under $1$-, $2$-, and $3$-sums, and establish regularity for several special classes of matroids, including graphic, cographic, and the matroid $R_{10}$. The blueprint records the logical structure of the proof, the precise dependencies between results, and their correspondence with Lean declarations. It is intended both as a guide for the ongoing formalization effort and as a human-readable reference for the organization of the proof.