LOMay 31
Formalizing multi-graded Brenner-Schröer Proj schemes and dilatations of rings in Lean4
arXiv:2606.0143813.1
Predicted impact top 59% in LO · last 90 daysOriginality Synthesis-oriented
AI Analysis
This work provides a foundational formalization for algebraic geometry in Lean4, enabling future verification of complex theorems.
The authors formalized multi-graded Proj constructions and ring dilatations in Lean4, enabling computer-verified proofs in algebraic geometry.
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.