陶哲轩宣布“等式理论计划”成功,人类AI协作,57天完成2200万+数学关系证明

2024-11-24 12:08
摘要:57天,人类和AI合作搞定了4694个等式之间22028942个蕴含关系!大神陶哲轩激动宣布:等式理论计划,成功。“等式理论计划”,由陶哲轩本人在2024年9月25日发起,目的是探索按蕴含关系排序的原群(magma)等式理论空间。..

57天,人类和AI合作搞定了4694个等式之间22028942个蕴含关系!

大神陶哲轩激动宣布:等式理论计划,成功。

“等式理论计划”,由陶哲轩本人在2024年9月25日发起,目的是探索按蕴含关系排序的原群(magma)等式理论空间。

特别的是,在这个项目里,陶哲轩不仅集合了人类数学家的力量,还把AI工具纳入了合作者的范围,包括ChatGPTClaudeGitHub C0pilot

项目发起当日就正式启动,仅仅9天,项目进度就达到了99.866%

而现在,在2200万+个需要证明的蕴含关系中,8178279个已被证实,13855193个已被证伪,仅有162个还悬而未决。

按陶哲轩的说法,就是离“宣布完全成功”基本只是“时间问题”:

因此,我们现在已经开始着手撰写论文了。

什么是“等式理论计划”

还是先来扒一扒陶哲轩这回究竟是整了个什么样的活儿。

简单说,“等式理论计划”是指:

采用”数学家+AI(包括自动定理证明系统和大模型)+证明辅助语言Lean”这样的协作方式,构建一个展示4694个magma等式(最多四次使用magma操作)之间所有蕴含关系的 “蕴含图”。

首先,这个计划的最初灵感源于陶哲轩本人对“去中心化”研究方式的畅想。

传统上,大部分数学研究项目都由少数专业数学家(通常1~5名)进行,每个人都对自己的部分更专业,且彼此可以相互验证。

不过也是因为存在验证环节,组织更大规模的数学项目(尤其是需要涉及公众贡献),一直具有挑战性。

而现在,通过AI工具以及Lean这样的证明辅助语言,数学项目的大规模协作变得可能。

打前阵的就有开源社区寻找梅森素数的成功尝试,在这个代号GIMPS的志愿项目中,任何拥有强大PC或GPU的人都可以加入寻找梅森素数。

虽然证明助手这样的AI工具在这个项目里用得还不多,但表达的精神是类似的。

因此,在开展等式理论计划之前,陶哲轩就打算搞一个实验:

在一个数学项目中,聚齐专业/业余数学家、AI工具、证明辅助语言Lean等,一同干大事!

受去年MathOverflow上一个等式问题的启发,这一次,陶哲轩将目光瞄准了代数领域中的magma。

当时的问题是酱婶儿的:

交换恒等式和常量恒等式之间是否存在等价关系?

抛开具体问题不谈,这里主要想说明magma涉及等式之间的关系。

简单来说,magma是一个代数结构,它由一个集合和一个在该集合上定义的二元运算组成,但不要求满足任何额外的代数性质,如结合律、交换律等。

我们常见的有关magma的等式包括:

而等式理论计划,就是要找出magma中不同等式之间的等价、推出和非推出关系。

就拿上面这11个等式来看,最终的关系图be like:

可以看出,常量公理等式(1)蕴含了其他所有等式,即如果1成立,那么其他等式也自动成立;而反身公理等式(11)由于最宽松(x=x),几乎所有的magma都满足这个公理。

回到计划本身,陶哲轩等人在初始阶段集中研究了那些只包含一个方程的magma定律,这些方程最多包含四个magma操作(即二元运算)。

举个例子,如果我们有一个magma(M,∗),其中M是元素的集合,∗是定义在M上的二元运算。

则一个“最多四次使用magma操作”的表达式如下:

a∗b(一次操作)

(𝑎∗𝑏)∗𝑐(a∗b)∗c(两次操作)

𝑎∗(𝑏∗(𝑐∗𝑑))a∗(b∗(c∗d))(三次操作)

((𝑎∗𝑏)∗𝑐)∗(𝑑∗𝑒)((a∗b)∗c)∗(d∗e)(四次操作)

其中𝑎,𝑏,𝑐,𝑑,𝑒都是集合M中的元素,每次∗的使用都算作一次magma操作。

这样的等式定律有4694个,由于每个定律都可能蕴含其他4693个定律(一个定律不能蕴含自身),因此总共有4694*(4694-1) =22,028,942个可能的蕴含关系需要被证明或反驳。

这里的蕴含关系包括“蕴含”和“反蕴含”,其中“蕴含”关系又涉及到两种类型:

已证明的蕴含:在Lean中已经过验证

推测的蕴含:尚未在Lean中验证,可能由人或计算机生成

更多项目细节,陶哲轩在项目日志中,留下了非常详细的记录——

9天进度99.866%,大模型有用但“表现低于预期”

简单总结“等式理论计划”的进度,就是一个字:

陶哲轩本人都说:

这个项目的进度远超我的预期。

有多快?

仅仅48小时,很大一部分蕴含关系就已“解决在望”。

项目启动第5天,项目参与者们已经从最初的约2200万条蕴含关系中解决了大量简单蕴含,只剩下约300万的数量尚待解决。

项目启动第9天,随着首次重大重构的完成——合作者们改进了magma的运算符号,以使Lean代码的编译速度显著加快,以及一些研究问题的推进,项目完成度一举从87%跃升到了99.866%

第19天,项目进度来到99.9963%。陶哲轩在他的博客文章中提及,写论文的事已经提上日程,并且可能包含数十名作者。

GitHub显示该项目有45位贡献者:

到了11月21日,也就是项目第57天,随着主项目最后一个未解决的蕴含关系被搞定(待验证),“等式理论计划”目标已宣告达成。

论文可以正式开写了。

陶哲轩透露,论文的框架早已拟好,但后续还需要大量工作来对其进行更新,并转换为可以提交的形式。

日志中也详细谈到了大模型工具发挥的作用。

第一天,陶哲轩就对GitHub C0pilot大加赞赏:

GitHub Copil0t在处理日常任务时非常有用,比如输入需要证明的新Lean定理,或者更新蓝图来整合最新的PR结果。

他具体举了个例子:要将Lean转换为LaTeX,把Lean代码粘贴为注释,开始敲LaTeX,GitHub Copil0t就会自动补全剩下的内容。

不过,陶哲轩也坦率表示,大模型们在项目中的表现“低于预期”,更多的时候,数学家们用到的还是“经典AI”,比如自动定理证明器Vampire等。

他还提到:

项目的参与者非常多元化,包括处在职业生涯各个阶段的数学家和计算机科学家,学生和业余爱好者。Lean在整合人类和机器生成的贡献方面表现出色。机器生成的部分在数量上是贡献的最主要来源,不过,许多自动生成的结果最初是人类在特殊情况下得出的,之后被进一步推广和形式化。

具体到项目中,GitHub Copil0t的主要作用还是加快代码的编写,而Claude则被用来帮忙创建可视化工具,比如这个“等式浏览器”:

ChatGPT则更多扮演激发数学家们灵感的小助手角色。

对陶哲轩来说,ChatGPT能帮他快速掌握通用代数的一些细节。

而lyphyser、Daniel Weber、Fan Zheng和Bhavik Mehta这几位项目参与者,还通过跟ChatGPT的讨论,证明1659这个等式可能具有非平凡的合流性。

主项目里程碑达成,不过“等式理论计划”的其他衍生项目仍在进行中,比如研究在有限原群限制下的类似蕴含图、对蕴含图进行数据分析等等。

陶哲轩也再次强调了这一项目和AI的联系:

希望项目中的蕴含关系能够作为未来AI数学工具的基准测试。

除了陶哲轩之外,项目的主要维护人还有意大利数学家Pietro Monticone和Shreyas Srinivas。两位都是Lean重度爱好者。

Shreyas Srinivas主页

Pietro Monticone还和他特伦托大学的同事们一起搞过指数3的费马大定理的Lean版证明。

GitHub:

https://github.com/teorth/equational_theories

参考链接:

[1]https://mathstodon.xyz/@tao/113522452070896956

[2]https://teorth.github.io/equational_theories/

[3]https://terrytao.wordpress.com/2024/10/12/the-equational-theories-project-a-brief-tour/

更新于:16天前