Title: Towards a mechanisation of Euler’s Infinite Analysis in the Proof Assistant Isabelle
Speaker: Imogen Morris
Abstract: 

In 1736 Euler published a proof of an astounding relation between π and the reciprocals of the squares.

π ² ⁄ 6 = 1+ 1⁄4 + 1/9 + 1/25 + …

Until this point, π had not been part of any mathematical relation outside of geometry. This relation would have had an almost supernatural significance to the mathematicians of the time. But even more amazing is Euler’s proof. He factorises a transcendental function as if it were a polynomial of infinite degree. He discards infinitely-many infinitely-small numbers. He substitutes 1 for the ratio of two distinct infinite numbers.

Nowadays Euler’s proof is held up as an example of both genius intuition and flagrantly unrigorous method. In my talk I will describe how, with the aid of nonstandard analysis, which gives a consistent formal theory of infinitely-small and large numbers, and the proof assistant Isabelle, we are in the process of constructing a formal proof of the Basel problem which uses the method of Euler’s original proof. We argue that Euler was consistent in his use of infinitely-large and infinitely-small numbers, and aim to show that his original reasoning provides the structure of a formal proof. We use the concept of “hidden lemmas”, developed by McKinzie and Tuckey based on Lakatos and  Laugwitz, to formalise general principles which Euler’s proof followed. Towards this end, we have developed a theory of infinite “hyperpolynomials”, formal proofs of a version of convergence of the infinite polynomials used by Euler, formalisation of the factorisation and expansion of Euler’s infinite polynomial and formal proofs of many steps in Euler’s proof.

This talk is part of my 3rd year review and will describe my work done so far, as well as the planned work, which together will become my PhD thesis.