github access: Erdős–Szekeres

Stream: new members

[Pontus Sundqvist]

I recently formalized a proof of the Erdős–Szekeres theorem in Lean. To make a PR for mathlib (starting with the parts that expand other APIs), could I get write access to non-main branches on mathlib? My username is Pazzaz

[Thomas Browning]

@maintainers

[Bryan Gin-ge Chen]

If I'm not mistaken, @Bhavik Mehta already contributed a version of this to mathlib: https://github.com/leanprover-community/mathlib/blob/master/archive/100-theorems-list/73_ascending_descending_sequences.lean

Nevertheless, invite sent! https://github.com/leanprover-community/mathlib/invitations

[Bryan Gin-ge Chen]

I do think the entry on our 100 theorems page should mention "Erdős–Szekeres" somewhere.

[Pontus Sundqvist]

Oh, I didn't see that proof. It sure is a lot shorter than mine :sweat_smile:.

[Benjamin Davidson]

@Bryan Gin-ge Chen Would you like me to update the list to make mention of Erdős–Szekeres?

[Benjamin Davidson]

Also, it looks like Pontus still needs access

[Bryan Gin-ge Chen]

Benjamin Davidson said:

Bryan Gin-ge Chen Would you like me to update the list to make mention of Erdős–Szekeres?

That'd be great, thanks!

When I try to invite Pazzaz again, it says "Already has access to this repository".

[Bryan Gin-ge Chen]

And I checked that they have "write" access just now too.

[Benjamin Davidson]

Bryan Gin-ge Chen said:

Nevertheless, invite sent! https://github.com/leanprover-community/mathlib/invitations

I'm just realizing now that I totally missed this part of the message! My bad...I thought no one had sent an invite. Sorry!