How helpful is non-standard analysis? So, I can understand how non-standard analysis is better than standard analysis in that some proofs become simplified, and infinitesimals are somehow more intuitive to grasp than epsilon-delta arguments (both these points are debatable).
However, although many theorems have been proven by non-standard analysis and transferred via the transfer principle, as far as I know all of these results were already known to be true.  So, my question is:
Is there an example of a result that was first proved using non-standard analysis?  To wit, is non-standard analysis actually useful for proving new theorems?
Edit: Due to overwhelming support of François' comment, I've changed the title of the question accordingly.
 A: In mathematical economics, one often faces the following problem: One wants to formalize the idea of a large, relatively anonymous group of people (an atomless measure space of agents) that all face some risk that is iid of these people. Since there are lots of people, this risk should cancel out in the aggregate by some law of large numbers. The expost empirical distribution should be the ex ante distribution of the risk. If one uses something like the unit interval endowed with Lebesgue measure, this does not work. Most sample realizations are not measurable in that case.
Yeneng Sun has shown that there are exact laws of large numbers with a continuum of random variables for certain types of measure spaces. The only known examples were obtained using the Loeb measure construction that relies heavily on NSA. Later, Konrad Podczeck has shown how to construct appropriate measure spaces using conventional methods.
A: I think the only known solution to the local version of the Hilbert's fifth problem heavily uses nonstandard analysis. To be more precise the result is: every locally euclidean local group is locally isomorphic to a Lie group. You can find details in Isaac Goldbring's paper Hilbert's Fifth Problem for Local Groups.
A: Gromov was writing in one of his books (among other things) about some new mathematics coming from nonstandard analysis. Another example is proving that some statistical field theories (and lattice QFTs) are well-defined by Sergio Albeverio et al. (look at their book about that kind of applications to physics). Kiesler has been emphasising that some functional spaces are much richer in nonstandard analysis and that this power is one of the main arguments for the theory. Analysts say that one should look for applications where one has several degrees of infinitesimals or asymptotics, to somewhat reduce fitting complicated estimates to satisfy all.
There are some other approaches to infinitesimals which are not nonstandard analysis (no general transfer principle), but are similar in spirit, namely the synthetic differential geometry.
A: I just came across a 2013 book by F. Herzberg entitled "Stochastic Calculus with Infinitesimals" where probability and stochastic analysis are done without having to develop the complexities of measure and integration theory first.  Ever since E. Nelson, such an approach is called "radically elementary" and it really is.  What this proves is the new result that stochastic calculus can be done without measure theory.
To give a historical parallel, recall that Leibniz's mentor in mathematics was Huygens.  When Huygens first learned of Leibniz's invention of infinitesimal calculus, Huygens was sceptical, and wrote to Leibniz that he is merely doing what Fermat and others have done before him in a different language.  What Huygens failed to recognize immediately (but did recognize later) was the generality of the methods and the lucidity of the presentation of Leibniz's new approach.  The Nelson–Herzberg approach to stochastic calculus is in a way more significant than merely a new "result", since it provides a new methodology.
A: The other answers are excellent, but let me add a few
points.
First, with a historical perspective, all the early
fundamental theorems of calculus were first proved via
methods using infinitesimals, rather than by methods using
epsilon-delta arguments, since those methods did not appear
until the nineteenth century. Calculus proceeded for
centuries on the infinitesimal foundation, and the early
arguments---whatever their level of rigor---are closer to
their modern analogues in nonstandard analysis than to
their modern analogues in epsilon-delta methods. In this
sense, one could reasonably answer your question by
pointing to any of these early fundamental theorems.
To be sure, the epsilon-delta methods arose in part because
mathematicians became unsure of the foundational validity
of infinitesimals. But since nonstandard analysis exactly
provides the missing legitimacy, the original motivation
for adopting epsilon-delta arguments appears to fall away.
Second, while it is true that almost any application of
nonstandard analysis in analysis can be carried out using
standard methods, the converse is also true. That is,
epsilon-delta arguments can often also be translated into
nonstandard analysis. Furthermore, someone raised with
nonstandard analysis in their mathematical childhood would
likely prefer things this way. In this sense, the
preference between the two methods may be a cultural matter
of upbringing.
For example, H. Jerome Keisler wrote an introductory calculus
textbook called Elementary Calculus: an infinitesimal
approach, and
this text was used for many years as the main calculus
textbook at the University of Wisconsin, Madison. I
encourage you to take a look at this interesting text,
which looks at first like an ordinary calculus textbook,
except that in the inside cover, next to the various
formulas for derivatives and integrals, there are also
listed the various rules for manipulating infinitesimals,
which fill the text. Kiesler writes:


This is a calculus textbook at the college Freshman
level based on Abraham Robinson's infinitesimals, which
date from 1960. Robinson's modern infinitesimal approach
puts the intuitive ideas of the founders of the calculus
on a mathematically sound footing, and is easier for
beginners to understand than the more common approach via
limits.


Finally, third, some may take your question to presume that
a central purpose of nonstandard analysis is to provide
applications in analysis. But this is not correct. The
concept of nonstandard models of arithmetic, of analysis
and of set theory arose in mathematical logic and has grown
into an entire field, with hundreds of articles and many
books, with its own problems and questions and methods,
quite divorced from any application of the methods in other
parts of mathematics. For example, the subject of Models
of
Arithmetic
is focused on understanding the nonstandard models of the
first order Peano Axioms, and it makes little sense to
analyze these models using only standard methods.
To mention just a few fascinating classical theorems: every
countable nonstandard model of arithmetic is isomorphic to
a proper initial segment of itself (H. Friedman). Under the
Continuum Hypothesis, every Scott set (a family of sets of
natural numbers closed under Boolean operations, Turing
reducibility and satisfying Konig's lemma) is the
collection of definable sets of natural numbers of some
nonstandard model of arithmetic (D. Scott and others).
There is no nonstandard model of arithmetic for which
either addition or multiplication is computable (S.
Tennenbaum). Nonstandard models of arithmetic were also
used to prove several fascinating independence results over
PA, such as the results on
Goodstein sequences,
as well as the
Paris-Harrington theorem on the
independence over PA of a strong Ramsey theorem. Another
interesting
result
shows that various forms of the pigeon hole principle are
not equivalent over weak base theories; for example, the
weak pigeon-hole principle that there is no bijection of n
to 2n is not provable over the base theory from the weaker
principle that there is no bijection of n with
n2. These proofs all make fundamental use of
nonstandard methods, which it would seem difficult or
impossible to omit or to translate to standard methods.
A: Here is one paper with some results I have only seen being done in non-standard analysis so far, perhaps it is helpful to you:
A mathematical proof of the existence of trends in financial time series by Michel Fliess & Cédric Join
From the abstract: "We are settling a longstanding quarrel in quantitative finance by proving the existence of trends in financial time series thanks to a theorem due to P. Cartier and Y. Perrin, which is expressed in the language of nonstandard analysis […]. Those trends, which might coexist with some altered random walk paradigm and efficient market hypothesis, seem nevertheless difficult to reconcile with the celebrated Black–Scholes model. They are estimated via recent techniques stemming from control and signal theory. Several quite convincing computer simulations on the forecast of various financial quantities are depicted. We conclude by discussing the role of probability theory."
See also Rigorous definition, detection and test for trending vs. mean-reverting behaviour of stochastic processes and its answers.
A: In 1986 C. Ward Henson and H. J. Keisler published “On the Strength of Nonstandard Analysis” (The Journal of Symbolic Logic, Vol. 51, No. 2 (Jun., 1986), pp. 377-386), which is a seminal contribution to the meta-mathematics of nonstandard analysis. Since their result bears directly on the issue in this thread which has been reopened after laying dormant for some time now, and since no reference to their work is referred to in the original thread, I am taking the liberty of quoting the introduction to Henson and Keisler’s important paper (which I believe is as current today as when it was published).

It is often asserted in the literature that any theorem which can be proved using nonstandard analysis can also be proved without it. The purpose of this paper is to show that this assertion is wrong, and in fact there are theorems which can be proved with nonstandard analysis but cannot be proved without it. There is currently a great deal of confusion among mathematicians because the above assertion can be interpreted in two different ways. First, there is the following correct statement: any theorem which can be proved using nonstandard analysis can be proved in Zermelo-Fraenkel set theory with choice, ZFC, and thus is acceptable by contemporary standards as a theorem in mathematics. Second, there is the erroneous conclusion drawn by skeptics: any theorem which can be proved using nonstandard analysis can be proved without it, and thus there is no need for nonstandard analysis. The reason for this confusion is that the set of principles which are accepted by current mathematics, namely ZFC, is much stronger than the set of principles which are actually used in mathematical practice. It has been observed (see [F] and [S]) that almost all results in classical mathematics use methods available in second order arithmetic with appropriate comprehension and choice axiom schemes. This suggests that mathematical practice usually takes place in a conservative extension of some system of second order arithmetic, and that it is difficult to use the higher levels of sets. In this paper we shall consider systems of nonstandard analysis consisting of second order nonstandard arithmetic with saturation principles (which are frequently used in practice in nonstandard arguments). We shall prove that nonstandard analysis (i.e. second order nonstandard arithmetic) with the $\omega_{1}$-saturation axiom scheme has the same strength as third order arithmetic. This shows that in principle there are theorems which can be proved with nonstandard analysis but cannot be proved by the usual standard methods. The problem of finding a specific and mathematically natural example of such a theorem remains open. However, there are several results, particularly in probability theory, whose only known proofs are nonstandard arguments which depend on saturation principles; see, for example, the monograph [Ke]. Experience suggests that it is easier to work with nonstandard objects at a lower level than with sets at a higher level. This underlies the success of nonstandard methods in discovering new results. To sum up, nonstandard analysis still takes place within ZFC, but in practice it uses a larger portion of full ZFC than is used in standard mathematical proofs.

[F] S. FEFERMAN. Theories of finite type related to mathematical practice, Handbook of mathematical logic (J. Barwise, editor), North-Holland, Amsterdam, .1977, pp. 913-971.
[Ke] H. J. KEISLER, An infinitesimal approach to stochastic analysis, Memoirs of the American Mathematical Society, No. 297 (1984).
[S] S. SIMPSON, Which set existence axioms are needed to prove the Cauchy/Peano theorem for ordinary differential equations? JSL, vol. 49 (1984), pp. 783-802.
It is perhaps worth adding that Keisler (making use of work of Avigad) subsequently published a sequel to his paper with Henson in which he introduces what might be regarded as a system of Reverse Mathematics for nonstandard analysis with the hope of being able to establish the strength of particular theorems proved using nonstandard analysis.  (See “The Strength of Nonstandard Analysis” by H.J. Keisler in The Strength of Nonstandard Analysis ed. By Imme van den Berg and Vitor Neves, Springer, 2007).
A: From the Wikipedia article:

the list of new applications in
mathematics is still very small. One
of these results is the theorem proven
by Abraham Robinson and Allen
Bernstein that every polynomially
compact linear operator on a Hilbert
space has an invariant subspace. Upon
reading a preprint of the
Bernstein-Robinson paper, Paul Halmos
reinterpreted their proof using
standard techniques. Both papers
appeared back-to-back in the same
issue of the Pacific Journal of
Mathematics. Some of the ideas used in
Halmos' proof reappeared many years
later in Halmos' own work on
quasi-triangular operators.

A: Nonstandard hulls of spaces are used all the time in Banach space theory, so much so that books devote sections to the construction of ultraproducts of Banach spaces (e.g. Absolutely summing operators by Diestel, Jarchow, and Tonge).  There are cases where NSA is used to prove the existence of an estimate, yet no one knows how directly to compute an estimate.  For example, the unconditional constant of any basis for the span of the first n unit basis vectors in the James' space of sequences of bounded quadratic variation must go to infinity, but the only known proof involves NSA.
A: I first understood what the Thurston-type-compactification of the space of properly strictly convex real projective structures on a closed surface was using non-standard methods. What had been murky and confusing was suddenly clear. I have struggled with the question of whether or not to use NSA in the written proof. It is so much easier to use NSA I think we will.
A: Steve Huntsman's claim attributed to wikipedia that "the list of new applications in mathematics is still very small" is patently false. In fact, I was unable to find such a claim there. To mention just the most famous results, there is the recent work by T. Tao et al, by I. Goldbring on the local version of Hilbert's 5, Albeverio (several applications in math physics), Arkeryd (see his piece Nonstandard analysis in the American Mathematical Monthly) in hydrodynamics, the works on "canards" in perturbation theory, Jin's work in additive number theory, as well as numerous applications in statistics and economics. Robinson's work also occasioned a critical re-evaluation of whig history dominated by a reductive epsilontist agenda.
A: Freiman conjectured a classification of finite sets $A$ of integers that have
$$\lvert A+A\rvert = 3\lvert A\rvert-3+b$$
for some $0\leq b \leq \lvert A\rvert/3-2$. Renling Jin recently resolved this in Freiman's $3k - 3 + b$ conjecture for almost bi-arithmetic progression using nonstandard analysis. He has quite a few other nice results that appeared first with nonstandard analysis; with regard to this, see also:

Renling Jin, Nonstandard methods for additive and combinatorial number theory, pp. 117–129 in: van den Berg, Imme (ed.); Neves, Vítor (ed.) The strength of nonstandard analysis. Based on the meeting on nonstandard mathematics, Aveiro, Portugal, July 2004, Springer 2007.

Therein, on page 130, Renling Jin announces his solution as follows:

Theorem 8.6.2 Suppose $f\colon\mathbb{N}\to\mathbb{N}$ is a function with $\lim_{k\to\infty}\frac{f(k)}{k}=0$. There exists a natural number $K$ such that for any finite set of integers $A$ with $\lvert A\rvert=k$, if $k>K$ and $\lvert A+A\rvert=3k-3+b$ for some $0\leq b\leq f(k)$, then $A$ is either a subset of an arithmetic progression of length at most $2k-1+2b$ or a subset of a bi-arithmetic progression of length at most $k+b$.

Here, a bi-arithmetic progression means any union of two arithmetic progressions $A$ and $B$, both of the same increment, and with the additional property that $A+A$, $A+B$, $B+B$ are pairwise disjoint.
Renling Jin's result is also cited (in what seems slightly stronger form: $\varepsilon k$ instead of $f(k) = o(k)$) as a theorem in Theorem 2.2 on page 65 of

Ram Krishna Pandey, On the lonely runner conjecture, Mathematica Bohemia, No. 1, 2010, pp. 63–68.

Neither the above preprint, nor the title mentioned in the conference proceedings seems to have published, but the relevant refereed publication seems to be

Renling Jin, Freiman's inverse problem with small doubling property, Advances in Mathematics 216 (2007) 711–752

wherein Theorem 1.4 is the slightly stronger version (replace $\exists f\in o(k)$ with $\exists \varepsilon > 0$ and $\varepsilon k$ instead of $f(k)$) of the above Theorem 8.6.2.
A: The asymptotic cone of a metric space (and hence of a finitely generated group endowed with the word metric) is constructed using non-standard analysis, and has been used to prove many nice theorems.  To take just one example, asymptotic cones are an important tool in the proof that mapping class groups are quasi-isometrically rigid (Jason Behrstock. Bruce Kleiner. Yair Minsky. Lee Mosher. "Geometry and rigidity of mapping class groups." Geom. Topol. 16 (2) 781 - 888, 2012.
projecteuclid, DOI: 10.2140/gt.2012.16.781).
A: This reminded me of a talk by Mircea Mustata in which he mentioned that non-standard analysis type arguments were used to prove some things related to algebraic geometry. I can't remember what the talk was about, but I found the paper that it was based on:
de Fernex and Mustata - Limits of log canonical thresholds.
The paper mentions that later Kollár found proofs avoiding these techniques (but they are similar in spirit).
A: Let $k$ be an algebraically closed field of characteristic $0$. Let $T_n$ be the set of all possible log canonical threshold of a pair $(X,Y)$ where $X/k$ is a smooth variety and $Y \subseteq X$ is a nonzero closed subschemes. The following two facts are first proved (Tommaso de Fernex, Mircea Mustata, Limits of log canonical thresholds) via non-standard methods:

*

*$T_n$ is closed in $\mathbb R$ for all $n$.


*The set of points of accumulations from above of $T_n$ is $T_{n-1}$.
I think proofs that avoid non-standard analysis emerged later (J. Kollár, Which powers of holomorphic functions are integrable?), but the first one used non-standard technique.
A: Edward Nelson was working on a book on NSA mentioned here:
https://web.math.princeton.edu/~nelson/books.html
His existing book "Radically elementary probability theory" (linked from that page) uses some NSA.  I've been wanting to read it but don't understand much of it.
