Nonstandard Geometric Proofs

This paper describes ongoing work in our formal investigation of some of the concepts and properties that arise when infinitesimal notions are introduced in a geometry theory. An algebraic geometry theory is developed in the theorem prover Isabelle using hyperreal vectors. We follow a strictly definitional approach and build our theory of vectors within the nonstandard analysis (NSA) framework developed in Isabelle. We show how this theory can be used to give intuitive, yet rigorous, nonstandard proofs of standard geometric theorems through the use of infinitesimal and infinite geometric quantities.