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

arXiv:2509.15116v1 Announce Type: cross
Abstract: We formalize the multi-graded Proj construction in Lean4, illustrating mechanized mathematics and formalization.