Conjectures.io

Number theory

Green60.green_60

Is there an absolute constant c>0c > 0 such that, whenever A⊆NA ⊆ \mathbb{N} is a set of squares with ∣A∣≥2|A| ≥ 2, the sumset A+AA + A satisfies ∣A+A∣≥∣A∣1+c|A + A| ≥ |A|^{1 + c}?

References

  • Ben Green's Open Problem 60

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∃ c > 0, ∀ (A : Finset ℕ), (∀ a ∈ A, IsSquare a) → 2 ≤ A.card → ↑(A + A).card ≥ ↑A.card ^ (1 + c)

What you must prove

import FormalConjectures.GreensOpenProblems.«60»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green60.green_60" := by
  sorry

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/60.lean

Source type SHA-256
sha256:dae916f88c61d34e3fbdf05354813ffe54f4ec35b1c65cd277599fcc501f5703
Task id
fc-379fc029-green60-green-60-1e9006bfbf-formalized-v1
Task commitment
sha256:9bec7154af29b7fe1b0257091ac9cfd6270d4b00cc677e38ca25ebd8898f8222

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.