Contribute to Mathlib4

Stream: mathlib4

[Chenyi Li]

Hello! I may wonder how we can contribute to Mathlib4. I am currently working on some topics in convex ananlysis and convex optimization. We are working on formalizing some properties related to the properties of the convex functions and the convergence rate of some classical optimization methods. How should we organize our code so that it meets the relevant requirements of mathlib？How do we upload our written code？Can there be some documentation written with relative requirements? Thank you very much for answering!

[Anatole Dedecker]

Hi! You should have a look at the whole "Contributing" section of https://leanprover-community.github.io/index.html
Unfortunately most of the information there is still about Lean3, and I’m not sure we have it updated for Lean4 anywhere, so you’ll have to adapt it a bit based on existing Mathlib4 code.