1.3. Structure of this document🔗

This document is organised in four main parts. First, a detailed introduction to the Lean language is presented, including its mathematical foundations and its use as an assistant for proving mathematics.

Next, some results of general topology are introduced. The goal of that section is not to develop a complete theory, but to illustrate through concrete examples how topological properties are formalised and how spaces are described in Lean.

The third part is the core of this work: the process of formalising Urysohn's lemma and its proof is presented in detail. The path followed is described together with the main difficulties encountered along the way and the strategies used to overcome them. The section ends with a comparison with the ideas used in the Mathlib proof.

All the code developed during the project, including the Lean definitions and proofs, is available in this public repository. This repository complements the written report and makes it easy to reproduce or consult the formal results obtained.

Finally, the conclusions are presented, focusing on the difficulties and advantages of writing proofs in a formal environment such as Lean.