Number theory

Erdős 41

Let A ⊆ ℕ be an infinite set such that the triple sums a + b + c are all distinct for a, b, c in A (aside from the trivial coincidences). Is it true that liminf n → ∞ |A ∩ {1, …, N}| / N^(1/3) = 0?

References

erdosproblems.com/41

No one has attempted this yet.

Formal statement

Lean type

∀ (A : Set ℕ),
  Erdos41.NtupleCondition A 3 →
    A.Infinite → Filter.liminf (fun N => ↑(A ∩ Set.Icc 1 N).ncard / ↑N ^ (1 / 3)) Filter.atTop = 0

What you must prove

import FormalConjectures.ErdosProblems.«41»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos41.erdos_41" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/41.lean

Source type SHA-256: sha256:d254b0ecdd34012c0f1b4044e03eb4cff0fda16778d2cd2a1f1d7b047e0cf084
Task id: fc-379fc029-erdos41-erdos-41-ca090a20de-formalized-v1
Task commitment: sha256:a15413ffa2e3a99753c439cd30f7a2f06ac86a98d30e326081c983bfce82fdcc

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.