Let $n \geq 3$ be a natural number and $PA$ denote Peano arithmetic. Do we have
$PA \models \forall x,y,z \geq 1 : x^n + y^n \neq z^n$?
In other words, does Fermat's Last Theorem hold also in non-standard models of the natural numbers?
If this problem is open, what is its current state of progress?