Additive number theory

Representing integers as sums from special sets, and the density of integer sets: sumsets of integers, subset sums and complete sequences, primitive sets, natural and logarithmic density, Romanoff's theorem; additive bases and complements and zero-sum constants go to additive combinatorics.

• Distinct multiples in an interval
• Erdős minimum overlap problem
• Geometric-progression-free sets of Hurwitz quaternions
• Natural and logarithmic density
• Primitive sets
• Quotients a/gcd(a, b) in sets of integers
• Reciprocal lcm sums of integer sets
• Romanoff's theorem
• Sets with no element dividing a product of two others
• Strongly complete sequences
• Sums of consecutive terms of a sequence
• Sums of numbers of the form 2^k 3^l
• Sums of powers of consecutive primes
• Sums of practical and polygonal numbers

TheoremDisproof of Erdős Problem 1 on distinct subset sums#●ready to prove

There is no real number \(C > 0\) such that for every natural number \(N \ne 0\) and every finite set \(A \subseteq \{1, \dots, N\}\) whose distinct subsets have distinct sums, \(C \cdot 2^{|A|} < N\).

Resolved false: Disproved: machine-checked disproof recorded in the FormalConjectures source record. Source: Lean 4 disproof of Erdos Problem 1 (proof by GPT-6 Astra in the FrontierMath Erdos benchmark; repository by T. Adamczewski), tadamcz/erdos1 at commit 0e395153306f34b3829d118b85bdd704136f2843, theorem Erdos1.erdos_1.disproof, https://github.com/tadamcz/erdos1/blob/0e395153306f34b3829d118b85bdd704136f2843/Erdos1/Resolutions/Erdos1_219usd_38h.lean#L2419. Moved from OpenConjectures/NumberTheory/ErdosProblem1.

public theorem_wanted conjecture_refuted : ¬ conjecture

TheoremOdd numbers \(1 < n < 2^{50}\) are squarefree plus a power of two#●ready to prove

Every odd natural number \(n\) with \(1 < n < 2^{50}\) can be written as \(n = s + 2^k\), where \(s\) is a squarefree positive integer and \(1 \le k \le 13\).

This is a finite verification of a conjecture of Erdős, which is open for all odd \(n\).

public theorem_wanted exists_squarefree_add_two_pow_of_odd_lt_two_pow_fifty (n : ℕ) (h1 : 1 < n)
    (h2 : n < 2 ^ 50) (hodd : Odd n) :
    ∃ s k : ℕ, 0 < s ∧ Squarefree s ∧ 1 ≤ k ∧ k ≤ 13 ∧ n = s + 2 ^ k

Sources

• Christian Hercher, On the Sum of a Squarefree Integer and a Power of Two, Journal of Integer Sequences 28 (2025), Article 25.3.1, Theorem 5 (jis-2025-25.3.1-thm-5).

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.