Abstract🔗

This project consists of an exploration of the Lean 4 system as a proof assistant through a case study: the formalisation of results in general topology. The main objective is to deepen the understanding of this system and to provide a critical perspective on its advantages and disadvantages when writing mathematics. A general overview of the foundational basis of the system, its syntax, and its concrete application to topology is provided. The project concludes with a description of the process of formalising the more complex result Urysohn's Lemma, as well as the insights gained throughout the work.