FormalConjectures/ErdosProblems/266.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 266

Reference: erdosproblems.com/266

Imports (1)
  1. theorem Erdos266.erdos_266 sorry line 43 source

    depends on sorry what this means

    Statement uses: Not, Nat, And, GE.ge, OfNat.ofNat, Summable, Real, HDiv.hDiv, SummationFilter.unconditional, Exists, Irrational, tsum, HAdd.hAdd

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

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. theorem Erdos266.erdos_266.variants.all_rationals In fact, Kovač and Tao proved in [KoTa24] that there exists a strictly increasing sequence sorry line 57 source

    Source documentation

    In fact, Kovač and Tao proved in [KoTa24] that there exists a strictly increasing sequence $a_n$ of positive integers such that $\sum \frac{1}{a_n + t}$ converges to a rational number for all $t \in \mathbb{Q}$ such that $t \ne -a_n$ for any $n$.

    [KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. arXiv:2406.17593 (2024).

    L4DEL explanation

    In fact, Kovač and Tao proved in [KoTa24] that there exists a strictly increasing sequence $a_n$ of positive integers such that $\sum \frac{1}{a_n + t}$ converges to a rational number for all $t \in \mathbb{Q}$ such that $t \ne -a_n$ for any $n$. [KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. arXiv:2406.17593 (2024).

    Sources and attribution: Pinned Lean source (1646ca16afd6)

    depends on sorry what this means

    Statement uses: Exists, Nat, And, StrictMono, GE.ge, OfNat.ofNat, Rat, Not, Eq, Neg.neg, HasSum, Real, HDiv.hDiv, HAdd.hAdd, SummationFilter.unconditional

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

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_266.variants.all_rationals:
    ∃ a : ℕ → ℕ, StrictMono a ∧ a 0 ≥ 1 ∧
      (∀ t : ℚ, (¬ ∃ n : ℕ, t = -(a n)) →
        (∃ q : ℚ, HasSum (fun n : ℕ => ((1 : ℝ) / ((a n) + t))) q)) := by
…