Skip to content

Problems · Vela Mathematics Program

Narrowed toproved ×source:erdos-ai-contributions-wiki ×Clear all

Problem ledger

11 problemsGraph view
declared proved · $500erdos:21
Erdős problem 21
combinatoricsintersecting familyA3915992 sources
declared proved · formalizederdos:152
True ↔ Filter.Tendsto Erdos152.f Filter.atTop Filter.atTop
sidon setsN/A4 sources
declared proved · formalizederdos:358
True ↔ ∃ A, StrictMono A ∧ Filter.Tendsto (Erdos358.f A) Filter.atTop Filter.atTop
number theoryadditive basisprimespossible3 sources
declared provederdos:380
Erdős problem 380
number theoryA070003 · A388654 · A387054 · A3891003 sources
declared proved · formalizederdos:480
True ↔ ∀ (x : ℕ → ℝ), (∀ (n : ℕ), x n ∈ Set.Icc 0 1) → ⨅ n, Filter.liminf (fun m => ↑↑n * |x (m + ↑n) - x m|) Filter.atTop ≤ 1 / √5
number theoryN/A3 sources
declared proved · formalizederdos:851
∀ ε ∈ Set.Ioo 0 1, ∃ r d, (Erdos851.TwoPowAddSet r).HasDensity d ∧ 1 - ε ≤ d
number theoryN/A4 sources
declared provederdos:863
Erdős problem 863
number theorysidon setsadditive combinatoricsN/A3 sources
declared provederdos:986
Erdős problem 986
graph theoryramsey theoryA000791 · A0594423 sources
declared proved · formalizederdos:987
True ↔ ∀ (x : ℕ → ℝ), (∀ (j : ℕ), x j ∈ Set.Ioo 0 1) → Filter.limsup (fun k => Erdos987.A x k) Filter.atTop = ⊤
analysisdiscrepancyN/A4 sources
declared provederdos:1153
Erdős problem 1153
analysispolynomialsN/A3 sources
declared provederdos:1217
Erdős problem 1217
number theorydivisorsprimitive setsN/A3 sources

Search problems.science

Find a Problem, Result, source, or page