The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction
Arnaud Mayeux, Jujian Zhang
Published: 2025/9/18
Abstract
We formalize the multi-graded Proj construction in Lean4, illustrating mechanized mathematics and formalization.