Tutte's theorem as an educational formalization project
Pim Otte
TL;DR
The paper tackles formalizing Tutte's theorem in Lean and introduces an educational framework to guide formalization projects. It combines a top-down formalization approach with a two-phase educational process (initial formalization and polishing) that minimizes teacher input while enabling community-driven learning. The key contributions are the near-complete integration of Tutte's theorem into Lean's mathlib and a practical, Bloom's taxonomy–aligned framework that supports scalable education in formal mathematics. This work advances formalization as a component of mathematical practice, offering a reusable template for similar formalization efforts and broader educational impact across communities.
Abstract
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 ready to be integrated in Lean's mathlib, it provides a valuable step in the path towards formalizing research-level mathematics in this area. The second result is a framework for doing educational formalization projects. This framework provides a structure to learn to formalize mathematics with minimal teacher input. This framework applies to both traditional academic settings and independent community-driven environments. We demonstrate the framework's use by connecting it to the process of formalizing Tutte's theorem.