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

在19世纪早期，人们发现欧几里得几何不仅是可能的几何。这是一个革命性的发现，让数学家们想知道我们生活在什么样的空间里。他们唯一能确定的就是太空是局部欧几里得的。这促使黎曼构思了流形的概念。然而，这个概念最初是模糊的，经过Poincarz和Weyl等数学家的重新解释，直到1936年Hassler Whitney才用现代形式提出了这个概念。该项目旨在使空间数学，即微分几何正规化，特别注重探索替代基础。具体地说，我们将形式化几何代数，这是一个历史上优先于更常见的向量空间概念的概念，是一个更具表现力和更强大的系统。我们还计划将几何代数的非标准扩展正式化，这应该会产生具有不寻常性质的对象，例如无限大和小的多重向量。我们打算在几何代数的背景下形式化流形的一般概念。我们将使用交互式定理证明器Isabelle，它已经拥有了代数和拓扑学中所需的概念，以及诸如Locale之类的工具，这些工具允许对结构的一般定义，这些结构稍后可以实例化到有趣的特殊情况。通过这种形式化，我们将获得对空间数学中涉及的概念的更好的理解和另一种解释，以及对数学史上最重要的转折点的更深层次的理解，这引发了当今数学研究的许多领域，包括代数几何、微分几何和拓扑学。相关的数学工具也完全是物理学中使用的工具，例如在描述广义相对论时使用的工具，因此对这些工具的替代基础的形式化和探索可能会带来新的见解。

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.