陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

释放双眼,带上耳机,听听看~!
了解陶哲轩最新发起的众包数学研究项目,探讨AI辅助证明数学研究的可行性,以及证明辅助语言在数学研究中的应用。了解如何利用众包和自动化工具进行数学探索,以及对现代数学问题的探索和评估。

【新智元导读】最近,陶哲轩向广大网友和数学爱好者发起了挑战:大众数学爱好者、证明助理、自动化助手和AI联合起来,是否可以证明扩展几个数量级的数学问题?

想参加陶哲轩发起的「众包」数学研究项目吗?

机会来了!

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

AI辅助证明数学研究,越来越可行了

在传统上,一个数学研究项目通常是由1到5名数学专家来完成的。

他们每个人都对项目的各方面都足够熟悉,可以验证彼此的贡献。

但如果要组织起更大规模的数学研究项目,特别是涉及公众贡献的项目,就麻烦多了。

原因在于,很难验证所有人的贡献。

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

2023年底,陶哲轩宣布:将多项式Freiman-Ruzsa猜想的证明形式化的Lean4项目,在三周后取得了成功(图为最新状态)

要知道,在数学论证某个部分中的单个错误,可能就会使整个项目失败。

而且,以一个典型数学项目的复杂程度来说,期待具有本科数学教育水平的公众做出有意义的贡献,也是不现实的。

由此我们也可以知道,把AI工具纳入到数学研究项目中,也是极有挑战性的。

因为AI会生成看似合理但实际上毫无意义的论证,因此需要额外验证,才能将AI生成的部分添加到项目中。

好在,证明辅助语言(比如Lean)提供了潜在的方法,能够克服这些障碍,并且让专业数学家、广大公众和AI工具的合作成为可能。

这种方法的前提是,项目可以以模块化的方式分解成更小的部分,这些部分可以在不必理解整个项目的情况下就能完成。

目前的例子主要有将现有数学结果形式化的项目(比如对Marton最近证明的PFR猜想的形式化)。

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

这些形式化工作,主要是通过众包方式由人类贡献者(包括专业数学家和感兴趣的公众)完成的。

同时,还有一些新兴的尝试,试图引入更多的自动化工具来完成,后者包括传统的自动定理证明器,以及更现代的基于AI的工具。

探索全新数学问题,成为可能

并且,陶哲轩还认为,这种全新范式不仅可以用于形式化现有的数学,还可以用来探索全新的数学!

过去,他曾经和继任组织过一个在线协作「Polymath」的项目,就是一个很好的例子。

不过,这个项目没有将证明辅助语言纳入工作流,贡献就必须由人类主持人管理和验证,这项工作非常耗时,也限制了将这些项目进一步扩大。

现在,陶哲轩希望,添加证明辅助语言能突破这个瓶颈。

而他尤其感兴趣的,就是是否可能使用这些现代工具同时探索一类数学问题,而不是一次只关注一两个问题。

本质上,这种方法是可模块化的重复任务,如果有适当的平台来严格协调所有贡献,众包和自动化工具可能会尤其有用。

如果用以前的方法,这种数学问题类型是无法扩大规模的。除非在多年时间里,随着个别论文慢慢地一次探索一个数据点,直到对这类问题获得合理的直觉。

此外,如果有一个大型问题数据集,可能有助于对各种自动化工具进行性能评估,并且比较不同工作流程的效率。

这类项目最近的一个例子,是「忙碌海狸挑战」。

在今年7月,第五个忙碌海狸数被证实为是47,176,870。

一些更早的众包计算项目,比如「互联网梅森素数大搜索」(Great Internet Mersenne Prime Search, GIMPS),在内在精神上跟这些项目也有些类似,尽管它们使用的是更传统的工作量证明机制,而不是证明辅助语言。

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

陶哲轩表示,很想知道是否还有其他现存的众包项目探索数学空间的例子,以及是否有可用的经验教训。

陶哲轩提出新项目

为此,陶哲轩自己也提出了一个项目,来进一步测试这一范式。

这个项目受到去年MathOverflow问题的启发。

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

不久后,陶哲轩在自己的Mathstodon上,对它进行了进一步讨论。

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

这个问题属于泛代数(universal algebra)领域,涉及对原群(magma)的简单等式理论的中等规模探索。

原群是一个配备了二元运算

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

的集合G。

最初,这个运算o没有附加任何额外的公理,因此原群本身是较为简单的结构。

当然,通过添加额外的公理,如恒等公理或结合律公理,我们可以得到更熟悉的数学对象,例如群、半群或幺半群。

在这里,我们感兴趣的是(无常数的)等式公理。这些公理涉及由运算o和G中的一个或多个未知变量构建的表达式的相等性。

此类公理的两个熟悉的例子,是交换律x o y = y o x和结合律(x o y) o z = x o (y o z)。

其中x,y,z是原群G中的未知变量。

另一方面,(左)恒等公理e o x = x在这里不被视为等式公理(equational axiom),因为它涉及一个常数e ∈ G。这类涉及常数的公理在本研究中不予讨论。

接下来,为了阐明自己发起的研究项目,陶哲轩介绍了十一个关于原群的等式公理例子。

这些等式公理是仅涉及原群运算和未知变量的等式——

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

因此,举例来说,等式7表示交换律公理,而等式10表示结合律公理。

常数公理等式1是最强的,因为它限制了原群G最多只能有一个元素;与之相反,自反公理等式11是最弱的,所有原群都满足这一公理。

接下来,我们就可以探讨这些公理之间的推导关系:哪些公理能推出哪些公理?

例如,等式1可以推导出这个列表中的所有其他公理,而这些公理又可以推导出等式11。

等式8作为特殊情况可以推导出等式9,而等式9又作为特殊情况可以推导出等式10。

这些公理之间完整的推导关系可以用以下哈斯图(Hasse diagram)来描述:

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

这一结果特别回答了数学问答网站MathOverflow上的一个问题:是否存在介于常数公理(等式1)和结合律公理(等式10)之间的等式公理(equational axioms)。

值得注意的是,这里大多数的蕴含关系都很容易证明。然而,其中存在一个非平凡的蕴含关系。

这个关系是在一个与前述问题密切相关的MathOverflow帖子回答中得到的:

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

命题1:等式4蕴含等式7

证明:假设G满足等式4,因此

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

对所有x,y ∈ G成立。

特别是,当y = x o x时,可以得出(x o x) o (x o x) = (x o x) o x。

再次应用(1),可以得出x o x是幂等的:

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

现在,在(1)中将x替换为x o x,然后使用(2),可以得出(x o x) o y = y o (x o x)。

尤其,x o x与y o y是可交换的:

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

此外,通过两次应用(1),可以得到(x o x) o (y o y) = (y o y) o x = x o y。

因此,(3)就可以简化为x o y = y o x,这就是等式7。

上述论证过程的形式化,可以在Lean中找到。

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

然而值得注意的是,确定一组等式公理是否决定另一组等式公理的一般问题,是不可判定的。

因此,这里的情况有点类似于「忙碌海狸」挑战,即在某个复杂点之后,我们必然会遇到不可判定的问题;但在达到这个阈值之前,我们仍有希望发现有趣的问题和现象。

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

上面的哈斯图不仅断言了列出的等式公理之间的蕴含关系,还断言了公理之间的非蕴含关系。

例如,如图所示,交换公理等式7并不蕴含等式4公理(x + x) + y = y + x。

要证明这一点,只需找出一个满足交换公理等式7但不满足等式4公理的原群的例子。

比如,在这种情况下,我们可以选择自然数集N,其运算为x o y := x+y。

更一般地,该图断言以下非蕴含关系,这些关系(连同已指出的蕴含关系)完整描述了这十一个公理之间蕴含关系的偏序集:

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

在此,陶哲轩邀请读者提出反例,来完成其中的部分证明。

最难找到的反例,就是等式9无法推出等式8了。

用Lean可以给出解决方案。

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

另外,陶哲轩还提供了一个GitHub存储库,包含了所有上述包含和反包含关系的Lean证明。

可以看出,仅仅计算11个等式的哈斯图就已经有些繁琐了。

而陶哲轩提出的项目,是尝试将这个哈斯图扩展几个数量级,覆盖更大范围的等式集。

他提议的集合是ε,即最多使用原群运算o四次的等式集,直到重新标记和等式的自反性和对称性公理。

这包括了上述十一个等式,但还有更多。

还有多少呢?

回想一下,卡特兰数C_n是用二元运算o(应用于n+1个占位符变量)形成表达式的方法数;而给定m个占位符变量的字符串,贝尔数B_m是为这些变量分配名称的方法数(可以重新标记),其中允许某些占位符被分配相同的名称。

因此,忽略对称性,最多涉及四次运算的等式数量是

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

左侧和右侧相同的等式数量是

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

这些都等同于自反公理(等式11)。

剩下的9118个等式由于等式的对称性成对出现,所以ε的总大小是

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

陶哲轩表示,自己还没有生成这样恒等式的完整列表,但他猜想,使用Python就可以轻松完成。

使用AI工具,应该能生成大部分所需的代码。

他表示,自己完全不清楚ε的几何结构会是什么样子。

大多数等式会彼此不可比较吗?它会分为「强」公理和「弱」公理吗?

现在,陶哲轩的留言区,已经有了几十条评论。

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

陶哲轩发起的众包数学研究项目,AI辅助证明数学研究的可行性

感兴趣的读者,陶哲轩也向你发出了邀请。

本网站的内容主要来自互联网上的各种资源,仅供参考和信息分享之用,不代表本网站拥有相关版权或知识产权。如您认为内容侵犯您的权益,请联系我们,我们将尽快采取行动,包括删除或更正。
AI资讯

Retake AI:废片修复利器,P图手残党的福音

2024-9-30 10:31:02

AI资讯

AI技术对未来就业市场的影响及建议

2024-9-30 12:17:38

个人中心
购物车
优惠劵
今日签到
有新私信 私信列表
搜索