Erdős Problem 13

Reference: erdosproblems.com/13

def Erdos13.IsForbiddenTripleFree (A : Finset ℕ) : Prop

A finite set of naturals A is said to be forbidden-triple-free if for all a, b, c ∈ A, if a < min(b, c) then a does not divide b + c.

Equations

• Erdos13.IsForbiddenTripleFree A = ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, a < min b c → ¬a ∣ b + c

theorem Erdos13.erdos_13 : ∃ (C : ℝ), ∀ (N : ℕ), ∀ A ⊆ Finset.Icc 1 N, IsForbiddenTripleFree A → ↑A.card ≤ ↑N / 3 + C

If $A \subseteq \{1, ..., N\}$ is a set with no $a, b, c \in A$ such that $a | (b+c)$ and $a < \min(b,c)$, then $|A| \le N/3 + O(1)$. This has been solved by Bedert [Be23].

[Be23] Bedert, B., On a problem of Erdős and Sárközy about sequences with no term dividing the sum of two larger terms. arXiv:2301.07065 (2023).

theorem Erdos13.erdos_13_general : sorry ↔ ∀ (r : ℕ), ∃ (C : ℝ), ∀ (N : ℕ), ∀ A ⊆ Finset.Icc 1 N, (∀ a ∈ A, ∀ (b : Fin r → ℕ), (∀ (i : Fin r), b i ∈ A) → (∀ (i : Fin r), a < b i) → ¬a ∣ ∑ i : Fin r, b i) → ↑A.card ≤ ↑N / (↑r + 1) + C

A general version asks, for a fixed $r \in \mathbb{N}$, if a set $A \subseteq \{1, ..., N\}$ has no $a \in A$ and $b_1, ..., b_r \in A$ such that $a | (b_1 + ... + b_r)$ and $a < \min(b_1, ..., b_r)$, then is it true that $|A| \le N/(r+1) + O(1)$?