一类新的数学（140210）

闵应骅

   计算机在改变世界，用它做销售，用它做通讯，用它做管理，还用它做基础研究。2014年2月CACM发表一个新闻，说现在有一批数学家和计算机科学家热衷于一类新的数学-----计算机辅助的数学证明。有人可能说，我国吴文俊院士老早就做了机器定理证明，有什么新鲜的？按本人的初浅了解，吴先生的机器定理证明其实是把“解析几何”中的“解析”用计算机来做，解决几何的问题。譬如，证明三点在一条直线上，就把两点的方程写出来，第三点坐标满足该方程，就证明了这三点在一条直线上。

   新发现不但扩展了计算机辅助定理证明的范围，而且提供新的更直观的方法把结果扣到数学基础上。使这座数学大楼更高大、更易进。大名顶顶的普林斯顿高等研究院数学学院有一位教授弗拉基米尔.沃沃斯基(Vladimir Voevodsky)，他是菲尔兹奖得主，我猜想他是原苏联人。他分享了国际数学联盟的领域奖章，该奖项和阿贝尔奖一样，号称是数学界的诺贝尔奖。他现在转向计算机怎样提升数学研究。2012-2013年这里聚集了几十位数学家和计算机科学家研究所谓同伦类型理论（HoTT）（http://homotopytypetheory.org/）。

大约一个世纪之前，数学家受到希尔伯特的“几何基础”的启发，希望所有数学都建立在几条公理之上。但是，后来证明，对于任何形式系统，关于该系统的所有定理基于几条公理不可能都得到证明。现代数学家试图把规定的那些基础与他们的目的无关，他们没有必要把他们每天的工作都归结为最初的基本原则。新的基础系统有许多实际性环节，它更接近数学推理方法，它更有利于数学家之间的合作。假如计算机验证证明(computer-verified proof)成为主流，数学家就可能做一个大的合作项目。如果计算机保证某一个结果是对的，其他人就可以在其基础上跟进，即使跟进的结果来自一个无名的研究者或者是一个初学者，或者是一个不同领域而有新想法的专家。人的独创性永远很重要。一个数学外行也可以用这个库进行高级的数学研究，只要他们有这种心理准备。计算机上的数学库还有一个好处是搜索相关结果。新想法能否成功不仅在于数学，还要看它是否被更多的数学家们所采用。

在数学的形式化证明方面，数学家和计算机科学家从未停止过探索。类型理论在集成电路设计验证中已经得到应用，在软件正确性证明、可信计算和安全验证领域也有应用。但是，建立新的类型的数学则是弗拉基米尔.沃沃斯基等人首创。近一个世纪，数学家们试图把集合论作为形式化所有数学的基础。从空集（对应于0）的概念开始，形成只有空集的第一个集合（对应为1），原理上说可以系统地构造所有数学对象。然而实际上这个过程冗长而无用。HoTT希望提供容易而又直观的工具，把严格而又形式化的数学变成标准化的实践。

   HoTT基于类型理论的数学框架。类型不像集合，可以包括任何东西，一个特定类型的对象有特定的规则去处理它们。这个概念很容易使人联想起程序语言中的数据类型，但是，数学的类型可以更复杂，譬如n-维向量，n可以是精确特征计算出来的自然数。类型理论作为自动证明助理始于1960年，但在纯数学里面很少采用。该框架对类型的概念有新的扩展。譬如说，定理的形式化本身就是一个类型，而其证明可以是该类型的一个对象。假如有一个对象存在，该定理就得到了证明。这就使类型不遗漏任何逻辑判断。大家熟知的一次成功是2005年由剑桥的微软研究院Georges Gonthier给出的四色问题的形式证明。其证明使用了证明助理Coq。Coq 2013年得ACM程序语言软件奖。瑞典哥德堡大学ThierryCoquand是开发者之一。类型理论的Coq 风格方便计算，特别是相等的可判定性。有一个算法去确定两个对象是否相等，这是证明中的关键步骤。相等的概念在HoTT中有了扩展，它是从不同数学分支的关系的实际中抽象出来的。譬如，圆、椭圆、双曲线、抛物线被统一为一个代数方程的截面，从而看出一个更大的实体。类似地，同伦类型理论表示了类型理论和同伦理论的一种关联。同伦理论是拓扑学的一个分支。从同伦的观点看，类型（可以是一个定理）看作是空间，而该同伦的对象（可以是一个证明）则是空间中的点。两点的相等可以看作是存在一条通路连接这两个点。许多同伦论的工具可以应用这种连接到数学证明。

   Coq原来是由计算机科学家设计的，基于编程语言和组合学，回过头来应用于更广大的数学。除了应用于逻辑推理之外，可以应用到拓扑问题。这种对应可以反过来，简化逻辑系统的详情，而转向拓扑学。证明的概念也要从几何证明方式中走出来。我不知道，我们国家在这方面是否开展了研究。看来在这些基础研究方面应该下力气。一方面，这些基础研究将有潜在的应用价值；另一方面，这方面原创的空间很大，国人又比较擅长理论研究。但是，切忌空谈，光谈感想、谈想法没有用，必须做实际的证明助理系统，比Coq更有独到之处，验证了自己的想法，才是中国人的创新。