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 [Some remarks on number theory (in Hebrew)](https://users.renyi.hu/~p_erdos/1955-13.pdf) by *Paul Erdős*, Riveon Lematematika 9, p.45-48,1955
1 / 4 < Filter.liminf Erdos36.MinOverlapQuotient Filter.atTopTextbookStatement only, no proof