上一版
能自动做数学题的AI
数学家的梦之国在一个名为Zulip的线上论坛上，一群志同道合的数学家几乎每天都会聚在一起创造他们所坚信的“未来”。他们都是Lean这个软件程序的狂热信徒。原则上来说，Lean是一个“证明助手”，能帮助数学家完成证明过程。但是在Lean能独当一面之前，数学家们得亲自将数学输入到程序中，将积累了数千年的数学知识翻译成Lean能理解的语言形式。
“显然，当你将某个事物数字化后，你就可以通过新方式利用它了，”伦敦帝国理工学院的Kevin Buzzard说道，“（所以）我们要对数学进行数字化，让它变得更好。”
一直以来这都是数学家们的梦想。他们预期的好处既包括用计算机给学生作业打分、给期刊审稿、替代人力完成一项证明中冗长重复的细节等等这样平凡的任务，也包括利用人工智能来发现新数学领域、为旧问题找新解这样宏伟的目标。
但是首先，在Zulip上集结的数学家们必须给Lean提供相当于一个图书馆级别的大学数学知识，可他们现在只完成了一半。Lean短期内还不能解决开放性问题，但从事该项目的人几乎可以肯定，在几年内，这个程序将至少能理解大三期末考试题的数学问题了。
漫长的训练之路
为了训练Lean，他们把整个夏天都贡献了出去：一群经验丰富的Lean用户开设了一个名为“好奇数学家的Lean”线上研讨会。在第一部分，澳大利亚悉尼大学的Scott Morrison展示了如何在程序中完成一个证明过程。
他首先用Lean能理解的语言输入他想证明的定理。比如说，“素数无限定理”。现在有多种方法可以证明这个定理，但Morrison希望对公元前300年欧几里得发现的第一种证明方法进行微调。这种方法通过将已知的全部素数相乘后再加一形成新的素数对定理进行了证明。Morrison的选择反映出使用Lean的基本要求：用户不得不独立想出自己的办法。
在输入题目、选择完解题策略之后，Morrison花费了几分钟的时间展示证明的结构：他定义了一系列相对容易证明的中间步骤。虽然Lean无法找到一个证明的总体策略时，它常常能帮助执行小而具体的步骤。在将证明过程分割成可管理的子任务的过程中，Morrison有点像一个厨子，指挥着一线厨师切洋葱、然后慢炖出一道美食。Morrison指出，“到了这个节骨眼上，你就可以期待Lean接管大局成为‘掌厨’，开始提供真正的帮助。”
Lean通过使用称为“策略”的自动化流程来执行这些中间任务。而这些“策略”可以被当作用于执行特定工作的短算法。
证明过程中，Morrison通过运行“数据库搜索”（library search）的策略算法搜索库中的数学结果并反馈一些数学定理填补到具体的证明过程中。一种名为“linarith”的策略算法可以接收关于两个实数的不等式并确认有关第三个数的新不等式的正确性。例如：如果a等于2，而b大于a，那么3a+4b大于12。其他策略算法可将基本代数规则如结合率等进行应用。
Morrison总共用了20分钟来完成欧几里德的证明。他自己在一些地方添加了细节，而另一些地方则是策略算法帮他完成的。Lean对每一步都进行了检查来确保他的工作与程序潜在的逻辑规则一致。
“这如同一款数独App。如果你的某一步是无效的，那它就会出问题，”Buzzard评论道。最终，Lean证明Morrison的证明过程有效。
不过欧几里德的证明过程已经存在了两千多年。而数学家们目前关心的问题太复杂以至于Lean还不能理解问题，更别说为它们的解答过程提供支持了。
“很可能还得过10多年它才成为一个研究工具，”Lean用户，美国福特汉姆大学的Heather Macbeth认为。因此，Lean还需学习更多数学。这看似是个简单的任务——只需将数学课本翻译成Lean可以理解的形式就行了。但不幸的是，很多数学知识并
不存在于教科书中，所以这项工作并不简单。
散落的知识
事实上，高中和大学数学、甚至很多研究生学到的数学只是微不足道的一小部分。数学的绝大部分内容还不够系统化。大量重要的数学知识从未被详细完整地记录下来，它们只存在于少数人的头脑里，几乎是民间传说一样的存在。
还有一些领域，虽然基本材料记录完备，但内容过于庞大复杂，人们无法检查它们的正确性。然而，数学家们却对此信心十足。“我们相信作者的声誉。我们知道他是个认真的天才，那么他的证明或理论一定是正确的，”巴黎-萨克雷大学的Patrick Massot说。这也是为什么“证明助手”（计算机辅助证明）如此诱人的一个原因。将数学翻译成一种计算机能理解的语言鞭策着数学家们对知识进行最终分类和精确定义。
法国国家研究院的Assia Mahboubi意识到了这个数字化数据库的潜能，“我觉得很有趣。从理论上讲，一个人可以通过纯粹的逻辑语言，捕获全部数学文献，并在计算机中存储一个能够用程序检索和查证的数学语料库。”
前车之鉴
其实，Lean并不是第一个有这种潜能的程序。世界上第一个计算机辅助证明程序是上世纪60年代发行的Automath。而1989年发行的Coq则是目前使用最广泛的“证明助手”程序。
直到2013年，微软研究员Leonardo de Moura才创造了Lean。他本希望该程序可以成为检查软件代码准确性的工具，而非用于数学。但检查软件的准确性与数学证明所用的思路十分类似。
因此，数学家们很快被这个新程序所吸引。他们在数学领域上提出的扩展问题耗费了de Moura大量时间。据Morrison描述，忍无可忍的de Moura对数学家们说，“你们这群家伙为什么不创建一个单独的数据存储库？”
于是，数学家们在2017年创建了名为mathlib的数据库并开始迫切地向其中填补世界上的数学知识，努力将它打造成21世纪的亚历山大图书馆（曾拥有西方世界最丰富的古籍收藏）。他们创建并上传了许多数字化的数学知识片段，逐渐构造出一个供Lean参考的目录。新构建的mathlib得以让数学家们从Coq等旧系统的局限性中吸取教训并学会留意对材料的组织方式。
最大的数学图书馆
Mathlib的首页可以显示项目进展的实时数据，还记录着已被数字化的数学知识总量。2019年10月时，Mathlib已经包含18416条定义和38315个定理。
利用Lean，数学家们可以将这些原料混合在一起创造新的数学知识。不过现在，mathlib还只是个有限的“原料储存室”。它几乎不包含高等数学多个领域常用的复杂分析和微分方程的内容，甚至无法陈述出任何一个美国克雷数学研究所（CMI）提出的千禧年大奖难题。
但是它在慢慢填补着知识空白。在Zulip上，数学家们不停地标示出需要创建的定义，并且自愿编写它们并及时为彼此的工作提供反馈意见。
“任何一个数学研究者在mathlib上都能发现几十个需要补充的定义或定理，”Macbeth说，“所以你决定填补这些漏洞。这能带来即时满足感。别人看到后会在24小时内评论。”
2020年夏天的研讨会上，法国里昂高等师范学院的Sophie Morel发现很多补充内容都是一小部分。作为练习，会议组织者给参与者提供了一些相对简单的数学陈述让他们使用Lean证明。在思考其中一个问题是，Morel意识到她的证明需要用到一个mathlib没有收录的引理（为了取得某个更好的结论而作为步骤被证明的命题）。于是，她就自己给这个引理写了三行代码。
当然，也有一些重量级的贡献。2019年，Gouzel在为mathlib研究几何学和拓扑学中有重要作用的“光滑流形”的定义。他认为，虽然基础定义只有一个，但对于更复杂的对象，可能有10到20种不同的方式使其形式化。为了在特殊性和普遍性中间找到平衡，他最后写出了1600行代码。
给收录对象在普遍性水平上找到合适的定义，无疑是构造mathlib的数学家们的主要工作。他们希望现在的研究对将来都有用。
通往真正的数学研究之路
为了证明Lean能够处理数学家们真正关心的问题，德国弗赖堡大学 的Buzzard，Massot和Johan Commelin在2019年开始了一项宏伟的概念证明项目。目标是给21世纪数学界最伟大的发明——完备空间做一个数字化定义。
他们将三千多个其他数学对象的定义与它们之间存在的三千多个联系相结合。这些定义涉及多个数学领域，从代数到拓扑再到几何。它们被逐步整合成一个单一对象的定义，这个过程生动地展现出数学是如何随时间变得越来越复杂的，也表明了正确奠定mathlib的基础有多么重要。
最终，他们成功进行了概念证明，定义了完备空间。不过，要确切表达完备空间中出现的数学问题，Lean还有很多知识需要学习。
虽然Lean成为真正的数学研究工具还需漫长的时间，但这并不意味着这个程序是个不可实现的概念。数学家们正努力在数学数字化的路上铺设第一条铁轨，虽然他们可能没有机会亲自搭乘最终跑起来的那班列车。（王千玥）