正则 matroid 的 Seymour 定理组合方向形式化验证
组合数学
2025-09-26 v1 计算机科学中的逻辑
摘要
Seymour 分解定理是 matroid 理论中的标志性成果，提供了正则 matroid 类的结构特征。matroid 理论的形式化面临诸多挑战，最重要的是仅限于已实现的概念和结果数量有限。本 work 我们对正则 matroid 的前向（组合）方向的证明进行形式化。为此，我们在 Lean 4 中开发了一个库，实现了关于全单调矩阵、向量 matroid、其标准表示、正则 matroid 以及由其标准表示给出的矩阵和二进制 matroid 的 1-、2-、3-和的定义和结果。使用该框架，我们形式化地阐述 Seymour 分解定理，并在矩阵具有有限秩且可能具有无限根集的情况下实现形式化验证的组合方向证明。
引用
@article{arxiv.2509.20539,
title = {Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified},
author = {Martin Dvorak and Tristan Figueroa-Reid and Rida Hamadani and Byung-Hak Hwang and Evgenia Karunus and Vladimir Kolmogorov and Alexander Meiburg and Alexander Nelson and Peter Nelson and Mark Sandey and Ivan Sergeev},
journal= {arXiv preprint arXiv:2509.20539},
year = {2025}
}