Skip to content

Problems · Vela Mathematics Program

Narrowed toproved (Lean) ×unit fractions ×Clear all

Problem ledger

11 problemsGraph view
declared proved (Lean) · formalizederdos:45
True ↔ ∀ (k : ℕ), 2 ≤ k → ∃ n, ∀ (colouring : ℕ → Fin k), ∃ colour, ∃ D' ⊆ {d ∈ n.divisors | 1 < d ∧ d < n}, (∀ d ∈ D', colouring d = colour) ∧ D'.reciprocalSum = 1
number theoryunit fractionsramsey theorypossible4 sources
declared proved (Lean) · formalizederdos:46
True ↔ ∀ (𝓒 : ℕ → ℕ), (Set.range 𝓒).Finite → ∃ S, (∀ n ∈ S, 2 ≤ n) ∧ ∑ n ∈ S, 1 / ↑n = 1 ∧ (𝓒 '' ↑S).Subsingleton
number theoryunit fractionsramsey theoryN/A4 sources
declared proved (Lean) · formalized · $100erdos:47
True ↔ ∀ (δ : ℝ), 0 < δ → ∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, δ * Real.log ↑N < A.reciprocalSum → ∃ S ⊆ A, S.reciprocalSum = 1
number theoryunit fractionsN/A4 sources
declared proved (Lean) · formalizederdos:283
True ↔ ∀ (p : Polynomial ℤ), Erdos283.Condition p
number theoryunit fractionsA3807916 sources
declared proved (Lean) · formalizederdos:290
True ↔ ∀ (a : ℕ), 1 ≤ a → ∃ b, a < b ∧ Erdos290.harmonicDen a (b + 1) < Erdos290.harmonicDen a b
number theoryunit fractionsA3750815 sources
declared proved (Lean) · formalizederdos:296
(∀ (N k : ℕ), Erdos296.HasDisjointUnitDecomps N k → ↑k ≤ Erdos296.recipSum (Finset.Icc 1 N)) ∧ ∀ (ε : ℝ), 0 < ε → ε < 1 → ∀ᶠ (N : ℕ) in Filter.atTop, Erdos296.HasDisjointUnitDecomps N ⌊(1 - ε) * Real.log ↑N⌋₊
number theoryunit fractionspossible5 sources
declared proved (Lean) · formalizederdos:298
True ↔ ∀ (A : Set ℕ), 0 ∉ A → 0 < A.upperDensity → ∃ S, ↑S ⊆ A ∧ ∑ n ∈ S, 1 / ↑n = 1
number theoryunit fractionsN/A4 sources
declared proved (Lean) · formalizederdos:303
True ↔ ∀ (𝓒 : ℤ → ℤ), (Set.range 𝓒).Finite → ∃ a b c, [a, b, c, 0].Nodup ∧ 1 / ↑a = 1 / ↑b + 1 / ↑c ∧ (𝓒 '' {a, b, c}).Subsingleton
number theoryunit fractionsN/A5 sources
declared proved (Lean) · formalizederdos:314
True ↔ Filter.liminf (fun n => ↑n ^ 2 * Erdos314.epsilon n) Filter.atTop = 0
number theoryunit fractionsN/A5 sources
declared proved (Lean) · formalizederdos:315
True ↔ ∀ (a : ℕ → ℕ), (∀ (i : ℕ), 0 < a i) → StrictMono a → (∃ i, a i ≠ Erdos315.u i + 1) → ∑' (i : ℕ), 1 / ↑(a i) = 1 → Filter.liminf (fun i => ↑(a i) ^ (1 / 2) ^ (i + 1)) Filter.atTop < Erdos315.c₀
number theoryunit fractionsA000058 · A0763935 sources
declared proved (Lean) · formalizederdos:355
True ↔ ∃ A, IsLacunary A ∧ ∃ u v, u < v ∧ ∀ (q : ℚ), ↑q ∈ Set.Ioo u v → q ∈ {x | ∃ A', ∃ (_ : ↑A' ⊆ Set.range A), ∑ a ∈ A', 1 / ↑a = x}
number theoryunit fractionsN/A5 sources

Search problems.science

Find a Problem, Result, source, or page