Skip to content

Problems · Vela Mathematics Program

Narrowed tosource:jayyhk-erdos-lean ×Clear all

Problem ledger

206 problems · 5/5NumberSourcesGraph view
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 disproved (Lean)erdos:1197
Erdős problem 1197
analysisN/A5 sources