Conjectures.io

Number theory

Erdős 1142

Are there infinitely many n>2n > 2 such that n−2kn - 2^k is prime for all k≥1k \geq 1 with 2k<n2^k < n? The only known such nn are 4,7,15,21,45,75,1054, 7, 15, 21, 45, 75, 105 (OEIS [A039669](https://oeis.org/A039669)).

References

  • [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999).
  • [MiWe69] Mientka, W. E. and Weitzenkamp, R. C., On f-plentiful numbers, Journal of Combinatorial Theory, Volume 7, Issue 4, December 1969, pages 374-377.

No one has attempted this yet.

Formal statement

Lean type

True ↔ Infinite ↑{n | Erdos1142.Erdos1142Prop n}

What you must prove

import FormalConjectures.ErdosProblems.«1142»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos1142.erdos_1142" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/1142.lean

Source type SHA-256
sha256:04dfbf3c7c9e470546dd6f9b372fcff4ddf4f1369f23d66a3fccc4ee628ee887
Task id
fc-379fc029-erdos1142-erdos-1142-a00a1d97b1-formalized-v1
Task commitment
sha256:0096d295218f9a97cd9d90d88aa944cac438b9fd4f3290b31b053375870e3aaa

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.