Skip to content

Erdős problem 221

Start work

Is there a set A⊂NA\subset\mathbb{N} such that, for all large NN, ∣A∩{1,…,N}∣≪N/log⁡N\lvert A\cap\{1,\ldots,N\}\rvert \ll N/\log N and such that every large integer can be written as 2k+a2^k+a for some k≥0k\geq 0 and a∈Aa\in A?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/221.lean

Formal Conjectures

FormalConjectures/ErdosProblems/221.leanErdos221.erdos_2214 linesExact file
True ↔  ∃ A,    ((fun N => ↑{a | a ∈ A ∧ a ≤ N}.ncard) =O[Filter.atTop] fun N => ↑N / Real.log ↑N) ∧      ∀ᶠ (N : ℕ) in Filter.atTop, ∃ k a, 0 ≤ k ∧ a ∈ A ∧ N = 2 ^ k + a
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:221
  • PLBY Lean proofsErdosProblems.Erdos221

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry