Schemes in Lean

Hassler Whitney, Differentiable manifolds , Ann. of Math. (2) 37

1936

Earlier work this paper cites.

André Weil, Foundations of Algebraic Geometry , American Mathematical Society Colloquium Publications, vol. 29, American Mathematical Society, New York, 1946. MR 0023093

1946

Earlier work this paper cites.

A. Grothendieck, Éléments de géométrie algébrique. I. Le langage des schémas , Inst. Hautes Études Sci. Publ. Math. (1960), no. 4, 228. MR 217083

1960

Earlier work this paper cites.

Robin Hartshorne, Algebraic geometry , Springer-Verlag, New York-Heidelberg, 1977, Graduate Texts in Mathematics, No. 52. MR 0463157

1977

Earlier work this paper cites.

Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer, The lean theorem prover (system description) , Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, 2015, pp. 378–388

2015

Cited alongside, same era.

Kevin Buzzard, Chris Hughes, and Kenny Lau, Formal verification of parts of the Stacks project in Lean , https://github.com/kbuzzard/lean-stacks-project , 2018

2018

Cited alongside, same era.

Ramon Fernández Mir, Schemes in Lean (v2) , https://github.com/ramonfmir/lean-scheme , 2019

2019

Cited alongside, same era.

Kevin Buzzard, Johan Commelin, and Patrick Massot, 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, 2020, 2020, pp. 299–312

2020

Later among the works it cites.

The mathlib community, 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, 2020, 2020, pp. 367–381

2020

Later among the works it cites.

The Stacks Project Authors, Stacks Project , https://stacks.math.columbia.edu , 2021

2021

Closest in time.