Computerising Euler’s Foundations of Differential Calculus using Nonstandard Analysis

Date: 29th January 2021
Time: 14:00-16:00
Location: online
Talks

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.