Zulip Chat Archive

Stream: new members

Topic: Mathlib proofs?

Joseph O (Apr 29 2022 at 18:39):

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

Julian Berman (Apr 29 2022 at 18:40):

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

Julian Berman (Apr 29 2022 at 18:40):

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 (Apr 29 2022 at 18:41):

(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 (Apr 29 2022 at 18:42):

I guess that is reasonable

Yaël Dillies (Apr 29 2022 at 18:47):

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 (Apr 29 2022 at 18:48):

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 (Apr 29 2022 at 19:40):

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

Jireh Loreaux (Apr 29 2022 at 20:14):

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 (Apr 29 2022 at 20:29):

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 (Apr 30 2022 at 13:14):

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 (Apr 30 2022 at 13:16):

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 (Apr 30 2022 at 14:25):

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 (Apr 30 2022 at 15:48):

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 (Apr 30 2022 at 18:01):

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.

Last updated: Dec 20 2023 at 11:08 UTC