Additive complements

DefinitionErdős Problem 477#✓fully proved

The statement that there are a polynomial \(f\) with integer coefficients of degree at least \(2\) and a set \(A\) of integers such that for every integer \(n\) there is exactly one pair \((a, b)\) with \(a \in A\), \(b = f(k)\) for some integer \(k\), and \(n = a + b\). Only the pair is required to be unique, not the integer \(k\).

def conjecture : Prop :=
  ∃ (f : Polynomial ℤ) (A : Set ℤ),
    (↑(2 : ℕ) : WithBot ℕ) ≤ Polynomial.degree f ∧
      ∀ n : ℤ, ∃! p : ℤ × ℤ, p.1 ∈ A ∧ p.2 ∈ Set.range (fun k : ℤ => Polynomial.eval k f) ∧ n =
        p.1 + p.2

Used by 1

Used byErdős Problem 477 has a positive answer

TheoremErdős Problem 477 has a positive answer#●ready to prove

There are a polynomial \(f\) with integer coefficients of degree at least \(2\) and a set \(A\) of integers such that for every integer \(n\) there is exactly one pair \((a, b)\) with \(a \in A\), \(b = f(k)\) for some integer \(k\), and \(n = a + b\).

Contrary to Erdős and Graham's expectation, GPT (prompted independently by L. Price and pipeline-math) proved that such a set \(A\) exists for \(f(k) = k^d\) with every even \(d \ge 6\), so \(f(k) = k^6\) is a witness.

public theorem_wanted conjecture_holds : conjecture

def conjecture : Prop :=
  ∃ (f : Polynomial ℤ) (A : Set ℤ),
    (↑(2 : ℕ) : WithBot ℕ) ≤ Polynomial.degree f ∧
      ∀ n : ℤ, ∃! p : ℤ × ℤ, p.1 ∈ A ∧ p.2 ∈ Set.range (fun k : ℤ => Polynomial.eval k f) ∧ n =
        p.1 + p.2

WantedExt/Combinatorics/ErdosProblem477Wanted.lean:25

Sources

T. F. Bloom, Erdős Problem #477, erdosproblems.com (live page, LaTeX source and forum threads read 2026-10-22), https://www.erdosproblems.com/477.

Uses 1

Statement usesErdős Problem 477

TheoremLorentz's theorem on additive complements (Erdős Problem 31)#●ready to prove

For every infinite set \(A\) of natural numbers there is a set \(B\) of natural numbers of natural density \(0\) such that every sufficiently large natural number lies in \(A + B = \{a + b \mid a \in A,\ b \in B\}\).

Resolved true: Proved by Lorentz [Lo54]. Source: George G. Lorentz, On a problem of additive number theory, Proceedings of the American Mathematical Society 5 (1954), 838–841, https://doi.org/10.1090/s0002-9939-1954-0063389-3. Moved from OpenConjectures/NumberTheory/ErdosProblem31.

public theorem_wanted conjecture_holds : conjecture

Uses 1

Statement usesDensity of a set

1 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.