## Stream: new members

### Topic: github access

#### Carlos Caralps (Apr 14 2021 at 10:41):

Hi there, I’m a math student. Last months I’ve been learning Lean being a participant of the Barcelona Lean Seminar. In this seminar we have focused our work in topological spaces with Lean and I’ve done some lemes about separation axioms.
I’d like to ask for permission to push to non-master branches of mathlib. I’d like to do my first PR with those lemmas.
carloscaralps
Thanks!

#### Kevin Buzzard (Apr 14 2021 at 10:42):

Your github userid is carloscaralps? Nice stuff! Is this being run by Marc?

#### Markus Himmel (Apr 14 2021 at 10:43):

I sent you an invite, it should appear at https://github.com/leanprover-community/mathlib/invitations

#### Carlos Caralps (Apr 14 2021 at 10:45):

Yes, my userid is carloscaralps and @Marc Masdeu is running the seminar

Thanks!

#### Kevin Buzzard (Apr 14 2021 at 10:51):

Great! I did some stuff with topological spaces with my students a couple of months ago: https://xenaproject.wordpress.com/2021/02/10/formalising-mathematics-workshop-4/

#### Marc Masdeu (Apr 14 2021 at 10:59):

Kevin, we are aware of your TCC workshops, the blog posts are extremely useful (at least to me). We did some basics (up to compacity and separation, you can see it at github.com/mmasdeu/barcelonaleanseminar), and one goal is to make the Topology Game. Right now, we decided to stop building topological spaces from scratch (we gave up when trying to prove that the Moebius band defined as a quotient of a square is homeomorphic to the strip as a subspace of R3), and move on to adapting all that we have to the Game.