A Combination of Geometry Theorem Proving and Nonstandard Analysis with Application to Newton’s Principia

Sir Isaac Newton’s philosophi Naturalis Principia Mathematica’(the Principia) contains a prose-style mixture of geometric and limit reasoning that has often been viewed as logically vague.In A Combination of Geometry Theorem Proving and Nonstandard Analysis, Jacques Fleuriot presents a formalization of Lemmas and Propositions from the Principia using a combination of methods from geometry and nonstandard analysis. The mechanization of the procedures, which respects much of Newton’s original r…