← All papers
Formalizing multi-graded Brenner-Schröer Proj schemes and dilatations of rings in Lean4
cs.LO
May 31, 2026 · v2
TL;DR
Formalizes multigraded Brenner–Schröer Proj schemes and algebraic dilatations of rings in Lean 4, presumably building on Mathlib's scheme theory.
Abstract
We present a detailed formalization in Lean4 of some multigraded algebraic geometry constructions, focusing on the Brenner–Schröer Proj construction and algebraic dilatations of rings.
Problem
Multigraded algebraic geometry constructions, including the Brenner–Schröer Proj construction and algebraic dilatations of rings, had not been formalized in a proof assistant.
Approach
The authors give a detailed Lean 4 formalization of these constructions. The Proj construction is developed in the multigraded setting, and dilatations of rings are formalized as algebraic objects.
Results
A Lean 4 formalization of the multigraded Brenner–Schröer Proj construction and of algebraic dilatations of rings.