github permission

Stream: mathlib4

[Jon Eugster]

Could I get the permissions to push to non-master branches for the mathlib4 repo, please? I'd be keen to start contributing to the port :)

[Yuyang Zhao]

I made PR #17477 but algebra/ne_zero is ported to mathlib4. Could I get write access to mathlib4? My github username is negiizhao.

[David Wärn]

Could I get permission to push? I'm dwarn on github

[Joël Riou]

May joelriou get push access on non-master branches of mathlib4?

[Scott Morrison]

Invite sent

[Matthew Ballard]

Could I get push access to non-master branches of mathlib4 and mathlib : mattrobball? :pray:

[Johan Commelin]

https://github.com/leanprover-community/mathlib/invitations

[Johan Commelin]

https://github.com/leanprover-community/mathlib4/invitations

[Matthew Ballard]

Thanks!

[Johan Commelin]

Voila

[Eric Rodriguez]

I'd also appreciate push access to mathlib4 :)

[Johan Commelin]

You already have it.

[Antoine Labelle]

Hi! I would like to start trying to contribute to the port. Could I get permission to push? My github username is antoinelab01.

[Alex Keizer]

I'm also here to ask for permission, I want to help with this PR: my username is alexkeizer

[Floris van Doorn]

I invited both of you! https://github.com/leanprover-community/mathlib4/invitations

[Thomas Murrills]

I'd also like permission for editing the port status page on mathlib, please! :) (I think I already have permission for mathlib4.) I'm @thorimur on github.

[Floris van Doorn]

Oh, porting wiki is part of mathlib4 and port status is part of mathlib? Hmm...
I invited you to mathlib: https://github.com/leanprover-community/mathlib/invitations
I think and hope that enables you to edit the port status page.

[Thomas Murrills]

Thanks! :)

[Alex Keizer]

Could someone drop me an invite for mathlib as well (having the same issue as Thomas). Again, I'm alexkeizer on github

[Johan Commelin]

@Alex Keizer https://github.com/leanprover-community/mathlib/invitations

[Anand Rao]

I would also like to start contributing to the port. My username is 0art0 - could I get push access to the non-master branches of mathlib4? Thanks.

[Johan Commelin]

@Anand Rao Voila: https://github.com/leanprover-community/mathlib4/invitations

[Shreyas Srinivas]

Hi, I would like to port data.nat.bits. My github username is Shreyas4991. May I get permission for pushing to non master branches of mathlib 4 and edit permission for the port status file in the wiki of mathlib please?

[Ruben Van de Velde]

@maintainers

[Johan Commelin]

@Shreyas Srinivas Voila: https://github.com/leanprover-community/mathlib4/invitations

[Shreyas Srinivas]

Johan Commelin said:

Shreyas Srinivas Voila: https://github.com/leanprover-community/mathlib4/invitations

Hi @Johan Commelin ,
I am not able to update https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status

[Johan Commelin]

Hmm, weird. You have the exact same permissions as other contributors...

[Siddhartha Gadgil]

Shreyas Srinivas said:

Johan Commelin said:

Shreyas Srinivas Voila: https://github.com/leanprover-community/mathlib4/invitations

Hi Johan Commelin ,
I am not able to update https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status

That wiki is on mathlib i.e., mathlib3 so needs permissions there.

[Johan Commelin]

Aaah, good point!

[Johan Commelin]

@Shreyas Srinivas Voila: https://github.com/leanprover-community/mathlib/invitations

[Shreyas Srinivas]

Johan Commelin said:

Shreyas Srinivas Voila: https://github.com/leanprover-community/mathlib/invitations

Got it. It works. thanks. updated the file

[Ruben Van de Velde]

Siddhartha Gadgil said:

Shreyas Srinivas said:

Johan Commelin said:

Shreyas Srinivas Voila: https://github.com/leanprover-community/mathlib4/invitations

Hi Johan Commelin ,
I am not able to update https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status

That wiki is on mathlib i.e., mathlib3 so needs permissions there.

Should we move it?

[Scott Morrison]

We are hoping to remove the need for it entirely, soon.

[Lukas Miaskiwskyi]

Hi, I would also like to request the usual github permissions for mathlib4, my github name is LukasMias

[Riccardo Brasca]

Invitation sent!

[Henrik Böving]

I would also like to request permissions for mathlib4. I'm hargoniX

Also I already made a fork of mathlib4 myself and ported + PRed a file from there because the wiki porting guide does not mention this (for GitHub) abnormal workflow so I forgot about it, could we maybe add a note there?

[Johan Commelin]

@Henrik Böving https://github.com/leanprover-community/mathlib4/invitations

[Pol'tta / Miyahara Kō]

I would like to contribute to the port. Could I get permission to access non-master branches?
My user name is Komyyy.

[Johan Commelin]

@Pol'tta / Kô Miyahara voila: https://github.com/leanprover-community/mathlib4/invitations

[Utku Okur]

Can I have permission to port
https://leanprover-community.github.io/mathlib-port-status/file/combinatorics/simple_graph/regularity/energy

My username is mrutkuokur

[Floris van Doorn]

invite sent

[Bulhwi Cha]

Can I get permission to push to non-master branches of Mathlib4? My GitHub username is chabulhwi.

[Kevin Buzzard]

@maintainers

[Johan Commelin]

@Bulhwi Cha Voila: https://github.com/leanprover-community/mathlib4/invitations

[MonadMaverick]

Could I have the permission?

I'm going to focus on measure_theory.

My github username is MonadMaverick.

Thank you in advance.

[Scott Morrison]

Invite sent!

[Timothy Gu]

Hello! Could I get added to the GitHub organization? I've made a PR here for an Infinite deriving handler, but was told that CI doesn't run on repo forks. My GitHub username is TimothyGu.

[Eric Rodriguez]

@maintainers

[Anne Baanen]

Invite sent for mathlib4: https://github.com/leanprover-community/mathlib4/invitations

[Anne Baanen]

And mathlib3: https://github.com/leanprover-community/mathlib/invitations

[Jujian Zhang]

@maintainers , can I kindly ask for permission to create PRs for mathlib4 please, my github name is jjaassoonn

[Anne Baanen]

Invite sent!

[Jujian Zhang]

Thanks!

[Yuma Mizuno]

@maintainers I would like to contribute to porting to mathlib4. Could I get a permission to access github to make RPs? My github name is yuma-mizuno.

[Scott Morrison]

@Yuma Mizuno , invitation sent! I'm excited to have some help porting the higher categorical material, if you're interested in that. :-)

[Apurva Nakade]

@maintainers can I please get permission to push to mathlib4 non-master branches? My Github username is apurvnakade
Thanks,

[Johan Commelin]

@Apurva Nakade Voila: https://github.com/leanprover-community/mathlib4/invitations

[Nikolas Kuhn]

Also asking for permission to contribute PRs for porting. Handle: nick-kuhn

[Kevin Buzzard]

@maintainers

[Scott Morrison]

@Nikolas Kuhn, invite sent.

[Kalle Kytölä]

@maintainers, could I have access to push to Mathlib4 branches? (handle: kkytola)

[Johan Commelin]

@Kalle Kytölä voila: https://github.com/leanprover-community/mathlib4/invitations

[Timo Carlin-Burns]

@maintainers requesting mathlib4 push access for timotree3

[Johan Commelin]

@Timo Carlin-Burns Voila: https://github.com/leanprover-community/mathlib4/invitations

[François G. Dorais]

@maintainers requesting mathlib4 push access for fgdorais.

[Scott Morrison]

@François G. Dorais, invite sent.

[Bernhard Reinke]

@maintainers I am porting my PR !3#18300 to mathlib4. Can I get mathlib4 push access for b-reinke? Thanks!

[Anne Baanen]

Done! https://github.com/leanprover-community/mathlib4/invitations

[Aaron Bies]

Hello, could someone give me permission to contribute to mathlib4? My handle is slerpyyy (link). I have already contributed to mathlib3 in the past.

[Ruben Van de Velde]

Aaron Bies said:

Hello, could someone give me permission to contribute to mathlib4? My handle is slerpyyy (link). I have already contributed to mathlib3 in the past.

@maintainers

[Aaron Bies]

(Also is there a better place for these requests? The guide just says to "ask in zulip")

[Riccardo Brasca]

Invitation sent!

[Kevin Buzzard]

I guess we could have a special thread (there are currently several) where you can ask, but right now the system works anyway.

[Notification Bot]

This topic was moved here from #general > mathlib4 github permission request by Kyle Miller.

[Kevin Buzzard]

If this is the stream where we want people to ask, we could say this in the guide

[Alex J. Best]

I updated the instructions here : https://github.com/leanprover-community/leanprover-community.github.io/pull/337

[Julian Berman]

@maintainers can I ask for mathlib4 branch permissions -- @Julian

[Johan Commelin]

@Julian Berman voila: https://github.com/leanprover-community/mathlib4/invitations

[FMLJohn]

@maintainers I would like to contribute to porting to mathlib4. Could I get a permission to access github to make RPs? My github name is FMLJohn.

[Scott Morrison]

Hi @FMLJohn, could you quickly tell us something about your background, and the sort of material you would like to contribute? Thanks!

[FMLJohn]

Hi! My full name is Fangming Li. I am a PhD student supervised by Professor Kevin Buzzard at Imperial College London. I am going to formalize something in algebra and algebraic geometry, such as Bezout's Theorem and Riemann-Roch Theorem.

[Scott Morrison]

@FMLJohn, please see https://github.com/leanprover-community/mathlib4/invitations!

[FMLJohn]

Thank you very much!

[Jonas van der Schaaf]

@maintainers My name is Jonas, currently a masters student at the University of Amsterdam. My main interests are in algebraic geometry and model theory. I recently attended the Lean workshop in Leiden and would like permission to access the git repository to make contributions to mathlib in these domains. My github username is jonasvanderschaaf.

[Kevin Buzzard]

Jonas made some definitions in algebraic geometry in Leiden as part of his project. It would be great to see some of this stuff make it into mathlib!

[Floris van Doorn]

Invite sent

[Jonas van der Schaaf]

Thank you!

[Ashvni Narayanan]

Hello, could I please get permission for PRing to mathlib4? My github username is laughinggas . Thank you!

[Anne Baanen]

Invite sent: https://github.com/leanprover-community/mathlib4/invitations!

[Ashvni Narayanan]

Thank you!

[Kaiyu Yang]

Hi, I'd like to fix some troubles caused by inconsistent uses of \r\n and \n. I'll also modify the linter to detect \r\n (see this PR). May I have access to non-master branches? My GitHub username is yangky11. Thanks!

[Eric Wieser]

Invite sent!

[Eric Wieser]

(You'll need to close the PR and re-open it from a branch)

[Isaac Hernando]

Hi, could I please have push access to mathlib4? I am working on a project (PR #6504) with @Adam Topaz. My github username is IsaacHernando. Thank you!

[Scott Morrison]

@Isaac Hernando, invitation sent: https://github.com/leanprover-community/mathlib4/invitations

[Coleton Kotch]

Hello, could I also have push access for PR #6504 with @Adam Topaz, github username is colejagdtiger? Thank you.

[Jireh Loreaux]

@Coleton Kotch invitation sent: https://github.com/leanprover-community/mathlib4/invitations

[Koundinya Vajjha]

Hello, could I have push access to the non-master branches on mathlib4? My github is kodyvajjha. Thanks!

[Scott Morrison]

@Koundinya Vajjha, please see https://github.com/leanprover-community/mathlib4/invitations

[Scott Carnahan]

May I have push access to non-master branches of mathlib4? My github username is ScottCarnahan.

[Patrick Massot]

Could you tell us a bit about what you hope to contribute?

[Johan Commelin]

I guess https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Scott.20Carnahan/near/372985652

[Johan Commelin]

@Scott Carnahan Voila: https://github.com/leanprover-community/mathlib4/invitations

[Scott Carnahan]

For the moment, I have some basic results on binomial rings and binomial coefficients that will be necessary for later work in vertex algebras.

[Vincent Beffara]

Hello, could I have push access to the non-master branches on mathlib4? My github is vbeffara

[Patrick Massot]

Done

[Wen Yang]

Hello, could I have push access to the non-master branches on mathlib4? My github username is shuxuezhuyi. I have just formalized a proof of the theorem which states that every continuous and injective function f : [a, b] → ℝ is strictly monotone. See here for the discussion.

[Ziyu Wang]

Hello, could I have push access to the non-master branches on mathlib4? My github username is TropicalFatFish. I have formalized the definition and some properties about Stronly Convex Function.

[Yaël Dillies]

Please ping me when the PR is open :)

[Anatole Dedecker]

Invitations sent to both of you

[Chenyi Li]

Hello, could I have push access to the non-master branches on mathlib4? My github username is chenyili0818. I have formalized the definition of a closed function and I am working on convex analysis. Thank you very much !

[Jiang Jiedong]

Hello, could I have push access to the non-master branches on mathlib4? My github username is jjdishere. I have formalized the some theorems about ramification theory in number theory. Thank you!

[Johan Commelin]

@Jiang Jiedong Voila: https://github.com/leanprover-community/mathlib4/invitations

[Patrick Massot]

Chenyi Li said:

Hello, could I have push access to the non-master branches on mathlib4? My github username is chenyili0818. I have formalized the definition of a closed function and I am working on convex analysis. Thank you very much !

What do you mean by "closed function"? Is that simply docs#IsClosedMap?

[Chenyi Li]

In convex analysis we describe a closed function as https://en.wikipedia.org/wiki/Closed_convex_function. It has a close connection with closed map, but the closed function is more related to convex optimization and convex analysis from my perspective

[Patrick Massot]

Wow, this is a really confusing terminology. We'll need to find a better name for use in Mathlib.

[Kevin Buzzard]

Just to confirm: did Chenyi get push access? Reading the messages I wonder if everyone other then them did...

[Anatole Dedecker]

Apparently not, I just did that.

[Apurva Nakade]

Hello, could I have push access to the non-master branches on mathlib4? My github username is apurvanakade.
(I already have access through apurvnakade but I have some issues with using this handle from different machines.)
Thank you,

[Anatole Dedecker]

Done, but it's not ideal. What kind of issue do you have?

[Apurva Nakade]

Thank you. My Mac refuses to let me change my username.

[Apurva Nakade]

I have been trying for a really long time trying to reset the osxkeychain or whatever but it just keeps reverting

[Anatole Dedecker]

Your GitHub username right? But yeah I understand this problem, my rule of thumb on a Mac is to never ever use the system keychain...

[Apurva Nakade]

I don't even know when I accepted this keychain option tbh. Just suddenly I'm stuck with this with no way to switch.

[Yufei Liu]

Hello, could I have push access to the non-master branches on mathlib4? My github username is 'liuyf0188', I was trying to add general matrix determinant lemma proof to SchurComplement.lean

[Anatole Dedecker]

Invitation sent!

[Michael Rothgang]

Hello! I'm working on formalising Sard's theorem (mentored by Floris van Doorn at LftCM 23) and would like to PR the parts I've completed. Could I have write access to non-master branches on mathlib4? My github username is grunweg.

[Anatole Dedecker]

That's very cool! Invitation sent!

[Richard Hill]

Hello, could I have permission to push to mathlib4? I have been working on differentiation and composition of formal power series. My github user name is rmhi.

[Anatole Dedecker]

Invitation sent!

[Sean Gonzales]

Hello, could I have permission to push to mathlib4? I'm working on the correspondence between normal field extensions and normal subgroups of the galois group. My username is ChimiSeanGa

[Scott Morrison]

@Sean Gonzales, please check https://github.com/leanprover-community/mathlib4/invitations!

[Chris Wong]

Hello, may I have permission to push to mathlib4?
I was around briefly for mathlib3 (added palindromes) and I'd like to contribute again :)
I've been investigating the TODOs around regular expressions and planar graphs.
My username is lambda-fairy
Thanks!

[Bolton Bailey]

@maintainers

[Patrick Massot]

Done

[Patrick Massot]

Chris, if you are interested in regular expressions , could you consider contributing to std some actual code instead of abstract theorems? Having functions to search and replace using regular expressions would make Lean look a lot more like an actual programming language.

[Alex J. Best]

I think the best way to get that quickly is to wrap some existing c regex library using alloy. I started this at some point but got distracted... I can link to my minimal progress later if desired.

[Patrick Massot]

Yes, wrapping an existing library would be fair game.

[Chris Wong]

Is C a hard requirement? I would prefer either RE2 or Rust's regex, as they're resistant to denial-of-service attacks.

[Arthur Paulino]

It's possible to wrap Rust code, but that would require everyone else building Std to have cargo installed.

Here's a way to wrap Rust code in case you need it anyway: https://github.com/lurk-lab/RustFFI.lean

[Jordan Brown]

Hello, could I have permission to push to mathlib4? Working on covering spaces; my username is jlcbrown

[Johan Commelin]

@Jordan Brown Welcome: https://github.com/leanprover-community/mathlib4/invitations

[Matthias U]

Hi, may I have push access to mathlib4? My github username is matthias567

[Johan Commelin]

Could you please provide some background information? What do you plan to contribute?

[Matthias U]

@Johan Commelin Sure, I plan to formalise amenability of group actions, thus leading to an implementation of amenability of groups. So far, I wrote a straightforward definition of what an amenable action of a monoid is.

[Johan Commelin]

@Matthias U Thanks, voila: https://github.com/leanprover-community/mathlib4/invitations

[Iván Renison]

Hello, can I have permission to push to mathlib4? Mi github username is IvanRenison
I want to formalize Dirac's theorem of graph theory (discussion)

[Robin Carlier]

Hi, can I have permission to push to mathlib4? I’m currently a math PhD student and I would like to add some facts on modules like a better API for flatness (I have a branch proving free modules are flats, as well as direct sums of flat, ultimately I’d like to add the characterization in 00HD of the stacks project) as well as stuff on finitely presented and coherent modules. My github username is robin-carlier.

[Johan Commelin]

@Iván Renison @Robin Carlier Voila: https://github.com/leanprover-community/mathlib4/invitations

[Robin Carlier]

Great, thanks!

[Andrew Yang]

Welcome! Jujian Zhang also have a project on flatness and I believe it has 00HD covered, but I'm not sure whether he plans to merge it into mathlib, and more API is always welcomed regardless.

[Robin Carlier]

Oh, I wasn’t aware of this project. I’m not anywhere near a formalization of 00HD yet anyway, as I believe it would be more natural to add some stuff on finitely presented modules first, so I guess I still have some stuff to do anyway. Should I submit my proof that free modules are flat as a small PR despite this project?

[Johan Commelin]

I don't think you should feel discouraged from PRing your own stuff because of this project. So yes, such a PR would certainly be welcome.

[Kevin Buzzard]

@Jujian Zhang are you PRing your work to mathlib? What's the status?

[Jujian Zhang]

00HD is complete here : https://github.com/leanprover-community/mathlib4/pull/7225

[Jujian Zhang]

I am trying to figure out the correct generality of the tensor hom adjunctiom, i.e, should I generalizeTensorProduct.AlgebraTensorModule where there are some assumptions on algebra instances

[Kevin Buzzard]

docs#TensorProduct.AlgebraTensorModule

[Jujian Zhang]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/TensorProduct/Tower.html#TensorProduct.AlgebraTensorModule.curry

[Julian Külshammer]

Would it be too hard to set this up already in a way that makes generalisation to non-commutative rings possible? I.e. by using an R^{op}-action on X?

[Jujian Zhang]

I assumed both rings are commutative, but upon inspection only TensorPrdocut.leftModule assumes commutativity. I think I should be able to assume only one of the rings being commutative.

[Daniel Lambert]

Hello, could I have push access to the non-master branches on mathlib4? My github username is Blackfeather007. I am working on convex analysis. Thank you very much !

[Kevin Buzzard]

@maintainers

[Floris van Doorn]

invite sent!

[Gareth Ma]

Hello, can I also have push/branch access on mathlib4? My github username is [deleted] :D. I am working on number theory and some combinatorics. Thank you very much!

[Floris van Doorn]

invite sent!

[Gareth Ma]

Thanks!

[Daniel Lambert]

Thanks!

[Utensil Song]

Hi, may I have branch access on mathlib4? My GitHub username is utensil. I'm still working on things related to Clifford Algebra. Thank you very much!

[Johan Commelin]

@Utensil Song Voila: https://github.com/leanprover-community/mathlib4/invitations

[Utensil Song]

Thanks!

[Eric Wieser]

Julian Külshammer said:

Would it be too hard to set this up already in a way that makes generalisation to non-commutative rings possible? I.e. by using an R^{op}-action on X?

I think this would be a mistake to go too far down this road without first doing #7152

[Thomas Zhu]

Hi, can I have access to non-master branches of mathlib? I would like to contribute to basic results in probability theory and information theory. I have proven that 2 random variables are independent iff their densities multiply to the joint density (https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/independent.20iff.20joint.20density.20is.20product), and I am proving some basic properties of entropy. My github username is hanwenzhu

[Bolton Bailey]

@maintainers

[Oliver Nash]

Invite sent

[Thomas Zhu]

Thank you!

[Miguel Marco]

Hi @maintainers, can I have access to non-master branches of mathlib?

I have written some basic tactics that were helpful in my courses. I think they might be helpful to other people too.

[Miguel Marco]

My github username is miguelmarco

[Rob Lewis]

Miguel Marco said:

My github username is miguelmarco

Invite sent!

[Claus Clausen]

Hey @maintainers , I am currently working on some basic distributions, that might be ready for a first pr soon. Can you give me a non-master access?
My github username is ClausenCl

[Patrick Massot]

Done

[Timo Carlin-Burns]

Why is https://github.com/leanprover-community/mathlib4 giving me 404 as though the repo is private? It's happening on and off for the last few minutes

[Patrick Massot]

GitHub seems to be struggling a lot currently.

[Patrick Massot]

It has nothing specific to Mathlib.

[Anatole Dedecker]

@Claus Clausen Do you mean distributions in the sense of probability or in the sense of distribution theory?

[Patrick Massot]

Probability

[Jannis Limperg]

Could @Xavier Généreux get access to the Aesop repo? We're collaborating on better forward reasoning.

[Johan Commelin]

@Xavier Généreux Voila: https://github.com/leanprover-community/aesop/invitations

[Jannis Limperg]

Thanks!

[Scott Morrison]

@Jannis Limperg, I also sent you an invite with admin rights to the repo. Sorry, you should of course have had that as soon as it was transferred!!

[Jannis Limperg]

Ah great, thank you very much!

[Xavier Généreux]

Johan Commelin said:

Xavier Généreux Voila: https://github.com/leanprover-community/aesop/invitations

Thanks!

[Xavier Xarles]

I would like t contribute to mathlib4. My username is XavierXarles. Thanks!

[Ruben Van de Velde]

Xavier Xarles said:

I would like t contribute to mathlib4. My username is XavierXarles. Thanks!

Anything in particular you're working on?

[Xavier Xarles]

Ruben Van de Velde said:

Xavier Xarles said:

I would like t contribute to mathlib4. My username is XavierXarles. Thanks!

Anything in particular you're working on?

I am working on Semirings (results done for rings that also work for semirings).

Right now I have a small change in the Mathlib.RingTheory.Ideal.Operations to propose.

[Riccardo Brasca]

Invitation sent!

[Riccardo Brasca]

And feel free to submit even very small PR, we usually like them very much!

[Xavier Xarles]

Riccardo Brasca said:

And feel free to submit even very small PR, we usually like them very much!

Done. There is a weird error in the commit (PR #8469).

[Jeremy Toh]

Hi, I tried doing the TODO in Mathlib.Analysis.PSeries, namely to generalise the arguments to Schlömilch's generalization of the Cauchy condensation test. I would like have the permission to open a PR for code review. My username is deepimpactmir. Thanks!

[Patrick Massot]

GitHub claims there is no such username.

[Jeremy Toh]

ah it's deepimpactmir oops for typo

[Patrick Massot]

This time it worked!

[Jeremy Toh]

thank you!

[Adrian Wüthrich]

Hello, I am currently working on the graph Laplacian. I have already proven some of its properties and would like to get non-master access. My username is awueth.

[Scott Morrison]

@Adrian Wüthrich: https://github.com/leanprover-community/mathlib4/invitations

[Adrian Wüthrich]

Thanks!

[Hunter Monroe]

Please provide github user hmonroe access to non-master branches of mathlib4.

[Scott Morrison]

@Hunter Monroe https://github.com/leanprover-community/mathlib4/invitations

[Ali Ramsey]

Hi, could I have permission to push to non-master branches? I'm working on formalising coalgebras and Hopf algebras. Right now I just wanted to make a PR for the definition of a coalgebra and an example. My GitHub username is al-ramsey.

[Scott Morrison]

@Ali Ramsey, I've just sent you an invitation at https://github.com/leanprover-community/mathlib4/invitations. Welcome to Mathlib!

[Ali Ramsey]

Thank you!

[Qi Ge]

Hello! I'm requesting github permission for handle GeQi. Thanks!

[Scott Morrison]

@Qi Ge, invitation sent!

[Dan Velleman]

Hi, can I get permission to make a PR to Mathlib? (See the discussion under "Pattern matching in set-builder notation" for what I'd like to add.)

[Dan Velleman]

I guess I should have said: my github username is djvelleman.

[Johan Commelin]

@Dan Velleman Welcome, voila: https://github.com/leanprover-community/mathlib4/invitations

[Dan Velleman]

Thank you!

[Ira Fesefeldt]

Heya, I have worked recently on ordinal approximants of least fixed points for the tarski knaster theorem and would like to contribute in this regard.
May I get permission for github? My github username is PhoenixIra

[Anne Baanen]

Invite sent! https://github.com/leanprover-community/mathlib4/invitations

[Anne Baanen]

@Ira Fesefeldt

[Fernando Chu]

Hello! I want to formalize sifted colimits and their commutativity w.r.t. finite products. I also want to try formalizing other basic results in category theory, algebra, or logic. My username is FernandoChu.

[Johan Commelin]

@Fernando Chu Welcome: https://github.com/leanprover-community/mathlib4/invitations

[Fernando Chu]

Thanks!

[Yongyi Chen]

Requesting github permission to add some missing group theory theorems. GIthub usernme is yongyi781

[Johan Commelin]

@Yongyi Chen Voila: https://github.com/leanprover-community/mathlib4/invitations

[Josha Dekker]

Hello, I'd like to request GitHub permission. My Github username is JADekker. I'm currently doing a PhD in Mathematical Finance and plan to (at some point) formalise some basic results from e.g. the theory of risk-measures, optimal stopping and possibly econometrics, or at least (if any) some of the more mathematical prerequisites for these. I just worked through MIL and will now try to dive into Mathlib and see where I can contribute!

[Yaël Dillies]

You should probably talk to @Jason KY.!

[Josha Dekker]

I would also like GitHub permission to PR the definition of Lindelöf sets & spaces. I'll try to add some basic results at a later stage as well, but feel free to add.

[Markus Himmel]

@Josha Dekker I sent you an invite: https://github.com/leanprover-community/mathlib4/invitations

[Chris Birkbeck]

Ok I'm ready to start PRing some more modular form things. Could I regain Github permission? my username is CBirkbeck. (I guess the mathlib3 doesn't carry over!)

[Johan Commelin]

@Chris Birkbeck https://github.com/leanprover-community/mathlib4/invitations

[Chris Birkbeck]

thank you!

[Andy Jiang]

Asking for permission. GitHub username: davikrehalt. Planning on initially contributing some theorems for working with lists/finsets. May continue other things in future.

[Kim Morrison]

@Andy Jiang could you be more specific / have a branch to point at?

[Andy Jiang]

Scott Morrison said:

Andy Jiang could you be more specific / have a branch to point at?

Um I don't have the code/branch/PR yet but I had some lemmas here ->

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Computing.20Finset.20sort.20of.20Finset.20range/near/410424794

which I thought would be good to have in Mathlib. If you want I can make a ready PR first and then ask for permission here? I just thought the convention was to ask for the permission here first, sorry if not.

[Kim Morrison]

No, that's great, you're doing the right thing. We're aspiring to consistently ask new authors about what they are proposing to contribute --- often we skip this step if the responding maintainer already knows the author somehow.

[Kim Morrison]

Those lemmas (at least the statements, I didn't look at the proofs) look good to have!

[Kim Morrison]

@Andy Jiang, invitation sent!

[Emilie (Shad Amethyst)]

Hello, I made my first contribution (https://github.com/leanprover-community/mathlib4/pull/9458), and I would like non-master write access so that I can assign myself the PR tags to let CI run on them.
I can and have run lake build locally, but I would like the piece of mind that I didn't accidentally screw up badly enough that my local setup somehow gives a false positive.

This contribution is the first one in a series to get my (currently ugly-looking but working) formalization of Rubin's Theorem (https://github.com/adri326/rubin-lean4/) into mathlib.

My github username, as hinted by the links above, is adri326

[Kevin Buzzard]

Once you have push access to non master branches you'll unfortunately need to close #9458 and open a new PR from a branch of the leanprover-community version of mathlib (we know this isn't the standard procedure for github, but at the end of the day it's the path of least resistance for the community).

[Emilie (Shad Amethyst)]

The CI is doomed to not run on PRs from forks?

[Kim Morrison]

@Emilie (Shad Amethyst), invitation sent.

[Raghuram]

I recently got push access to non-master branches to work on this.

However, although I was able to create a new branch on GitHub using a web browser, I can't seem to push to it from my local copy of the repository (I get a message "Permission to leanprover-community/mathlib4.git denied to raghuram-13." and a 403 error).

Is there something special I have to do (or does the personal access token need special permissions) to push with this kind of access?

[Ruben Van de Velde]

You may need to set up an SSH key if you don't have it today

[Raghuram]

So personal access tokens don't work?

[Raghuram]

OK, I've set up SSH and successfully pushed. Thanks Ruben Van de Velde!

[Gian Cordana Sanjaya]

Hello,

Can I ask for permission for write access? I want to first try on a small lemma over PNat, and I'm thinking of adding more results over PNat for now. Thank you very much.
GitHub username: mortarsanjaya

[Kim Morrison]

@Gian Cordana Sanjaya, invitation sent!

[Joseph Tooby-Smith]

Hi. Please can I have GitHub permissions? I initially want to add some constructors for horns in low dimension cases from faces, and more generically help in formalising algebraic topology and infinity-category theory. GitHub user name is: jstoobysmith. Many thanks

[Johan Commelin]

@Joseph Tooby-Smith Voila: https://github.com/leanprover-community/mathlib4/invitations

[Diana Kalinichenko]

Hi! Can I have GitHub permissions? I proved Fin.Tuple.Repeat.repeat_comp_rev and want to make a PR. My username is technosentience :smile:

[Kim Morrison]

@Diana Kalinichenko, I've sent the invite: https://github.com/leanprover-community/mathlib4/invitations

[Chris Ahn]

Hi, I'm planning to familiarise myself with the mathlib4 repository by tackling some of #7987, could I have write access? My github username is s1m7u.

[Floris van Doorn]

invite sent!

[Alena Gusakov]

Hi, can I have permission to contribute to mathlib4? I'm working on Gaussian coefficients and want to make a branch

[Ruben Van de Velde]

What's your github user name?

[Alena Gusakov]

Ruben Van de Velde said:

What's your github user name?

agusakov

[Johan Commelin]

@Alena Gusakov voila: https://github.com/leanprover-community/mathlib4/invitations

[Alena Gusakov]

@Johan Commelin Thank you!!

[Nir Paz]

Hi, can get the permissions? I want to contribute some set theory theorems about cardinals. My username is YnirPaz

[Kim Morrison]

@Nir Paz , please see https://github.com/leanprover-community/mathlib4/invitations

[Colin Jones ⚛️]

Hi can I get permission to add to Mathlib. I would like to formalize the definitions of weird, abundant, semiperfect, and deficient numbers and contribute to number theory. My github username is Colin166

[Johan Commelin]

@Colin Jones ⚛️ voila: https://github.com/leanprover-community/mathlib4/invitations

[Colin Jones ⚛️]

Thank you!

[Shaopeng]

Hello, may I please get the permissions to write to non-master branches of the mathlib? I would like to work on some of the good first issues for starters, and later contribute to the model theory or the category theory libs. My GitHub username is LibertasSpZ. Thank you very much!

[Johan Commelin]

@Shaopeng voila: https://github.com/leanprover-community/mathlib4/invitations

[Shaopeng]

Thanks a lot, @Johan Commelin .

[Edward van de Meent]

can i get permissions for writing to non-master branches? i'd like to push some of my work on defining metric spaces with a generic codomain

[Edward van de Meent]

my github username is blizzard_inc

[Johan Commelin]

@Edward van de Meent Voila: https://github.com/leanprover-community/mathlib4/invitations

[Oliver Butterley]

Hi! Could I have write access to non-master branches, please. Github: oliver-butterley. I would prepare a sInter version of an iInter theorem that is useful. As per discussion.

[Riccardo Brasca]

Invitation sent!

[Christian K]

Hi there,
I'm a student from germany and I am working on a project to formalize the Banach Tarski Paradox in Lean. During this project, we created some auxiliary theorems (Matrix.adjugate_fin_three). In my opinion, these would fit greatly in to the mathlib. So i want to ask for acces to the mathlib repo to make a pull request. (Github: https://github.com/Bergschaf/)

[Johan Commelin]

@Christian K voila: https://github.com/leanprover-community/mathlib4/invitations

[Alessandro Iraci]

Hi! Can I get write access to non-master branches? I would like to add symmetric functions to the library. My Github username is SashaIr. Thanks!

[Riccardo Brasca]

Invitation sent!

[Daniel Weber]

Hi, I've been working on a few theorems for docs#AddChar, could I please get write access to non-master branches? My Github username is Command-Master. Thanks!

[Michael Stoll]

It would make sense to merge #11049 before further changes are made to additive characters.

[Frédéric Marbach]

Hi! Could I please get write access to non-master branches? I would like to contribute to (free) Lie algebras. My GitHub username is frederic-marbach. Thanks!

[Johan Commelin]

@Frédéric Marbach voila: https://github.com/leanprover-community/mathlib4/invitations

Are you aware of the ongoing Lie theory project?

[Johan Commelin]

https://github.com/orgs/leanprover-community/projects/17?query=is%3Aopen+sort%3Aupdated-desc

[Frédéric Marbach]

Thank you! No, I was not aware of this project. At first sight, it looks rather independent from what I am planning to do. I will of course discuss everything here before doing anything serious. I am interested in: the Poincaré–Birkhoff–Witt theorem, Hall sets/bases of the free Lie algebra, the Guillemin–Sternberg realization theorem for transitive Lie algebras and its explicit Blattner–Draisma realization formula within the Lie algebra of formal vector fields.

[Panagiotis Angelinos]

Hello! Could I please get write access to non-master branches? My GitHub username is pangelinos. I've managed to prove one small thing (compact open subsets of spectral spaces are spectral). My code is about 100 lines, so I would like to contribute it and hopefully get feedback on it as well.

[Anne Baanen]

@Panagiotis Angelinos Sent! https://github.com/leanprover-community/mathlib4/invitations

[Daniel Weber]

Michael Stoll said:

It would make sense to merge #11049 before further changes are made to additive characters.

I worked with its version, so there shouldn't be conflicts, but yeah.

[Michael Stoll]

#11049 has been merged by now.

[Jon Bannon]

Dear friends, might I be granted write permission for the mathlib4 repo? (I'm working with)Thanks, in advance!

GitHub user name is JonBannon.

[Jireh Loreaux]

What's your Github username?

[Jireh Loreaux]

Nevermind, found it.

[Jireh Loreaux]

Please see https://github.com/leanprover-community/mathlib4/invitations

[Jireh Loreaux]

Jon is planning a small refactor of docs#Matrix.IsHermitian.eigenvectorMatrix

[Calle Sönne]

Hey, could I have write access to mathlib4? I would like to make a small PR containing lemmas about commutative squares. My github username is callesonne

[Kim Morrison]

@Calle Sönne, invitation sent.

[Mitchell Lee]

Hello! I would like to add some results to mathlib4 about reduced words in Coxeter groups, including Matsumoto's theorem. My github username is trivial1711.

[Tom Soucies]

Hello, can I get permission to add to Mathlib? I would like to work on some properties of bitvectors. My GitHub username is Tom-Soucies. Thank you!

[Johan Commelin]

@Tom Soucies My impression is that all material on bitvectors is being moved out of mathlib and into std. So it probably makes more sense to work on std.

cc @Scott Morrison

[Kim Morrison]

@Tom Soucies, in fact, please make PRs about BitVec direct to the Lean 4 repo. Happy to discuss plans your plans for BitVec.

[John Talbot]

Hi, please could I get write access to mathlib4? I'm interested in contributing results in extremal graph theory.
My Github username is jt496. Thanks!

[Oliver Nash]

@John Talbot Invite sent

[John Talbot]

Thanks!

[Yaël Dillies]

Hey! Just letting you know I started cleaning up your Turan formalisation for inclusion in mathlib

[Mitchell Lee]

Hello, I requested access a while ago. I hate to ask again, but I suspect that people might just have missed it. My github username is trivial1711.

Mitchell Lee said:

Hello! I would like to add some results to mathlib4 about reduced words in Coxeter groups, including Matsumoto's theorem. My github username is trivial1711.

[Oliver Nash]

@Mitchell Lee Sorry to keep you waiting; invite sent.

[Eyesomorphic]

Hello, is it possible if I could have write access to mathlib4? I'm working on formalising some categorical logic following Lambek and Scott's book, thanks :) My github username is Isaac-Ling

[Markus Himmel]

@Eyesomorphic Inviste sent, see https://github.com/leanprover-community/mathlib4/invitations

[Julien Michel]

Hello, I am interested in contributing to mathlib4. I was thinking to start with expanding the theory on data structures, and later work on graph theory topics.
Can I get write permissions to non-master branches ? My github name is michelsol.
Thanks in advance,

[Johan Commelin]

Data structures are mostly moving to the Std library. Could you please elaborate a bit what you have in mind?

[Julien Michel]

I was thinking to expand the basic theory on binary trees, BST's, tree based heaps, and other basic structures in their abstract form. I wasn't thinking of writing fast implementations. But I'm not sure how broad the scope of std is either.

[Kim Morrison]

Data structures are probably best developed in separate libraries. Particularly useful ones with thorough APIs (e.g. RBMap) can move to Std.

[Notification Bot]

A message was moved from this topic to #mathlib4 > Should data structures theory sit in mathlib? by Julien Michel.

[Bryan Gin-ge Chen]

@Julien Michel Invite sent! https://github.com/leanprover-community/mathlib4/invitations
I think the question of whether what you'd like to contribute about data structures is in scope for mathlib4 is something that can potentially be settled in the context of a PR or draft PR and shouldn't hold up an invitation to the repo. In any case, contributions on graph theory are certainly welcome.

[Christoph Spiegel]

Hi, can I get permissions to open a branch to clean up some Finset and Set naming discrepancies? I checked with @Yaël Dillies that they in fact aren't intentional. Github username is ForderUniver.

[Johan Commelin]

Github says:

Could not find a GitHub account matching ForderUniver

[Rida Hamadani]

They meant FordUniver.

[Christoph Spiegel]

Johan Commelin said:

Github says:

Could not find a GitHub account matching ForderUniver

:melting_face: it's FordUniver, let's hope my PR will be more thorough than this.

[Johan Commelin]

Voila: https://github.com/leanprover-community/mathlib4/invitations

[ZHAO Jiecheng]

Hi, can I get permission to open a branch to add some lemmas about the Array and ByteArray data structure. The code is currently in my gist . My git user name is JiechengZhao.

[Kim Morrison]

Could you say more about these lemmas? Generally I'd prefer lemmas about Array and ByteArray go as high as possible (i.e. Lean or Std).

[Notification Bot]

8 messages were moved from this topic to #general > (Byte)Array lemmas by Johan Commelin.

[Judith Ludwig]

Hi, could I get permission to open a branch in mathlib? I want to change a docstring and work on characterizations of etale morphisms.

[Riccardo Brasca]

What is your github username?

[Judith Ludwig]

sorry, it's judithludwig

[Riccardo Brasca]

Invitation sent!

[Edgar Costa]

I would like to mark a lemma as simp.
Can you please give me permission? my username is edgarcosta

[Floris van Doorn]

Invite sent!

[Edgar Costa]

tks

[Daniel Weber]

I want to add @to_additive to docs#Finset.card_mul_mul_le_card_div_mul_card_div, docs#Finset.card_div_mul_le_card_mul_mul_card_div, etc (and fix their docstrings). Could I please have permission? My username is Command-Master.

[Floris van Doorn]

@Daniel Weber Invite sent! Those lemmas indeed should have to_additive.

[Amos Turchet]

Hi, we will probably start the PRs from the Ostrowski's project in LFTCM2024. I think I had permission long time ago (but for Lean 3), could I have permission again? Thanks! My Git-hub user is amosturchet

[Riccardo Brasca]

Invitation sent!

[Enrico Borba]

Do we need additional permission to merge a PR into mathlib, or should I tell bors to merge or something else: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/github.20permission

I have a PR that is ready to merge but i'm not "authorized"

[Yaël Dillies]

If it's labelled ready-to-merge, it will soon be merged

[Johan Commelin]

@Enrico Borba Which PR number is this?

[Enrico Borba]

https://github.com/leanprover-community/mathlib4/pull/10189

[Sam Ezeh]

Hi! My GitHub username is dignissimus and I'm looking to contribute some lemmas for Hopf Algebras and help contribute to the tactic library

[Yaël Dillies]

Enrico Borba said:

https://github.com/leanprover-community/mathlib4/pull/10189

That PR hasn't been approved. You need to remove awaiting-author and add back awaiting-review so that other know they should review it. Then eventually a reviewer (eg me) or maintainer (eg Johan) will approve the PR and it will then be merged.

[Yaël Dillies]

Also on Zulip you can write #10189 and it will display #10189

[Kevin Buzzard]

@maintainers don't miss Sam Ezeh's request above, they're doing interesting stuff :-)

[Johan Commelin]

@Sam Ezeh Voila: https://github.com/leanprover-community/mathlib4/invitations

[Enrico Borba]

Yaël Dillies said:

Enrico Borba said:

https://github.com/leanprover-community/mathlib4/pull/10189

That PR hasn't been approved. You need to remove awaiting-author and add back awaiting-review so that other know they should review it. Then eventually a reviewer (eg me) or maintainer (eg Johan) will approve the PR and it will then be merged.

Sorry I was on mobile and didn't know the PR number, I just copied it from the github mobile app.

Also I took the approval from @Ruben Van de Velde as an approval of the PR. I'll add the label. Thanks!

[Enrico Borba]

Sorry for the constant messaging about this PR by the way. My experience with working on other open source projects and companies using github is a bit different from the PR flow here on mathlib. Really cool to see how it works on such a large repository with so many contributors.

[Hannah Fechtner]

Hi, could I have write access? I want to start making PRs for bits and pieces of the braid word problem (starting with presented monoids). My username is hannahfechtner

[Patrick Massot]

You have an invitation!

[Hannah Fechtner]

Screenshot-2024-04-01-at-9.51.19PM.png

[Patrick Massot]

Where do you see that?

[Hannah Fechtner]

lol, it's working now!

[Hannah Fechtner]

i switched my primary email to my cmu email, and then refreshed, and it worked. couldn't tell you why!

[Patrick Massot]

Happy PRing!

[Yaël Dillies]

@Tomáš Jakl, regarding https://github.com/leanprover-community/mathlib4/pull/11761#issuecomment-2031358499, you should ask for permission to modify mathlib branches here

[Yaël Dillies]

In fact, let me ask it for you: @maintainers, could jaklt get access?

[Tomáš Jakl]

thanks!

[Riccardo Brasca]

Invitation sent!

[Tomáš Jakl]

Got it and accepted, thanks!

[Salvatore Mercuri]

Hi, could I please get write access? My github username is smmercuri. I'm looking to start PRing some recent work formalising the proof that the adele ring of a number field is locally compact -- https://github.com/smmercuri/adele-ring_locally-compact . For now, I'd just like to add the one result Homeomorph.locallyCompactSpace that homeomorphisms preserve local compactness, but will PR more in the future.

[Oliver Nash]

@Salvatore Mercuri invite sent

[Oliver Nash]

I presume you've been in contact with @María Inés de Frutos Fernández about this work? Indeed I see you have.

[Salvatore Mercuri]

Oliver Nash said:

Salvatore Mercuri invite sent

received, thank you!

[Patrick Stevens]

Could I please have permission to push branches to mathlib4? Username is Smaug123; I had a few mathlib3 PRs merged back in the day. I have a couple of documentation changes I'd like to make.

[Oliver Nash]

@Patrick Stevens invite sent!

[Hyeokjun Kwon]

Hi, I would like to makes some PRs to the Mathlib. Could I please get write access to non-master branches? My Github username is Jun2M. I have a theorem about polytopes and more tiny lemmas that I proved playing with Lean.

[Anatole Dedecker]

Invitation sent!

[Robert Maxton]

I'd like PR permission for mathlib; I've got an extension of TFAE to Type-level objects under an equivalence, a matching command tfae_def to express the idiom "the following definitions of a particular identifier are equivalent", and then all colimits for AlgebraCat to contribute. (In seperate PRs, of course.) My github is https://github.com/robertmaxton42

[Kim Morrison]

Invitation sent, looking forward to seeing it!

[blfang]

Hi all, could I get write access to non-master branches? Username is blfang. Would like to get my feet wet with some undergrad probability topics, and eventually move on to results in statistics, concentration inequalities, and related areas.

[Anne Baanen]

blfang said:

Hi all, could I get write access to non-master branches? Username is blfang. Would like to get my feet wet with some undergrad probability topics, and eventually move on to results in statistics, concentration inequalities, and related areas.

Invite sent! https://github.com/leanprover-community/mathlib4/invitations

[Cedric Holle]

Hello, can I have permission to push to mathlib4? My github username is todbeibrot. I am currently working on interfacing Lean with Oscar. I already made a pull request for a simple bug fix and would like to mark it as awaiting review

[Alex J. Best]

The PR looks fine but seeing as its from a fork rather than a branch I'm not sure CI will ever run on it, and correspondingly bors may be unhappy merging it. I'd recommend reopening the PR from a branch on the main mathlib repo itself when you get permission for simplicity

[Gregory Constantine]

Hello! I would like to work on some missing lemmas in Combinatorics/SimpleGraph. In the meantime, I have completed some basic list lemmas and have found a tiny bug in the docs. If possible, I would appreciate PR permissions. My github username is greg-const.

[Kevin Buzzard]

Invitation sent! https://github.com/leanprover-community/mathlib4/invitations

[Huanchen Bao]

Hi. This is Huanchen from National University of Singapore. We have a group working the combinatorics of Coxeter groups. I am writing to ask for permission for branches on Mathlib. Github username: mathnus

[Kevin Buzzard]

The maintainers are reluctant to give write access to mathlib to a group of people who are all using one GitHub account, and as has been pointed out before this use of GitHub is against the GitHub terms and conditions. The correct way to set up a multiuser situation like this is to have each user create an individual account and then create an organisation containing all those users.

[Huanchen Bao]

We actually used the Github to create an organization on formalization (for some practical purpose). All members are in the organization already. In any case, let us use my Github : HuanchenNUS

[Mario Carneiro]

from what I can tell https://github.com/mathnus is not an organization account

[Mario Carneiro]

it looks like the organization is https://github.com/NUS-Math-Formalization

[Huanchen Bao]

Do you mean to give access to the organization https://github.com/NUS-Math-Formalization? The github mathnus is just for admin purpose. No one is contributing using this.

[Kevin Buzzard]

I don't think it's possible to give access to an organisation?

[Huanchen Bao]

Then maybe we can just use mine : HuanchenNUS ?

[Ruben Van de Velde]

I am concerned by the use of "we" in that sentence. Each person in your group should create and use an individual account

[Huanchen Bao]

By "we" I mean us here in the Zulip.

[Huanchen Bao]

Everyone is using individual github acount in our organization.

[Vláďa Sedláček]

Hi, could I please get write access to mathlib4 to start PR'ing some of the work on
Prime Number Theorem+? My GitHub name is VladaSedlacek (I'm currently a postdoc at Rutgers, with experience in cryptography and some number theory). Thanks!

[Cedric Holle]

Cedric Holle said:

Hello, can I have permission to push to mathlib4? My github username is todbeibrot. I am currently working on interfacing Lean with Oscar. I already made a pull request for a simple bug fix and would like to mark it as awaiting review

My request for a permission is still open. I would love to contribute.

[Bryan Gin-ge Chen]

@Cedric Holle Sorry that your request fell through the cracks! I've sent you an invite:
https://github.com/leanprover-community/mathlib4/invitations

[Bryan Gin-ge Chen]

@Vláďa Sedláček I've sent you an invite: https://github.com/leanprover-community/mathlib4/invitations

[Kim Morrison]

Huanchen Bao said:

Everyone is using individual github acount in our organization.

@Huanchen Bao, are there others who will be making PRs? (If so, what are the user names?) I'm still a bit unclear on what the plan is here.

[Huanchen Bao]

I will be the only making the PR request, on behalf of the team. And I am the only one using this github account. Does this clarify the situation?

[Jake Jongejans]

Good morning! I'd like to contribute to Mathlib over the coming period as I am working on a parallel project (proving quantum algorithms) using Lean and Mathlib.

I will be discussing my progress on that project here and if there is anything useful that benefits everybody, such as Imaginary Number Representation, I intend to polish my code according to Lean and Mathlib standards and PR it.

My GitHub username is Javernus.

[Markus Himmel]

@Jake Jongejans I've sent you an invite: https://github.com/leanprover-community/mathlib4/invitations

[Ralf Stephan]

Hello,
I'm just preparing a first addition to PNat (raw version already visible here), so I would ask you for permission to do direct PRs, after I sorted and documented the theorems into the resp. mathlib files. These are the result of trying to find a prod_Icc_* proof using PNat as index (which I think is a natural choice). Username: rwst.

[Floris van Doorn]

invite sent!

[Yves Jäckle]

Hey!
I want to add a List lemma:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/List.20lemma.20for.20mathlib/near/435553663
My username is: Happyves

[Yves Jäckle]

Nevermind, Michael Rothgang and Bolton Bailey are handling it

[Yaël Dillies]

It's not because someone gave you code on Zulip that they are going to PR it!

[Kevin Buzzard]

@Yves Jäckle invite sent! Feel free to make the PR, don't just assume someone else will do it, even if it's all their code (it's fine to PR someone else's code).

[Ben Eltschig]

I'd like to open a PR adding the IsHomeomorph predicate that I asked about a few days ago, but just realised I don't yet have the necessary permissions - could someone give them to me maybe? My username is peabrainiac.

[Nirvana Coppola]

I'd like to request the permission. My username is NirvanaC93

[Johan Commelin]

@Ben Eltschig @Nirvana Coppola , voila: https://github.com/leanprover-community/mathlib4/invitations

[Tom Kranz]

I would like to ask for permission, too. I'm TpmKranz on Github.

[Floris van Doorn]

invite sent!

[Keegan Perry]

Hi there, I'd like to request permission. My username is keeganperry7.

[Kevin Buzzard]

What kind of things are you interested in adding?

[Keegan Perry]

Kevin Buzzard said:

What kind of things are you interested in adding?

I'm interested in adding the proofs for some of the closure properties of epsilon NFAs, which will help with formalizing the equivalence of regular expressions and finite automata.

[Floris van Doorn]

It would be good to get some automata theory in Mathlib. I sent you an invite.

[Herman Chau]

Hi, I'd like to request permission. My github username is kcaze and I'm interested in contributing to Mathlib.RingTheory.PowerSeries.

[Floris van Doorn]

invite sent

[John Tristan]

Hi, I would like to obtain write-access to non-master branches of the Mathlib4 repository. My github username is jtristan. I'm planning on contributing simple but useful theorems that I wish were available when doing program verification. That would include topics such as extended non-negative reals, infinite sums, analysis.

[Matthew Ballard]

@John Tristan invitation sent!

[Emily Riehl]

I'd like to try to submit my first pull request, so am hoping for write access. My github is emilyriehl

Update: thanks!

[Riccardo Brasca]

Invitation sent!

[Eric Paul]

Hello, I'd like to request access. I'm interested in contributing to Linear Orders!
My usernamne is ericluap

[Kevin Buzzard]

@Eric invitation sent!

[Lode Vermeulen]

Hi! I'd like to request push access to hopefully make and close some PRs in graph theory. My GitHub username is LodeVermeulen.

[Kyle Miller]

@Lode Vermeulen Invitation sent!

[Markus Schmaus]

I would like to request access, so I can potentially modify the mathlib branch for Lean PR #4242. My github name is markusschmaus.

[Markus Himmel]

@Markus Schmaus done: https://github.com/leanprover-community/mathlib4/invitations

[Alvan Arulandu]

Hello! I'm Alvan, a Math/CS student at Harvard interested in contributing to Probability by proving some measure theory theorems and hopefully the CLT. If I could get push access, that'd be great, and I'd love advice as well!

[Kevin Buzzard]

Did you write any code yet or are you just beginning?

[Alvan Arulandu]

Kevin Buzzard said:

Did you write any code yet or are you just beginning?

Besides a few arbitrary undergrad math theorems for practice, I haven't written much code. My current plan is to work through Axler's Measure, Integration, and Real Analysis book while verifying the necessary results to finally get CLT, using Jeremy Avigad's proof in Isabelle/HOL for reference.

[Kevin Buzzard]

Then I think you're a fair way from needing push access :-) One thing about working through a book: (1) don't redo any definitions, we have them already, possibly in far more generality than you'll need and (2) it might not be the best idea to just prove all the theorems in the order they're proved in the book, as they're stated in the book, if you're ultimately interested in contributing to mathlib. Before embarking on any nontrivial proof you might want to discuss what statement/version is appropriate for mathlib.

[Alvan Arulandu]

Kevin Buzzard said:

Then I think you're a fair way from needing push access :-) One thing about working through a book: (1) don't redo any definitions, we have them already, possibly in far more generality than you'll need and (2) it might not be the best idea to just prove all the theorems in the order they're proved in the book, as they're stated in the book, if you're ultimately interested in contributing to mathlib. Before embarking on any nontrivial proof you might want to discuss what statement/version is appropriate for mathlib.

That makes sense. Thank you so much!

[t4ccer]

Hi, could I get push access please? I'd like to clean up use of List.nthLe in GroupTheory.Perm.List. My github username is t4ccer

[Kim Morrison]

Do you have an existing branch somewhere?

[t4ccer]

Yes, I have it on my fork

[Kim Morrison]

Invitation sent!

[Kim Morrison]

I think you may be able to get better statements for the new lemmas.

[Chance Nahuway]

Hello, I've written two simple lemmas/simps for negating matrices that are partitioned by row and by column in the Mathlib.Data.Matrix.ColumnRowPartitioned.lean file, as suggested by @Martin Dvořák . Could I be granted access to push those changes please? My GitHub username is chancenahuway — thank you for considering my request!

[Kevin Buzzard]

@Chance Nahuway invite sent!

[Niklas Mohrin]

Hey, last semester we worked on a theorem from Network Flows (see my other thread) and I have now continued working on it a bit to generalize the definitions first to Int and now to arbitrary rings / fields. I have some code for the definitions which I would PR to mathlib to see if it is useful, could anyone give me the permission to push a branch?

[Floris van Doorn]

invite sent

[Ted Hwa]

Could I get permissions to push a branch for mathlib4? My github username is hwatheod. I have ported to mathlib4 the theorems about surreal number multiplication from this old mathlib3 branch. Right now it is in a separate project and I just need to move everything to the proper place in mathlib4.

[Floris van Doorn]

invite sent

[Aadhavan Kumaran]

Hey, may I have permissions to push a branch? I would like to add a few lemmas to the Nat.dist file which will make induction on distance easier. My github is Awe1230.

[Stefan Kebekus]

Dear all, I would like to request permissions to push a branch for mathlib4 on GitHub. My intention is to improve the documentation a little, and add API, definitions and basic theorem concerning Harmonic functions and the Laplacian.

My GitHub user name is kebekus.

[Patrick Massot]

You have an invitation!

[Stefan Kebekus]

Patrick Massot schrieb:

You have an invitation!

Thank you so much.

[Seewoo Lee]

Hi, could I get a GitHub permission for mathlib4? We (me and @Jineon Baek ) would work on our formalization of Mason-Stother's theorem over polynomials (this repo https://github.com/seewoo5/lean-poly-abc and also there's a thread that I don't know how to mention...) My GitHub username is seewoo5.

[Yaël Dillies]

Thread

[Kim Morrison]

@Seewoo Lee, invitation sent!

[Seewoo Lee]

Thank you!

[Jineon Baek]

I will also need a permission for the same reason as @Seewoo Lee. Thank you in advance!

[Kim Morrison]

@Jineon Baek, invitation sent!

[Jackie Lang]

Hi, could I get permission to open a branch in math lib? I'd like to change a docstring and contribute. My Github name is jaclynlang. Thank you!

[Kim Morrison]

Hi @Jackie Lang, invitation sent!

[Samyak Tuladhar]

Hi, could I get permission for pushing branches on mathlib4? My intention is to work on simulatenous diagonalization of tuples of symmetric operators. My GitHub username is Samyak-DT

[Kim Morrison]

@Samyak Tuladhar, invitation sent!

[Anthony Bordg]

Dear mathlib4 @maintainers,
I would like to request write access to non-master branches. My Github username is AnthonyBordg .

[Kim Morrison]

@Anthony Bordg, invitation sent.

[Anthony Bordg]

Thank you, @Kim Morrison :smile:

[Alain Chavarri Villarello]

Hi! Could I get push access please? (I previously had it for Mathlib3  :grimacing: ). I’d like to PR some lemmas about polynomial irreducibility over finite fields. Username: alainchmt

[Kevin Buzzard]

@Alain Chavarri Villarello invitation sent!

[Janette Setälä]

Could I have permission to Mathlib branches to PR this? My GitHub username is janemms.

[Nick Decroos]

Dear mathlib4 maintainers, I'd like to request write access to non-master branches of the mathlib4 repository.
My GitHub username is ndcroos.

[Johan Commelin]

@Janette Setälä Voila: https://github.com/leanprover-community/mathlib4/invitations

[Johan Commelin]

@Nick Decroos Could you please tell a bit more about what you want to work on / contribute?

[Nick Decroos]

Hi @Johan Commelin I'd like to work on the Shapley-Folkman lemma as a first project, as described here: https://github.com/leanprover-community/mathlib4/issues/14427

[Johan Commelin]

Thanks. Voila: https://github.com/leanprover-community/mathlib4/invitations

[Kim Morrison]

And just a general reminder for everyone asking for permission for write access: the standing request is that your write a sentence or two along with your request about what you're planning to contribute.

Often we overlook this for people "we know", but it's helpful if everyone asking here does this for consistency!

[Ludwig Monnerjahn]

Hi, Iid like to get write access to non-master branches of the mathlib4 repository for this PR #13930. My Github username is Louis-Le-Grand.

[Kim Morrison]

@Ludwig Monnerjahn, invitation sent.

[Quang Dao]

Hi, I'd like to get write access to non-master branches of the mathlib4 repo for adding mapAlgHom and supporting theorems to Polynomial. My Github username is quangvdao.

[Quang Dao]

^wanted to bump up the request above in case it got lost

[Kim Morrison]

@Quang Dao, invitation sent.

[Hannah Scholz]

Hi, I'd like to request write access to non-master branches to right now add a lemma about Set.Subsingletons being closed and later to add some of the code I am writing about CW-complexes. My github username is scholzhannah.

[Floris van Doorn]

invitation sent!

[Matteo Del Vecchio]

Hello, I would like to request write access to non-master branches. Right now, I have generalized Mathlib.Analysis.Complex.Hadamard so that the theorem works on any vertical strip instead of just the strip of complex numbers with real part between 0 and 1. My github username is madeve-unipi.

[Riccardo Brasca]

Ciao! You should have an invitation

[Eloi Torrents]

Hi, I would like to request GH permission. I want to contribute some category theory lemmas like Under x ≅ (Over (.op x : Cᵒᵖ))ᵒᵖ or IsSplitMono f ↔ IsSplitEpi f.op and variants of those if they are useful. My Github user is eloitor.

[Kin Yau James Wong]

Hi, I'd like to request Github permission. I am currently working on refactoring Disintegration in ProbabilityTheory.Kernelwith @Yaël Dillies. My username is james18lpc.

[Rémy Degenne]

Invite sent

[Kevin Buzzard]

Rémy Degenne said:

Invite sent

To Eloi or Kin?

[Rémy Degenne]

To Kin. Sorry, I did not see there were several.

[Rémy Degenne]

Sent to Eloi as well.

[Notification Bot]

13 messages were moved here from #mathlib4 > github permission by Yaël Dillies.

[Bjørn Kjos-Hanssen]

Hi, my Github username is bjoernkjoshanssen. I'm working on various Lean projects, many of which are not Mathlib-level or Mathlib-relevant yet, but one small contribution I could make now was mentioned here: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Measure.2Ecomap.20injectivity/near/446350591

[Victor Liu]

Hi there! My GitHub username is victorliu5296. I am requesting write access to Mathlib4 for non-master ranches. I am working on formalizing the Newton-Kantorovich theorem and have already completed the Mean Value Theorem for Functions of class C^1 with Values in a Banach Space lemma, which is a variation of the Fundamental Theorem of Calculus part 2. The source code can be found here.

[Kevin Buzzard]

Bjoern and Victor -- invitations sent!

[Bjørn Kjos-Hanssen]

Thanks @Kevin Buzzard it seems that I was able to make a (very small) PR just now.

[Nicolas Rolland]

Hi,

Could you grant me (nrolland) write access to mathlib4 for non-master branches ?
I aim to add distributors in mathlib4, and will start with a few small contributions, like Monoidal instance for Cat

[Kim Morrison]

@Nicolas Rolland, invitation sent!

[Shuhao Song]

Hi, my GitHub name is meow-sister. I would like to submit some code about graph theory.

[Kim Morrison]

@Shuhao Song, invitation sent!

[Henrik Lievonen]

Hi! I would like to contribute some documentation updates and some helpers for SimpleGraphs. My Github account is henkkuli.

[Kim Morrison]

Invitation sent!

[Henrik Lievonen]

Thanks! Accepted and opened PRs for my changes: #15542 and #15541.

[Alexander Hicks]

Hello! I would like to contribute a straightforward definition for the weight of a vector (for any given boolean predicate) that, if I'm not mistaken, doesn't seem to currently exist in mathlib. My github account is alexanderlhicks.

[Bolton Bailey]

@maintainers :this:
Also @Alexander Hicks if you are referring to Hamming weight, you might be interested in docs#hammingNorm

[Alexander Hicks]

I've seen it! I just thought something that works with any boolean predicate might be useful, with the hamming weight being the special case with predicate (· ≠ 0). (Assuming that variable [∀ i, Zero (β i)] [∀ i, Zero (γ i)] doesn't already provide this)

[Kim Morrison]

@Alexander Hicks, invite sent.

[Nick Mertes]

Hello, I am requesting write access for mathlib4 based on the recommendation here. I am hoping to edit rel_iso_iff to make the theorem universe polymorphic. My GitHub is nmertes7.

[Kim Morrison]

@Nick Mertes what universe polymorphism is possible there? Because it is talking about categorical hom, the source and target objects must be the same universe.

[Nick Mertes]

@Kim Morrison my proposal is to change C := Type to C := Type u in the statement and proof. As the theorem is currently stated, C := Type makes RelCat : Type 1. But with C := Type u then RelCat : Type (u + 1).

[Kim Morrison]

@Nick Mertes, invitation sent.

[Nicky Mouha]

Hi! Could you grant me (nmouha) write access to mathlib4 for non-master branches?

I have two pull requests (#15602 and #15665) related to Data/Nat/Factorial that I made from my personal account. I will close these two pull requests and make new two new ones from the main mathlib4 repository.

Thanks!
Nicky

[Kim Morrison]

@Nicky Mouha, invitation sent!

[Kim Morrison]

And welcome! Looking forward to more crypto-relevant PRs. :-)

[Nicky Mouha]

Thank you, @Kim Morrison! I've closed the two PRs and reopened them (#15757 and #15758).

[Nicky Mouha]

In case someone might be interested in the cryptographic application of descFactorial_le and descFactorial_mul_descFactorial. It's related to Chaskey (https://mouha.be/chaskey/). The inequality on page 11 of https://eprint.iacr.org/2014/386.pdf can be turned into the inequality below, and its proof follows from descFactorial_mul_descFactorial to split all the sums, followed by some simple rewriting involving descFactorial_le and Nat.mul_le_mul.

[Nicky Mouha]

example {D₁ D₂ D₃ T M : ℕ} : M.descFactorial (D₁ + D₂ + D₃) ≤
  (M + T).descFactorial D₁ * (M + T).descFactorial D₂ * (M + T).descFactorial D₃ := by
    sorry

[Nicky Mouha]

It seems that computer algebra systems can't handle such inequalities involving factorials, and that an interactive theorem prover is necessary here.

[Yaël Dillies]

Nicky Mouha said:

Thank you, @Kim Morrison! I've closed the two PRs and reopened them (https://github.com/leanprover-community/mathlib4/pull/15757 and https://github.com/leanprover-community/mathlib4/pull/15758).

Welcome! FYI you can write #15757 and Zulip will turn it into #15757

[Ahmad Alkhalawi]

Hello, I'd like to request write access. I'm planning on submitting the Woodbury identity as my first pr. My github name is 4hma4d.

[Nicky Mouha]

Thank you, @Yaël Dillies , for pointing this out! I've edited my post to correct this.

[Junqi Liu]

Hello! I would like to work on some lemmas in Legendre Polynomial. If possible, I would appreciate PR permissions. My github username is ahhwuhu.

[Kim Morrison]

ahhwuhu said:

Hello! I would like to work on some lemmas in Legendre Polynomial. If possible, I would appreciate PR permissions. My github username is ahhwuhu.

@ahhwuhu, could you say a little more about what you are planning on doing?

[Artie Khovanov]

Hi, requesting write permission for non-master branches (GitHub acct: FM22).

I am working on formalising material relating to real closed fields, but right now I am just trying to PR a one line change relaxing a typeclass contraint (https://github.com/leanprover-community/mathlib4/pull/15840).

[Artie Khovanov]

Thank you @Matthew Ballard

[Kai L]

Could I get permission to write to non-master branches, trying to work on https://github.com/leanprover-community/mathlib4/issues/10267
my github is Xmask19

[Notification Bot]

11 messages were moved from this topic to #mathlib4 > Woodbury identity by Eric Wieser.

[Eric Wieser]

Ahmad Alkhalawi said:

Hello, I'd like to request write access. I'm planning on submitting the Woodbury identity as my first pr. My github name is 4hma4d.

@Kim Morrison, I moved the technical discussion to a new thread for visibility; are you happy to grant access?

[Dexin Zhang]

Hello, I'd like to request write access to non-master branches. I want to open a PR to define the ordinal ranks of ZFSet. Here are some discussion. My github username is staroperator. Thanks!

[Junqi Liu]

(deleted)

[Junqi Liu]

Kim Morrison said:

ahhwuhu said:

Hello! I would like to work on some lemmas in Legendre Polynomial. If possible, I would appreciate PR permissions. My github username is ahhwuhu.

ahhwuhu, could you say a little more about what you are planning on doing?

@Kim Morrison Sure! I did some lemma on the basic properties of Legendre Polynomial.

[Isak Colboubrani]

Hello! I would like to contribute some code to allow Lean to automatically recognize ideals as non-unital rings (as suggested here).

[Kim Morrison]

ahhwuhu said:

Kim Morrison said:

ahhwuhu said:

Hello! I would like to work on some lemmas in Legendre Polynomial. If possible, I would appreciate PR permissions. My github username is ahhwuhu.

ahhwuhu, could you say a little more about what you are planning on doing?

Kim Morrison Sure! I did some lemma on the basic properties of Legendre Polynomial.

@ahhwuhu, you don't seem to have given any more information in your reply than you did in your initial message! Could you please give a little more detail?

[Junqi Liu]

Kim Morrison said:

ahhwuhu said:

Kim Morrison said:

ahhwuhu said:

Hello! I would like to work on some lemmas in Legendre Polynomial. If possible, I would appreciate PR permissions. My github username is ahhwuhu.

ahhwuhu, could you say a little more about what you are planning on doing?

Kim Morrison Sure! I did some lemma on the basic properties of Legendre Polynomial.

ahhwuhu, you don't seem to have given any more information in your reply than you did in your initial message! Could you please give a little more detail?

@Kim Morrison ok! I mainly defined Legendre Polynomial and proved that the Legendre Polynomial is a polynomial with integer coefficients , $P_n(x) = (-1 )^n P_n(1-x)$ and some useful lemma.

[Floris van Doorn]

@ahhwuhu I sent you an invite!

[Junqi Liu]

Floris van Doorn said:

ahhwuhu I sent you an invite!

Thanks!

[Rida Hamadani]

Kai L said:

Could I get permission to write to non-master branches, trying to work on https://github.com/leanprover-community/mathlib4/issues/10267
my github is Xmask19

Bumping this, I am working with Kai to fix the issue.

[Kim Morrison]

When I tried to invite, github says there is a pending invitation already.

[Notification Bot]

20 messages were moved from this topic to #mathlib4 > github permission (stacks annotations) by Eric Wieser.

[Eric Wieser]

(If you come to this thread because you want to "mark and add theorems in the Stacks project", please use the thread above instead)

[Alex Brodbelt]

Hi! I formalized problem 3 of the 1982 IMO https://github.com/AlexBrodbelt/LeanIMO/blob/main/Imo1982Q3/Basic.lean

I'd like to request write access to non-master branches. I want to open a PR to add this file to the Archive/Imo folder. My github username is AlexBrodbelt

[Matthew Ballard]

@Alex Brodbelt invitation sent!

[mdnestor]

Hi, I am interested in adding Lawvere's fixed point theorem as well as some generalizations. My github is mdnestor. I have a working implementation at https://github.com/mdnestor/LawvereFixedPoint

Prior discussion at #Is there code for X? > Lawvere fixed point theorem

[Kim Morrison]

@mdnestor, invitation sent.

[Yongle Hu]

Could I get permission to write to non-master branches? I am working on formalizing the proof of is integral closed is a local property. My github name is mbkybky. Here is my code https://github.com/jjdishere/neukirch/blob/master/AlgebraicNumberTheory/AlgebraicIntegersPart2/Localization.lean

[Suzuka Yu]

Greetings! I wish to apply for permission to commit to non-master branch [**PKU**_PR_JacobsonNoether](https://github.com/leanprover-community/mathlib4/tree/PKU_PR_JacobsonNoether) - I did some improvements to final_aux and certain calcs

[Kevin Buzzard]

Hi! It was really interesting working with you all over the last few days. I'm really sorry that I can't add you right now because I can't access github, but I can definitely vouch for you both :-) @Suzuka Yu or possibly @Suzuka Yu we need to know your github userid (and ideally you would also delete one of your accounts if these are both you). Edit: aah I see from your Zulip that you're Yu-Misaka.

[Suzuka Yu]

oh, yes that's me, thanks! It's my honor to work under your guidance. :heart: (I don't remember to have two accounts, but I'll check later)

Kevin Buzzard 发言道：

Hi! It was really interesting working with you all over the last few days. I'm really sorry that I can't add you right now because I can't access github, but I can definitely vouch for you both :-) Suzuka Yu or possibly Suzuka Yu we need to know your github userid (and ideally you would also delete one of your accounts if these are both you). Edit: aah I see from your Zulip that you're Yu-Misaka.

[Bryan Gin-ge Chen]

@Suzuka Yu Invite sent (to Yu-Misaka): https://github.com/leanprover-community/mathlib4/invitations

[Kevin Buzzard]

Sorry, we also need user mbkybky above. I'll be back in the land of Github-accessibility in 48 hours :-)

[Bryan Gin-ge Chen]

@Yongle Hu invite sent! https://github.com/leanprover-community/mathlib4/invitations

[Albert.J]

Hi, I am working on improving the proof of Jacobson-Noether theorem (with Suzuka Yu above). See PR Here
I'd like to request write access to non-master branch so that I can push some of my changes on the proof of hc, my GitHub username is AlbertJ-314, thanks very much!

[Riccardo Brasca]

Invitation sent!

[Kim Morrison]

(and just a reminder that we do recommend that people asking for write access to Mathlib have a username matching their usual name offline, while understanding that there are many reasons to prefer not to, and that no explanation is needed)

[Filippo A. E. Nuccio]

Welcome @Albert.J !

[Arthur Adjedj]

Hi, I’m working on lean4#3160, and would need permissions on the mathlib4 repo to have CI run on a branch which would fix the mathlib breakages associated with the PR. My github username is arthur-adjedj.
Thank you very much :)

[Kim Morrison]

@Arthur Adjedj , invitation sent.

[Metin Ersin Arıcan]

Hi! I am requesting write-access to non-master branches of mathlib. I have been learning lean for quite some time and I want to contribute to Mathlib.ModelTheory. At first, I will start simple and prove that the theory of dense linear orders is ℵ₀.Categorical. This fact already exists in mathlib in terms of various instances LinearOrder, NoBotOrder etc. I will just transfer it to the model theory world. Later, I am planning to define conjunctive/disjunctive normal forms and prove that every formula is equivalent to a formula in these forms. My github username is metinersin. Thanks in advance.

[Riccardo Brasca]

Invitation sent!

[Yaël Dillies]

Hey! Thank you for your interest. I suggest you coordinate with @Aaron Anderson who is currently adding very similar statements to mathlib.

[Aaron Anderson]

@Metin Ersin Arıcan and I just discussed this - categoricity is basically immediate from recent work on Fraïssé theory, so I am PRing that (#16804), but I very much look forward to the work on normal forms.

[Aaron Hill]

Hi - I'm working on contributing a proof of the reverse direction of the lucas_primality theorem, and I'd like to request write access to non-master branches. My Github username is Aaron1011

I've managed to get a proof locally (without any sorrys), but it's a total mess since I'm very new to lean.

[Kim Morrison]

@Aaron Hill, invitation sent!

[Pieter Cuijpers]

As a theoretical computer scientists, I'd like to work on adding Quantales and Labeled Transition Systems to Mathlib. Can I please have push access tot the non-master branches? My github username is PieterCuijpers.

[Kevin Buzzard]

Are you sure that those belong in mathlib? Which mathematical theorems will use them?

[Kevin Buzzard]

These sound more appropriate for the CSLib library that we sometimes dream of.

[Kim Morrison]

@Pieter Cuijpers, do you have some existing code?

[Yaël Dillies]

FWIW some quantales show up in mathlib already, eg docs#ENNReal. It would be nice to have the typeclass if only for generalising a few lemmas

[Patrick Massot]

Generalizing to which other examples?

[Pieter Cuijpers]

@Kim Working on it...

[Pieter Cuijpers]

@Kevin Buzzard I think Quantales definitely belong in mathlib. They are a generalization of locales/frames which are already in there. Applications range from CS to quantum mechanics (where they were originally conceived).

Whether LTS belong in mathlib is, I guess, more debatable. I'm not a person who makes distinctions between fields. I like to skip and jump from one to the other without caring what it is called. But if there would be a CSLib library, then that would be more logical indeed. What would be needed to make that happen? And what would be the argument against including LTS in mathlib? What is your criterion for considering something mathematics or not?

[Rémy Degenne]

A practical consideration is that for something to go to Mathlib, we need to have reviewers/maintainers able to review and then maintain it. If nobody among the reviewers and maintainers knows about those LTS (I am not sure if that's the case or not), it's a sign Mathlib may not be the right place. In that case you could always develop them in a separate repository. For reference, here is the list of maintainers and their areas of expertise: https://github.com/leanprover-community/mathlib4?tab=readme-ov-file#maintainers .

The question is not really whether it is math or not math, but whether it is the kind of math that should go to Mathlib. A good guideline to know if it should go to Mathlib is to ask whether that subject would be introduced in an undergraduate or graduate level course in a research mathematics department.

[Yaël Dillies]

Patrick Massot said:

Generalizing to which other examples?

Submodules, eg

[Pieter Cuijpers]

@Rémy Degenne thanks for the attempt to give a guideline - I think in the end it is indeed about maintenance, and creating a maintenance team that is large enough to cover the target domain yet small enough to still be able to agree on things. Adding CS-maintainers to the team would probably open up a too large domain to still be able to agree, so having a CSLib may make more sense.

What is needed to create a CSLib? I suspect the Coq community already did quite some of the ground work for that?

[Kim Morrison]

Does it make sense to talk about LTS in the #graph theory channel?

[Mario Carneiro]

yes, please don't talk about unrelated matters on this topic since most maintainers get pinged on every message

[Raphael Douglas Giles]

Hi there, I'd like to request write access to non-master branches of mathlib. I'd like to add some lemmas about the topological Krull dimension (mainly that it's homeomorphism invariant). My github username is Raph-DG

[Kevin Buzzard]

@Raphael Douglas Giles invitation sent!

[Alvaro Belmonte]

I would like to make my first PR about Codiscrete Categories. Could I have write access? AlvaroRBO

[Matthew Ballard]

@Alvaro Belmonte what is your github username?

[Alvaro Belmonte]

Sorry, i forgot to add it. Just edited my last message

[Matthew Ballard]

Invitation sent! Looking forward to the PR :)

[Pieter Cuijpers]

Pieter Cuijpers said:

As a theoretical computer scientists, I'd like to work on adding Quantales and Labeled Transition Systems to Mathlib. Can I please have push access tot the non-master branches? My github username is PieterCuijpers.

Kim suggested I simply make a PR for my Quantale definitions. Can anyone give me access pls?

[Kim Morrison]

Invitation sent, @Pieter Cuijpers.

[Nicky Mouha]

Nicky Mouha said:

In case someone might be interested in the cryptographic application of descFactorial_le and descFactorial_mul_descFactorial. It's related to Chaskey (https://mouha.be/chaskey/). The inequality on page 11 of https://eprint.iacr.org/2014/386.pdf can be turned into the inequality below, and its proof follows from descFactorial_mul_descFactorial to split all the sums, followed by some simple rewriting involving descFactorial_le and Nat.mul_le_mul.

Just FYI: I've written a blog post about this: https://mouha.be/computer-checked-proofs-for-chaskey/

Feedback is welcome!

[Daniel Carranza]

Hello! I would like to request write access to non-master branches of Mathlib. I am working on adding a proof that every closed monoidal category is enriched in itself.

My Github username is: daniel-carranza . Many thanks in advance!

[Kim Morrison]

@Daniel Carranza, invitation sent.

[syur2]

Could I get permission to write to non-master branches? I am working on formalizing the proof of localization of the submodules ⊥ (resp. ⊤) is also ⊥ (resp. ⊤) . My github name is syur2. Here is my code.

[Johan Commelin]

@syur2 Voila: https://github.com/leanprover-community/mathlib4/invitations

[Zhu]

Hi, I am attempting to prove some theorems related to computational complexity, such as the Lovász Local Lemma. And I'd like to request write access to non-master branch, my Github username is hehepig166, thanks a lot :)

[Yaël Dillies]

Hey! LLL was already proved by @Yves Jäckle, but feel free to tackle something else :smile:

[Zhu]

Oh, sorry, I didn't find the proof when I searched earlier. Could you share the link to Yves Jäckle's proof? I'd love to study the code. Thanks! :folded_hands:

[Yaël Dillies]

I believe it is somewhere in here but I am not sure

[Yves Jäckle]

A full proof of LLL is at: https://github.com/nsglover/lean-lovasz-local-lemma
I tried implementing the standard proof (refer for example to that in "Extremal Combinatorics" by Jukna) at some point, I don't think I completed it... The standard proof is actually false in most textbooks: you need two inductions, as was done in the original (refer to p.8 of the attached paper)
lll_original_p8.pdf

[Yves Jäckle]

@Zhu
Local_Lemma.lean
Dug up the original code, which is in a horrible state.

[Zhu]

Yves Jäckle said:

A full proof of LLL is at: https://github.com/nsglover/lean-lovasz-local-lemma
I tried implementing the standard proof (refer for example to that in "Extremal Combinatorics" by Jukna) at some point, I don't think I completed it... The standard proof is actually false in most textbooks: you need two inductions, as was done in the original (refer to p.8 of the attached paper)
lll_original_p8.pdf

Thank you all so much for your helpful responses!
I really appreciate the guidance, and I'd be happy to make efforts to get LLL into mathlib. I'll take a look at the resources you provided and will reach out if I need further assistance.
Thanks again! :smile:

[Jeremy Avigad]

@Zhu, @Nathan Glover is now a PhD student at Carnegie Mellon working on other things, but I am sure he would be happy to talk about the formalization.

[Javier Lopez-Contreras]

Hello! I've been told in #mathlib4 > Hello + mathlib non-main write permission? that this is the correct place to ask for github write permissions for (non-main branch) in Mathlib4. My github username is javierlcontreras

[Kevin Buzzard]

Usually we ask for descriptions of what you're planning to PR but given that you're my new PhD student I think everyone can guess. Invitation sent!

[Ruben Van de Velde]

I'm guessing Euclidean geometry

[Alex Loitzl 🐓]

Hi,
I'd like to request write access for a non-master branch. My Github username is AlexLoitzl. I'm working on formalizing the pumping lemma for CFG here, with help from @Martin Dvořák .

[Mark Santa Clara Munro]

Hi! I'm working on contributing with a proof on the correctness of Gaussian Elimination. I am working with @Christopher Lynch, and we have proved many properties of elementary row operations already.

I would like to request write access to a non-master branch. My GitHub username is markimunro and Dr. Lynch's is cxlynch. Let me know if he needs to send a message as well and thank you so much in advance!

[Kim Morrison]

Invitations sent for both!

[Mark Santa Clara Munro]

Thank you so much!

[Christoph Spiegel]

Hey, could ooovi get github permissions for mathlib? We want to try to address the two TODOs in Combinatorics.SimpleGraph.Clique in a PR.

[Kevin Buzzard]

Does this person not have a Zulip account?

[ooovi]

Kevin Buzzard said:

Does this person not have a Zulip account?

Hello, I now do have a Zulip account. I'd like to work with @Christoph Spiegel on trying to address the two TODOs in Combinatorics.SimpleGraph.Clique in a PR.

[Patrick Luo]

Hi, I'm interested in adding toric varieties to Lean eventually and was wondering if I could get github permission? My username is m3hgu5t4

[Yury G. Kudryashov]

Could you please add your github name to your Zulip profile?

[Kevin Buzzard]

(that comment applies to both of the people requesting access; we're hoping to encourage this behaviour from now on)

[Tristan Figueroa-Reid]

Hi! I'd like to request write access for a non-master branch. My GitHub username is LeoDog896. I would like to work on formalizing the surreal numbers and some proofs from Combinatorial Game Theory.

[Kevin Buzzard]

@Tristan Figueroa-Reid invite sent!

[ooovi]

Hi, my github name is now added to my Zulip profile. Sorry for having missed the wish to do that when reading the contributors guideline. Could I obtain permission now?

[Patrick Luo]

I have also added it; it didn't seem to be possible on the mobile app earlier.

[Rick de Wolf]

Hi! I would like to get write access for non-master branches - my Github handle is RickDW. My interests lie in probability theory, information theory, and random graphs and I would like to work on those topics.

[Kim Morrison]

@ooovi, @Patrick Luo , @Rick de Wolf, you should all find invitations in your email inboxes now!

[Rick de Wolf]

Thank you!

[Daniel Morrison]

Hi, I'd like access to work on adding the Hodge star operator. My GitHub is morrison-daniel.

[Kim Morrison]

@Daniel Morrison, please check your email inbox for an invite.

[Daniel Morrison]

Thank you!

[Jason Gross]

Can someone start the CI on #18263 and/or give me write access to non-main branches? (My GitHub username is JasonGross, I'm a Coq dev who's worked with Lean only a little bit. I don't currently have plans for other formalizations to add to mathlib, but might acquire them in the future.)

[Julian Berman]

(I did the first part, but somewhat unsurprisingly it immediately failed given Mathlib doesn't really use a forking model, so we'll have to wait for an actual maintainer to grant access)

[Patrick Massot]

@Jason Gross you have an invitation. Please read https://leanprover-community.github.io/contribute/index.html about our weird workflow.

[Alex Mobius]

WRT https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60Finmap.60.20.60GetElem.3F.60.20instance.3F - my GitHub handle is @ElectronicRU, I am planning to add a typeclass instance and some supporting lemmas by way of analogue with e.g. HashMap, if maintainers feel there's need to do so.

[Kim Morrison]

I'll reply on the other thread.

[Oliver Bøving]

Hey! I've made infinite/tsum/ENNReal versions of Finset.sum_biUnion that I'd like to upsteam to mathlib. I've got the changes on a personal fork, but I'd like open a PR. Should I do so from a mathlib branch or from my own? In the first case may I have access? I'm oeb25 on GitHub :)

[Kim Morrison]

@Oliver Bøving, would you mind also adding your github handle to your zulip profile? This is helpful for reviewers.

[Kim Morrison]

I've sent an invitation now.

[Johannes Choo]

Hi there, I'd like write access for non-master branches. My name is jhanschoo. I'd like to refactor https://github.com/jhanschoo/mathlib4/blob/master/Mathlib/Computability/TuringMachine.lean as a preliminary to formalizing computational complexity results. At the moment it uses some deprecated lemmas and is too long; some part of the development can be broken out. Thanks!

[Kim Morrison]

@Johannes Choo, could you please add your github handle to your zulip profile?

[Kim Morrison]

Please check your email inbox for an invitation.

[Johannes Choo]

Got it, did it, thanks!

[Guo Zixun]

Hello! My GitHub handle is yhtq, and I have made some refinement about IsFractionRing and IsGalois as well as added some tiny definition and lemmas to transfer an algebra to another ring with a ring equiv. Could I ask for write permission?

[Kevin Buzzard]

Invitation sent!

[Kevin Buzzard]

(@Guo Zixun )

[Guo Zixun]

@Kevin Buzzard Thanks!

[Tobias Leichtfried]

Hi! I would like to request write permission for a non-master branch. I have some definitions and theorems about leftmost derivations in context free grammars. My Github username is TobiasLeichtfried.

[Kim Morrison]

@Tobias Leichtfried, please check you email for the invitation!

[Tobias Leichtfried]

Thank you!

[Tomaz Mascarenhas]

Hi! My Github handle is tomaz1502. Could I ask for write permission? I did some work about formalizing runtime complexity of sorting algorithms (a long time ago). I did some PRs through my fork but I guess I should have done it through a branch: https://github.com/leanprover-community/mathlib4/pull/15449#issuecomment-2451507054

[Kim Morrison]

@Tomaz Gomes, pleases check you email inbox for the invitation!

[Tomaz Mascarenhas]

thanks!

[Zhu]

Hi! My GitHub username is hehepig166.
I'd like to request write permission for a non-master branch to contribute some definitions and theorems on Lucas's theorem.
Additionally, I found a todo related to the conditions for equality in the AM-GM inequality during a formalization that requires this result, and I'd be happy to work on it as well.
I'm also currently exploring the formalization of Lovasz Local Lemma, with hopes of potentially adding it to mathlib in the future.

[Kevin Buzzard]

@Zhu , invitation sent!

[Zhu]

Thank you!

[Jakob Stiefel]

Hi! I would like to request write permission for a non-master branch to contribute some results on characteristic functions of finite measures. My Github username is JakobStiefel.

[Kim Morrison]

@Jakob Stiefel, please check your email inbox for the invitation.

[Jakob Stiefel]

thanks!

[Joris Roos]

Hi! Could I have write access to non-master branches? My github username is roos-j. I'm interested in formalizing analysis or working towards making it easier to formalize analysis. I recently formalized some Fourier analysis on Boolean functions, https://github.com/roos-j/lean-booleanfun

[Kim Morrison]

@Joris Roos, please check your email inbox for the invitation.

[Joris Roos]

Thanks!

[Tian Chen]

Hi! I'd like to add a result about the determinant of reflection (and other miscellaneous things). My github username is peakpoint

[Kim Morrison]

@Tian Chen, please check your email inbox for the invitation.

[Nick Ward]

Hi, all. I am working on a proof that the nerve of a category is a quasicategory. My github username is @gio256. Could a kind maintainer please create a branch for me?

[Kim Morrison]

@Nick Ward, please check your email inbox for the invitation.

[Nick Ward]

@Kim Morrison thank you!

[metakuntyyy]

Also, I'd like to request write access to mathlib4 repo. Per the contributing guidelines I'd like to add some documentation. My github handle is metakunt

[Óscar Álvarez]

Hi, could I get write access to the mathlib4 repository? I’d like to contribute to some results on Coxeter groups (Zulip thread). My GitHub username is bolito2. Thanks!

[Kim Morrison]

metakuntyyy said:

Also, I'd like to request write access to mathlib4 repo. Per the contributing guidelines I'd like to add some documentation. My github handle is metakunt

@metakuntyyy, could you please add your github handle to your zulip profile?

[Kim Morrison]

Óscar Álvarez said:

Hi, could I get write access to the mathlib4 repository? I’d like to contribute to some results on Coxeter groups (Zulip thread). My GitHub username is bolito2. Thanks!

@Óscar Álvarez, please check your email inbox for the invitation.

[metakuntyyy]

@Kim Morrison Should work now

[Kim Morrison]

@metakuntyyy, please check your email inbox for the invitation.

[Kim Morrison]

@metakuntyyy, note also that we recommend (but do not require) that people who want to contribute to Mathlib do so with an identifiable real-world name on their Zulip and/or Github account.

[Justus Springer]

Hello, may I get write access to the mathlib4 repo? I was a contributor for mathlib3 in 2021 but never worked with mathlib4 before. I'm trying to get back into lean now, possibly attempting to define toric varieties. My github username is justus-springer.

[Matthew Ballard]

@Justus Springer Sent! Welcome back :)

[Justus Springer]

thanks!

[Óscar Álvarez]

@Kim Morrison Thanks!

[Byung-Hak Hwang]

Hi! I'm working on a project for formalizing the decomposition theorem of regular matroids. I'd like to ask for write access to non-master branches. My GitHub username is ByungHakHwang.

[Kim Morrison]

@Byung-Hak Hwang, please check your email for an invitation.

[Byung-Hak Hwang]

Thank you!

[William Coram]

Hi all. I am working on defining Newton polygons, as well as a few other projects needed for my goal (for my PhD) of formalising results about slopes of compact Hecke operators. Could I get write access to the mathlib4 repo, please. My github username is WilliamCoram

[Kevin Buzzard]

@William Coram invitation sent!

[Mitchell Horner]

Hi hi, re: #graph theory > Erdős-Stone-Simonovits. Could I get write access to create my own branch. :grinning_face_with_smiling_eyes:

My GitHub username is mitchell-horner.

[Vasily Ilin]

Hi. We have proven some lemmas about moment generating functions -- mgf of iid random variables, and mgf of a gaussian. I would like to make a PR to mathlib. Can I get write access? Here is the first lemma I want to add: https://github.com/Vilin97/central_limit_theorem/blob/master/CentralLimitTheorem/main.lean#L72
My Github username is Vilin97

[Rémy Degenne]

Invite sent @Vasily Ilin

[Rémy Degenne]

and also @Mitchell Horner

[Kim Morrison]

@Vasily Ilin, would you mind adding your Github username to your user profile? (This is something we trying to ask of everyone asking for write access.)

[Vasily Ilin]

@Kim Morrison , Do you mean here on Zulip? If so, I did it now!

[Vasily Ilin]

I did my best to follow the PR guide. Since this is my first PR, can someone experienced tell me if I missed anything? https://github.com/leanprover-community/mathlib4/pull/19798

[Alex Loitzl 🐓]

Alex Loitzl 🐓 said:

Hi,
I'd like to request write access for a non-master branch. My Github username is AlexLoitzl. I'm working on formalizing the pumping lemma for CFG here, with help from Martin Dvořák .

I think I never got an invite :/
I finished Chomsky Normal Form Translation and would like to open a PR for that

[Matthew Ballard]

@Alex Loitzl 🐓 Done! Welcome.

[Nir Paz]

Not sure where else to ask this, can I get permission to push to branches on the vscode extension github?

[Julian Berman]

It's just Mathlib that's weird, the vscode extension is a normal Git(Hub) repo which you can contribute to by forking it

[Mehmet Emre]

Hi, I am working on formalizing computability and automata-related stuff. I want to add these formalizations of regular language closure properties. Can I get write access to non-master branches? My GitHub username is maemre

[言绎心]

Hello, I try to add a lemma in mathlib4, here is my pr: https://github.com/leanprover-community/mathlib4/pull/20158
Could I get write access?
Github User Name: Yan-Zero
https://github.com/Yan-Zero

[Kevin Buzzard]

@言绎心 can you add your github username to your Zulip account profile? We like that people do this before we give them access, as it helps us keep track.

@Mehmet Emre invitation sent!

[mars0i]

Hi, I'd like write access to mathlib. Currently I have a PR to ProofWidgets4. Mathlib compiles on my computer with this change, but I'm doing further testing for which it would be helpful to use the mathlib CI. (Discussion in this thread.)

Question: What I'd like to do is to submit a mathlib branch that (temporarily) refers to my clone of ProofWidgets4, before the PR has been accepted into ProofWidgets4. Would that be OK? It would make it easier to test my modified ProofWidgets4 as a dependency in my own project. I'd prefer to do that before the PR is accepted, even though testing within ProofWidgets4 has been successful.

Thanks!

[Kevin Buzzard]

@mars0i invite sent!

[言绎心]

Kevin Buzzard said:

言绎心 can you add your github username to your Zulip account profile? We like that people do this before we give them access, as it helps us keep track.

Mehmet Emre invitation sent!

Okay, I have done.

[Zhang Qinchuan]

Hello, I want to add some lemmas to mathlib4 (for example : Vieta's formula for quadratic equation).
May I have write access? My github user name is zqc17.

[Tanner Duve]

Hi, I am working on a project involving oracle computability and Turing degrees. I have some work ready to be pushed with the initial definitions and some basic facts and have a lot of stuff in progress. Could I be granted write access? My GitHub username is tannerduve.

[Ilmārs Cīrulis]

Hello, I want to do PR that fixes tiny typo in Combinatorics/SimpleGraph/Maps.lean (in the documentation).

My Github username is LessnessRandomness

[Sidharth Hariharan]

Hi, I was wondering if I could get write access to non-master branches of Mathlib4. I'm working on the sphere packing project and there are several little facts we've proved along the way that it might be good to have in the library. Eg. most recently, I proved that n.divisors can have cardinality at most n. My GitHub username is thefundamentaltheor3m. Thank you

[Kevin Buzzard]

@Tanner Duve @Sidharth Hariharan invitations sent!

@Lessness the maintainers are currently fretting over the idea of a growing number of serious contributors having anonymous usernames. Using reals names is the norm in free software development. Can we persuade you to start using your full real name on this forum? Note that we're not saying "if you don't do this, you can't have access", we're just saying "we'd very much like it if you used your full real name". This is all part of a more general issue which we are going to have to start discussing at some point.

[Ilmārs Cīrulis]

Done. This is my real name.

[Ilmārs Cīrulis]

part of a more general issue

With me? :sweat_smile: :melting_face: Or just something more general related to anonymous usernames or something like that?

[言绎心]

Kevin Buzzard said:

言绎心 can you add your github username to your Zulip account profile? We like that people do this before we give them access, as it helps us keep track.

Mehmet Emre invitation sent!

I don't think I've received the invitation yet. Did you forget to send it?

[Tanner Duve]

thanks!

[Patrick Massot]

Ilmārs Cīrulis said:

part of a more general issue

With me? :sweat_smile: :melting_face: Or just something more general related to anonymous usernames or something like that?

I’m pretty sure Kevin means a general issue with anonymous users, not with you.

[Patrick Massot]

And thanks for changing your username!

[Sidharth Hariharan]

Kevin Buzzard said:

Tanner Duve Sidharth Hariharan invitations sent!

Thank you!

[Zhang Qinchuan]

hilbert said:

Hello, I want to add some lemmas to mathlib4 (for example : Vieta's formula for quadratic equation).
May I have write access? My github user name is zqc17.

Hello, May I have write access? My github user name is zqc17.

Or what should I do to meet the requirement?

[Kevin Buzzard]

It would be great if you could change your username here to your full real name, like most of the contributors to mathlib.

[Zhang Qinchuan]

Kevin Buzzard said:

It would be great if you could change your username here to your full real name, like most of the contributors to mathlib.

Done. I have change my username to my full real name.

[Kevin Buzzard]

Many thanks! Invitatio sent @Zhang Qinchuan !

[Ilmārs Cīrulis]

Hello again! :)
Did I miss the invitation? Or I must do something more?

[Kevin Buzzard]

Apologies @Ilmārs Cīrulis ! Invitation sent!

[Li Xuanji]

Hi, I would like github permission to open a PR to extend DihedralGroup.r_one_pow from k : ℕ to k : ℤ

[Oliver Nash]

@Li Xuanji Invite sent!

[Oliver Nash]

Based on a quick look, it seems to me that we should keep the version using (k : ℕ) and add another version saying:

theorem r_one_zpow (z : ℤ) : (r 1 : DihedralGroup n) ^ z = r z := by
   sorry -- your proof

[Joe Stubbs]

Hi, I'm working with @Walter Moreira on formalizing some facts about Euclidean numbers (we posed about this in #new members > Formalizing Special Numbers from Concrete Mathematics ). We'd like github permission to push to non-master branches. My github username is joestubbs and Walter's is waltermoreira. Thanks in advance!

[Kim Morrison]

@Joe Stubbs, @Walter Moreira, you should find invitations in your (email) inbox!

[Anthony DeRossi]

Hi. I recently completed a formalization of Thompson's method for constructing nondeterministic finite automata from regular expressions. I think some/all of this work might be worth contributing. Could I have write access on GitHub to send a few PRs? My username is anthonyde.

[Kevin Buzzard]

@Anthony DeRossi invitation sent!

[Anthony DeRossi]

Thanks!

[Parth Shastri]

May I have write access? I want to push to branches used by the lean4 PR CI.

[Kevin Buzzard]

I'm a bit confused here. Are you looking to push to mathlib or to lean 4? For Lean 4 people make PRs from forks (after having gone through an RFC).

[Parth Shastri]

I have already made the PRs to lean4, and I want to push to the lean-pr-testing-XXXX branches of mathlib4 (that were automatically created) in order for me to fix the build failures.

[Kevin Buzzard]

Thanks for the explanation, and thanks for offering to fix the branches too! Invitation sent.

[Lenny Taelman]

Hi. Can I get write access to mathlib4? I would want to try turn the tactic tauto_set implemented here into a PR.

[Kevin Buzzard]

@Lenny Taelman invitation sent!

[Wang Jingting]

Hi. I'm working with @Xuchun Li to port one of Andrew Yang's repository in lean3 to lean4 with the aid of some automated tools. (@Christian Merten has discussed with him about it and got his approval). Can we get the access to open a branch on mathlib4? My github account is xyzw12345 and his is Xuchun-Li. Thanks!

[Ching-Tsun Chou]

It was suggested that my proof of the non measurability of the Vitali set be added to mathlib4/Counterexamples:
#maths > The nonmeasurability of the Vitali set
May I ask for write-access to non-master branches of mathlib4 so that I can make a PR for it? Thanks in advance!

[Anatole Dedecker]

@Ching-Tsun Chou Invitation sent!

[Ching-Tsun Chou]

Thanks! I've accepted the invite.

[Kevin Buzzard]

@Wang Jingting and @Xuchun Li invitations sent!

[Wang Jingting]

Thanks! We've received and accepted the invitation!

[Michał Staromiejski]

Hi, I'm quite new here, I'm a software engineer (for living) and a hobby mathematician. As a hobby project I formalized my PhD results (math part, as my PhD was Computer Science/Algebra combo), here is the repo with my code: https://github.com/mistarro/local-rings.
I've proven some common facts in (commutative) algebra that I could not find in Mathlib4 and I thought it would be a good idea to contribute those to the library. They are in LocalRings/Utils subdirectory of my project. If you find my own results interesting enough for Mathlib4, I could of course contribute them as well :smile:.
I'd like to ask for write permission to non-master branches to create PRs. My github user name is mistarro (as you might have inferred from the links above). Thanks!

[Johan Commelin]

@Michał Staromiejski voila: https://github.com/leanprover-community/mathlib4/invitations

[Yi.Yuan]

Hello!
I'm working on a Project mainly about Filtered Rings. Could I get writing permissions (on non-main branches) of the mathlib4 repo? My github name is yuanyi-350. thank you very much

[Johan Commelin]

@Yi.Yuan It seems you already have write permission :smiley:

[Bryan Gin-ge Chen]

Don't forget to add your github username to your Zulip profile!

[Yi.Yuan]

Thank you for the reminder.

[Lian Tattersall]

Hi, last year I was working with @John Talbot on a project formalising the Andrasfai-Erdos-Sos theorem (https://github.com/jt496/AESBrandt). Could I get write access to mathlib4 for non main branches?

[Wang Jingting]

Wang Jingting said:

Hi. I'm working with Xuchun Li to port one of Andrew Yang's repository in lean3 to lean4 with the aid of some automated tools. (Christian Merten has discussed with him about it and got his approval). Can we get the access to open a branch on mathlib4? My github account is xyzw12345 and his is Xuchun-Li. Thanks!

Now @张守信(Shouxin Zhang) will also be joining us, so can he get an access to write on the branches we've opened as well? His github account is ShouxinZhang. Thanks!

[Yunkai Zhang]

Hi! I'd like to make a PR for  mathlib #20878 and get write permission for a port error. My GitHub username is YunkaiZhang233 Thanks!

[Johan Commelin]

@Wang Jingting @Yunkai Zhang voila: https://github.com/leanprover-community/mathlib4/invitations

[Laurance Lau]

Hello, my name is Laurance and my Github handle is LLaurance. I seem to have found typos in Mathlib.Algebra.BigOperators.Fin.lean on lines 58 and 67 where it should say "sum" instead of "product". May I have the necessary permissions to write this change somewhere? Thanks.

[Kevin Buzzard]

@Lian Tattersall nice to meet you on Friday and sorry your request fell through the cracks! You should have an invite.

[Kevin Buzzard]

@张守信(Shouxin Zhang) can you add your github account name to your Zulip profile?

[Kevin Buzzard]

@Laurance Lau invitation sent!

[Lian Tattersall]

thanks!

[Sorrachai Yingchareonthawornchai]

Hi, my Github is sorrachai. Could I ask for write permission? Yael and I have started a formalizing project on forbidden 0-1 matrix theory . Some famous theorems have been formalized, such as Marcus-Tardos Theorem.

[Kevin Buzzard]

Can you put your github in your Zulip profile?

[Sorrachai Yingchareonthawornchai]

Yes, I have added github in my Zulip profile.

[Kim Morrison]

@Sorrachai Yingchareonthawornchai, please check your email inbox for the invitation.

[Sorrachai Yingchareonthawornchai]

Thank you!

[Park Sanghyeok]

Hi. My Github ID is sksgurdldi. Could I ask for write permission? I would like to work on some lemmas.

[Kim Morrison]

@Nausicaa:

• We strongly recommend, but don't require, that users asking for write access use their real name on the Zulip.
• Could you say more about which lemmas you intend to work on?

[Park Sanghyeok]

• I changed my name.:blush:
• I'm working on Buchberger's criteria. Before that, I would like to first post a lemma that shows the relationship between List.zipwith and finset.sum.

[Kim Morrison]

@Park Sanghyeok, please check you email inbox for the Github invitation.

[Park Sanghyeok]

@Kim Morrison Thank you!

[Rudy Peterson]

Hello,

My name is Rudy Peterson, and I am working furthering the Formal Language Theory libraries in Mathlib4. I will be working on implementing and verifying transformations for finite state machines, regular languages, context free languages, and potentially writing the foundations for weighted languages. I may also work on a weighted version of the Myhill-Nerode theorem.

Would it be possible for me to get write access to non-master branches of Mathlib4? My github is rudynicolop.

Thank you!

[Kim Morrison]

@Rudy Peterson, please check you email inbox for the invitation from Github.

[Yiming Fu]

Hello, my partner @Dai Zhixuan and I would like to add some elementary facts about homogeneous relations and homogeneous ideals to mathlib4. Could we please get access to a non-master branch on mathlib4? His github username is atstarrysky and mine is pelicanhere. Thanks!

[Kim Morrison]

Welcome! Please both check your (email) inboxes for the invitations.

[Yiming Fu]

@Kim Morrison Thanks!

[Rudy Peterson]

@Kim Morrison Thank you!

[Samy Avrillon]

Hello
I'm currently writing on an implementation of Hyperdoctrines in Category Theory, as defined here.
May i have access to a private branch on the Mathlib repository to publish my changes and later make a PR ?
My Github username is MysaaJava
Thank you !

[Janos Wolosz]

Hi,

I am currently working on defining Lie algebra nilradicals within the framework of the Lean project:
https://github.com/orgs/leanprover-community/projects/17

I would like to request write access to the mathlib4 repository so that I can push my local branch to the remote and share my progress with @Oliver Nash. I plan to name my feature branch: janos-wolosz/lie-algebra-nilradical.

A bit about my background: I hold a PhD in Mathematics from Eötvös Loránd University, where I specialized in representation theory and group theory. I have also worked as a C++ developer. I would be happy to gain experience and contribute to mathlib! :)

My github username: jano-wol

[Kevin Buzzard]

@Samy Avrillon you might want to discuss in #mathlib4 with some people about whether we want this stuff in mathlib (we might, I'm not competent to judge, but I looked at the paper and was scared off by the non-classical logic; mathlib is pretty much a classical library). @Janos Wolosz invitation sent!

[Stefan Hetzl]

Hello! I would like to request write access to non-master branches of mathlib. A student of mine, @Tobias Leichtfried , has formalised some results in automata theory, specifically that pushdown automata are equivalent to context-free grammars. I would like to contribute them to mathlib. My github username is shetzl.

[Kim Morrison]

@Stefan Hetzl, please check your (email) inbox for the invitation.

[Stefan Hetzl]

@Kim Morrison Thank you!

[Yacine Benmeuraiem]

Hello, I have formalized Tannaka duality for finite groups and I'm looking to implement it in mathlib. May I have write access to non-master branches of mathlib? My github username is ybenmeur. Thanks!

[Devon Tuma]

Hello, I have not made contributions since mathlib3 but would like to start porting some parts of the program verification work I've done since then. My github username is dtumad if I could get access to push new branches, thanks.

[Kim Morrison]

@Devon Tuma, could you please add you Github username to your Zulip profile?

[Devon Tuma]

Done

[Kim Morrison]

@Yacine Benmeuraiem, please check you (email) inbox for the invitation.

[Kim Morrison]

@Devon Tuma, similarly!

[Markus de Medeiros]

Hey! I have a small PR to make to mathlib about the monoidal product in the Giry monad. Could I be given access to the non-baster branches of mathlib? Username markusdemedeiros

[Kim Morrison]

@Markus de Medeiros, please check your (email) inbox for the invitation.

[Markus de Medeiros]

@Kim Morrison Got it, thanks : )

[Joseph Rotella]

Hi! I'm trying to push a fix to a PR-testing branch in the mathlib repo for some changes I've PRed to Lean core but realized that I don't have write access to that branch. Could I be given the appropriate access to do so? My GitHub username is jrr6.

[Markus Himmel]

@Joseph Rotella Done.

[Kevin Buzzard]

Heh, I wondered why it said "has a pending invitation to this repository" :-)

[Joseph Rotella]

Thank you!

[Ruben Van de Velde]

@Joseph Rotella please add your github username to your zulip profile as well

[Pablo Donato]

Hi! I have formalized subobject classifiers in CategoryTheory.Subobject.Classifier together with their representability theorem, for now in a separate repo. I would like to get push access to a new branch in order to start a PR very soon. My GitHub username is Champitoad.

[Patrick Massot]

You should have an invitation

[Pablo Donato]

Yes I have accepted the invitation, thank you!

[Vlad Tsyrklevich]

I'd like to request GitHub permission as I'm starting to generate some preliminary results for auto-generalizing type classes that I'd like to benchmark in a draft PR. My username is in my profile

[Albus Dompeldorius]

Hi, I would like to request write access to non-master branches of mathlib. I have made a small contribution that I'd like to merge. My github username is adompeldorius.

[Kevin Buzzard]

@Vlad Tsyrklevich and @Albus Dompeldorius invitations sent! @Albus Dompeldorius I guess I would personally prefer it if contributors to mathlib used their full real names on the Lean Zulip (as many of us do).

[Aaron Liu]

Hi, I would like to ask for write access to non-master branches of mathlib. I found a lemma with a typeclass assumption that could be generalized (docs#OnePoint.instNormalSpaceOfLocallyCompactSpaceOfR1Space).

[Bryan Gin-ge Chen]

Invite sent! https://github.com/leanprover-community/mathlib4/invitations

[Michał Mrugała]

Hi, we have a PRs with some simple lemmas from the #toric project (https://github.com/YaelDillies/Toric/tree/master/Toric/Mathlib). Could I get write access to contribute them? My github username is Kiolt.

[Kevin Buzzard]

Hi Michal! Invitation sent!

[Zichen Wang]

Hi,

Here's Wang Zichen.

I am currently seeking permission to create a new branch where we can contribute our formalized codes to Mathlib. I would also like to make PRs.

My Github username: imathwy

I have worked on formalizing the intrinsic interior, closure, and related properties of convex sets in a normed vector space, focusing on interactions with affine spans, closures, and intersections. I have proved several results, including that the intrinsic interior and closure of a convex set exhibit specific relationships with topological properties and affine spans.

The PR #22312 prove the following theorems:

theorem openSegment_sub_intrinsicInterior {s : Set V} (hsc : Convex 𝕜 s) {x y : V}
    (hx : x ∈ intrinsicInterior 𝕜 s) (hy : y ∈ intrinsicClosure 𝕜 s) :
    openSegment 𝕜 x y ⊆ intrinsicInterior 𝕜 s

theorem convex_intrinsicInterior (hsc : Convex 𝕜 s) :
    Convex 𝕜 (intrinsicInterior 𝕜 s)

theorem convex_intrinsicClosure (hsc : Convex 𝕜 s) :
    Convex 𝕜 (intrinsicClosure 𝕜 s)

theorem affinespan_intrinsicInterior [FiniteDimensional ℝ V] (hsc : Convex ℝ s) :
  affineSpan ℝ (intrinsicInterior ℝ s) = affineSpan ℝ s

theorem intrinsicInterior_intrinsicInterior [FiniteDimensional ℝ V] (hsc : Convex ℝ s) :
    intrinsicInterior ℝ (intrinsicInterior ℝ s) = intrinsicInterior ℝ s

theorem intrinsicInterior_iff
    {z : V} (hs : Convex ℝ s)(hn : (intrinsicInterior ℝ s).Nonempty) :
    z ∈ intrinsicInterior ℝ s ↔ ∀ x ∈ s, ∃ μ > (1 : ℝ), (1 - μ) • x + μ • z ∈ s

theorem intrinsicInterior_intrinsicClosure (h : Convex ℝ s) (hc : (intrinsicInterior ℝ s).Nonempty):
    intrinsicInterior ℝ (intrinsicClosure ℝ s) = intrinsicInterior ℝ s

theorem intrinsicClosure_intrinsicInterior (h : Convex 𝕜 s)
      (hc : (intrinsicInterior 𝕜 s).Nonempty) :
    intrinsicClosure 𝕜 (intrinsicInterior 𝕜 s) = intrinsicClosure 𝕜 s

theorem intrinsicInterior_tfae [FiniteDimensional ℝ V] (hs : Convex ℝ s) {t} (ht : Convex ℝ t) :
  [closure s = closure t, intrinsicInterior ℝ s = intrinsicInterior ℝ t,
  intrinsicInterior ℝ s ⊆ t ∧ t ⊆ closure s].TFAE

theorem iIntersection_closure_eq_intrinsicInterior_closure
    (h : ∀ (i : ι), Convex ℝ (s i))
    (hinter : ∃ x, ∀ i, x ∈ intrinsicInterior ℝ (s i)) :
    ⋂ i, closure (s i) = closure (⋂ i, s i)

theorem iIntersection_intrinsicInterior_eq_intrinsicInterior_iIntersection [Finite ι]
    (h : ∀ (i : ι), Convex ℝ (s i))
    (hinter : ⋂ i, (intrinsicInterior ℝ (s i)) ≠ ∅):
    ⋂ i, intrinsicInterior ℝ (s i) = intrinsicInterior ℝ (⋂ i, s i)

[Kim Morrison]

@PrinChern, please add your github username to your zulip profile.

[Kim Morrison]

(Optionally, but preferably, we suggest that users committing to Mathlib use their real names as the Zulip names.)

[Zichen Wang]

OK. I have modified.

[Kim Morrison]

@Zichen Wang, it looks like someone else has already given you access. Please check your email inbox for the invitation.

[Kim Morrison]

(Reminder to other maintainers, it's nice to post something when you've given access, both as a record, as a reply to the requester, and to avoid other maintainers duplicating work.)

[Damiano Testa]

According to this page it should be possible to trigger actions when giving access. This could be hooked into the zulip reaction bot: should we try it?

[Kim Morrison]

I think doing this manually is fine: it's more welcoming to new users.

[Qi Wen Wei]

Hey, I'm a second year student at Uoft and saw that there was a TODO on /Data/Nat/Factorization/Basic for the following:
"-- TODO: Port lemmas from Data/Nat/Multiplicity to here, re-written in terms of factorization"

I've forked the mathlib4 repo and made the changes for that TODO. You can check it out here.

I would like to request write access to non-master branches of mathlib so that I can contribute to the open source mathlib.

Also, I'm quite new to this so I'm not sure about the style of code I should be writing (comments, setting deprecated and so on). Is there anyone who can help me clean up the code?

[Kevin Buzzard]

This looks nice! I am not sure that people will like the large import increase, maybe it should go in its own file in Data/Nat/Factorization rather than just being added to Basic. I sent you an invite -- check the email associated with your github account.

[Jovan Gerbscheid]

Hi, can I have write access to non-master branches of batteries? I need to fix some breakage in the testing branch of lean4#7301

[Kevin Buzzard]

I'm not sure if the batteries people are reading this thread. But looking at the PRs it seems that they use the usual github workflow, i.e. PRs from forks.

[Jovan Gerbscheid]

I need the write access to be able to fix the testing branch lean-pr-testing-7301. I'm not sure how else to make a mathlib branch for lean4#7301 with a working batteries.

[Johan Commelin]

cc @Kim Morrison @Matthew Ballard @François G. Dorais

[Markus Himmel]

You can open a PR against the testing branch from your Batteries fork. The Batteries maintainers are usually very responsive about merging these.

[Jovan Gerbscheid]

Sounds good: batteries#1154

[Kim Morrison]

'd

[Sabbir Rahman]

Hi, I'm Sabbir Rahman (github username: upobir). I am seeking permission to create a branch to add the lemma continuous_const_rpow which states {a : ℝ} (h: a ≠ 0) : Continuous fun x : ℝ ↦ a ^ x. There was a very minor discussion on #new members > proving 2^x is continous regarding it not being present. Wanted to make a contribution by adding the lemma.

[Kevin Buzzard]

Invitation sent!

[Huỳnh Trần Khanh]

hello I need access to get #general > cardinality of product of two sets into mathlib

[Huỳnh Trần Khanh]

my username is huynhtrankhanh

[Huỳnh Trần Khanh]

I am working on an internal project and I will need to add lemmas to mathlib quite often

[Huỳnh Trần Khanh]

to avoid duplicate work

[Ruben Van de Velde]

Please add your github username to your zulip profile

[Huỳnh Trần Khanh]

done

[Kim Morrison]

@Huỳnh Trần Khanh please check your email inbox for the invitation.

[Joshua Render]

Hi, my name is Joshua Render (github JoshJRJ) and I am a masters student working on automated theorem proving in LEAN for a group project.
You may have seen someone else within our group discussing our definitions for Berge's Theorem, and I would like access to a non-master branch so we could start submitting some of our definitions and early lemmas for approval.
Thank you in advance!

[David Ledvinka]

Hello, I am a PhD student at Uoft and would like to contribute to probability theory in LEAN. In particular I would like to add a theorem which says that the law of the (monoid) product of independent monoid valued random variables is given by the convolution of the laws. My github handle is: DavidLedvinka.

[Matteo Cipollina]

Hi, my background is in mathematical logic and philosophy of science (with minors in math and physics). I'm working on a few projects and would like to start following best practices and try to PR to Mathlib, bit by bit, some (possibly) useful stuff on Probability Theory, Distributions and Set theory. If possible I would like to have access to a non-master branch. My github is or4nge19. Thanks!

[Kevin Buzzard]

I love how people who go to universities beginning with T assume that there's only one university in the world which begins with T :-) I've seen this a bit for other letters, but with T it seems weirdly common.

I've sent invites to all three of you; please check your email for the invitation.

[Kim Morrison]

Oh, and by the way, it is "Lean", not "LEAN". :-)

[Bernardo Anibal Subercaseaux Roa]

Hi! I'm a PhD student at Carnegie Mellon University, trying to formalize some of my papers in discrete mathematics. Doing so I've come across a bunch of little humble lemmas missing that I'd like to contribute. My github handle is bsubercaseaux :) Thanks!

[Ruben Van de Velde]

Please add your github username to your zulip profile as well

[Kim Morrison]

@Bernardo Anibal Subercaseaux Roa, please check your email inbox for the invite.

[Kim Morrison]

(and don't forget to ask your question from office hours about the Subgraph issue in the #graph theory channel!)

[Loïc Simon]

Dear all,

I would like to make a contribution to mathlib. Could I get write access with the following github account : https://github.com/DrLSimon

Any advice on common pitfalls in the PR process is welcome.

Best regards,
Loïc

[Kim Morrison]

@Loïc Simon, could you please say briefly what you would like to contribute?

[Kim Morrison]

Please see https://leanprover-community.github.io/contribute/index.html for advice about making a PR.

[Loïc Simon]

I'm an associate professor in CS/Stats, and I've develop a small contribution that links the sub of two positive measures to the Jordan decomposition of the sub of the associated signed measure.

[Bryan Gin-ge Chen]

@Loïc Simon Invite sent! https://github.com/leanprover-community/mathlib4/invitations

Please also remember to add your github username to your Zulip profile, as mentioned in the instructions that Kim linked.

[Loïc Simon]

thanks

[Kiril Vinogradov]

Hello, I'm a University of Leeds student doing an undergrad project on Lean. As part of it, I would like to add a contribution I've created for the SimpleGraph folder of applying the bypass definition in showcasing the fact that every circuit contains a cycle and having this transformation defined in Path.lean, my Github account is: https://github.com/kirilvino
Thank you in advance for any response!

[Markus Himmel]

@Kiril Vinogradov I sent you an invitation.

[Robin Arnez]

Hello, I have a PR for lean (lean#7499) and I'd want to push fixes to the corresponding mathlib testing branch.

[Markus Himmel]

@Robin Arnez I sent you an invitation.

[Hanliu Jiang]

my name is HanLiu Jiang ,my Github name is SEU-Prime , i work my project in BICMR with Shanwen Wang to Formalization p-adic L function,thanks you in advance

[Riccardo Brasca]

Invitation sent!

[Bryan Gin-ge Chen]

@prime Could you please add your github username to your Zulip profile per https://leanprover-community.github.io/contribute/index.html ? Thank you!

[Maja Kądziołka]

Hi, I'd like to expand overview.yaml for the Computability development and improve its docs somewhat, can I have repo access?

[Kevin Buzzard]

prime said:

my name is HanLiu Jiang ,my Github name is SEU-Prime , i work my project in BICMR with Shanwen Wang to Formalization p-adic L function,thanks you in advance

We also prefer that contributors to mathlib use their real name for their Zulip acount.

[Kevin Buzzard]

@Maja Kądziołka invitation sent!

[Kim Morrison]

@Riccardo Brasca, just pinging you to make sure you saw these follow up requests -- best to do these prior to sending the invitation. :-)

[VTrelat]

Hi, my name is Vincent Trélat (git: VTrelat) and I have extended the ZFC set theory theories from Mathlib (on ZFSet) for my PhD. I have defined naturals, integers and rationals in this setting, along with many theorems on them. As it is starting to grow quite quickly, I thought it would be a good idea to include it in Mathlib. Is it possible to get write access? The files need some cleaning to get along with the recommended style, but I should be able to do that quickly.

[Ruben Van de Velde]

Hi Vincent, welcome! I guess we'll need to see if there's a maintainer who can commit to reviewing the code; I'm not sure anyone has shown much interest in zfset recently

[Bhavik Mehta]

Ruben is completely right: putting these things into mathlib could be a slow process.
My advice is to make your repository public (and perform your cleanups there), then gradually start upstreaming to mathlib. In this way, you can check for yourself that the definitions and lemmas that you're making in ZFSet are the right ones in practice, and maintainers can see the ways in which you're using them. (The PR process is usually smoother if you can explicitly demonstrate what the new things are for!). Plus, this means that others can contribute to your code!

[Moisés Herradón Cueto]

Hi, I'm Moisés, and I work at the Autonomous University of Madrid. I'm trying to learn by contributing to the toric varieties project. I'm Moises-Herradon-Cueto on github.

[Yaël Dillies]

(can confirm, Moisés did some good stuff and we want it in mathlib!)

[Bryan Gin-ge Chen]

Invite sent! https://github.com/leanprover-community/mathlib4/invitations

[Moisés Herradón Cueto]

<3

[William Swartworth]

Hi, I'm William (github wswartworth) and I'm postdoc at CMU. While it's not my main research, recently I've been particularly excited about the interaction between machine learning and interactive theorem proving. I'd also like to get some experience programming by hand in Lean by contributing to Mathlib.

I thought that a good start might be to try adding some basic eigenvalue inequalities to the linear algebra library (e.g. Courant-Fischer and interlacing) since they seem to be missing. As a first step, I filled in a TODO in Analysis.InnerProductSpace.Spectrum so that the the eigenvalues (and eigenvectors) are sorted in increasing order. This builds correctly, but I'd be interested in getting feedback on stylistic correctness. I wasn't sure if it's best to ask here first, or to just create a pull request. Thanks!

[Michael Rothgang]

Usually, I would say "create a pull request" --- as github's tooling makes it much easier to review your code and provide suggestions on how to improve it. So asking here looks like the right move!

[Huỳnh Trần Khanh]

is getting write access to non master branches no longer required to make pull requests anymore

[Ruben Van de Velde]

No, it is still required

[Kevin Buzzard]

@William Swartworth invitation sent!

[Yunge Yu]

Hi, I'm Yunge (GitHub: xcloudyunx), and a student at the University of Auckland. I'm exploring, learning (and hopefully will be contributing to) the SimpleGraph library.

[Matthew Jasper]

Hi, I'm Matthew, (GitHub: matthewjasper). I've been recently contributing to FLT and I will be contributing some results from there and maybe some related algebra results that aren't directly needed by FLT.

[Kevin Buzzard]

@Yunge Yu can you add your github username to your Zulip account?

[Kevin Buzzard]

@Matthew Jasper invitation sent!

[Yunge Yu]

done

[Kevin Buzzard]

@Yunge Yu invitation sent!

[VTrelat]

Bhavik Mehta said:

Ruben is completely right: putting these things into mathlib could be a slow process.
My advice is to make your repository public (and perform your cleanups there), then gradually start upstreaming to mathlib. In this way, you can check for yourself that the definitions and lemmas that you're making in ZFSet are the right ones in practice, and maintainers can see the ways in which you're using them. (The PR process is usually smoother if you can explicitly demonstrate what the new things are for!). Plus, this means that others can contribute to your code!

Hey! Thanks a lot for the advice, I have started the process and have done my first PR. Although it is blocked for the moment since I don't have write access, I will carry on gradually pushing my changes.

[Igor Shimanogov]

Good day! I would like to get an invitation.
I plan to start contributing with a theorem on list commutativity #new members > Need help proving termination!
Looking forward to contribute some theorems about (Countable) Boolean Algebras: mostly interested in proving Vaught criterion of Countable BAs isomorphism and Stone duality.

[Chu Zheng]

Hi, my name is Chu Zheng. I'm currently working on formalizing some IMO geometry problems in Lean 4, and I would like to contribute some missing theorems in Euclidean geometry, such as triangle metrics. My GitHub username is zcyemi. Thanks~

[Michael Rothgang]

Just in case you don't know: @Joseph Myers has thought a lot about how to formalise Euclidean geometry best; it would be useful to discuss the formalisation strategy with them.

[Notification Bot]

Yury G. Kudryashov has marked this topic as resolved.

[Alok Singh]

i would like to formalize the hypernatural numbers of nonstandard analysis, canI have permission? my gh username is alok.

[Notification Bot]

Yury G. Kudryashov has marked this topic as unresolved.

[Sehun Kim]

Hello. My name is Sehun Kim(Github: sehun1024) from Seoul university. I want to contribute Jordan Curve Theorem and other related things in homology theory and category theory. Could you invite me to make a new branch and a pull request?

[Floris van Doorn]

@Igor Shimanogov @Chu Zheng @Alok Singh @Sehun Kim invite sent!

[Floris van Doorn]

(Github changed the interface for adding people to an organization. It now displays only their real name and not their username, which makes it significantly more annoying to pick the right person to invite </rant>)

[Floris van Doorn]

@VTrelat invite sent as well (sorry for the delay).

Please post here again if you requested access but haven't gotten a response yet.

[Bryan Gin-ge Chen]

@Sehun Kim Please remember to add your github username to your Zulip profile! Thanks!

[Yijun Yuan]

Hi, my name is Yijun Yuan (GitHub ID: YijunYuan). Currently, I'm a PhD student at Yau Mathematical Science Center, Tsinghua University. I want to contribute some results related to Cohen-Macaulay rings. Thank you.

[Riccardo Brasca]

You should have an invitation!

[William Du]

Hi, my name is William Du (Github: w1lldu). I'm an undergrad at Northeastern University, looking to contribute some theorems on measure algebras. Thanks.

[Ruben Van de Velde]

Please add your GitHub user name to your zulip profile

[William Du]

done