Pith. sign in

REVIEW 1 major objections 6 minor 2 cited by

Formalizing multi-graded Brenner-Schr\"oer Proj schemes and dilatations of rings in Lean4

T0 review · 1 major / 6 minor · reviewed 2026-07-12 · grok-4.5

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

Pith's one-line read A complete Lean 4 formalization of multi-graded Brenner–Schröer Proj schemes and ring dilatations is given, with public code.

desk verdict Solid Lean 4 library for multi-graded Brenner–Schröer Proj and dilatations; real infrastructure, not a new theorem. read the letter →

arxiv 2606.01438 v2 pith:MWB3D6SC submitted 2026-05-31 cs.LO

Arnaud Mayeux , Jujian Zhang This is my paper · ORCID
classification cs.LO MSC 14A1513A0268V20
keywords multi-gradedProjBrenner–SchröerLean4formalizationpotionshomogeneouslocalizationdilatationsofringsgraded
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

The paper builds a machine-checked account, inside Lean 4, of multi-graded projective schemes in the sense of Brenner and Schröer: schemes obtained by gluing “potions” (degree-zero pieces of homogeneous localizations) of rings graded by arbitrary abelian groups. It also formalizes multi-centered dilatations of rings and proves their universal property. The development supplies the graded-ring infrastructure, the notions of relevant homogeneous submonoids and good potion ingredients, the gluing data that produce the Proj scheme, functoriality of the construction, and the algebraic theory of dilatations. A sympathetic reader cares because multi-graded Proj appears in geometric representation theory and the minimal model program, while dilatations sit beside localization and blow-ups; a verified implementation turns these constructions into reusable, type-safe building blocks for further formalized algebraic geometry.

What carries the argument

Potions (degree-zero homogeneous localizations of a multi-graded ring at relevant finitely generated homogeneous submonoids) together with the gluing data that assemble Spec of those potions into the Proj scheme; the parallel formalization of multi-centered dilatations and their universal property.

What would settle it

Clone the cited repository, check out the revision corresponding to the paper, and run the Lean 4 build; any remaining sorry/admit or a mismatch between a formal statement and the corresponding mathematical claim would falsify the completeness claim.

Watch

Extended reading notes

Core claim

The authors give a fully formal Lean 4 implementation of the Brenner–Schröer multi-graded Proj construction (via relevant homogeneous submonoids, potions, finite potion generators, open immersions, and cocycle-compatible gluing) together with the definition and universal property of multi-centered dilatations of rings, following the algebraic treatment in the literature and releasing the corresponding code.

Load-bearing premise

That the publicly cited Lean code matches the statements of the paper and compiles without unfinished proofs; the manuscript itself only shows excerpts.

Editorial extensions

If this is right

  • Multi-graded Proj schemes become available as first-class objects inside a theorem prover for further geometric constructions.
  • Functoriality of the formalized Proj map is available for maps of graded rings.
  • The universal property of multi-centered dilatations can be invoked in other formal proofs that need blow-up-like ring operations.
  • Enlarging a family of good potion ingredients yields isomorphic formal Proj schemes, giving a flexible open cover.
  • The graded-ring and homogeneous-localization library can be reused for other multi-graded constructions.

Reading between the lines

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

  • The same infrastructure should support formal proofs of classical comparison results between multi-graded Proj and ordinary Proj or toric varieties.
  • Once dilatations are formal, one can attempt a machine-checked development of formal blow-ups and related deformation spaces.
  • The cocycle and open-immersion lemmas suggest a pattern for formalizing other gluing constructions that arise from monoid-graded rings.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

1 major / 6 minor

Summary. The paper presents a detailed Lean 4 formalization of multi-graded algebraic geometry constructions, centered on the Brenner–Schröer Proj of rings graded by abelian monoids/groups more general than N or Z, and on multi-centered dilatations of rings. Following the algebraic treatment of Mayeux–Riche and related literature, it develops graded ring homomorphisms, homogeneous and relevant submonoids, homogeneous localization, graded localization and tensor products, potions (degree-zero parts of homogeneous localizations), finite potion generators, gluing data via Scheme.GlueData, functoriality of Proj, and the definition plus universal property of dilatations. The manuscript supplies definitions, lemmas, theorems, and extensive Lean code excerpts, with the corresponding library made publicly available on GitHub.

Significance. Multi-graded Proj schemes appear in geometric representation theory and the minimal model program; a machine-checked formalization of the Brenner–Schröer construction and of dilatations therefore supplies reusable infrastructure for formalized algebraic geometry in Lean/mathlib. The work ships concrete, publicly available code covering relevant homogeneous submonoids, potions, gluing, functoriality, and the universal property of multi-centered dilatations—strengths that are load-bearing for a formalization paper. If the repository matches the claims, the contribution is a solid foundation for further formal developments rather than a purely expository account.

major comments (1)
  1. The central claim is that a complete formalization exists and is publicly available ([11]). The manuscript contains only excerpts and no commit hash, Lean version pin, or statement that the repository is free of sorry/admit. For a formalization paper this is a load-bearing verification gap: an independent reader cannot re-check from the text alone that the formal statements match the mathematical claims of §§3–11 (especially the GlueData construction of §8 and the universal property of §11). A fixed commit hash and a short verification note would close the gap without altering the mathematics.
minor comments (6)
  1. Abstract and Introduction: the hyphenation and spelling of “Brenner–Schröer” / “Schroër” / “Schroer” are inconsistent; standardize throughout.
  2. §2, Listing 1 and surrounding text: the general graded-ring setup is versatile but dense; a short pointer to the Wieser–Zhang graded-rings paper [14] already cited would help readers less familiar with the mathlib design.
  3. §7–8: the terminology “potion” / “good potion ingredient” is taken from [9] but may be opaque on first reading; a one-sentence reminder of the mathematical meaning (degree-zero part of a homogeneous localization; relevant and finitely generated homogeneous submonoid) at the first occurrence would improve accessibility.
  4. §10, Remark 9: the type-theoretic obstruction to writing Proj as a strict contravariant functor (id⋆F not definitionally equal to F) is correctly noted; a brief remark on whether a future redesign could remove the need for projHomOfLE would be useful for library maintainers.
  5. References: several arXiv numbers and “to appear” entries are fine for a formalization paper, but ensuring that the GitHub link [11] remains stable (or is archived) would aid long-term reproducibility.
  6. Scattered typos and formatting: “constructoin”, “exsitence”, “ingrient”, “Schroër” vs “Schröer”, and occasional missing spaces around math mode; a light copy-edit pass would clean these.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: Lean formalization of published multi-graded Proj and dilatations, with only minor self-citations to authors' prior announcement and code repo.

full rationale

The paper is a formalization effort whose central deliverable is a Lean 4 implementation of the Brenner–Schröer multi-graded Proj (via relevant homogeneous submonoids, potions, Scheme.GlueData gluing, and functoriality) and of multi-centered dilatations (including the universal property). The mathematical development tracks the algebraic treatment of Mayeux–Riche [9] and classical sources [2,3,8,12]; definitions (e.g., HomogeneousSubmonoid, IsRelevant, PotionGen, GoodPotionIngredient, Dilatation) and lemmas are constructed from first principles inside Lean and do not reduce by construction to the target claims. Self-citations ([9], short note [10], GitHub [11]) document prior announcements and the code itself; they are not used to import an unverified uniqueness theorem or ansatz that forces the results. There are no fitted parameters, no self-definitional loops equating a prediction to its input, and no renaming of an empirical pattern presented as a new derivation. Residual risk that the public repository may contain sorry/admit is extrinsic to the paper's argument and does not create circularity in the derivation chain. Score 1 reflects only the presence of ordinary author self-citation that is not load-bearing.

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

The paper is a formalization of existing mathematics; it introduces no free parameters and no new physical or mathematical entities. The only background assumptions are standard Lean/mathlib foundations (commutative algebra, scheme theory already present in mathlib) and the correctness of the external GitHub repository.

assumptions (2)
  • standard math Standard commutative algebra and scheme theory as formalized in mathlib (graded rings, localizations, Spec, GlueData).
    Used throughout Sections 2–11 as the ambient library.
  • domain assumption The algebraic treatment of multi-graded Proj given in Mayeux–Riche [9] is correct.
    The formalization follows that reference; any gap in [9] would propagate.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Formalizing multi-graded Brenner-Schr\"oer Proj schemes and dilatations of rings in Lean4." pith.science (2026). https://pith.science/paper/MWB3D6SC

@misc{pith2026260601438,
  author       = {Pith},
  title        = {Pith review of: Formalizing multi-graded Brenner-Schr\"oer Proj schemes and dilatations of rings in Lean4},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/MWB3D6SC}},
  note         = {Machine review of arXiv:2606.01438}
}
read the original abstract

We present a detailed formalization in Lean4 of some multigraded algebraic geometry constructions, focusing on the Brenner--Schr\"oer Proj construction and algebraic dilatations of rings.

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Dilatations of categories, via their lean formalization

    cs.LO 2026-08 conditional novelty 6.0 of 10

    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.

  2. Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge

    cs.DL 2026-06 unverdicted novelty 5.0 of 10

    Authors propose a bridge database linking math publications to formal proof libraries and introduce a formalization score estimated via cross-document alignment to Lean as a feasibility study.

Reference graph

Works this paper leans on

14 extracted references · 3 linked inside Pith · cited by 2 Pith papers

  1. [11]

    Mayeux and J

    A. Mayeux and J. Zhang,Multi-graded Proj construction in Lean4, https://github.com/ProjConstruction/Proj (2025)

    2025

  2. [1]

    Bouthier, E

    A. Bouthier, E. Vasserot,On the geometric Satake equivalence for Kac-Moody groups, arXiv:2510.11466 (2025)

    arXiv 2025

  3. [2]

    H.Brenner, S.Schröer,Ample families, multihomogeneous spectra, and alge- braization of formal schemesPacific J. Math. 208 (2003), no. 2, 209–230

    2003

  4. [3]

    Dubouloz, A

    A. Dubouloz, A. Mayeux, and J. P. dos Santos,A survey on algebraic dilatations, arXiv:2306.17003

    arXiv

  5. [4]

    Etude globale elementaire de quelques classes de morphismesPublications mathématiques de l’I.H.E.S., tome 8 (1961), p

    A.Grothendieck,EGA : II. Etude globale elementaire de quelques classes de morphismesPublications mathématiques de l’I.H.E.S., tome 8 (1961), p. 5-222 32

    1961

  6. [5]

    Kuronya, P

    A. Kuronya, P. Souza, and M. Ulirsch,Tropicalization of toric prevarieties, preprint arXiv:2107.03139

    arXiv

  7. [6]

    Li and J

    F. Li and J. Zhang,Dimension Theory in Lean4, 2025, https://github.com/jjaassoonn/DimensionTheory

    2025

  8. [7]

    The mathlib Community,Mathlib4 Documentation

Show all 14 references
  1. [8]

    MayeuxMulti-centered Dilatations, Congruent Isomorphisms and Rost Dou- ble Deformation Space.Volume 31, pages 1801–1850 (2026)

    A. MayeuxMulti-centered Dilatations, Congruent Isomorphisms and Rost Dou- ble Deformation Space.Volume 31, pages 1801–1850 (2026)

    2026

  2. [9]

    Mayeux and S

    A. Mayeux and S. Riche,On multi-graded Proj schemes, Publ. Res. Inst. Math. Sci. (2026)

    2026

  3. [10]

    Mayeux and J

    A. Mayeux and J. Zhang,The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction, Springer Proc. Math. Stat., to appear

  4. [12]

    Zhang,Formalising the Proj construction in Lean, in14th International Con- ference on Interactive Theorem Proving, Art

    J. Zhang,Formalising the Proj construction in Lean, in14th International Con- ference on Interactive Theorem Proving, Art. No. 35, LIPIcs. Leibniz Int. Proc. Inform., 268 (2023)

    2023

  5. [13]

    E.Wieser and J.Zhang,Graded rings in Lean’s dependent type theory,inIntel- ligent computer mathematics, 122–137, Lecture Notes in Comput. Sci. Lecture Notes in Artificial Intelligence, 13467 , Springer, Cham, 2022

    2022

  6. [14]

    Yasuda,An algorithm for the minimal model program in dimension three, (2026) arXiv:2603.13703 33

    T. Yasuda,An algorithm for the minimal model program in dimension three, (2026) arXiv:2603.13703 33

    2026 arXiv

Pith tools

Reviewed July 12, 2026 · model on record in the stance chip above.