FormalConjectures/OEIS/180017.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

7 declarations, 1 contain sorry, 0 declared as axioms

Difference of digit sums in base 3 and base 2

Difference of sums of digits of $n$ in ternary and in binary: $$a(n) = \sum \mathrm{digits}_3(n) - \sum \mathrm{digits}_2(n).$$

References:

Imports (1)
  1. def OeisA180017.a Difference of sums of digits of $n$ in ternary and in binary line 34 source

    Source documentation

    Difference of sums of digits of $n$ in ternary and in binary.

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

    Statement uses: Nat, Int

    Proof uses: HSub.hSub, List.sum, Nat.digits, OfNat.ofNat

    8 instances, coercions and auxiliary constants left out.

    def a (n : ℕ) : ℤ :=
…
  2. theorem OeisA180017.a_0 line 38 source

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

    Statement uses: Eq, Int, OeisA180017.a, OfNat.ofNat, Nat

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HSub.hSub, List.sum, Nat.digits, congr, List, List.nil, Nat.digits_zero, CharP.cast_eq_zero, sub_self, eq_self, eq_true, True.intro

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. theorem OeisA180017.a_1 line 41 source

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

    Statement uses: Eq, Int, OeisA180017.a, OfNat.ofNat, Nat

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HSub.hSub, List.sum, Nat.digits, congr, List.cons, List.nil, List, HMod.hMod, HDiv.hDiv, Nat.digits_of_two_le_of_pos, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true and 12 more

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  4. theorem OeisA180017.a_2 line 44 source

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

    Statement uses: Eq, Int, OeisA180017.a, OfNat.ofNat, Nat

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HSub.hSub, List.sum, Nat.digits, congr, List.cons, List.nil, List, HMod.hMod, HDiv.hDiv, Nat.digits_of_two_le_of_pos, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true and 18 more

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  5. theorem OeisA180017.a_3 line 47 source

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

    Statement uses: Eq, Int, OeisA180017.a, OfNat.ofNat, Nat, Neg.neg

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HSub.hSub, List.sum, Nat.digits, congr, List.cons, List.nil, List, HMod.hMod, HDiv.hDiv, Nat.digits_of_two_le_of_pos, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true and 19 more

    48 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  6. theorem OeisA180017.a_4 line 50 source

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

    Statement uses: Eq, Int, OeisA180017.a, OfNat.ofNat, Nat

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HSub.hSub, List.sum, Nat.digits, congr, List.cons, List.nil, List, HMod.hMod, HDiv.hDiv, Nat.digits_of_two_le_of_pos, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true and 19 more

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  7. theorem OeisA180017.conjecture "This sequence is positive on average, since 1/log(3) > 1/log(4) sorry line 56 source

    Source documentation

    "This sequence is positive on average, since 1/log(3) > 1/log(4). Do all integers appear infinitely often?" - Charles R Greathouse IV, Feb 07 2013

    depends on sorry what this means

    Statement uses: Int, Set.Infinite, Nat, Set.ofPred, Eq, OeisA180017.a

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

    1 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem conjecture (z : ℤ) : Set.Infinite {n : ℕ | a n = z} := by
…

    Mentions: OeisA180017.a