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

Erdős Problem 100

References:

Imports (1)
  1. def Erdos100.DistancesSeparated If two distances in A differ, they differ by at least 1 line 37 source

    Source documentation

    If two distances in A differ, they differ by at least 1.

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

    Statement uses: Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat

    Proof uses: Membership.mem, Ne, Dist.dist, ENNReal, GE.ge, abs, HSub.hSub

    20 instances, coercions and auxiliary constants left out.

    def DistancesSeparated (A : Finset ℝ²) : Prop :=
…
  2. theorem Erdos100.erdos_100 Is the diameter of $A$ at least $Cn$ for some constant $C > 0$? sorry line 44 source

    Source documentation

    Is the diameter of $A$ at least $Cn$ for some constant $C > 0$?

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, Finset, EuclideanSpace, Fin, Eq, Finset.card, Erdos100.DistancesSeparated, Metric.diam, ENNReal, HMul.hMul, 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_100 :
    answer(sorry) ↔ ∃ C > (0 : ℝ), ∀ᶠ n in atTop, ∀ A : Finset ℝ²,
      A.card = n →
      DistancesSeparated A →
      diam (A : Set ℝ²) > C * n := by
…

    Mentions: Erdos100.DistancesSeparated

  3. theorem Erdos100.erdos_100.variants.strong Stronger conjecture: diameter $\geq n - 1$ for sufficiently large $n$ sorry line 53 source

    Source documentation

    Stronger conjecture: diameter $\geq n - 1$ for sufficiently large $n$.

    depends on sorry what this means

    Statement uses: Filter.Eventually, Nat, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Eq, Finset.card, Erdos100.DistancesSeparated, GE.ge, Metric.diam, ENNReal, HSub.hSub, 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_100.variants.strong :
    ∀ᶠ n in atTop, ∀ A : Finset ℝ²,
      A.card = n →
      DistancesSeparated A →
      diam (A : Set ℝ²) ≥ n - 1 := by
…

    Mentions: Erdos100.DistancesSeparated

  4. theorem Erdos100.erdos_100.variants.kanold From [Kanold]: diameter $\geq n^{3/4}$ sorry line 63 source

    Source documentation

    From [Kanold]: diameter $\geq n^{3/4}$. TODO: find reference

    depends on sorry what this means

    Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, Finset, EuclideanSpace, Fin, Eq, Finset.card, Erdos100.DistancesSeparated, GE.ge, Metric.diam, ENNReal, HPow.hPow, HDiv.hDiv, Filter.atTop

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

    52 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_100.variants.kanold :
    ∃ C > (0 : ℝ), ∀ᶠ n in atTop, ∀ A : Finset ℝ²,
      A.card = n →
      DistancesSeparated A →
      diam (A : Set ℝ²) ≥ (n : ℝ) ^ (3 / 4 : ℝ) := by
…

    Mentions: Erdos100.DistancesSeparated

  5. theorem Erdos100.erdos_100.variants.guth_katz From [GuKa15]: diameter $\gg n / \log n$ sorry line 72 source

    Source documentation

    From [GuKa15]: diameter $\gg n / \log n$.

    depends on sorry what this means

    Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, Finset, EuclideanSpace, Fin, Eq, Finset.card, Erdos100.DistancesSeparated, GE.ge, Metric.diam, ENNReal, HDiv.hDiv, HMul.hMul, Real.log, Filter.atTop

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

    48 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_100.variants.guth_katz :
    ∃ C > (0 : ℝ), ∀ᶠ n in atTop, ∀ A : Finset ℝ²,
      A.card = n →
      DistancesSeparated A →
      diam (A : Set ℝ²) ≥ C * n / log n := by
…

    Mentions: Erdos100.DistancesSeparated

  6. theorem Erdos100.erdos_100_piepmeyer From [Piepmeyer]: 9 points with diameter $< 5$ sorry line 82 source

    Source documentation

    From [Piepmeyer]: 9 points with diameter $< 5$. TODO: find reference

    depends on sorry what this means

    Statement uses: Exists, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, And, Eq, Finset.card, Erdos100.DistancesSeparated, LT.lt, Metric.diam, ENNReal

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

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_100_piepmeyer :
    ∃ A : Finset ℝ², A.card = 9 ∧ DistancesSeparated A ∧
      diam (A : Set ℝ²) < 5 := by
…

    Mentions: Erdos100.DistancesSeparated