Romanoff's theorem

DefinitionNatural numbers with at most \(r\) distinct prime factors#✓fully proved

For natural numbers \(n\) and \(r\), \(n\) has at most \(r\) distinct prime factors when \(n = 0\) or at most \(r\) distinct primes divide \(n\); the number \(0\) is counted as having no prime factors.

def HasAtMostRPrimeFactors (n r : ℕ) : Prop :=
  n.primeFactors.card ≤ r

Sources

• EP-851 [Erdős Problems].

Used by 1

Used bySums of a power of two and a number with few prime factors

DefinitionSums of a power of two and a number with few prime factors#✓fully proved

For a natural number \(r\), a natural number \(m\) is of this form when \(m = 2^k + n\) for some natural numbers \(k\) and \(n\) such that \(n = 0\) or at most \(r\) distinct primes divide \(n\).

def Representable (r m : ℕ) : Prop :=
  ∃ k n : ℕ, m = 2 ^ k + n ∧ HasAtMostRPrimeFactors n r

Sources

• EP-851 [Erdős Problems].

Uses 1 · Used by 1

Statement usesNatural numbers with at most \(r\) distinct prime factors

Used byErdős Problem 851

DefinitionSums of a power of two and a prime#✓fully proved

A natural number \(m\) is of this form when \(m = 2^k + p\) for some natural number \(k\) and some prime \(p\).

def PrimeRepresentable (m : ℕ) : Prop :=
  ∃ k p : ℕ, m = 2 ^ k + p ∧ p.Prime

Sources

• Romanoff's theorem in EP-851 [Erdős Problems].

Used by 1

Used byErdős Problem 851

DefinitionErdős Problem 851#✓fully proved

The proposition asserts two things. First, the set of natural numbers of the form \(2^k + p\), with \(k\) a natural number and \(p\) prime, has positive lower density (Romanoff's theorem). Second, for every real number \(\varepsilon > 0\) there is a natural number \(r\) such that the set of natural numbers of the form \(2^k + n\), with \(k\) and \(n\) natural numbers and with \(n = 0\) or at most \(r\) distinct primes dividing \(n\), has lower density at least \(1 - \varepsilon\).

noncomputable def Statement : Prop :=
  0 < Set.lowerDensity {m | PrimeRepresentable m} ∧
    ∀ (ε : ℝ), ε > 0 → ∃ r : ℕ, 1 - ε ≤ Set.lowerDensity {m | Representable r m}

Sources

• EP-851 [Erdős Problems].

Uses 3 · Used by 1

Statement usesSums of a power of two and a prime · Sums of a power of two and a number with few prime factors · Lower density

Used byErdős Problem 851 is true

TheoremErdős Problem 851 is true#●ready to prove

The set of natural numbers of the form \(2^k + p\), with \(k\) a natural number and \(p\) prime, has positive lower density. Moreover, for every real number \(\varepsilon > 0\) there is a natural number \(r\) such that the set of natural numbers of the form \(2^k + n\), with \(k\) and \(n\) natural numbers and with \(n = 0\) or at most \(r\) distinct primes dividing \(n\), has lower density at least \(1 - \varepsilon\).

Romanoff proved the positive-density clause in 1934; Price and GPT-5.2 Pro proved the near-one density statement affirmatively in 2026.

public theorem_wanted Statement_holds : Statement

Sources

• Lean proof of Erdős Problem 851, https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos851.lean#L37; Yuchen Ding and Wenguang Zhai, A generalization of the Romanoff theorem, arXiv:2401.15892v3 (2024), https://arxiv.org/abs/2401.15892v3.

Uses 1

Statement usesErdős Problem 851

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.