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.
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
Carlos Caralps (Apr 14 2021 at 10:47):
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.
Kevin Buzzard (Apr 14 2021 at 11:06):
Thanks for the link!
Patrick Massot (Apr 14 2021 at 13:56):
I can believe there are missing lemmas about the zoo of separation conditions in mathlib. However I'm a bit worried that the proof you will have won't blend nicely with mathlib if you didn't use filters all over the place.
Last updated: May 08 2021 at 04:14 UTC