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

8 declarations, 2 contain sorry, 0 declared as axioms

Numerator of $\zeta(4n)/\zeta(2n)^2$ (with $a(0)=2$ instead of $-2$)

The ratio $\zeta(4n)/\zeta(2n)^2$ for $n \ge 1$ is the rational number $$ Q_n = -2 \frac{B_{4n}}{B_{2n}^2 \binom{4n}{2n}} $$ where $B_k$ is the $k$-th Bernoulli number. The sequence $a(n)$ is the numerator of $Q_n$, with $a(0)$ defined as $2$.

References:

Imports (1)
  1. def OeisA114362.a The primary defining sequence a line 44 source

    Source documentation

    The primary defining sequence a. Numerator of $\zeta(4n)/\zeta(2n)^2$ (with $a(0)=2$ instead of $-2$).

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

    Statement uses: Nat

    Proof uses: ite, Eq, OfNat.ofNat, Rat, bernoulli, HMul.hMul, Nat.choose, HDiv.hDiv, Neg.neg, Int.natAbs, Rat.num

    11 instances, coercions and auxiliary constants left out.

    noncomputable def a (n : ℕ) : ℕ :=
…
  2. theorem OeisA114362.a_0 line 55 source

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

    Statement uses: Eq, Nat, OeisA114362.a, OfNat.ofNat

    Proof uses: Eq.refl

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. theorem OeisA114362.a_1 line 59 source

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

    Statement uses: Eq, Nat, OeisA114362.a, OfNat.ofNat

    Proof uses: Eq.mpr, Int.natAbs, Rat.num, HDiv.hDiv, Rat, Neg.neg, HMul.hMul, bernoulli, Inv.inv, Nat.choose, id, congrFun', congrArg, Eq.trans, ite, ite_cond_eq_false, Int, congr, mul_one, neg_mul and 45 more

    65 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  4. theorem OeisA114362.a_2 line 64 source

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

    Statement uses: Eq, Nat, OeisA114362.a, OfNat.ofNat

    Proof uses: id, Eq.mpr, ite, Rat, bernoulli, HMul.hMul, Nat.choose, HDiv.hDiv, Neg.neg, Int.natAbs, Rat.num, Or, Int, bernoulli', Eq.trans, congrFun', congrArg, False, ite_congr, eq_false_of_decide and 80 more

    100 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  5. theorem OeisA114362.a_3 line 75 source

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

    Statement uses: Eq, Nat, OeisA114362.a, OfNat.ofNat

    Proof uses: id, Eq.mpr, ite, Rat, bernoulli, HMul.hMul, Nat.choose, HDiv.hDiv, Neg.neg, Int.natAbs, Rat.num, HAdd.hAdd, bernoulli', congrFun', congrArg, ite_congr, False, eq_false, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat and 82 more

    103 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  6. theorem OeisA114362.conjecture1 Conjecture: if an integer $n > 1$ is odd, then $\zeta(2n)/\zeta(n)^2$ is irrational sorry line 89 source

    Source documentation

    Conjecture: if an integer $n > 1$ is odd, then $\zeta(2n)/\zeta(n)^2$ is irrational. Cf. W. Kohnen (link) and my conjecture in A348829. - Thomas Ordowski, Jan 05 2022

    depends on sorry what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, Odd, Irrational, Complex.re, HDiv.hDiv, Complex, riemannZeta, HMul.hMul, HPow.hPow

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

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem conjecture1 (n : ℕ) (hn_gt_one : 1 < n) (hn_odd : Odd n) :
    Irrational ((riemannZeta (2 * n : ℂ) / (riemannZeta (n : ℂ)) ^ 2).re) := by
…
  7. def OeisA114362.t t n is used in the second conjecture line 94 source

    Source documentation

    t n is used in the second conjecture.

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

    Statement uses: Nat, Real

    Proof uses: HDiv.hDiv, Complex.re, riemannZeta, HMul.hMul, Complex, OfNat.ofNat, HPow.hPow

    14 instances, coercions and auxiliary constants left out.

    noncomputable def t (n : ℕ) : ℝ :=
…
  8. theorem OeisA114362.conjecture2 sorry line 105 source

    depends on sorry what this means

    Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, HSub.hSub, HDiv.hDiv, OfNat.ofNat, OeisA114362.t, HAdd.hAdd, HPow.hPow

    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.