Erdős Problem 634

### What is the conjecture

https://www.erdosproblems.com/634

Find all $n$ such that there is at least one triangle which can be cut into $n$ congruent triangles.

Status: open

### Choose either option
- [ ] I plan on working on this conjecture
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Read the conjecture at https://www.erdosproblems.com/634, then inspect the repository's existing formalized Erdős problems for the expected Lean statement and structure. Done means adding a formalization of the triangle-partition conjecture to the collection and satisfying the project's checks.

Written by the indexing model from the issue text.