github permission (stacks annotations)

Stream: mathlib4

[Nailin Guan]

Hello, I'd like to get write access to non-master branches of the mathlib4 repo for marking and adding the theorems in Stacks project. My github name is Thmoas-Guan .

[Kevin Buzzard]

Invitation sent!

[catmeow123456]

Hello, I'd like to get permission to write to non-master branches, trying to marking and adding the theorems in stacks project. My github name is catmeow123456 . thanks!

[Yiming Fu]

Hello, I would like to obtain a permission to non-master branches to add some theorems in Stacks project. My GitHub username is pelicanhere. Thanks!

[Patrick Massot]

Could you tell us a bit more about this sudden wave of people wanting to add things from the Stacks project? Are you working together?

[Yuyang Zhao]

Jiang Jiedong said:

Hi everyone,

Given that the Stacks Project is well organized and serves as a comprehensive, encyclopedic resource in commutative algebra and algebraic geometry, what do you think about organizing a group of motivated students to formalize certain sections in the Stacks Project?

There are 10-20 motivated students at Peking University, who already have some basic experience in formalizing exercises of abstract algebra. The teachers can teach them commutative algebra before they begin formalizing.

Since we are most interested in algebra, maybe beginning with "Chapter 9: Fields" is a good start and then we can try to progress towards "Chapter 10: Commutative Algebra". A (maybe stubborn) working method is to check one by one whether a theorem in the Stacks Project is already formalized in mathlib. If yes, we add the corresponding Stacks Project tag to the comments of the formal theorem (or its formal variant). If not, we try to formalize and add this theorem into Mathlib. If the theorem is too early to be formalized yet, we may leave it as a TODO.

I hold the belief that "every theorem in the stacks project should be formalized (possibly in a variant form) into Mathlib". Do you have any suggestions and comments on this project? Thank you!

The WIP PRs are #16105 and #16116.

[Suzuka Yu]

Greetings! I am working on making annotations in Stacks project (https://github.com/leanprover-community/mathlib4/tree/stacks_project_tag), hence I'd like to request for access to non-master branches. My GitHub account is Yu-Misaka. Thanks a lot! (btw, I am indeed working together with the Stacks team)

[Yi.Yuan]

Hello, I'd like to get write access to non-master branches of the mathlib4 repo for marking and adding the theorems in Stacks project. My github name is yuanyi-350

[Yongle Hu]

Hello, I'd like to get write access to non-master branches of the mathlib4 repo for marking and adding the theorems in Stacks project. My github name is mbkybky. Thanks a lot!

[Albert.J]

Hello, I'd like to get write access to non-master branches of the mathlib4 repo for marking and adding the theorems in Stacks project. My github name is AlbertJ-314. Thanks a lot!

[Sihan Su]

Hello, I'd like to get write access to non-master branches of the mathlib4 repo for marking and adding the theorems in Stacks project. My github name is su00000 . Thanks!

[张守信(Shouxin Zhang)]

Hello, I would like to obtain a permission to non-master branches to add some theorems in Stacks project. My GitHub username is ShouxinZhang. Thanks!

[Xuchun Li]

Hello, I would like to obtain a permission to non-master branches to add some theorems in Stacks project. My GitHub username is Xuchun-Li. Thanks!

[Yanpeng Dong]

Hello, I'd like to get write access to non-master branches of the mathlib4 repo for marking and adding the theorems in Stacks project. My github name is dyyynUU . Thanks!

[Hanliu Jiang]

nr

[Hanliu Jiang]

Hello, I'd like to get write access to non- branches of the mathlib4 repo for marking and adding the theorems in Stacks project. My github name is . SEU-Prime Thanks a lot!

[Shossone]

Hello, I'd like to get write access to non-master branches of the mathlib4 repo for marking and adding the theorems in Stacks project. My github name is Shossone. Thanks a lot!

[Sihan Wu]

Hello, I'd like to get write access to non-master branches of the mathlib4 repo for marking and adding the theorems in Stacks project. My github name is Old-Turtledove. Thanks a lot!

[syur2]

Hello, I'd like to get write access to non-master branches of the mathlib4 repo for marking and adding the theorems in Stacks project. My github name is syur2. Thanks a lot!

[LW_1104]

Hello, I'd like to get write access to non-master branches of the mathlib4 repo for marking and adding the theorems in Stacks project. My github name is LW_1104. Thanks!

[Notification Bot]

20 messages were moved here from #mathlib4 > github permission by Eric Wieser.

[Kim Morrison]

@Thomas-Guan, @catmeow123456, @pel, @Yuyang Zhao, @Suzuka Yu, @yuanyi-350, @Yongle Hu , @Albert.J, @su00000, @张守信(Shouxin Zhang), @Xuchun Li, @Yanpeng Dong, @prime, @Shossone, @Sihan Wu, @syur2, @LW_1104

Dear all, please be patient with us as we catch up with this influx of enthusiasm!

Could I ask all of you to please:

• Add your github username to your zulip account (this request goes to everyone on zulip, in fact ...) by visiting https://leanprover.zulipchat.com/#settings/profile
• Note that we do prefer (but not insist) that users requesting write access use their usual full name as their Zulip account name.
• To make sure you've read the existing (ancient) thread about the stacks tag at #general > stacks tags .
• We're going to need to implement some infrastructure in order to usefully record lots of stacks tags. I propose that we have a discussion over at the above linked thread to sort that out!
• We may request that you all coordinate on a fork, and then when you're ready to make a PR push the relevant branch to the main repo and make a PR from it. If the PR is solely adding stacks tags, we don't mind it being a large PR (usually we like small PRs).

[Yuyang Zhao]

cc @Jiang Jiedong

[Jiang Jiedong]

We are happy to submit a single tag PR to mathlib. Maybe we can work on a fork first before the infrastructure is finished, just adding the tag to the end of the comments. After the infrastructure is completed, we modify the tags using the infrastructure.

[Kim Morrison]

That sounds great!

[Kim Morrison]

Hopefully someone can get the attribute implemented for you asap.

[Hanliu Jiang]

Hello, I'd like to get write access to non- branches of the mathlib4 repo for marking and adding the theorems in Stacks project. My github name is  SEU-Prime Thanks a lot!