Skip to content

Problems · Vela Mathematics Program

Narrowed toopen ×unit fractions ×Clear all

Problem ledger

17 problemsGraph view
declared openerdos:148
Erdős problem 148
number theoryunit fractionsA076393 · A006585
declared open · formalizederdos:282
∀ {x : ℚ}, x ∈ Set.Ioo 0 1 → Odd x.den → Erdos282.greedyUnitFractionRem {n | Odd n} x =ᶠ[Filter.atTop] 0
number theoryunit fractionsN/A2 sources
declared open · formalizederdos:288
sorry ↔ {I | ∀ (j : Fin 2), (I j).1 ≤ (I j).2 ∧ ∃ n, ∑ j, ∑ nⱼ ∈ (Set.Icc (I j).1 (I j).2).toFinset, (↑↑nⱼ)⁻¹ = ↑↑n}.Finite
number theoryunit fractionsN/A3 sources
declared open · formalizederdos:289
True ↔ ∀ᶠ (k : ℕ) in Filter.atTop, ∃ I, (∀ (i : Fin k), (I i).1 < (I i).2) ∧ (∀ (i j : Fin k), i ≠ j → (I i).2 < (I j).1 ∨ (I j).2 < (I i).1) ∧ ∑ i, ∑ n ∈ Finset.Icc (I i).1 (I i).2, (↑n)⁻¹ = 1
number theoryunit fractionsN/A2 sources
declared open · formalizederdos:291
Erdos291.L 1 = 1 ∧ Erdos291.L 2 = 2 ∧ Erdos291.L 3 = 6 ∧ Erdos291.L 4 = 12
number theoryunit fractionsA1105663 sources
declared openerdos:293
Erdős problem 293
number theoryunit fractionspossible
declared open · formalizederdos:295
sorry ↔ Filter.Tendsto (fun N => ↑(Erdos295.k N) - (Real.exp 1 - 1) * ↑N) Filter.atTop Filter.atTop
number theoryunit fractionsA1928812 sources
declared openerdos:301
Erdős problem 301
number theoryunit fractionsA390394
declared open · formalizederdos:302
∀ (f : ℕ → ℕ), (∀ (N : ℕ), Erdos302.IsMaxNoTripleCard N (f N)) → Filter.Tendsto (fun N => ↑(f N) / ↑N) Filter.atTop (nhds sorry)
number theoryunit fractionsA3903953 sources
declared open · formalizederdos:304
∀ {a b : ℕ}, 1 ∈ Erdos304.unitFractionExpressible a b → a ∣ b
number theoryunit fractionsA097847 · A0978492 sources
declared open · formalizederdos:306
If a/b∈Q>0a/b \in \mathbb{Q}_{>0} and bb is squarefree, can a/ba/b always be written as a finite sum of reciprocals of distinct products of two distinct primes?
number theoryunit fractionsN/A4 sources
declared openerdos:311
Erdős problem 311
number theoryunit fractionsN/A
declared open · formalizederdos:312
True ↔ ∃ c, 0 < c ∧ ∀ (K : ℝ), 1 < K → ∃ N₀, ∀ (n : ℕ) (a : Fin n → ℕ), n ≥ N₀ ∧ ∑ i, (↑(a i))⁻¹ > K → ∃ S, 1 - Real.exp (-(c * K)) < ∑ i ∈ S, (↑(a i))⁻¹ ∧ ∑ i ∈ S, (↑(a i))⁻¹ ≤ 1
number theoryunit fractionsN/A2 sources
declared open · formalizederdos:313
sorry ↔ Erdos313.erdos313Solutions.Infinite
number theoryunit fractionsA0543772 sources
declared open · formalizederdos:317
∀ᶠ (n : ℕ) in Filter.atTop, ∀ (δ : Fin n → ℚ), δ '' Set.univ ⊆ {-1, 0, 1} → |∑ k, δ k / (↑↑k + 1)| ≠ 0 → |∑ k, δ k / (↑↑k + 1)| ≥ 1 / ↑((Finset.Icc 1 n).lcm id)
number theoryunit fractionsN/A2 sources
declared open · formalizederdos:319
∀ (N : ℕ), IsGreatest {x | ∃ A, ∃ (_ : A ⊆ Finset.Icc 1 N) (_ : ∃ δ, ∑ n ∈ A, ↑↑(δ n) / ↑n = 0 ∧ ∀ A' ⊂ A, A'.Nonempty → ∑ n ∈ A', ↑↑(δ n) / ↑n ≠ 0), A.card = x} sorry
number theoryunit fractionspossible2 sources
declared openerdos:327
Erdős problem 327
number theoryunit fractionsA3849272 sources

Search problems.science

Find a Problem, Result, source, or page