Erdős Problem 201

### What is the conjecture

https://www.erdosproblems.com/201

Let $G_k(N)$ be such that any set of $N$ integers contains a subset of size at least $G_k(N)$ which does not contain a $k$-term arithmetic progression. Determine the size of $G_k(N)$. How does it relate to $R_k(N)$, the size of the largest subset of $\\{1,\ldots,N\\}$ without a $k$-term arithmetic progression? Is it true that $$\lim_{N\to \infty}\frac{R_3(N)}{G_3(N)}=1?$$

Status: open

### Prerequisites needed
$k$-term arithmetic progressions are in `ForMathlib`

### 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 by reviewing the k-term arithmetic progression definitions in ForMathlib and nearby formalized conjectures. Formalize Erdős Problem 201, including the definitions of G_k(N) and R_k(N) and the stated limit question, then confirm that the resulting Lean declarations compile.

Written by the indexing model from the issue text.