REVIEW 4 major objections 3 minor 9 references
Dilatations of categories, via their lean formalization
T0 review · 4 major / 3 minor · reviewed 2026-08-11 · deepseek-v4-flash
Pith's one-line read 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…
desk verdict 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. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
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$.
What would settle it
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.
Extended reading notes
Core claim
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.
Load-bearing premise
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.
Editorial extensions
If this is right
- 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.
Reading between the lines
- 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.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
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.
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 (4)
- [§1.2 and Data availability] 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).
- [§1.2 and Appendix A] 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.
- [§8.2, Remark 8.1] 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.
- [§10.1 and Appendix C] 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.
minor comments (3)
- [Proposition C.1] 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.
- [§10.1] 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.
- [§5.2] 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.
Circularity Check
No substantive circularity: the formalized derivation is self-contained, and the self-citations are not load-bearing as unverified authority.
full rationale
The paper's derivation chain does not reduce to its inputs. The dilatation Dila Z is built from a center via Mathlib's free path category and quotient category, and the central universal property (Theorem 5.8, Dila_universal_property) is stated as an existence-plus-uniqueness theorem with explicit hypotheses (the sieve inclusion and Σ-regularity), then proved by path induction (Lemma 5.9), an explicit lift H, a descent lemma H_descends, and a uniqueness argument. Sections 6, 7, and 8 then instantiate this theorem rather than assuming it. The one statement that is visibly by construction is Fact 4.1: DilaRel is defined as equality of images in the raw localization, so faithfulness of DilaToLoc is immediate. The paper explicitly says this is 'close to a tautology once phrased this way,' so it is a transparent design choice, not a hidden assumption or a prediction. Self-citations to [4], [5], [6], and [8] do not carry the argument as unverified authority: the paper formalizes [5] and, notably, reports concrete corrections to it, weakening [5, Proposition 3.15] and refuting [5, Proposition 5.1] with an explicit counterexample; this is evidence of independence rather than circularity. The ring-theoretic input is vendored from a separate Lean formalization [8], which is machine-checked support. The genuine weakness is artifact auditability: the data availability statement provides only a GitHub URL with no commit hash, build log, or sorry/admit audit, so the advertised full formalization cannot be verified from the PDF. That is a reproducibility gap, not a circularity gap, and it does not raise the circularity score.
Assumptions & free parameters
assumptions (4)
- domain assumption Mathlib's CategoryTheory.Localization.Construction correctly formalizes localization at a morphism property.
- domain assumption The vendored formalization of multi-centered dilatations of rings [8] is correct.
- domain assumption The external Lean repository rndmx/DilCat compiles in the state described and matches the paper.
- standard math Lean 4's kernel and the quotient and classical-choice axioms are sound.
Cite this review
Pith. "Pith review of Dilatations of categories, via their lean formalization." pith.science (2026). https://pith.science/paper/YMK6YR4H
@misc{pith2026260809305,
author = {Pith},
title = {Pith review of: Dilatations of categories, via their lean formalization},
year = {2026},
howpublished = {\url{https://pith.science/paper/YMK6YR4H}},
note = {Machine review of arXiv:2608.09305}
}
abstract
Given a category $\calC$ and a center, that is a collection of pairs $(d_i, N_i)$ consisting of a morphism $d_i$ and a sieve $N_i$ over its codomain, the dilatation of $\calC$ is a new category $\calC'$ in which every $n \in N_i$ factors, uniquely and functorially, through $d_i$. This paper presents the theory of dilatations of categories through a full formalization of the construction and its main theorems in the Lean~4 proof assistant, on top of the Mathlib library. An appendix collects a systematic dictionary between the mathematical statements and the Lean declarations that formalize them.
Reference graph
Works this paper leans on
-
[5]
Mayeux, Dilatations of categories,Higher Structures, 9(2), 2025, 62– 75
A. Mayeux, Dilatations of categories,Higher Structures, 9(2), 2025, 62– 75
work page 2025
-
[8]
A. Mayeux and J. Zhang, Formalizing multi-graded Brenner–Schröer Proj schemes and dilatations of rings in Lean4, arXiv:2606.01438, 2026
arXiv 2026
-
[1]
A. Dubouloz, A. Mayeux and J.P. dos Santos, A survey on algebraic dilatations,Fields Institute Monographs, Springer, to appear
-
[2]
P. Gabriel and M. Zisman,Calculus of fractions and homotopy theory, Ergebnisse der Mathematik und ihrer Grenzgebiete 35, Springer-Verlag, New York, 1967
work page 1967
-
[3]
The mathlib Community, The Lean mathematical library, inProceed- ings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020, 367–381
work page 2020
-
[4]
A. Mayeux, Multi-centered dilatations, congruent isomorphisms and Rost double deformation space,Transformation Groups, 31 (2026), 1801–1850
work page 2026
-
[6]
A. Mayeux, Formalizing all indexed mathematics as a benchmark for general reasoning, inIntelligent Systems and Applications — Proceed- ings of the 2026 Intelligent Systems Conference (IntelliSys), Lecture Notes in Networks and Systems, Springer, to appear, arXiv:2606.03835
arXiv 2026
- [7]
Show all 9 references
-
[9]
de Moura and S
L. de Moura and S. Ullrich, The Lean 4 theorem prover and program- ming language, inAutomated Deduction — CADE 28, Lecture Notes in Computer Science 12699, Springer, 2021, 625–635. University of Wisconsin–Madison, Madison, WI, USA Email address:mayeux@wisc.edu
2021
Reviewed August 11, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.