分享:

通往真正的数学研究之路:AI 助力数学运算

2021-04-13 16:43:25 中国航空报 王千玥

index.jpg

数学家的梦之国在一个名为Zulip的线上论坛上,一群志同道合的数学家几乎每天都会聚在一起创造他们所坚信的“未来”。他们都是Lean这个软件程序的狂热信徒。原则上来说,Lean是一个“证明助手”,能帮助数学家完成证明过程。但是在Lean能独当一面之前,数学家们得亲自将数学输入到程序中,将积累了数千年的数学知识翻译成Lean能理解的语言形式。

“显然,当你将某个事物数字化后,你就可以通过新方式利用它了,”伦敦帝国理工学院的Kevin Buzzard说道,“(所以)我们要对数学进行数字化,让它变得更好。”

一直以来这都是数学家们的梦想。他们预期的好处既包括用计算机给学生作业打分、给期刊审稿、替代人力完成一项证明中冗长重复的细节等等这样平凡的任务,也包括利用人工智能来发现新数学领域、为旧问题找新解这样宏伟的目标。

但是首先,在Zulip上集结的数学家们必须给Lean提供相当于一个图书馆级别的大学数学知识,可他们现在只完成了一半。Lean短期内还不能解决开放性问题,但从事该项目的人几乎可以肯定,在几年内,这个程序将至少能理解大三期末考试题的数学问题了。

index (5).jpg

漫长的训练之路

为了训练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可以理解的形式就行了。但不幸的是,很多数学知识并

不存在于教科书中,所以这项工作并不简单。

责任编辑:助理编辑

相关新闻
关键词:
数学家,AI,运算