Erdős problem 397
Are there only finitely many solutions to with the distinct?
Sources
FormalConjectures/ErdosProblems/
397.lean
Retained formal statement
Are there only finitely many solutions to with the distinct?
Somani, using ChatGPT, has given a negative answer. In fact, for any , if , 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.
False ↔ {(M, N) | Disjoint M N ∧ ∏ i ∈ M, i.centralBinom = ∏ j ∈ N, j.centralBinom}.Finite