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)

[12] Carneiro (2024)

←[11] Carneiro (2019)[13] Lean Prover Community (2023)→

[12] Carneiro (2024)🔗

Mario Carneiro, 2024. “Lean4Lean: Towards a formalized metatheory for the Lean theorem prover”. arXiv e-prints, arXiv:2403.

←[11] Carneiro (2019)[13] Lean Prover Community (2023)→