Advanced search
Publication Cover
Experimental Mathematics Volume 31, 2022 - Issue 2
Submit an article Journal homepage
5,852
Views
1
CrossRef citations to date
0
Altmetric
Interactive Theorem Provers

Schemes in Lean

Kevin Buzzarda Department of Mathematics, Imperial College London, London, UKCorrespondence[email protected]
View further author information
,
Chris Hughesa Department of Mathematics, Imperial College London, London, UKView further author information
,
Kenny Laua Department of Mathematics, Imperial College London, London, UKView further author information
,
Amelia Livingstona Department of Mathematics, Imperial College London, London, UKView further author information
,
Ramon Fernández Mirb School of Informatics, University of Edinburgh, Edinburgh, UKView further author information
&
Scott Morrisonc School of Mathematics and Statistics, University of Sydney, Sydney, AustraliaView further author information
Pages 355-363 | Published online: 25 Nov 2021

References

  • Buzzard, K., Commelin, J., Massot, P. (2020). Formalising perfectoid spaces, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20–21, pp. 299–312.
  • Buzzard, K., Hughes, C., Lau, K. (2018). Formal verification of parts of the Stacks project in Lean, https://github.com/kbuzzard/lean-stacks-project.
  • de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J. (2015). The lean theorem prover (system description). Automated Deduction—CADE-25 -25th International Conference on Automated Deduction, Berlin, Germany, August 1–7, 2015, Proceedings, pp. 378–388.
  • Fernández Mir, R. (2019). Schemes in Lean (v2), https://github.com/ramonfmir/lean-scheme.
  • Grothendieck, A. (1960). Eléments de géométrie algébrique. I. Le langage des schémas, Inst. Hautes Études Sci. Publ. Math. no. 4, 228.
  • Hartshorne, R. (1977). Algebraic geometry, New York: Springer-Verlag, Graduate Texts in Mathematics, No. 52.
  • The mathlib community, (2020). The Lean mathematical library, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20–21, pp. 367–381.
  • The Stacks Project Authors. (2021). Stacks Project. Available at: https://stacks.math.columbia.edu.
  • Weil, A. (1946). Foundations of Algebraic Geometry, American Mathematical Society Colloquium Publications, Vol. 29. New York: American Mathematical Society.
  • Whitney, H. (1936). Differentiable manifolds. Ann. Math. (2) 37(3):645–680.

Related research

People also read lists articles that other readers of this article have read.

Recommended articles lists articles that we recommend and is powered by our AI driven recommendation engine.

Cited by lists all citing articles based on Crossref citations.
Articles with the Crossref icon will open in a new tab.