Email Gateway (Jun 10 2026 at 16:00): Email Gateway (Jun 10 2026 at 16:00):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce a very rare contribution involving non-standard analysis. It's great to see NSA applied to justify “unsound" historical mathematics.
Euler's Exponential Series as an Infinite Polynomial
Jacques D. Fleuriot
In this formalisation, we reconstruct Euler's derivation of the power series for the exponential function as expounded in his famous Introductio in analysin infinitorum, first published in 1748. Using nonstandard analysis, we mechanize his mixture of infinitesimal and infinite `algebraic' reasoning in the proof assistant Isabelle. In so doing, we demonstrate that the gist of his arguments can be reconstructed formally, with Isabelle and nonstandard analysis shoring up crucial aspects of his reasoning that some historians have qualified as being ``more a matter of faith than science''.
https://isa-afp.org/entries/Euler_Exponential.html
Last updated: Jun 12 2026 at 04:13 UTC