1. 朴素实在期（前17世纪）​

欧几里得、毕达哥拉斯

直观几何与算术。点、线、面、自然数是自明的、客观存在的实体。欧氏几何是空间的绝对真理。

为数学提供了直观基础，但建立在“自明性”上，缺乏严格性。

2. 危机与抽象化（17-19世纪）​

牛顿/莱布尼茨、高斯/罗巴切夫斯基/黎曼、康托尔

微积分、非欧几何、集合论。空间可以是弯曲的（非欧几何）；无限可以精确处理（微积分严格化）；所有数学对象可归结为集合（集合论）。

直观崩溃。发现数学对象并非直接自明，需要更基础的概念（如集合、极限）来定义。

3. 结构主义兴起（20世纪中叶）​

诺特、布尔巴基学派

数学结构。关注对象之间的关系（如群、环、域），而非对象的内在本质。数学是研究结构的科学。

从“是什么”转向“如何关联”。为范畴论的诞生铺平了道路。

4. 范畴论革命（1940s-1960s）​

艾伦伯格、麦克莱恩、格罗滕迪克

范畴、函子、自然变换。数学宇宙由对象和态射（关系）组成。格罗滕迪克的宏伟纲领：任何空间都由其上所有可能的“层”（即所有可能的观测方式）来定义。

飞跃：相对性原理。一个对象的性质由它与其他对象的关系决定。几何不再依赖于点集。

5. 拓扑斯的诞生（1960s-1970s）​

格罗滕迪克、蒂尔内

拓扑斯。一个自身拥有内在逻辑的范畴。它本身就是一个“数学宇宙”。集合论只是其中一个特例（集合拓扑斯）。

飞跃：逻辑的几何化。不同的拓扑斯有不同的逻辑（如直觉主义逻辑）。数学宇宙是多元的。

6. 高阶范畴与∞-拓扑斯（1980s-至今）​

奎伦、卢里、雷伊兹等

∞-范畴、∞-拓扑斯。承认“等价”具有不同的强度（层次）。一个∞-拓扑斯是一个具有无限复杂、柔性“等价”关系的数学宇宙。

终极形态：柔性的宇宙。数学实在是一个具有高阶对称性和无穷维结构的复杂网络，其中“相等”是一个丰富的、具有层次的概念。

1. 古典逻辑期（前19世纪）​

亚里士多德、莱布尼茨

三段论、普遍语言。追求推理的普遍规则。莱布尼茨梦想一种“通用符号语言”，可将推理变为计算。

提供了基本的推理规则，但缺乏数学的完全形式化。

2. 形式化运动（19-20世纪初）​

弗雷格、罗素、怀特海、希尔伯特

数理逻辑、公理化、形式系统。数学命题可写为符号公式，证明可变为符号序列的机械变换。希尔伯特计划：用有穷方法证明数学的相容性。

飞跃：推理的精确化。将主观的“数学思想”客观化为可操作的“符号游戏”。

3. 哥德尔危机与计算转向（1930s）​

哥德尔、丘奇、图灵

不完备性定理、可计算性理论。任何足够强的形式系统都无法证明自身相容性。但“有效计算”的概念（λ演算、图灵机）被厘清。

希尔伯特计划失败。但注意力转向“计算”本身，为“证明即程序”埋下伏笔。

4. 构造性革命（1960s-1970s）​

海丁、马丁-洛夫

直觉主义逻辑、构造性数学、类型论。拒绝排中律，要求证明必须是构造性的。马丁-洛夫类型论将“命题”视为“类型”，其“证明”是该类型的一个具体“项”（程序）。

飞跃：命题即类型，证明即程序。证明从抽象的逻辑判断，转变为具体的、可计算的构造活动。

5. 自动化与验证（1980s-2000s）​

科莫伦德、Coq/Agda等

定理证明器、依赖类型论。类型论成为计算机辅助证明的基础。数学家真正开始在机器中形式化并验证证明。

飞跃：认知的机械化。数学推理的可靠性达到了前所未有的高度。

6. 几何化认知（21世纪初）​

沃伊德沃茨基

同伦类型论、单值公理。将类型解释为“空间”，将类型的等价解释为空间的“同伦等价”。单值公理断言：在宇宙中，逻辑上的“等价”就是几何上的“相同”。

终极形态：认知的几何化。最抽象的推理规则（语法）本身，呈现出具体的几何图像（语义）。