Skip to content

Problems · Vela Mathematics Program

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

Problem ledger

258 problems · 6/6NumberSourcesGraph view
declared open · formalizederdos:1139
True ↔ Filter.limsup (fun k => (↑↑(Nat.nth (fun n => 0 < n ∧ ArithmeticFunction.cardFactors n ≤ 2) (k + 1)) - ↑↑(Nat.nth (fun n => 0 < n ∧ ArithmeticFunction.cardFactors n ≤ 2) k)) / ↑(Real.log (↑k + 1))) Filter.atTop = ⊤
number theoryprimesA037143 · A1010413 sources
declared disproved (Lean) · formalizederdos:1141
False ↔ Infinite ↑{n | Erdos1141.Erdos1141Prop n}
number theoryprimesA2145836 sources
declared proved (Lean) · formalizederdos:1148
True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, Erdos1148.Erdos1148Prop n
number theoryA390380 · A3931686 sources
declared solved (Lean) · formalizederdos:1190
∀ (ε : ℝ), 0 < ε → ∀ᶠ (m : ℕ) in Filter.atTop, scaleL m ^ (-1 - ε) < Erdos1190.eps m ∧ Erdos1190.eps m < scaleL m ^ (-1 + ε)
number theorycovering systemspossible6 sources
declared solved (Lean) · formalizederdos:1193
False ↔ ∀ (A : Set ℕ) (g : ℕ → ℕ), Monotone g → (∀ (n : ℕ), 0 < g n) → {n | AdditiveCombinatorics.sumRep A n = g n}.lowerDensity = 0
additive combinatoricsN/A5 sources
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 open · formalizederdos:1201
Is it true that for every ϵ,η>0\epsilon,\eta>0 there exists a kk such that the density of nn for which P(n(n+1)⋯(n+k))>n1−ϵP(n(n+1)\cdots(n+k))>n^{1-\epsilon} is at least 1−η1-\eta, where P(m)P(m) is the greatest prime divisor of mm? A short argument via the Matomäki-Radziwiłł theorem establishes the lower-density version.
number theoryprimespossible4 sources
declared open · formalizederdos:1209
False ↔ ∃ f, ∀ (a : ℕ → ℕ), StrictMono a → (∀ (k : ℕ), f k ≤ a k) → (∃ n, ∀ (k : ℕ), Nat.Prime (n + a k)) → {n | ∀ (k : ℕ), Nat.Prime (n + a k)}.Infinite
number theorypossible3 sources

Search problems.science

Find a Problem, Result, source, or page