|国家预印本平台
首页|Tutte's theorem as an educational formalization project

Tutte's theorem as an educational formalization project

Tutte's theorem as an educational formalization project

来源:Arxiv_logoArxiv
英文摘要

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.点此复制

评论