5.3. Possible improvements and extensions🔗

There are several directions in which the work done could be extended or improved:

• Systematic use of Mathlib definitions

  Although in early versions I used my own definitions for certain concepts, later on I replaced them with the Mathlib definitions. However, there are still some objects that I have not managed to integrate completely, such as the definition of topological subspace or that of the usual topology.

  The goal of this work was not primarily to make the result reusable in other developments, since the formalisation of Urysohn's lemma already exists in Mathlib, but to understand the formalisation process in detail and reflect on the difficulties that may arise. Nevertheless, it would be interesting to rewrite the proof in such a way that only standard Mathlib definitions and constructions are used, in order to go deeper into their implementations and usage patterns.

  In particular, it is proposed to express the theorem in the following form:

  theorem declaration uses `sorry`Urysohn {X : Type} [T : TopologicalSpace X] [N : NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : ∃ f : X → ℝ, Continuous f ∧ Set.EqOn f 0 s ∧ Set.EqOn f 1 t ∧ ∀ x, f x ∈ Set.Icc 0 1 := byX:TypeT:TopologicalSpace XN:NormalSpace Xs:Set Xt:Set Xhs:IsClosed sht:IsClosed thd:Disjoint s t⊢ ∃ f, Continuous f ∧ Set.EqOn f 0 s ∧ Set.EqOn f 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1 sorryAll goals completed! 🐙

  In this statement, the topology accompanying the space of real numbers is automatically assumed in the definition of continuity through an instance that Lean infers by default. Therefore, it would only remain to check that this instance corresponds to the definition of the usual topology I have used, by proving this result:

  lemma declaration uses `sorry`my_usual_equiv : @UniformSpace.toTopologicalSpace ℝ (by⊢ UniformSpace ℝ exact PseudoEMetricSpace.toUniformSpaceAll goals completed! 🐙) = UsualTopology := by⊢ PseudoEMetricSpace.toUniformSpace.toTopologicalSpace = UsualTopology sorryAll goals completed! 🐙

• Code documentation

  A possible improvement would be to write the documentation of the code following the style used in Mathlib's. The Lean community offers a tool that generates this kind of documentation automatically from the comments written in the .lean filesSee: https://github.com/leanprover-community/doc-gen.. Another option could be to use a tool such as leanblueprint, which makes it possible to create and publish, in an automated way, a presentation of the project in the form of a "blueprint"See: https://github.com/PatrickMassot/leanblueprint..

• Topology Game

  An interesting line would be to design a resource similar to the Natural Number Game, but focused on introducing the basic concepts of topology formalised in Lean. This would not only reinforce my own learning, but could also be useful for other people interested in getting started with Lean in the context of topology. In fact, a game with this idea already existsSee: https://mmasdeu.github.io/topologygame/, but it uses the Lean 3 version, so it would be interesting to update it.

  Moreover, this kind of game is developed directly in Lean using an already available baseSee: https://github.com/leanprover-community/lean4game/blob/main/doc/create_game.md., which also offers the opportunity to explore Lean as a functional programming language, beyond its use as a proof verifier.

• Lean as a program verifier

  Finally, it is worth mentioning that I have been admitted to the Master's in Formal Methods in Computer Science (UCM with UPM). This will allow me to continue exploring Lean and other verifiers from a new perspective: the use of these tools in the verification of programs and formal specifications. I believe this training will naturally complement the work done in this project, since it will allow me to go deeper into another relevant and current facet of verification systems.