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.

[guiwan]

I am trying to configure mathlib according to the official tutorial. When I proceed to the following operation in VScode：

Run cd mathematics_in_lean
Run lake exe cache get

It always shows that :

fatal: unable to read tree (984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb)
error: external command 'git' exited with code 128

I have tried reinstalling git, but it still doesn't work.

[Julian Berman]

That sounds like somehow your cloned repository is corrupt. Assuming you haven't done any work in that directory, delete mathematics_in_lean, reclone it, and then let us know what you see from running that command.

[guiwan]

Julian Berman said:

That sounds like somehow your cloned repository is corrupt. Assuming you haven't done any work in that directory, delete mathematics_in_lean, reclone it, and then let us know what you see from running that command.

Thank you very much. The original error did not appear, but there is a new error. I will try to solve it first. Thank you again.

[Jafar Tanoukhi]

Hello I am currently in the process of learning about Lean4. I am interested in learning by attempting to contribute to mathlib as I get the impression that it is "friendly" to contribute to. Do you recommend a beginner like me to do so, and what if i'm not already well versed in a particular math topic (but open to learn about it while attempting an issue), would that be okay?

[Kim Morrison]

We'd love new contributors, but please be aware that it is quite challenging, and both some formalization experience and significant maths experience is helpful!

The best way to start is to post here (or in #**new members>) about your mathematical interests, and to try to identify something that you know well, but is not in Mathlib, but all of the prerequisites are already!

[Jafar Tanoukhi]

Hmmm, I am only recently getting into mathematically rigourous topics which I guess puts me at a big disadvantage here. I was hoping to maybe find a good first issue and then learn the math/formalization skills it would require as I go. From what you say though, that sounds far fetched maybe ?

[Weiyi Wang]

Maybe you can try what I did for my first contribution: create your own project on a topic you'd like to formalize without caring too much about mathlib contribution yet. During the formalization process, you will likely encounter small lemmas that feels "should be in mathlib but somehow not yet", that's what you can start creating PRs for. The first few could be just five lines, and that's good because you can get familiar with the review process easily with shorter ones.

[Jafar Tanoukhi]

That sounds awesome, thanks I will do so.