1. FormalConjectures
  2. ErdosProblems
  3. «36»
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Erdős Problem 36

References:

open scoped Topologyopen Filternamespace Erdos36

The number of solutions to the equation $a - b = k$, for $a \in A$ and $b \in B$. This represents the "overlap" between sets $A$ and $B$ for a given difference $k$.

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

The maximum overlap for a given pair of sets $A$ and $B$, taken over all possible integer differences $k$.

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

Let $A$ and $B$ be two complementary subsets, a splitting of the numbers ${1, 2, \dots, 2n}$, such that both have the same cardinality $n$. Define $M(n)$ to be the minimum MaxOverlap that can be achieved, ranging over all such partitions $(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)}

A small API lemma: every pair (a, b) ∈ A × B contributes to Overlap A B (a - b).

@[category API, AMS 5 11] private lemma one_le_overlap {A B : Finset ℤ} {a b : ℤ} (ha : a ∈ A) (hb : b ∈ B) : 1 ≤ Overlap A B (a - b) := Finset.card_pos.mpr ⟨(a, b), Finset.mem_filter.mpr ⟨Finset.mem_product.mpr ⟨ha, hb⟩, rfl⟩⟩

For a fixed difference k, the first coordinate determines the second, so an overlap is never larger than either side. This is what makes MaxOverlap a supremum of a bounded set.

@[category API, AMS 5 11] private lemma overlap_le_card_left (A B : Finset ℤ) (k : ℤ) : Overlap A B k ≤ A.card := A:Finset ℤB:Finset ℤk:ℤ⊢ Overlap A B k ≤ A.card A:Finset ℤB:Finset ℤk:ℤp:ℤ × ℤhp:p ∈ ↑({x ∈ A.product B | match x with | (a, b) => a - b = k})⊢ p.1 ∈ ↑AA:Finset ℤB:Finset ℤk:ℤp:ℤ × ℤhp:p ∈ ↑({x ∈ A.product B | match x with | (a, b) => a - b = k})q:ℤ × ℤhq:q ∈ ↑({x ∈ A.product B | match x with | (a, b) => a - b = k})h:p.1 = q.1⊢ p = q A:Finset ℤB:Finset ℤk:ℤp:ℤ × ℤhp:p ∈ ↑({x ∈ A.product B | match x with | (a, b) => a - b = k})⊢ p.1 ∈ ↑A All goals completed! 🐙 A:Finset ℤB:Finset ℤk:ℤp:ℤ × ℤhp:p ∈ ↑({x ∈ A.product B | match x with | (a, b) => a - b = k})q:ℤ × ℤhq:q ∈ ↑({x ∈ A.product B | match x with | (a, b) => a - b = k})h:p.1 = q.1⊢ p = q A:Finset ℤB:Finset ℤk:ℤp:ℤ × ℤhp:p ∈ ↑({x ∈ A.product B | match x with | (a, b) => a - b = k})q:ℤ × ℤhq:q ∈ ↑({x ∈ A.product B | match x with | (a, b) => a - b = k})h:p.1 = q.1hpk:match p with | (a, b) => a - b = k⊢ p = q A:Finset ℤB:Finset ℤk:ℤp:ℤ × ℤhp:p ∈ ↑({x ∈ A.product B | match x with | (a, b) => a - b = k})q:ℤ × ℤhq:q ∈ ↑({x ∈ A.product B | match x with | (a, b) => a - b = k})h:p.1 = q.1hpk:match p with | (a, b) => a - b = khqk:match q with | (a, b) => a - b = k⊢ p = q exact Prod.ext h (A:Finset ℤB:Finset ℤk:ℤp:ℤ × ℤhp:p ∈ ↑({x ∈ A.product B | match x with | (a, b) => a - b = k})q:ℤ × ℤhq:q ∈ ↑({x ∈ A.product B | match x with | (a, b) => a - b = k})h:p.1 = q.1hpk:match p with | (a, b) => a - b = khqk:match q with | (a, b) => a - b = k⊢ p.2 = q.2 All goals completed! 🐙)

The range of Overlap A B is bounded, so MaxOverlap is a genuine supremum rather than the junk value sSup returns on an unbounded set.

@[category API, AMS 5 11] private lemma bddAbove_range_overlap (A B : Finset ℤ) : BddAbove (Set.range (Overlap A B)) := A:Finset ℤB:Finset ℤ⊢ BddAbove (Set.range (Overlap A B)) A:Finset ℤB:Finset ℤ⊢ A.card ∈ upperBounds (Set.range (Overlap A B)) A:Finset ℤB:Finset ℤk:ℤ⊢ Overlap A B k ≤ A.card All goals completed! 🐙@[category API, AMS 5 11] private lemma maxOverlap_le_card_left (A B : Finset ℤ) : MaxOverlap A B ≤ A.card := ciSup_le fun k => overlap_le_card_left A B k

An overlap can only be nonzero for a difference that is actually realised, which confines the search for MaxOverlap to a finite set.

A:Finset ℤB:Finset ℤk:ℤhk:k ∉ Finset.image (fun p ↦ p.1 - p.2) (A ×ˢ B)⊢ ∀ ⦃x : ℤ × ℤ⦄, x ∈ A.product B → ¬match x with | (a, b) => a - b = k A:Finset ℤB:Finset ℤa:ℤb:ℤhab:(a, b) ∈ A.product Bhk:a - b ∉ Finset.image (fun p ↦ p.1 - p.2) (A ×ˢ B)⊢ False All goals completed! 🐙

MaxOverlap as a supremum over a finite set of differences. This is the form that makes it possible to evaluate: the iSup in the definition ranges over all of ℤ, but every difference outside A - B contributes 0.

@[category API, AMS 5 11] private lemma maxOverlap_eq_sup (A B : Finset ℤ) : MaxOverlap A B = ((A ×ˢ B).image fun p => p.1 - p.2).sup (Overlap A B) := A:Finset ℤB:Finset ℤ⊢ MaxOverlap A B = (Finset.image (fun p ↦ p.1 - p.2) (A ×ˢ B)).sup (Overlap A B) A:Finset ℤB:Finset ℤk:ℤ⊢ Overlap A B k ≤ (Finset.image (fun p ↦ p.1 - p.2) (A ×ˢ B)).sup (Overlap A B)A:Finset ℤB:Finset ℤk:ℤx✝:k ∈ Finset.image (fun p ↦ p.1 - p.2) (A ×ˢ B)⊢ Overlap A B k ≤ MaxOverlap A B A:Finset ℤB:Finset ℤk:ℤ⊢ Overlap A B k ≤ (Finset.image (fun p ↦ p.1 - p.2) (A ×ˢ B)).sup (Overlap A B) A:Finset ℤB:Finset ℤk:ℤhk:k ∈ Finset.image (fun p ↦ p.1 - p.2) (A ×ˢ B)⊢ Overlap A B k ≤ (Finset.image (fun p ↦ p.1 - p.2) (A ×ˢ B)).sup (Overlap A B)A:Finset ℤB:Finset ℤk:ℤhk:k ∉ Finset.image (fun p ↦ p.1 - p.2) (A ×ˢ B)⊢ Overlap A B k ≤ (Finset.image (fun p ↦ p.1 - p.2) (A ×ˢ B)).sup (Overlap A B) A:Finset ℤB:Finset ℤk:ℤhk:k ∈ Finset.image (fun p ↦ p.1 - p.2) (A ×ˢ B)⊢ Overlap A B k ≤ (Finset.image (fun p ↦ p.1 - p.2) (A ×ˢ B)).sup (Overlap A B) All goals completed! 🐙 A:Finset ℤB:Finset ℤk:ℤhk:k ∉ Finset.image (fun p ↦ p.1 - p.2) (A ×ˢ B)⊢ Overlap A B k ≤ (Finset.image (fun p ↦ p.1 - p.2) (A ×ˢ B)).sup (Overlap A B) All goals completed! 🐙 A:Finset ℤB:Finset ℤk:ℤx✝:k ∈ Finset.image (fun p ↦ p.1 - p.2) (A ×ˢ B)⊢ Overlap A B k ≤ MaxOverlap A B All goals completed! 🐙

The pairs M n ranges over are exactly the n-element subsets of {1, …, 2n}, each paired with its complement. This turns the sInf over an unbounded family of Finset ℤ into an infimum over a Finset.

n:ℕA:Finset ℤhA:A ⊆ Finset.Icc 1 (2 * ↑n)hn:A.card = n⊢ n = (2 * ↑n + 1 - 1).toNat - n All goals completed! 🐙

A computable stand-in for MaxOverlap. Overlap is already computable; the only obstacle is the iSup, and maxOverlap_eq_sup says it agrees with this Finset.sup.

private def maxOverlapC (A B : Finset ℤ) : ℕ := ((A ×ˢ B).image fun p => p.1 - p.2).sup (Overlap A B)@[category API, AMS 5 11] private lemma maxOverlap_eq_maxOverlapC (A B : Finset ℤ) : MaxOverlap A B = maxOverlapC A B := maxOverlap_eq_sup A B

The n-element subsets of {1, …, 2n}.

private def parts (n : ℕ) : Finset (Finset ℤ) := (Finset.Icc (1 : ℤ) (2 * n)).powerset.filter fun A => A.card = n@[category API, AMS 5 11] private lemma mem_parts {n : ℕ} {A : Finset ℤ} : A ∈ parts n ↔ A ⊆ Finset.Icc (1 : ℤ) (2 * n) ∧ A.card = n := n:ℕA:Finset ℤ⊢ A ∈ parts n ↔ A ⊆ Finset.Icc 1 (2 * ↑n) ∧ A.card = n All goals completed! 🐙n:ℕ⊢ (↑n + 1 - 1).toNat = n; All goals completed! 🐙

M n as the minimum of a Finset of naturals, which is what makes it evaluable.

n:ℕ⊢ (fun A ↦ MaxOverlap A (Finset.Icc 1 (2 * ↑n) \ A)) '' {A | A ⊆ Finset.Icc 1 (2 * ↑n) ∧ A.card = n} = (fun A ↦ maxOverlapC A (Finset.Icc 1 (2 * ↑n) \ A)) '' {A | A ⊆ Finset.Icc 1 (2 * ↑n) ∧ A.card = n} All goals completed! 🐙

MaxOverlap {1} {2} = 1: the only nonzero overlap is at k = -1.

⊢ MaxOverlap {1} {2} ≤ {(1, 2)}.card ⊢ ∀ (x : ℤ), Overlap {1} {2} x ≤ {(1, 2)}.card k:ℤ⊢ Overlap {1} {2} k ≤ {(1, 2)}.card k:ℤ⊢ {x ∈ {1}.product {2} | match x with | (a, b) => a - b = k} ⊆ {(1, 2)} k:ℤp:ℤ × ℤhp:p ∈ {x ∈ {1}.product {2} | match x with | (a, b) => a - b = k}⊢ p ∈ {(1, 2)} k:ℤp:ℤ × ℤhp:p ∈ {x ∈ {1}.product {2} | match x with | (a, b) => a - b = k}hp1:p ∈ {1}.product {2}right✝:match p with | (a, b) => a - b = k⊢ p ∈ {(1, 2)} k:ℤp:ℤ × ℤhp:p ∈ {x ∈ {1}.product {2} | match x with | (a, b) => a - b = k}hp1:p ∈ {1}.product {2}right✝:match p with | (a, b) => a - b = kha:p.1 ∈ {1}hb:p.2 ∈ {2}⊢ p ∈ {(1, 2)} k:ℤp:ℤ × ℤhp:p ∈ {x ∈ {1}.product {2} | match x with | (a, b) => a - b = k}hp1:p ∈ {1}.product {2}right✝:match p with | (a, b) => a - b = kha:p.1 = 1hb:p.2 = 2⊢ p ∈ {(1, 2)} All goals completed! 🐙 ⊢ 1 ≤ MaxOverlap {1} {2} ⊢ BddAbove (Set.range (Overlap {1} {2}))⊢ 1 ≤ Overlap {1} {2} (-1) ⊢ BddAbove (Set.range (Overlap {1} {2})) ⊢ 1 ∈ upperBounds (Set.range (Overlap {1} {2})) k:ℤ⊢ Overlap {1} {2} k ≤ 1 exact (Finset.card_filter_le _ _).trans (k:ℤ⊢ ({1}.product {2}).card ≤ 1 All goals completed! 🐙) ⊢ 1 ≤ Overlap {1} {2} (-1) All goals completed! 🐙

This example calculates the value of $M 1$. The set is ${1, 2}$, so the only partition is $A = {1}, B = {2}$ (or vice versa). The possible differences are $1 - 2 = -1$ and $2 - 1 = 1$. The Overlap for $k=-1$ is 1 (if $A={1}, B={2}$) and for $k=1$ also 1 (if $A={2}, B={1}$ ). The MaxOverlap is $1$, since the Overlap is $0$ for other $k$. Thus, $M 1 = 1$.

All goals completed! 🐙 a:ℤhca:{a}.card = 1b:ℤhcb:{b}.card = 1hd:Disjoint {a} {b}hu:{a} ∪ {b} = Finset.Icc 1 (2 * ↑1)hsc:{a}.card = {b}.cardhcardsum:{a}.card + {b}.card = 2⊢ 1 ≤ Overlap {a} {b} (a - b) All goals completed! 🐙

For $n = 2$, the set is ${1, 2, 3, 4}$. The balanced partition $A = {1, 4}, B = {2, 3}$ has all four pairwise differences ($\pm 1, \pm 2$) distinct, so MaxOverlap = 1. Any balanced partition has both pieces nonempty, so MaxOverlap \geq 1.

⊢ (Finset.image (fun A ↦ maxOverlapC A (Finset.Icc 1 (2 * ↑2) \ A)) (parts 2)).min' ⋯ = 1 All goals completed! 🐙

For n = 3 the best splitting of {1, …, 6} has maximum overlap 2.

⊢ (Finset.image (fun A ↦ maxOverlapC A (Finset.Icc 1 (2 * ↑3) \ A)) (parts 3)).min' ⋯ = 2 All goals completed! 🐙set_option maxRecDepth 8000 in

For n = 4 the best splitting of {1, …, 8} still has maximum overlap 2.

⊢ (Finset.image (fun A ↦ maxOverlapC A (Finset.Icc 1 (2 * ↑4) \ A)) (parts 4)).min' ⋯ = 2 All goals completed! 🐙set_option maxRecDepth 40000 in

For n = 5 the best splitting of {1, …, 10} has maximum overlap 3.

⊢ (Finset.image (fun A ↦ maxOverlapC A (Finset.Icc 1 (2 * ↑5) \ A)) (parts 5)).min' ⋯ = 3 All goals completed! 🐙

The quotient of the minimum maximum overlap $M(N)$ by $N$. The central question of the minimum overlap problem is to determine the asymptotic behavior of this quotient as $N \to \infty$.

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

A lower bound of $\frac 1 4$. See Some remarks on number theory (in Hebrew) by Paul Erdős, Riveon Lematematika 9, p.45-48,1955

@[category textbook, AMS 5 11] theorem minimum_overlap.variants.lower.erdos_1955 : (1 : ℝ) / 4 < atTop.liminf MinOverlapQuotient := ⊢ 1 / 4 < liminf MinOverlapQuotient atTop All goals completed! 🐙

A lower bound of $1 - frac{1}{\sqrt 2}$. Scherk (written communication), see On the minimal overlap problem of Erdös by Leo Moser, Аста Аrithmetica V, p. 117-119, 1959

@[category research solved, AMS 5 11] theorem minimum_overlap.variants.lower.scherk_1955 : 1 - (√2)⁻¹ < atTop.liminf MinOverlapQuotient := ⊢ 1 - (√2)⁻¹ < liminf MinOverlapQuotient atTop All goals completed! 🐙

A lower bound of $\frac{4 - \sqrt{6}}{5}$. See On the intersection of a linear set with the translation of its complement by Stanisław Świerczkowski1, Colloquium Mathematicum 5(2), p. 185-197, 1958

@[category research solved, AMS 5 11] theorem minimum_overlap.variants.lower.swierczkowski_1958 : (4 - 6 ^ ((1 : ℝ) / 2)) / 5 < atTop.liminf MinOverlapQuotient := ⊢ (4 - 6 ^ (1 / 2)) / 5 < liminf MinOverlapQuotient atTop All goals completed! 🐙

A lower bound of $\sqrt{4 - \sqrt{15}}$.

@[category research solved, AMS 5 11] theorem minimum_overlap.variants.lower.haugland_1996 : (4 - 15 ^((1 : ℝ) / 2)) ^ ((1 : ℝ) / 2) < atTop.liminf MinOverlapQuotient := ⊢ (4 - 15 ^ (1 / 2)) ^ (1 / 2) < liminf MinOverlapQuotient atTop All goals completed! 🐙

A lower bound of $0.379005$. See Erdős' minimum overlap problem by Ethan Patrick White, 2022

@[category research solved, AMS 5 11] theorem minimum_overlap.variants.lower.white_2022 : 0.379005 < atTop.liminf MinOverlapQuotient := ⊢ 0.379005 < liminf MinOverlapQuotient atTop All goals completed! 🐙

The example (with $N$ even), $A = {\frac N 2 + 1, \dots, \frac{3N}{2}}$ shows an upper bound of $\frac 1 2$.

@[category research solved, AMS 5 11] theorem minimum_overlap.variants.upper.erdos_1955 : atTop.limsup MinOverlapQuotient ≤ (1 : ℝ) / 2 := ⊢ limsup MinOverlapQuotient atTop ≤ 1 / 2 All goals completed! 🐙

An upper bound of $\frac 2 5$. See Minimal overlapping under translation. by T. S. Motzkin, K. E. Ralston and J. L. Selfridge, in "The summer meeting in Seattle" by V. L. Klee Jr., Bull. Amer. Math. Soc.62, p. 558, 1956

@[category research solved, AMS 5 11] theorem minimum_overlap.variants.upper.MRS_1956 : atTop.limsup MinOverlapQuotient ≤ (2 : ℝ) / 5 := ⊢ limsup MinOverlapQuotient atTop ≤ 2 / 5 All goals completed! 🐙

An upper bound of $0.38200298812318988$. See Advances in the Minimum Overlap Problem by Jan Kristian Haugland, Journal of Number Theory Volume 58, Issue 1, p 71-78, 1996

@[category research solved, AMS 5 11] theorem minimum_overlap.variants.upper.haugland_1996 : atTop.limsup MinOverlapQuotient ≤ 0.38200298812318988 := ⊢ limsup MinOverlapQuotient atTop ≤ 0.38200298812318988 All goals completed! 🐙

An upper bound of $0.3809268534330870$. See The minimum overlap problem by Jan Kristian Haugland

@[category research solved, AMS 5 11] theorem minimum_overlap.variants.upper.haugland_2022 : atTop.limsup MinOverlapQuotient ≤ 0.3809268534330870 := ⊢ limsup MinOverlapQuotient atTop ≤ 0.3809268534330870 All goals completed! 🐙

Find a better lower bound!

@[category research open, AMS 5 11] theorem erdos_36.variants.lower: ∃ (c : ℝ), 0.379005 < c ∧ c ≤ atTop.liminf MinOverlapQuotient ∧ c = answer(sorry) := ⊢ ∃ c, 0.379005 < c ∧ c ≤ liminf MinOverlapQuotient atTop ∧ c = sorry All goals completed! 🐙

Find a better upper bound!

@[category research open, AMS 5 11] theorem erdos_36.variants.upper : ∃ (c : ℝ), c < 0.380926853433087 ∧ atTop.limsup MinOverlapQuotient ≤ c ∧ c = answer(sorry) := ⊢ ∃ c < 0.380926853433087, limsup MinOverlapQuotient atTop ≤ c ∧ c = sorry All goals completed! 🐙

The limit of MinOverlapQuotient exists and it is less than $0.385694$.

@[category research solved, AMS 5 11] theorem erdos_36.variants.exists : ∃ c, atTop.Tendsto MinOverlapQuotient (𝓝 c) ∧ c < 0.385694 := ⊢ ∃ c, Tendsto MinOverlapQuotient atTop (𝓝 c) ∧ c < 0.385694 All goals completed! 🐙

Find the value of the limit of MinOverlapQuotient!

@[category research open, AMS 5 11] theorem erdos_36 : atTop.Tendsto MinOverlapQuotient (𝓝 answer(sorry)) := ⊢ Tendsto MinOverlapQuotient atTop (𝓝 sorry) All goals completed! 🐙end Erdos36