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

The source's own material, retained exactly.

8 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

633.lean

Retained formal statement1 of 8

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

FormalConjectures/ErdosProblems/633.leanErdos633.erdos_6331 lineExact file

1∀ {T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))}, T ∈ sorry ↔ ∀ (n : ℕ), Erdos633.IsCuttable n T → IsSquare n

OpenStatement only, no proof