FormalConjectures/Wikipedia/MinimalOverlapProblem.lean

Minimum Overlap Problem

The minimum overlap problem asks for the limit of the minimum, over all splittings of $\{1, \ldots, 2n\}$ into two sets $A$ and $B$ of equal size, of the maximum number of representations of any integer $k$ as $a - b$ with $a \in A$, $b \in B$, divided by $n$.

Reference: Wikipedia

This file points to the canonical formalization in FormalConjectures.ErdosProblems.«36».