FormalConjectures.ErdosProblems.«633»

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import FormalConjecturesUtil

Erdős Problem 633

Reference:

erdosproblems.com/633

[So09] Soifer, Alexander, How Does One Cut a Triangle? I

[So09c] Soifer, Alexander, Is there anything beyond the solution?

[BLZ26] Beeson, Michael, Laczkovich, Miklós, and Zhang, Yan, Solution of Erdős problem 633.

@[expose] public sectionopen Affineopen scoped Congruent EuclideanGeometry Similarnamespace Erdos633variable {n : ℕ} {T : Triangle ℝ ℝ²}variable (n T) in

A triangle is n-cuttable if it can be decomposed into n congruent triangles.

def IsCuttable : Prop :=
  ∃ Ts : Fin n → Triangle ℝ ℝ²,
    (∀ i j, (Ts i).points ≅ (Ts j).points) ∧
      Pairwise (fun i j ↦ Disjoint (Ts i).interior (Ts j).interior) ∧
      ⋃ i, (Ts i).closedInterior = T.closedInterior

A triangle isn't cuttable into zero triangles.

@[category API, AMS 5 51]
lemma IsCuttable.ne_zero (hT : IsCuttable n T) : n ≠ 0 := byn:ℕT:Triangle ℝ ℝ²hT:IsCuttable n T⊢ n ≠ 0
  rintro rflT:Triangle ℝ ℝ²hT:IsCuttable 0 T⊢ False
  obtain ⟨Ts, -, -, hT⟩ := hTT:Triangle ℝ ℝ²Ts:Fin 0 → Triangle ℝ ℝ²hT:⋃ i, Simplex.closedInterior (Ts i) = Simplex.closedInterior T⊢ False
  exact T.closedInterior_nonempty.ne_empty <| byT:Triangle ℝ ℝ²Ts:Fin 0 → Triangle ℝ ℝ²hT:⋃ i, Simplex.closedInterior (Ts i) = Simplex.closedInterior T⊢ Simplex.closedInterior T = ∅ simpa using hT.symmAll goals completed! 🐙

Every triangle is cuttable into any non-zero square number of congruent triangles.

@[category API, AMS 5 51]
protected lemma IsCuttable.sq (hn : n ≠ 0) : IsCuttable (n ^ 2) T := sorry

Every triangle is cuttable into any non-zero square number of congruent triangles.


@[category API, AMS 5 51]
lemma IsCuttable.of_isSquare (hn₀ : n ≠ 0) (hn : IsSquare n) : IsCuttable n T := byn:ℕT:Triangle ℝ ℝ²hn₀:n ≠ 0hn:IsSquare n⊢ IsCuttable n T
  obtain ⟨n, rfl⟩ := hnT:Triangle ℝ ℝ²n:ℕhn₀:n * n ≠ 0⊢ IsCuttable (n * n) T; rw [← sqT:Triangle ℝ ℝ²n:ℕhn₀:n * n ≠ 0⊢ IsCuttable (n ^ 2) TT:Triangle ℝ ℝ²n:ℕhn₀:n * n ≠ 0⊢ IsCuttable (n ^ 2) T]T:Triangle ℝ ℝ²n:ℕhn₀:n * n ≠ 0⊢ IsCuttable (n ^ 2) T; exact .sq <| byT:Triangle ℝ ℝ²n:ℕhn₀:n * n ≠ 0⊢ n ≠ 0 simpa using hn₀All goals completed! 🐙

A triangle whose side lengths and angles are integrally independent is cuttable only into a non-zero square number of congruent triangles. This is proved in [So09c].

@[category research solved, AMS 5 51]
lemma isCuttable_iff_isSquare_of_linearIndependent
    (hTsides : LinearIndependent ℤ
      ![dist (T.points 0) (T.points 1),
        dist (T.points 1) (T.points 2),
        dist (T.points 2) (T.points 0)])
    (hTangles : LinearIndependent ℤ
      ![∠ (T.points 0) (T.points 1) (T.points 2),
        ∠ (T.points 1) (T.points 2) (T.points 0),
        ∠ (T.points 2) (T.points 0) (T.points 1)]) :
    IsCuttable n T ↔ n ≠ 0 ∧ IsSquare n := byn:ℕT:Triangle ℝ ℝ²hTsides:LinearIndependent ℤ ![dist (T.points 0) (T.points 1), dist (T.points 1) (T.points 2), dist (T.points 2) (T.points 0)]hTangles:LinearIndependent ℤ
  ![∠ (T.points 0) (T.points 1) (T.points 2), ∠ (T.points 1) (T.points 2) (T.points 0),
    ∠ (T.points 2) (T.points 0) (T.points 1)]⊢ IsCuttable n T ↔ n ≠ 0 ∧ IsSquare n
  exact ⟨fun hT ↦ ⟨hT.ne_zero, sorry⟩, fun hn ↦ .of_isSquare hn.1 hn.2⟩All goals completed! 🐙

-- The complete classification is too involved to encode as the answer set here.
set_option linter.style.category_answer false in

Which triangles can only be decomposed into a square number of congruent triangles?

Beeson, Laczkovich, and Zhang [BLZ26] classify the triangles that can be tiled only into a square number of congruent triangles, settling this problem. The classification is too involved to encode in the answer slot here, so the answer is left as sorry and the reference records the result.

@[category research solved, AMS 5 51]
lemma erdos_633 : T ∈ (answer(sorry) : Set <| Triangle ℝ ℝ²) ↔
    ∀ n, IsCuttable n T → IsSquare n := sorry

variable (n T) in

A triangle is n-simili-cuttable if it can be decomposed into n similar triangles.

def IsSimiliCuttable (n : ℕ) (T : Triangle ℝ ℝ²) : Prop :=
  ∃ Ts : Fin n → Triangle ℝ ℝ²,
    (∀ i j, (Ts i).points ∼ (Ts j).points) ∧
      Pairwise (fun i j ↦ Disjoint (Ts i).interior (Ts j).interior) ∧
      ⋃ i, (Ts i).closedInterior = T.closedInterior

A triangle isn't simili-cuttable into zero triangles.

@[category API, AMS 5 51]
lemma IsSimiliCuttable.ne_zero (hT : IsSimiliCuttable n T) : n ≠ 0 := byn:ℕT:Triangle ℝ ℝ²hT:IsSimiliCuttable n T⊢ n ≠ 0
  rintro rflT:Triangle ℝ ℝ²hT:IsSimiliCuttable 0 T⊢ False
  obtain ⟨Ts, -, -, hT⟩ := hTT:Triangle ℝ ℝ²Ts:Fin 0 → Triangle ℝ ℝ²hT:⋃ i, Simplex.closedInterior (Ts i) = Simplex.closedInterior T⊢ False
  exact T.closedInterior_nonempty.ne_empty <| byT:Triangle ℝ ℝ²Ts:Fin 0 → Triangle ℝ ℝ²hT:⋃ i, Simplex.closedInterior (Ts i) = Simplex.closedInterior T⊢ Simplex.closedInterior T = ∅ simpa using hT.symmAll goals completed! 🐙

Every triangle is simili-cuttable into any number of similar triangles, except 0, 2, 3, 5. This is proved in [So09].

@[category research solved, AMS 5 51]
lemma IsSimiliCuttable.of_ne_zero_two_three_five (hn₀ : n ≠ 0) (hn₂ : n ≠ 2) (hn₃ : n ≠ 3)
    (hn₅ : n ≠ 5) : IsSimiliCuttable n T := sorry

There exists a triangle which isn't simili-cuttable into 0, 2, 3, 5 parts. This is proved in [So09].

@[category research solved, AMS 5 51]
lemma exists_isSimiliCuttable_iff_ne_zero_two_three_five :
    ∃ T, ∀ n, IsSimiliCuttable n T ↔ n ≠ 0 ∧ n ≠ 2 ∧ n ≠ 3 ∧ n ≠ 5 := sorry

end Erdos633