← All papers
Schemes in Lean
math.AG
Jan 7, 2021 · v2
TL;DR
Describes three approaches to formalizing algebraic geometry schemes in Lean.
Abstract
We tell the story of how schemes were formalised in three different ways in the Lean theorem prover.
Problem
Schemes are central objects in algebraic geometry, but formalizing their definition in a proof assistant requires handling complex constructions involving sheaves, locally ringed spaces, and gluing.
Approach
The authors formalize schemes in the Lean theorem prover, exploring three different approaches to the definition. The work demonstrates how different formalization strategies affect the difficulty and elegance of the resulting formal development.
Results
The paper tells the story of three different formalizations of schemes in Lean, contributing to the mathematical library and demonstrating feasibility of formalizing modern algebraic geometry.