Schemes in Lean

2021/01/07 by Kevin Buzzard, Chris Hughes, Kenny Lau +3 · 2 voices · 1 citation
Mathematics · #math.AG

paper · pdf · doi:10.1080/10586458.2021.1983489

Abstract

We tell the story of how schemes were formalised in three different ways in the Lean theorem prover.

Cited by

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

Discussions

• Schemes in Lean [lobsters, 5 points, 0 comments]
• Schemes in Lean [hn, 1 points, 0 comments]

Related

• First steps towards Computational Polynomials in Lean
• A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances
• A Novice-Friendly Induction Tactic for Lean
• Lean-SMT: An SMT tactic for discharging proof goals in Lean
• LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover