Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2504.18146 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908337497440256 |
|---|---|
| author | Otte, Pim |
| author_facet | Otte, Pim |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_18146 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Tutte's theorem as an educational formalization project Otte, Pim Logic in Computer Science Combinatorics 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. |
| title | Tutte's theorem as an educational formalization project |
| topic | Logic in Computer Science Combinatorics |
| url | https://arxiv.org/abs/2504.18146 |