1.2. Work plan🔗

The first step was to acquire basic knowledge about Lean. To do so, I enrolled in the Lean course taught by CompuMates at the Faculty of Mathematics during the 2023/24 academic year. This gave me some first basic notions and let me start writing small proofs in Lean 3, mainly focused on propositional logic.

From then on, my interest in Lean grew, and I began to study, in a self-taught way, the more recent Lean 4 version, currently under active development. In particular, I followed in detail the online course Formalising Mathematics 2024 taught by Kevin Buzzard (Kevin Buzzard, 2024)Kevin Buzzard, 2024. “Formalising Mathematics 2024”. Imperial College London. Last accessed: June 22, 2025., completing the proposed exercises up to chapter 10, devoted to topological spaces.

That chapter was very brief, and only included two examples of concrete topological spaces and some questions about continuity of functions. The exercises I solved during this initial stage can be found in this repository.

Given the scarcity of material about topology, I decided to reinforce this learning by taking as a reference the notes I had taken during the Elementary Topology course of the degree. I began to formalise the main results I had seen in class. Part of this work is presented in section 3 of this document.

While making progress on this task, I reached the topic of separation axioms. Since we had not worked with normal spaces during the course, I turned to other sources to understand this notion. It was then that I wrote for the first time in Lean the statement of Urysohn's lemma and, from that point on, I focused the rest of the work on its formalisation.

Finally, since this result was already proved in the official Mathlib library, I have studied that implementation with the aim of understanding its approach and comparing its fundamental ideas with the ones used in my own formalisation.