Formalising Mathematics with Lean
Formalising Mathematics with Lean
Table of Contents
Abstract
1.
Introduction
2.
Lean Theorem Prover
3.
Topological Spaces in Lean
4.
Urysohn's Lemma
5.
Conclusion
References
References
[1] Trinh, Wu, Le, He and Luong (2024)
[2] Geuvers (2009)
[3] Buzzard (2024)
[4] Avigad, De Moura, Kong, Ullrich and Lean community contributors (2024)
[5] Lean Prover Community
[6] Bailey and Lean community contributors (2024)
[7] Avigad, De Moura and Kong (2021)
[8] Sørensen and Urzyczyn (2006)
[9] Coquand and Huet (1986)
[10] Pierce (2002)
[11] Carneiro (2019)
[12] Carneiro (2024)
[13] Lean Prover Community (2023)
[14] Morph (2023)
[15] Gao, Ju, Jiang, Qin and Dong (2024)
[16] Willard (2012)
[17] Lean Prover Community (2023)
[9] Coquand and Huet (1986)
←
[8] Sørensen and Urzyczyn (2006)
[10] Pierce (2002)
→
[9] Coquand and Huet (1986)
🔗
Thierry Coquand y Gérard Huet, 1986.
The calculus of constructions
. Tesis doctoral, INRIA
←
[8] Sørensen and Urzyczyn (2006)
[10] Pierce (2002)
→