willing to contribute

Stream: new members

[fzyzcjy]

Hi friends! I am interested in Lean, and want to contribute a little bit - as much as I can though I do not have a lot of time. I checked the doc (https://leanprover-community.github.io/contribute/index.html) but it does not seem to mention what proofs should one do. To be honest, I major in computer science, with interest in mathematics (only take a few math major courses though), so I am definitely not a mathematician. Is there any proofs that I can do? Thanks
(You can also find me on github https://github.com/fzyzcjy if I did not check zulip)

[Martin Dvořák]

Be careful; that webpage if written for Lean 3, which we all just abandoned.

[fzyzcjy]

Sure!

[Yaël Dillies]

Yaël ∉ all :upside_down:

[fzyzcjy]

@Yaël Dillies Sorry I do not quite get it...

[Yaël Dillies]

I just meant that not everyone has abandoned Lean 3, and I'm one of the people who hasn't.

[fzyzcjy]

Oh I see

[Martin Dvořák]

The main info for you is that Mathlib3 is dead. If you want to contribute to Mathlib, you need to use Lean 4.

[fzyzcjy]

I am learning lean4 currently (the grammar looks a bit more natural to me compared with lean3 the last time I learnt)

[Moritz Doll]

fzyzcjy said:

Hi friends! I am interested in Lean, and want to contribute a little bit - as much as I can though I do not have a lot of time. I checked the doc (https://leanprover-community.github.io/contribute/index.html) but it does not seem to mention what proofs should one do. To be honest, I major in computer science, with interest in mathematics (only take a few math major courses though), so I am definitely not a mathematician. Is there any proofs that I can do? Thanks
(You can also find me on github https://github.com/fzyzcjy if I did not check zulip)

The answer to your question depends on what you want to prove. We can then give you guidance on what in that direction is feasible and might help you understand mathlib more. Most people have learned first mathematics and then started formalizing what they knew for some time (that usually involves learning more mathematics, because formalization usually goes a different path than most math textbooks).

[fzyzcjy]

@Moritz Doll Thank you! Excluding the math courses for computer science (discrete math etc), the math major courses I have taken are abstract algebra and advanced linear algebra, but I plan to self-study more (maybe starting from basic real analysis?). So if it is suggested to formalize what I have learned, I guess I may only be able to work in these areas currently.

[Kyle Miller]

It's worth formalizing anything you find interesting, since what will inevitably happen is you'll find gaps in mathlib,and that'll give you things to contribute!

[fzyzcjy]

I see, thank you!