How to get involved

Stream: new members

[Linus Tang]

Hi! I'm Linus Tang, and I started learning Lean recently. I think formal proof languages are pretty cool from an aesthetics standpoint and might also unlock a new paradigm for machine learning.

I come from a math olympiad background, and I'm most interested in combinatorics and number theory. I'm working through the Mathematics in Lean tutorial, and I've learned chapters 1, 2, 3, 4, and 6 so far.

I'm trying to get an idea of what I can do to get more involved with the community (e.g. how to start contributing to Mathlib). I'm not set on any specific "path" yet; I just want to get a feel for what I can work on in the near future.

Any help would be appreciated!

[Niels Voss]

If you do plan on contributing to mathlib, I would recommend checking in here or in the "Is there Code for X" channel with your plan so that you don't accidentally duplicate existing work. I would also recommend getting your definitions checked by the community for generality, correctness, efficiency, and ease of use before starting the meat of your proof, because new members tend to struggle a lot with making good definitions.

[Michael Rothgang]

(... which is because making good definitions is not easy. In general, formalising definitions is much "harder"/the right way takes much longer to learn than for proving theorems.)

[Linus Tang]

Thanks for the tips!

[Mariano Suárez-Álvarez]

Is there a channel on which someone barely starting with lean could ask (probably silly) questions?

[Jovan Gerbscheid]

That would be here, in new members :smiley:

[Mariano Suárez-Álvarez]

kudos to whomever named the channel :-)

[Michael Rothgang]

Let me just emphasize: silly questions are also welcome there!

(Pedantic footnote: as long as you're asking in good faith... otherwise, that's just not nice to everybody else.)

[Linus Tang]

I have another question for anyone here:
What advice (e.g. recommended resources, learning strategies) would you give your past self to speed up the learning process?

[Ilmārs Cīrulis]

Get financially stable and mentally healthy as much as possible and then learn Lean/Mathlib (or anything else, for that matter), instead of trying to go the opposite way.

Well, at least that's advice for my past self. :sweat_smile:

[Weiyi Wang]

To myself: "you should have started this earlier when you had nothing to do"

[Ryan Smith]

Depending on your background, there is a very large community effort to formalize the proof of FLT.

[Linus Tang]

Weiyi Wang said:

To myself: "you should have started this earlier when you had nothing to do"

that's so real :sweat_smile:

[Linus Tang]

Ryan Smith said:

Depending on your background, there is a very large community effort to formalize the proof of FLT.

yes, I've heard of this effort
I don't have the background for this yet
(perhaps that will be slightly less true by the end of the year; I'm taking MIT's number theory class 18.785 this semester)

[Scott Carnahan]

To past self: Don’t give up on Lean for 3 years just because you got stuck on a level in Inequality World.

[Kevin Buzzard]

Some levels in inequality world are surprisingly hard! You're lucky you weren't there at the beta testing phase when <= was defined recursively and I was encouraging players to do induction on <= to solve the levels!

[Michael Rothgang]

Not necessarily to my past self:
Lean has an addicting quality. Take good care of yourself: take breaks, drink and eat enough. Enjoy other things in live :-) Take e.g. a walk regularly to get your mind off. In my experience, if a Lean proof is stubborn, walking away often solves it.

[Ansar Azhdarov]

There are Compfiles and Mathlib/Archive/Imo where you can contribute by formalizing math olympiad problems, since you have that background.