Pith. sign in

REVIEW 2 major objections 7 minor 33 references

Tutte's theorem as an educational formalization project

T0 review · 2 major / 7 minor · reviewed 2026-08-16 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Tutte's theorem now has a machine-checked proof, and the project doubles as a template for teaching formalization.

desk verdict The Lean formalization of Tutte's theorem is credible and the educational framework is honest, but the preprint does not itself show the proof, so artifact availability is the key review issue. read the letter →

arxiv 2504.18146 v1 pith:5U4HYNKY submitted 2025-04-25 cs.LO math.CO

Pim Otte This is my paper · ORCID
classification cs.LOmath.CO MSC 05C7068V2003B35
keywords Tutte'stheoremperfectmatchingsgraphtheoryformalverificationinteractiveprovingproofassistantsformalizationeducationLean
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper reports two connected results. The first is a machine-checked proof of Tutte's theorem on perfect matchings in finite graphs, written in the Lean theorem prover and ready to be merged into the prover's main mathematical library. The second is an educational framework for large formalization projects, organized into an initial formalization phase and a later polishing phase, designed to run with minimal teacher input. The author argues that this structure lets a beginner with tutorial-level experience carry out a substantial formalization, with the community around the prover serving as the teacher in the worked example. Together the two results matter because matching theory is a core part of graph theory and because the framework offers a route to training more formalizers than current teachers could handle one-on-one.

What carries the argument

The load-bearing notion is the Tutte violator: a set $U\subseteq V$ whose deletion leaves more odd-sized connected components in $G-U$ than vertices in $U$. The theorem's content is that a perfect matching exists exactly when no Tutte violator exists. The proof machinery is the contrapositive sufficiency argument that passes to an edge-maximal graph with no perfect matching, removes its universal vertices, and either builds a perfect matching when the remainder is a union of cliques, or uses the symmetric difference of two near-perfect matchings along an alternating cycle to merge them into a matching for the original graph. The educational machinery is the two-phase structure (initial formalization, then polishing and integration), which maps onto lower-order and higher-order learning goals and limits the teacher's role to choosing a correct goal statement, recommending resources, and reviewing the polished product.

What would settle it

Download the code at the cited commit and run the proof checker on the file declaring the theorem `tutte`; the claim is settled if and only if it compiles with no remaining `sorry` axioms and the printed statement says a perfect matching exists exactly when every vertex set $U$ leaves at most $|U|$ odd components in $G-U$.

Watch

Extended reading notes

Core claim

On the mathematical side, the paper claims that Tutte's theorem—a finite graph $G$ has a perfect matching exactly when deleting any subset $U$ of vertices leaves at most $|U|$ connected components of odd size—has a complete formal proof in the Lean proof assistant. The proof follows the standard sufficiency argument: reduce to an edge-maximal graph with no perfect matching, consider the universal vertices, split into the case where the remaining graph is a disjoint union of cliques and the case where it is not, and in the latter case combine two near-perfect matchings through the symmetric difference with an alternating cycle. On the educational side, the paper claims that a two-phase framework, in which a student first produces a working formalization and then polishes and integrates it, teaches the skills needed for large formalization projects with minimal teacher involvement. The case report notes that following this framework the formalization shrank from about 5,757 lines in one file to 686 lines across two files during the polishing phase.

Load-bearing premise

The claim stands or falls on whether the code at the cited commit, which the paper mostly shows with proofs omitted as 'sorry', actually contains complete proofs that the proof checker accepts.

Editorial extensions

If this is right

  • A verified statement of Tutte's theorem will sit in the main library, so later formalizations of matching theory—for instance Gallai–Edmonds structure theory or the Tutte–Berge formula—can build on it without redoing the groundwork.
  • A beginner who has worked through standard tutorials can attempt a large formalization under this framework, since the worked example shows most teacher input arrives only in the polishing phase.
  • The second phase exercises refactoring and abstraction skills: the example shrank from roughly 5,757 lines to 686 lines while becoming ready for integration.
  • The proof contributes reusable library components, including definitions of alternating cycles and lemmas about symmetric differences with perfect matchings, that other graph theory formalizations can call on.
  • The framework applies outside classrooms, because the teacher role can be filled by volunteer reviewers and maintainers in community-driven projects.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the cited code commit compiles cleanly, the formalization doubles as a machine-checkable certificate of Tutte's theorem and could become a test case for tools that translate informal proofs into proof-assistant code.
  • The abstraction pattern for representatives of connected components, stated as a bijection from a chosen set of vertices onto the set of components, looks reusable beyond this proof; searching a large formal library for analogous patterns could identify other places where the same abstraction pays off.
  • The 'rule of three' heuristic for when to introduce a general abstraction could be tested empirically in other formalization projects by comparing early abstraction against waiting for a third concrete use.
  • The two-phase teaching structure may transfer to other proof assistants, provided the teacher can supply a correct formal statement and a mechanism for reviewing students' code.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 7 minor

Summary. The paper reports two contributions. First, it claims a machine-checked formalization of Tutte's theorem (the perfect-matching characterization) in the Lean theorem prover, built on mathlib, with the proof following Lovász's argument as presented in Diestel. The formalization is described as nearly fully integrated into mathlib, with the final code located at a cited mathlib branch commit. Second, it proposes a two-phase educational framework for formalization projects (an initial formalization phase followed by a polishing phase), embedded in Bloom's taxonomy, together with conjectured necessary conditions and a case study based on the author's own formalization of Tutte's theorem. The paper displays selected Lean definitions and theorem statements, but many displayed proofs are replaced by `sorry` or omitted entirely; the complete proof is claimed to be available only at the external branch commit.

Significance. If the cited Lean development is complete and sorry-free, the formalization is a solid and useful contribution: it provides the first formalization of Tutte's theorem in Lean, complements Abdulaziz's independent Isabelle/HOL formalization, and extends mathlib's simple graph library with augmenting-matching machinery. The educational framework is thoughtfully structured around Bloom's taxonomy and is honestly labeled as conjectural in the body; the case-study example concerning abstraction of representatives is instructive. The paper is transparent about its use of `sorry` placeholders and the provisional status of the mathlib integration, and it does not claim empirical validation of the educational claims beyond a self-report. The writing is generally clear and the related-work coverage is appropriate, including relevant recent formalization efforts.

major comments (2)
  1. [Section 2, Listings 10-14] The central claim that Tutte's theorem has a complete machine-checked proof in Lean is not verifiable from the manuscript. Listing 10's proof of `tutte` delegates to `isTutteViolator_empty` and `not_IsTutteViolator` (Listing 11), `exists_of_isClique_supp` (Listing 13), and `tutte_exists_isPerfectMatching_of_near_matchings` (Listing 14), all of which are displayed with `sorry` or, in Listing 12, with an empty proof body. The text explains that proofs were omitted for clarity and points to the mathlib branch commit `0d2016d6...`, but that commit is neither bundled nor archived with the paper. Since the formalization is the paper's primary claimed result, the displayed code is only a skeleton; the reader cannot confirm that the theorem is actually proved. I ask that the complete Lean source be supplied as a supplementary artifact (for example, a `.lean` file or an archived repository with a DOI), or that the paper explicitly state that the formalization is not yet complete.
  2. [Section 2.3, Listing 12] The lemma `exists_TutteViolator` is the core sufficiency step of the proof, yet its displayed body is empty (`:= by`), which is not even a valid placeholder such as `by sorry`. The surrounding argument gives the overall Lovász structure but not the content of this lemma. Because the main theorem's displayed proof depends entirely on this lemma, this omission is load-bearing rather than a cosmetic cut. At minimum, the manuscript should contain the full statement and proof of `exists_TutteViolator` in an appendix, or provide an exact link to the corresponding lines in the artifact.
minor comments (7)
  1. [Section 2, preamble] The statement that all code snippets before Section 2.3 are from mathlib version 4.1.7 conflicts with the displayed `support_eq_verts` theorem in Listing 4, which contains `sorry`; since mathlib never contains `sorry`, please clarify that even the pre-2.3 snippets have been edited for display.
  2. [Section 2.1.2, Listing 4] The text says that all definitions are stated in Listing 4, but `IsMatching.support_eq_verts` is a theorem rather than a definition; please rephrase to 'definitions and a lemma'.
  3. [Section 1.1] The theorem statement writes `U ⊂ V`, which usually denotes a proper subset; the formal statement and the surrounding argument require `U ⊆ V`, so please correct the notation.
  4. [Section 3.2] The sentence 'If the initial formalization is can be completed in half the allotted time' contains a redundant 'is'; it should read 'If the initial formalization can be completed...'.
  5. [Section 4] The phrase 'An more ambitious project' should be 'A more ambitious project'.
  6. [Abstract, Introduction, Conclusion] Please unify the descriptions of the formalization's status: the abstract says 'ready to be integrated', the introduction says 'nearly completely integrated', and the conclusion says 'largely been contributed to mathlib'; these should be made consistent with each other and with the actual state of the cited commit.
  7. [Section 3.3, final paragraph] The claim that the learning goals were achieved is based on the author's self-assessment; I suggest adding one sentence noting that independent validation of the educational outcomes is left to future work.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the formalization builds on mathlib's existing definitions and an external, checkable commit; the visible sorry placeholders are a completeness concern, not a circular one.

full rationale

The paper's main claimed result is a Lean formalization of Tutte's theorem built on mathlib's existing SimpleGraph, Subgraph, matching, walk, and connected-component API. The theorem statement is not defined in terms of the formalization, and the proof skeleton shown follows the standard Lovász sufficiency argument; no fitted parameter is renamed as a prediction, and no equation is asserted to follow from its own conclusion. The only potentially load-bearing external dependency is the cited mathlib branch commit 0d2016d6b2de4c164766a24bce95ca948950844c, and the displayed listings in Section 2 explicitly contain `sorry` placeholders, with the text saying 'we have omitted most proofs using sorry' and that code samples were 'modified for clarity.' Thus the paper as printed does not itself exhibit a sorry-free derivation, but that is a verification and completeness concern about an external artifact, not circularity: the commit can in principle be checked independently and does not take the target theorem as an input. The educational framework is explicitly conjectural ('we cannot be certain of the exact conditions to successfully apply this framework'), is grounded in Bloom's taxonomy, and is demonstrated through an external case study, so it is not validated by its own conclusion. The single self-citation [25] is cited only as initial inspiration for choosing matching theory and is not load-bearing. No step in the derivation chain reduces, by construction or by self-citation, to its own input.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

No free parameters or invented mathematical entities are introduced. The formalization leans on Lean's standard foundation and on the finite simple graph setting, plus the unverified external premise that the cited branch commit is complete.

assumptions (3)
  • standard math Lean 4's type theory with classical choice and quotient axioms
    The formalization uses classical, Quot, and choice-based tactics inside mathlib; these are standard logical foundations for Lean.
  • domain assumption Finite simple graphs via Fintype V
    Tutte's theorem is stated and proved for finite simple graphs only, as encoded in Listing 10 with the Fintype V instance.
  • ad hoc to paper The referenced mathlib branch commit contains the complete proof without sorry
    The paper omits most proofs and points to commit 0d2016d6b2de4c164766a24bce95ca948950844c; if this external artifact is incomplete, the formalization claim is not supported.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Tutte's theorem as an educational formalization project." pith.science (2026). https://pith.science/paper/5U4HYNKY

@misc{pith2026250418146,
  author       = {Pith},
  title        = {Pith review of: Tutte's theorem as an educational formalization project},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/5U4HYNKY}},
  note         = {Machine review of arXiv:2504.18146}
}
read the original 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.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

33 extracted references · 24 canonical work pages

  1. [1]

    A formal correctness proof of edmonds' blossom shrinking algorithm, 2024

    Mohammad Abdulaziz. A formal correctness proof of edmonds' blossom shrinking algorithm, 2024. URL: https://arxiv.org/abs/2412.20878, https://arxiv.org/abs/2412.20878 arXiv:2412.20878

    arXiv 2024

  2. [2]

    Isabelle graph theory library/tutte\_theorem at c5bcc149ad868d1bb6667f3d2fb48013ca8c588f, 2024

    Mohammad Abdulaziz. Isabelle graph theory library/tutte\_theorem at c5bcc149ad868d1bb6667f3d2fb48013ca8c588f, 2024. Accessed: 2024-02-24. URL: https://github.com/mabdula/Isabelle-Graph-Library/tree/c5bcc149ad868d1bb6667f3d2fb48013ca8c588f/Tutte\_Theorem

    work page 2024

  3. [3]

    A taxonomy for learning, teaching, and assessing: A revision of Bloom's taxonomy of educational objectives: complete edition

    Lorin W Anderson and David R Krathwohl. A taxonomy for learning, teaching, and assessing: A revision of Bloom's taxonomy of educational objectives: complete edition . Addison Wesley Longman, Inc., 2001

    work page 2001

  4. [4]

    The solution of the four-color-map problem

    Kenneth Appel and Wolfgang Haken. The solution of the four-color-map problem. Scientific American , 237(4):108--121, 2025/03/14/ 1977. Full publication date: October 1977. URL: http://www.jstor.org/stable/24953967

    work page arXiv 2025

  5. [5]

    Theorem proving in lean 4, 2025

    Jeremy Avigad, Leonardo De Moura, Soonho Kong, and Sebastian Ullrich. Theorem proving in lean 4, 2025. Electronic book with contributions from the Lean Community

    work page 2025

  6. [6]

    Mathematics in lean, 2020

    Jeremy Avigad and Patrick Massot. Mathematics in lean, 2020. Electronic book

    work page 2020

  7. [7]

    Functional programming in lean, 2022

    David Thrane Christiansen. Functional programming in lean, 2022. Electronic book. URL: https://lean-lang.org/functional_programming_in_lean/

    work page 2022

  8. [8]

    The Lean Language Reference , 2025

    The Lean Developers. The Lean Language Reference , 2025. Online manual. URL: https://lean-lang.org/doc/reference/latest/

    work page 2025

Show all 33 references
  1. [9]

    Graph theory , volume 173 of Graduate Texts in Mathematics

    Reinhard Diestel. Graph theory , volume 173 of Graduate Texts in Mathematics . Springer, Berlin, fifth edition, 2017. https://doi.org/10.1007/978-3-662-53622-3 doi:10.1007/978-3-662-53622-3

    2017 doi

  2. [10]

    Undirected graph theory

    Chelsea Edmonds. Undirected graph theory. Archive of Formal Proofs , September 2022. https://isa-afp.org/entries/Undirected_Graph_Theory.html, Formal proof development

    2022

  3. [11]

    A superlinear bound on the number of perfect matchings in cubic bridgeless graphs

    Louis Esperet, František Kardoš, and Daniel Král’. A superlinear bound on the number of perfect matchings in cubic bridgeless graphs. European Journal of Combinatorics , 33(5):767--798, 2012. EuroComb '09. URL: https://www.sciencedirect.com/science/article/pii/S019566981100175...

    2012 doi

  4. [12]

    Refactoring: improving the design of existing code

    Martin Fowler. Refactoring: improving the design of existing code . Addison-Wesley Professional, 2018

    2018

  5. [13]

    A semantic search engine for mathlib4

    Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong. A semantic search engine for mathlib4. arXiv preprint arXiv:2403.13310 , 2024

    2024 arXiv

  6. [14]

    Formal proof--the four-color theorem

    Georges Gonthier et al. Formal proof--the four-color theorem. Notices of the AMS , 55(11):1382--1393, 2008

    2008

  7. [15]

    W. T. Gowers, Ben Green, Freddie Manners, and Terence Tao. On a conjecture of marton, 2023. URL: https://arxiv.org/abs/2311.05762, https://arxiv.org/abs/2311.05762 arXiv:2311.05762

    2023 arXiv

  8. [16]

    Formalizing hall's marriage theorem in lean

    Alena Gusakov, Bhavik Mehta, and Kyle A Miller. Formalizing hall's marriage theorem in lean. arXiv preprint arXiv:2101.00127 , 2021

    2021 arXiv

  9. [17]

    Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek. Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing -- SAT 2016 , pages 228--245, Cham, 2...

    2016

  10. [19]

    Aesop: White-box best-first proof search for lean

    Jannis Limperg and Asta Halkj r From. Aesop: White-box best-first proof search for lean. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs , CPP 2023, page 253–266, New York, NY, USA, 2023. Association for Computing Machinery. htt...

    2023

  11. [20]

    Matching theory , volume 367

    L \'a szl \'o Lov \'a sz and Michael D Plummer. Matching theory , volume 367. American Mathematical Soc., 2009

    2009

  12. [21]

    The mechanics of proof, 2023

    Heather Macbeth. The mechanics of proof, 2023. Electronic book. URL: https://hrmacbeth.github.io/math2001/index.html

    2023

  13. [22]

    Teaching Mathematics Using Lean and Controlled Natural Language

    Patrick Massot. Teaching Mathematics Using Lean and Controlled Natural Language . In Yves Bertot, Temur Kutsia, and Michael Norrish, editors, 15th International Conference on Interactive Theorem Proving (ITP 2024) , volume 309 of Leibniz International Proceedings in Informatic...

    2024 doi

  14. [23]

    Research report - Proof assistants for teaching: a survey

    Fr \'e d \'e ric Tran Minh, Laure Gonnord, and Julien Narboux. Research report - Proof assistants for teaching: a survey . Technical report, LCIS, Grenoble-INP , April 2024. URL: https://hal.science/hal-04705580

    2024

  15. [24]

    A graph library for isabelle

    Lars Noschinski. A graph library for isabelle. Mathematics in Computer Science , 9(1):23--39, 2015

    2015

  16. [25]

    Counting matchings in cubic graphs, 2014

    Pim Otte. Counting matchings in cubic graphs, 2014. BSc thesis. URL: https://resolver.tudelft.nl/uuid:cb8e5779-0423-4a7e-861f-ad4c3436a3b9

    2014

  17. [26]

    Investigations in Graph-theoretical Constructions in Homotopy Type Theory

    Jonathan Prieto-Cubides. Investigations in Graph-theoretical Constructions in Homotopy Type Theory . PhD thesis, University of Bergen, 2024. URL: https://hdl.handle.net/11250/3168844

    2024

  18. [27]

    Formalization of some central theorems in combinatorics of finite sets

    Abhishek Kr Singh. Formalization of some central theorems in combinatorics of finite sets. In Thomas Eiter, David Sands, Geoff Sutcliffe, and Andrei Voronkov, editors, IWIL Workshop and LPAR Short Presentations , volume 1 of Kalpa Publications in Computing , pages 43--57. Easy...

    2017 doi

  19. [28]

    A constructive formalization of the weak perfect graph theorem

    Abhishek Kr Singh and Raja Natarajan. A constructive formalization of the weak perfect graph theorem. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs , CPP 2020, page 313–324, New York, NY, USA, 2020. Association for Computing Ma...

    2020

  20. [29]

    Teaching of formal methods for software engineering

    Maria Spichkova and Anna Zamansky. Teaching of formal methods for software engineering. In Proceedings of the 11th International Conference on Evaluation of Novel Software Approaches to Software Engineering - Volume 1: COLAFORM, (ENASE 2016) , pages 370--376. INSTICC, SciTePre...

    2016 doi

  21. [30]

    Learning about proof with the theorem prover lean: the abundant numbers task

    Athina Thoma and Paola Iannone. Learning about proof with the theorem prover lean: the abundant numbers task. International Journal of Research in Undergraduate Mathematics Education , 8(1):64--93, Apr 2022. https://doi.org/10.1007/s40753-021-00140-1 doi:10.1007/s40753-021-00140-1

    2022 doi

  22. [31]

    On a system of computer-aided instruction of logic

    Andrzej Trybulec. On a system of computer-aided instruction of logic. Bulletin of the Section of Logic , 12(4):214--218, 1983

    1983

  23. [32]

    The factorization of linear graphs

    William T Tutte. The factorization of linear graphs. Journal of the London Mathematical Society , 1(2):107--111, 1947

    1947

  24. [33]

    Waterproof: Transforming a proof assistant into an educational tool

    Aalt Jelle Wemmenhove. Waterproof: Transforming a proof assistant into an educational tool . Phd thesis 1 (research tu/e / graduation tu/e), Mathematics and Computer Science, March 2025. Proefschrift

    2025

  25. [34]

    Isabelle/Isar---a versatile environment for human-readable formal proof documents

    Markus M Wenzel. Isabelle/Isar---a versatile environment for human-readable formal proof documents . PhD thesis, Technische Universit \"a t M \"u nchen, 2002

    2002

Pith tools

Reviewed August 16, 2026 · model on record in the stance chip above.