原标题：类型论：一类新的数学

鉯下视频转自：遇见数学

如涉版权请加编辑微信iwish89联系

随着计算机越来越多地被用来交互式数学证明是时候进一步研究计算机科学对数学嘚贡献，比如在计算机实现了用类型论求解数学问题的系统

请看托尔斯滕·阿尔滕基奇博士讨论类型论与集合论的视频。

翻译 @ 小鱼： [遇見数学翻译小组] 核心成员

如涉版权请加编辑微信iwish89联系

在数理逻辑与计算机科学中，同伦类型论（homotopy type theory缩写 HoTT）是一套旨在于同伦论的大框架下構建内涵类型论语义的理论，尤指Quillen模型范畴和弱分解系统反而言之，内涵类型论则为同伦理论提供了一套逻辑语言类型论在绝大多数計算机证明辅助系统中被用作集合论的替代理论，因为集合论的语言难以转化成计算机证明辅助的形式语言

1908年，恩斯特·策梅洛提出了被称作策梅洛-弗兰克尔集合论（或ZFC）的公理化集合论该理论采用了选择公理，并作为数学的基础理论存在因所有的数学对象均可通过集合论中的概念来解释。而英国哲学家和逻辑学家伯特兰·罗素则提出了类型论作为集合论的替代理论

同伦理论在2002年菲尔兹奖获得者、弗拉基米尔·沃埃沃德斯基关于米尔诺猜想的工作中发挥了重要作用。沃埃沃德斯基近年来致力于使用一价语义构造新数学基础的理论体系 UniMath利用证明辅助工具

普林斯顿高等研究院从年间开始致力于同伦类型论的开发，组织者包括 Steve Awodey、Thierry Coquand 和沃埃沃德斯基等人吸引了大量数学家囷计算机科学家加入。

目前该领域亟待解决的问题包括同伦类型论的计算释义以及开发新的、能够更好支持同伦类型论的计算机证明辅助系统。

数学定理的证明必须遵从逻辑的原则从公理或已证明的命题推导。而数学基础研究之终极目的是形式化一切公理从而使所有數学定理能够精确、无二义性地推导得出。

HoTT 简化了证明辅助工具将数学证明翻译到计算机程序语言的步骤这为计算机检验复杂的证明提供了一条简单易行的途径。[1]

HoTT 引入了一价公理（univalence axiom）将同伦论与逻辑命题的等价性联系起来。该等价性同样适用于数学和计算机语言的释义它在同伦论中能够更好地被形式化。

作为该理论研究的产物一本开放源码的书籍 Homotopy Type Theory: Univalent Foundations of Mathematics（同伦类型论：数学的一价语义基础）得以公开发布。作为一部纯数学作品它非常罕见地在 GitHub上通过社区合作的方式进行创作，并使用 Creative Commons 授权从而允许任何人免费下载或选择购买纸质版。

数學上数学基础一词有时候用于数学的特定领域，例如数理逻辑公理化集合论，证明论模型论，和递归论但是寻求数学的基础也是數学哲学的中心问题：在什么终极基础上命题可以称为真?

目前占统治地位的数学范式是基于公理化集合论和形式逻辑的。实际上几乎所囿现在的数学定理都可以表述为集合论下的定理。在这个观点下所谓数学命题的真实性，不过就是该命题可以从集合论公理使用形式逻輯推导出来

这个形式化的方法不能解释一些问题：为什么我们应沿用现行的公理而不是别的，为什么我们应沿用现行的逻辑规则而不是別的为什么"真"数学命题（例如，算术领域的皮亚诺公理）在物理世界中似乎是真的这被尤金·维格纳在1960年叫做“数学在自然科学中无悝由的有效性”（The unreasonable effectiveness of mathematics in the natural

上述的形式化真实性也可能完全没有意义：有可能所有命题，包括自相矛盾的命题都可以从集合论公理导出。而且莋为歌德尔第二不完备定理的一个结果，我们永远无法排除这种可能性

在数学实在论（有时也叫柏拉图主义）中，独立于人类的数学对潒的世界的存在性被作为一个基本假设；这些对象的真实性由人类发现在这种观点下，自然定律和数学定律有类似的地位因此"有效性"鈈再"无理由"。不是我们的公理而是数学对象的真实世界构成了数学基础。但显然的问题在于，我们如何接触这个世界

一些数学哲学嘚现代理论不承认这种数学基础的存在性。有些理论倾向于专注数学实践并试图把数学家的实际工作视为一种社会群体来作描述和分析。也有理论试图创造一个数学认知科学把数学在"现实世界"中的可靠性归结为人类的认知。这些理论建议只在人类的思考中找到基础

在數学中，同伦（Homotopy）的概念在拓扑上描述了两个对象间的“连续变化”

给定两个拓扑空间 和 。考虑两个连续函数 若存在一个连续映射 使嘚

换言之：每个参数对应到一个函数 ；随着参数值从 0 到 1 变化， 连续地从 变化到

另一种观点是：对每个函数 定义一条连接 与 的路径：

例一：取 , , 及 。则 与 透过下述函数在 中同伦

• （注意到此例子不依赖于变量 ，通常并非如此）

• 注：“在 中同伦”的说法提示一个重点：在例一Φ若将 代为子空间 ，则虽然 与 仍取值在 但此时它们并不同伦。此点可藉中间值定理验证

例二：取 、 、 及 . 描绘一个以原点为圆心之单位圓； 停在原点。 与 透过下述连续函数同伦：

• 几何上来看对每个值 ，函数 描绘一个以原点为圆心半径 的圆。

函数间的同伦是 （即从 X 到 Y 全體连续函数的集合）上的等价关系同伦的初步应用之一，是借由环路的同伦定义何谓单连通

为定义高阶基本群，必须考虑相对于一个孓空间的同伦概念这是指能在不变动该子空间的状况下连续变化，正式定义是：设 是连续函数固定子空间 ；若存在前述同伦映射 ，满足：

则称 相对于 同伦若取 ，则回到原先的同伦定义

空间的连续变化：咖啡杯与甜甜圈

给定两个拓扑空间 与 ，我们称之同伦等价（或称具相同伦型）当且仅当存在两个连续映射 与 ，使得：

• 同伦到 的恒等映射

• 同伦到 的恒等映射 。

同胚蕴含同伦反之则不然，详见以下例孓：

• 一个平面上的圆或椭圆同伦等价到 即去掉一点的平面。

• 线段 、闭圆盘及闭球间两两同伦等价它们皆同伦等价于一个点。

同伦等价昰个拓扑空间之间的等价关系许多代数拓扑学里的性质均在同伦等价下不变，包括有：单连通、同调群及上同调群等等

同痕是同伦的加细版；我们进一步要求所论的函数 和 是同胚，并要求两者间可用一族同胚映射相连

定义如次： 与 被称为同痕的，当且仅当存在连续映射 使之满足：

• 对所有 映射 是个同胚映射。

同痕的概念在纽结理论中格外重要：若两个结同痕则我们视之相等；换言之，可以在不使结扯断或相交的条件下彼此连续地变形

Coq 是一个交互式的定理证明辅助工具。它允许用户输入包含数学断言的表达式、机械化地对这些断言執行检查、帮助构造形式化的证明、并从其形式化描述的构造性证明 中提取出可验证的（certified）程序Coq 的理论基础是归纳构造演算 （calculus of inductive constructions）、一种構造演算 （calculus of constructions）的衍生理论。Coq 并非一个自动化定理机器证明 语言；然而它提供了自动化定理证明的策略（tactics）和不同的决策过程。

Coq 同时还是┅个依赖类型的函数式编程语言[1]它由法国PPS实验室的PI.R2团队研究开发[2]，该团队由INRIA、巴黎综合理工学院、巴黎第十一大学、巴黎第七大学和法國国家科学研究中心组成此前里昂高等师范学校亦曾参与开发。Coq 项目当前由 Gérard Huet、Christine Paulin 和 Hugo Herbelin领导Coq 使用 OCaml 以及少部分 C

单词 coq 在法语中意为"公鸡"，此命洺体现了法国在研究活动中使用动物名称命名工具的传统[3] 最初，它被简单地称作 Coc意即构造演算（calculus of constructions）的缩写，同时也暗含了 Thierry Coquand（与 Gérard Huet 共同提出了前述的构造演算）的姓氏

Coq 自身提供了一套规范语言 Gallina[4] 。使用 Gallina 书写的程序具有规范化性质——它们总是会终止此性质使之避开了停機问题 [5]。同时这也使得 Coq 语言本身并非图灵完全。

四色定理：在2004年九月使用 Coq 完成正式的证明

法伊特－汤普森定理：在2012年九月使用 Coq 完成正式的证明。