用编程语言验证数学构造，让证明可机器检查。

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

• 用 Lean4 编程语言形式化多分次 Proj 构造
• 完成数学证明的机械化验证，确保无逻辑漏洞
• 适合数学研究者与形式化系统爱好者

我们使用 Lean4 对多分次 Proj 构造进行了形式化，展示了机械化数学与形式化验证的实践方法。该工作将抽象代数几何中的核心构造转化为计算机可检查的证明，确保其逻辑严谨性。通过在 Lean4 中构建完整定义与定理链，验证了多分次射影谱的构造过程，为后续形式化代数几何奠定了基础。该成果体现了形式化数学在提高可信度和促进知识积累方面的潜力。

原文摘要 · Abstract (English)

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

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。