Erdős problem 36
This example calculates the value of . The set is , so the only partition is (or vice versa). The possible differences are and . The Overlap for is 1 (if ) and for also 1 (if ). The MaxOverlap is , since the Overlap is for other . Thus, .
Sources
FormalConjectures/ErdosProblems/
36.lean
Retained formal statement
An upper bound of . See [Advances in the Minimum Overlap Problem](https://doi.org/10.1006%2Fjnth.1996.0064) by *Jan Kristian Haugland*, Journal of Number Theory Volume 58, Issue 1, p 71-78, 1996
Filter.limsup Erdos36.MinOverlapQuotient Filter.atTop ≤ 0.38200298812318988SolvedStatement only, no proof