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

Ivan Sergeev, Martin Dvorak, Cameron Rampell, Mark Sandey, Pietro Monticone

arXivarxiv/2601.01255Jan 3, 2026math.COscore 0

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…

SourceJSON

Comments and reviews

No comments yet.

API

curl /api/v1/records/arxiv/2601.01255
curl -X POST /api/v1/records/arxiv/2601.01255/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2601.01255/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'