Schemes in Lean
From MaRDI portal
Publication:5094471
Abstract: We tell the story of how schemes were formalised in three different ways in the Lean theorem prover.
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
Cites work
- scientific article; zbMATH DE number 3572315 (Why is no real title available?)
- scientific article; zbMATH DE number 3108009 (Why is no real title available?)
- The Lean theorem prover (system description)
- É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)
Cited in
(5)- A formalization of Dedekind domains and class groups of global fields
- Exploring formalisation. A primer in human-readable mathematics in Lean 3 with examples from simplicial topology
- Simple type theory is not too simple: Grothendieck's schemes without dependent types
- scientific article; zbMATH DE number 7699422 (Why is no real title available?)
- Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project
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)
