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

Arnaud Mayeux, Jujian Zhang

We formalize the multi-graded Proj construction in Lean4, illustrating mechanized mathematics and formalization.