Proof Archeology: Historical Mathematics from an Interactive Theorem Proving Standpoint

Add to your list(s) Download to your calendar using vCal

• Jacques Fleuriot (University of Edinburgh)
• Friday 14 July 2017, 11:30-12:30
• Seminar Room 1, Newton Institute.

If you have a question about this talk, please contact INI IT.

BPRW01 - Computer-aided mathematical proof

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

• http://homepages.inf.ed.ac.uk/jdf – Speaker's homepage

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.