Erdős Problem 558

### What is the conjecture

https://www.erdosproblems.com/558

Let $R(G;k)$ denote the minimal $m$ such that if the edges of $K_m$ are $k$-coloured then there is a monochromatic copy of $G$. Determine
$$R(K_{s,t};k)$$
where $K_{s,t}$ is the complete bipartite graph with $s$ vertices in one component and $t$ in the other.

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

Start with the conjecture statement and the repository's existing formalized-conjecture organization; this issue names no target file, test, or entry point. Confirm the expected Lean representation and repository checks before attempting the formalization, with the conjecture added in a form that passes those checks as the definition of done.

Written by the indexing model from the issue text.