FormalConjectures/Arxiv/2107.12475/CollatzLike.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

2 declarations, 1 contain sorry, 0 declared as axioms

Digit $2$ in base $3$ representation of $2^n$

References:

Imports (1)
  1. theorem Arxiv.«2107.12475».CollatzLike For $n > 8$, $2^n$ is not the the sum of distinct powers of $3$ sorry line 48 source

    Source documentation

    For $n > 8$, $2^n$ is not the the sum of distinct powers of $3$. Expressed here in terms of the base $3$ digits of $n$.

    This conjecture is equivalent to the halting of a $15$-state $2$-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.

    depends on sorry what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, Membership.mem, List, Nat.digits, HPow.hPow

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem CollatzLike (n : ℕ) (hn : 8 < n) : 2 ∈ Nat.digits 3 (2^n) := by
…
  2. theorem Arxiv.«2107.12475».two_not_in_digits_three_pow_eight For $n = 8$, $2$ is not contained in the base $3$ digits of $n$ line 55 source

    Source documentation

    For $n = 8$, $2$ is not contained in the base $3$ digits of $n$.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Not, Membership.mem, Nat, List, Nat.digits, OfNat.ofNat, HPow.hPow

    Proof uses: of_eq_true, Eq.trans, True, False, congrArg, Or, Eq, List.cons, List.nil, congrFun', HMod.hMod, HDiv.hDiv, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.trans, Nat.pow, Mathlib.Meta.NormNum.IsNatPowT.bit0 and 17 more

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem two_not_in_digits_three_pow_eight : 2 ∉ Nat.digits 3 (2^8) := by norm_num
…