Starting with Mathlib

Stream: new members

[Janos Wolosz]

Hi,

I have learned the basics of Lean (I worked through The Mechanics of Proof) and have an overview of the process for contributing to mathlib (installing the Lean project, opening a PR on GitHub, etc.).

I think the next step for me would be to contribute to an ongoing project. Can you recommend one, where a beginner could be helpful? As a first step, I would feel more comfortable working on a topic related to discrete structures (combinatorics, finite group theory, etc.).

To be honest, whenever I look at some proofs in mathlib, I feel humbled by how complex the whole library is, but I hope I can get used to it.

[Kevin Buzzard]

The proofs in mathlib are not really written to be readable by the beginner for the most part. It doesn't have to be like this, for example in the module topology file I've been writing normal proofs in comments amongst the lean proofs and nobody's objected. But this is not the norm. The trick with reading the maths library is not to read the proofs but just to read and understand the statements of the theorems, probably in most cases the proof is "this follows without too much trouble from what has already been proved" and unfortunately this sometimes turns into "...and so let's see if we can smoosh the entire argument together into under two lines".