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

Erdős ProblemsNumber theory

Erdős Problem 123: Powers 2 3 5 Snug

In [Er92b] Erdős makes the stronger conjecture (for a=2a=2, b=3b=3, and c=5c=5) that, for any ϵ>0\epsilon>0, all large integers nn can be written as the sum of distinct integers b1<⋯<btb_1<\cdots <b_t of the form 2k3l5m2^k3^l5^m where bt<(1+ϵ)b1b_t<(1+\epsilon)b_1.

Number theoryAMS 11

Mathematical statement

In [Er92b] Erdős makes the stronger conjecture (for a=2a=2, b=3b=3, and c=5c=5) that, for any ϵ>0\epsilon>0, all large integers nn can be written as the sum of distinct integers b1<⋯<btb_1<\cdots <b_t of the form 2k3l5m2^k3^l5^m where bt<(1+ϵ)b1b_t<(1+\epsilon)b_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_123.variants.powers_2_3_5_snug

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem erdos_123.variants.powers_2_3_5_snug :    answer(sorry) ↔ ∀ ε > 0, ∀ᶠ n in atTop,      ∃ A : Finset ℕ, (A : Set ℕ) ⊆ ↑(powers 2) * ↑(powers 3) * ↑(powers 5) ∧ IsSnug ε A ∧        ∑ x ∈ A, x = 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/123background