github permission_XMUM LEAN group

Stream: mathlib4

[math.xmum]

Hi,

Here‘s  XMUM LEAN Group.

We are currently seeking the permission to create a new branch where we can contribute our formalized codes to Mathlib. You may see the introduction message in the link attatched below! :grinning_face_with_smiling_eyes:

github uername: math-xmum

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Xiamen.20University.20Malaysia.20LEAN.20Group.3A.20Seeking.20to.20Contribute/near/433830965

[Eric Wieser]

It's a little strange to have a single github account for everyone in your group; so much so that it is against the github TOS:

Your login may only be used by one person — i.e., a single login may not be shared by multiple people.

[Eric Wieser]

Usually the way you would handle this is:

• Have everyone in your group create a personal account
• Create math-xmum as a github organization, and add all your members too it.

[Kim Morrison]

And in particular, we will not give out write access to such a group account. Please make individual accounts and ask again for those.

[Ma, Jia-Jun]

(deleted)

[Ma, Jia-Jun]

Kim Morrison said:

And in particular, we will not give out write access to such a group account. Please make individual accounts and ask again for those.

Hi Kim, can you grant me write access to the Mathlib? My Github account is "jiajunma," and I am supervising the team at Xiamen University Malaysia, working on the basics of game theory. Moreover, I also collaborate with the team at the National University of Singapore, working on the Coxeter group and Hecke algebra. I have accumulated a certain number of codes and wish to push them into the Mathlib. Thanks.

[Kim Morrison]

@Ma, Jia-Jun, I've sent the invite. As above, if there are others in the group who would like to make PRs, please have them ask for write access separately.

[Hennessy]

My Github ID is Hennessyyyyy

[Shaojun Zhang]

Kim Morrison said:

Ma, Jia-Jun, I've sent the invite. As above, if there are others in the group who would like to make PRs, please have them ask for write access separately.

Hello, Kim, I am writing def and some lemmas about Hecke algebra by lean, and I would like to make PRs. My github ID is zzsj2001.

[Kim Morrison]

Hennessy said:

My Github ID is Hennessyyyyy

Hi Hennessy, could you say what you are planning on working on?

[Kevin Buzzard]

@Shaojun Zhang what kind of Hecke algebras? (there is more than one, in some sense; do you mean the modular forms ones or other ones?)

[Shaojun Zhang]

The Hecke algebra of Coxeter group

[Haocheng Wang]

@Kim Morrison Hi Kim. I am Wang Haocheng and I have finished the formalization of

- Auction Theory: Including formalized proofs on no-dominant strategies in first-price auctions, the DSIC (Dominant Strategy Incentive Compatible) mechanisms, and non-negative utility in second-price auctions.
- Myerson's Lemma: Optimal auctions addressing a wide range of auction design problems for sellers.

We are planning to set a new branch maybe named Gametheory. And I may push my codes to it and named Gametheory.Auction,

Seeking the permission to contributing to Mathlib!
My github user id:hcWang942

[Kim Morrison]

No need to ping me specifically, any of the @maintainers can give permission (and I'm away from the computer for a bit, so hopefully someone else will take this!)

[Kim Morrison]

It might be a good idea to post on zulip your definitions (rather than the proofs), separately from making PRs, as these may need some discussion and iteration to get right.

[Riccardo Brasca]

Invitation sent!