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.