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
For n = 4 the best splitting of {1, …, 8} still has maximum overlap 2.
Erdos36.M 4 = 2TestStatement only, no proof