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

2025/09/18 by Arnaud Mayeux, Mayeux, Arnaud, Zhang, Jujian
Business, Management and Accounting · Computer Science · #Algebraic Geometry (math.AG) #Artificial Intelligence (cs.AI) #Big Data and Business Intelligence #Competitive and Knowledge Intelligence #FOS: Computer and information sciences #FOS: Mathematics #Logic in Computer Science (cs.LO) #Semantic Web and Ontologies

paper · pdf · doi:10.48550/arxiv.2509.15116

openalex publication_date 2025/09/18 · openalex created_date 2025/10/13 · openalex updated_date 2026/07/28

Abstract

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

Citations

• Schemes in Lean

Related

• A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances
• Schemes in Lean
• Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4
• First steps towards Computational Polynomials in Lean
• Lean-auto: An Interface between Lean 4 and Automated Theorem Provers