therefore
Sign up
Open navigation
All open problems
Source labels openChecked July 26, 2026

Erdős ProblemsCombinatorics

Erdős Problem 13: General

A general version asks, for a fixed r∈Nr \in \mathbb{N}, if a set A⊆{1,...,N}A \subseteq \{1, ..., N\} has no a∈Aa \in A and b1,...,br∈Ab_1, ..., b_r \in A such that a∣(b1+...+br)a | (b_1 + ... + b_r) and a<min⁡(b1,...,br)a < \min(b_1, ..., b_r), then is it true that ∣A∣≤N/(r+1)+O(1)|A| \le N/(r+1) + O(1)?

CombinatoricsAMS 5AMS 11

Mathematical statement

A general version asks, for a fixed r∈Nr \in \mathbb{N}, if a set A⊆{1,...,N}A \subseteq \{1, ..., N\} has no a∈Aa \in A and b1,...,br∈Ab_1, ..., b_r \in A such that a∣(b1+...+br)a | (b_1 + ... + b_r) and a<min⁡(b1,...,br)a < \min(b_1, ..., b_r), then is it true that ∣A∣≤N/(r+1)+O(1)|A| \le N/(r+1) + O(1)?

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

erdos_13.variants.general

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem erdos_13.variants.general : answer(sorry) ↔ ∀ r : ℕ, ∃ C : ℝ, ∀ N : ℕ,    ∀ A ⊆ Icc 1 N,    (∀ a ∈ A, ∀ (b : Fin r → ℕ), (∀ i, b i ∈ A) → (∀ i, a < b i) →      ¬ (a ∣ ∑ i, b i)) →    (A.card : ℝ) ≤ (N : ℝ) / (r + 1) + C := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References

Pinned Formal Conjectures sourceformalizationerdosproblems.com/13background