Papers With

← All papers
First page of Tutte's theorem as an educational formalization project

Tutte's theorem as an educational formalization project

Pim Otte

cs.LO Apr 25, 2025 · v1
formalization mathlib combinatorics
Read PDF arXiv abstract Code
TL;DR
Formalizes Tutte's theorem on graph matchings in Lean, contributing the development to Mathlib.
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.
Problem

Tutte's theorem, a key result characterizing perfect matchings in graphs, had not been formalized in Lean. Additionally, there is no established framework for educational formalization projects that allows students to learn theorem proving with minimal teacher input.

Approach

The authors formalize Tutte's theorem in Lean, ready for integration into Mathlib. They also propose a two-phase framework for educational formalization projects: Phase 1 focuses on initial formalization (learning to work with an ITP, proving goals), and Phase 2 on polishing (refactoring, architecting formal proofs). The framework applies to both academic settings and community-driven environments.

Results

Tutte's theorem is formalized and largely contributed to Mathlib, providing a stepping stone toward formalizing research-level matching theory. The educational framework is demonstrated through the project, showing that beginners can undertake extensive formalization with minimal teacher input.