Fleuriot, Jacques

Kokciyan, Nadin

Morris, Imogen I.

Engineering and Physical Sciences Research Council (EPSRC)

2023-10-24T11:56:03Z

2023-10-24T11:56:03Z

2023-10-24

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 this thesis we 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'. We use our proof to demonstrate that Euler was systematic in his use of infinitely-large and infinitely-small numbers and did not make unjustified leaps of intuition. The concept of 'hidden lemmas' was developed by McKinzie and Tuckey based on Lakatos and Laugwitz to represent general principles which Euler's proof followed. We develop a theory of infinite 'hyperpolynomials' in Isabelle in order to formalise these hidden lemmas and we find that formal reconstruction of his proof using hidden lemmas is an effective way to discover the nuances in Euler's reasoning and demystify the controversial points. In conclusion, we find that Euler's reasoning was consistent and insightful, and yet has some distinct methodology to modern deductive proof.

https://hdl.handle.net/1842/41096

http://dx.doi.org/10.7488/era/3835

en

The University of Edinburgh

Euler

nonstandard analysis

theorem proving

Isabelle/HOL

18th century

formal proof

Mechanising Euler's use of infinitesimals in the proof of the Basel problem

Thesis or Dissertation

Doctoral

PhD Doctor of Philosophy