1. FormalConjectures
  2. GreensOpenProblems
  3. «32»
/- Copyright 2026 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

Green's Open Problem 32

Reference:

open Asymptotics Filteropen scoped Pointwise namespace Green32

A set $A$ has a gap of length $L$ if there exists $x$ such that $x, x+1, \dots, x+L-1$ are all not in $A$.

def HasGap {p : ℕ} (A : Finset (ZMod p)) (L : ℕ) : Prop := ∃ x : ZMod p, ∀ (i : ℕ), i < L → x + (i : ZMod p) ∉ A

Any set has a gap of length 0 (vacuously true).

@[category test, AMS 5 11] theorem hasGap_zero {p : ℕ} (A : Finset (ZMod p)) : HasGap A 0 := p:ℕA:Finset (ZMod p)⊢ HasGap A 0 exact ⟨0, fun _ h => absurd h (p:ℕA:Finset (ZMod p)x✝:ℕh:x✝ < 0⊢ ¬x✝ < 0 All goals completed! 🐙)⟩

The empty set has a gap of any length.

@[category test, AMS 5 11] theorem hasGap_empty {p : ℕ} (L : ℕ) : HasGap (∅ : Finset (ZMod p)) L := p:ℕL:ℕ⊢ HasGap ∅ L exact ⟨0, fun _ _ => p:ℕL:ℕx✝¹:ℕx✝:x✝¹ < L⊢ 0 + ↑x✝¹ ∉ ∅ All goals completed! 🐙⟩

The full set in $\mathbb{Z}/p\mathbb{Z}$ has no gap of positive length.

@[category test, AMS 5 11] theorem not_hasGap_univ {p : ℕ} [NeZero p] : ¬ HasGap (Finset.univ : Finset (ZMod p)) 1 := p:ℕinst✝:NeZero p⊢ ¬HasGap Finset.univ 1 p:ℕinst✝:NeZero px:ZMod phx:∀ i < 1, x + ↑i ∉ Finset.univ⊢ False have := hx 0 (p:ℕinst✝:NeZero px:ZMod phx:∀ i < 1, x + ↑i ∉ Finset.univ⊢ 0 < 1 All goals completed! 🐙) All goals completed! 🐙

Concrete: ${0}$ in $\mathbb{Z}/5\mathbb{Z}$ has a gap of length 4 starting at 1.

@[category test, AMS 5 11] theorem hasGap_concrete : HasGap ({(0 : ZMod 5)} : Finset (ZMod 5)) 4 := ⊢ HasGap {0} 4 i:ℕhi:i < 4⊢ 1 + ↑i ∉ {0} i:ℕhi:0 < 4⊢ 1 + ↑0 ∉ {0}i:ℕhi:1 < 4⊢ 1 + ↑1 ∉ {0}i:ℕhi:2 < 4⊢ 1 + ↑2 ∉ {0}i:ℕhi:3 < 4⊢ 1 + ↑3 ∉ {0} i:ℕhi:0 < 4⊢ 1 + ↑0 ∉ {0}i:ℕhi:1 < 4⊢ 1 + ↑1 ∉ {0}i:ℕhi:2 < 4⊢ 1 + ↑2 ∉ {0}i:ℕhi:3 < 4⊢ 1 + ↑3 ∉ {0} All goals completed! 🐙

The generalized problem: for a prime $p$ and a set $A \subset \mathbb{Z}/p\mathbb{Z}$ of size $\lfloor \omega(p) \rfloor$, is there a dilate of $A$ containing a gap of length $\lfloor 100p/\omega(p) \rfloor$?

def HasLargeGapDilate (ω : ℕ → ℝ) : Prop := ∀ᶠ p in atTop, p.Prime → 100 < ω p ∧ ω p < p ∧ ∀ A : Finset (ZMod p), A.card = ⌊ω p⌋₊ → ∃ c : (ZMod p)ˣ, HasGap (c • A) ⌊100 * (p : ℝ) / ω p⌋₊

Let $p$ be a prime and let $A \subset \mathbb{Z}/p\mathbb{Z}$ be a set of size $\lfloor \sqrt{p} \rfloor$. Is there a dilate of $A$ containing a gap of length $100\sqrt{p}$?

@[category research open, AMS 5 11] theorem declaration uses 'sorry'green_32 : answer(sorry) ↔ HasLargeGapDilate (fun p ↦ Real.sqrt p) := ⊢ True ↔ HasLargeGapDilate fun p => √↑p All goals completed! 🐙

[Sh20, Theorem 1] implies a gap of at least $\lfloor 2p/|A| - 2 \rfloor$.

@[category research solved, AMS 5 11] theorem declaration uses 'sorry'green_32.variants.sh20_general : ∀ (p : ℕ), p.Prime → -- Theorem 1 is for any prime p, not just asymptotically ∀ A : Finset (ZMod p), 1 < A.card → ∃ c : (ZMod p)ˣ, HasGap (c • A) ⌊2 * (p : ℝ) / A.card - 2⌋₊ := ⊢ ∀ (p : ℕ), Nat.Prime p → ∀ (A : Finset (ZMod p)), 1 < A.card → ∃ c, HasGap (c • A) ⌊2 * ↑p / ↑A.card - 2⌋₊ All goals completed! 🐙

[Sh20] has used the polynomial method to show that this is true with 100 replaced by 2 [Gr24].

Note: More precisely [Sh20, Theorem 1] implies a gap of at least $\lfloor 2p/|A| - 2 \rfloor$. For a set $A$ of size $\lfloor \sqrt{p} \rfloor$, this guarantees a gap of at least $\lfloor 2\sqrt{p} \rfloor - 2$.

@[category research solved, AMS 5 11] theorem declaration uses 'sorry'green_32.variants.sh20_sqrt : ∀ᶠ p in atTop, p.Prime → ∀ A : Finset (ZMod p), A.card = ⌊Real.sqrt p⌋₊ → ∃ c : (ZMod p)ˣ, HasGap (c • A) (⌊2 * Real.sqrt p⌋₊ - 2) := ⊢ ∀ᶠ (p : ℕ) in atTop, Nat.Prime p → ∀ (A : Finset (ZMod p)), A.card = ⌊√↑p⌋₊ → ∃ c, HasGap (c • A) (⌊2 * √↑p⌋₊ - 2) All goals completed! 🐙

In the regime $\omega(p) \sim c p$, this is Szemerédi's theorem [Gr24].

@[category research solved, AMS 5 11] theorem declaration uses 'sorry'green_32.variants.szemeredi_regime : ∀ c, 0 < c ∧ c < 1 → ∀ ω : ℕ → ℝ, ω ~[atTop] (fun p ↦ c * p) → HasLargeGapDilate ω := ⊢ ∀ (c : ℝ), 0 < c ∧ c < 1 → ∀ (ω : ℕ → ℝ), (ω ~[atTop] fun p => c * ↑p) → HasLargeGapDilate ω All goals completed! 🐙

In the regime $\omega(p) \le c \log p$, this is basically Dirichlet's lower bound for the size of Bohr sets [Gr24].

@[category research solved, AMS 5 11] theorem declaration uses 'sorry'green_32.variants.dirichlet_regime : ∃ c > 0, ∀ ω : ℕ → ℝ, (∀ᶠ p in atTop, 100 < ω p ∧ ω p ≤ c * Real.log p) → HasLargeGapDilate ω := ⊢ ∃ c > 0, ∀ (ω : ℕ → ℝ), (∀ᶠ (p : ℕ) in atTop, 100 < ω p ∧ ω p ≤ c * Real.log ↑p) → HasLargeGapDilate ω All goals completed! 🐙

Even what happens in the regime $\omega(p) \sim 10 \log p$ is unclear [Gr24].

@[category research open, AMS 5 11] theorem declaration uses 'sorry'green_32.variants.log_regime : answer(sorry) ↔ (∀ ω : ℕ → ℝ, ω ~[atTop] (fun p ↦ 10 * Real.log p) → HasLargeGapDilate ω) := ⊢ True ↔ ∀ (ω : ℕ → ℝ), (ω ~[atTop] fun p => 10 * Real.log ↑p) → HasLargeGapDilate ω All goals completed! 🐙

A set $A$ has a coset hole of size $L$ if there exists a subspace $W$ and a vector $v$ such that the affine space $v + W$ has size at least $L$ and is disjoint from $A$.

def HasCosetHole {n : ℕ} (A : Finset (𝔽₂ n)) (L : ℕ) : Prop := ∃ W : Submodule (ZMod 2) (𝔽₂ n), ∃ v : 𝔽₂ n, L ≤ Nat.card W ∧ ∀ w : W, v + (w : 𝔽₂ n) ∉ A

The empty set in $\mathbb{F}_2^n$ has a coset hole (using the trivial subspace).

@[category test, AMS 5 11] theorem hasCosetHole_empty (n : ℕ) : HasCosetHole (∅ : Finset (𝔽₂ n)) 0 := n:ℕ⊢ HasCosetHole ∅ 0 exact ⟨⊥, 0, Nat.zero_le _, fun _ => n:ℕx✝:↥⊥⊢ 0 + ↑x✝ ∉ ∅ All goals completed! 🐙⟩

Tom Sanders' finite field variant [Gr24]. If $N = 2^n$ and $A$ is a subset of size $\lfloor \sqrt{N} \rfloor$, then $A^c$ contains a coset of size at least $100\sqrt{N}$ for sufficiently large $n$.

@[category research solved, AMS 5 11] theorem declaration uses 'sorry'green_32.variants.finite_field : ∀ᶠ n in atTop, ∀ A : Finset (𝔽₂ n), A.card = ⌊Real.sqrt (2^n : ℝ)⌋₊ → HasCosetHole A ⌊100 * Real.sqrt (2^n : ℝ)⌋₊ := ⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (A : Finset (𝔽₂ n)), A.card = ⌊√(2 ^ n)⌋₊ → HasCosetHole A ⌊100 * √(2 ^ n)⌋₊ All goals completed! 🐙 end Green32