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

References:

Let f_2(n) be the maximum number of pairs of points at distance exactly 1 among any set of n points in ℝ², under the condition that all pairwise distances are at least 1.

Estimate the growth of f_2(n).

Status: open.

Imports (1)
  1. def Erdos1084.f The maximal number of pairs of points which are distance 1 apart that a set of n 1-separated points in ℝ^d make line 46 source

    Source documentation

    The maximal number of pairs of points which are distance 1 apart that a set of n 1-separated points in ℝ^d make.

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

    Statement uses: Nat

    Proof uses: iSup, Finset, EuclideanSpace, Real, Fin, Eq, Finset.card, Metric.IsSeparated', OfNat.ofNat, ENNReal, unitDistNum

    17 instances, coercions and auxiliary constants left out.

    noncomputable def f (d n : ℕ) : ℕ :=
…
  2. theorem Erdos1084.erdos_1084.variants.upper_d1 It is easy to check that $f_1(n) = n - 1$ sorry line 53 source

    Source documentation

    It is easy to check that $f_1(n) = n - 1$.

    depends on sorry what this means

    Statement uses: Nat, Eq, Erdos1084.f, OfNat.ofNat, HSub.hSub

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

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_1084.variants.upper_d1 : f 1 n = n - 1 := by
…

    Mentions: Erdos1084.f

  3. theorem Erdos1084.erdos_1084.variants.easy_upper_d2 It is easy to check that $f_2(n) < 3n$ sorry line 58 source

    Source documentation

    It is easy to check that $f_2(n) < 3n$.

    depends on sorry what this means

    Statement uses: Nat, Ne, OfNat.ofNat, LT.lt, Erdos1084.f, HMul.hMul

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

    8 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_1084.variants.easy_upper_d2 (hn : n ≠ 0) : f 2 n < 3 * n := by
…

    Mentions: Erdos1084.f

  4. theorem Erdos1084.erdos_1084.variants.upper_d2 Erdős showed that there is some constant $c > 0$ such that $f_2(n) < 3n - c n^{1/2}$ sorry line 63 source

    Source documentation

    Erdős showed that there is some constant $c > 0$ such that $f_2(n) < 3n - c n^{1/2}$.

    depends on sorry what this means

    Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Nat, LT.lt, Erdos1084.f, HSub.hSub, HMul.hMul, Real.sqrt

    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_1084.variants.upper_d2 : ∃ c > (0 : ℝ), ∀ n > 0, f 2 n < 3 * n - c * sqrt n := by
…

    Mentions: c, Erdos1084.f

  5. theorem Erdos1084.erdos_1084.variants.triangular_optimal_d2 Erdős conjectured that the triangular lattice is best possible in 2D, in particular that $f_2(3n^2 + 3n + 1) = 9n^2 + 3n$ sorry line 73 source

    Source documentation

    Erdős conjectured that the triangular lattice is best possible in 2D, in particular that $f_2(3n^2 + 3n + 1) = 9n^2 + 3n$. Harborth [Ha74b] proved this, and more generally $f_2(n) = \lfloor 3n - \sqrt{12n - 3} \rfloor$ for all $n \geq 2$.

    Note: in [Er75f] is read $9n^2 + 6n$, but this seems to be a typo.

    depends on sorry what this means

    Statement uses: Nat, Eq, Erdos1084.f, OfNat.ofNat, HAdd.hAdd, HMul.hMul, HPow.hPow

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

    18 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_1084.variants.triangular_optimal_d2 : f 2 (3 * n ^ 2 + 3 * n + 1) = 9 * n ^ 2 + 3 * n := by
…

    Mentions: Erdos1084.f

  6. theorem Erdos1084.erdos_1084.variants.upper_lower_d3 Erdős claims the existence of two constants $c_1, c_2 > 0$ such that $6n - c_1 n^{2/3} ≤ f_3(n) \le 6n - c_2 n^{2/3}$ sorry line 79 source

    Source documentation

    Erdős claims the existence of two constants $c_1, c_2 > 0$ such that $6n - c_1 n^{2/3} ≤ f_3(n) \le 6n - c_2 n^{2/3}$.

    depends on sorry what this means

    Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, LE.le, HSub.hSub, HMul.hMul, HPow.hPow, HDiv.hDiv, Erdos1084.f, 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_1084.variants.upper_lower_d3 :
    ∃ c₁ : ℝ, ∃ c₂ > (0 : ℝ), ∀ᶠ n in atTop,
      6 * n - c₁ * n ^ (2 / 3 : ℝ) ≤ f 3 n ∧ f 3 n ≤ 6 * n - c₂ * n ^ (2 / 3 : ℝ) := by
…

    Mentions: Erdos1084.f