Back to Problems

minimum_overlap.variants.upper.MRS_1956

Specification

An upper bound of $\frac 2 5$. See [Minimal overlapping under translation.](https://projecteuclid.org/journals/bulletin-of-the-american-mathematical-society/volume-62/issue-6) by *T. S. Motzkin*, *K. E. Ralston* and *J. L. Selfridge*, in "The summer meeting in Seattle" by *V. L. Klee Jr.*, Bull. Amer. Math. Soc.62, p. 558, 1956

Actions

Submit a Proof

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

Submit Proof
Lean 4 Statement
theorem minimum_overlap.variants.upper.MRS_1956 :
    atTop.limsup MinOverlapQuotient ≤ (2 : ℝ) / 5
ID: ErdosProblems__36__minimum_overlap.variants.upper.MRS_1956
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.