Source labels openChecked July 26, 2026

Ben Green's Open Problem 41

How many rotated (about the origin) copies of the 'pyjama set' $\\{(x, y) \in \mathbb{R}^2 : \text{dist}(x, \mathbb{Z}) \leq \varepsilon\\}$ are needed to cover $\mathbb{R}^2$ ?

Geometry AMS 51 AMS 52

Mathematical statement

How many rotated (about the origin) copies of the 'pyjama set' $\\{(x, y) \in \mathbb{R}^2 : \text{dist}(x, \mathbb{Z}) \leq \varepsilon\\}$ are needed to cover $\mathbb{R}^2$ ?

In particular, can one find a better bound than the best-known bound from [KrLe25]?

Statement source: Green's Open Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

green_41

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem green_41 :    ∃ C : ℝ, C > 0 ∧ ∃ ε₀ > 0, ∀ ε ∈ Ioc 0 ε₀,      let ans := (answer(sorry) : ℝ)      (minCopies ε : ℝ) ≤ ans ∧ ans < Real.exp (Real.exp (Real.exp (ε ^ (-C)))) := by  sorry

Statement source: Formal Conjectures
Lean version: v4.27.0
Placeholder: Present; no proof artifact
Source evidence: Pinned source index
Fidelity review: Community formulation

References

Pinned Formal Conjectures sourceformalization Ben Green's Open Problem 41background