Digit $2$ in base $3$ representation of $2^n$
For , is not the the sum of distinct powers of . Expressed here in terms of the base digits of .
Mathematical statement
For , is not the the sum of distinct powers of . Expressed here in terms of the base digits of .
This conjecture is equivalent to the halting of a -state -symbol Turing Machine.
TODO(lezeau): Formalize the Turing Machine version of this problem.
Source: Hardness of Busy Beaver Value BB(15): https://link.springer.com/chapter/10.1007/978-3-031-72621-7_9 This is also https://arxiv.org/abs/2107.12475.
Statement source: arXiv statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
CollatzLike
theorem CollatzLike (n : ℕ) (hn : 8 < n) : 2 ∈ Nat.digits 3 (2^n) := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References