Skip to content

Problems · Vela Mathematics Program

Narrowed toprimitive sets ×Clear all

Problem ledger

9 problemsGraph view
declared open · formalized · $500erdos:143
True ↔ ∀ (A : Set ℝ), Erdos143.WellSeparatedSet A → Filter.liminf (fun x => ↑(A ∩ Set.Icc 1 x).ncard / x) Filter.atTop = 0
primitive setsN/A2 sources
declared proved (Lean) · formalizederdos:164
True ↔ ∀ (A : Set ℕ), (∀ a ∈ A, 2 ≤ a) → Erdos1196.IsPrimitive A → ∑' (a : ↑A), 1 / (↑↑a * Real.log ↑↑a) ≤ ∑' (p : ↑{p | Nat.Prime p}), 1 / (↑↑p * Real.log ↑↑p)
number theoryprimitive setsA1372455 sources
declared open · formalizederdos:486
True ↔ ∀ (X : (n : ℕ) → Set (ZMod n)), ∃ d, {m | ∀ (n : ℕ), ↑m ∉ X n}.HasLogDensity d
number theoryprimitive setsN/A2 sources
declared solvederdos:858
Erdős problem 858
number theoryprimitive setsN/A4 sources
declared open · formalizederdos:872
True ↔ ∃ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos872.L n) ≥ ε * ↑n
number theoryprimitive setspossible3 sources
declared solvederdos:882
Erdős problem 882
number theoryprimitive setspossible
declared openerdos:892
Erdős problem 892
number theoryprimitive setsN/A
declared proved (Lean) · formalizederdos:1196
Bounds the weighted sum ∑1/(alog⁡a)\sum 1/(a \log a) taken over primitive sets of integers (sets where no element divides another).
number theoryprimitive setspossible6 sources
declared provederdos:1217
Erdős problem 1217
number theorydivisorsprimitive setsN/A3 sources

Search problems.science

Find a Problem, Result, source, or page