1.1. Objectives🔗

The main objective is to acquire a solid knowledge of the Lean proof assistant, becoming able to formalise simple results from the Mathematics degree.

Once a certain familiarity with the system has been reached, an additional objective is the formalisation of a relevant result that illustrates the difficulties of the process of proving results in a formal language.

To this end, Urysohn's lemma was chosen: a central result of general topology whose proof requires, among other tools, the use of different kinds of induction. This makes it possible to reach a more advanced command of the Lean system, since it involves features that are not elementary.

Finally, through this process of learning and testing, the aim is to come to understand the advantages and the difficulties involved in bringing mathematics into the environment of a proof assistant.