FormalConjectures/ErdosProblems/930.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, 3 contain sorry, 0 declared as axioms

Erdős Problem 930

Reference: erdosproblems.com/930

Imports (1)
  1. def Erdos930.IsPower $n$ is a perfect power if there exist natural numbers $m$ and $l$ such that $1 < l$ and $m^l = n$ line 36 source

    Source documentation

    $n$ is a perfect power if there exist natural numbers $m$ and $l$ such that $1 < l$ and $m^l = n$.

    standard axioms: propext what this means

    Statement uses: Nat

    Proof uses: Exists, And, LT.lt, OfNat.ofNat, Eq, HPow.hPow

    6 instances, coercions and auxiliary constants left out.

    def IsPower (n : ℕ) : Prop :=
…
  2. theorem Erdos930.erdos_930 Documented declaration: erdos_930 sorry line 49 source

    Source documentation

    Is it true that, for every $r$, there is a $k$ such that if $I_1,\ldots,I_r$ are disjoint intervals of consecutive integers, all of length at least $k$, then $$ \prod_{1\leq i\leq r}\prod_{m\in I_i}m $$ is not a perfect power?

    depends on sorry what this means

    Statement uses: Iff, True, Nat, GT.gt, OfNat.ofNat, Exists, Fin, And, LT.lt, LE.le, HAdd.hAdd, Not, Erdos930.IsPower, Finset.prod, Finset.univ, Finset.Icc

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

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_930 :
    answer(sorry) ↔ ∀ r > 0, ∃ k, ∀ I₁ I₂ : Fin r → ℕ,
      (∀ i : Fin r, 0 < I₁ i ∧ I₁ i + k ≤ I₂ i + 1) →
        (∀ i j : Fin r, i < j → I₂ i < I₁ j) →
          ¬ IsPower (∏ i : Fin r, ∏ m ∈ Icc (I₁ i) (I₂ i), m) := by
…

    Mentions: Erdos930.IsPower

  3. def Erdos930.nextPrime Returns the least prime satisfying $k \le p$ line 59 source

    Source documentation

    Returns the least prime satisfying $k \le p$

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

    Statement uses: Nat

    Proof uses: Nat.find, And, LE.le, Nat.Prime, Nat.exists_infinite_primes

    4 instances, coercions and auxiliary constants left out.

    def nextPrime (k : ℕ) : ℕ :=
…
  4. theorem Erdos930.erdos_930.variants.consecutive_strong Let $k$, $l$, $n$ be integers such that $k \ge 3$, $l \ge 2$ and $n + k \ge p^{(k)}$, where $p^{(k)}$ is the least prime satisfying $p^{(k)} \ge k$ sorry line 73 source

    Source documentation

    Let $k$, $l$, $n$ be integers such that $k \ge 3$, $l \ge 2$ and $n + k \ge p^{(k)}$, where $p^{(k)}$ is the least prime satisfying $p^{(k)} \ge k$. Then there is a prime $p \ge k$ for which $l$ does not divide the multiplicity of the prime factor $p$ in $(n + 1) \ldots (n + k)$.

    Theorem 2 from [ErSe75].

    [ErSe75] Erdős, P. and Selfridge, J. L., The product of consecutive integers is never a power. Illinois J. Math. (1975), 292-301.

    depends on sorry what this means

    Statement uses: Nat, LE.le, OfNat.ofNat, Erdos930.nextPrime, HAdd.hAdd, Exists, And, Nat.Prime, Not, Dvd.dvd, Finsupp, Nat.factorization, Finset.prod, Finset.Icc

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

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_930.variants.consecutive_strong :
    ∀ k l n, 3 ≤ k → 2 ≤ l → nextPrime k ≤ n + k →
      ∃ p, k ≤ p ∧ p.Prime ∧
        ¬ (l ∣ Nat.factorization (∏ m ∈ Icc (n + 1) (n + k), m) p) := by
…

    Mentions: Erdos930.nextPrime

  5. theorem Erdos930.erdos_930.variants.consecutive_integers Erdos and Selfridge [ErSe75] proved that the product of consecutive integers is never a power (establishing the case $r=1$) sorry line 90 source

    Source documentation

    Erdos and Selfridge [ErSe75] proved that the product of consecutive integers is never a power (establishing the case $r=1$).

    Theorem 1 from [ErSe75].

    It is implied from erdos_930.variants.consecutive_strong.

    [ErSe75] Erdős, P. and Selfridge, J. L., The product of consecutive integers is never a power. Illinois J. Math. (1975), 292-301.

    depends on sorry what this means

    Statement uses: Nat, LE.le, OfNat.ofNat, Not, Erdos930.IsPower, Finset.prod, Finset.Icc, HAdd.hAdd

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

    14 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_930.variants.consecutive_integers :
    ∀ n k, 0 ≤ n → 2 ≤ k →
      ¬ IsPower (∏ m ∈ Icc (n + 1) (n + k), m) := by
…

    Mentions: Erdos930.IsPower