Digit properties of integers

Digit sums and products, Niven, happy, Kaprekar, Keith numbers, comma sequences, decimal expansions of fractions (Midy, repetends).

TheoremGrundman's bound on consecutive Niven numbers#✓fully proved

Let \(b \ge 2\) and \(a \ge 1\) be integers. Then for some \(i\) with \(0 \le i \le 2b\), the integer \(a + i\) is not divisible by the sum of its base-\(b\) digits. Equivalently, the \(2b + 1\) consecutive integers \(a, a + 1, \dots, a + 2b\) are not all \(b\)-Niven numbers, where a \(b\)-Niven number is a positive integer divisible by the sum of its base-\(b\) digits.

theorem grundman_consecutive_niven_bound
    (b a : ℕ) (hb : 2 ≤ b) (ha : 0 < a) :
    ∃ i : ℕ, i ≤ 2 * b ∧
      ¬ ((Nat.digits b (a + i)).sum ∣ a + i)

Sources

Michael Gohn, Joshua Harrington, Sophia Lebiere, Hani Samamah, Kyla Shappell, and Tony W. H. Wong, "Arithmetic Progressions of b-Prodigious Numbers," Journal of Integer Sequences 25 (2022), Article 22.8.7, line 149, https://cs.uwaterloo.ca/journals/JIS/VOL25/Wong/wong42.tex, citing as the original result Heidi Grundman, "Sequences of consecutive n-Niven numbers," Fibonacci Quarterly 32 (1994), 174–175.

TheoremTu–Deng conjecture#●ready to prove

For every integer \(k \ge 2\) and every nonzero residue \(t\) modulo \(2^k - 1\), the number of pairs \((a, b)\) of residues modulo \(2^k - 1\) with \(a + b = t\) and \(w(a) + w(b) \le k - 1\) is at most \(2^{k-1}\), where \(w(a)\) is the binary digit sum of the representative of \(a\) in \(\{0, 1, \dots, 2^k - 2\}\).

public theorem_wanted tuDengConjecture_holds : tuDengConjecture

def tuDengConjecture : Prop :=
  ∀ (k : ℕ), 2 ≤ k → ∀ t : ZMod (2 ^ k - 1), t ≠ 0 →
    {p : ZMod (2 ^ k - 1) × ZMod (2 ^ k - 1) |
      p.1 + p.2 = t ∧ binDigitSum p.1.val + binDigitSum p.2.val ≤ k - 1}.ncard
      ≤ 2 ^ (k - 1)

WantedExt/NumberTheory/TuDengConjectureWanted.lean:25

Sources

T. W. Cusick, Proof of the Tu-Deng Conjecture, arXiv:2608.14821 (2026), https://arxiv.org/abs/2608.14821.

Uses 1

Statement usesBinary digit sum

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.