Formalizing Hall's Marriage Theorem in Lean

TL;DR

This paper formalizes Hall's Marriage Theorem within the Lean theorem prover, providing multiple representations and extending it to infinite cases, contributing to the development of a comprehensive mathematical library.

Contribution

It introduces formal proofs of Hall's Marriage Theorem in Lean, including finite and infinite cases, with multiple theorem presentations and related graph theory formalizations.

Findings

Formal proof of Hall's Marriage Theorem in Lean

Extension to countably infinite cases using Kőnig's lemma

Descriptions of graph formalizations in mathlib

Abstract

We formalize Hall's Marriage Theorem in the Lean theorem prover for inclusion in mathlib, which is a community-driven effort to build a unified mathematics library for Lean. One goal of the mathlib project is to contain all of the topics of a complete undergraduate mathematics education. We provide three presentations of the main theorem statement: in terms of indexed families of finite sets, of relations on types, and of matchings in bipartite graphs. We also formalize a version of K\H{o}nig's lemma (in terms of inverse limits) to boost the theorem to the case of countably infinite index sets. We give a description of the design of the recent mathlib library for simple graphs, and we also give a necessary and sufficient condition for a simple graph to carry a function.