Tutte's theorem as an educational formalization project

Pim Otte

In this work, we present two results: The first result is the formalization of Tutte's theorem in Lean, a key theorem concerning matchings in graph theory. As this formalization is…