The Graham--Knuth--Patashnik central-binomial conjecture

This file records the conjecture from Exercise 5.112 of Concrete Mathematics and its restriction to powers of two. The conjecture itself remains open.

def GKPCarry.gkpConjecture : Prop

The Graham--Knuth--Patashnik conjecture: if n > 4 and n ∉ {64, 256}, then Nat.centralBinom n is divisible by 4 or by 9.

Equations

• GKPCarry.gkpConjecture = ∀ (n : ℕ), 4 < n → n ≠ 64 → n ≠ 256 → 4 ∣ n.centralBinom ∨ 9 ∣ n.centralBinom

def GKPCarry.gkpPowerOfTwoConjecture : Prop

The power-of-two restriction of the GKP conjecture.

Equations

• GKPCarry.gkpPowerOfTwoConjecture = ∀ (k : ℕ), 2 < k → k ≠ 6 → k ≠ 8 → 9 ∣ (2 ^ k).centralBinom