Skip to content

Problems · Vela Mathematics Program

Narrowed toproved (Lean) ×source:gpt-erdos ×Clear all

Problem ledger

4 problemsGraph view
declared proved (Lean) · formalizederdos:281
True ↔ ∀ (n : ℕ → ℕ), StrictMono n → (∀ (i : ℕ), 0 < n i) → (∀ (a : Erdos281.ResidueChoice n), (Erdos281.avoidAll n a).HasIntDensity 0) → ∀ (ε : ℝ), 0 < ε → ∃ k, ∀ (a : Erdos281.ResidueChoice n), ∃ d, (Erdos281.avoidPrefix n a k).HasIntDensity d ∧ d < ε
number theorycovering systemsN/A7 sources
declared proved (Lean) · formalizederdos:369
True ↔ ∀ (ε : ℝ), 0 < ε → ∀ (k : ℕ), 2 ≤ k → ∀ᶠ (n : ℕ) in Filter.atTop, ∃ a, n / 2 ≤ a + 1 ∧ a + k ≤ n ∧ ∀ j < k, ∀ p ∈ (a + 1 + j).primeFactors, ↑p ≤ ↑n ^ ε
number theoryN/A7 sources
declared proved (Lean) · formalizederdos:1014
∀ (k : ℕ), 3 ≤ k → Filter.Tendsto (fun l => ↑R(k, l + 1) / ↑R(k, l)) Filter.atTop (nhds 1)
graph theorypossible7 sources
declared proved (Lean) · formalizederdos:1022
False ↔ ∃ c, Filter.Tendsto c Filter.atTop Filter.atTop ∧ ∀ (t : ℕ), Erdos1022.SparseImpliesPropertyB t (c t)
combinatoricshypergraphspossible6 sources

Search problems.science

Find a Problem, Result, source, or page