Green's open problem 2

Let

A \subset \mathbf{Z}

be a set of

n

integers. Is there a set

S \subset A

of size

(\log n)^{100}

such that the restricted sumset

S \hat{+} S

is disjoint from

A

Withdrawn 30 Sept 2026

WITHDRAWN (removed from the open catalog at Ben Green’s request; prior solved entries and results remain available)

nobody has started

Formal statement

Proof target

import FormalConjectures.GreensOpenProblems.«2»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green2.green_2" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔
  ∀ᶠ (n : ℕ) in Filter.atTop,
    ∀ (A : Finset ℤ), A.card = n → ↑(Green2.maxRestrictedSumAvoidingSubsetSize A) ≥ Real.log ↑n ^ 100

Original conjecture source: FormalConjectures/GreensOpenProblems/2.lean

Task id: fc-6a786f99-green2-green-2-8eb34f0fec-formalized-v1
Task commitment: sha256:bcdd4623b0a627b01479de5e7150466a1b2f46f464532cf60d1ab8c43d1e2ffb

References

[Gr24] Green, Ben. "100 open problems." (2024).
[Er65] P. Erdős. Extremal problems in number theory, In Proc. Sympos. Pure Math., Vol. VIII, pages 181–189. Amer. Math. Soc., Providence, R.I., 1965.
[Sa21] Sanders, Tom. "The Erdős–Moser Sum-free Set Problem." Canadian Journal of Mathematics 73.1 (2021): 63-107.
[Ru05] I. Z. Ruzsa, Sum-avoiding subsets. Ramanujan J., 9 (2005) (1-2):77–82.
[Ch71] S. L. G. Choi. On a combinatorial problem in number theory. Proc. London Math. Soc. (3), 23:629–642, 1971. doi:10.1112/plms/s3-23.4.629.
[BSS00] A. Baltz, T. Schoen, and A. Srivastav. Probabilistic construction of small strongly sum-free sets via large Sidon sets. Colloq. Math., 86(2):171–176, 2000. doi:10.4064/cm-86-2-171-176.

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.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord

Contribution history

Individual lemmas, special cases and supporting work, shown in their original scope.

Nothing has been published against this problem yet.

Where this lives

conjectures-tasks

The pinned statement, the Lean challenge file and the exact bundle you build against.

pool/tier-1/green-2-formalized →

conjectures-contribution

Every published piece for this problem, with its Lean source and its signed record.

contributions/green-2 →