Formal target: Corpus.Arxiv210712475CollatzLike.CollatzLike

For $n > 8$, $2^n$ is not the the sum of distinct powers of $3$.

Exact formal statement

∀ (n : Nat), LT.lt.{0} 8 n → Membership.mem.{0, 0} (Nat.digits 3 (HPow.hPow.{0, 0, 0} 2 n)) 2

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

Environment availability: available.