Schemes in Lean
From MaRDI portal
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
(9)- 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
- Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project
- scientific article; zbMATH DE number 7699422 (Why is no real title available?)
- The functor of points approach to schemes in cubical Agda
- A complete formalization of Fermat's last theorem for regular primes in Lean
- Formalization of derived categories in Lean/mathlib
- Constructing the Lie algebra of smooth vector fields on a Lie group in Isabelle/HOL
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)
