Erdős Problem 283

References:

• erdosproblems.com/283
• [Al19] Alekseyev, Max A., On partitions into squares of distinct integers whose reciprocals sum to 1. (2019), 213--221.
• [Ca60] Cassels, J. W. S., On the representation of integers as the sums of distinct summands taken from a fixed set. Acta Sci. Math. (Szeged) (1960), 111-124.
• [Gr63] Graham, R. L., A theorem on partitions. J. Austral. Math. Soc. (1963), 435-441.
• [vD25] W. van Doorn, Partitions with prescribed sum of rationals: asymptotic bounds. arXiv:2502.02200 (2025).

def Erdos283.Condition (p : Polynomial ℤ) : Prop

Given a polynomial p, the predicate that if the leading coefficient is positive and there exists no $d≥2$ with $d ∣ p(n)$ for all $n≥1$, then for all sufficiently large $m$, there exist integers $1≤n_1<\dots < n_k$ such that $$1=\frac{1}{n_1}+\cdots+\frac{1}{n_k}$$ and $$m=p(n_1)+\cdots+p(n_k)$$?

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos283.erdos_283 : True ↔ ∀ (p : Polynomial ℤ), Condition p

Let $p\colon \mathbb{Z} \rightarrow \mathbb{Z}$ be a polynomial whose leading coefficient is positive and such that there exists no $d≥2$ with $d ∣ p(n)$ for all $n≥1$. Is it true that, for all sufficiently large $m$, there exist integers $1≤n_1<\dots < n_k$ such that $$1=\frac{1}{n_1}+\cdots+\frac{1}{n_k}$$ and $$m=p(n_1)+\cdots+p(n_k)$$?

GPT 5.5 Pro (prompted by Price) has given a proof that the answer is yes, for the stronger version with $1$ replaced by any rational $\alpha>0$.

This was formalized in Lean by Ammanamanchi using Opus 4.6 and GPT 5.5 Pro.

theorem Erdos283.erdos_283.variants.graham : Condition Polynomial.X

Graham [Gr63] has proved this when $p(x)=x$.

theorem Erdos283.erdos_283.variants.graham_alpha (p : Polynomial ℤ) (α : ℚ) : 0 < p.leadingCoeff → (¬∃ d ≥ 2, ∀ n ≥ 1, d ∣ Polynomial.eval n p) → α > 0 → ∀ᶠ (m : ℕ) in Filter.atTop, ∃ (S : Finset ℕ), (∀ n ∈ S, 1 ≤ n) ∧ ∑ n ∈ S, 1 / ↑n = α ∧ ∑ n ∈ S, Polynomial.eval (↑n) p = ↑m

Graham also conjectures that this remains true with $1$ replaced by an arbitrary rational $\alpha>0$ (provided $m$ is taken sufficiently large depending on $\alpha$).

theorem Erdos283.erdos_283.variants.cassels (p : Polynomial ℤ) : 0 < p.leadingCoeff → (¬∃ d ≥ 2, ∀ n ≥ 1, d ∣ Polynomial.eval n p) → ∀ᶠ (m : ℕ) in Filter.atTop, ∃ (S : Finset ℕ), (∀ n ∈ S, 1 ≤ n) ∧ ∑ n ∈ S, Polynomial.eval (↑n) p = ↑m

Cassels [Ca60] has proved that these conditions on the polynomial imply every sufficiently large integer is the sum of $p(n_i)$ with distinct $n_i$.

theorem Erdos283.erdos_283.variants.burr (k : ℕ) : k ≥ 1 → ∀ᶠ (m : ℕ) in Filter.atTop, ∃ (M : Multiset ℕ), (∀ n ∈ M, 1 ≤ n) ∧ (Multiset.map (fun (n : ℚ) => 1 / n) do let a ← M pure ↑a).sum = 1 ∧ (Multiset.map (fun (n : ℤ) => n ^ k) do let a ← M pure ↑a).sum = ↑m

Burr has proved this if $p(x)=x^k$ with $k\geq 1$ and if we allow $n_i=n_j$.

theorem Erdos283.erdos_283.variants.alekseyev (m : ℕ) : m > 8542 → ∃ (S : Finset ℕ), (∀ n ∈ S, 1 ≤ n) ∧ ∑ n ∈ S, 1 / ↑n = 1 ∧ ∑ n ∈ S, ↑n ^ 2 = ↑m

Alekseyev [Al19] has proved this when $p(x)=x^2$, for all $m>8542$.

theorem Erdos283.erdos_283.variants.van_doorn_linear (b : ℤ) : 1 ≤ b → b ≤ 5000 → Condition (Polynomial.X + Polynomial.C b)

van Doorn [vD25] has investigated the question of what 'sufficiently large' means for $p(x)=x$. van Doorn has also proved the original conjecture for many linear and quadratic polynomials. For example, if $p(x) = x + b$ with $1 \leq b \leq 5000$, then the conjecture is true.

theorem Erdos283.erdos_283.variants.van_doorn_quadratic (b : ℤ) : 1 ≤ b → b ≤ 800 → Condition (Polynomial.X ^ 2 + Polynomial.C b)

van Doorn [vD25] has proved the original conjecture for many linear and quadratic polynomials. For example, if $p(x) = x^2 + b$ with $1 \leq b \leq 800$, then the conjecture is true.