Title: Computerising Euler’s Foundations of Differential Calculus using Nonstandard Analysis
Speaker: Richard Stansfield
Abstract: I will discuss my progress using nonstandard analysis in Isabelle to rigorously formalise of a handful of Euler’s proofs from his Foundations of Differential Calculus. I will walk through an example of this process, highlighting the challenges that Euler’s reasoning and Isabelle present and where I am in my project.