Back to Problems
minimum_overlap.variants.upper.erdos_1955
Specification
The example (with $N$ even), $A = \{\frac N 2 + 1, \dots, \frac{3N}{2}\}$ shows an upper bound of $\frac 1 2$.
Lean 4 Statement
theorem minimum_overlap.variants.upper.erdos_1955 :
atTop.limsup MinOverlapQuotient ≤ (1 : ℝ) / 2
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.