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

Erdős ProblemsCombinatorics

Erdős Problem 312

Does there exist a constant c > 0 such that, for any K > 1, whenever A is a sufficiently large finite multiset of integers with ∑n∈A1/n>K\sum_{n \in A} 1/n > K there exists some S⊆AS \subseteq A such that 1−exp⁡(−(c∗K))<∑n∈S1/n≤11 - \exp(-(c*K)) < \sum_{n \in S} 1/n \le 1?

CombinatoricsAMS 5AMS 11

Mathematical statement

Does there exist a constant c > 0 such that, for any K > 1, whenever A is a sufficiently large finite multiset of integers with ∑n∈A1/n>K\sum_{n \in A} 1/n > K there exists some S⊆AS \subseteq A such that 1−exp⁡(−(c∗K))<∑n∈S1/n≤11 - \exp(-(c*K)) < \sum_{n \in S} 1/n \le 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_312

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem erdos_312 :    answer(sorry) ↔    ∃ (c : ℝ), 0 < c ∧      ∀ (K : ℝ), 1 < K →        ∃ (N₀ : ℕ),          ∀ (n : ℕ) (a : Fin n → ℕ),            (n ≥ N₀ ∧ (∑ i : Fin n, (a i : ℝ)⁻¹) > K) →              ∃ (S : Finset (Fin n)),                1 - Real.exp (-(c * K)) < (∑ i ∈ S, (a i : ℝ)⁻¹) ∧                ∑ i ∈ S, (a i : ℝ)⁻¹ ≤ 1 := 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/312background