skip to content

Proof Archeology: Historical Mathematics from an Interactive Theorem Proving Standpoint

Presented by: 
Jacques Fleuriot University of Edinburgh
Friday 14th July 2017 - 11:30 to 12:30
INI Seminar Room 1
The active study of historical mathematics is often viewed as being of peripheral interest to the working mathematician. The original work is instead recast within modern notation and standards of rigour, with the new formulation becoming the authoritative approach, while the analysis of the source text is left to historians. Although this is not inherently bad, since mathematical descriptions and ideas can become obsolete, one may argue that in the case of mathematical expositions that have shaped the field there is still much to be gained by going back to original sources.

In this talk, we argue that interactive theorem proving can be an effective tool for the systematic analysis of such historical mathematics. It not only provides a rigorous means of investigating the original texts but can also act as a framework for formally reconstructing the proofs in ways that often respect the original reasoning, while eliciting steps and lemmas that can shine new light on the results. Synergistically, such reconstructions also often push the boundaries of formalized mathematics, resulting in new libraries and in the improvement, or even reformulation, of existing ones.

We support our claims by examining proofs from Euler’s Introductio in Analysin Infinitorum (the "Introductio") published in 1748. In this, using what he calls “ordinary algebra”, he (algorithmically) derives the series for the exponential and trigonometric functions, and proves Euler’s Formula among many other classic results. We describe how Euler’s deft algebraic manipulations of infinitesimals and infinite numbers can be formally restored in the Isabelle theorem prover and argue that Euler was not as heedless as some have claimed.

Related Links
The video for this talk should appear here if JavaScript is enabled.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons