{"id":"3803ee1e-2260-4313-8c18-839ac4aaa840","arxiv_id":"2608.09305","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The full theory of dilatations of categories is formalized and machine-checked in Lean 4, and two errors in the original published paper are identified and corrected.","lead":"This paper reports a complete Lean 4 formalization of the theory of dilatations of categories, including a machine-checked universal property and an erratum to the original published theory. It matters because it is a working example of a full paper being verified in a proof assistant, and it surfaces two actual defects in the earlier theory.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The paper's central claim is an artifact claim, but the artifact is unpinned and unaudited; the submission itself provides no way to confirm that every theorem is actually machine-checked.","rationale":"The reader's weakest assumption was already that the external Lean repository must compile, match the paper, and contain no unadvertised sorry declarations, and that the PDF does not provide enough information to audit this. My stress-test pass agrees with that identification. I looked for a separate mathematical flaw in the construction: the two-stage quotient presentation in §4, the descent argument in §5.3.1, the bimorphism-cancellation argument for uniqueness, and the use of the universal property in §6–§10 all appear internally sound and appropriately matched to the Lean statements shown. The paper is unusually transparent about its conditional result for [5, Proposition 3.15(2)] and about the counterexample to [5, Proposition 5.1], and these are not weaknesses of the paper's own argument. The one genuinely load-bearing concern is auditability of the formalization artifact itself: no commit hash, no build log, no sorry audit, and a GitHub URL that could be updated, deleted, or fail to build at review time. This does not change the reader's conditional verdict: the paper should be accepted only once the artifact is pinned and independently built and checked. I therefore set verdict_should_be to UNCHANGED rather than moving the verdict, and I agree with the reader's identification of the weakest assumption.","tokens_in":29957,"tokens_out":7983,"duration_ms":86956,"concrete_test":"Clone the repository at the stated URL, record the resolved commit and the contents of lean-toolchain, run `lake build` from a clean environment, then run an audit script that (1) greps the main file and its transitive imports for `sorry`, `admit`, and top-level `axiom`/`constant`/`unsafe` declarations that are not part of Mathlib's own axioms, and (2) executes `#check` on every declaration named in Appendix A, including `Dila_universal_property`, `DilaLift`, `Iso51`, `no_realizing_center`, `prop_2_24`, and the erratum-related declarations. If the build succeeds, the sorry audit is clean, and all `#check` commands pass, then the load-bearing concern is resolved; otherwise the paper's central claim is unsupported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim—that every definition and theorem in the paper is formalized and machine-checked in Lean 4/Mathlib—is an empirical claim about a software artifact, and the submission does not make that artifact auditable. The data-availability statement in §Data availability and §1.2 give only the URL github.com/rndmx/DilCat, with no commit hash, no Lean toolchain version, no build configuration or log, and no sorry/admit/axiom audit. Because the paper's contribution is the existence of this formalization, build reproducibility is not administrative detail but the load-bearing evidence itself. The mathematical text can be internally coherent and still fail this claim if the repository is stale, incomplete, or contains unadvertised admissions. The paper itself shows that 'formalized' has shades: Appendix A marks several statements from [5] as not formalized (e.g., [5, Corollary 2.16] is listed as 'not formalized'), and §10.1 explains that the ring dilatation A[M] is 'vendored, essentially verbatim, from [8]', so the precise meaning of 'full formalization in a single file' also needs to be checked against the actual repository layout. None of this is a mathematical accusation; it is a precise statement of what currently prevents the headline assertion from being verified from the submission.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents a Lean 4/Mathlib formalization of dilatations of categories. It defines centers, builds the dilatation as a quotient of a freely generated path category by a congruence inherited from Mathlib's localization construction, proves the canonical functor's universal property (Theorem 5.8), and derives restriction, shrinking, and combining operations, codilatations via opposite categories, and a comparison with dilatations of commutative rings. The paper also reports two corrections to the printed theory [5]: Proposition 3.15(2) is formalized only under an extra regularity hypothesis hreg (§8.2), and Proposition 5.1 is refuted by an explicit finite counterexample, with a corrected reindexed statement in Theorem 10.1 (§10). The formalization is claimed to be the primary source and to be contained in a single Lean file, with a systematic dictionary in Appendix A.","tokens_in":30202,"tokens_out":5564,"duration_ms":59184,"significance":"If the referenced Lean repository supports the claims, this is a valuable piece of formalized mathematics: the universal property of dilatations, the path-category quotient construction, the faithfulness and fullness comparison functors, the codilatation duality transport, and the ring/category comparison are machine-checked, and the explicit counterexample to [5, Proposition 5.1] gives a formalized correction rather than a rhetorical one. The paper is also unusually honest: it marks [5, Proposition 3.15(2)] as not proved unconditionally and states that parts (3), (5), and (6) inherit the hypothesis hreg. The statement-by-statement dictionary and the erratum make the work usable and checkable in principle. The main uncertainty is not mathematical coherence but artifact auditability: the submission does not currently allow a reader to verify the central artifact claim from the PDF alone.","major_comments":[{"comment":"The paper's central claim is that every definition and theorem is accompanied by a machine-checked Lean 4 formalization, but the submission does not make this claim auditable: the only artifact reference is the URL https://github.com/rndmx/DilCat, with no commit hash, no Lean toolchain version, no build script or log, and no statement about the absence of `sorry`, `admit`, or `axiom` in the relevant declarations. Because the value of the paper is precisely the existence of this checked formalization, the artifact must be pinned and reproducible; please provide a specific revision, build instructions, and an axiom/sorry audit (for example `#print axioms` output for the declarations listed in Appendix A).","section":"§1.2 and Data availability"},{"comment":"The blanket statement that 'every definition and every theorem in this text is accompanied by its Lean 4 formalization' is too broad relative to the paper's own material: Appendix A explicitly marks [5, Corollary 2.16] and [5, Remark 3.9] as 'not formalized', and §A.5 states that §5.3 and §5.4 of [5] have no formalized standalone constructions. In addition, §10.1 says the ring dilatation A[M] is not developed in the file discussed in this paper but is vendored from [8]. The authors should replace the blanket claim with a precise inventory: which statements are proved in this project's file, which are imported or vendored from external developments, and which are deliberately left informal.","section":"§1.2 and Appendix A"},{"comment":"The abstract and introduction list 'combining centers' as one of the main results, but the combining-center theorem is not established unconditionally: [5, Proposition 3.15(2)] is explicitly not rigorously proved and not formalized without the extra hypothesis hreg, and parts (3), (5), and (6) of that proposition inherit this hypothesis. This is not a mathematical error, but it is a scope issue: the paper should state in the abstract or introduction that the two-stage dilatation isomorphism for arbitrary centers is conditional on an open regularity hypothesis, so that readers do not take 'combining centers' as a fully proved unconditional theorem.","section":"§8.2, Remark 8.1"},{"comment":"The comparison with dilatations of rings depends on an external Lean development [8] whose precise version and relationship to the present repository are not documented. Since the formalization of A[M] is 'vendored, essentially verbatim' from [8], the reader cannot tell from the paper whether the ring-theoretic declarations are part of the claimed single file, are imported from another repository, or were re-checked in this project's build. This should be clarified together with the artifact details, because the claim 'contained in a single file' is otherwise ambiguous.","section":"§10.1 and Appendix C"}],"minor_comments":[{"comment":"The displayed formula in Proposition C.1 contains a corrupted fragment ('ihn') and is not typeset correctly; the display should be regenerated so that the two-stage dilatation formula is readable.","section":"Proposition C.1"},{"comment":"The notation `M^N` for exponent profiles is introduced only parenthetically as `N (I)`; please define the exponent-profile type before using it in displayed code, since `N` is also used for sieves and for the natural numbers.","section":"§10.1"},{"comment":"The displayed Lean code for `faithful_of_comp_faithful` omits the separating commas in the binders (`(p : C 1 ⇒C 2) (e : C 2 ⇒C 3)`), which makes the snippet hard to parse; use the standard syntax with commas between dependent arguments.","section":"§5.2"}],"recommendation":"major_revision","confidential_remarks":"The mathematical narrative appears coherent and the erratum is credible, but the paper's central contribution is an artifact claim, and the current submission does not allow that claim to be verified. I would ask the editor to ensure that the revision is reviewed with access to the Lean repository, or by a reviewer who can build Lean 4/Mathlib projects. The self-citation level is high, but the paper's own counterexample and conditional statements show that the formalization is not merely assumed from prior work."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Arnaud Mayeux has formalized his own theory of dilatations of categories in Lean 4, and the formalization caught two real problems in the printed version: [5, Prop 3.15(2)] turns out not to be proved as stated, and [5, Prop 5.1] is false, with an explicit counterexample. That is the headline. Papers in which a proof assistant refutes a published statement are rare, and this one handles the aftermath plainly.\n\nMathematically the framework is the author's own, so the novelty is not the concept. The new part is the machine-checked development: the dilatation is built as a freely generated category quotiented by agreement in the raw localization, which avoids the usual painful associativity proof for fraction composition. That is a clean design choice and worth stealing. The universal property, the restriction/shrinking/combining operations, codilatations via the opposite category, and the ring comparison are all actual Lean declarations with names, and Appendix A is a genuinely useful dictionary. The erratum is clear: the problematic part of 3.15 is turned into an explicit hypothesis hreg, and 5.1 is replaced by the corrected triple identification in Theorem 10.1.\n\nThe main weakness is the one the stress-test flags: the central claim that every theorem in the text is machine-checked is an artifact claim, and the artifact is not pinned. No commit hash, no Lean toolchain version, no build log, no sorry/admit/axiom audit. The GitHub URL is not enough. Also, formalized has gradations: several statements from the original paper are marked 'not formalized' in Appendix A, and the ring dilatation is vendored from a companion formalization. That is all transparent, but it means a reader cannot verify the central claim from the PDF.\n\nThis is not a reason to desk reject. It is a reason to send the paper to review with explicit artifact evaluation. Have the reviewers check out the repo, pin a commit, run the build, and grep for sorry/admit. If that passes, the paper is a solid contribution to the ITP community and useful training data. If it fails, the main claim collapses. The mathematical narrative itself is coherent; I found no internal contradiction.\n\nSo: send it out, and resolve the conditional verdict by a build rather than by the editor's guess.","headline":"A Lean 4 formalization that actually catches a false statement in the author's own published theory; the construction is clean and the erratum is honest, but the unpinned repository is the real weakness and should be settled by artifact review.","tokens_in":30711,"tokens_out":5929,"would_cite":true,"duration_ms":52198,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper claims that the entire theory of dilatations of categories—construction, universal property, operations, duality, and ring comparison—has been formalized in a machine-checked proof assistant, with the formalization treated as…","keywords":["dilatations of categories","localization of categories","Lean 4 formalization","formalized mathematics","universal property","sieve","codilatation","category theory"],"falsifier":"Open the distributed Lean source file and check that it builds with the stated toolchain and contains no undeclared `admit` or `sorry`; a single admitted theorem or a failed build would show that the formalization claim is not established as advertised. For the ring comparison, one can also re-run the paper's explicit counterexample: with $A=\\mathbb{Z}[X]$, $a=2$, $M=(X)$, the element $(X+2)/2$ lies in $A[M]$ but is not in the image of the naive comparison functor.","tokens_in":29756,"feed_emoji":"✔️","tokens_out":10267,"duration_ms":97969,"temperature":0.7,"pith_summary":"The paper sets out to establish that a full theory of dilatations of categories can be carried out in a machine-checked proof assistant, and that the formalized version should be taken as the primary mathematical source. A dilatation takes a category, a family of morphisms $d_i$, and a sieve $N_i$ over each codomain, and produces a new category in which every morphism in $N_i$ factors through $d_i$ uniquely and functorially; the paper claims this construction, its universal property, and all derived operations are mechanically verified. If the claim is correct, the theory has a kind of foundational security rarely available in informal category theory: no step is left implicit, and the process of formalization has already produced two concrete corrections to the earlier printed treatment. A reader who trusts the formalization can rely on Theorem 5.8, the restriction and shrinking comparison functors, the codilatation duality, and the corrected comparison with dilatations of rings.","feed_headline":"Category dilatation theory is now fully machine-checked","feed_subtitle":"A proof assistant verifies the universal property, the key operations, and two corrections to the earlier printed theory.","key_machinery":"The central object is a center: a family of pairs $(d_i,N_i)$ in which $d_i$ is a morphism and $N_i$ is a sieve over its codomain, meaning a collection of morphisms into that object closed under precomposition. The dilatation $Dila\\,Z$ is built as a quotient of the path category generated by original morphisms and formal fraction edges, with two paths identified exactly when they have the same image in the localization of $C$ at all the $d_i$. This single construction carries the whole argument: it inherits associativity of composition from the generic path-category and quotient-category machinery, and it supplies the induction principle (Lemma 5.9) used to prove both existence and uniqueness in the universal property. Theorem 5.8 characterizes when a functor $F\\colon C\\to D$ factors uniquely through the canonical functor $\\Theta$, namely the sieve-inclusion condition $S^{F(N_i)}\\subset S^{F(d_i)}$ together with $\\Sigma$-regularity of $F$.","core_discovery":"The central discovery, stated as the author would state it, is that dilatations of categories are not only formalizable but are best formalized by a two-stage construction. One first forms the free path category on a quiver whose edges are the original morphisms of the category together with formal 'fraction' edges indexed by pairs $(i,n)$ with $n\\in N_i$; one then quotients by the relation that identifies two paths exactly when they have the same image in the raw localization of the category at the family $d_i$. This makes the technical core, the universal property of Theorem 5.8, provable by induction on the free category, with uniqueness coming from a faithfulness condition called $\\Sigma$-regularity. The same machinery gives restriction, shrinking, combining, codilatations, and the comparison with ring dilatations, and it yields two corrections: one printed proposition requires an additional hypothesis, and another is false as stated, with a corrected reindexed statement replacing it.","pith_inferences":["The two-stage template—free path category followed by quotient against a map to a known localization—could be reused to formalize other universal constructions presented by generators and relations, since associativity is inherited rather than rebuilt.","The missing regularity hypothesis in the combining-centers proposition suggests a concrete testable question: does there exist an explicit pair of centers where the hypothesis fails and the final isomorphism genuinely fails, or can the hypothesis be removed by a sharper proof?","The ring counterexample isolates additive closure as the structural ingredient missing from the categorical notion; a quotient construction that builds finite sums into the fraction calculus would likely restore the naive identification.","Because the formalization is primary, its guarantees are tied to a particular version of the proof-assistant library; a change in that library could alter which statements compile, so the verification is best treated as a snapshot."],"forward_implications":["Every numbered definition and theorem in the paper is accompanied by a machine-checked Lean declaration, with the formalization authoritative whenever informal text and formal proof diverge.","The universal property of dilatations holds as stated, giving a precise existence-and-uniqueness criterion for factoring functors through the canonical functor.","Restricting a center, shrinking its sieves, and combining two centers all produce comparison functors with the fullness, faithfulness, or isomorphism properties claimed under the stated hypotheses.","Codilatations are obtained for free from dilatations by passing to the opposite category, with no duplication of proofs.","The comparison with dilatations of rings requires reindexing the center by exponent profiles; the literal i-indexed identification is false and is replaced by a corrected triple isomorphism."],"supporting_citations":[{"why":"The published theory of dilatations of categories whose statements are formalized, including Proposition 3.15 and Proposition 5.1 that the formalization corrects.","marker":"[5]"},{"why":"Provides the Lean 4 proof assistant language in which the formalization is written.","marker":"[9]"},{"why":"Supplies the mathematical library infrastructure for categories, sieves, localization, path categories, and quotient categories on which the formalization is built.","marker":"[3]"},{"why":"Defines multi-centered dilatations of rings and the non-zero-divisor facts used for the ring comparison.","marker":"[4]"},{"why":"Vendors the Lean formalization of ring dilatations used as a black box in Section 10.","marker":"[8]"},{"why":"Gives the classical calculus-of-fractions localization whose structure the quotient construction refines.","marker":"[2]"}],"fun_headline_variants":["Lean 4 checks category dilatation theory","Dilatations formalized, two errors fixed","Machine-checked proof for dilatations","Category dilatations, now Lean-verified"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole advertised verification stands or falls on the external Lean source file actually compiling exactly as described and containing no hidden admitted proofs; the paper gives no commit hash, build script, or compiler output, so that claim cannot be audited from the printed text alone.","fun_headline_variants_meta":{"raw":{"variants":["Lean 4 checks category dilatation theory","Dilatations formalized, two errors fixed","Machine-checked proof for dilatations","Category dilatations, now Lean-verified"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000106,"raw_usage":{"total_tokens":993,"prompt_tokens":853,"completion_tokens":140,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":469,"completion_tokens_details":{"reasoning_tokens":84}},"tokens_in":469,"tokens_out":140,"duration_ms":2147,"temperature":1.0,"reasoning_tokens":84,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T19:43:16.772147+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Open the distributed Lean source file and check that it builds with the stated toolchain and contains no undeclared `admit` or `sorry`; a single admitted theorem or a failed build would show that the formalization claim is not established as advertised. For the ring comparison, one can also re-run the paper's explicit counterexample: with $A=\\mathbb{Z}[X]$, $a=2$, $M=(X)$, the element $(X+2)/2$ lies in $A[M]$ but is not in the image of the naive comparison functor.","supporting_citations":[{"cited_title":"Mayeux, Dilatations of categories,Higher Structures, 9(2), 2025, 62– 75","cited_arxiv_id":null,"evidence_quote":"The published theory of dilatations of categories whose statements are formalized, including Proposition 3.15 and Proposition 5.1 that the formalization corrects."},{"cited_title":"de Moura and S","cited_arxiv_id":null,"evidence_quote":"Provides the Lean 4 proof assistant language in which the formalization is written."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the mathematical library infrastructure for categories, sieves, localization, path categories, and quotient categories on which the formalization is built."},{"cited_title":"Mayeux, Multi-centered dilatations, congruent isomorphisms and Rost double deformation space,Transformation Groups, 31 (2026), 1801–1850","cited_arxiv_id":null,"evidence_quote":"Defines multi-centered dilatations of rings and the non-zero-divisor facts used for the ring comparison."},{"cited_title":"Gabriel and M","cited_arxiv_id":null,"evidence_quote":"Gives the classical calculus-of-fractions localization whose structure the quotient construction refines."}],"review_version":1}