Papers With

← All papers
First page of Formalizing Hall's Marriage Theorem in Lean

Formalizing Hall's Marriage Theorem in Lean

Alena Gusakov, Bhavik Mehta, Kyle A. Miller

math.CO Jan 1, 2021 · v1
formalization mathlib combinatorics
Read PDF arXiv abstract
TL;DR
Formalizes Hall's Marriage Theorem with three statement variants and a König's lemma extension in Lean.
Abstract
The authors formalize Hall's Marriage Theorem in the Lean theorem prover for inclusion in mathlib, the community-driven mathematics library for Lean. They provide three presentations of the theorem statement and formalize a version of König's lemma (in terms of inverse limits) to extend the theorem to the case of countably infinite index sets.
Problem

Hall's Marriage Theorem, a fundamental result in combinatorics about systems of distinct representatives, had not been formalized in Lean for inclusion in mathlib, and extending it to countably infinite index sets required additional machinery.

Approach

The authors formalize Hall's Marriage Theorem in the Lean theorem prover, providing three presentations of the theorem statement. They formalize a version of Konig's lemma in terms of inverse limits to extend the theorem from the finite case to countably infinite index sets. The formalization targets inclusion in mathlib.

Results

The formalization covers both the finite and countably infinite cases of Hall's Marriage Theorem and is structured for inclusion in mathlib, Lean's community-driven mathematics library.