2 papers
cs.SC2025
Structuring Definitions in Mathematical Libraries
Alena Gusakov, Peter Nelson, Stephen Watt
Codifying mathematical theories in a proof assistant or computer algebra system is a challenging task, of which the most difficult part is, counterintuitively, structuring definiti…
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…