Title: Exploring Euler’s Differentials of Trigonometric Functions in Isabelle using Nonstandard Analysis
Speaker: Alice Johansen
Abstract: In 1755, Euler published ‘Foundations of Differential Calculus’ which presented and defined theories of differential calculus. While influential, Euler’s text has been criticized by many for lacking rigour, particularily when it comes to his treatment of infinitesimal numbers. For my project, I’ve attempted to formulate Euler’s reasoning in a rigourous setting, using Isabelle with nonstandard analysis. Isabelle with nonstandard analysis has been a powerful tool for this project, where my goal is to understand how Euler’s proofs must be adapted and elaborated upon in order to maintain rigour and consistency. My project focuses on Euler’s proofs of the differentials of trigonometric functions, which require consideration when replicated in Isabelle due to their domains and relationships.