The various chapters of this book have covered the development of a range of theories in the theorem prover Isabelle. The main unifying theme has been the use of infinitesimals as valuable tools that are once again respectable in mathematics. Infinitesimals have been around for over 2 000 years and generally had a bad press. Their use has at times been free and viewed as a blessing (throughout the eighteenth century, for example), and at others viewed as heresy and banned (from the nineteenth century until the middle of this century). What is undeniable is that they have been valued as intuitive tools at all times by generations of mathematicians who used them to solve problems and carry out proofs. Even those trying to get rid of them sometimes lapsed into infinitesimal reasoning. The great insight of Robinson, leading to the creation of NSA, has been praised over and over again. In a sense, his work vindicates the (sometimes blind) faith of influential mathematicians such as the Marquis de L’Hospital in the use of infinitesimals. The major achievement of Robinson and his followers was not only to rehabilitate the infinitesimal as a sound mathematical concept but also to bring along new types of numbers that added to the power of the nonstandard approach.
KeywordsNumber System Euclidean Geometry Differential Calculus Diagrammatic Reasoning Geometry Theorem
Unable to display preview. Download preview PDF.