Skip to content

Problems · Vela Mathematics Program

Narrowed toformalized ×discrepancy ×Clear all

Problem ledger

5 problemsGraph view
declared proved · formalized · $500erdos:67
∀ (f : ℕ → ↥{-1, 1}) (C : ℝ), 0 < C → ∃ d ≥ 1, ∃ m ≥ 1, C < |∑ k ∈ Finset.Icc 1 m, ↑(f (k * d))|
discrepancyA181740 · A2376952 sources
declared proved (Lean) · formalizederdos:178
True ↔ ∀ (a : ℕ → ℕ → ℕ), (∀ (i : ℕ), StrictMono (a i)) → ∃ f, (∀ (n : ℕ), f n = 1 ∨ f n = -1) ∧ ∀ (d : ℕ), ∃ C, ∀ (m i : ℕ), i < d → |∑ j ∈ Finset.range m, f (a i j)| ≤ ↑C
discrepancyN/A5 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 proved (Lean) · formalizederdos:997
True ↔ ∀ (α : ℝ), ¬Erdos997.IsWellDistributed fun n => Int.fract (α * ↑(Nat.nth Nat.Prime n))
analysisdiscrepancyprimesN/A6 sources
declared solved (Lean) · formalizederdos:1028
(fun n => ↑(Erdos1028.H n)) =Θ[Filter.atTop] fun n => ↑n ^ (3 / 2)
graph theorydiscrepancypossible5 sources

Search problems.science

Find a Problem, Result, source, or page