Exponential Diophantine equations

Equations with unknown exponents: Pillai, Catalan, Størmer, Nagell–Ljunggren, Ramanujan–Nagell and Terai-type equations, powers plus one.

TheoremStørmer's theorem#✓fully proved

For every natural number \(y \ge 2\), there is a finite set \(S\) of pairs of natural numbers such that, for every positive integer \(n\) such that all prime factors of \(n\) and all prime factors of \(n + 1\) are at most \(y\), the pair \((n, n + 1)\) lies in \(S\).

theorem stormer_theorem (y : ℕ) (hy : 2 ≤ y) :
    ∃ S : Finset (ℕ × ℕ), ∀ n : ℕ, 0 < n →
      (∀ p ∈ n.primeFactors, p ≤ y) →
      (∀ p ∈ (n + 1).primeFactors, p ≤ y) →
      (n, n + 1) ∈ S
Sources
  • https://en.wikipedia.org/wiki/St%C3%B8rmer%27s_theorem.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.