Skip to content

Erdős problem 818

Start work

Let AA be a finite set of integers such that ∣A+A∣≪∣A∣\lvert A+A\rvert \ll \lvert A\rvert. Is it true that ∣AA∣≫∣A∣2(log⁡∣A∣)C\lvert AA\rvert \gg \frac{\lvert A\rvert^2}{(\log \lvert A\rvert)^C} for some constant C>0C>0?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/818.lean

Formal Conjectures

FormalConjectures/ErdosProblems/818.leanErdos818.erdos_8189 linesExact file
True ↔  ∀ (K : ℝ),    0 < K →      ∃ C,        0 < C ∧          ∃ c,            0 < c ∧              ∀ (A : Finset ℤ),                2 ≤ A.card → ↑(A + A).card ≤ K * ↑A.card → c * ↑A.card ^ 2 / Real.log ↑A.card ^ C ≤ ↑(A * A).card
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:818
  • PLBY Lean proofsErdosProblems.Erdos818

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry