UWSpace is currently experiencing technical difficulties resulting from its recent migration to a new version of its software. These technical issues are not affecting the submission and browse features of the site. UWaterloo community members may continue submitting items to UWSpace. We apologize for the inconvenience, and are actively working to resolve these technical issues.
 

Formalizing the Excluded Minor Characterization of Binary Matroids in the Lean Theorem Prover

Thumbnail Image

Files

Gusakov_Alena.pdf (1.01 MB)

Date

2024-01-23

Authors

Gusakov, Alena

Journal Title

Journal ISSN

Volume Title

Publisher

University of Waterloo

Abstract

A matroid is a mathematical object that generalizes the notion of linear independence of a set of vectors to an abstract independence of sets, with applications to optimization, linear algebra, graph theory, and algebraic geometry. Matroid theorists are often concerned with representations of matroids over fields. Tutte's seminal theorem proven in 1958 characterizes matroids representable over GF(2) by noncontainment of U2,4 as a matroid minor. In this thesis, we document a formalization of the theorem and its proof in the Lean Theorem Prover, building on its community-built mathematics library, mathlib.

Description

Keywords

formalization, matroid theory, representable matroid, binary matroid, excluded minor characterization, lean theorem prover

LC Keywords

Citation

URI

http://hdl.handle.net/10012/20273

Collections

Theses
Combinatorics and Optimization