New mathlib4 porting PRs by new people

Stream: mathlib4

[Jeremy Tan]

A sizeable number of people have opened porting PRs for mathlib4. They are totally new in the sense of having no other GitHub contributions other than their respective PRs:
!4#3386
!4#3384
!4#3382
!4#3385
I haven't seen anyone grant write permissions to these new people. Where did they all come from?

[Kevin Buzzard]

Where did you come from? :-)

[Jeremy Tan]

Singapore

[Kevin Buzzard]

At least one of the people on your list I know, by the way, and I can vouch that they know a fair bit about writing lean 3 code, although they have not posted much if at all on the Zulip.

[Kevin Buzzard]

My point is that you also appeared out of the blue, only a few weeks ago, and there have been other porting people before you with this property too.

[Eric Wieser]

I think @Jeremy Tan's confusion might be that (apparently) the request for github access happened privately rather than in a public channel; I don't think we have any official policy on that.

[Matthew Ballard]

Almost all remaining files have < 500 dependencies. Things are getting flatter and more hands is great!

[MonadMaverick]

I'm also new (first time heard about lean 2 wks ago)
!4#3351
!4#3170
!4#3324
!4#3325
!4#3349
I need help on this OuterMeasure PR :upside_down:

[Patrick Massot]

@Jeremy Tan I don't understand the point of your message, especially coming from you, as Kevin pointed out. Do you fear someone hacked a maintainer account to offer people the possibility to contribute?

[Patrick Massot]

Anyway, for curious people, we did have an initiation to mathlib porting in Orsay this morning and all those new people were there. There either students or researchers in the Paris/Orsay area.

[Patrick Massot]

And those people are very welcome to help with the port, especially since they easily have access to expert help.

[Jeremy Tan]

Patrick Massot said:

Jeremy Tan I don't understand the point of your message, especially coming from you, as Kevin pointed out. Do you fear someone hacked a maintainer account to offer people the possibility to contribute?

Yes, I feared unauthorised write access had happened

[James Gallicchio]

MonadMaverick said:

I'm also new (first time heard about lean 2 wks ago)

impressive to already be contributing to the port! :D