类型论中的数学

数学是什么？我认为基本上可以分为四类。有定义、真/假陈述、证据和想法。

定义(例如实数或π)和真/假陈述(例如费马大定理的陈述或黎曼假设的陈述)是数学科学的一部分：这些都是黑白的东西，在某些基本系统中具有完全严格的意义。

从某种意义上说，证明是数学的通货：证明赢得奖品。建造它们是一门艺术，检查它们是一门科学。这非常简单地解释了为什么计算机验证系统，如精益、Coq、Isabelle/HOL、AGDA…。更擅长检查证据而不是构建证据。

而思想是数学中纯粹的艺术部分。那个“电灯泡”时刻，使你能够解决问题的洞察力--这就是难以捉摸的数学概念。

从形式上讲，思想是我对数学理解最少的部分。这里有两个问题：

第一个问题是一个精确的“科学”问题。群是具有某种额外结构并满足某些公理的集合。正式的答案在维基百科的群组页面上。组是一个定义。但是第二个问题是一个不同类型的问题。不同的人对群体有不同的看法。比方说是由满足条件的元素生成的群。你能说些什么呢？如果你是一名刚刚看到组的正式定义的数学本科生，你可能什么都不会说。如果你对群论有了更成熟的理解，你马上就会知道这个群体是微不足道的，因为你对正在发生的事情有一个更复杂的模型。想法是复杂的，而且依赖于人类。计算机对群的概念，实际上是维基百科中定义的副本，这也是目前计算机不善于自己证明新定理的原因之一。你可以通过教计算机关于群的定理，或者教它群的例子，或者尝试编写自动计算群论定理或群的例子的人工智能来发展它的直觉。但是直觉是一个非常微妙的东西，我一点也不理解，所以我在这里就不再多说这些想法了。我认为地图是“规范”的概念是一种想法，而不是定义--我认为不同的数学家对这个黄鼠狼这个词有不同的思考方式。在这篇文章中，我将讨论其他三个概念是如何在类型理论、精益定理证明器中实现的。

与思想相反，数学的其他部分(定义、定理/猜想和证明)可以在一个基本系统中形式化，因此可以以精确的方式在计算机上创建和存储。这里，我不是指pdf文件！PDF文件正是我想要离开的地方！我的意思是，人们设计了理解各种数学基础(集合论、类型论、范畴论)之一的计算机编程语言，然后数学家可以用这种语言编写代码来表示所讨论的定义、对/错陈述或证明。

我当然没有资格用范畴论来解释这一切是如何运作的。在集合论中，我只做一个观察。集合论中的定义，例如实数或的定义是一个集合。而证明是逻辑上的一系列步骤。在我看来，定义和证明在集合论中是完全不同的两件事。群是这些东西的混合体-群是满足一些公理的有序四元组，所以它是一个附加了一些逻辑的集合。

然而，在类型理论中，情况却出人意料地不同。所有三件事--定义、真/假陈述和证据--都是一回事！这些都是条款。一组，一个证明，实数--它们都是术语。这种定义和证明的统一-集合和逻辑-似乎使类型理论成为向计算机教授所有本科生水平的数学的实用基础系统。

在类型理论中，一切都是一个术语。但有些术语是类型。不是每个术语都是一种类型，但每个术语都有一种类型。冒号用于表示精益中术语的类型-符号x：t表示x是T类型的术语。例如，实数π(Pi)是精益中的术语，实数ℝ是一种类型，我们有π:ℝ，即π是ℝ类型的术语。在集合论中我们写的是π∈ℝ，在类型论中我们写的是π:ℝ。它们都表达了相同的数学概念--“π是一个实数”。

现在，π是一个术语，但它不是一种类型。在精益中，x：π毫无意义。在集合论中，x∈π碰巧是有意义的，但这是一个奇怪的巧合，因为一切都是一个集合。此外，π的实际元素将取决于实数是如何实现的(例如，DedekindCuts或Cauchy序列)，因此在集合论中x∈π没有数学意义；它碰巧是有意义的，但这是系统的一个奇特现象。

我在上面声称，每个学期都有一种类型。那么ℝ的类型是什么呢？事实证明，ℝ：TYPE。实数是一个被称为类型的“宇宙”类型的术语，类型理论类似于所有集合的类别。

许多数学家认为是定义的数学对象要么有类型Type，要么有类型T，其中T：type。作为一个模糊的经验法则，我们用大写字母书写的东西(组、环、…)。或者花哨的字母(实数，有理数)的类型是Type，而我们用小写字母(组中的元素g，实数r或整数n)写的东西都有类型T，其中T是我们认为的包含这些元素的集合。例如，2：ℕ和ℕ：Type，或者如果是组的一个元素，那么在Lean中我们有g：g和g：Type。你可以看到这里有一个三层的层次结构--术语在底部，类型在它们上面，宇宙在顶部。

类型的例子有：ℝ，ℕ、G(群)、R(环)、X(集合论者称之为集合)、Banach空间等等。形式上，我们说ℝ：TYPE。

术语的例子：π(ℝ类型的术语)，g(群G的元素，所以是G类型的术语)，x(X的元素，所以是X类型的术语)。正式地说，我们说g：g。

这种层次结构比集合论中的层次结构更具表现力，集合论中的层次结构只有两个级别：类(例如，所有集合的类)和集合。

冒号在数学中有一个标准用法--在函数的表示法中。如果X和Y是集合(如果你在做集合论)或类型(如果你在做类型论)，那么从X到Y的函数的符号是f：X→Y。这实际上与Lean对冒号的使用是一致的；Lean对从X到Y的函数集合的符号是X→Y，它是一种类型(即X→Y：TYPE，对应于集合论者认为是集合的事实)，f：X→Y意味着f是类型X→Y的术语，是的类型理论版本，也就是说f是类型理论中从X到Y的函数。

(不是为了考试)严格地说，宇宙是类型，类型是术语，但这是一个语言问题：人们谈到类型，往往是指不是宇宙的类型，当人们谈到术语时，他们指的是不是类型的术语。但并不总是这样。当我还是个初学者的时候，这让我很困惑。

这就是有趣的开始。到目前为止，看起来类型就是类型理论家所说的集合，而术语就是他们所说的元素。但现在让我们看看Lean的类型理论中的另一个宇宙，真/假陈述的宇宙支柱，在这个宇宙中，我们对正在发生的事情的传统心理模型是完全不同的。我们将了解定理和证明如何以与类型和项相同的方式建模。

那么，这一切是怎么运作的呢？除了宇宙类型，在利恩的类型理论中还有第二个宇宙，称为道具。Prop类型的术语是真/假陈述。这里有一个不幸的符号冲突。在数学中，命题这个词经常被用来表示婴儿定理，而定理是真的(否则它们就是猜想或反例之类的)。在这里，我们用与逻辑学家相同的方式使用命题-命题是一种通用的真/假陈述，其真值是无关紧要的。

有了例子，这一切都会变得更加清楚。2+2=4是一个命题，所以我们可以写2+2=4：命题。但是2+2=5也是一个命题，所以2+2=5也是命题。我再说一遍--命题不一定是真的！命题是对/错的陈述。让我们来看一些更复杂的例子。

对于所有自然数的真/假陈述是一个命题：在精益中，这可以表示为(∀x：ℕ，x+0=x)：prop。命题是一个Prop类型的术语(就像我们前面看到的类型是类型术语一样)。设RH表示黎曼假设的陈述。那么RH：道具。我们不在乎它是真是假，独立于数学公理，不可判定，等等。命题是对/错的陈述。让我们看看Lean的类型理论层次结构中的一部分，它生活在道具宇宙中。

类型的例子：2+2=4，2+2=5，费马大定理的陈述，黎曼假设的陈述。

这就是类型理论的世界与集合论中的事物设置方式严重背离的地方，也是直到三年前我大脑中的事物设置方式的严重背离。在试图理解这里发生的事情时，我甚至意识到，数学家们在这里的语言上有一些自由。在我们开始之前，先考虑一下这一点。Bolzano-Weierstrass定理是对具有收敛子序列的有界序列进行分析时的某种表述。我想谈谈数学家在实践中是如何使用“玻尔扎诺-魏尔斯特拉斯定理”这一短语的。数学家会说，Bolzano-Weierstrass定理是关于具有收敛子序列的序列的这一陈述。但是如果他们在证明过程中，需要应用它来继续他们的证明，他们会说，“根据Bolzano-Weierstrass定理，我们推导出有一个收敛的子序列”。这一切似乎一点都不好笑。但我想指出的是，数学家们正在以两种不同的方式使用“玻尔扎诺-魏尔斯特拉斯定理”。当他们说它是什么的时候，他们指的是定理的陈述。但当他们说他们在使用玻尔扎诺·魏尔斯特拉斯定理时，他们实际上使用的是它的证明。Birch和Swinnerton-Dyer猜想是一个完美的真/假陈述，你当然可以说它是什么。但是如果你想要你的证明是完整的，你不能在证明其他东西的过程中使用Birch和Swinnerton-Dyer猜想，因为在写这篇文章的时候，这个猜想还是一个悬而未决的问题。在这里，明确区分定理的陈述和定理的证明是很重要的。数学家可能会用短语“博尔扎诺-魏尔斯特拉斯定理”来表示这两个概念中的任何一个。这种非正式的记号滥用可能会让初学者感到困惑，因为在下面的内容中，能够区分定理陈述和定理证明是非常重要的；它们是完全不同的两件事。

在自然数游戏中，我使用这种记数法的滥用，因为我试图与数学家交流。语句∀x：ℕ，x+0=x是真的，我会说“这在精益中叫做ADD_ZERO”。在自然数游戏中，我编写了诸如ADD_ZERO：∀x：ℕ，x+0=x的语句，但这意味着在精益中称为ADD_ZERO的术语是∀x：ℕ，x+0=x的证明！冒号正以类型论的方式使用。在自然数游戏中，我故意对这个概念含糊其辞。我让数学家相信ADD_ZERO在某种程度上等于所有人的“想法”。但是在幕后，∀x：ℕ，x+0=x是一个命题，它是一个类型，而Add_Zero是它的证明，这是一个术语。在这里，明确区分定理的陈述和证明是很重要的。陈述是类型，证据是术语。

类型的例子：2+2=4，2+2=37，费马大定理的陈述-∀x y z：ℕ，n>；2∧x^n+y^n=z^n→x*y=0。

项的例子：2+2=4的证明(类型为2+2=4的项)，费马大定理的证明(类型为∀x y z：ℕ，n>；2∧x^n+y^n=z^n→x*y=0)。

因此，我们对声明π:ℝ的心智模型是，类型ℝ是“东西的集合”，而术语π是该集合的成员。如果我们继续这个类比，它说语句2+2=4是某种集合，并且2+2=4的证明是该集合的成员。换句话说，Lean建议我们将真/假陈述2+2=4建模为某种集合，2+2=4的证明是该集合的一个元素。在精益理论中，命题的所有证明都是平等的，这是一个固有的公理。所以，如果a：2+2=4，b：2+2=4，那么a=b，这是因为我们在Prop宇宙中工作，这就是命题在精益中的表现。在类型宇宙中，这个类比一点也不正确--我们有π:ℝ和37：ℝ，当然还有π≠37。道具宇宙的这种特殊怪癖被称为“证据无关”。形式上我们可以说，如果P：Prop，如果a：P，如果b：P，那么a=b。当然，如果一个命题是假的，那么它根本没有证据！就像是空集。所以Lean的命题模型是，真的就像有1个元素的集合，而假的就像有0个元素的集合。

回想一下，如果f：x，→，Y，那么这意味着f是从X到Y的函数，现在，假设和是命题，假设我们知道。这是什么意思？这意味着这意味着。它的意思是，如果是真的，那么就是真的。这意味着如果我们有证据，我们就可以证明。它是从证明到证明的函数。它是将的元素发送到的元素的函数。它是一个P-→，Q类型的项。同样，证明是一项h：P，→，Q。这就是为什么在自然数博弈中，我们用→符号来表示蕴涵。

让false表示一般的false语句(认为是有0个元素的集合)，让true表示一般的true语句(认为是有1个元素的集合)。我们能构造一个类型为False→False或类型为True→True的项吗？当然可以--只需使用身份识别功能即可。事实上，在这两种情况下都有一个唯一的函数-HOM集的大小为1。我们能构造一个类型为False→True的项吗？当然，有一个函数，从有0个元素的集合到有1个元素的集合，而且这个函数也是唯一的。但是我们能构造一个True→False类型的项吗？不，我们不能，因为我们要把真实性的证明寄到哪里？没有假的证据可以寄给你。所以True，→，False是一个大小为0的集合。这与→的标准真值表相对应，在该表中，我们分析的前三个陈述是真的，最后一个是假的。

那么∀x y z：ℕ，n>；2∧x^n+y^n=z^n→x*y=0的证明是什么样子呢？在这个命题中有一个箭头，所以费马大定理的陈述是某种形式的集合，这意味着在Lean中，费马大定理的证明实际上是一个函数！。下面是该函数的功能。它有四个输入。前三个输入是自然数x，y和z。第四个输入是证明：它是命题n>；2∧x^n+y^n=z^n的证明。该函数的输出是命题x*y=0的证明。这是一种相当非常规的方式来思考费马大定理的证明是什么，我要强调的是，这对实际试图理解证明毫无帮助-但这是一个完全一致的数学工作方式的心理模型。将数字和证明的概念统一起来-将它们都视为术语-使您能够将证明视为函数。LEAN是一种函数式编程语言，特别是它是以函数为核心进行设计的。我相信，这就是为什么像Lean、Coq和Isabelle/HOL这样的定理证明者使用