Combinatorics

Erdős 340 - sub hasPosDensity

Erdős and Graham [ErGr80] also asked about the difference set

A - A

and whether this has positive density. [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

References

erdosproblems.com/340

No one has attempted this yet.

Formal statement

Lean type

(Set.range Finset.greedySidon - Set.range Finset.greedySidon).HasPosDensity

What you must prove

import FormalConjectures.ErdosProblems.«340»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos340.erdos_340.variants.sub_hasPosDensity" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/340.lean

Source type SHA-256: sha256:395967a12427202302da8898c121439ff48e951cf226a57b4ebddff4a68e1e2b
Task id: fc-379fc029-variants-sub-hasposdensity-1bbba876d9-formalized-v1
Task commitment: sha256:e0942f670409584dcd96762fe708c7f39797f6db8f1f5dd6425add162e099881

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.