Title: Exploring Euler’s Differentials of Trigonometric Functions in Isabelle using Nonstandard Analysis
Speaker: Alice Johansen
Abstract:

In 1755, Euler published his influential ‘Foundations of Differential Calculus’ which presented and defined theories of differential calculus and discussion of the infinite. While Euler makes missteps and often excludes assumptions in his proofs, one must remember that in context, eighteenth-century mathematicians did not have the same expectations of rigour that one might have today, and thus there is value in formulating Euler’s reasoning now with the diligence that his text lacked. Returning to our current time, interactive proof assistant Isabelle has helped verify countless theorems across mathematics and computer science domains, and I will use this powerful tool to explore and prove Euler’s differential definitions for trigonometric functions sin, cos and hopefully more via nonstandard analysis