how to get to committing

Stream: new members

[Andrea Bourque]

This is broad, vague, and possibly unanswerable, but how does one get to the point of being able to formalize new things and commit to mathlib? Note that not asking how to commit, but how to get the skills and knowledge to write commitable code.

[Patrick Massot]

This is usually a three steps process. First learn the basics, for instance working through #mil. Then discuss a suitable project, write code and open a pull-request. Then go through the review process without getting discouraged, and trying to learn.

[Riccardo Brasca]

I agree. At the beginning don't worry about mathlib, just prove something, and then learn the mathlib way.

[Andrea Bourque]

I somehow wasn't aware of mil. I just finished doing the natural number game (for the second time; I did it a while back and forgot it all), and did some of the follow up challenges. I'll work through that to get an understanding and post back to discuss working on something (I want to work on some of the representation theory that hasn't been done, according to the undergrad todo list)

[Winston Yin (尹維晨)]

For representation theory, there’s docs#Action, but it’s written in category theory language.

[Andrea Bourque]

As it should be

[Winston Yin (尹維晨)]

Challenge: if you didn't learn representation theory from a categorical PoV, find Schur's lemma in Mathlib.

[Winston Yin (尹維晨)]

I played with Lean on/off for over a year before I submitted a proper PR that was merged. I started with #tpil, which gave me a good idea of type theory. Then, I set some realistic goals like "formalise the statement of this theorem in Lean" or "write a definition and prove basic facts about it". By working through them, I learned what's in the library and the standard proof style in Lean. They are probably not going to be PR-ready, but they should prepare you for your first project in Lean.

[Shreyas Srinivas]

There was a short window of time early this year when one could get code in by porting mathlib from lean 3 to lean 4. That was my entry point. In programming we often say that it is important to read code that other people have written. This is definitely true for lean. So once you feel comfortable I would also suggest stepping through some mathlib proofs with your cursor in a local copy.