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

Erdős Problem 137

References:

Imports (1)
Imported by 1 file
  1. theorem Erdos137.erdos_137 We say that $N$ is powerful if whenever $p\mid N$ we also have $p^2\mid N$ sorry line 37 source

    Source documentation

    We say that $N$ is powerful if whenever $p\mid N$ we also have $p^2\mid N$.

    Let $k\geq 3$. Can the product of any $k$ consecutive positive integers ever be powerful?

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Nat, And, GE.ge, OfNat.ofNat, Nat.Powerful, Finset.prod, Finset.Ioc, 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_137 : answer(sorry) ↔ ∃ k ≥ 3, ∃ n, (∏ x ∈ Finset.Ioc n (n + k), x).Powerful := by
…
  2. theorem Erdos137.erdos_137.variants.perfect_power Let $k\geq 2$ sorry line 48 source

    Source documentation

    Let $k\geq 2$. Erdős and Selfridge [ES75] proved that the product of any $k$ consecutive integers $N$ cannot be a perfect power.

    [ES75] P. Erdös, J. L. Selfridge, "The product of consecutive integers is never a power", Illinois J. Math. 19(2): 292-301, 1975

    depends on sorry what this means

    Statement uses: Nat, GE.ge, OfNat.ofNat, LE.le, Ne, Finset.prod, Finset.Ioc, HAdd.hAdd, HPow.hPow

    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_137.variants.perfect_power (k : ℕ) (hk : k ≥ 2) (n : ℕ) (x l : ℕ) (hl : 2 ≤ l) :
    (∏ x ∈ Finset.Ioc n (n + k), x) ≠ x ^ l := by
…
  3. theorem Erdos137.erdos_137.variants.multiple_powerful_factors Documented declaration: multiple_powerful_factors sorry line 60 source

    Source documentation

    Erdős [Er82c] conjectures that, if $k$ is fixed, then for all $n$ sufficiently large and all positive integers $m$, there must be at least $k$ distinct primes $p$ such that $p\mid m(m+1)\cdots (m+n)$ and yet $p^2$ does not divide the right hand side.

    [Er82c] Erdős, Paul, "Miscellaneous problems in number theory". Congr. Numer. (1982), 25-45.,

    depends on sorry what this means

    Statement uses: Nat, Filter.Eventually, LT.lt, OfNat.ofNat, Exists, Finset, And, Eq, Finset.card, Membership.mem, Nat.Prime, Dvd.dvd, Finset.prod, Finset.Ioc, HAdd.hAdd, Not, HPow.hPow, Filter.atTop

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

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_137.variants.multiple_powerful_factors (k : ℕ) : ∀ᶠ n in Filter.atTop,
    ∀ (m : ℕ) (hm : 0 < m),
    letI N := ∏ x ∈ Finset.Ioc m (m + n), x
…