【原】小乐数学科普：人机合作加速数学研究

zzllrr小乐 2023-10-25 发布于江苏

展开全文

本文作者是苏珊·达戈斯蒂诺（Susan D'Agostino），哥伦比亚大学数学家和科普作家[21]（撰稿日期：2023-9）

有人可能会认为，获得菲尔兹奖以后，可以平息任何数学家对他们继续往前写证明的能力的唠叨怀疑。但在彼得·舒尔茨（Peter Scholze）获得2018年奖项后不久，[1] 他质疑他与达斯汀·克劳森（Dustin Clausen）合著的液体向量空间定理（liquid vector space theorem）证明的一部分。于是舒尔茨谦虚地向数学界求助。

“我在2019年的大部分时间里都沉迷于这个定理的证明，几乎为之疯狂，”舒尔茨在2020年12月Xena Project博客上写道关于证明中包含的泛函分析（functional analysis）黑匣子。[2] “我认为没有人敢看这个细节，所以我仍然有一些挥之不去的小疑问。...这可能是我迄今为止最重要的定理......最好确定它是正确的。”

事实上，阿尔伯塔大学数学助理教授亚当·托帕兹（Adam Topaz）紧张地笑着承认，他和他的研究小组在2020年阅读该定理时跳过了该定理的证明。

“他是一个非常有说服力的人，”Topaz在2023年2月加州大学洛杉矶分校（UCLA）的纯数学与应用数学研究所举行的机器辅助证明会议中的一次演讲中说[3]。“如果他说什么是正确的，人们往往会倾向于相信他。”

这就是为什么舒尔茨和由德国弗莱堡大学的Johan Commelin领导的团队启动了一个大型合作项目，使用免费开源的Lean证明助手来验证证明。这个由社区驱动的软件主要由莱昂纳多·德·莫拉（Leonardo de Moura）在微软研究院工作时提供的[4]，并得到Lean社区建立的数学库的支持。托帕兹和其他数学家以及计算机科学家加入Commelin的费力尝试。根据Topaz的说法，到 2021年5月，他们达到了第一个目标，而到2022年7月，他们完成了需要98000行代码的项目。

“我觉得交互式证明助手，现在处于可以在非常合理的时间跨度内正式验证困难的原创研究的水平，这绝对是疯狂的，”舒尔茨在他的博客上写道。

Topaz说，如果没有机器的帮助，仔细检查证明将是“不可能开始的”（nonstarter）。作为发现和修复一些不准确之处并验证主定理证明的奖励，Topaz说该小组还证明了一些辅助陈述，回答了舒尔茨注记中的一些问题，并填补了Lean数学库中的一些空白，特别是在同调代数（homological algebra），拓扑（topology）和范畴论（category theory）方面。

“这真的是一个人类项目，而不是一个机器人项目，”Topaz说。

自2022年底以来，学术界一直在谈论ChatGPT、GPT-4 和其他可能改变研究和大学写作的人工智能AI写作工具。但数学界也在努力应对颠覆，正如人机合作在数学研究的最前沿编写困难定理的证明所辅助所做。机器不仅验证人类发现的数学结果，还帮助数学家推理，探索新想法，甚至学习新的数学。

自动化和交互式方法

形式方法是计算机科学的一个子领域，它使用基于计算逻辑的技术来协助数学推理，卡内基梅隆大学哲学和数学科学教授杰里米·阿维加德（Jeremy Avigad）表示。在子领域中，有自动化方法和交互式方法。广义上讲，使用前者，一个人问一个问题，按下一个按钮，然后得到一个答案——或者得到一个“我不知道”，这可能会让数学家陷入困境。使用后者，用户与计算机一起探索或检查推理。这为可能性留下了空间。

“现在还为时过早，我们仍在弄清楚这项技术可以做什么，”Avigad说。“但有很多希望和兴奋点。”

当数学家与交互式证明助手一起工作时，他们可能会通过输入基本定义和定理来“教”会计算机数学的新领域。他们以后可能会“询问”机器对这些对象的了解。在形式化证明时，他们将尝试让计算机确定是否遵循先前的陈述，并在必要时提供更多信息。通过这种方式，人机合作填充细节并推进尝试走向严格化。

但是根据Avigad的说法，区分自动化和交互式方法是一种错误的二分法（dichotomy）。

“即使你正在交互式地做数学，你也希望尽可能自动化繁琐的部分，”Avigad说。“即使你正在使用自动化，每当你尝试一些不起作用的东西时，你也会做出改变并重试。所以，这个领域的两方面共同成长。

丹佛大学数学教授迈克尔·金尼恩（Michael Kinyon）在使用工具时也模糊了这一界限。也就是说，他使用自动定理证明器，但他将它们用作证明助手。这项工作改变了他对研究问题的方法。

“我们可能会更快一些，例如，先使用该软件尝试一些东西，然后再坐下来凝视空白并试图自己弄清楚，”Kinyon说。“在这些事情的早期阶段，人们更愿意进行实验。”

一些人认为，计算机的“思考”方式与人类不同，促进了人类的发现过程。

“这打破了我们的模式，加深了我们的理解，”威斯康星大学数学教授乔丹·艾伦伯格（ Jordan Ellenberg）说。“你可以把形式化看作是向机器传授数学思想，而机器的'思维’与我们的非常不同。”2016年，Ellenberg和荷兰代尔夫特理工大学数学教授迪恩·吉斯韦特（Dion Gijswijt）解决了杯盖集猜想（cap set conjecture，cap set为仿射几何中的术语[19] [20]，这里cap暂译为杯盖∩，与英语中的cup杯子∪相对，zzllrr小乐译注），这一结果后来发表在[5]《数学年鉴》中。

后来，在2019年，数学家Sander Dahmen和来自阿姆斯特丹自由大学的计算机科学家Johannes Hölzl和Robert Lewis使用Lean定理证明器来形式化Ellenberg和Gijswijt定理的证明[6]。作者认为，与其他数学子领域的证明相比，形式化证明所必需的组合背景“不那么令人生畏”。这种形式化工作提供了一些保证，即在有利的情况下，人们可以通过计算机检查《数学年鉴》最近的一篇论文。但是，在这本受人尊敬的期刊中，只有极少数论文包含具有“不那么令人生畏”的先决条件的简短证明。热心者可以希望该软件会随着时间的推移而改进。

事关优雅

有些人可能想知道机器是否将证明简化为计算。但福特汉姆大学数学助理教授希瑟·麦克白（Heather Macbeth）认为，这种还原主义并不是这项工作的核心。这是因为人类为了理解编写证明，而计算可能无法提供这一点。

“你可能会认为，当你从纸张转向计算机时，我们把[美]扔出窗外，我们已经决定我们将拥抱功能而不是形式，我们真的要走向一个完成证明很重要的世界，”麦克白说。“那倒不是。”（麦克白在纯数学与应用数学研究所会议上的发言）。

麦克白花了三年时间编写了数千行Lean代码，以努力使证明形式化。两年来，她还与其他人合作维护Lean数学库。在这个角色中，她审查了其他人编写的数千行代码，以评估代码是否可以改进，并确保它适合库的其余部分。

“我觉得其中一些真的很美，有些我不觉得，”麦克白说。“几乎所有在纸上写的好数学的原则都延伸到形式数学中的相应原则。”

根据麦克白的说法，自动证明中包含的论证并不总是模仿人类思维模式。

“尽管如此，有一个很好的证明，并不完全是人类会想到的，”麦克白说。她观察到，为了提高效率，人类可能会在寻找证明的不同步骤中修剪搜索空间。然而，机器可能会检查更多的情况，包括那些最初看起来不太有希望的情况。

“这实际上是一个关于存在差异以及为什么这些差异很有趣的问题，”麦克白说。

此外，一些证明在形式化过程中变得优雅。托马斯·布朗宁（Thomas Browning）和帕特里克·卢茨（Patrick Lutz）都是加州大学伯克利分校（University of California，Berkeley——UCB）的数学研究生，他们努力将伽罗瓦理论形式化——这是一个许多人已经认为很优雅的子领域。但是在他们工作的某个时刻，他们需要使用任意的有限序列，根据Browning和Lutz的说法，这不是Lean的优势。因此，他们找到了解决方法。

“这种策略主要只是为了避免处理某些类型的论证，这些论证在Lean中不能很好地进行，”Browning和Lutz在他们的论文中写道。“但它确实有一个额外的好处，即当使用这种新的归纳原理重写时，一些标准证明会变得更简单。”

加速的趋势

几十年前，机器辅助证明被主流数学家视为边缘项目，布拉格捷克信息学、机器人和控制论研究所的杰出研究员约瑟夫·厄本（Josef Urban）表示。

“知名数学家说，像汤姆·黑尔斯（Tom Hales）这样的人通过正式证明开普勒猜想来浪费他们的才能，”Urban谈到这位数学家时说，他在通常裁判过程的挫败感反应之后，提供了一个机器验证的证明。“在过去的15年里，这种情况真的发生了变化，这尤其要归功于Hales。”

可以肯定的是，机器辅助证明仍然有反对者，包括哥伦比亚大学数学教授迈克尔·哈里斯（Michael Harris）。使用定理证明器的数学家必须学会用计算机理解的术语编码和表达问题，这减少了花在数学上的时间。

“在我将我的问题重新构建成一种可以适应这项技术的形式前，我会自己解决问题，”哈里斯告诉量子杂志[7]。

罗格斯大学（Rutgers University）数学教授多伦·泽尔伯格（Doron Zeilberger）也不是机器证明的粉丝，尽管他的厌恶始于人类编写的证明，并延伸到机器辅助证明。

“我们不需要人类生成的数学的更多'正式版本’，”去年当注意到对Avigad 和其他人的开创性工作的赞赏时，Zeilberger在他的博客上写道[8]。“形式化已知的证明与倒读隐语（Pig-Latin）没有什么不同。一旦你做了几次，它就不再有趣了。虽然这在智力和技术上都具有挑战性，否则这些聪明的人不会参与其中，但这些人正在浪费他们的才能。”

“事实上，我们的硅仆人，即将成为我们的主人，可以更有成效地使用，”Zeilberger继续说道。“Coq（另一个交互式定理证明器）和Lean延续了有害的希腊传统，它引入了公理化方法，使数学成为演绎的、以逻辑为中心的科学。”

但这些观点似乎与人工智能的顶头风背道而驰，人工智能的顶头风似乎正在推动当前社会的发展，包括数学界。

伦敦帝国理工学院纯数学教授凯文·巴扎德（Kevin Buzzard）在 2022年国际数学家大会上作了演讲，“数学中形式主义的兴起”[9][23]。在那里，他将情绪称为不是“结束的开始”，而是“开始的开始”。在他看来，数学研究人员的工作没有风险。然而，机器将越来越多地帮助人类证明数学定理，不仅通过找出例子，而且通过推理。根据Buzzard的说法，计算机还将帮助人类在数据库中找到证明或反例，构建简单的证明，并且通常使人类更容易学习数学。

巡回会议似乎支持这一说法。除了二月份在纯粹与应用数学研究所举行的机器辅助证明会议外，其他可敬的机构今年也投入时间和空间让数学家聚集在一起讨论这一加速的趋势。

5月，班夫国际数学创新与发现研究站（Banff International Research Station for Mathematical Innovation and Discovery）举办了上同调理论形式化（Formalization of Cohomology Theories）研讨会[10]，这汇集了形式化专家和学科专家，朝着前沿研究迈进。6月，西蒙斯·劳费尔数学科学研究所（Simons Laufer Mathematical Sciences Institute）在数学形式化暑期研究生院课程中向研究生介绍了其背后的技术和思想[11]。7月，麻省理工学院洛仑兹中心举办机器检查数学研讨会[12]，针对那些听说过但尚未尝试这项技术的数学家。

在美国以外，哥本哈根大学在6月举办了一个大师班[13]，称为数学的形式化，以建立舒尔茨的液体张量实验。7月，荷兰洛伦兹中心提供[14]机器检查数学，为期一周的入门研讨会，面向感兴趣的数学家，旨在促进合作。同样在夏天，豪斯多夫数学研究所提供了一个计划[15]，形式数学的前景，为专家和初级研究人员提供一个论坛，让他们聚集、合作，并“更好地将他们与数学主流联系起来”。9月，该机构提供[16]为期一周的系列讲座[17]，形式数学和计算机辅助证明。更多内容可以在Lean社区网站上找到[18]。此外，Lean并不是唯一的交互式定理证明器。根据Buzzard的说法，其他系统包括Coq，Isabelle / HOL，HOL Light，Agda，cubical Agda，Metamath和Mizar。

“他们数字化了音乐 - CD，MP3 - 但当时没有人预见到后果是 - Napster，Spotify，”Buzzard在演讲中说。“我们正在将数学数字化，我相信这将不可避免地改变数学。欢迎您加入我们。”

参考资料

https://www./science/Fields-Medal

https://xenaproject./2020/12/05/liquid-tensor-experiment/

https://www.ipam./programs/workshops/machine-assisted-proofs/?tab=schedule

https://leanprover-community./

https://annals.math./2017/185-1/p08

https://drops./opus/volltexte/2019/11070/

https://www./how-close-are-computers-to-automating-mathematical-reasoning-20200827/

https://sites.math./~zeilberg/Opinion184.html

https://www./watch?v=SEID4XYFN7o

https://www./events/2023/5-day-workshops/23w5124