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

5 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 933

References:

Imports (1)
  1. def Erdos933.k The 2-adic valuation of $n(n+1)$ line 37 source

    Source documentation

    The 2-adic valuation of $n(n+1)$.

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

    Statement uses: Nat

    Proof uses: padicValNat, OfNat.ofNat, HMul.hMul, HAdd.hAdd

    5 instances, coercions and auxiliary constants left out.

    def k (n : ℕ) : ℕ := padicValNat 2 (n * (n + 1))
  2. def Erdos933.l The 3-adic valuation of $n(n+1)$ line 40 source

    Source documentation

    The 3-adic valuation of $n(n+1)$.

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

    Statement uses: Nat

    Proof uses: padicValNat, OfNat.ofNat, HMul.hMul, HAdd.hAdd

    5 instances, coercions and auxiliary constants left out.

    def l (n : ℕ) : ℕ := padicValNat 3 (n * (n + 1))
…
  3. theorem Erdos933.erdos_933 If $n(n+1)=2^k3^lm$, where $(m,6)=1$, then is it true that $\limsup_{n\to \infty} \frac{2^k3^l}{n\log n}=\infty$? sorry line 47 source

    Source documentation

    If $n(n+1)=2^k3^lm$, where $(m,6)=1$, then is it true that $\limsup_{n\to \infty} \frac{2^k3^l}{n\log n}=\infty$?

    depends on sorry what this means

    Statement uses: Iff, True, Eq, EReal, Filter.limsup, Nat, HDiv.hDiv, Real, HMul.hMul, HPow.hPow, OfNat.ofNat, Erdos933.k, Erdos933.l, Real.log, Filter.atTop, Top.top

    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_933 :
    answer(sorry) ↔
      atTop.limsup (fun n : ℕ ↦
        ((((2 ^ k n * 3 ^ l n : ℕ) : ℝ) / ((n : ℝ) * Real.log (n : ℝ))) : EReal)) = ⊤ := by
…

    Mentions: Erdos933.k, Erdos933.l

  4. theorem Erdos933.erdos_933.variants.mahler Mahler proved (a more general result that implies in particular) that $2^k3^l<n^{1+o(1)}$ sorry line 57 source

    Source documentation

    Mahler proved (a more general result that implies in particular) that $2^k3^l<n^{1+o(1)}$.

    depends on sorry what this means

    Statement uses: Exists, Nat, Real, And, Asymptotics.IsLittleO, Filter.atTop, OfNat.ofNat, Filter.Eventually, LT.lt, HMul.hMul, HPow.hPow, Erdos933.k, Erdos933.l, HAdd.hAdd

    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 erdos_933.variants.mahler :
    ∃ c : ℕ → ℝ, (c =o[atTop] (1 : ℕ → ℝ)) ∧
      ∀ᶠ n in atTop, ((2 ^ k n * 3 ^ l n : ℕ) : ℝ) < (n : ℝ) ^ (1 + c n) := by
…

    Mentions: c, Erdos933.k, Erdos933.l

  5. theorem Erdos933.erdos_933.variants.lower_bound Erdős [Er76d] wrote 'it is easy to see' that for infinitely many $n$, $2^k 3^l > n\log n$ line 69 source

    Source documentation

    Erdős [Er76d] wrote 'it is easy to see' that for infinitely many $n$, $2^k 3^l > n\log n$.

    Steinerberger has noted a simple proof of this fact follows from taking $n=2^{3^r}$ for any integer $r\geq 1$, when $k=3^r$ and $l=r+1$.

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

    Statement uses: Set.Infinite, Nat, Set.ofPred, GT.gt, Real, HMul.hMul, HPow.hPow, OfNat.ofNat, Erdos933.k, Erdos933.l, Real.log

    Proof uses: Set.infinite_of_injective_forall_mem, HAdd.hAdd, Function.Injective.comp, Nat.pow_right_injective, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, add_left_injective, Eq, Eq.mpr, padicValNat, id, congrArg, Erdos933.k.eq_1, padicValNat.mul, ne_of_gt, pow_pos, Mathlib.Meta.Positivity.pos_of_isNat and 146 more

    158 instances, coercions and auxiliary constants left out.

    Tactic trace: 37 steps

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

    theorem erdos_933.variants.lower_bound :
    Set.Infinite { n : ℕ | ((2 ^ k n * 3 ^ l n : ℕ) : ℝ) > (n : ℝ) * Real.log (n : ℝ) } := by
…

    Mentions: Erdos933.k, Erdos933.l