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

4 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 189

Reference: erdosproblems.com/189

Imports (1)
  1. def Erdos189.Erdos189For Erdős problem 189 asked whether the below holds for all rectangles line 33 source

    Source documentation

    Erdős problem 189 asked whether the below holds for all rectangles.

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

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

    Proof uses: GT.gt, Exists, And, LE.le, Set, Insert.insert, Singleton.singleton, Set.preimage, EuclideanGeometry.IsCcwConvexPolygon, Nat.succ, ENNReal, Matrix.vecCons, Matrix.vecEmpty, Eq

    32 instances, coercions and auxiliary constants left out.

    def Erdos189For (P : ℝ² → ℝ² → ℝ² → ℝ² → Prop) (A : ℝ² → ℝ² → ℝ² → ℝ² → ℝ) :=
…
  2. theorem Erdos189.erdos_189 If $\mathbb{R}^2$ is finitely coloured then must there exist some colour class which contains the vertices of a rectangle of every area? sorry line 56 source

    Source documentation

    If $\mathbb{R}^2$ is finitely coloured then must there exist some colour class which contains the vertices of a rectangle of every area?

    Graham, "On Partitions of 𝔼ⁿ", Journal of Combinatorial Theory, Series A 28, 89-91 (1980). (See "Concluding Remarks" on page 96.)

    Solved (with answer False, as formalised below) in: Vjekoslav Kovač, "Coloring and density theorems for configurations of a given volume", 2023 https://arxiv.org/abs/2309.09973 In fact, Kovač's colouring is even Jordan measurable (the topological boundary of each monochromatic region is Lebesgue measurable and has measure zero).

    This was formalized in Lean by Alexeev and Kovac using Aristotle.

    depends on sorry what this means

    Statement uses: Iff, False, Erdos189.Erdos189For, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, And, Submodule.IsOrtho, ENNReal, AffineSubspace.direction, affineSpan, Insert.insert, Set, Singleton.singleton, HMul.hMul, Dist.dist

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

    76 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_189 :
    answer(False) ↔ Erdos189For
      (fun a b c d ↦
        line[ℝ, a, b].direction ⟂ line[ℝ, b, c].direction ∧
        line[ℝ, b, c].direction ⟂ line[ℝ, c, d].direction ∧
        line[ℝ, c, d].direction ⟂ line[ℝ, d, a].direction)
      (fun a b c d ↦ dist a b * dist b c) := by
…

    Mentions: Erdos189.Erdos189For, c

  3. theorem Erdos189.erdos_189.variants.square Graham claims this is "easy to see" sorry line 67 source

    Source documentation

    Graham claims this is "easy to see".

    depends on sorry what this means

    Statement uses: Not, Erdos189.Erdos189For, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, And, Submodule.IsOrtho, ENNReal, AffineSubspace.direction, affineSpan, Insert.insert, Set, Singleton.singleton, Eq, Dist.dist, HMul.hMul

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

    76 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_189.variants.square :
    ¬ Erdos189For
      (fun a b c d ↦
        line[ℝ, a, b].direction ⟂ line[ℝ, b, c].direction ∧
        line[ℝ, b, c].direction ⟂ line[ℝ, c, d].direction ∧
        line[ℝ, c, d].direction ⟂ line[ℝ, d, a].direction ∧
        dist a b = dist b c)
      (fun a b c d ↦ dist a b * dist b c) := by
…

    Mentions: Erdos189.Erdos189For, c

  4. theorem Erdos189.erdos_189.variants.parallelogram Seems to be open, as of January 2025 sorry line 81 source

    Source documentation

    Seems to be open, as of January 2025.

    depends on sorry what this means

    Statement uses: Not, Erdos189.Erdos189For, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, And, AffineSubspace.Parallel, ENNReal, affineSpan, Insert.insert, Set, Singleton.singleton, HMul.hMul, Dist.dist, Real.Angle.sin, EuclideanGeometry.oangle

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

    84 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_189.variants.parallelogram :
    ¬ Erdos189For
      (fun a b c d ↦
        line[ℝ, a, b] ∥ line[ℝ, c, d] ∧
        line[ℝ, a, d] ∥ line[ℝ, b, c])
      (fun a b c d ↦ dist a b * dist b c * (∡ a b c).sin) := by
…

    Mentions: Erdos189.Erdos189For, c