Source labels openChecked July 26, 2026

Ben Green's Open Problem 61

Suppose that $A + A$ contains the first $n$ squares. Is $|A| \geq n^{1 - o(1)}$ ?

Mathematical statement

Suppose that $A + A$ contains the first $n$ squares. Is $|A| \geq n^{1 - o(1)}$ ?

It is known that necessarily $|A| \geq n^{2/3 - o(1)}$ , whilst in the other direction there do exist such $A$ with $|A| \ll_C n / \log^C n$ for any $C$ .

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_61

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem green_61 :    answer(sorry) ↔      ∃ f : ℕ → ℝ, Tendsto f atTop (𝓝 0) ∧        ∀ n : ℕ, n ≥ 1 → ∀ (A : Finset ℕ),          (Finset.Icc 1 n).image (· ^ 2) ⊆ A + A →            (n : ℝ) ^ (1 - f n) ≤ A.card := 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 61background