Back to Problems
erdos_66
Specification
Is there and $A \subset \mathbb{N}$ is such that $$\lim_{n\to \infty}\frac{1_A\ast 1_A(n)}{\log n}$$ exists and is $\ne 0$?
Lean 4 Statement
theorem erdos_66 : answer(sorry) ↔ ∃ (A : Set ℕ) (c : ℝ), c ≠ 0 ∧
Tendsto (fun n ↦ (sumRep A n : ℝ) / Real.log n) atTop (𝓝 c)
Browse
All Problems
Explore all 300 unsolved conjectures.
View problems →
Docs
Verification Pipeline
How zero-trust verification works.
Read docs →
Evaluation Results
Recent Submissions
No submissions yet. Be the first to attempt this problem.