建设未来的数学图书馆

2020-11-12 02:31:37

每天,数十名志同道合的数学家聚集在一个名为Zulip的在线论坛上,建立他们认为是他们所在领域未来的东西。

他们都是名为精益(Lean)的软件程序的忠实拥护者。这是一个“证明助手”,原则上可以帮助数学家写证明。但在精益能够做到这一点之前,数学家们自己必须手动将数学输入到程序中,将数千年积累的知识转化为精益能够理解的形式。

伦敦帝国理工学院(Imperial College London)的凯文·巴扎德(Kevin Buzzard)说:“很明显,当你把东西数字化时,你可以用新的方式来使用它。”“我们将把数学数字化,这会让它变得更好。”

数学数字化是一个长期的梦想。预期的好处从平凡的计算机给学生的作业评分,到超凡的:使用人工智能发现新的数学,找到旧问题的新解决方案。数学家预计,证据助手还可以审查期刊提交的文件,发现人类审查员偶尔遗漏的错误,并处理填写证据所有细节所需的繁琐技术工作。

但首先,聚集在Zulip上的数学家必须向Lean提供相当于本科数学知识的图书馆,而他们只完成了一半。Lean不会在短期内解决悬而未决的问题,但从事这项工作的人几乎可以肯定,几年后,该程序至少能够理解四年级期末考试中的问题。

在那之后,谁知道呢?参与这些努力的数学家们并没有完全预料到数字数学会有什么用处。

雷恩大学(University Of Rennes)的塞巴斯蒂安·古泽尔(Sébastien Gouëzel)说:“我们真的不知道我们的目标是什么。”

整个夏天,一群经验丰富的精益用户举办了一个名为“好奇的数学家的精益”的在线研讨会。在第一节课中,悉尼大学的斯科特·莫里森演示了如何在程序中编写证明。

他首先输入了他想要用Lean理解的语法来证明的陈述。简单地说,它的意思是“有无穷多个质数。”有几种方法可以证明这一说法,但莫里森想要使用对已发现的第一个方法的轻微修改,即公元前300年欧几里得的证明,它涉及将所有已知素数相乘,然后加1来找到新的素数(要么乘积本身,要么是它的一个因子是素数)。莫里森的选择反映了使用精益的一些基本原理:用户必须自己想出证明的大点子。

莫里森在后来的一次采访中说:“你要为第一个建议负责。”

在输入陈述和选择策略后,莫里森花了几分钟时间阐述了证据的结构:他定义了一系列中间步骤,每个步骤都相对简单,单靠自己就能证明。虽然精益不能提出证明的整体策略,但它通常可以帮助执行更小、更具体的步骤。莫里森把证据分成几个可管理的子任务,这有点像大厨指导线条厨师切洋葱、炖炖肉。莫里森说:“在这一点上,你希望精益能接手并开始提供帮助。”

精益通过使用被称为“战术”的自动化流程来执行这些中间任务。可以把它们看作是为执行非常具体的工作而量身定做的短小算法。

在研究他的证明时,莫里森使用了一种名为“图书馆搜索”的策略。它搜索了Lean的数学结果数据库,并返回了一些它认为可以填充证明特定部分细节的定理。其他策略执行不同的数学杂务。一种叫做“线性”的方法,可以利用两个实数之间的一组不等式,为你确认一个涉及第三个数的新的不等式是正确的:如果a是2,b大于a,那么3a+4b大于12。另一种方法完成了应用基本代数规则(如结合性)的大部分工作。

伦敦帝国学院(Imperial College London)数学专业本科生阿米莉亚·利文斯顿(Amelia Livingston)正从Buzzard那里学习精益课程,她说:“两年前,你必须自己在精益课程中[应用联想属性]。”“然后(有人)写了一个战术,可以为你做所有的事情。每次我使用它,我都会非常开心。“。

莫里森总共花了20分钟才完成欧几里德的证明。在一些地方,他自己填写细节;在另一些地方,他使用策略为他做这件事。在每一步,Lean都会检查以确保他的工作与程序的基本逻辑规则一致,这些规则是用一种名为依赖类型理论的形式语言编写的。

“这就像一款数独应用。如果你做出一个无效的举动,它就会引起轰动。“Buzzard说。最后,利恩证明莫里森的证明是有效的。

当技术介入做一些你过去自己做的事情时,这种练习总是令人兴奋的。但欧几里德的证据已经存在了2000多年。当今数学家关心的问题是如此复杂,以至于利恩甚至还不能理解这些问题,更不用说支持回答它们的过程了。

另一位Lean用户、福特汉姆大学(Fordham University)的希瑟·麦克白(Heather Macbeth)说:“这可能需要几十年的时间才能成为研究工具。”

因此,在数学家能够与Lean合作解决他们真正关心的问题之前,他们必须在程序中配备更多的数学知识。这实际上是一项相对简单的任务。

莫里森说:“精益能够理解一些东西,很大程度上就是人类把数学教科书翻译成精益能够理解的形式。”

不幸的是,直截了当并不意味着容易,特别是考虑到对于许多数学来说,教科书并不真正存在。

如果你没有学过高等数学,这门课可能看起来很精确,而且有很好的文档:代数I通向代数II,预微积分通向微积分,所有这些都在教科书中列出,答案在后面。

但高中和大学数学--甚至很多研究生数学--在整个知识中只占极小的一部分。其中绝大多数都没有那么有条理。

数学中有许多巨大而重要的领域从未被完整地记录下来。它们储存在一小群人的脑海中,他们从从发明者那里学到数学的人那里学到了他们的子领域--也就是说,它几乎和民间传说一样存在。

还有其他领域已经写下了基础材料,但它是如此冗长和复杂,以至于没有人能够检查它是否完全正确。取而代之的是,数学家们只是有信心。

他说:“我们依赖作者的声誉。巴黎萨克雷大学的帕特里克·马索特说:“我们知道他是个天才,也是个细心的人,所以这一定是正确的。”

这就是为什么取证助手如此有吸引力的原因之一。将数学翻译成计算机能够理解的语言,迫使数学家最终将他们的知识归类,并精确地定义对象。

法国国家研究机构Inria的阿西娅·马赫布比(Assia Mahboubi)回忆说,她第一次意识到这样一个有序的数字图书馆的潜力时说:“从理论上讲,人们可以通过纯粹的逻辑语言捕捉整个数学文献,并将数学语料库存储在计算机中,然后使用这些软件进行检查和浏览,这对我来说是一件令人着迷的事情。”

Lean并不是第一个拥有这种潜力的项目。第一个叫Automath,在20世纪60年代问世,Coq,当今使用最广泛的证据助手之一,在1989年问世。CoQ用户已经用它的语言形式化了很多数学,但这项工作一直是分散的和无组织的。数学家从事他们感兴趣的项目,只定义执行项目所需的数学对象,通常以独特的方式描述这些对象。结果,Coq图书馆给人的感觉是杂乱无章,就像一座无规划的城市。

“CoQ现在已经是个老头了,它有很多伤痕,”马赫布比说,他曾广泛参与过这个项目。“随着时间的推移,它得到了许多人的共同维护,而且由于其悠久的历史,它也存在着众所周知的缺陷。”

2013年,一位名叫莱昂纳多·德莫拉(Leonardo De Moura)的微软研究员推出了Lean。这个名字反映了德莫拉希望创造一个高效、整洁设计的程序的愿望。他打算让这个程序成为检查软件代码准确性的工具,而不是数学。但事实证明,检查软件的正确性很像验证证据。

De Moura说:“我们创建精益是因为我们关心软件开发,而构建数学和构建软件之间存在着类比。”

当Lean问世时,有很多其他的证明助手可用,包括Coq,它与Lean最相似--这两个程序的逻辑基础都基于依赖类型理论。但精益代表着一个重新开始的机会。

数学家们很快就被它吸引住了。他们是这个项目的狂热拥护者,以至于他们开始把德·莫拉的时间花在专门针对数学的发展题上。“他对不得不管理数学家感到有点厌烦,于是说,‘你们做一个单独的储存库怎么样?’”莫里森说。

数学家在2017年创建了这个图书馆。他们称它为Mathlib,并急切地开始用世界上的数学知识填满它,使它成为一种21世纪的亚历山大图书馆。数学家们创造并上传了数字化的数学作品,逐渐为利恩建立了一个可供参考的目录。因为Mathlib是新的,他们可以从Coq这样的旧系统的局限性中学习,并额外注意他们是如何组织材料的。

麦克白说:“我们正在努力打造一个完整的数学库,其中所有的部分都能与所有其他部分协同工作。”

Mathlib的首页有一个实时仪表盘,显示了项目的进度。它有一个由顶级贡献者组成的排行榜,按照他们创建的代码行数进行排名。还有一份已经数字化的数学总量的最新统计:截至10月初,Mathlib包含了18416个定义和38315个定理。

这些都是数学家可以在精益课程中混合在一起组成数学的要素。目前,尽管有这些数字,但它只是一个有限的储藏室。它几乎不包含复杂分析或微分方程--许多高等数学领域的两个基本元素--的内容,它甚至不足以说明任何千年奖的问题,这是克莱数学研究所列出的最重要的数学问题。

但Mathlib正在慢慢充实起来。这项工作有一种谷仓抬高的感觉。在Zulip上,数学家识别需要创建的定义,自愿编写这些定义,并迅速提供对彼此工作的反馈。

麦克白说:“任何一位研究数学家都可以查看数学库,发现它遗漏了40件事。”“所以你决定填补其中一个漏洞。这真的是立竿见影的满足感。其他人会在24小时内阅读并发表评论。

今年夏天,里昂学院诺曼尔学院的索菲·莫雷尔在“好奇的数学家的学习”研讨会上发现,许多新增加的项目都是小规模的。(译者注:来自里昂诺曼尔学院的索菲·莫雷尔)在今年夏天举办的“好奇的数学家的学习”研讨会上发现了这一点。会议组织者给了与会者相对简单的数学陈述,让他们在精益实践中加以证明。在研究其中一个的过程中,莫雷尔意识到她的证明需要一个引理--一种简短的踏脚石结果--这是数学库所没有的。

“这是关于线性代数的一件非常小的事情,但不知何故,它还没有出现。”编写数学库的人试图做到透彻,但你永远不可能想得一清二楚。“莫雷尔说,她自己编写了这三行引理。

其他贡献更为重要。在过去的一年里,Gouëzel一直在为Mathlib定义“光滑流形”。光滑流形是空间--如直线、圆和球的表面--在几何学和拓扑学的研究中起着基础性的作用。它们也经常出现在数论和分析等领域的重大成果中。在没有定义数学研究的情况下,你不能指望做大多数形式的数学研究。

但流畅的流形有不同的伪装,这取决于背景。它们可以是有限维的,也可以是无限维的,既可以有“边界”,也可以没有边界,并且可以在各种数系上定义,例如实数、复数或p-进制数。定义光滑的流形几乎就像试图定义爱:当你看到它的时候你就知道了,但任何严格的定义都可能排除这种现象的一些明显的例子。

“对于一个基本的定义,你没有任何选择(如何定义它),”古泽尔说。但对于更复杂的物体,可能有10到20种不同的方法来形式化它。

古泽尔不得不在特殊性和概括性之间保持平衡。他说:“我的规则是,我知道15种我想要陈述的流形应用。”“但我不希望定义过于笼统,因为那样你就不能使用它了。”

他提出的定义填满了1600行代码,这使得数学库的定义相当长,但与它在Lean中释放的数学可能性相比可能微不足道。

“既然我们有了语言,我们就可以开始证明定理了,”他说。

在正确的概括性水平上为一个对象找到正确的定义,是构建数学库的数学家们的一个主要关注点。它的创建者希望以一种现在有用但又足够灵活的方式来定义对象,以适应数学家可能对这些对象进行的意想不到的使用。

麦克白说:“我们强调的是,所有的东西在未来都是有用的。”

但精益不仅仅是有用的--它为数学家提供了以一种新的方式投入工作的机会。麦克白还记得她第一次尝试打样助手的情景。那是2019年,项目是Coq(尽管她现在使用精益)。她爱不释手。

“在一个疯狂的周末,我每天花12个小时在上面,”她说。“这完全让人上瘾。”

其他数学家也以同样的方式谈论这一经历。他们说,在精益公司工作感觉就像在玩电子游戏--完全是那种基于奖励的神经化学冲动,让人很难放下遥控器。利文斯顿说:“你可以一天玩14个小时,一整天都不会感到疲倦和兴奋。”“你不断地得到积极的强化。”

尽管如此,精益社区认识到,对于许多数学家来说,没有足够的水平可供发挥。

谷歌(Google)工程师克里斯蒂安·塞格迪(Christian Szegedy)说,“如果你要量化多少数学是形式化的,我会说这远远不到千分之一。”他希望人工智能系统能够自动阅读和形式化数学教科书。

但数学家们正在提高这一比例。虽然今天Mathlib包含了本科二年级数学的大部分内容,但贡献者希望在几年内增加剩余的课程-这是一个重要的里程碑。

巴扎德说:“在这些系统存在的50年里,没有一个人说过,‘让我们坐下来组织一个连贯的数学体系,代表本科教育。’”“我们正在制作能够理解本科期末考试试题的东西,这是以前从未有过的。”

Mathlib可能需要几十年的时间才能拥有真正的研究库的内容,但精益用户已经证明,这样一个全面的目录至少是可能的--要做到这一点,只需在所有的数学运算中编程即可。

为此,去年德国弗莱堡大学的Buzzard、Massot和Johan Commelin进行了一个雄心勃勃的概念验证项目。他们暂时抛开本科数学的逐渐积累,跃居该领域的先锋。其目标是定义21世纪数学的伟大创新之一--波恩大学的彼得·肖尔茨在过去十年中开发出的一种名为完美拟态空间的物体。2018年,这项工作为肖尔茨赢得了菲尔兹奖,这是数学的最高荣誉。

Buzzard、Massot和Commelin希望证明,至少在原则上,精益能够处理数学家真正关心的那种数学。马赫布比说:“他们采用了一些非常复杂和最新的技术,并展示了在验证助手的帮助下,对这些物体进行研究是可能的。”

为了定义一个完美的拟态空间,这三位数学家必须将3000多个其他数学对象的定义和它们之间的3万个联系结合在一起。这些定义涉及数学的许多领域,从代数到拓扑学再到几何学。它们共同定义单个对象的方式生动地说明了数学是如何随着时间的推移变得越来越复杂的,以及为什么正确地奠定数学库的基础是如此重要。

麦克白说:“高等数学的许多领域都需要你在本科时学到的每一种数学。”

这三人成功地定义了一个完美拟态空间,但至少目前,数学家们还不能对它做太多的工作。精益需要更多的数学知识,才能提出完美拟态空间中出现的各种复杂问题。

马索特说:“利恩知道什么是完美拟人空间,却不知道复杂的分析,这有点荒谬。”

巴扎德对此表示赞同,他称完美拟人空间的正规化是一种“噱头”--这是一种新技术有时会表演的展示其价值的早期特技。在这种情况下,它起作用了。

“你不应该认为是因为我们的工作,地球上的每个数学家都开始使用证明助手,”马索特说,“但我认为他们中的相当一部分人注意到了这一点,并提出了很多问题。”

精益要真正成为数学研究的一部分还需要很长一段时间。但这并不意味着该节目如今只是科幻杂耍。忙于开发它的数学家们认为他们的工作类似于铺设第一条铁轨-这是一项重要努力的必要开始,即使他们自己可能永远也没有机会去兜风。

麦克白说:“这将是非常酷的,值得现在投入大笔时间。”“我现在正在投入时间,这样将来的某个人就可以拥有那种令人惊叹的体验。”

更正:2020年10月2日这篇文章的前一个版本错误地陈述了帕特里克·马索特所在的大学,因为它最近更名了。这篇文章已经做了相应的修改。