Skip to content

Erdős problem 633

Start work

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

Open selected source

FormalConjectures/ErdosProblems/

633.lean

Retained formal statement8 of 8

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

FormalConjectures/ErdosProblems/633.leanErdos633.IsSimiliCuttable.of_ne_zero_two_three_five2 linesExact file
∀ {n : ℕ} {T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))},  n ≠ 0 → n ≠ 2 → n ≠ 3 → n ≠ 5 → Erdos633.IsSimiliCuttable n T
SolvedStatement only, no proof