Mathlib proofs?

Stream: new members

[Joseph O]

Why are the mathlib proofs so golfed? Shouldn’t they be readable for people who want to learn from them

[Julian Berman]

glossary#golfing has the rationale I perceived (or was told).

[Julian Berman]

Essentially people care more about statements than proofs often. When the proof is mechanical or uninteresting -- in the sense that it's felt there isn't much to learn mathematically from understanding the proof -- then the shorter the better.

[Julian Berman]

(That being said though I think for more interesting proofs there indeed is a hope or feeling that mathlib could have a bit more commenting and exposition than it does today).

[Joseph O]

I guess that is reasonable

[Yaël Dillies]

There's much distinction between API proofs, and actual theorems. A way to think of it is that compressing the trivial makes what's not stand out.

[Yaël Dillies]

Golfed proofs are also usually easier to maintain, because they have less moving parts and tend to compile quicker (so they are less prone to time out).

[Eric Wieser]

You can also learn a lot by reading a golfed proof too; usually less mathematics and more about how to do golfling

[Jireh Loreaux]

Golfing has an additional benefit (frequently, not always) of showing you how things are less complicated than you were making them. (Maybe this is what Eric was saying, I'm not quite sure)

[Kyle Miller]

You can also usually ungolf a golfed proof to see how it works. Luckily they tend to just be compressed and optimized rather than truly code golfed (which tends result in highly obfuscated code -- take a look at https://codegolf.stackexchange.com/).

[Filippo A. E. Nuccio]

I still second @Joseph O 's remark: sometimes proofs in mathlib looks too golfed to me. Once one knows how to de-golf a proof, this is more or less fine, but I believe this is hard for beginners, who can easily be discouraged by condensed way these proofs are stored in mathlib. I am thinking of taking an easy lemma that one wishes to adapt to another setting by saying "oh, let me see if I can mimik the proof". I was very upset with this at the beginning and I am still not convinced by maximising golfing.

[Filippo A. E. Nuccio]

The idea stated here is really to make code as short as possible (sic!) and this might be too short, but that is clearly a matter of personal taste.

[Arthur Paulino]

I am skeptical about golfing improving speed. Sometimes it's evident but very often it's about making more use of syntactic sugar and Lean's type inference powers, which is potentially slower, I believe

[Eric Wieser]

Often "golfing" is used to mean "convert tactic proofs to term proofs", which probably can improve speeds - especially if the tactic proof use simp when the term proof is just foo.trans bar

[Julian Berman]

Filippo A. E. Nuccio said:

The idea stated here is really to make code as short as possible (sic!) and this might be too short, but that is clearly a matter of personal taste.

I quoted the "general" (non-lean specific) definition more or less from the first sentence of https://en.wikipedia.org/wiki/Code_golf:

Code golf is a type of recreational computer programming competition in which participants strive to achieve the shortest possible source code that solves a certain problem.

Of course happy to tweak the language there if you think it's too harsh, but personally I fully agree with your point that balance is needed between "as short as possible" and "as short as both possible and a good idea via some subjective collective wisdom". E.g. no one I think would say it is a good idea for mathlib to use 1 letter variable names everywhere just because it'd golf some proofs shorter.