Papers With

← All papers
First page of The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction

The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction

Arnaud Mayeux, Jujian Zhang

cs.LO Sep 18, 2025 · v1
formalization algebra geometry
Read PDF arXiv abstract Code
TL;DR
Formalizes the multi-graded Proj construction from algebraic geometry in Lean 4.
Abstract
We formalize the multi-graded Proj construction in Lean4, illustrating mechanized mathematics and formalization.
Problem

The multi-graded Proj construction in algebraic geometry, which generalizes the classical Proj to gradings by arbitrary commutative monoids, lacked a machine-checked formalization.

Approach

The authors formalize the multi-graded Proj construction in Lean 4, covering the relevant homogeneous localizations, the gluing of affine schemes, and the Segre embedding relating products of Proj schemes. The formalization illustrates the mechanization of modern algebraic geometry.

Results

The formalization includes key results such as covering properties of Spec(A_(f1+...+fn)) and the isomorphism Proj^{MxM'}(A tensor A') = Proj^M(A) x Proj^{M'}(A') over Spec(R).