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!

[dave de Sa]

Hi everyone! I'm a software engineer with a background in data science and ML, and I'm excited to contribute to mathlib4.
I've been looking at the undergrad_todo list and I'm particularly interested in working on analysis and Distribution Theory topics. I'm planning to start small to learn the ropes before tackling anything substantial.
Longer term, I'm interested in adding integral transform functionality since I noticed it's on the wishlist and there don't seem to be any active PRs for it. Any advice for a first-time contributor would be appreciated!

[Kenny Lau]

make use of loogle a lot, and statements/definitions are harder to get right than proofs, so make use of the existing 7000 files in mathlib to find the best way to phrase something, and start small, say try to prove that derivative of x^3 is 3x^2 by yourself using as few (high-level) tactics as possible

[Luigi Massacci]

For distributions, note that @Anatole Dedecker, @Moritz Doll and I have a lot of open PRs, the list is not super up to date. You are of course very welcome to contribute : )

[Moritz Doll]

I am hiking in the Rockies until the 12th, so I have very limited time to think about easy problems, but if I remember correctly we still don't have the Gaussian as a Schwartz function (calculating its Fourier transform should be implicit in the inversion theorem). Also if you want very easy ways of contributing: for the functions of temperate growth, we are missing that they are closed under all the algebraic operations (I have a PR for multiplication, but add, sub and neg are missing)

[dave de Sa]

Thanks all... I started poking around. I'll take a look at the open PRs and reach out with any questions... Thanks- I'm grateful for the guidance, and happy to help out.