Is there a version of Lie theory using infinitesimals? Is there a version of Lie theory using nonstandard analysis in which «infinitesimal elements» (i.e. the Lie algebra, tangent space) are actually infinitesimal (in the sense of the hyperreal number system) or the standard part of some expression using infinitesimals?
I know that Sophus Lie apparently thought of Lie algebras as "infinitesimal elements" of Lie groups and then had to work a lot to make his theory rigorous. So I was wondering if there is or would be any heuristic payoff to using Robinson's rigorous formulation of infinitesimals to understand Lie theory, since conceptually it would seem to more closely mirror Lie's own ideas/inspirations.
 A: As the answer I accepted noted, the answer is "yes" if we are flexible about what type of infinitesimals we use. If we want to stick to Robinson's infinitesimals (non-standard analysis, as opposed to the smooth infinitesimal analysis used in synthetic differential geometry), the answer appears to be largely "no". There is very little work which has been done in this area, at least as far as I could tell while doing a Google search. The best results I found:


*

*"Differential Geometry via Infinitesimal Displacements" by Tahl Nowik and Mikhail G. Katz. This does apparently cover Lie brackets along with other aspects of smooth manifolds. (1)Published version (2)Pre-print.

*"On some applications of non-standard analysis in geometry" by Angela Pasarescu (I couldn't render the Romanian symbols correctly) see here.

*Mentioned here on p.95 of a book about nonstandard analysis which I have not been able to get access to ("Nonstandard Analysis and its Applications" - edited  by Nigel Cutland, in the first section, "An Invitation to Nonstandard Analysis" by Tom Lindstrom) is an article published by Stroyan back in 1977 "Infinitesimal Analysis of Curves and Surfaces" which apparently explains how ideas from non-standard analysis can be transferred into differential geometry -- in Handbook of Mathematical Logic (K.J. Barwise, ed.) North-Holland, Amsterdam, pp. 197-231. Unfortunately North-Holland is owned by Elsevier. The mention is in the notes corresponding to Lindstrom's section II.3 about Brownian motion, interestingly enough.

A: In the synthetic differential geometry you have infinitesimals. Example of applications to Lie groups and algebras: 
From Lie Algebras to Lie Groups within Synthetic Differential Geometry: Weil Sprouts of Lie's Third Fundamental Theorem.
The "problem" with SDG: intuitionistic logic is required.
A: To part of your question, the answer is yes. In Remark 1 of this post, Terry Tao sort of indicates how you would formalize a Lie algebra nonstandardly. However, in my opinion there is little "heuristic payoff" here, in comparison to some other methods from nonstandard analysis. 
There are also some other connections between nonstandard analysis and Lie theory besides the classical intuition you suggest. See for instance, the PhD thesis of Isaac Goldbring, accessible here.
