Erdős 397: central binomial product identity

[XC0R]

Summary

Proves erdos_397 — the central binomial product identity has infinitely many solutions.

For a ≥ 2, defines c(a) = 8a² + 8a + 1 and shows:
C(2a,a) · C(4a+4, 2a+2) · C(2c, c) = C(2a+2, a+1) · C(4a, 2a) · C(2c+2, c+1)

Proof technique: ℚ factorial cancellation via field_simp + factorial_succ recurrences + push_cast + ring. Wrapper proves Finset disjointness, product equality, injectivity of the family, and Set.Infinite.

Assisted by Claude (Anthropic) for Lean translation.

[mo271]

Thanks, let's use the formal_proof using formal_conjectures at ... here

[mo271]

Suggested change

	@[category research solved, AMS 11, formal_proof using lean4 at "https://gist.github.com/llllvvuu/40d68cfa9de9f43eece07ff4fdc3b0ef"]
	@[category research solved, AMS 11, formal_proof using formal_conjectures at "https://github.com/XC0R/formal-conjectures/blob/3c356a50a21bcbf3543f960b0c92d7fb26228cb6/FormalConjectures/ErdosProblems/397.lean#L147"]

Let's remove the helping theorems/lemmas above and the proof here and instead use formal_proof using formal_conjectures (this is better than the formal_proof using lean4 what we currently have.