IMO 2021 Q1

Stream: new members

[Mantas Baksys]

Hello all! As a small project, I have formalised the solution to IMO 2021 Q1. Here is the code for the solution : https://gist.github.com/MantasBaksys/5db553021d417b62f33a8c821581498f. Would this be worth PR'ing? For context, I have never contributed to mathlib and I'm sure my code can be significantly improved :smiley:

[Eric Rodriguez]

Do you have the mathlib access? Regardless, yes — we usually store IMO problems in the "archive" section. I'll definitely give it a bigger review then, but it's worth cleaning up a little before PRing — stuff in archive tends to be "as well documented and clear as possible".

Some of the things that jump out at me right now is that mathlib style doesn't give either of { } their own lines, and uses a bit more indentation; and also I'd encourage it to give more detail about what your solution actually does!

[Eric Rodriguez]

oh, and another thing - usally operators in mathlib are typset with spaces around them consistently, so instead of (43*x)+123/3, we'd tend to write (43 * x) + 123 / 3. (even powers!)

[Eric Rodriguez]

oh, and instead lemma blah : ∀ (n : ℤ) (hn : p n), asdf, we'd also tend to write lemma blah (n : ℤ) (hn : p n) : asdf; these should keep you busy whilst maintainers give you PR access

[Eric Rodriguez]

instead of using split so much, you could also consider tactic#refine and anonymous constructors (the ⟨⟩ things you may have seen)

[Mantas Baksys]

Thanks for your reply @Eric Rodriguez. I do not have mathlib access yet and my Github username is MantasBaksys. I will keep busy improving my code, as you have suggested in the meantime :smiley:.

[Bryan Gin-ge Chen]

(I've just sent you an invite: https://github.com/leanprover-community/mathlib/invitations )

[Mantas Baksys]

Thanks for the invite, I have accepted it and was trying to make my first PR, following the steps in this video : https://www.youtube.com/watch?v=Bnc8w9lxe8A&ab_channel=leanprovercommunity. However, after pushing, the pop-up window crashed and calling git push again results in nothing. Is there a manual way to authenticate Github? Sorry if this is very dumb, I'm very new to Github :smiley:.

[Kevin Buzzard]

I can't help with your git issues, I usually use it from the command line. But here's a golf of your first lemma:

lemma lower_bound (n : ℕ) (l : ℤ) (hl : 2 * (l : ℝ) ≥ 2 + sqrt (4 + 2 * n)) :
  (n : ℤ) + 4 * l ≤ 2 * l * l :=
begin
  have h₁ : sqrt (4 + 2 * n) ≤ 2 * l - 2 := by linarith,
  replace h₁ := (sqrt_le_iff.1 h₁).2,
  norm_cast at h₁, push_cast at h₁,
  linarith,
end