Zulip Chat Archive

Stream: new members

Topic: github access


view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Apr 14 2021 at 10:42):

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

view this post on Zulip Markus Himmel (Apr 14 2021 at 10:43):

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

view this post on Zulip Carlos Caralps (Apr 14 2021 at 10:45):

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

view this post on Zulip Carlos Caralps (Apr 14 2021 at 10:47):

Thanks!

view this post on Zulip 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/

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 14 2021 at 11:06):

Thanks for the link!

view this post on Zulip 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