Erdos397Starter

Erdős problem 397 in use: central binomial coefficients and the Somani family

Open in Workbench View on GitHub

1-- Erdős problem 397 in use: central binomial coefficients and the Somani family2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Erdos397Starter8import Grace.Cumulus.NumberTheory.Erdos397910-- Binomial coefficients compute: C(6, 3) = 20 and C(10, 5) = 252.11theorem central_three12  shows central(3) = 2013proof14  compute1516theorem central_five17  shows central(5) = 25218proof19  compute2021-- The first member of the family, a = 2 and c = 49:22-- C(4, 2) · C(12, 6) · C(98, 49) = C(6, 3) · C(8, 4) · C(100, 50).23theorem first_solution24  shows central(2) * (central(6) * central(49)) = central(3) * (central(4) * central(50))25proof26  simp2728-- Its indices are distinct, as the problem requires.29theorem first_solution_indices30  shows 2 ≠ 2 * 2 + 2 ∧ 2 ≠ 8 * 2 * 2 + 8 * 2 + 1 ∧ 2 * 2 + 2 ≠ 8 * 2 * 2 + 8 * 2 + 131proof32  have two : 2 ≤ 2 by arith33  have all := erdos397.distinct with two34  rcases all with ⟨left, rest⟩35  exact left36