How to use Lean to prove this problem related to generating

Stream: new members

[Yiran Wang]

Hello everyone, I am a beginner in Lean 4 and currently interested in using Lean to prove combinatorial theorems. However, I have encountered a problem that seems to require generating functions for the proof. So far, I have considered using induction, but I am unable to complete the proof. Could anyone share some ideas or methods to solve this problem in Lean 4? Thank you so much for your help!
image.png
import Mathlib

open BigOperators Nat Finset

open Set

open Nat

open Function

theorem idt_148:∑ k in range (n + 1),choose n k * (-1:ℝ)^k / (2*k+1) = (2^n*n !)^2/(2*n+1)!:= by

sorry

[Eric Wieser]

@Yiran Wang, it seems you are one of many users trying to formalize problems from "The Art of Proving Binomial Identities". Are you able to say where the sudden interest in this document is coming from?

[Notification Bot]

This topic was moved here from #lean4 > How to use Lean to prove this problem related to generating by Eric Wieser.

[Yiran Wang]

Because this is a relatively challenging book in the field of combinatorial theorem proofs, and a considerable number of problems in it include proof steps, making it suitable for learning and formalization. May I kindly ask if you are interested in this particular problem?

[Yury G. Kudryashov]

First, you need to read #mwe and #backticks. Then you should complete some Lean tutorials and try to follow the informal proof you have in the book yourself. Once you're stuck at a particular step, you come back, explain what you've done yourself and ask for help.

[Yury G. Kudryashov]

Yiran Wang said:

Because this is a relatively challenging book in the field of combinatorial theorem proofs, and a considerable number of problems in it include proof steps, making it suitable for learning and formalization. May I kindly ask if you are interested in this particular problem?

Given that none of these identities were discussed here until recently, and more than one user comes, asks a question about an identity from this book without discussing simpler problems first (e.g., did you complete the Natural Numbers Game? formalized the first identities from the same book?), it seems reasonable to assume that a third party asked you to formalize these identities. Is it true, or it's just a coincidence?

[Yiran Wang]

@Yury G. Kudryashov Hello, the other user who asked about the identities and I are classmates. I have already completed the proofs for simpler combinatorial identities before, but as the difficulty increased, I found it challenging (especially when it involves probability and calculus). Apologies, but I have not thought through the steps for this particular problem. May I first come up with steps in natural language and then consult you to see if these steps are feasible?