Schemes in Lean

DOI10.1080/10586458.2021.1983489zbMATH Open1497.14003arXiv2101.02602OpenAlexW3217786894MaRDI QIDQ5094471FDOQ5094471

Authors:

Publication date: 3 August 2022

Published in: Experimental Mathematics (Search for Journal in Brave)

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

Full work available at URL: https://arxiv.org/abs/2101.02602

Recommendations

• Simple type theory is not too simple: Grothendieck's schemes without dependent types
• On the role of formalization in computational mathematics
• Exploring formalisation. A primer in human-readable mathematics in Lean 3 with examples from simplicial topology
• Formalizing geometric algebra in Lean
• scientific article; zbMATH DE number 7699422

zbMATH Keywords

formal proofschemeLean

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20) Schemes and morphisms (14A15)

Cites Work

• The Lean Theorem Prover (System Description)
• Title not available (Why is that?)
• Éléments de géométrie algébrique. I: Le langage des schémas. II: Étude globale élémentaire de quelques classe de morphismes. III: Étude cohomologique des faisceaux cohérents (première partie)
• Title not available (Why is that?)

Cited In (3)

• Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types
• Title not available (Why is that?)
• Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project

Uses Software

• Lean
• mathlib

This page was built for publication: Schemes in Lean

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5094471)