一个小型的数学家社区正在使用精益来建立新的数字基础。他们希望这将确保他们科学领域的未来。
每天，数十位志同道合的数学家在Zulip聊天中相聚，共同致力于塑造他们科学领域的未来。
他们都是精益计划的粉丝。它是一个交互式定理证明工具，从原理上讲，它可以帮助数学家编写证明。但是，为此，数学家必须将数学规则手动输入到程序库中，从而将数千年来收集的知识转化为计算机可以理解的形式。
对于该项目的许多参与者而言，其收益几乎是不言而喻的。凯文·巴扎德（Kevin Buzzard）
表示：“从根本上讲，一旦数字化了，就可以以新的方式使用它了。”来自伦敦帝国学院。“而且我们将数字化数学，使其变得更好。”
数学数字化是一个古老的梦想。预期的好处从琐碎的工作-用计算机检查学生的功课到非凡的工作：使用人工智能进行新的数学发现并找到解决旧问题的新方法。数学家认为，自动定理证明者还将能够审阅提交给期刊的文章，发现人类审稿人有时会遗漏的错误，并从事繁琐的技术工作，即用所有必要的细节填写证明。
但是首先，在聊天室中开会的数学家需要在学校数学框架内为精益知识配备知识，而到目前为止，这项任务仅完成了一半。在不久的将来，精益不可能解决开放性问题，但是在基地工作的人们几乎可以肯定，该计划将在短短几年内至少学会了解高中的考试水平问题。
谁知道？参与该项目的数学家并不总是清楚数字数学可以做什么用。雷恩大学的塞巴斯蒂安·古瑟尔（SebastienGösel）
说：“我们不知道确切的去向。”
你计划，精益工作
在夏季，一群经验丰富的精益用户举行了在线研讨会“好奇数学家精益”。在第一课中，悉尼大学的Scott Morrison展示了如何使用程序编写证明。
他首先写下了他想用精益论证的陈述。在人类语言中，它的意思是“质数无穷”。有多种方法可以证明这一说法，但莫里森想使用由欧几里得从公元前300年发现的第一批证据的略微修改版本。在证明中，将所有已知的质数相乘，然后在加1后获得一个新的质数（乘积本身或其除数之一将是质数）。莫里森的选择基于使用精益的基本规则之一：用户必须自己提出证明的主要思想。
莫里森在一次采访中说：“你应对第一个猜测负责。”
输入断言并选择策略后，Morrison在几分钟内概述了证明的结构。他确定了一系列中间步骤，每个步骤都相对容易证明。尽管精益不能提供通用的证明策略，但它可以帮助您执行小的，具体的步骤。将证明分解为可访问的子任务，Morrison有点像厨师指示普通厨师切碎洋葱或烧开水。 “这是您希望精益管理能够接手并帮助您的地方，”莫里森说。
精益使用称为战术的自动化流程来完成中间任务。这些是设计用于执行非常具体的任务的简短算法。
借助证据，Morrison发起了一种称为图书馆搜索的策略。她梳理了该程序的数学数据库，并返回了一些定理，她认为这些定理可以弥补证明中特定部分的空白。不同的策略执行不同的数学任务。其中一个，linarith，可以为例如两个实数取一组不等式，并确认新不等式的真相，其中包括第三个数：如果a为2且b大于a，则3a + 4b大于12。另一个则执行大多数使用基本的代数规则，例如关联性。
“两年前在精益技术中，必须手动应用关联性，”伦敦帝国理工学院的数学系学生，正在与巴扎德一起学习精益技术的阿米莉亚·利文斯顿说。 -然后有人写了一个为您做的战术。每次使用我都会感到高兴。”
莫里森总共花了20分钟才能完成对欧几里得的证明。他到处都亲自完成了细节。有时候，战术家为他做了。每一步骤之后，Lean都会根据以称为依赖类型理论的形式语言编写的内置逻辑规则，检查证明的一致性。
“它看起来像Sudoku应用程序。 “如果您采取了错误的举动，它会发出哔声，”巴扎德说。结果，精益证实了莫里森的证明有效。
这是一个非常有趣的练习-通常情况下，技术可以为您效劳。但是，欧几里得的证明已经存在了2000多年。当今的数学家的问题是如此复杂，以至于精益甚至无法理解这些问题，更不用说帮助他们回答了。Lean的用户之一，福特汉姆大学的Heather Macbeth
说：“这个工具可能需要数十年的时间才能帮助研究。”
因此，在数学家可以与Lean合作解决他们真正感兴趣的问题之前，他们必须向程序中添加更多数学规则。实际上，这是一个相当简单的任务。
证明构建程序的剖析：精益帮助数学家通过验证工作并自动执行证明中的某些步骤来证明定理。
1）数学家描述证明的基本结构，并写下精益中的步骤顺序。
2）数学程序的mathlib库具有执行该证明步骤的一组策略。数学家一直在向mathlib添加新数据。经证明的定理已添加到mathlib中。
3）内核算法使用简单的规则检查证明的正确性。
*章鱼在某种程度上已成为精益社区中愉悦情绪的代名词。
“为了使精益能够理解某些东西，人们需要将数学教科书翻译成程序可以理解的形式，”莫里森说。
不幸的是，问题的简单性并不意味着它很容易完成-鉴于教科书中并未涵盖许多数学运算。
分散的知识
如果您还没有学习过高级数学，那么这方面可能看起来很准确，并且对您的描述很好。代数，微积分，数学分析-一切都源于一切，教科书末尾列出了所有问题的答案。
但是，学校课程，大学课程甚至大学的大部分课程中的数学仅占全部知识的很小一部分。他们大多数人组织得不好。
在数学领域有巨大而重要的领域没有得到充分描述。它们存储在少数人的头脑中，这些人从人们那里学习数学的子领域，从发明它的人们那里学到的东西-也就是说，它们是基于民间传说而存在的。
在其他地方还记录了基本材料，但是它非常复杂且冗长，以至于没有人能够验证其正确性。相反，数学家只是相信他。
“我们依靠作者的声誉。巴黎萨克莱大学的帕特里克·马索特（Patrick Massot）说：“我们知道他是一个天才和一丝不苟的人，因此证明很可能是真的。
这就是定理证明程序如此吸引人的原因之一。将数学转换成计算机可以理解的语言，迫使数学家最终对他们的知识进行分类并精确定义所有对象。
阿西亚·马布比（Assia Mabubi）法国国家信息与自动化研究所的研究人员回忆起她第一次意识到这样一个有序的数字图书馆的潜力：“我被使用纯逻辑语言对所有数学文献进行理论覆盖，将整个数学图书馆存储在计算机中，在其中检查和搜索数据的可能性深深地吸引住了我。借助程序”。
精益不是第一个具有这种潜力的程序。第一个是Automath，它出现在1960年代，而今天最流行的之一是Coq，它出现在1989年。Coq用户使用程序语言对许多数学进行了形式化，但是这项工作是分散的并且组织得不好。数学家仅在他们感兴趣的项目上工作，并且仅识别他们自己的工作所需的那些对象，通常以独特的方式描述它们。结果，Coq的图书馆看上去很杂乱，就像一个自然发展的城市的蓝图。
“ Coq如今是个有伤痕的老人，”积极参与该计划的Mabubi说。 “他得到了很多人的长期支持，由于他悠久的历史，他的缺点现在众所周知。”
2013年，微软研究员Leonardo de Mura启动了精益项目。它的名称[lean]反映了de Moore想要创建一个高效，干净的程序的愿望。他认为该程序将是检查其他程序代码准确性的工具，而不是数学工具。但是，事实证明，检查程序的正确性与检查证明非常相似。
“我们创建Lean是因为我们对软件开发感兴趣，并且在创建数学和编写代码之间有一个类比，” de Moore说。
精益用户之一，福特汉姆大学的希瑟·麦克白
在精益发布之时，还有很多其他帮助程序，包括与精益最相似的Coq。这两个程序的逻辑基础都是基于依赖类型的理论。但是，精益提供了一个重新开始的机会。
她很快吸引了数学家。他们热情地使用它，以至于他们开始将de Moore的所有空闲时间用于有关数学领域发展的问题。 “他对顶尖的数学家有些厌倦，并说-你们为什么不建立一个单独的存储库？”莫里森说。
数学家于2017年创建了这个库。他们称其为mathlib，并热心着手用世界数学知识填充它，从而创建类似于亚历山大图书馆的类似物。在二十一世纪。数学家创建并上传了数字化数学摘要，并逐渐为精益创建了目录。而且由于mathlib是新的，因此他们可以从过去的系统（例如Coq）的局限中学习，并跟踪材料的组织方式。
麦克白说：“有意创建一个整体的数学库，其所有片段都可以相互配合。”
亚历山大Mathlib
该mathlib项目主页有图，显示实时项目的进展情况。该项目列出了投资最多的领导者名单，按代码行数排序[首先，是俄罗斯数学家Yuri Kudryashov /大约。翻译]。还计算了数字化数学对象的总数：10月初，它包含18,756个定义和39,157个定理。
可以将所有这些数学成分混合在一起，以在精益中创建数学。到目前为止，尽管看似令人印象深刻的数字，但它们的范围受到严重限制。复杂分析或微分方程领域几乎没有任何东西-这是许多高等数学领域的两个基本要素。此外，该程序还不够了解甚至无法描述任何千年问题-克莱数学学院在2000年将数学问题定义为“多年未解决的重要经典问题”。
mathlib正在缓慢但肯定会进行填充。这项工作本着团队合作的精神进行。在Zulip聊天中，数学家选择定义进行形式化，要求他们将其写下来，并提供对他人工作的及时反馈。
麦克白说：“任何研究数学家都可以学习mathlib并列出40种不存在的东西。” -因此，他决定弥补所有这些缺点。而且保证了即时的愉悦-有人会在24小时内阅读您的作品并发表评论。”
正如Sophie Morel发现的那样，许多附件很小来自里昂师范大学的在线研讨会“好奇的数学家精益”。会议组织者给与会人员相对简单的数学陈述，以在“精益”实践中得到证明。与其中之一合作，Morel意识到她的证明需要一个引理-一个小的中间结果-在mathlib中找不到。
“这是线性代数的一小部分，由于某种原因，它还不存在。填充mathlib的人员试图掌握所有内容，但是您无法预见所有选项，”莫雷尔说，他自己将所需引理输入三行。
其他贡献更为重要。去年，Gösel一直在为mathlib定义平滑流形。光滑流形是在几何和拓扑研究中起基本作用的组（例如直线，圆或球的表面）。它们通常在诸如数论和微积分等领域的问题中也起重要作用。没有它们，大多数数学研究是不可能的。
但是，平滑的歧管可以隐藏在不同的外观下-一切都取决于上下文。它们可以具有有限或无限数量的尺寸，可以有边界也可以不具有边界，可以在各种数字系统上定义-在实数，复数或p-adic集合上数字。定义平滑的多样性就像定义爱：当您遇到爱时，您就会认识到它，但是任何严格的定义肯定会丢弃这种现象的一些最明显的例子。
“定义基本事物时，您不必做出任何选择，”Gösel说。 “但是更复杂的对象可以用10-20种不同的方式形式化。”
Gösel需要在特异性和泛化性之间保持平衡。他说：“我有一条规则-我希望能够定义流形的15种不同用途。” “同时，我不希望定义过于笼统，否则将无法使用它。”
他开发的定义适合1600行代码-对于mathlib的定义来说，这是很多，但与他向Lean提出的所有数学可能性相比，可能就不那么多了。
他说：“现在我们有了所需的语言，我们就可以开始证明定理。”
找到具有普遍性的对象的正确定义是填补mathlib的数学家的主要职业。该库的创建者希望以一种当今有用的方式来定义对象，同时又要具有足够的灵活性以至于可以以当今无法预测的方式来使用这些对象。
麦克白说：“强调了对在遥远的将来有用的一切需求。”
Perfectoid是从实践中诞生的
但是精益不仅是一种有用的工具，它还为数学家提供了重新参与工作的机会。麦克白仍然记得她第一次尝试使用程序来帮助编写证明。那是2019年，该计划是Coq（尽管现在已转换为精益）。她停不下来。
她说：“在一个疯狂的周末，我连续12个小时与该计划合作。” “那真是上瘾。”
其他数学家也以类似的方式描述他们的经历。他们说，精益就像一个电脑游戏-归因于相同的奖励荷尔蒙，这使得很难将游戏控制器放在一边。利文斯顿说：“您一天可以这样做14个小时，而不会整天感到疲倦和处于紧张状态。” “您一直都得到积极的反馈。”
SebastienGösel
然而，精益社区了解到，对于许多数学家来说，他们的课程根本没有足够的水平。
Google致力于AI系统的Google程序员克里斯蒂安·塞格迪（Christian Szegedi）表示：“如果量化形式化数学的百分比，我说还不到百分之一。”他梦想着能够独立阅读和形式化数学教科书。
但是数学家正在增加这个百分比。如果今天mathlib包含大学二年级教授的大多数材料，则项目团队希望在几年内增加该计划的其余部分-这将是一项重大成就。
“在所有这些系统的50年中，没有人提出建议：让我们坐下来组织一个一致的数学知识库，描述研究所的材料，”巴扎德说。 “我们正在创造一种可以理解学院考试问题的东西-以前从未发生过。”
mathlib的内容与研究库匹配可能需要数十年的时间，但精益用户至少证明了创建此类目录的理论可能性-要实现这一目标，仅取决于以程序代码形式输入数据库中的所有数学。
为此，去年，德国弗莱堡大学的Buzzard，Masso和Johan Kommelin实施了一个项目，证明了这一梦想的可行性。他们暂时推迟了基地材料的逐步填充，并转移到高级地区。他们的目标是确定21世纪数学上最伟大的创新之一-例如波恩大学的Peter Scholze在过去十年中开发的“完美空间” 。 2018年，他因其工作获得了菲尔兹奖，这是数学领域的最高奖项。
Buzzard，Masso和Commelin希望证明，至少在原理上，精益可以与数学家真正感兴趣的数学一起工作。 “他们采用了非常复杂和新颖的技术，并表明可以使用帮助编写证明的程序来操纵这些对象，”马布比说。
凯文·巴扎德（Kevin Buzzard）
要定义一个完美的空间，三位数学家需要结合3,000多个数学对象的定义以及它们之间的30,000个连接。从代数到拓扑和几何，定义已经延伸到许多数学领域。将它们放在一起定义一个有力的证明，随着时间的推移，数学的复杂性不断增长-以及为什么正确建立mathlib的基础如此重要。
麦克白说：“许多高级数学领域要求您了解教给学生的各种数学。”
三位一体已成功定义了完美空间，但到目前为止，数学家对此几乎无能为力。在程序至少可以公式化出现这些完美类空间的那些复杂问题之前，需要将更多的数学定义引入精益。
Masso说：“精益知道什么是完美的空间，却不知道复杂的分析，这真是愚蠢的。”
伯扎德对此表示同意，称完美样态空间的形式化是“ gi头”，这是新技术有时表现出的技巧，以证明其有用性。这次这招成功了。
马索说：“您不必认为，由于我们的工作，地球上的所有数学家都开始使用程序来帮助编写证明，但我认为其中许多人已经注意到了这种可能性，并开始提出问题。”
精益成为数学研究的真正组成部分还需要很长时间。但是，这并不意味着今天的程序是科幻小说的图画。参与其开发的数学家将他们的工作与铺设第一条铁轨进行了比较，这是重要企业的必要开端，即使他们自己可能无法驾驭。
麦克白说：“这将是一件很酷的事情，今天值得付出麻烦。” “我现在在她身上投入时间，以便将来某人可以和她一起工作，获得如此美妙的体验。”