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

arXiv: https://arxiv.org/abs/2606.01438 · HTML: https://mlsanity.com/paper/2606.01438/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 31 May 2026.

## Built on by (most cited first, 2 of 2)

- [Lean Pool: An AI-Maintained Archive of Formalized Mathematics](https://mlsanity.com/paper/2609.25199/) (2026)
- [Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge](https://mlsanity.com/paper/2606.11430/) (2026)

## Abstract (arXiv)

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.