Zulip Chat Archive

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 (Dec 13 2022 at 20:33):

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 (Dec 13 2022 at 21:01):

Thanks! :)

Alex Keizer (Dec 14 2022 at 09:25):

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

Johan Commelin (Dec 14 2022 at 09:27):

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

Anand Rao (Dec 16 2022 at 04:34):

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 (Dec 16 2022 at 06:55):

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

Shreyas Srinivas (Dec 16 2022 at 12:02):

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 (Dec 16 2022 at 12:04):

@maintainers

Johan Commelin (Dec 16 2022 at 12:15):

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

Shreyas Srinivas (Dec 16 2022 at 13:58):

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 (Dec 16 2022 at 14:09):

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

Siddhartha Gadgil (Dec 16 2022 at 14:09):

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 (Dec 16 2022 at 14:11):

Aaah, good point!

Johan Commelin (Dec 16 2022 at 14:12):

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

Shreyas Srinivas (Dec 16 2022 at 14:14):

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 (Dec 16 2022 at 15:09):

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 (Dec 17 2022 at 01:45):

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

Lukas Miaskiwskyi (Dec 22 2022 at 13:17):

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

Riccardo Brasca (Dec 22 2022 at 13:24):

Invitation sent!

Henrik Böving (Dec 24 2022 at 13:19):

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 (Dec 24 2022 at 13:24):

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

Pol'tta / Miyahara Kō (Feb 02 2023 at 05:48):

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

Johan Commelin (Feb 02 2023 at 06:24):

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

Utku Okur (Feb 28 2023 at 20:47):

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 (Mar 01 2023 at 00:15):

invite sent

Bulhwi Cha (Mar 12 2023 at 05:19):

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

Kevin Buzzard (Mar 12 2023 at 09:46):

@maintainers

Johan Commelin (Mar 13 2023 at 04:59):

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

MonadMaverick (Mar 29 2023 at 09:29):

Could I have the permission?

I'm going to focus on measure_theory.

My github username is MonadMaverick.

Thank you in advance.

Scott Morrison (Mar 29 2023 at 09:32):

Invite sent!

Timothy Gu (Apr 24 2023 at 07:33):

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 (Apr 24 2023 at 08:32):

@maintainers

Anne Baanen (Apr 24 2023 at 08:33):

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

Anne Baanen (Apr 24 2023 at 08:33):

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

Jujian Zhang (Apr 28 2023 at 11:26):

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

Anne Baanen (Apr 28 2023 at 11:27):

Invite sent!

Jujian Zhang (Apr 28 2023 at 11:27):

Thanks!

Yuma Mizuno (May 13 2023 at 05:17):

@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 (May 13 2023 at 07:02):

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

Apurva Nakade (May 13 2023 at 19:14):

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

Johan Commelin (May 13 2023 at 19:55):

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

Nikolas Kuhn (May 15 2023 at 18:03):

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

Kevin Buzzard (May 15 2023 at 18:21):

@maintainers

Scott Morrison (May 15 2023 at 21:06):

@Nikolas Kuhn, invite sent.

Kalle Kytölä (Jun 25 2023 at 13:59):

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

Johan Commelin (Jun 25 2023 at 14:49):

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

Timo Carlin-Burns (Jul 01 2023 at 02:36):

@maintainers requesting mathlib4 push access for timotree3

Johan Commelin (Jul 01 2023 at 09:09):

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

François G. Dorais (Jul 11 2023 at 20:00):

@maintainers requesting mathlib4 push access for fgdorais.

Scott Morrison (Jul 11 2023 at 22:09):

@François G. Dorais, invite sent.

Bernhard Reinke (Jul 12 2023 at 11:16):

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

Anne Baanen (Jul 12 2023 at 11:16):

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

Aaron Bies (Jul 19 2023 at 11:32):

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 (Jul 19 2023 at 11:33):

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 (Jul 19 2023 at 11:36):

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

Riccardo Brasca (Jul 19 2023 at 11:43):

Invitation sent!

Kevin Buzzard (Jul 19 2023 at 11:58):

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 (Jul 19 2023 at 12:16):

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

Kevin Buzzard (Jul 19 2023 at 12:25):

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

Alex J. Best (Jul 19 2023 at 15:49):

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

Julian Berman (Jul 22 2023 at 17:46):

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

Johan Commelin (Jul 23 2023 at 06:48):

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

FMLJohn (Jul 24 2023 at 20:36):

@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 (Jul 24 2023 at 20:44):

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

FMLJohn (Jul 24 2023 at 20:48):

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 (Jul 24 2023 at 20:50):

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

FMLJohn (Jul 24 2023 at 21:12):

Thank you very much!

Jonas van der Schaaf (Jul 25 2023 at 19:22):

@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 (Jul 25 2023 at 19:28):

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 (Jul 25 2023 at 19:30):

Invite sent

Jonas van der Schaaf (Jul 25 2023 at 19:42):

Thank you!

Ashvni Narayanan (Jul 26 2023 at 14:40):

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

Anne Baanen (Jul 26 2023 at 14:52):

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

Ashvni Narayanan (Jul 26 2023 at 14:55):

Thank you!

Kaiyu Yang (Aug 10 2023 at 17:33):

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 (Aug 10 2023 at 17:47):

Invite sent!

Eric Wieser (Aug 10 2023 at 17:48):

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

Isaac Hernando (Aug 10 2023 at 20:22):

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 (Aug 11 2023 at 00:18):

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

Coleton Kotch (Aug 13 2023 at 21:46):

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

Jireh Loreaux (Aug 13 2023 at 21:51):

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

Koundinya Vajjha (Aug 30 2023 at 05:03):

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

Scott Morrison (Aug 30 2023 at 05:05):

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

Scott Carnahan (Aug 31 2023 at 17:44):

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

Patrick Massot (Aug 31 2023 at 17:54):

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

Johan Commelin (Aug 31 2023 at 17:57):

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

Johan Commelin (Aug 31 2023 at 17:58):

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

Scott Carnahan (Aug 31 2023 at 17:59):

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 (Aug 31 2023 at 18:29):

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

Patrick Massot (Aug 31 2023 at 18:30):

Done

Wen Yang (Sep 07 2023 at 10:53):

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 (Sep 07 2023 at 11:00):

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 (Sep 07 2023 at 11:04):

Please ping me when the PR is open :)

Anatole Dedecker (Sep 07 2023 at 11:08):

Invitations sent to both of you

Chenyi Li (Sep 07 2023 at 11:20):

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 (Sep 07 2023 at 11:30):

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 (Sep 07 2023 at 11:52):

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

Patrick Massot (Sep 07 2023 at 12:36):

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 (Sep 07 2023 at 15:00):

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 (Sep 07 2023 at 15:04):

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

Kevin Buzzard (Sep 07 2023 at 15:29):

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

Anatole Dedecker (Sep 07 2023 at 15:41):

Apparently not, I just did that.

Apurva Nakade (Sep 07 2023 at 21:25):

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 (Sep 07 2023 at 21:35):

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

Apurva Nakade (Sep 07 2023 at 21:36):

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

Apurva Nakade (Sep 07 2023 at 21:36):

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

Anatole Dedecker (Sep 07 2023 at 21:38):

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 (Sep 07 2023 at 21:39):

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 (Sep 08 2023 at 06:16):

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 (Sep 08 2023 at 07:24):

Invitation sent!

Michael Rothgang (Sep 09 2023 at 09:24):

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 (Sep 09 2023 at 09:56):

That's very cool! Invitation sent!

Richard Hill (Sep 16 2023 at 13:53):

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 (Sep 16 2023 at 14:03):

Invitation sent!

Sean Gonzales (Sep 18 2023 at 23:05):

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 (Sep 18 2023 at 23:46):

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

Chris Wong (Sep 24 2023 at 14:17):

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 (Sep 24 2023 at 14:32):

@maintainers

Patrick Massot (Sep 24 2023 at 14:35):

Done

Patrick Massot (Sep 24 2023 at 14:36):

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 (Sep 24 2023 at 14:39):

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 (Sep 24 2023 at 14:55):

Yes, wrapping an existing library would be fair game.

Chris Wong (Sep 24 2023 at 14:57):

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 (Sep 24 2023 at 15:01):

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 (Sep 25 2023 at 22:27):

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

Johan Commelin (Sep 26 2023 at 08:03):

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

Matthias U (Sep 26 2023 at 11:53):

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

Johan Commelin (Sep 26 2023 at 11:55):

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

Matthias U (Sep 26 2023 at 12:41):

@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 (Sep 26 2023 at 12:51):

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

Iván Renison (Oct 07 2023 at 11:17):

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 (Oct 07 2023 at 18:10):

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 (Oct 07 2023 at 18:14):

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

Robin Carlier (Oct 07 2023 at 18:14):

Great, thanks!

Andrew Yang (Oct 07 2023 at 18:21):

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 (Oct 07 2023 at 18:25):

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 (Oct 07 2023 at 18:30):

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 (Oct 10 2023 at 11:49):

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

Jujian Zhang (Oct 10 2023 at 11:51):

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

Jujian Zhang (Oct 10 2023 at 11:53):

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 (Oct 10 2023 at 11:54):

docs#TensorProduct.AlgebraTensorModule

Jujian Zhang (Oct 10 2023 at 11:54):

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

Julian Külshammer (Oct 10 2023 at 12:49):

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 (Oct 10 2023 at 13:02):

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 (Oct 18 2023 at 13:06):

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 (Oct 18 2023 at 13:07):

@maintainers

Floris van Doorn (Oct 18 2023 at 13:10):

invite sent!

Gareth Ma (Oct 18 2023 at 13:10):

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 (Oct 18 2023 at 13:11):

invite sent!

Gareth Ma (Oct 18 2023 at 13:11):

Thanks!

Daniel Lambert (Oct 18 2023 at 13:13):

Thanks!

Utensil Song (Oct 21 2023 at 09:59):

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 (Oct 21 2023 at 11:06):

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

Utensil Song (Oct 21 2023 at 11:08):

Thanks!

Eric Wieser (Oct 28 2023 at 05:41):

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 (Oct 29 2023 at 16:27):

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 (Oct 29 2023 at 16:29):

@maintainers

Oliver Nash (Oct 29 2023 at 17:04):

Invite sent

Thomas Zhu (Oct 29 2023 at 17:29):

Thank you!

Miguel Marco (Oct 29 2023 at 19:51):

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 (Oct 29 2023 at 20:12):

My github username is miguelmarco

Rob Lewis (Oct 29 2023 at 23:31):

Miguel Marco said:

My github username is miguelmarco

Invite sent!

Claus Clausen (Nov 03 2023 at 17:59):

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 (Nov 03 2023 at 18:01):

Done

Timo Carlin-Burns (Nov 03 2023 at 18:54):

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 (Nov 03 2023 at 18:54):

GitHub seems to be struggling a lot currently.

Patrick Massot (Nov 03 2023 at 18:55):

It has nothing specific to Mathlib.

Anatole Dedecker (Nov 03 2023 at 20:21):

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

Patrick Massot (Nov 03 2023 at 21:28):

Probability

Jannis Limperg (Nov 04 2023 at 09:38):

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

Johan Commelin (Nov 04 2023 at 09:45):

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

Jannis Limperg (Nov 04 2023 at 10:07):

Thanks!

Scott Morrison (Nov 04 2023 at 11:13):

@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 (Nov 04 2023 at 12:54):

Ah great, thank you very much!

Xavier Généreux (Nov 04 2023 at 13:40):

Johan Commelin said:

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

Thanks!

Xavier Xarles (Nov 17 2023 at 10:05):

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

Ruben Van de Velde (Nov 17 2023 at 10:08):

Xavier Xarles said:

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

Anything in particular you're working on?

Xavier Xarles (Nov 17 2023 at 10:13):

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 (Nov 17 2023 at 10:15):

Invitation sent!

Riccardo Brasca (Nov 17 2023 at 10:16):

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

Xavier Xarles (Nov 17 2023 at 13:09):

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 (Nov 19 2023 at 04:30):

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 (Nov 19 2023 at 04:34):

GitHub claims there is no such username.

Jeremy Toh (Nov 19 2023 at 04:46):

ah it's deepimpactmir oops for typo

Patrick Massot (Nov 19 2023 at 04:48):

This time it worked!

Jeremy Toh (Nov 19 2023 at 04:50):

thank you!

Adrian Wüthrich (Nov 19 2023 at 16:32):

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 (Nov 20 2023 at 00:25):

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

Adrian Wüthrich (Nov 20 2023 at 09:57):

Thanks!

Hunter Monroe (Nov 22 2023 at 02:10):

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

Scott Morrison (Nov 22 2023 at 05:03):

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

Ali Ramsey (Nov 23 2023 at 23:00):

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 (Nov 24 2023 at 00:04):

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

Ali Ramsey (Nov 24 2023 at 00:18):

Thank you!

Qi Ge (Nov 27 2023 at 16:10):

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

Scott Morrison (Nov 28 2023 at 03:44):

@Qi Ge, invitation sent!

Dan Velleman (Dec 04 2023 at 21:57):

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 (Dec 05 2023 at 01:14):

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

Johan Commelin (Dec 05 2023 at 06:38):

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

Dan Velleman (Dec 05 2023 at 12:07):

Thank you!

Ira Fesefeldt (Dec 08 2023 at 08:04):

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 (Dec 08 2023 at 16:12):

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

Anne Baanen (Dec 08 2023 at 16:13):

@Ira Fesefeldt

Fernando Chu (Dec 09 2023 at 03:01):

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 (Dec 09 2023 at 05:02):

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

Fernando Chu (Dec 09 2023 at 12:52):

Thanks!

Yongyi Chen (Dec 13 2023 at 19:53):

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

Johan Commelin (Dec 13 2023 at 21:37):

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

Josha Dekker (Dec 16 2023 at 13:10):

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 (Dec 16 2023 at 13:12):

You should probably talk to @Jason KY.!

Josha Dekker (Dec 16 2023 at 14:35):

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 (Dec 16 2023 at 14:42):

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

Last updated: Dec 20 2023 at 11:08 UTC