5.2. Formalisation of Urysohn's lemma🔗

The formalisation of Urysohn's lemma has been, without a doubt, the most demanding part of the work. Since it is a proof with relatively complex mathematical ideas, trying to adapt them to Lean's paradigm, which is much more structured and restrictive, has been an added difficulty. Many intuitions that are immediate on paper require considerable effort to be translated into the formal language.

An example of this is the proof that the sequence of open sets obtained was monotone (the property ★). In all the sources consulted, this property is presented as something that follows trivially from the construction. However, in Lean it was necessary to build this part carefully, and finding the right way to do it took me several months.

Of course, once the formalisation was complete, the result was an extensive piece of code hundreds of lines long. In the same way as in the previous stage, I have been simplifying it, mainly by extracting auxiliary results out of the main file so that they could be reused later. In spite of everything, the Mathlib proof we discussed at the end is still significantly shorter.

Beyond this, this experience has made me see that there is a certain way of thinking that develops over time when working with Lean: it is not simply a matter of translating the paper proof line by line, but of finding a formulation that is more computationally suitable. For example, topology in Mathlib is formalised, in general, using the language of filters. In my case, since I was not familiar with this tool, I opted for an alternative strategy that fitted my knowledge better, but which in the end turned out to be much less efficient.

In any case, this effort has been a great opportunity to improve my command of the language. An especially difficult part has been the use of different kinds of induction throughout the proof. Since many of my initial ideas did not work, I ended up writing and proving different variants of induction in order to understand why certain approaches were not valid and how to adapt them correctly.

Another aspect I found complex was cooperating with Lean's type inference. Although in general Lean automatically resolves many typing details, saving a lot of work, sometimes this automation becomes an obstacle. A clear example of this has been having to define a modified version of the function F so that it returned sets in \mathbb{R} instead of in \mathbb{Q} and thus be able to define its real infimum.

However, this difficulty has also led me to learn to use especially useful tools such as the exact_mod_cast tactic or the Subtype.val function of Mathlib.

In summary, this process has been key to consolidating my knowledge of Lean and understanding how to approach the formalisation of complex mathematical results within an assisted environment.