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

Erdős Problem 1082

Reference: erdosproblems.com/1082

Imports (1)
  1. theorem Erdos1082.erdos_1082.parts.i Let $A\subset \mathbb{R}^2$ be a set of $n$ points with no three on a line sorry line 37 source

    Source documentation

    Let $A\subset \mathbb{R}^2$ be a set of $n$ points with no three on a line. Does $A$ determine at least $\lfloor n/2\rfloor$ distinct distances?

    depends on sorry what this means

    Statement uses: Iff, True, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, EuclideanGeometry.NonTrilinear, ENNReal, LE.le, HDiv.hDiv, Finset.card, distinctDistances

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

    54 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_1082.parts.i : answer(sorry) ↔ ∀ (A : Finset ℝ²) (hA_n3c : NonTrilinear (A : Set ℝ²)),
    A.card / 2 ≤ distinctDistances A:= by
…

    Mentions: distinctDistances

  2. theorem Erdos1082.erdos_1082.parts.ii Let $A\subset \mathbb{R}^2$ be a set of $n$ points with no three on a line sorry line 56 source

    Source documentation

    Let $A\subset \mathbb{R}^2$ be a set of $n$ points with no three on a line. Must there exist a single point from which there are at least $\lfloor n/2\rfloor$ distinct distances?

    This question has been answered negatively by Xichuan in the comments, who gave a set of $42$ points in $\mathbb{R}^2$, with no three on a line, such that each point determines only $20$ distinct distances.

    A smaller counterexample has been formalised here: it comprised of $8$ points, where each point only determines $3$ distances.

    This counterexample has originally been found by Heiko Harborth.

    L4DEL explanation

    Let $A\subset \mathbb{R}^2$ be a set of $n$ points with no three on a line. Must there exist a single point from which there are at least $\lfloor n/2\rfloor$ distinct distances? This question has been answered negatively by Xichuan in the comments, who gave a set of $42$ points in $\mathbb{R}^2$, with no three on a line, such that each point determines only $20$ distinct distances. A smaller counterexample has been formalised here: it comprised of $8$ points, where each point only determines $3$ distances. This counterexample has originally been found by Heiko Harborth.

    Sources and attribution: Pinned Lean source (1646ca16afd6)

    depends on sorry what this means

    Statement uses: Iff, False, Finset, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Finset.Nonempty, EuclideanGeometry.NonTrilinear, ENNReal, Exists, Membership.mem, LE.le, HDiv.hDiv, Finset.card, distinctDistancesFrom

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

    56 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_1082.parts.ii : answer(False) ↔
    ∀ (A : Finset ℝ²) (hA : A.Nonempty) (hA_n3c : NonTrilinear (A : Set ℝ²)),
    ∃ (a : ℝ²) (ha : a ∈ A), A.card / 2 ≤ distinctDistancesFrom A a := by
…

    Mentions: distinctDistancesFrom