# Complexity of finding large grid minors

What is the complexity of finding the largest $k\times k$ grid graph that is a minor of a given graph $G$? It is FPT in $k$, and it seems likely to be NP-hard (or NP-complete in a decision version asking whether there exists such a minor for given $k$) but I don't know of a published proof.

There are some papers on constant factor approximations to this problem, e.g.:

Is it hard to $(1+\epsilon)$-approximate, for some $\epsilon>0$?

If I understood well the problem, perhaps this is an idea for a reduction from the Hamiltonian path problem: given $G$ with $|V| = n$, a source and target node $s, t \in V$; you can extend it adding a $(n-1) \times n$ "full" grid graph having the bottom-left node of the last row connected to $s$ and the bottom right node of the last row connected to $t$.
Then connect each of the $n-2$ remaining nodes of the last row to each of the nodes in $|V| \setminus \{s,t\}$ adding $(n-2)^2$ edges.
The resulting graph $G'$ has a graph minor of size $n \times n$ if and only if there is an Hamiltonian path from $s$ to $t$ in the source graph $G$.
In the following picture a no instance (left) and a yes instance (right) with the corresponding $n \times n$ grid graph minor.