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

6 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 888

References:

Imports (1)
Imported by 1 file
  1. def Erdos888.RequiredCondition Condition on the sets $A$ appearing in Erdős 888 line 39 source

    Source documentation

    Condition on the sets $A$ appearing in Erdős 888. Namely, let $A$ be a subset of ${1,...,n}$ such that if $a ≤ b ≤ c ≤ d ∈ A$ and $abcd$ square then $ad=bc$.

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

    Statement uses: Finset, Nat

    Proof uses: And, LE.le, Finset.Ioc, OfNat.ofNat, Membership.mem, IsSquare, HMul.hMul, Eq

    11 instances, coercions and auxiliary constants left out.

    def RequiredCondition (A : Finset ℕ) (n : ℕ) : Prop :=
…
  2. def Erdos888.p Proposition that for a specific $n$ an $A$ with the above defined condition and cardinality $k$ exists line 47 source

    Source documentation

    Proposition that for a specific $n$ an $A$ with the above defined condition and cardinality $k$ exists.

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

    Statement uses: Nat

    Proof uses: Exists, Finset, And, Erdos888.RequiredCondition, Eq, Finset.card

    def p (n : ℕ) (k : ℕ) : Prop := ∃ A : Finset ℕ, RequiredCondition A n ∧ A.card = k
…

    Mentions: Erdos888.RequiredCondition

  3. theorem Erdos888.erdos_888 sorry line 58 source

    depends on sorry what this means

    Statement uses: Asymptotics.IsTheta, Nat, Real, Filter.atTop, Nat.findGreatest, Erdos888.p, Classical.propDecidable, HDiv.hDiv, HMul.hMul, Real.log

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

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  4. theorem Erdos888.erdos_888.variants.sarkozy Erdős claims that Sárközy proved that $\lvert A\rvert =o(n)$ (a proof of this bound is provided by Tao in the comments) sorry line 69 source

    Source documentation

    Erdős claims that Sárközy proved that $\lvert A\rvert =o(n)$ (a proof of this bound is provided by Tao in the comments).

    depends on sorry what this means

    Statement uses: Asymptotics.IsLittleO, Nat, Real, Filter.atTop, Nat.findGreatest, Erdos888.p, Classical.propDecidable

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

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_888.variants.sarkozy :
    (fun n ↦ (Nat.findGreatest (p n) n : ℝ)) =o[atTop] (Nat.cast : ℕ → ℝ) := by
…

    Mentions: Erdos888.p

  5. theorem Erdos888.erdos_888.variants.primes The primes show that $\lvert A\rvert \gg n/\log n$ is possible sorry line 78 source

    Source documentation

    The primes show that $\lvert A\rvert \gg n/\log n$ is possible.

    depends on sorry what this means

    Statement uses: Asymptotics.IsBigO, Nat, Real, Filter.atTop, HDiv.hDiv, Real.log, Nat.findGreatest, Erdos888.p, Classical.propDecidable

    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_888.variants.primes :
    (fun n : ℕ ↦ (Nat.findGreatest (p n) n : ℝ)) ≫ (fun n : ℕ ↦ (n : ℝ) / Real.log n) := by
…

    Mentions: Erdos888.p

  6. theorem Erdos888.erdos_888.variants.semiprimes Cambie and Weisenberg have noted in the comments that the set of semiprimes also works, showing $(1+o(1))\frac{\log\log n}{\log n}n \leq \lvert A\rvert$ is achievable sorry line 88 source

    Source documentation

    Cambie and Weisenberg have noted in the comments that the set of semiprimes also works, showing $(1+o(1))\frac{\log\log n}{\log n}n \leq \lvert A\rvert$ is achievable.

    depends on sorry what this means

    Statement uses: Exists, Nat, Real, And, Asymptotics.IsLittleO, Filter.atTop, OfNat.ofNat, Filter.Eventually, LE.le, HMul.hMul, HAdd.hAdd, HDiv.hDiv, Real.log, Nat.findGreatest, Erdos888.p, Classical.propDecidable

    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_888.variants.semiprimes :
    ∃ c : ℕ → ℝ, c =o[atTop] (1 : ℕ → ℝ) ∧ ∀ᶠ n : ℕ in atTop,
      (1 + c n) * ((n : ℝ) * Real.log (Real.log n) / Real.log n) ≤ Nat.findGreatest (p n) n := by
…

    Mentions: c, Erdos888.p