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)

[11] Carneiro (2019)

←[10] Pierce (2002)[12] Carneiro (2024)→

[11] Carneiro (2019)🔗

Mario Carneiro, 2019. “The Type Theory of Lean”. Section 5, "Reduction of inductive types to W-types".

←[10] Pierce (2002)[12] Carneiro (2024)→