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

4 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 886

References:

Imports (1)
Imported by 1 file
  1. def Erdos886.Erdos886Divisors The set of divisors of $n$ in the interval $(n^{1/2}, n^{1/2} + n^{1/2-\epsilon})$ line 38 source

    Source documentation

    The set of divisors of $n$ in the interval $(n^{1/2}, n^{1/2} + n^{1/2-\epsilon})$.

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

    Statement uses: Nat, Real, Finset

    Proof uses: Finset.filter, And, LT.lt, HPow.hPow, HDiv.hDiv, OfNat.ofNat, HAdd.hAdd, HMul.hMul, HSub.hSub, Nat.divisors

    20 instances, coercions and auxiliary constants left out.

    noncomputable def Erdos886Divisors (n : ℕ) (ε : ℝ) (C : ℝ) : Finset ℕ :=
…
  2. theorem Erdos886.erdos_886 Let $\epsilon>0$ sorry line 49 source

    Source documentation

    Let $\epsilon>0$. Is it true that, for all large $n$, the number of divisors of $n$ in $(n^{1/2},n^{1/2}+n^{1/2-\epsilon})$ is $O_\epsilon(1)$?

    Erdős attributes this conjecture to Ruzsa.

    depends on sorry what this means

    Statement uses: Iff, True, Real, GT.gt, OfNat.ofNat, Exists, Nat, Filter.Eventually, LE.le, Finset.card, Erdos886.Erdos886Divisors, Filter.atTop

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

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_886 :
    answer(sorry) ↔ ∀ ε > 0, ∃ K : ℕ, ∀ᶠ n in atTop, (Erdos886Divisors n ε 1).card ≤ K := by
…

    Mentions: Erdos886.Erdos886Divisors

  3. theorem Erdos886.erdos_886.variants.rosenfeld_infinite Erdős and Rosenfeld [ErRo97] proved that there are infinitely many $n$ such that there are four divisors of $n$ in $(n^{1/2},n^{1/2}+16n^{1/4})$ sorry line 58 source

    Source documentation

    Erdős and Rosenfeld [ErRo97] proved that there are infinitely many $n$ such that there are four divisors of $n$ in $(n^{1/2},n^{1/2}+16n^{1/4})$.

    depends on sorry what this means

    Statement uses: Set.Infinite, Nat, Set.ofPred, LE.le, OfNat.ofNat, Finset.card, Erdos886.Erdos886Divisors, HDiv.hDiv, Real

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

    22 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_886.variants.rosenfeld_infinite :
    Set.Infinite {n | 4 ≤ (Erdos886Divisors n (1/4) 16).card} := by
…

    Mentions: Erdos886.Erdos886Divisors

  4. theorem Erdos886.erdos_886.variants.rosenfeld_bound Erdős and Rosenfeld [ErRo97] proved that, for any constant $C>0$, all large $n$ have at most $1+C^2$ many divisors in $[n^{1/2}, n^{1/2}+Cn^{1/4}]$ sorry line 67 source

    Source documentation

    Erdős and Rosenfeld [ErRo97] proved that, for any constant $C>0$, all large $n$ have at most $1+C^2$ many divisors in $[n^{1/2}, n^{1/2}+Cn^{1/4}]$.

    depends on sorry what this means

    Statement uses: Real, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, LE.le, Finset.card, Finset.filter, And, HPow.hPow, HDiv.hDiv, HAdd.hAdd, HMul.hMul, Nat.divisors, Filter.atTop

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

    54 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_886.variants.rosenfeld_bound :
    ∀ C > 0, ∀ᶠ (n : ℕ) in atTop,
    ((divisors n).filter (fun (d : ℕ) =>
      (n : ℝ) ^ (1 / 2 : ℝ) ≤ (d : ℝ) ∧ (d : ℝ) ≤ (n : ℝ) ^ (1 / 2 : ℝ) + C * (n : ℝ) ^ (1 / 4 : ℝ))).card
      ≤ 1 + C ^ 2 := by
…