Number theory

Erdős 479

Is it true that, for all

k\neq 1

, there are infinitely many

n

such that

2^n\equiv k\pmod{n}

References

erdosproblems.com/479

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∀ k > 1, {n | 2 ^ n ≡ k [MOD n]}.Infinite

What you must prove

import FormalConjectures.ErdosProblems.«479»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos479.erdos_479" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/479.lean

Source type SHA-256: sha256:c20dd4a8e6b82d93c8dd560d6f1dc58abb05c3c35925d3cae21535502306d94f
Task id: fc-379fc029-erdos479-erdos-479-e30691e7d7-formalized-v1
Task commitment: sha256:4462cddf070281fad99996c691749184e8be3ef70fead8dc0691f6e00d189542

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.