elegance of proofs and contributing to mathlib

Stream: mathlib4

[Pietro Lavino]

I am working as a summer project with my supervisor to formalize some results with intention of them (hopefully) being included in mathlib eventually. Although I have been progressing and completing some of the proofs, I find that a lot of them are clunky and could most probably be done in a shorter and more elegant way. I was wondering how important the optimization of a proof is relevant when being considered for contribution? or if the proof is completed the job can be considered done?

[Kevin Buzzard]

The fact that #queue has size 200 is plenty of evidence that just completing the proof is a long way from the job being done, when it comes to getting PRs merged into mathlib.

[Damiano Testa]

My advice would be to focus on your project first, making sure that you formalize some proof. The process of contributing to mathlib is, in my opinion, an extra layer of complication that may very well be bigger (and almost certainly) longer than the scope of the summer project.

[Kim Morrison]

Don't worry too much about "elegance" to begin with. Splitting things up into small lemmas (hopefully "natural" ones) goes a very long way to solving this problem.

[Michael Rothgang]

Let me add: the way I learned a lot about writing more concise or elegant proofs was by submitting pull requests to mathlib and learning from the review feedback. For merging code into mathlib, it should be reasonably concise - but this process can also happen during code review.