Contributing to Mathlib

Stream: new members

[Pietro Lavino]

Hello I am undergrad student in mathematics and this summer (4 months) I will be working on lean 4 and my professor set as a goal to formalize the point wise ergodic theorem. I was wondering what the process of contributing to Mathlib looks like and where can I find the group of people that are working on this formalization if there are any. I was also wondering if formalizing such a result as an undergrad is feasible.

[Kevin Buzzard]

I would start by not worrying about PRing to mathlib and just trying to get going with your project using mathlib. If and when you get stuck, ask questions in this stream and you'll probably get answers. You don't have to worry about what's feasible, the important thing is to have a goal. You'll find out soon enough what's feasible :-)

[Filippo A. E. Nuccio]

Pietro Lavino said:

Hello I am undergrad student in mathematics and this summer (4 months) I will be working on lean 4 and my professor set as a goal to formalize the point wise ergodic theorem. I was wondering what the process of contributing to Mathlib looks like and where can I find the group of people that are working on this formalization if there are any. I was also wondering if formalizing such a result as an undergrad is feasible.

ping @Sébastien Gouëzel and @Marco Lenci

[Marco Lenci]

Hello Pietro, a group of us (@Marcello Seri @Oliver Butterley and I) have been working on and off on Birkhoff’s Ergodic Theorem for the past few months (the last few of which have honestly been “off”), initially spurred by @Sébastien Gouëzel. Other people have recently contacted us about the same project and have done quite a lot of work. I’m not tagging them here, as I’m on my phone and busy doing out-of-the-office things. But I’m sure @Oliver Butterley will do that and fill the gap as to what the state of the art is… Thanks Oliver! :smile:

[Kevin Buzzard]

This conversation might want to move to a new thread in e.g. #mathlib4

[Lua Viana Reis]

I recently finished (as in sorry-free) a proof of pointwise Birkhoff (see https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Summer.20project.3A.20dynamics.20and.20ergodic.20theory), but I think there is still a lot of work to make it into a form that can go to mathlib

[Lua Viana Reis]

The code is here:
https://github.com/lucasvreis/BirkhoffErgodicThm/

[Oliver Butterley]

Pietro Lavino said:

Hello I am undergrad student in mathematics and this summer (4 months) I will be working on lean 4 and my professor set as a goal to formalize the point wise ergodic theorem. I was wondering what the process of contributing to Mathlib looks like and where can I find the group of people that are working on this formalization if there are any. I was also wondering if formalizing such a result as an undergrad is feasible.

See also this discussion where some others have mentioned dynamics related stuff that they have done.

I'm always keen on better coordinating our efforts but it's a bit unclear the best way.

[Shanghe Chen]

Hi some codes about mathlib possibly may be discussed better in GitHub with PR like https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/unitor.20for.20product.20of.20categories.3F If possible please grant me (github username: onriv ) the push access to non-master branch. Thank you very much!

[Kevin Buzzard]

@Shanghe Chen invitation sent!

[Shanghe Chen]

I get it now! Thank you very much!