5.1. Learning Lean🔗

The process of learning Lean has been very smooth. The availability of resources such as Kevin Buzzard's course (Formalising Mathematics), the official documentation and other materials created by the community, such as the Natural Number GameThe Natural number game is an interactive game devoted to learning how to work with natural numbers in Lean's tactic mode. See: https://adam.math.hhu.de/#/g/leanprover-community/nng4., made my first steps enormously easier.

However, as I made progress, I began to detect a second, more subtle level of learning: although my solutions to the exercises proposed by Buzzard were correct from a formal point of view (accepted by Lean), they were considerably longer and more convoluted than the solutions proposed in the course.

This made me see that, besides learning to construct valid proofs, there is an additional learning process focused on how to write efficient and elegant proofs in Lean, which requires a deeper understanding of the tactics and the good practices of the language (such as avoiding the overuse of simp).

This same situation repeated itself during the formalisation of the basic topology results of the second section. Many of the proofs that appear in this report were initially much longer, more redundant or more confusing. The work of revision and simplification has been constant; as I learned new ways of simplifying problems, I went back over my steps to improve the previous results.

Even so, there is still room for improvement. Compared with the versions available in Mathlib, my proofs could be reduced even further. Nevertheless, I consider that this simplification effort has a reasonable limit in the context of the objectives of this work, since optimising to the maximum usually comes at the expense of code readability. Some Mathlib proofs are very hard to follow precisely because of their high level of compactness.

During this stage I also understood the importance of reusing the definitions existing in Mathlib. Although at the beginning I defined concepts such as continuity, closure or normal spaces on my own, later on I switched to using the standard definitions of the library, which turned out to be much more practical.

This process also forced me to consolidate my understanding of the mathematical concepts I was working with, since formalising them demands facing their definitions with a level of precision and detail that is not usually required when working on paper. Moreover, I got a fairly clear idea of how certain objects can be formalised by comparing my definitions with those of the library that I used afterwards.

Finally, this transition allowed me to start developing a certain intuition about which results are already formalised in Mathlib and in what way they might be written, in order to locate them through tools such as exact?. Also, upon running into the limitations of these tools, I learned to use more powerful tools such as LeanSearch or Moogle.

For all of this, including this part in the work seemed especially relevant to me.