闵应骅的博客分享 http://blog.sciencenet.cn/u/ymin 一位IEEE终身Fellow对信息科学及其发展的看法

博文

一类新的数学(140210) 精选

已有 8022 次阅读 2014-2-10 08:49 |个人分类:计算机|系统分类:科研笔记| 同伦类型理论, 机器定理证明

一类新的数学(140210

闵应骅

 

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

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

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

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

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

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




http://blog.sciencenet.cn/blog-290937-766146.html

上一篇:神秘的大脑(140129)
下一篇:以小见大找科研----计算摄影(140217)

19 彭思龙 唐常杰 徐传胜 温世正 邹斌 文克玲 苏德辰 韦玉程 强涛 李伟钢 王小平 柳林涛 仲银鹏 王号 赵凤光 张利华 dulizhi95 sunyuhan1991 dailiangren

该博文允许注册用户评论 请点击登录 评论 (26 个评论)

数据加载中...
扫一扫,分享此博文

Archiver|手机版|科学网 ( 京ICP备07017567号-12 )

GMT+8, 2020-10-29 05:15

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部