{"id":"111815e2-a219-40e1-b036-8325e21bdd33","arxiv_id":"2504.18146","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A Lean formalization of Tutte's theorem is presented and contributed to mathlib, together with a two-phase framework for educational formalization projects.","lead":"This paper reports a computer-checked proof of Tutte's theorem, a classic graph theory result about perfect matchings, written in the Lean proof assistant. It also proposes a two-phase framework for learning to write such formal proofs with minimal help from a teacher.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The formalization claim rests on an external branch commit whose contents are never shown: Listings 11, 13 and 14 display sorry placeholders, so the paper does not itself demonstrate that the cited commit contains a complete, sorry-free proof.","rationale":"The reader identified the same load-bearing assumption: the external branch commit must actually contain a complete, compiling formalization with no sorries. My reading confirms this is the pivotal point. Every displayed occurrence of sorry in Listings 11, 13 and 14 is explicitly described as an omission for clarity, and the paper points to named results in the repository as the authoritative code. That is a reasonable way to present a formalization in a paper, but it makes the claim externally verifiable rather than self-contained. The reviewer's conditional verdict is therefore appropriate: if the cited commit contains the full proof and builds cleanly, the formalization claim stands; if not, it collapses. The educational framework is weaker evidence but not the load-bearing concern, because the authors themselves mark the necessary conditions as conjectured and support the framework with a single self-assessed example. That limitation is disclosed, so it does not undermine the paper's second contribution beyond what is already acknowledged. The concrete test I propose would settle the main concern definitively: rebuild the exact cited commit and check for absence of sorries and axioms. Until that is done, the paper's central claim should remain conditional on the artifact being as described. No further adjustment to the reader's verdict is needed.","tokens_in":862,"tokens_out":2048,"duration_ms":36949,"concrete_test":"Fetch commit 0d2016d6b2de4c164766a24bce95ca948950844c from the Lean mathlib repository, check out the files containing the Tutte formalization, build them with the repository's pinned Lean toolchain, and run a script that (a) rejects any sorry, admit, or axiom declarations in those files, and (b) evaluates #print axioms tutte after importing the relevant files, requiring the output to be empty. If the commit cannot be fetched or the axiom list is nonempty, the central claim is not supported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's first and primary result is that Tutte's theorem has a formalized proof in Lean that is 'ready to be integrated' into mathlib, backed by the commit 0d2016d6b2de4c164766a24bce95ca948950844c. The displayed formalization, however, contains several theorems whose proofs are replaced by sorry: Listing 11 (isTutteViolator_empty and not_IsTutteViolator), Listing 13 (exists_of_isClique_supp), Listing 14 (tutte_exists_isPerfectMatching_of_near_matchings), and Listing 10's top-level proof itself relies on these. The text explicitly says 'we have omitted most proofs using sorry' and that code samples were 'modified for clarity.' This is honest about the listings, but it means the reader cannot distinguish between a complete verified development and a skeleton. The central claim therefore depends entirely on an external artifact: the cited mathlib branch commit. That artifact is not bundled, not archived, and not checked in the paper. Because the commit is on a branch rather than a stable release, it may be deleted or force-updated. Additionally, the phrase 'nearly completely integrated' is weaker than 'complete formalization,' yet the abstract and introduction present the formalization as a finished contribution. This concern is not about the mathematics or the framework, which is explicitly labeled conjectural; it is about whether the headline formalization result is actually established by the paper as written.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":15062,"tokens_out":10099,"duration_ms":97109,"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":[{"comment":"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.","section":"Section 2, Listings 10-14"},{"comment":"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.","section":"Section 2.3, Listing 12"}],"minor_comments":[{"comment":"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.","section":"Section 2, preamble"},{"comment":"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'.","section":"Section 2.1.2, Listing 4"},{"comment":"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.","section":"Section 1.1"},{"comment":"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...'.","section":"Section 3.2"},{"comment":"The phrase 'An more ambitious project' should be 'A more ambitious project'.","section":"Section 4"},{"comment":"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.","section":"Abstract, Introduction, Conclusion"},{"comment":"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.","section":"Section 3.3, final paragraph"}],"recommendation":"major_revision","confidential_remarks":"The formalization claim rests entirely on an unarchived mathlib branch commit that is not bundled with the paper. If the authors cannot provide a stable, checkable artifact, the paper should not be accepted in its current form, regardless of the mathematical correctness of the sketch. The educational framework is a single-case proposal and should be framed accordingly. I found no evidence of circularity or data fabrication; the reported timeline and line counts are internally consistent."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nHere's my take on Otte's Tutte formalization paper. The new thing is the first Lean formalization of Tutte's theorem, using Lovász's sufficiency proof, and it appears to be serious work destined for mathlib. The educational framework—two phases from initial formalization to polishing, mapped onto Bloom's taxonomy—is sensible and the author is upfront that it is a conjecture based on one self-assessed case. The example of abstracting representatives of connected components is genuinely useful for anyone teaching formalization.\n\nNow the soft spot. The paper's listings contain sorry, and the real proof lives on a branch commit of mathlib that is not bundled or archived. The author says the names link to the actual code, and that is likely true, but a reader cannot verify from the preprint that the formalization is complete and sorry-free. That matters because the abstract calls it 'ready to be integrated' and the first result is the formalization itself. For a machine-checked proof, the artifact should be as easy to check as possible. I would not call this fatal—the branch is cited, and the mathlib PR process gives some confidence—but it is a real reproducibility gap. If I were the referee, I'd ask for a stable archive or for the code to be merged before final acceptance.\n\nThe theorem statement matches the standard one, and the proof sketch follows Diestel's presentation of Lovász, so the mathematics looks sound. The related-work section is fair about the parallel Isabelle/HOL work by Abdulaziz and the existing Hall's marriage theorem formalization.\n\nThis is a subfield contribution, not a paradigm shift. It deserves a serious referee, though the bar for 'complete formalization' should be raised to include a checkable artifact. I'd send it to review with a request to address artifact availability.\n\nIf you work on Lean graph theory, you'll likely cite this. For a reading group, it could prompt a good discussion about reproducibility criteria for formalization papers.","headline":"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.","tokens_in":15624,"tokens_out":3215,"would_cite":true,"duration_ms":32286,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["05C70","68V20","03B35"],"pacs":[],"model":"deepseek-v4-flash","headline":"Tutte's theorem now has a machine-checked proof, and the project doubles as a template for teaching formalization.","keywords":["Tutte's theorem","perfect matchings","graph theory","formal verification","interactive theorem proving","proof assistants","formalization education","Lean"],"falsifier":"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$.","tokens_in":14571,"feed_emoji":"✅","tokens_out":8163,"duration_ms":72109,"temperature":0.7,"pith_summary":"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.","feed_headline":"Tutte's theorem gets a machine-checked proof","feed_subtitle":"A verified proof is ready for the main library, plus a two-phase plan for teaching formalization.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the original statement and proof of Tutte's theorem, the mathematical target of the formalization.","marker":"[32]"},{"why":"Provides the textbook version of the sufficiency proof whose structure the formalization follows.","marker":"[9]"},{"why":"Supplies the existing formalization of Hall's marriage theorem in the same library, giving the matching and subgraph vocabulary used.","marker":"[16]"},{"why":"Supplies the proof-search tactic used to discharge the symmetry and irreflexivity side conditions in the graph definitions.","marker":"[19]"},{"why":"Supplies the prerequisite tutorial that the framework assumes a student has completed before starting a formalization project.","marker":"[5]"},{"why":"Provides the revised Bloom's taxonomy used to argue that the two phases target lower-order then higher-order learning skills.","marker":"[3]"}],"fun_headline_variants":["Lean proof of Tutte's theorem ready for mathlib","Learners formalize Tutte's theorem in Lean with two-phase method","Tutte's theorem proof in Lean doubles as a teaching template","Machine-checked Tutte's theorem: a lesson in formalization","Tutte's theorem formal proof ready for mathlib, with pedagogy plan"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Lean proof of Tutte's theorem ready for mathlib","Learners formalize Tutte's theorem in Lean with two-phase method","Tutte's theorem proof in Lean doubles as a teaching template","Machine-checked Tutte's theorem: a lesson in formalization","Tutte's theorem formal proof ready for mathlib, with pedagogy plan"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000923,"raw_usage":{"total_tokens":3906,"prompt_tokens":846,"completion_tokens":3060,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":462,"completion_tokens_details":{"reasoning_tokens":2968}},"tokens_in":462,"tokens_out":3060,"duration_ms":22297,"temperature":1.0,"reasoning_tokens":2968,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T10:23:12.021836+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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$.","supporting_citations":[{"cited_title":"Formalizing Hall's Marriage Theorem in Lean","cited_arxiv_id":"2101.00127","evidence_quote":"Supplies the existing formalization of Hall's marriage theorem in the same library, giving the matching and subgraph vocabulary used."},{"cited_title":"Theorem proving in lean 4, 2025","cited_arxiv_id":null,"evidence_quote":"Supplies the prerequisite tutorial that the framework assumes a student has completed before starting a formalization project."},{"cited_title":"A taxonomy for learning, teaching, and assessing: A revision of Bloom's taxonomy of educational objectives: complete edition","cited_arxiv_id":null,"evidence_quote":"Provides the revised Bloom's taxonomy used to argue that the two phases target lower-order then higher-order learning skills."}],"review_version":1}