The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction
arXiv:2509.15116
Abstract
We formalize the multi-graded Proj construction in Lean4, illustrating mechanized mathematics and formalization.
Short note