discrete math

Stream: new members

[Ryan]

Hello, I'm a student interested in discrete math and computer proof verification. I enjoyed natural number game but I have little experience in math, so I cannot use lean very well. As an exercise for combinatorial proofs in lean, I made a lean3 proof for a simple binomial coefficient identity. Although the proof is complicated since it uses combinatorial arguments, I wonder if the result can be contributed to mathlib (data.nat.choose.sum). Also, should I need to learn lean4 instead of lean3? Thank you.

theorem hockey_stick (n k : ℕ):
  ∑ i in Ico k (n+1), i.choose k = (n+1).choose (k+1)

[Scott Morrison]

I'd guess we have this in mathlib, let me see.

[Scott Morrison]

Maybe not! At least I don't see it by searching for sum.*choose in mathlib...

[Scott Morrison]

I doubt we would want a combinatorial proof, however.

[Scott Morrison]

Either of the inductive proof, or the proof by telescoping would be fine, though.

[Eric Wieser]

If it did exist, I'd guess docs#nat.choose_succ or docs#nat.succ_choose_succ? Neither of which exist!