This project is a formalization of the basic proofs about topology spaces created by the Barcelona LEAN Seminar (BLS), conducted by Dr Marc Masdeu (from UAB). This project was created in the first sessions of the BLS to learn how to formalize basic definitions and propositions with LEAN.

The GitHub repository can be found here.