Skip to content
Home
Problems
Updates
Vela Mathematics Program
/
Problems
/
890
Search or jump
⌘K
Overview
Problem ledger
Claims
Proposed changes
Commits
Reproduce
Problem
erdos:890
sorry ↔ ∀ k ≥ 1, Filter.liminf (fun n => ∑ i ∈ Finset.range k, ↑(Erdos890.omegaGt k (n + i))) Filter.atTop ≤ ↑k
Open Current State
Declared status
open
Formalization
formalized
Subjects
number theory
·
primes
OEIS
N/A
Sources
source:erdos-problems
·
source:formal-conjectures
Statement
www.erdosproblems.com
Matching claims
0
No direct claims
This problem has no directly related claim record.
Browse this Repository’s Claims