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)

[14] Morph (2023)

←[13] Lean Prover Community (2023)[15] Gao, Ju, Jiang, Qin and Dong (2024)→

[14] Morph (2023)🔗

Morph, 2023. “Moogle, a semantic search engine for Mathlib, the Lean mathematical library”. Last accessed: May 24, 2025.

←[13] Lean Prover Community (2023)[15] Gao, Ju, Jiang, Qin and Dong (2024)→