Formal target: Corpus.Erdos406.erdos_406.variants.one_two

If we only allow the digits $1$ and $2$ then $2^{15}$ seems to be the largest such power of $2$.

Exact formal statement

IsGreatest.{0}
  (Set.ofPred.{0} fun n =>
    And n.isPowerOfTwo (HasSubset.Subset.{0} (Nat.digits 3 n) (List.cons.{0} 1 (List.cons.{0} 2 List.nil.{0}))))
  (HPow.hPow.{0, 0, 0} 2 15)

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record