Title: Nonstandard analysis for Euler’s proof of the Basel Problem
Speaker: Imogen Morris
Abstract: I will describe the background theory of nonstandard analysis which I am using to formalise the proof of the Basel problem from Euler’s `Introduction to the Analysis of the Infinite’. 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 will explain some of the properties of these numbers and how they can be constructed. I will also explain hyperfinite sums and internal functions, which are both necessary to for my theory of ‘infinite polynomials’. I will describe some of the relevant theorems which I have formalised in the proof assistant Isabelle.