Skip to content

Erdős problem 397

Are there only finitely many solutions to ∏i(2mimi)=∏j(2njnj) \prod_i \binom{2m_i}{m_i}=\prod_j \binom{2n_j}{n_j} with the mi,njm_i,n_j distinct?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

397.lean

Retained formal statement1 of 1

Are there only finitely many solutions to ∏i(2mimi)=∏j(2njnj) \prod_i \binom{2m_i}{m_i}=\prod_j \binom{2n_j}{n_j} with the mi,njm_i,n_j distinct?

Somani, using ChatGPT, has given a negative answer. In fact, for any a≥2a\geq 2, if c=8a2+8a+1c=8a^2+8a+1, (2aa)(4a+42a+2)(2cc)=(2a+2a+1)(4a2a)(2c+2c+1).\binom{2a}{a}\binom{4a+4}{2a+2}\binom{2c}{c}= \binom{2a+2}{a+1}\binom{4a}{2a}\binom{2c+2}{c+1}. Further families of solutions are given in the comments by SharkyKesa.

This was earlier asked about in a [MathOverflow] question, in response to which Elkies also gave an alternative construction which produces solutions - at the moment it is not clear whether Elkies' argument gives infinitely many solutions (although Bloom believes that it can).

This was formalized in Lean by Wu using Aristotle.

FormalConjectures/ErdosProblems/397.leanErdos397.erdos_3971 lineExact file
False ↔ {(M, N) | Disjoint M N ∧ ∏ i ∈ M, i.centralBinom = ∏ j ∈ N, j.centralBinom}.Finite
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.