Part 2 of 2

TheoremSquaring the square with distinct squares#●ready to prove

There are an integer \(n > 1\) and real numbers \(x_i\), \(y_i\) and \(s_i > 0\) for \(i = 1, \dots, n\), with the \(s_i\) pairwise distinct, such that the union of the closed squares \([x_i, x_i + s_i] \times [y_i, y_i + s_i]\) is the unit square \([0, 1] \times [0, 1]\) and any two of these squares with different indices have disjoint interiors.

theorem_wanted squaringTheSquareDistinctSquares :
    ∃ (n : ℕ) (x y s : Fin n → ℝ),
      (1 < n) ∧
      (∀ i, 0 < s i) ∧
      (∀ i j, i ≠ j → s i ≠ s j) ∧
      (⋃ i, Set.Icc (x i, y i) (x i + s i, y i + s i) =
        Set.Icc (0, 0) (1, 1)) ∧
      ∀ i j, i ≠ j →
        Disjoint
          (interior (Set.Icc (x i, y i) (x i + s i, y i + s i)))
          (interior (Set.Icc (x j, y j) (x j + s j, y j + s j)))

Sources

• S. Ruziewicz, Problem 59 of the Scottish Book, asking whether a square can be decomposed into a finite number of squares all different from one another; the answer is affirmative. The first published solution is R. Sprague's 1939 squaring of the square with distinct squares; see the commentary in R. D. Mauldin (ed.), The Scottish Book, 2nd ed. (Birkhäuser, 2015), and the 2026 survey "90+ years of the Scottish Book" (arXiv:2603.27867).

TheoremSylvester–Gallai theorem#✓fully proved

Every finite non-collinear subset of the real Euclidean plane determines an ordinary line: two points of the set such that no third point of the set is collinear with them.

theorem sylvester_gallai
    (s : Set (EuclideanSpace ℝ (Fin 2)))
    (hs_fin : s.Finite)
    (hs_noncollinear : ¬Collinear ℝ s) :
    ∃ a ∈ s, ∃ b ∈ s, a ≠ b ∧
      ∀ c ∈ s, Collinear ℝ ({a, b, c} : Set (EuclideanSpace ℝ (Fin 2))) → c = a ∨ c = b

Sources

• J. J. Sylvester, Mathematical Question 11851, Educational Times 59 (1893) 98; L. M. Kelly, A resolution of the Sylvester–Gallai problem, Discrete Comput. Geom. 1 (1986) 101–104 standard real-plane version.

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.