## Stream: maths

### Topic: How is readability valued in the mathlib

#### Golol (Oct 17 2020 at 10:20):

I am not used to tactic style proofs yet and I am wondering if a tactic style or (detailed) term style proof is considered more readable for an experienced user.
Furthermore, are proofs in the mathlib supposed to be easily readable or instead short and concise?
I think I understand dependent type theory in lean well enough to get started soon but I am struggling to understand the fundamentals of topological or measure spaces for example, as they are implemeneted in the mathlib.
Do people just remember all these small lemmas? Do you only look for a lemma when you need one?
Thanks for the help.

#### Ruben Van de Velde (Oct 17 2020 at 10:27):

That's a lot of questions at once - I guess one first thing to note is that readability without the benefit of seeing the tactic state (as you get when looking at a proof in vscode or emacs) is not considered important, so don't assume you can learn much from just looking at the code

#### Ruben Van de Velde (Oct 17 2020 at 10:29):

For the small lemmas, the idea is that the naming convention should be consistent enough that you can (mostly) guess the name of the lemma you need, and autocompletion can do the rest if needed. If that doesn't work, library_search and suggest can (sometimes) find relevant lemmas

#naming

#### Kevin Buzzard (Oct 17 2020 at 10:47):

Many of the topological space lemmas have very short proofs using filters. I tend not to look at proofs, if I need a lemma I guess its name and then find it with ctrl-space autocompletion

#### Golol (Oct 17 2020 at 15:17):

Okay guys, thanks for the information!