Tutte's theorem as an educational formalization project
Tutte's theorem as an educational formalization project
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.
Pim Otte
数学计算技术、计算机技术
Pim Otte.Tutte's theorem as an educational formalization project[EB/OL].(2025-04-25)[2025-05-17].https://arxiv.org/abs/2504.18146.点此复制
评论