Conjectures.io

Number theory

Erdős 936 - two pow add one

Is 2n+12^n + 1 powerful for finitely many nn?

References

No one has attempted this yet.

Formal statement

Lean type

True ↔ Erdos936.EventuallyNotPowerful fun x => 2 ^ x + 1

What you must prove

import FormalConjectures.ErdosProblems.«936»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos936.erdos_936.variants.two_pow_add_one" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/936.lean

Source type SHA-256
sha256:56857fb4f011f4102531040d48634aa7cbdf8195d55c530ad57a8535888868a2
Task id
fc-379fc029-variants-two-pow-add-one-4646479eea-formalized-v1
Task commitment
sha256:2b04a42deef4628bd7bab127a480edb8fcf130b9d53392d8c28c48ad9f575106

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.