Is there a first order statement about the natural numbers (not nonstandard analysis) such that the truth of the statement is easier to see in a nonstandard model? In other words, do nonstandard models offer "more" mathematical insight in some way about the standard model? Compare this with the use of the compactness theorem to prove certain facts about infinite objects which follows in a straightforward manner from that about finite objects; whereas a direct "mathematical" argument tends to be more tedious (eg. 4 colorability of an infinite planar graph).



nonstandard models and mathematical theorems
I view nonstandard models (particularly those produced by ultraproducts) as a convenient way to take limits of discrete structures to obtain continuous structures that capture all of the asymptotic first-order properties of the discrete structure. This of course can also be done by the compactness theorem, but ultraproducts also offer good saturation properties, which tends to make the continuous structure "complete" or "locally compact" in various senses. This allows one to usefully deploy various tools from continuous mathematics (e.g. measure theory, ergodic theory, topological group theory) in a manner which would be inconvenient to do back in the discrete setting, or even in a continuous model that was constructed purely through a compactness argument. I give some examples of this at <https://terrytao.wordpress.com/2013/12/07/ultraproducts-as-a-bridge-between-discrete-and-continuous-analysis/> . Some more sophisticated examples include the [proof of the inverse conjecture for the Gowers norms](http://www.ams.org/mathscinet-getitem?mr=2950773), or [the inverse theorem for approximate groups](http://www.ams.org/mathscinet-getitem?mr=3090256); at present the only known proofs of these results proceed via nonstandard methods (though I am sure that if one really wanted to, one could unpack the nonstandard arguments and obtain a fully standard, but very messy, proof of these results).


Model theorists have become quite good at exploiting additional properties of (suitably constructed) nonstandard models, such as the existence of a very large group of automorphisms, which (when combined with sufficiently strong saturation properties) then leads to the ability to describe "generic" elements, "indiscernible" sequences of elements, representatives of various "types", and similar useful gadgets. I'm not so familiar with this aspect of nonstandard methods though.


