Erdős minimum overlap problem

DefinitionOverlap count of two finite sets of integers#✓fully proved

For finite sets \(A, B \subseteq \mathbb{Z}\) and an integer \(k\), the overlap of \(A\) and \(B\) at \(k\) is the number of pairs \((a, b) \in A \times B\) with \(a - b = k\).

def Overlap (A B : Finset ℤ) (k : ℤ) : ℕ :=
  ((A.product B).filter fun (a, b) => a - b = k).card

Used by 4

Used byUniversal asymptotic lower bound for discrete overlaps · Maximum overlap · The maximum overlap is attained · Overlaps are bounded by the maximum overlap

DefinitionMaximum overlap#✓fully proved

For finite sets \(A, B \subseteq \mathbb{Z}\), the maximum overlap of \(A\) and \(B\) is the natural number obtained as the supremum over all integers \(k\) of \(\#\{(a, b) \in A \times B : a - b = k\}\).

noncomputable def MaxOverlap (A B : Finset ℤ) : ℕ :=
  iSup (Overlap A B)

Uses 1 · Used by 6

Statement usesOverlap count of two finite sets of integers

Used byBalanced partitions of \(\{1, \dots, 2n\}\) exist · Erdős minimum overlap function · The minimum overlap is attained · The minimum overlap bounds every balanced partition · The maximum overlap is attained · Overlaps are bounded by the maximum overlap

DefinitionErdős minimum overlap function#✓fully proved

For a natural number \(n\), \(M(n)\) is the least value of the maximum overlap of \(A\) and \(B\), the supremum over \(k \in \mathbb{Z}\) of \(\#\{(a, b) \in A \times B : a - b = k\}\), taken over all pairs of disjoint finite sets \(A, B \subseteq \mathbb{Z}\) with \(A \cup B = \{1, \dots, 2n\}\) and \(|A| = |B|\).

noncomputable def M (n : ℕ) : ℕ :=
  sInf {MaxOverlap A B | (A : Finset ℤ) (B : Finset ℤ)
    (_disjoint : Disjoint A B)
    (_union : A ∪ B = Finset.Icc (1 : ℤ) (2 * n))
    (_same_card : A.card = B.card)}

 /-- Every overlap count is bounded by the maximum overlap. -/

Uses 1 · Used by 3

Statement usesMaximum overlap

Used byThe minimum overlap is attained · The minimum overlap bounds every balanced partition · Normalized minimum overlap

TheoremOverlaps are bounded by the maximum overlap#✓fully proved

For finite sets \(A, B \subseteq \mathbb{Z}\) and every integer \(k\), the overlap \(\#\{(a, b) \in A \times B : a - b = k\}\) is at most the maximum overlap of \(A\) and \(B\).

theorem Overlap_le_MaxOverlap (A B : Finset ℤ) (k : ℤ) :
    Overlap A B k ≤ MaxOverlap A B

Uses 2

Statement usesMaximum overlap · Overlap count of two finite sets of integers

TheoremThe maximum overlap is attained#✓fully proved

For finite sets \(A, B \subseteq \mathbb{Z}\) there is an integer \(k\) such that the maximum overlap of \(A\) and \(B\), the supremum over \(j \in \mathbb{Z}\) of \(\#\{(a, b) \in A \times B : a - b = j\}\), equals \(\#\{(a, b) \in A \times B : a - b = k\}\).

theorem MaxOverlap_attained (A B : Finset ℤ) :
    ∃ k : ℤ, MaxOverlap A B = Overlap A B k

Uses 2

Statement usesMaximum overlap · Overlap count of two finite sets of integers

TheoremBalanced partitions of \(\{1, \dots, 2n\}\) exist#✓fully proved

For every natural number \(n\), the set of maximum overlaps of \(A\) and \(B\), taken over all pairs of disjoint finite sets of integers \(A\) and \(B\) with \(A \cup B = \{1, \dots, 2n\}\) and \(|A| = |B|\), is nonempty.

For example, \(A = \{1, \dots, n\}\) and \(B = \{n + 1, \dots, 2n\}\) is such a pair.

theorem balancedPartition_nonempty (n : ℕ) :
    {MaxOverlap A B | (A : Finset ℤ) (B : Finset ℤ)
      (_disjoint : Disjoint A B)
      (_union : A ∪ B = Finset.Icc (1 : ℤ) (2 * n))
      (_same_card : A.card = B.card)}.Nonempty

Uses 1 · Used by 1

Statement usesMaximum overlap

Used byThe minimum overlap is attained

TheoremThe minimum overlap is attained#✓fully proved

For every natural number \(n\) there are disjoint finite sets \(A, B \subseteq \mathbb{Z}\) with \(A \cup B = \{1, \dots, 2n\}\) and \(|A| = |B|\) such that the minimum overlap \(M(n)\) equals the maximum overlap of \(A\) and \(B\), the supremum over \(k \in \mathbb{Z}\) of \(\#\{(a, b) \in A \times B : a - b = k\}\).

theorem M_attained (n : ℕ) :
    ∃ (A B : Finset ℤ), Disjoint A B ∧
      A ∪ B = Finset.Icc (1 : ℤ) (2 * n) ∧ A.card = B.card ∧
      M n = MaxOverlap A B

Uses 3

Statement usesErdős minimum overlap function · Maximum overlap

Proof usesBalanced partitions of \(\{1, \dots, 2n\}\) exist

TheoremThe minimum overlap bounds every balanced partition#✓fully proved

Let \(n\) be a natural number and let \(A, B \subseteq \mathbb{Z}\) be disjoint finite sets with \(A \cup B = \{1, \dots, 2n\}\) and \(|A| = |B|\). Then the minimum overlap \(M(n)\) is at most the maximum overlap of \(A\) and \(B\), the supremum over \(k \in \mathbb{Z}\) of \(\#\{(a, b) \in A \times B : a - b = k\}\).

theorem M_le_MaxOverlap (n : ℕ) (A B : Finset ℤ) (hd : Disjoint A B)
    (hu : A ∪ B = Finset.Icc (1 : ℤ) (2 * n)) (hc : A.card = B.card) :
    M n ≤ MaxOverlap A B

Uses 2

Statement usesErdős minimum overlap function · Maximum overlap

DefinitionNormalized minimum overlap#✓fully proved

For a natural number \(N\), the normalized minimum overlap is the real number \(M(N) / N\), where \(M(N)\) is the Erdős minimum overlap function; for \(N = 0\) the quotient is \(0\) by the convention \(x / 0 = 0\).

noncomputable def MinOverlapQuotient (N : ℕ) : ℝ :=
  (M N : ℝ) / N

Uses 1 · Used by 1

Statement usesErdős minimum overlap function

Used byThe proposition that \(M(N)/N\) tends to \(C_{1b}\)

DefinitionUniversal asymptotic lower bound for discrete overlaps#✓fully proved

A real number \(c\) is a universal asymptotic lower bound when for every \(\varepsilon > 0\) there is a positive integer \(N_0\) such that for every \(N \ge N_0\) and all disjoint finite sets \(A, B \subseteq \mathbb{Z}\) with \(A \cup B = \{1, \dots, 2N\}\) and \(|A| = |B|\), some integer \(x\) satisfies \((c - \varepsilon) N \le \#\{(a, b) \in A \times B : a - b = x\}\).

The positive size threshold \(N_0\) is chosen before the size \(N\) and the partition.

def DiscreteUniversalLowerBound (c : ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ N₀ : ℕ, 0 < N₀ ∧
    ∀ N : ℕ, N₀ ≤ N → ∀ A B : Finset ℤ,
      Disjoint A B → A ∪ B = Finset.Icc (1 : ℤ) (2 * N) → A.card = B.card →
        ∃ x : ℤ, (c - ε) * (N : ℝ) ≤ (Overlap A B x : ℝ)

Uses 1 · Used by 1

Statement usesOverlap count of two finite sets of integers

Used byThe proposition that \(C_{1b}\) is the largest asymptotic overlap constant

DefinitionContinuous support interval#✓fully proved

The support interval of the continuous minimum-overlap problem is the closed interval \([-1, 1]\) of real numbers.

Functions in the continuous model are extended by zero outside this interval.

def continuousSupportInterval : Set ℝ := Icc (-1) 1

Used by 3

Used byAdmissible pairs for the continuous minimum-overlap problem · The continuous minimum-overlap constant is at most \(1/2\) · Continuous overlap

DefinitionTranslation interval of the continuous overlap model#✓fully proved

The translation interval of the continuous minimum-overlap model is the closed interval \([-2, 2] \subseteq \mathbb{R}\).

def continuousTranslationInterval : Set ℝ := Icc (-2) 2

Used by 2

Used byThe continuous minimum-overlap constant is at most \(1/2\) · Continuous overlap values

DefinitionContinuous overlap integrand#✓fully proved

For functions \(f, g : \mathbb{R} \to \mathbb{R}\) and real numbers \(x\) and \(t\), the overlap integrand is \(f(t)\,g(x + t)\).

def continuousOverlapIntegrand (f g : ℝ → ℝ) (x t : ℝ) : ℝ :=
  f t * g (x + t)

Used by 2

Used byThe continuous minimum-overlap constant is at most \(1/2\) · Continuous overlap

DefinitionContinuous overlap#✓fully proved

For functions \(f, g : \mathbb{R} \to \mathbb{R}\) and a translation \(x \in \mathbb{R}\), the overlap of \(f\) and \(g\) at \(x\) is \(\int_{-1}^{1} f(t)\,g(x + t)\,dt\), the integral of the overlap integrand over the support interval \([-1, 1]\).

The integral is the Lebesgue (Bochner) integral, which is \(0\) when the integrand is not integrable.

noncomputable def continuousOverlap (f g : ℝ → ℝ) (x : ℝ) : ℝ :=
  ∫ t in continuousSupportInterval, continuousOverlapIntegrand f g x t

Uses 2 · Used by 2

Statement usesContinuous overlap integrand · Continuous support interval

Used byThe continuous minimum-overlap constant is at most \(1/2\) · Continuous overlap values

DefinitionContinuous overlap values#✓fully proved

For functions \(f, g : \mathbb{R} \to \mathbb{R}\), the set of overlap values of \(f\) and \(g\) is the image of the translation interval \([-2, 2]\) under the overlap \(x \mapsto \int_{-1}^{1} f(t)\,g(x + t)\,dt\).

def continuousOverlapValues (f g : ℝ → ℝ) : Set ℝ :=
  continuousOverlap f g '' continuousTranslationInterval

Uses 2 · Used by 2

Statement usesContinuous overlap · Translation interval of the continuous overlap model

Used byThe continuous minimum-overlap constant is at most \(1/2\) · Continuous pair score

StructureAdmissible pairs for the continuous minimum-overlap problem#✓fully proved

A pair of functions \(f, g : \mathbb{R} \to \mathbb{R}\) is admissible when \(f\) and \(g\) are almost everywhere measurable with respect to Lebesgue measure, take values in \([0, 1]\) at every point, vanish at every point outside the support interval \([-1, 1]\), satisfy \(f(t) + g(t) = 1\) for every \(t \in [-1, 1]\), and satisfy \(\int_{\mathbb{R}} f(t)\,dt = 1\).

Since measurability is only required almost everywhere, Lebesgue-null modifications of Borel functions are included. Integrability and the bounds on the overlap follow from these conditions.

structure ContinuousAdmissible (f g : ℝ → ℝ) : Prop where
  measurable_f : AEMeasurable f volume
  measurable_g : AEMeasurable g volume
  range_f : ∀ t : ℝ, f t ∈ Icc (0 : ℝ) 1
  range_g : ∀ t : ℝ, g t ∈ Icc (0 : ℝ) 1
  zero_outside_f : ∀ t : ℝ, t ∉ continuousSupportInterval → f t = 0
  zero_outside_g : ∀ t : ℝ, t ∉ continuousSupportInterval → g t = 0
  complementary : ∀ t ∈ continuousSupportInterval, f t + g t = 1
  integral_f : (∫ t : ℝ, f t) = 1

Uses 1 · Used by 2

Statement usesContinuous support interval

Used byThe continuous minimum-overlap constant is at most \(1/2\) · Universal lower bound in the continuous overlap model

DefinitionContinuous pair score#✓fully proved

For functions \(f, g : \mathbb{R} \to \mathbb{R}\), the pair score of \(f\) and \(g\) is the supremum of the overlap values \(\int_{-1}^{1} f(t)\,g(x + t)\,dt\) over the translations \(x \in [-2, 2]\).

As with every supremum of real numbers here, it is \(0\) when the set is not bounded above; for admissible pairs the overlap values lie in \([0, 1]\).

noncomputable def continuousPairScore (f g : ℝ → ℝ) : ℝ :=
  sSup (continuousOverlapValues f g)

Uses 1 · Used by 2

Statement usesContinuous overlap values

Used byThe continuous minimum-overlap constant is at most \(1/2\) · Universal lower bound in the continuous overlap model

DefinitionUniversal lower bound in the continuous overlap model#✓fully proved

Call a pair of functions \(f, g : \mathbb{R} \to \mathbb{R}\) admissible when \(f\) and \(g\) are almost everywhere measurable, take values in \([0, 1]\), vanish outside \([-1, 1]\), satisfy \(f + g = 1\) on \([-1, 1]\), and \(\int_{\mathbb{R}} f = 1\), and let the pair score \(S(f, g)\) be the supremum over \(x \in [-2, 2]\) of \(\int_{-1}^{1} f(t)\, g(x + t)\, dt\). A real number \(c\) is a universal lower bound when \(c \le S(f, g)\) for every admissible pair \((f, g)\).

def ContinuousUniversalLowerBound (c : ℝ) : Prop :=
  ∀ (f g : ℝ → ℝ), ContinuousAdmissible f g → c ≤ continuousPairScore f g

Uses 2 · Used by 2

Statement usesAdmissible pairs for the continuous minimum-overlap problem · Continuous pair score

Used byThe continuous Erdős minimum-overlap constant · The continuous minimum-overlap constant is at most \(1/2\)

DefinitionThe continuous Erdős minimum-overlap constant#✓fully proved

For an admissible pair \((f, g)\) let \(S(f, g)\) be its pair score, the supremum over \(x \in [-2, 2]\) of \(\int_{-1}^{1} f(t)\,g(x + t)\,dt\). The continuous minimum-overlap constant \(C_{1b}\) is the supremum of the set of real numbers \(c\) such that \(c \le S(f, g)\) for every admissible pair \((f, g)\).

noncomputable def continuousMinimumOverlapConstant : ℝ :=
  sSup continuousValidLowerBounds

Sources

• Optimization Problems, Constant 1b.

Uses 1 · Used by 1

Statement usesUniversal lower bound in the continuous overlap model

Used byNotation \(C_{1b}\)

AbbreviationNotation \(C_{1b}\)#✓fully proved

We write \(C_{1b}\) for the continuous Erdős minimum-overlap constant.

noncomputable abbrev C₁ᵦ : ℝ := continuousMinimumOverlapConstant

Uses 1 · Used by 19

Statement usesThe continuous Erdős minimum-overlap constant

Used byThe proposition that \(C_{1b}\) is the largest asymptotic overlap constant · The proposition that \(M(N)/N\) tends to \(C_{1b}\) · The continuous minimum-overlap constant is at most \(1/2\) · The proposition \(1/4 \le C_{1b}\) · The proposition \(\sqrt{4 - \sqrt{15}} \le C_{1b}\) · The proposition \((4 - \sqrt{6})/5 \le C_{1b}\) · Scherk's lower bound for the minimum-overlap constant (statement) · White's lower bound for the minimum-overlap constant (statement) · Erdős's upper bound \(1/2\) for the minimum-overlap constant (statement) · Erdős's unpublished upper bound \(4/9\) for the minimum-overlap constant (statement) · AlphaEvolve upper bound for the minimum-overlap constant (statement) · Statement of Haugland's 1996 upper bound for the minimum-overlap constant · Statement of Haugland's 2016 upper bound for the minimum-overlap constant · Statement of Haugland's unpublished 1993 upper bound for the minimum-overlap constant · Statement of the Motzkin–Ralston–Selfridge upper bound \(5/12\) for the minimum-overlap constant · Statement of the Motzkin–Ralston–Selfridge upper bound \(0.4\) for the minimum-overlap constant · Together AI 2026 upper bound statement for the minimum overlap constant · TTT-Discover 2026 upper bound statement for the minimum overlap constant · SimpleTES 2026 upper bound statement for the minimum overlap constant

TheoremThe continuous minimum-overlap constant is at most \(1/2\)#✓fully proved

The continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(C_{1b} \le 1/2\).

The bound is witnessed by the admissible pair \(f = g\) with value \(1/2\) on \([-1, 1]\) and \(0\) elsewhere.

theorem continuousMinimumOverlapConstant_le_half : C₁ᵦ ≤ (1 : ℝ) / 2

Uses 9

Statement usesNotation \(C_{1b}\)

Proof usesAdmissible pairs for the continuous minimum-overlap problem · Universal lower bound in the continuous overlap model · Continuous overlap · Continuous overlap integrand · Continuous overlap values · Continuous pair score · Continuous support interval · Translation interval of the continuous overlap model

DefinitionThe proposition that \(M(N)/N\) tends to \(C_{1b}\)#✓fully proved

For a natural number \(N\) let \(M(N)\) be the Erdős minimum overlap function: the least, over all pairs of disjoint finite sets \(A, B \subseteq \mathbb{Z}\) with \(A \cup B = \{1, \dots, 2N\}\) and \(|A| = |B|\), of the largest number of pairs \((a, b) \in A \times B\) with a given difference \(a - b\). This is the proposition that \(M(N)/N\) tends to the continuous Erdős minimum-overlap constant \(C_{1b}\) as \(N \to \infty\).

def continuousDiscreteEquivalence : Prop :=
  Filter.Tendsto MinOverlapQuotient Filter.atTop (nhds C₁ᵦ)

Sources

• Haugland 2016; Optimization Problems, Constant 1b.

Uses 2 · Used by 1

Statement usesNotation \(C_{1b}\) · Normalized minimum overlap

Used byThe normalized minimum overlap tends to \(C_{1b}\)

DefinitionThe proposition that \(C_{1b}\) is the largest asymptotic overlap constant#✓fully proved

Call a real number \(c\) a universal asymptotic lower bound when for every \(\varepsilon > 0\) there is a positive integer \(N_0\) such that for every \(N \ge N_0\) and all disjoint finite sets \(A, B \subseteq \mathbb{Z}\) with \(A \cup B = \{1, \dots, 2N\}\) and \(|A| = |B|\), some integer \(x\) satisfies \((c - \varepsilon) N \le \#\{(a, b) \in A \times B : a - b = x\}\). This is the proposition that the continuous Erdős minimum-overlap constant \(C_{1b}\) is a universal asymptotic lower bound and that every universal asymptotic lower bound \(c\) satisfies \(c \le C_{1b}\).

def continuousDiscreteAsymptoticCharacterization : Prop :=
  IsGreatest {c : ℝ | DiscreteUniversalLowerBound c} C₁ᵦ

Sources

• Haugland 2016; Optimization Problems, Constant 1b.

Uses 2 · Used by 1

Statement usesNotation \(C_{1b}\) · Universal asymptotic lower bound for discrete overlaps

Used byThe continuous constant \(C_{1b}\) is the largest asymptotic overlap constant

DefinitionErdős's upper bound \(1/2\) for the minimum-overlap constant (statement)#✓fully proved

The statement that the continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(C_{1b} \le 1/2\).

def upperBound_E1955_half : Prop := C₁ᵦ ≤ (1 : ℝ) / 2

Sources

• Erdős 1955; Optimization Problems, Constant 1b.

Uses 1

Statement usesNotation \(C_{1b}\)

DefinitionErdős's unpublished upper bound \(4/9\) for the minimum-overlap constant (statement)#✓fully proved

The statement that the continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(C_{1b} \le 4/9\).

def upperBound_Erdos_unpublished_fourNinths : Prop := C₁ᵦ ≤ (4 : ℝ) / 9

Sources

• Erdős, unpublished; Optimization Problems, Constant 1b.

Uses 1 · Used by 1

Statement usesNotation \(C_{1b}\)

Used byErdős's unpublished upper bound \(4/9\) for the minimum-overlap constant

DefinitionStatement of the Motzkin–Ralston–Selfridge upper bound \(5/12\) for the minimum-overlap constant#✓fully proved

Statement of the Motzkin–Ralston–Selfridge upper bound \(5/12\) for the minimum-overlap constant. The proposition that the continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(C_{1b} \le 5/12\).

def upperBound_MRS1956_fiveTwelfths : Prop := C₁ᵦ ≤ (5 : ℝ) / 12

Sources

• Motzkin--Ralston--Selfridge 1956; Optimization Problems, Constant 1b.

Uses 1 · Used by 1

Statement usesNotation \(C_{1b}\)

Used byMotzkin–Ralston–Selfridge upper bound \(5/12\) for the minimum-overlap constant

DefinitionStatement of the Motzkin–Ralston–Selfridge upper bound \(0.4\) for the minimum-overlap constant#✓fully proved

Statement of the Motzkin–Ralston–Selfridge upper bound \(0.4\) for the minimum-overlap constant. The proposition that the continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(C_{1b} \le 0.4\).

def upperBound_MRS1956_pointFour : Prop := C₁ᵦ ≤ (4 : ℝ) / 10

Sources

• Motzkin--Ralston--Selfridge 1956; Optimization Problems, Constant 1b.

Uses 1 · Used by 1

Statement usesNotation \(C_{1b}\)

Used byMotzkin–Ralston–Selfridge upper bound \(0.4\) for the minimum-overlap constant

DefinitionStatement of Haugland's unpublished 1993 upper bound for the minimum-overlap constant#✓fully proved

The proposition that the continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(C_{1b} \le 0.385694\).

def upperBound_Haugland_unpublished_1993 : Prop := C₁ᵦ ≤ (385694 : ℝ) / 1000000

Sources

• Haugland, unpublished 1993; Optimization Problems, Constant 1b.

Uses 1 · Used by 1

Statement usesNotation \(C_{1b}\)

Used byHaugland's unpublished 1993 upper bound for the minimum-overlap constant

DefinitionStatement of Haugland's 1996 upper bound for the minimum-overlap constant#✓fully proved

The proposition that the continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(C_{1b} \le 0.382002\).

def upperBound_H1996 : Prop := C₁ᵦ ≤ (382002 : ℝ) / 1000000

Sources

• Haugland 1996; Optimization Problems, Constant 1b.

Uses 1 · Used by 1

Statement usesNotation \(C_{1b}\)

Used byHaugland's 1996 upper bound for the minimum-overlap constant

DefinitionStatement of Haugland's 2016 upper bound for the minimum-overlap constant#✓fully proved

The proposition that the continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(C_{1b} \le 0.380926\).

def upperBound_H2016 : Prop := C₁ᵦ ≤ (380926 : ℝ) / 1000000

Sources

• Haugland 2016; Optimization Problems, Constant 1b.

Uses 1 · Used by 1

Statement usesNotation \(C_{1b}\)

Used byHaugland's 2016 upper bound for the minimum-overlap constant

DefinitionAlphaEvolve upper bound for the minimum-overlap constant (statement)#✓fully proved

The statement that the continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(C_{1b} \le 0.380924\).

def upperBound_GGSWT2025_AlphaEvolve : Prop := C₁ᵦ ≤ (380924 : ℝ) / 1000000

Sources

• Georgiev--Gómez-Serrano--Tao--Wagner 2025; Optimization Problems, Constant 1b.

Uses 1 · Used by 1

Statement usesNotation \(C_{1b}\)

Used byAlphaEvolve upper bound for the minimum-overlap constant

DefinitionTTT-Discover 2026 upper bound statement for the minimum overlap constant#✓fully proved

This is the proposition that the continuous Erdős minimum-overlap constant \(C_{1b}\) is at most \(0.380876\).

def upperBound_YKLBMWKCZGS2026_TTTDiscover : Prop := C₁ᵦ ≤ (380876 : ℝ) / 1000000

Sources

• Yuksekgonul et al. 2026 (TTT-Discover); Optimization Problems, Constant 1b.

Uses 1 · Used by 1

Statement usesNotation \(C_{1b}\)

Used byTTT-Discover 2026 upper bound for the minimum overlap constant holds

DefinitionTogether AI 2026 upper bound statement for the minimum overlap constant#✓fully proved

This is the proposition that the continuous Erdős minimum-overlap constant \(C_{1b}\) is at most \(0.380871\).

def upperBound_T2026_TogetherAI : Prop := C₁ᵦ ≤ (380871 : ℝ) / 1000000

Sources

• Together AI 2026; Optimization Problems, Constant 1b.

Uses 1 · Used by 1

Statement usesNotation \(C_{1b}\)

Used byTogether AI's 2026 upper bound for the minimum-overlap constant

DefinitionSimpleTES 2026 upper bound statement for the minimum overlap constant#✓fully proved

This is the proposition that the continuous Erdős minimum-overlap constant \(C_{1b}\) is at most \(0.380868\).

def upperBound_YLTLYSTYLLGDHZSWZSHMELCZX2026_SimpleTES : Prop :=
  C₁ᵦ ≤ (380868 : ℝ) / 1000000

Sources

• Ye et al. 2026 (SimpleTES); Optimization Problems, Constant 1b.

Uses 1 · Used by 1

Statement usesNotation \(C_{1b}\)

Used bySimpleTES 2026 upper bound for the minimum overlap constant holds

DefinitionThe proposition \(1/4 \le C_{1b}\)#✓fully proved

This is the proposition that the continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(1/4 \le C_{1b}\).

def lowerBound_E1955_quarter : Prop := (1 : ℝ) / 4 ≤ C₁ᵦ

Sources

• Erdős 1955; Optimization Problems, Constant 1b.

Uses 1 · Used by 1

Statement usesNotation \(C_{1b}\)

Used byErdős's lower bound \(C_{1b} \ge 1/4\)

DefinitionScherk's lower bound for the minimum-overlap constant (statement)#✓fully proved

The statement that the continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(1 - 1/\sqrt{2} \le C_{1b}\).

def lowerBound_Scherk_unpublished_1955 : Prop := 1 - 1 / Real.sqrt 2 ≤ C₁ᵦ

Sources

• Scherk, unpublished 1955; Optimization Problems, Constant 1b.

Uses 1 · Used by 1

Statement usesNotation \(C_{1b}\)

Used byScherk's lower bound for the minimum-overlap constant

DefinitionThe proposition \((4 - \sqrt{6})/5 \le C_{1b}\)#✓fully proved

This is the proposition that the continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \((4 - \sqrt{6})/5 \le C_{1b}\).

def lowerBound_S1958 : Prop := (4 - Real.sqrt 6) / 5 ≤ C₁ᵦ

Sources

• Swierczkowski 1958; Optimization Problems, Constant 1b.

Uses 1 · Used by 1

Statement usesNotation \(C_{1b}\)

Used byŚwierczkowski's lower bound \(C_{1b} \ge (4 - \sqrt{6})/5\)

DefinitionThe proposition \(\sqrt{4 - \sqrt{15}} \le C_{1b}\)#✓fully proved

This is the proposition that the continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(\sqrt{4 - \sqrt{15}} \le C_{1b}\).

def lowerBound_M1959 : Prop := Real.sqrt (4 - Real.sqrt 15) ≤ C₁ᵦ

Sources

• Moser 1959; Optimization Problems, Constant 1b.

Uses 1 · Used by 1

Statement usesNotation \(C_{1b}\)

Used byMoser's lower bound \(C_{1b} \ge \sqrt{4 - \sqrt{15}}\)

DefinitionWhite's lower bound for the minimum-overlap constant (statement)#✓fully proved

The statement that the continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(0.379005 \le C_{1b}\), where \(0.379005\) is the exact rational number \(379005/1000000\).

def lowerBound_W2022 : Prop := (379005 : ℝ) / 1000000 ≤ C₁ᵦ

Sources

• White 2022; Optimization Problems, Constant 1b.

Uses 1 · Used by 1

Statement usesNotation \(C_{1b}\)

Used byWhite's lower bound for the minimum-overlap constant

TheoremThe normalized minimum overlap tends to \(C_{1b}\)#●ready to prove

For a natural number \(N\) let \(M(N)\) be the Erdős minimum overlap function: the least, over all pairs of disjoint finite sets \(A, B \subseteq \mathbb{Z}\) with \(A \cup B = \{1, \dots, 2N\}\) and \(|A| = |B|\), of the largest number of pairs \((a, b) \in A \times B\) with a given difference \(a - b\). Then \(M(N)/N\) tends to the continuous Erdős minimum-overlap constant \(C_{1b}\) as \(N \to \infty\).

public theorem_wanted continuousDiscreteEquivalence_holds : continuousDiscreteEquivalence

Sources

• Haugland 2016 and Optimization Problems 1b.

Uses 1

Statement usesThe proposition that \(M(N)/N\) tends to \(C_{1b}\)

TheoremThe continuous constant \(C_{1b}\) is the largest asymptotic overlap constant#●ready to prove

Call a real number \(c\) a universal asymptotic lower bound when for every \(\varepsilon > 0\) there is a positive integer \(N_0\) such that for every \(N \ge N_0\) and all disjoint finite sets \(A, B \subseteq \mathbb{Z}\) with \(A \cup B = \{1, \dots, 2N\}\) and \(|A| = |B|\), some integer \(x\) satisfies \((c - \varepsilon) N \le \#\{(a, b) \in A \times B : a - b = x\}\). Then the continuous Erdős minimum-overlap constant \(C_{1b}\) is a universal asymptotic lower bound, and every universal asymptotic lower bound \(c\) satisfies \(c \le C_{1b}\).

public theorem_wanted continuousDiscreteAsymptoticCharacterization_holds :
  continuousDiscreteAsymptoticCharacterization

Sources

• Haugland 2016 and the uniform partition clause of Optimization Problems 1b.

Uses 1

Statement usesThe proposition that \(C_{1b}\) is the largest asymptotic overlap constant

TheoremErdős's unpublished upper bound \(4/9\) for the minimum-overlap constant#●ready to prove

The continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(C_{1b} \le 4/9\).

public theorem_wanted upperBound_Erdos_unpublished_fourNinths_holds :
  upperBound_Erdos_unpublished_fourNinths

Sources

• Erdős, unpublished, recorded by Optimization Problems 1b.

Uses 1

Statement usesErdős's unpublished upper bound \(4/9\) for the minimum-overlap constant (statement)

TheoremMotzkin–Ralston–Selfridge upper bound \(5/12\) for the minimum-overlap constant#●ready to prove

The continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(C_{1b} \le 5/12\).

public theorem_wanted upperBound_MRS1956_fiveTwelfths_holds : upperBound_MRS1956_fiveTwelfths

Sources

• Motzkin--Ralston--Selfridge 1956 and Optimization Problems 1b.

Uses 1

Statement usesStatement of the Motzkin–Ralston–Selfridge upper bound \(5/12\) for the minimum-overlap constant

TheoremMotzkin–Ralston–Selfridge upper bound \(0.4\) for the minimum-overlap constant#●ready to prove

The continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(C_{1b} \le 0.4\).

public theorem_wanted upperBound_MRS1956_pointFour_holds : upperBound_MRS1956_pointFour

Sources

• Motzkin--Ralston--Selfridge 1956 and Optimization Problems 1b.

Uses 1

Statement usesStatement of the Motzkin–Ralston–Selfridge upper bound \(0.4\) for the minimum-overlap constant

TheoremHaugland's unpublished 1993 upper bound for the minimum-overlap constant#●ready to prove

The continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(C_{1b} \le 0.385694\).

public theorem_wanted upperBound_Haugland_unpublished_1993_holds :
  upperBound_Haugland_unpublished_1993

Sources

• Haugland, unpublished 1993, recorded by Optimization Problems 1b.

Uses 1

Statement usesStatement of Haugland's unpublished 1993 upper bound for the minimum-overlap constant

TheoremHaugland's 1996 upper bound for the minimum-overlap constant#●ready to prove

The continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(C_{1b} \le 0.382002\).

public theorem_wanted upperBound_H1996_holds : upperBound_H1996

Sources

• Haugland 1996 and Optimization Problems 1b.

Uses 1

Statement usesStatement of Haugland's 1996 upper bound for the minimum-overlap constant

TheoremHaugland's 2016 upper bound for the minimum-overlap constant#●ready to prove

The continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(C_{1b} \le 0.380926\).

public theorem_wanted upperBound_H2016_holds : upperBound_H2016

Sources

• Haugland 2016 and Optimization Problems 1b.

Uses 1

Statement usesStatement of Haugland's 2016 upper bound for the minimum-overlap constant

TheoremAlphaEvolve upper bound for the minimum-overlap constant#●ready to prove

The continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(C_{1b} \le 0.380924\).

public theorem_wanted upperBound_GGSWT2025_AlphaEvolve_holds :
  upperBound_GGSWT2025_AlphaEvolve

Sources

• Georgiev--Gómez-Serrano--Tao--Wagner 2025 and Optimization Problems 1b.

Uses 1

Statement usesAlphaEvolve upper bound for the minimum-overlap constant (statement)

TheoremTTT-Discover 2026 upper bound for the minimum overlap constant holds#●ready to prove

The continuous Erdős minimum-overlap constant \(C_{1b}\) is at most \(0.380876\).

public theorem_wanted upperBound_YKLBMWKCZGS2026_TTTDiscover_holds :
  upperBound_YKLBMWKCZGS2026_TTTDiscover

Sources

• Yuksekgonul et al. 2026 and Optimization Problems 1b.

Uses 1

Statement usesTTT-Discover 2026 upper bound statement for the minimum overlap constant

TheoremTogether AI's 2026 upper bound for the minimum-overlap constant#●ready to prove

The continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(C_{1b} \le 0.380871\).

public theorem_wanted upperBound_T2026_TogetherAI_holds : upperBound_T2026_TogetherAI

Sources

• Together AI 2026 and Optimization Problems 1b.

Uses 1

Statement usesTogether AI 2026 upper bound statement for the minimum overlap constant

TheoremSimpleTES 2026 upper bound for the minimum overlap constant holds#●ready to prove

The continuous Erdős minimum-overlap constant \(C_{1b}\) is at most \(0.380868\).

public theorem_wanted upperBound_YLTLYSTYLLGDHZSWZSHMELCZX2026_SimpleTES_holds :
  upperBound_YLTLYSTYLLGDHZSWZSHMELCZX2026_SimpleTES

Sources

• Ye et al. 2026 and Optimization Problems 1b.

Uses 1

Statement usesSimpleTES 2026 upper bound statement for the minimum overlap constant

TheoremErdős's lower bound \(C_{1b} \ge 1/4\)#●ready to prove

The continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(1/4 \le C_{1b}\).

public theorem_wanted lowerBound_E1955_quarter_holds : lowerBound_E1955_quarter

Sources

• Erdős 1955 and Optimization Problems 1b.

Uses 1

Statement usesThe proposition \(1/4 \le C_{1b}\)

TheoremScherk's lower bound for the minimum-overlap constant#●ready to prove

The continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(1 - 1/\sqrt{2} \le C_{1b}\).

public theorem_wanted lowerBound_Scherk_unpublished_1955_holds :
  lowerBound_Scherk_unpublished_1955

Sources

• Scherk, unpublished 1955, recorded by Optimization Problems 1b.

Uses 1

Statement usesScherk's lower bound for the minimum-overlap constant (statement)

TheoremŚwierczkowski's lower bound \(C_{1b} \ge (4 - \sqrt{6})/5\)#●ready to prove

The continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \((4 - \sqrt{6})/5 \le C_{1b}\).

public theorem_wanted lowerBound_S1958_holds : lowerBound_S1958

Sources

• Swierczkowski 1958 and Optimization Problems 1b.

Uses 1

Statement usesThe proposition \((4 - \sqrt{6})/5 \le C_{1b}\)

TheoremMoser's lower bound \(C_{1b} \ge \sqrt{4 - \sqrt{15}}\)#●ready to prove

The continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(\sqrt{4 - \sqrt{15}} \le C_{1b}\).

public theorem_wanted lowerBound_M1959_holds : lowerBound_M1959

Sources

• Moser 1959 and Optimization Problems 1b.

Uses 1

Statement usesThe proposition \(\sqrt{4 - \sqrt{15}} \le C_{1b}\)

TheoremWhite's lower bound for the minimum-overlap constant#●ready to prove

The continuous Erdős minimum-overlap constant \(C_{1b}\) satisfies \(0.379005 \le C_{1b}\).

public theorem_wanted lowerBound_W2022_holds : lowerBound_W2022

Sources

• White 2022 and Optimization Problems 1b.

Uses 1

Statement usesWhite's lower bound for the minimum-overlap constant (statement)

39 fully proved17 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.