BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Proof Archeology: Historical Mathematics from an Interactive Theor
 em Proving Standpoint - Jacques Fleuriot (University of Edinburgh)
DTSTART:20170714T103000Z
DTEND:20170714T113000Z
UID:TALK73278@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:The active study of historical mathematics is often viewed as 
 being of peripheral interest to the working mathematician. The original wo
 rk is instead recast within modern notation and standards of rigour\, with
  the new formulation becoming the authoritative approach\, while the analy
 sis of the source text is left to historians. Although this is not inheren
 tly bad\, since mathematical descriptions and ideas can become obsolete\, 
 one may argue that in the case of mathematical expositions that have shape
 d the field there is still much to be gained by going back to original sou
 rces. <br><br>In this talk\, we argue that interactive theorem proving can
  be an effective tool for the systematic analysis of such historical mathe
 matics. It not only provides a rigorous means of investigating the origina
 l texts but can also act as a framework for formally reconstructing the pr
 oofs in ways that often respect the original reasoning\, while eliciting s
 teps and lemmas that can shine new light on the results. Synergistically\,
  such reconstructions also often push the boundaries of formalized mathema
 tics\, resulting in new libraries and in the improvement\, or even reformu
 lation\, of existing ones.  <br><br>We support our claims by examining pro
 ofs from Euler&rsquo\;s Introductio in Analysin Infinitorum (the "Introduc
 tio") published in 1748. In this\, using what he calls &ldquo\;ordinary al
 gebra&rdquo\;\, he (algorithmically) derives the series for the exponentia
 l and trigonometric functions\, and proves Euler&rsquo\;s Formula among ma
 ny other classic results. We describe how Euler&rsquo\;s deft algebraic ma
 nipulations of infinitesimals and infinite numbers can be formally restore
 d in the Isabelle theorem prover and argue that Euler was not as heedless 
 as some have claimed. <br><br>Related Links<ul><li><a target="_blank" rel=
 "nofollow" href="http://www-old.newton.ac.uk/cgi/http%3A%2F%2Fhomepages.in
 f.ed.ac.uk%2Fjdf">http://homepages.inf.ed.ac.uk/jdf</a> - Speaker&#39\;s h
 omepage</li></ul>
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR