Turning Points in the Mathematics of Space: a Formalisation of Alternative Foundations for Differential Geometry

During the early 19th century, it was found that Euclidean geometry was not only possible geometry. This was a revolutionary discovery and caused mathematicians to wonder what kind of space it is that we live in. All they knew for certain was that space is locally Euclidean. This led Riemann to conceive of the notion of a manifold. However, this concept was initially vague, and, after reinterpretations by mathematicians such as Poincarz and Weyl, it was only stated in its modern form by Hassler Whitney in 1936.

This project aims to formalise the mathematics of space, i.e. differential geometry, with a particular focus on exploring alternative foundations. Specifically, we will formalise geometric algebra, which is a historically-prior concept to the more common idea of vector spaces, and is a more expressive and more powerful system. We also plan to formalise the nonstandard extension of geometric algebra, which should give rise to objects with unusual properties e.g. infinitely large and small multivectors. We intend to formalise a general notion of manifolds within the context of geometric algebra. We will use the interactive theorem prover Isabelle which already has the required notions from algebra and topology as well as tools such as locales which allow general definition of structures which can later be instantiated to interesting special cases.

With this formalisation we will obtain an improved understanding and alternative interpretation of the concepts involved in the mathematics of space along with deeper appreciation of the most significant turning point in history of mathematics, which gave rise to many areas of present day mathematics research, including algebraic geometry, differential geometry and topology. The relevant mathematical tools are also exactly those used in physics, e.g. in describing general relativity, so a formalisation and exploration of alternative foundations for these tools could lead to new insights.