Title: L’Hopital’s Theorems and Euler’s Notions of Orders of Infinity in Isabelle/HOL
Speaker: Kyriakos Katsamaktsis
Abstract:
In his paper on “Orders of Infinity” Euler writes, without rigorous proofs, about “infinitely large” and “infinitely small” quantities and how they relate to one another. For example, he writes that if x is infinite, then its logarithm is also infinite, and the ratio of the logarithm of x divided by x is infinitely small. Such statements can be put on a rigorous footing using nonstandard analysis, which treats infinity as a number (or more than one) without using limits. We will describe the formalisation of parts of Euler’s paper in Isabelle using nonstandard analysis. We will shed light on a few vague statements and show how fairly standard modern mathematics plus some nonstandard analysis can resolve them.