Title: Exploring Euler’s Differentials of Exponential Functions in Isabelle using Nonstandard Analysis
Speaker: Richard Stansfield
Abstract:

Many of the proofs of important results in analysis from Euler’s Foundations of Differential Calculus have been called into question due to their lack of rigour and reliance on the existence of infinitely small numbers, which standard mathematics now rejects. However, using nonstandard analysis formalised in Isabelle we may now be able to rigorously rehabilitate them and in doing so uncover the implicit reasoning behind some of the legendary mathematician’s results.

In particular, my project will focus on a handful of proofs regarding differentials of functions involving exponentiation. I will talk about the background to the project – hopefully giving an intuitive impression of nonstandard analysis for the unfamiliar – as well as discussing some of the difficulties that arise when converting Euler to Isabelle.