Looking for theorems to contribute to Mathlib

Stream: new members

[Kamila Szewczyk]

Hi, I was looking for some theorems the proofs of which I could contribute to mathlib4. To clarify, I am not very good at various abstract branches of mathematics; I take more interest in numerical analysis, real analysis and some information theory. Any chance someone would have pointers/suggestions for what I could contribute and where would I begin?

[Julian Berman]

I think the usual advice that experts here give is to pick some attainable (or even slightly beyond attainable) project for something that you know well, try to formalize it, and if you run into missing things, to contribute those.

Another avenue is the undergraduates file (https://github.com/leanprover-community/mathlib4/blob/master/docs/undergrad.yaml) where wherever you see an empty string there may be something at the undergraduate mathematics level which is missing (though sometimes the file isn't fully up to date so it's best to ask when you see something specific you're interested in).

And a third possibility is someone who knows the fields you mentioned to drive by with specific recommendations. And just because I see it, I think some work on information theory was being done in the #Polynomial Freiman-Ruzsa conjecture stream where there was a need for some results on entropy -- I only followed from afar, and am definitely not an expert myself, not to mention that I think the definitions are being done in quite abstract / generalized ways -- but maybe that's yet another thing you might find yourself interested in.

[Julian Berman]

(Also welcome!)