633.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

10 declarations, 5 contain sorry, 0 declared as axioms

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.

Imports (1)

FormalConjecturesUtil

def Erdos633.IsCuttable A triangle is n-cuttable if it can be decomposed into n congruent triangles line 41 source
Source documentation
A triangle is n-cuttable if it can be decomposed into n congruent triangles.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Affine.Triangle, Real, EuclideanSpace, Fin, OfNat.ofNat, ENNReal
Proof uses: Exists, And, Congruent, HAdd.hAdd, Affine.Simplex.points, Pairwise, Disjoint, Set, Affine.Simplex.interior, Eq, Set.iUnion, Affine.Simplex.closedInterior
65 instances, coercions and auxiliary constants left out.
```
def IsCuttable : Prop :=
…
```
lemma Erdos633.IsCuttable.ne_zero A triangle isn't cuttable into zero triangles line 49 source
Source documentation
A triangle isn't cuttable into zero triangles.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Affine.Triangle, Real, EuclideanSpace, Fin, OfNat.ofNat, ENNReal, Erdos633.IsCuttable, Ne
Proof uses: Eq, False, And, Congruent, HAdd.hAdd, Affine.Simplex.points, Pairwise, Disjoint, Set, Affine.Simplex.interior, Set.iUnion, Affine.Simplex.closedInterior, Set.Nonempty.ne_empty, Affine.Simplex.closedInterior_nonempty, Eq.mp, EmptyCollection.emptyCollection, congrArg, Set.iUnion_of_empty, Eq.symm
71 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma IsCuttable.ne_zero (hT : IsCuttable n T) : n ≠ 0 := by
…
```
Mentions: Erdos633.IsCuttable
lemma Erdos633.IsCuttable.sq Every triangle is cuttable into any non-zero square number of congruent triangles sorry line 56 source
Source documentation
Every triangle is cuttable into any non-zero square number of congruent triangles.

depends on sorry what this means
Statement uses: Nat, Affine.Triangle, Real, EuclideanSpace, Fin, OfNat.ofNat, ENNReal, Ne, Erdos633.IsCuttable, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
60 instances, coercions and auxiliary constants left out.
```
protected lemma IsCuttable.sq (hn : n ≠ 0) : IsCuttable (n ^ 2) T := sorry
…
```
Mentions: Erdos633.IsCuttable
lemma Erdos633.IsCuttable.of_isSquare Every triangle is cuttable into any non-zero square number of congruent triangles line 60 source
Source documentation
Every triangle is cuttable into any non-zero square number of congruent triangles.

depends on sorry what this means
Statement uses: Nat, Affine.Triangle, Real, EuclideanSpace, Fin, OfNat.ofNat, ENNReal, Ne, IsSquare, Erdos633.IsCuttable
Proof uses: Eq, HMul.hMul, Eq.mpr, HPow.hPow, id, congrArg, Eq.symm, sq, Erdos633.IsCuttable.sq, Eq.mp, Not, Eq.trans, Or, or_self
78 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma IsCuttable.of_isSquare (hn₀ : n ≠ 0) (hn : IsSquare n) : IsCuttable n T := by
…
```
Mentions: Erdos633.IsCuttable
lemma Erdos633.isCuttable_iff_isSquare_of_linearIndependent A triangle whose side lengths and angles are integrally independent is cuttable only into a non-zero square number of congruent triangles sorry line 66 source
Source documentation
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].

depends on sorry what this means
Statement uses: Nat, Affine.Triangle, Real, EuclideanSpace, Fin, OfNat.ofNat, ENNReal, LinearIndependent, Nat.succ, Int, Matrix.vecCons, Dist.dist, Affine.Simplex.points, HAdd.hAdd, Matrix.vecEmpty, EuclideanGeometry.angle, Iff, Erdos633.IsCuttable, And, Ne and 1 more
Proof uses: Iff.intro, And.intro, Erdos633.IsCuttable.ne_zero, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Erdos633.IsCuttable.of_isSquare, And.left, And.right
90 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
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 := by
…
```
Mentions: Erdos633.IsCuttable
lemma Erdos633.erdos_633 Which triangles can only be decomposed into a square number of congruent triangles? sorry line 88 source
Source documentation
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.

depends on sorry what this means
Statement uses: Affine.Triangle, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Iff, Membership.mem, Set, sorryAx, Bool.false, Erdos633.IsCuttable, IsSquare
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
56 instances, coercions and auxiliary constants left out.
```
lemma erdos_633 : T ∈ (answer(sorry) : Set <| Triangle ℝ ℝ²) ↔
    ∀ n, IsCuttable n T → IsSquare n := sorry
…
```
Mentions: Erdos633.IsCuttable
def Erdos633.IsSimiliCuttable A triangle is n-simili-cuttable if it can be decomposed into n similar triangles line 93 source
Source documentation
A triangle is n-simili-cuttable if it can be decomposed into n similar triangles.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Affine.Triangle, Real, EuclideanSpace, Fin, OfNat.ofNat, ENNReal
Proof uses: Exists, And, Similar, HAdd.hAdd, Affine.Simplex.points, Pairwise, Disjoint, Set, Affine.Simplex.interior, Eq, Set.iUnion, Affine.Simplex.closedInterior
65 instances, coercions and auxiliary constants left out.
```
def IsSimiliCuttable (n : ℕ) (T : Triangle ℝ ℝ²) : Prop :=
…
```
lemma Erdos633.IsSimiliCuttable.ne_zero A triangle isn't simili-cuttable into zero triangles line 101 source
Source documentation
A triangle isn't simili-cuttable into zero triangles.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Affine.Triangle, Real, EuclideanSpace, Fin, OfNat.ofNat, ENNReal, Erdos633.IsSimiliCuttable, Ne
Proof uses: Eq, False, And, Similar, HAdd.hAdd, Affine.Simplex.points, Pairwise, Disjoint, Set, Affine.Simplex.interior, Set.iUnion, Affine.Simplex.closedInterior, Set.Nonempty.ne_empty, Affine.Simplex.closedInterior_nonempty, Eq.mp, EmptyCollection.emptyCollection, congrArg, Set.iUnion_of_empty, Eq.symm
71 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma IsSimiliCuttable.ne_zero (hT : IsSimiliCuttable n T) : n ≠ 0 := by
…
```
Mentions: Erdos633.IsSimiliCuttable
lemma Erdos633.IsSimiliCuttable.of_ne_zero_two_three_five Every triangle is simili-cuttable into any number of similar triangles, except 0, 2, 3, 5 sorry line 109 source
Source documentation
Every triangle is simili-cuttable into any number of similar triangles, except 0, 2, 3, 5. This is proved in [So09].

depends on sorry what this means
Statement uses: Nat, Affine.Triangle, Real, EuclideanSpace, Fin, OfNat.ofNat, ENNReal, Ne, Erdos633.IsSimiliCuttable
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
52 instances, coercions and auxiliary constants left out.
```
lemma IsSimiliCuttable.of_ne_zero_two_three_five (hn₀ : n ≠ 0) (hn₂ : n ≠ 2) (hn₃ : n ≠ 3)
    (hn₅ : n ≠ 5) : IsSimiliCuttable n T := sorry
…
```
Mentions: Erdos633.IsSimiliCuttable
lemma Erdos633.exists_isSimiliCuttable_iff_ne_zero_two_three_five There exists a triangle which isn't simili-cuttable into 0, 2, 3, 5 parts sorry line 115 source
Source documentation
There exists a triangle which isn't simili-cuttable into 0, 2, 3, 5 parts. This is proved in [So09].

depends on sorry what this means
Statement uses: Exists, Affine.Triangle, Real, EuclideanSpace, Fin, OfNat.ofNat, Nat, ENNReal, Iff, Erdos633.IsSimiliCuttable, And, Ne
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
52 instances, coercions and auxiliary constants left out.
```
lemma exists_isSimiliCuttable_iff_ne_zero_two_three_five :
    ∃ T, ∀ n, IsSimiliCuttable n T ↔ n ≠ 0 ∧ n ≠ 2 ∧ n ≠ 3 ∧ n ≠ 5 := sorry
…
```
Mentions: Erdos633.IsSimiliCuttable