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

3 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 1004

Reference: erdosproblems.com/1004

Imports (1)
  1. def Erdos1004.IsDistinctTotientRun IsDistinctTotientRun n K means that the values φ(n+1), φ(n+2), ..., φ(n+K) are all distinct line 33 source

    Source documentation

    IsDistinctTotientRun n K means that the values φ(n+1), φ(n+2), ..., φ(n+K) are all distinct.

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

    Statement uses: Nat

    Proof uses: Set.InjOn, Nat.totient, Set.Icc, HAdd.hAdd, OfNat.ofNat

    4 instances, coercions and auxiliary constants left out.

    def IsDistinctTotientRun (n K : ℕ) : Prop :=
…
  2. theorem Erdos1004.erdos_1004 For any fixed c > 0, if x is sufficiently large then there exists n ≤ x such that the values of φ(n+k) are all distinct for 1 ≤ k ≤ (log x)^c sorry line 42 source

    Source documentation

    For any fixed c > 0, if x is sufficiently large then there exists n ≤ x such that the values of φ(n+k) are all distinct for 1 ≤ k ≤ (log x)^c. This is an open problem.

    depends on sorry what this means

    Statement uses: Iff, True, Real, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, Exists, And, LE.le, Erdos1004.IsDistinctTotientRun, Nat.floor, HPow.hPow, Real.log, Filter.atTop

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

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_1004 :
    answer(sorry) ↔ ∀ c > (0 : ℝ), ∀ᶠ x in atTop, ∃ n ≤ x,
      IsDistinctTotientRun n ⌊(Real.log (x : ℝ)) ^ c⌋₊ := by
…

    Mentions: c, Erdos1004.IsDistinctTotientRun

  3. theorem Erdos1004.erdos_1004.variants.le_of_isDistinctTotientRun Erdős, Pomerance, and Sárközy [EPS87] proved that if φ(n+k) are all distinct for 1 ≤ k ≤ K then K ≤ n / exp(c (log n)^{1/3}) for some constant c > 0 sorry line 53 source

    Source documentation

    Erdős, Pomerance, and Sárközy [EPS87] proved that if φ(n+k) are all distinct for 1 ≤ k ≤ K then K ≤ n / exp(c (log n)^{1/3}) for some constant c > 0. Here we state the existence of such a constant c.

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Real, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, Erdos1004.IsDistinctTotientRun, LE.le, HDiv.hDiv, Real.exp, HMul.hMul, HPow.hPow, Real.log, Filter.atTop

    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_1004.variants.le_of_isDistinctTotientRun :
    answer(True) ↔ ∃ (c : ℝ) (hc : c > 0),
      ∀ᶠ n in atTop, ∀ (K : ℕ), IsDistinctTotientRun n K →
        (K : ℝ) ≤ (n : ℝ) / Real.exp (c * (Real.log n) ^ (1/3 : ℝ)) := by
…

    Mentions: c, Erdos1004.IsDistinctTotientRun