Schemes in Lean
Algebraic Geometry
2022-03-21 v2
Authors:
Kevin Buzzard
, Chris Hughes
, Kenny Lau
, Amelia Livingston
, Ramon Fernández Mir
, Scott Morrison
Abstract
We tell the story of how schemes were formalised in three different ways in the Lean theorem prover.
Cite
@article{arxiv.2101.02602,
title = {Schemes in Lean},
author = {Kevin Buzzard and Chris Hughes and Kenny Lau and Amelia Livingston and Ramon Fernández Mir and Scott Morrison},
journal= {arXiv preprint arXiv:2101.02602},
year = {2022}
}
Comments
10 pages. To appear in Experimental Mathematics
Related papers
View all related →
Logic in Computer Science · Computer Science
The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction
Arnaud Mayeux, Jujian Zhang
2025-09-19
Artificial Intelligence · Computer Science
Using Argumentation Schemes to Model Legal Reasoning
Trevor Bench-Capon, Katie Atkinson
2022-10-04
Computation and Language · Computer Science
LeanReasoner: Boosting Complex Logical Reasoning with Lean
Dongwei Jiang, Marcio Fonseca, Shay B. Cohen
2024-03-21
Logic in Computer Science · Computer Science
Formalizing Chemical Physics using the Lean Theorem Prover
Maxwell P. Bobbin, Samiha Sharlin, Parivash Feyzishendi, An Hong Dang +2
2023-12-14
Logic in Computer Science · Computer Science
Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean
Viviana del Barco, Gustavo Infanti, Exequiel Rivas, Paul Schwahn
2025-05-27
Optimization and Control · Mathematics
Verified Optimization
Alexander Bentkamp, Jeremy Avigad
2021-11-15
Logic in Computer Science · Computer Science
Elements of Differential Geometry in Lean: A Report for Mathematicians
Anthony Bordg, Nicolò Cavalleri
2021-08-03
Combinatorics · Mathematics
Capturing properties of planar diagrams in Lean proof assistant software
Alastair Litterick, Alexei Vernitski, Billy Woods
2026-02-11
Logic in Computer Science · Computer Science
Verified reductions for optimization
Alexander Bentkamp, Ramon Fernández Mir, Jeremy Avigad
2023-02-23
Logic in Computer Science · Computer Science
Voting Theory in the Lean Theorem Prover
Wesley H. Holliday, Chase Norman, Eric Pacuit
2021-10-19
Logic in Computer Science · Computer Science
A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances
Xichen Tang
2025-02-03
Logic in Computer Science · Computer Science
Intuitionistic Propositional Logic in Lean
Dafina Trufaş
2024-11-01
Logic in Computer Science · Computer Science
A Novice-Friendly Induction Tactic for Lean
Jannis Limperg
2020-12-17
Computation and Language · Computer Science
Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4
Xichen Tang
2024-11-11
Logic in Computer Science · Computer Science
Elaboration in Dependent Type Theory
Leonardo de Moura, Jeremy Avigad, Soonho Kong, Cody Roux
2015-12-18
Logic in Computer Science · Computer Science
A formalization of the change of variables formula for integrals in mathlib
Sébastien Gouëzel
2022-07-27
Logic in Computer Science · Computer Science
A formalization of forcing and the unprovability of the continuum hypothesis
Jesse Michael Han, Floris van Doorn
2019-04-25
Human-Computer Interaction · Computer Science
Explorable Theorems: Making Written Theorems Explorable by Grounding Them in Formal Representations
Hita Kambhamettu, Will Crichton, Sean Welleck, Harrison Goldstein +1
2026-04-13
Number Theory · Mathematics
Formalising the Bruhat-Tits Tree
Judith Ludwig, Christian Merten
2026-04-22
Human-Computer Interaction · Computer Science
Human-in-the-Loop Schema Induction
Tianyi Zhang, Isaac Tham, Zhaoyi Hou, Jiaxuan Ren +11
2023-08-23
Logic in Computer Science · Computer Science
Translating Informal Proofs into Formal Proofs Using a Chain of States
Ziyu Wang, Bowen Yang, Chenyi Li, Yuan Zhang +3
2025-12-15
Logic in Computer Science · Computer Science
Formalizing computability theory via partial recursive functions
Mario Carneiro
2019-07-19
Logic in Computer Science · Computer Science
Bootstrapping LCF Declarative Proofs
Phil Scott, Steven Obua, Jacques Fleuriot
2017-03-17
Logic in Computer Science · Computer Science
A Formalization of Divided Powers in Lean
Antoine Chambert-Loir, María Inés de Frutos-Fernández
2025-07-09
Logic · Mathematics
A Formal Proof of the Independence of the Continuum Hypothesis
Jesse Michael Han, Floris van Doorn
2021-02-08