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
A lower bound of . See [On the intersection of a linear set with the translation of its complement](https://bibliotekanauki.pl/articles/969027) by *Stanisław Świerczkowski1*, Colloquium Mathematicum 5(2), p. 185-197, 1958
(4 - 6 ^ (1 / 2)) / 5 < Filter.liminf Erdos36.MinOverlapQuotient Filter.atTopSolvedStatement only, no proof