Proof Archeology: Historical Mathematics from an Interactive Theorem Proving Standpoint
Duration: 53 mins 1 sec
Share this media item:
Embed this media item:
Embed this media item:
About this item
| Description: |
Fleuriot, J
Friday 14th July 2017 - 11:30 to 12:30 |
|---|
| Created: | 2017-07-26 15:28 |
|---|---|
| Collection: | Big proof |
| Publisher: | Isaac Newton Institute |
| Copyright: | Fleuriot, J |
| Language: | eng (English) |
| Distribution: |
World
(downloadable)
|
| Explicit content: | No |
| Aspect Ratio: | 16:9 |
| Screencast: | No |
| Bumper: | UCS Default |
| Trailer: | UCS Default |
| Abstract: | 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 |
|---|---|
Available Formats
| Format | Quality | Bitrate | Size | |||
|---|---|---|---|---|---|---|
| MPEG-4 Video | 640x360 | 1.94 Mbits/sec | 771.93 MB | View | Download | |
| WebM | 640x360 | 586.53 kbits/sec | 227.75 MB | View | Download | |
| iPod Video | 480x270 | 521.77 kbits/sec | 202.61 MB | View | Download | |
| MP3 | 44100 Hz | 249.76 kbits/sec | 97.08 MB | Listen | Download | |
| Auto * | (Allows browser to choose a format it supports) | |||||