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

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

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 a2a\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 ∧ ∏ iM, i.centralBinom = ∏ jN, 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.

Search problems.science

Find a Problem, Result, source, or page