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

Erdős ProblemsCombinatorics

Erdős Problem 865: Sos

Erdős and Sós conjectured that fk(N)∼12(1+∑1≤r≤k−214r)Nf_k(N)\sim \frac{1}{2}\left(1+\sum_{1\leq r\leq k-2}\frac{1}{4^r}\right) N, where fk(N)f_k(N) is the minimal size of a subset of {1,…,N}\{1, \dots, N\} guaranteeing kk elements have all pairwise sums in the set.

CombinatoricsAMS 5AMS 11

Mathematical statement

Erdős and Sós conjectured that fk(N)∼12(1+∑1≤r≤k−214r)Nf_k(N)\sim \frac{1}{2}\left(1+\sum_{1\leq r\leq k-2}\frac{1}{4^r}\right) N, where fk(N)f_k(N) is the minimal size of a subset of {1,…,N}\{1, \dots, N\} guaranteeing kk elements have all pairwise sums in the set.

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_865.variants.sos

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem erdos_865.variants.sos :    ∀ᵉ (k : ℕ) (hk : 2 ≤ k),    (fun N ↦ (f N k : ℝ)) ~[atTop] (fun N ↦ (1 / 2 : ℝ) * (1 + ∑ r ∈ Icc 1 (k - 2),      (1 / 4 : ℝ) ^ r) * N) := 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/865background