Gilbreath's conjecture

Reference: Wikipedia

noncomputable def Gilbreath.d : ℕ → ℕ → ℕ

Gilbreath's nth difference, $d^n$ Let $d^0(n) = p_n$ and $d^k(n) = |d^{k-1}(n+1) - d^{k-1}(n)|

Equations

• Gilbreath.d 0 = fun (n : ℕ) => Nat.nth Nat.Prime n
• Gilbreath.d k.succ = fun (n : ℕ) => (↑(Gilbreath.d k (n + 1)) - ↑(Gilbreath.d k n)).natAbs

theorem Gilbreath.gilbreath_conjecture (k : ℕ+) : d (↑k) 0 = 1

Gilbreath's conjecture Gilbreath's conjecture states that every term in the sequence $d^k_0$ for $k > 0$ is equal to 1.