Proof of Project Euler 1 -- Feedback

Stream: new members

[Marcelo Fornet]

I recently started learning LEAN, by reading theorem proving in lean4 and playing the natural number games.

As an extra challenge, I took problem 1 from Project Euler, defined as close as possible to the problem statement, wrote a faster solution, and proved both of them are equivalent.

Here is the whole proof: https://github.com/mfornet/project-euler-lean/blob/main/ProjectEuler/P1.lean

This is the first code I write outside of a tutorial and I'd love to get some feedback about how could it be improved.

Some questions:

1. How do you decide between using theorem vs lemma vs inline lemma (i.e have h : ...)
2. Using exact? was helpful from time to time, but rw? or apply? was never helpful. Most of the time apply? would suggest theorems related to the bitwise representation of the integers. Is there anyway to make those more helpful.
3. If I want to share this with colleagues, and let them verify this proof is ok, what command should they run? Right now I just see locally there are no sorry

[Martin Dvořák]

Congratulations!

Question 1 is just a matter of style. Some people don't use the keyword lemma at all (I use lemma a lot and private lemma all over the place). As for those inline lemmas (have), please break line after := or after by so that your code isn't pushed so much to the right side. Inline lemmas are great because they don't force you to repeat the local context in a new declaration. Just avoid them when (1) you want to use the same or similar inline lemma in two different proofs, or (2) when the elaboration takes a long time. And BTW, if you have an inline lemma whose proof happens to be just one step, ask yourself, maybe you want to do just the one step in the original proof without creating the inline lemma.

Question 2 is not something I can help you with. I also find exact? extremely helpful and apply? only seldom helpful. I just recommend that, after you find the right lemma to close the subgoal, you delete the by exact part, as these two words basically cancel each other out.

Question 3 is for @Scott Morrison because he wrote the lean4checker.
https://github.com/leanprover/lean4checker

Overall, good job! I don't have much to criticize about it (apart from small unimportant things such as redundant imports or proofs that could be shortened).

PS: I just noticed that for blocks you use . and sometimes {}. Neither of them is the recommended style. Use · written by \. in VS Code.

[Martin Dvořák]

If you want to see an example of what can be easily shortened in your proof:

theorem eq_sum_mul_k_to_n (k n : ℕ) (h : k > 0): SumMulKToN k n = SetSum (MulKToN k n h) := by
  unfold MulKToN
  rw [← cancel_mul_k_finset]
  unfold SumMulKToN
  have nat_mul_left_cancel {n m k : ℕ } (h : m = k) : n * m = n * k := by exact congrArg (HMul.hMul n) h
  apply nat_mul_left_cancel
  rw [sum_first_n]

The same thing can be written as follows:

theorem eq_sum_mul_k_to_n (k n : ℕ) (h : k > 0): SumMulKToN k n = SetSum (MulKToN k n h) := by
  unfold MulKToN
  rw [← cancel_mul_k_finset, sum_first_n]
  rfl

I personally use rewrite in place of rw that directly precedes rfl but this distinction is not important.

[Marcelo Fornet]

I tried with rewrite and it didn't close the goal, probably because it is not exactly the same without unfolding SumMulKToN

[Martin Dvořák]

I mean, you can do the intermediate:

theorem eq_sum_mul_k_to_n (k n : ℕ) (h : k > 0): SumMulKToN k n = SetSum (MulKToN k n h) := by
  unfold MulKToN
  rw [← cancel_mul_k_finset]
  unfold SumMulKToN
  rw [sum_first_n]

[Kim Morrison]

Typically lean4checker isn't really relevant in this scenario: it's for when you have a really skeptical audience who worry you might be cheating. :-)

Making sure your project is set up so that everything builds with lake build is probably the answer to question 3?

[Martin Dvořák]

The "build everything" setup has just been discussed here:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/build.20all.20my.20code