# Zulip Chat Archive

## Stream: new members

### Topic: willing to contribute

#### fzyzcjy (Aug 30 2023 at 07:39):

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 (Aug 30 2023 at 08:03):

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

#### fzyzcjy (Aug 30 2023 at 08:05):

Sure!

#### Yaël Dillies (Aug 30 2023 at 08:07):

Yaël ∉ all :upside_down:

#### fzyzcjy (Aug 30 2023 at 09:48):

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

#### Yaël Dillies (Aug 30 2023 at 09:49):

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

#### fzyzcjy (Aug 30 2023 at 09:49):

Oh I see

#### Martin Dvořák (Aug 30 2023 at 09:51):

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

#### fzyzcjy (Aug 30 2023 at 09:51):

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

#### Moritz Doll (Aug 31 2023 at 10:17):

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 (Aug 31 2023 at 11:01):

@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 (Aug 31 2023 at 12:31):

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 (Aug 31 2023 at 14:08):

I see, thank you!

Last updated: Dec 20 2023 at 11:08 UTC