Erdős Problem 477

References:

• erdosproblems.com/477
• Sek59 Milan Sekanina, Замечания к фактoризации беcкoнечнoй цикличеcкoй группы, Czechoslovak Mathematical Journal, Vol. 9 (1959), No. 4, 485–495

theorem Erdos477.erdos_477 : sorry ↔ ∃ (f : Polynomial ℤ), 2 ≤ f.degree ∧ ∃ (A : Set ℤ), ∀ (z : ℤ), ∃! ab : ℤ × ℤ, ab ∈ A ×ˢ ((fun (a : ℤ) => Polynomial.eval a f) '' {n : ℤ | 0 < n}) ∧ z = ab.1 + ab.2

Is there a polynomial $f:\mathbb{Z}\to \mathbb{Z}$ of degree at least $2$ and a set $A\subset \mathbb{Z}$ such that for any $z\in \mathbb{Z}$ there is exactly one $a\in A$ and $b\in \{ f(n) : n\in\mathbb{Z}\}$ such that $z=a+b$?

theorem Erdos477.erdos_477.S_sq (A : Set ℤ) : ∃ (z : ℤ), ¬∃! a : ℤ × ℤ, a ∈ A ×ˢ ((fun (a : ℤ) => Polynomial.eval a (Polynomial.X ^ 2)) '' {n : ℤ | 0 < n}) ∧ z = a.1 + a.2

There is no such $A$ for the polynomial $f(x) = X^2$.

This is shown in [Sek59].

theorem Erdos477.erdos_477.degree_two_dvd_condition_b_ne_zero {a b c : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) (hab : a ∣ b) : have f := a • Polynomial.X ^ 2 + b • Polynomial.X + Polynomial.C c; ∀ (A : Set ℤ), ∃ (z : ℤ), ¬∃! a : ℤ × ℤ, a ∈ A ×ˢ ((fun (a : ℤ) => Polynomial.eval a f) '' {n : ℤ | 0 < n}) ∧ z = a.1 + a.2

There is no such $A$ for any polynomial $f(x) = aX^2 + bX + c$, if $a | b$ with $a \ne 0$ and $b \ne 0. This was found be AlphaProof for the specific instance $X^2 - X + 1$ and then generalised.

theorem Erdos477.erdos_477.X_pow_three (A : Set ℤ) : ∃ (z : ℤ), ¬∃! a : ℤ × ℤ, a ∈ A ×ˢ ((fun (a : ℤ) => Polynomial.eval a (Polynomial.X ^ 3)) '' {n : ℤ | 0 < n}) ∧ z = a.1 + a.2

Probably there is no such $A$ for the polynomial $X^3$.

theorem Erdos477.erdos_477.monomial (k : ℕ) (hk : 2 ≤ k) (A : Set ℤ) : ∃ (z : ℤ), ¬∃! a : ℤ × ℤ, a ∈ A ×ˢ ((fun (a : ℤ) => Polynomial.eval a (Polynomial.X ^ k)) '' {n : ℤ | 0 < n}) ∧ z = a.1 + a.2

Probably there is no such $A$ for the polynomial $X^k$ for any $k \ge 2$. This is asked in [Sek59].