Skip to content

Problems · Vela Mathematics Program

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

Problem ledger

5 problemsGraph view
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 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 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

Search problems.science

Find a Problem, Result, source, or page