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

在世纪早期，人们发现欧几里德几何不仅是可能的几何。这是一个革命性的发现，引起了数学家们对我们生活在什么样的空间的好奇。他们所能确定的只是空间是局部欧几里得空间。这导致黎曼设想的概念，一个流形。然而，这个概念最初是模糊的，在庞加莱和魏尔等数学家重新解释后，它只是在1936年由哈斯勒·惠特尼以现代形式提出。该项目旨在正式化空间数学，即微分几何，特别关注探索替代基础。具体来说，我们将形式化几何代数，这是一个历史上的概念，更常见的概念向量空间，是一个更有表现力和更强大的系统。我们还计划将几何代数的非标准扩展形式化，这应该会产生具有不寻常属性的对象，例如无限大和小的多向量。我们打算在几何代数的范围内形式化流形的一般概念。我们将使用交互式定理证明器Isabelle，它已经具备了代数和拓扑学所需的概念，以及允许结构的一般定义的工具，这些结构可以在以后实例化为有趣的特殊情况。通过这种形式化，我们将对空间数学中涉及的概念有更好的理解和替代解释，沿着更深入地了解最重要的转折。数学史上的一个重要转折点，引发了现代数学研究的许多领域，包括代数几何、微分几何和拓扑学。相关的数学工具也正是物理学中使用的工具，例如描述广义相对论，因此这些工具的形式化和对替代基础的探索可能会带来新的见解。

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.