A Combination of Geometry Theorem Proving and Nonstandard Analysis with Application to Newton's Prin

Introduction.- A Brief History of the Infinitesimal.- The Principia and its Methods.- On Nonstandard Analysis.- Objectives.- Achieving our Goals.- Organisation of this book.- Geometry Theorem Proving.- Historical Background.- Algebraic Techniques.- Coordinate-Free Techniques.- Formalizing Geometry in Isabelle.- Concluding remarks.- Constructing the Hy perreals.- Isabelle/HOL.- Properties of an Infinitesimal Calculus.- Internal Set Theory.- Constructions Leading to the Reals.- Filters and Ultrafilters.- Ultrapower Construction of the Hyperreals.- Structure of the Hyperreal Number Line.- The Hypernatural Numbers.- An Alternative Construction for the Reals.- Related Work.- Concluding Remarks.- Infinitesimal and Analytic Geometry.- Non-Archimedean Geometry.- New Definitions and Relations.- Infinitesimal Geometry Proofs.- Verifying the Axioms of Geometry.- Concluding Remarks.- Mechanising Newton's Principia.- Formalizing Newton's Properties.- Mechanized Propositions and Lemmas.- Ratios of Infinitesimals.- Case Study: Propositio Kepleriana.- Expanding Newton's Proof.- Conclusions.- Nonstandard Real Analysis.- Extending a Relation to the Hyperreals.- Towards an Intuitive Calculus.- Real Sequences and Series.- Some Elementary Topology of the Reals.- Limits and Continuity.- Differentiation.- On the Transfer Principle.- Related Work and Conclusions.- Conclusions.- Geometry, Newton and the Principia.- Hyperreal Analysis.- Further Work.- Concluding Remarks.-