Grace/Cumulus/NumberTheory/Erdos397.g17

Imports

Declarations

central def
add_one.nonzero theorem derivation
central.step theorem derivation
erdos397.identity theorem derivation
erdos397.distinct theorem derivation
erdos397.unbounded theorem derivation
Source

1-- Erdős problem 397: infinitely many coincidences among products of central2-- binomial coefficients3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.NumberTheory.Erdos3979import Binomial1011-- Erdős and Graham asked whether the equation12--   ∏ᵢ C(2mᵢ, mᵢ) = ∏ⱼ C(2nⱼ, nⱼ)13-- has only finitely many solutions in distinct positive integers. The answer14-- is no: for every a ≥ 2, with c = 8a² + 8a + 1,15--   C(2a, a) · C(4a + 4, 2a + 2) · C(2c, c)16--     = C(2a + 2, a + 1) · C(4a, 2a) · C(2c + 2, c + 1).17-- The family was found by Neel Somani with ChatGPT in January 2026. This18-- module checks it from the axioms of set theory: the identity rests on one19-- step law for central binomial coefficients and a polynomial identity.2021-- The central binomial coefficient C(2n, n).22def central (n : Nat) : Nat := 2 * n choose n2324theorem add_one.nonzero (x : Nat)25  shows x + 1 ≠ 026proof27  arith2829-- Each step of the central binomial sequence:30--   C(2n + 2, n + 1) · (n + 1)² = C(2n, n) · (2n + 2)(2n + 1).31theorem central.step (n : Nat)32  shows central(n + 1) * ((n + 1) * (n + 1)) =33    central(n) * ((2 * n + 2) * (2 * n + 1))34proof35  unfold central36  have lower := choose.factorial at n with n37  have upper := choose.factorial at n + 1 with n + 138  have outer := factorial.succ at n + n + 1 with *39  have inner := factorial.succ at n + n with *40  have step := factorial.succ at n with *41  have nonzero := factorial.nonzero at n with *42  have squareNonzero := mul.nonzero with nonzero, nonzero43  have key : (n! * n!) * ((2 * (n + 1) choose n + 1) * ((n + 1) * (n + 1))) =44      (n! * n!) * ((2 * n choose n) * ((2 * n + 2) * (2 * n + 1)))45    ring [upper, lower, outer, inner, step]46  exact mul.left_cancel_positive with squareNonzero, key4748-- The identity behind every solution in the family: with c = 8a² + 8a + 1,49--   C(2a, a) · C(4a + 4, 2a + 2) · C(2c, c)50--     = C(2a + 2, a + 1) · C(4a, 2a) · C(2c + 2, c + 1).51-- Multiply both sides by (a + 1)²(2a + 1)²(2a + 2)²(c + 1)² and apply the52-- step law to each central binomial coefficient whose index is a successor.53theorem erdos397.identity (a : Nat)54  shows central(a) * (central(2 * a + 2) * central(8 * a * a + 8 * a + 1)) =55    central(a + 1) * (central(2 * a) * central(8 * a * a + 8 * a + 2))56proof57  have e1 : 2 * a + 2 = 2 * a + 1 + 1 by ring58  have e2 : 8 * a * a + 8 * a + 2 = 8 * a * a + 8 * a + 1 + 1 by ring59  rw [e1, e2]60  have s1 := central.step at a with *61  have s2 := central.step at 2 * a with *62  have s3 := central.step at 2 * a + 1 with *63  have s4 := central.step at 8 * a * a + 8 * a + 1 with *64  have n1 := add_one.nonzero at a with *65  have n2 := add_one.nonzero at 2 * a with *66  have n3 := add_one.nonzero at 2 * a + 1 with *67  have n4 := add_one.nonzero at 8 * a * a + 8 * a + 1 with *68  have q1 := mul.nonzero with n1, n169  have q2 := mul.nonzero with n2, n270  have q3 := mul.nonzero with n3, n371  have q4 := mul.nonzero with n4, n472  have q34 := mul.nonzero with q3, q473  have q234 := mul.nonzero with q2, q3474  have nonzero := mul.nonzero with q1, q23475  have key : ((a + 1) * (a + 1)) *76        (((2 * a + 1) * (2 * a + 1)) *77          (((2 * a + 1 + 1) * (2 * a + 1 + 1)) *78            ((8 * a * a + 8 * a + 1 + 1) * (8 * a * a + 8 * a + 1 + 1)))) *79        (central(a) *80          (central(2 * a + 1 + 1) * central(8 * a * a + 8 * a + 1))) =81      ((a + 1) * (a + 1)) *82        (((2 * a + 1) * (2 * a + 1)) *83          (((2 * a + 1 + 1) * (2 * a + 1 + 1)) *84            ((8 * a * a + 8 * a + 1 + 1) * (8 * a * a + 8 * a + 1 + 1)))) *85        (central(a + 1) * (central(2 * a) * central(8 * a * a + 8 * a + 1 + 1)))86    ring [s1, s2, s3, s4]87  exact mul.left_cancel_positive with nonzero, key8889-- For a ≥ 2 the three indices on each side are distinct, and the two sides90-- use different indices, so each a gives a genuine solution.91theorem erdos397.distinct (a : Nat)92  requires large : 2 ≤ a93  shows (a ≠ 2 * a + 2 ∧ a ≠ 8 * a * a + 8 * a + 1 ∧94      2 * a + 2 ≠ 8 * a * a + 8 * a + 1) ∧95    (a + 1 ≠ 2 * a ∧ a + 1 ≠ 8 * a * a + 8 * a + 2 ∧96      2 * a ≠ 8 * a * a + 8 * a + 2) ∧97    (a ≠ a + 1 ∧ a ≠ 2 * a ∧ a ≠ 8 * a * a + 8 * a + 2)98proof99  arith100101-- Infinitely many solutions: beyond any bound there is another a.102theorem erdos397.unbounded (N : Nat)103  shows ∃ a ∈ ℕ, N < a ∧ 2 ≤ a ∧104    central(a) * (central(2 * a + 2) * central(8 * a * a + 8 * a + 1)) =105    central(a + 1) * (central(2 * a) * central(8 * a * a + 8 * a + 2))106proof107  have witnessNat : Nat(N + 2) by typecheck108  have member := nat.omega.forward with witnessNat109  refine ⟨N + 2, member, ?_, ?_, erdos397.identity at N + 2 with *⟩110  . arith111  . arith112