5. Conclusion🔗

Throughout this work, three main objectives have been pursued: learning to use Lean as a proof assistant, formalising an advanced-level mathematical result, Urysohn's lemma, and, as a result of both, acquiring a deep understanding of the formal verification process, its advantages and its difficulties. This section presents the main conclusions I have drawn from this experience.

1. 5.1. Learning Lean
2. 5.2. Formalisation of Urysohn's lemma
3. 5.3. Possible improvements and extensions