Zulip Chat Archive

Stream: maths

Topic: How is readability valued in the mathlib


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Oct 17 2020 at 10:30):

#naming

view this post on Zulip 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

view this post on Zulip Golol (Oct 17 2020 at 15:17):

Okay guys, thanks for the information!

view this post on Zulip Floris van Doorn (Oct 17 2020 at 17:17):

About readability: We try to make statements as readable as we can, but don't spend much efforts to make proofs readable.

view this post on Zulip Floris van Doorn (Oct 17 2020 at 17:18):

If you are struggling to understand the Lean definitions of concepts, your best bet is to read the documentation around it (module docs and doc strings). If they don't explain it well enough to you, please ask questions here, and once you understand what is going on, improve the doc strings!


Last updated: May 06 2021 at 17:38 UTC