Erdős problem 633
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].
Sources
FormalConjectures/ErdosProblems/
633.lean
Retained formal statement
Every triangle is simili-cuttable into any number of similar triangles, except 0, 2, 3, 5. This is proved in [So09].
∀ {n : ℕ} {T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))}, n ≠ 0 → n ≠ 2 → n ≠ 3 → n ≠ 5 → Erdos633.IsSimiliCuttable n TSolvedStatement only, no proof