2 papers
math.CO2021
Formalizing Hall's Marriage Theorem in Lean
Alena Gusakov, Bhavik Mehta, Kyle A. Miller
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 go…
math.GT2018
Planar diagrams for local invariants of graphs in surfaces
Calvin McPhail-Snyder, Kyle A. Miller
In order to apply quantum topology methods to nonplanar graphs, we define a planar diagram category that describes the local topology of embeddings of graphs into surfaces. These \…