FormalConjectures/ErdosProblems/69.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, 2 contain sorry, 0 declared as axioms

Erdős Problem 69

Reference: erdosproblems.com/69

Imports (1)
  1. theorem Erdos69.erdos_69 Is $$ \sum_{n\geq 2}\frac{\omega(n)}{2^n} $$ irrational? sorry line 40 source

    Source documentation

    Is $$ \sum_{n\geq 2}\frac{\omega(n)}{2^n} $$ irrational? (Here $\omega(n)$ counts the number of distinct prime divisors of $n$.)

    depends on sorry what this means

    Statement uses: Irrational, tsum, Real, Nat, HDiv.hDiv, ArithmeticFunction, ArithmeticFunction.cardDistinctFactors, HAdd.hAdd, OfNat.ofNat, HPow.hPow, SummationFilter.unconditional

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

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_69 : Irrational <| ∑' n, ω (n + 2) / 2 ^ (n + 2) := by
…
  2. theorem Erdos69.erdos_69.variants.specialisation_of_erdos_257 Tao observed that erdos_69 is a special case of erdos_257, since $$ \sum_{n\geq 2}\frac{\omega(n)}{2^n} = \sum_p \frac{1}{2^p - 1}. $$ sorry line 50 source

    Source documentation

    Tao observed that erdos_69 is a special case of erdos_257, since $$ \sum_{n\geq 2}\frac{\omega(n)}{2^n} = \sum_p \frac{1}{2^p - 1}. $$

    depends on sorry what this means

    Statement uses: Set, Nat, Set.ofPred, Nat.Prime, Eq, Real, tsum, HDiv.hDiv, ArithmeticFunction, ArithmeticFunction.cardDistinctFactors, HAdd.hAdd, OfNat.ofNat, HPow.hPow, SummationFilter.unconditional, HSub.hSub, Membership.mem

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

    60 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_69.variants.specialisation_of_erdos_257 :
    let A := { n : ℕ | n.Prime }
…