Erdős Problem 439

### What is the conjecture

https://www.erdosproblems.com/439

Is it true that, in any finite colouring of the integers, there must be two integers $x\neq y$ of the same colour such that $x+y$ is a square? What about a $k$ th power?

Status: solved

### 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

Start with the conjecture statement at erdosproblems.com/439 and inspect existing formalized Erdős problems in the repository; the issue names no target file or test. Done means adding a Lean formalization of the stated finite-colouring claim, with the k-th-power question handled according to the project’s conventions and repository checks passing.

Written by the indexing model from the issue text.