/-
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 FormalConjecturesUtilGreen's Open Problem 39
[Gr24] Green, Ben. "100 open problems." (2024).
[BJR11] Bollobás, Béla, Svante Janson, and Oliver Riordan. "On covering by translates of a set." Random Structures & Algorithms 38.1‐2 (2011): 33-67.
open Filter Topologyopen scoped Pointwise
namespace Green39
The proportion of subsets of $\mathbb{Z}/p\mathbb{Z}$ of size $k$ that can cover $\mathbb{Z}/p\mathbb{Z}$ using at most $c$ translates.
If p = 0 or k > p, return 0 by convention.
def proportionCoverable (p k c : ℕ) : ℚ :=
if h : p = 0 then 0
else if k > p then 0
else
have : NeZero p := ⟨h⟩
let S : Finset (Finset (ZMod p)) := Finset.powersetCard k Finset.univ
let coverable := S.filter (fun A => ∃ T : Finset (ZMod p), T.card ≤ c ∧ A + T = Finset.univ)
(coverable.card : ℚ) / (S.card : ℚ)
@[category test, AMS 5 60]
theorem proportionCoverable_p_p_1 : proportionCoverable 3 3 1 = 1 := ⊢ proportionCoverable 3 3 1 = 1 All goals completed! 🐙
@[category test, AMS 5 60]
theorem proportionCoverable_t_0 : proportionCoverable 5 2 0 = 0 := ⊢ proportionCoverable 5 2 0 = 0 All goals completed! 🐙
@[category test, AMS 5 60]
theorem proportionCoverable_2_1_2 : proportionCoverable 2 1 2 = 1 := ⊢ proportionCoverable 2 1 2 = 1 All goals completed! 🐙
@[category test, AMS 5 60]
theorem proportionCoverable_3_1_2 : proportionCoverable 3 1 2 = 0 := ⊢ proportionCoverable 3 1 2 = 0 All goals completed! 🐙
@[category test, AMS 5 60]
theorem proportionCoverable_a_gt_p : proportionCoverable 3 4 2 = 0 := ⊢ proportionCoverable 3 4 2 = 0 All goals completed! 🐙
@[category test, AMS 5 60]
theorem proportionCoverable_7_4_2 :
proportionCoverable 7 4 2 = (3 : ℚ) / 5 := ⊢ proportionCoverable 7 4 2 = 3 / 5
All goals completed! 🐙
@[category test, AMS 5 60]
theorem proportionCoverable_11_3_4 :
proportionCoverable 11 3 4 = (1 : ℚ) / 3 := ⊢ proportionCoverable 11 3 4 = 1 / 3
All goals completed! 🐙
@[category test, AMS 5 60]
theorem proportionCoverable_11_4_3 :
proportionCoverable 11 4 3 = (1 : ℚ) / 6 := ⊢ proportionCoverable 11 4 3 = 1 / 6
All goals completed! 🐙
If $A \subset \mathbb{Z}/p\mathbb{Z}$ is random, $|A| = \sqrt{p}$, can we almost surely cover $\mathbb{Z}/p\mathbb{Z}$ with $100\sqrt{p}$ translates of $A$? [Gr24]
@[category research open, AMS 5 60]
theorem green_39 : answer(sorry) ↔
Tendsto
(fun p : {q : ℕ // q.Prime} ↦
let k := Nat.sqrt p
let c := 100 * k
(proportionCoverable p k c : ℝ))
atTop (𝓝 1) := ⊢ True ↔
Tendsto
(fun p =>
let k := (↑p).sqrt;
let c := 100 * k;
↑(proportionCoverable (↑p) k c))
atTop (𝓝 1)
All goals completed! 🐙
"I do not know how to answer this even with 100 replaced by 1.01." [Gr24]"
@[category research open, AMS 5 60]
theorem green_39.variant_101 : answer(sorry) ↔
Tendsto
(fun p : {q : ℕ // q.Prime} ↦
let k := Nat.sqrt p
let c := ⌊1.01 * (k : ℝ)⌋₊
(proportionCoverable p k c : ℝ))
atTop (𝓝 1) := ⊢ True ↔
Tendsto
(fun p =>
let k := (↑p).sqrt;
let c := ⌊1.01 * ↑k⌋₊;
↑(proportionCoverable (↑p) k c))
atTop (𝓝 1)
All goals completed! 🐙
Similar questions are interesting with $\sqrt{p}$ replaced by $p^\theta$ for any $\theta \le 1/2$. [Gr24]
NOTE: using $C p^\theta$ translates as stated makes the conjecture trivially false by the pigeonhole principle. Indeed for a set of size $p^\theta$, we cover at most $C p^{2\theta}$ elements, which is strictly less than $p$ for $\theta < 1/2$. We interpret the question as asking whether $O(p^{1-\theta})$ translates suffice. This generalizes the main conjecture where $\sqrt{p} = p^{1-1/2}$.
@[category research open, AMS 5 60]
theorem green_39.variant_theta : answer(sorry) ↔
∀ (θ : ℝ), 0 < θ → θ ≤ 1/2 →
∃ C > 1, Tendsto
(fun p : {q : ℕ // q.Prime} ↦
let k := ⌊(p : ℝ) ^ θ⌋₊
let c := ⌊C * (p : ℝ) ^ (1 - θ)⌋₊
(proportionCoverable p k c : ℝ))
atTop (𝓝 1) := ⊢ True ↔
∀ (θ : ℝ),
0 < θ →
θ ≤ 1 / 2 →
∃ C > 1,
Tendsto
(fun p =>
let k := ⌊↑↑p ^ θ⌋₊;
let c := ⌊C * ↑↑p ^ (1 - θ)⌋₊;
↑(proportionCoverable (↑p) k c))
atTop (𝓝 1)
All goals completed! 🐙
end Green39