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

2 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 648

References:

Imports (1)
  1. def Erdos648.g g n is the largest t such that there exist integers 2 ≤ a 0 < a 1 < ⋯ < a (t - 1) < n whose greatest prime factors are strictly decreasing line 48 source

    Source documentation

    g n is the largest t such that there exist integers 2 ≤ a 0 < a 1 < ⋯ < a (t - 1) < n whose greatest prime factors are strictly decreasing.

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

    Statement uses: Nat

    Proof uses: SupSet.sSup, Set.ofPred, Exists, Fin, And, StrictMono, Membership.mem, Set, Set.Ico, OfNat.ofNat, StrictAnti, Nat.maxPrimeFac

    6 instances, coercions and auxiliary constants left out.

    noncomputable def g (n : ℕ) : ℕ :=
…
  2. theorem Erdos648.erdos_648 Let $g(n)$ denote the largest $t$ such that there exist integers $2\leq a_1P(a_2)>\cdots >P(a_t)$$ where $P(m)$ is the greatest prime factor of $m$ sorry line 67 source

    Source documentation

    Let $g(n)$ denote the largest $t$ such that there exist integers $2\leq a_1<a_2<\cdots <a_t <n$ such that $$P(a_1)>P(a_2)>\cdots >P(a_t)$$ where $P(m)$ is the greatest prime factor of $m$. Estimate $g(n)$.

    Stijn Cambie has proved [Ca25b] $$g(n) \asymp \left(\frac{n}{\log n}\right)^{1/2}.$$ Cambie further asks whether there exists a constant $c$ such that $$g(n) \sim c \left(\frac{n}{\log n}\right)^{1/2}.$$ Cambie's proof shows that such a $c$ must satisfy $2\leq c\leq 2\sqrt{2}$.

    The sequence $a_1<a_2<\cdots<a_t$ is packaged as a strictly monotone map a : Fin t → ℕ with $2\leq a_i<n$, the greatest prime factor $P$ is Nat.maxPrimeFac, and $g(n)$ is the supremum in ℕ of the achievable lengths $t$.

    L4DEL explanation

    Let $g(n)$ denote the largest $t$ such that there exist integers $2\leq a_1P(a_2)>\cdots >P(a_t)$$ where $P(m)$ is the greatest prime factor of $m$. Estimate $g(n)$. Stijn Cambie has proved [Ca25b] $$g(n) \asymp \left(\frac{n}{\log n}\right)^{1/2}.$$ Cambie further asks whether there exists a constant $c$ such that $$g(n) \sim c \left(\frac{n}{\log n}\right)^{1/2}.$$ Cambie's proof shows that such a $c$ must satisfy $2\leq c\leq 2\sqrt{2}$. The sequence $a_1<a_2<\cdots<a_t$ is packaged as a strictly monotone map a : Fin t → ℕ with $2\leq a_i<n$, the greatest prime factor $P$ is Nat.maxPrimeFac, and $g(n)$ is the supremum in ℕ of the achievable lengths $t$.

    Sources and attribution: Pinned Lean source (1646ca16afd6)

    depends on sorry what this means

    Statement uses: Asymptotics.IsTheta, Nat, Real, Filter.atTop, Erdos648.g, Real.sqrt, HDiv.hDiv, Real.log

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

    15 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_648 :
    (fun n => (g n : ℝ)) =Θ[atTop] fun n => Real.sqrt ((n : ℝ) / Real.log (n : ℝ)) := by
…

    Mentions: Erdos648.g