Source labels openChecked July 26, 2026

Green's Open Problem 47

Suppose that a large sieve process leaves a set of quadratic size. Is that set quadratic?

Mathematical statement

Suppose that a large sieve process leaves a set of quadratic size. Is that set quadratic?

The following very particular instance is probably the simplest [Gr24]: Suppose that $A \subset \mathbb{N}$ is a set with the property that $|A \pmod p| \leqslant \frac{1}{2}(p + 1)$ for all sufficiently large $p$ . Is it true that either $|A \cap [X]| \ll X^{1/2} / \log^{100} X$ , or $A$ is contained in the image of $\mathbb{Z}$ under a quadratic map $\phi : \mathbb{Q} \to \mathbb{Q}$ ?

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_47

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem green_47 :    answer(sorry) ↔ ∀ A : Set ℕ,      (∀ᶠ p in atTop, Nat.Prime p → Set.ncard (Set.image (fun a : ℕ => (a : ZMod p)) A) ≤ (p + 1) / 2) →      ((fun X : ℕ => ((A ∩ Set.Iic X).ncard : ℝ)) ≪ (fun X : ℕ => Real.sqrt (X : ℝ) / (Real.log (X : ℝ)) ^ 100))      ∨ (∃ P : Polynomial ℚ, P.degree = 2 ∧ ∀ a ∈ A, ∃ z : ℤ, (a : ℚ) = P.eval (z : ℚ)) := 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 100 Open Problemsbackground