Erdős problem 47
If and is sufficiently large in terms of , and is such that then must there exist such that ?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/47.leanTrue ↔ ∀ (δ : ℝ), 0 < δ → ∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, δ * Real.log ↑N < A.reciprocalSum → ∃ S ⊆ A, S.reciprocalSum = 1Proof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:47 - PLBY Lean proofs
ErdosProblems.Erdos47