Back to Problems

erdos_890.variants.liminf_lower_bound

Specification

A question of Erdős and Selfridge [ErSe67], who observe that $\liminf_{n\to \infty}\sum_{0\leq i < k}\omega(n+i)\geq k+\pi(k)-1$ for every $k$. This follows from Pólya's theorem that the set of $k$-smooth integers has unbounded gaps - indeed, $n(n+1)\cdots (n+k-1)$ is divisible by all primes $\leq k$ and, provided $n$ is large, all but at most one of $n,n+1,\ldots,n+k-1$ has a prime factor $>k$ by Pólya's theorem.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement
theorem erdos_890.variants.liminf_lower_bound (k : ℕ) :
    liminf (fun n ↦ (∑ i ∈ range k, (ω (n + i) : EReal))) atTop ≥ k + π k - 1
ID: ErdosProblems__890__erdos_890.variants.liminf_lower_bound
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.