Title: Mechanising Euler’s Infinite Analysis in the Proof Assistant Isabelle
Speaker: Imogen Morris
Abstract:

I will describe my work this year on formalising Euler’s proof of the Basel problem . The proof which I have partially formalised is from Euler’s textbook `Introduction to the Analysis of the Infinite’, in which he aims to show that the manipulation of infinitely small and infinitely large quantities can be accomplished using `ordinary algebra’. Euler’s arguments using infinity and his theory of infinitesimals are not considered rigorous by present-day mathematicians. However, there is a modern theory of infinities and infinitesimals called nonstandard analysis, which captures many of the properties that 18th century mathematicians ascribed to infinite and infinitesimal numbers. I use this theory and the proof assistant Isabelle, as the framework to mechanise Euler’s proof. My project aims to demonstrate that Euler’s reasoning can be made consistent and that Euler appreciated the subtleties of infinitesimals. In my talk, I will also outline my plans for further research which include other arguments from Euler’s textbook e.g. the infinite product for sine in terms of its roots and generalisations of the Basel problem.