Formal target: Corpus.Erdos11.erdos_11

Is every odd $n > 1$ the sum of a squarefree number and a power of 2?

Exact formal statement

∀ (n : Nat),
  Odd.{0} n →
    LT.lt.{0} 1 n →
      Exists.{1} fun k =>
        Exists.{1} fun l => And (Squarefree.{0} k) (Eq.{1} n (HAdd.hAdd.{0, 0, 0} k (HPow.hPow.{0, 0, 0} 2 l)))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record