The mystery of Euler's disappearing numbers and how Isabelle helped me solve it
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/16 …
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 this talk I 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 construct a partial formal proof of the Basel problem which follows the method of Euler's proof from his 'Introductio in Analysin Infinitorum'. Our proof utilises the concept of 'hidden lemmas' which was developed by McKinzie and Tuckey based on Lakatos and Laugwitz to represent general principles which Euler followed. We develop a theory of infinite 'hyperpolynomials' in Isabelle in order to formalise these hidden lemmas. Formal reconstruction of Euler's proof demystifies his reasoning and reveals mistakes in previous descriptions of his proof. We use our formalisation to demonstrate that Euler was systematic in his use of infinitely-small and large numbers, did not make unjustified leaps of intuition, and yet used distinct methodology to modern deductive proof.
About the speaker: Imogen Morris studied mathematics at the University of Edinburgh and continued there for her PhD research supervised by Jacques Fleuriot which this talk is based on. She now holds a postdoctoral position at the University of Edinburgh working on compound axiomatic memory models with Vijay Nagarajan, Tobias Grosser and Andrés Goens. Her research interests include nonstandard analysis, philosophy and history of mathematics, formalisation of mathematics in proof assistants and formal methods.
