Formalising Mathematics with Lean

 Formalising Mathematics with Lean. A Case Study: Results in General Topology.🔗

Pepa Montero Jimena

Supervised by Jorge Carmona Ruber

Bachelor's Thesis (Trabajo de Fin de Grado) — Academic year 2024/2025.

Faculty of Mathematical Sciences, Degree in Mathematics, Department of Computer Systems and Computing, Universidad Complutense de Madrid.

Contents

  1. Abstract
  2. 1. Introduction
  3. 2. Lean Theorem Prover
  4. 3. Topological Spaces in Lean
  5. 4. Urysohn's Lemma
  6. 5. Conclusion
  7. References