网易首页 > 网易号 > 正文 申请入驻

AI颠覆数学研究!陶哲轩借AI破解数学猜想,形式化成功惊呆数学圈

0
分享至


新智元报道

编辑:编辑部

【新智元导读】历时三周,陶哲轩成功地用AI工具完成了形式化多项式Freiman-Ruzsa猜想证明过程的工作。他再次呼吁数学研究者学会正确利用AI工具,网友惊呼:以后的数学论文不需要人类可读了?

用AI工具辅助研究数学的项目,再一次被陶哲轩跑通!

三周前,他曾发布一篇博文,记录下自己使用Blueprint在Lean4中形式化多项式Freiman-Ruzsa猜想的证明过程。


就在昨天,他激动宣布:将多项式Freiman-Ruzsa猜想的证明形式化的Lean4项目,在三周后取得了成功!


现在,依赖关系图已经完全被绿色所覆盖,Lean编译器也报告说,这个猜想完全遵循标准公理。


陶哲轩表示,在整个团队中,自己贡献的代码大概只有5%。这个结果很鼓舞人心,因为这意味着数学家即使不具备Lean编程技能,也能领导Lean的形式化项目。

他发现,项目中在数学上最有趣的部分,形式化起来比较容易,而技术上看起来最显而易见的步骤,却最耗时。

而使用Blueprint将项目分解成难度小到中等的部分,效果很好,这就让大量并行工作成为可能。

这样,许多贡献者就可以处理特定的子任务,而无需理解整个证明过程,甚至可以完全不了解相关的数学领域知识。


就在几分钟前,Lean成功证明了PFR猜想,且没有留下任何悬而未决的问题(后文将会提到的「sorry」)。这意味着,这个项目的所有主要目标,都已经圆满完成。

与此同时,他在三周前也就是11月18日的那篇博客也被网友翻出,引发热议。

果然,AI加持数学研究颠覆力量的后劲,得需要数月的时间才能让人们认识到。

而只有在最前线的研究者,才能在第一时间切实感觉到这种巨大力量的冲击和震撼。

陶哲轩呼吁:数学家们一定要学会用AI了

有网友向陶哲轩提问:这是否意味着,有越来越多的证明是人类不可理解,但机器可解决的?


陶哲轩表示,恰恰相反,如果证明的形式化变得更加主流,并且更多地得到AI辅助,那完全有可能创建出既人类可读、又能被机器阅读的证明。

PFR证明的blueprint就证明了这一点——既人类可读,每个证明步骤还带有形式化的理由,还能得到一个依赖关系图,来可视化整个论证的全局结构。


当然,陶哲轩也提醒道,不要把「计算机辅助证明」和「不能提供理解/偶然成立的证明」搞混了。

比如对于有限单群分类的超过10000页的证明,几乎百分百是由人工生成的,但一个由计算机协助处理的替代证明,在某些方面看更令人满意。


跟网友经过几轮讨论后,陶哲轩做出以下总结——

Blueprint本身就是一种编程语言,可以看作一种Lean的伪代码。

许多数学家都应该将写作风格从标准数学英语/LaTex,转换为Blueprint/LaTex。


网友:以后研究都不需要「人类可读」,AI懂就行了

网友表示,陶哲轩对于各种研究工具随意掌握的程度,几乎可以称得上是可怕。

我在研究生阶段对数学的尝试,就就好像一个穴居人本来在摇晃一辆普通的独轮车,忽然眼前出现了一辆直升机,上面的人向我伸出手,告诉我来试试看,一点也不可怕。 自从听说四色定理以来,我一直很清楚,形式化是数学的未来。但我没有预料到的是,陶哲轩如此从容不迫,形式化才刚刚获得牵引力,他就能用AI完成几乎所有的数学写作。


形式化,是指从基本公理和规则中真正推导出证明中的每个陈述。而陶哲轩在这篇博文里,把需要死记硬背的劳动都抽象出来,交给了机器。

他的工作表明,形式化才刚刚开始在主流数学中受到关注。


已经有人开始畅想:很可能会有一段时间,大多数证明只是在Lean或类似系统中完成,再也没有人需要费心写一篇「人类可读」的论文了。

数学,将变成一种编程!


一位数学硕士表示,现在自己的研究步骤有三步——

1.理解自己想证明的东西,通过阅读或者与人交谈; 2.用纸笔绘制出包含要点的草图; 3.将校样输入到LaTeX中,让自己要交的作业变得人类可读。


是的,如果我们只是要训练或微调AI来产生答案,然后编写一个循环来反馈,直到编译器正确输出,那我们自己并不需要真的理解。

用这种方法,我们还能生成更多的训练示例,可以手动检查结果是否符合要求,做上注释。而训练,可以提高初始答案的准确性。


PFR猜想的形式化过程

以下是陶哲轩发在博客上的形式化过程,感兴趣的读者可以挑战一下。

11月,陶哲轩与Yael Dillies和Bhavik Mehta启动了一个合作项目,目的是利用Lean4对自己之前关于Freiman-Ruzsa(PFR)猜想的预印本论文进行形式化。


项目虽然启动不到一周,但进展相当顺利,大部分文件都被形式化了。

这个项目得益于Patrick Massot的Blueprint工具,这个工具让团队能够编写与Lean形式化紧密相关的、人类可读的证明「蓝图」。

在Blueprint中,有一个陶哲轩特别喜欢的功能,那就是自动生成的依赖图。它可以提供形式化进度的大致快照。截至当时,依赖图的样子如下:


在依赖图的图例中,不同的气泡(表示引理)和矩形(表示定义)被赋予了不同的颜色。

简单来说,绿色的气泡或矩形表示那些已经被完全形式化的引理或定义,而蓝色的则指那些已准备好进行形式化的引理或定义(这意味着它们的陈述已经形式化,但证明还没有,同时所有相关的前置引理和证明也是如此)。

而陶哲轩团队的目标,就是将所有通向「pfr」气泡的底部气泡,都变成绿色。

点击依赖图底部的「pfr」气泡时,可以看到以下内容:


图中,Blueprint显示出一种人类可读的PFR语句形式,还附带了这个语句的人类可读证明,该证明依赖于项目中的其他语句:


注意,「pfr」气泡是白色的,但有一个绿色边框,这意味着PFR的陈述已经在Lean中正式化,然而证明并没有。

证明本身还没有准备好被形式化,是因为一些先决条件(特别是「entropy-pfr」Theorem 6.16)甚至还没有形式化的陈述。

单击依赖关系图中PFR陈述下方的Lean链接,就可以进入相应的Lean文档:


这就是Lean中的典型定理的样子。在冒号之前有许多假设,例如:

G是一个属于顺序2的有限初等阿贝尔群 (这就是团队选择形式化有限场向量空间的方式);A是G的非空子集;A+A的基数<K倍A的基数。

冒号后边的陈述是结论:A可以以c+H的和的形式包含在G的子群H中,以及在最多 的基数的集合c中。

聪明的读者可能会注意到,上面的定理似乎缺少一两个细节,例如,它没有明确断言H是一个子群。

这是因为「pretty printing」模式抑制了定理陈述中的一些信息,只要单击「来源」链接,就可以看到了。


可以看到,H需要具有G加法子群的类型。

该定理底部有一个明显的「sorry」,这意味着尚未为该定理提供证明,但最终意图当然是用实际证明,来代替这个「sorry」。

填补这个「sorry」现在还很难做到,所以需要寻找一个更简单的任务。

下面是一个简单的中间引理「ruzsa-nonneg」,它出现在证明中:


该表达式 指的是X和Y之间的熵Ruzsa距离,它是一个实数。

气泡是蓝色的,带有绿色边框,这意味着陈述已经形式化,证明也准备好形式化了。

Blueprint依赖关系图表明,这个引理可以从前面的一个引理中推导出来,称为「ruzsa-diff」:


「uzsa-diff」也是蓝色的,边框是绿色的,所以它与「ruzsa-nonneg」具有相同的当前状态:陈述是形式化的,证明也准备好形式化了,但证明还没有用Lean编写。其中, 是X的香农熵。

通过观察Lemma 3.11和Lemma 3.13,我们可以清楚地看到|H[X] - H[Y]|显然是非负的。

因此,即使我们还不知道如何证明Lemma 3.11,但假设Lemma 3.11成立,并补全Lemma 3.13的证明,应该是轻而易举的事。

Lemma 3.11的形式化如下:(「sorry」表示Lemma目前还没有证明)

同时,Lemma 3.13的形式化为:


现在,我们要试着把后一个「sorry」填上。

在PFR github仓库的本地副本中,陶哲轩用编辑器(Visual Studio Code,扩展名为lean4)打开了相关的Lean文件,并导航到「rdist_nonneg」的「sorry」处。

随附的「Lean信息视图」就会显示Lean证明的当前状态:


在底部,可以看到我们需要证明的目标。

接下来,在证明这个说法时,需要运用一系列「战术」来改变目标和/或假设。

第一步是加入应用Lemma 3.11所需的因子2。


现在,我们有了两个目标(和两个「sorry」):一个是证明 等价于 ; 另一个是证明 。

在填上第一个「sorry」之后的状态如下(删去了一些无关的假设):


这里可以使用一种非常方便的「linarith」策略,它能解决任何可以通过现有假设的线性运算得出的目标:


成功之后可以看到,状态报告显示这个分支已经没有需要证明的目标了。所以,我们继续剩下的「sorry」,也就是证明 :


在这里,我们将尝试引用Lemma 3.11。为此,陶哲轩添加了几行代码:


于是,我们又有了两个子目标,一个是证明约束 (可以称之为「h」),另一个是就从h推导出前一个目标。

对于第一个目标,需要调用正在编码Lemma 3.11的「diff_ent_le_rdist」引理。

其中一种方法是尝试使用「exact? 」策略,它会自动搜索,看目标是否可以立即从现有的引理中推导出来:


于是,陶哲轩点击了建议的代码(系统会自动将其粘贴到正确的位置)。结果成功了,只留下最后的「sorry」:


这里,陶哲轩通用使用了「exact?」策略,并按照它的建议建立匹配了边界:


在补全最后一个「sorry」时,陶哲轩再一次尝试了「exact?」,想知道如何把h和h'结合起来才能达到预期目标,结果成功了!


可以看到,所有的下划线都消失了。也就是说,Lean已将其视为有效证明。

通过省略几个中间步骤,我们可以将这个证明压缩得相当紧凑:


现在证明完成了!

我们最后得到的,基本就是一个「单线证明」,考虑到Lemma 3.11和Lemma 3.13是如此接近,这也是合情合理的。

然后,陶哲轩将所有内容推送回Github主版本库。

Blueprint的重建需要相当长的时间(约半小时),依赖关系图现在以绿色显示 「ruzsa-nonneg」:


因此可以说,PFR的形式化更接近完成了。

不过,虽然「ruzsa-nonneg」现在被涂成绿色,但还没有这个结果的完整证据,因为它所依赖的引理「ruzsa-diff」不是绿色的。

从这一点上看,证明仍然是局部完成的。

陶哲轩表示,希望在未来的某个时候,前身结果也能被证明,那时,就可以说PFR猜想的结果,得到了完全的证明。

参考资料:

https://news.ycombinator.com/item?id=38528582

https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/

特别声明:以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布,本平台仅提供信息存储服务。

Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.

相关推荐
热点推荐
为何一楼架空层起火,会烧到30多层?南京火灾亲历者讲述逃生经过:“我是楼层里第一个发现起火的”

为何一楼架空层起火,会烧到30多层?南京火灾亲历者讲述逃生经过:“我是楼层里第一个发现起火的”

鲁中晨报
2024-02-24 15:49:23
著名演员佘诗曼在香港的“豪宅”,没看错吧,也就4-50平方米

著名演员佘诗曼在香港的“豪宅”,没看错吧,也就4-50平方米

静静时光
2024-02-23 12:52:56
甘肃网红“杨老二”今日下葬,妻子因悲伤过度哭晕过去 邻居痛惜:他一直乐观

甘肃网红“杨老二”今日下葬,妻子因悲伤过度哭晕过去 邻居痛惜:他一直乐观

红星新闻
2024-02-24 18:21:37
致命的电瓶车电池!南京居民楼火灾致15死:只是 2.1万起火灾之一

致命的电瓶车电池!南京居民楼火灾致15死:只是 2.1万起火灾之一

大风文字
2024-02-24 11:32:32
3-2!国乒女团豪取六连冠,孙颖莎2分,陈梦制胜,元宵佳节献礼

3-2!国乒女团豪取六连冠,孙颖莎2分,陈梦制胜,元宵佳节献礼

天涯沦落人
2024-02-24 22:40:20
南京小区火灾,背后真相令人悲痛!

南京小区火灾,背后真相令人悲痛!

梦马笔谈
2024-02-24 16:04:48
云南网红“墨江小宗哥”去世 妻子:拍摄时意外溺水身亡 刚结婚一个月

云南网红“墨江小宗哥”去世 妻子:拍摄时意外溺水身亡 刚结婚一个月

红星新闻
2024-02-24 15:22:12
1957年,倪匡伪造多种公章证件介绍信,由内蒙古畏罪潜逃至广州

1957年,倪匡伪造多种公章证件介绍信,由内蒙古畏罪潜逃至广州

回京历史梦
2024-02-24 16:02:13
英国皇室又出丑闻!威廉王子被曝长期出轨,凯特患上绿色癌症

英国皇室又出丑闻!威廉王子被曝长期出轨,凯特患上绿色癌症

萌神木木
2024-02-24 13:48:05
不满海航飞机二次安检,男子大手一挥:我TM不坐了,评论区被点燃

不满海航飞机二次安检,男子大手一挥:我TM不坐了,评论区被点燃

看晓天下事
2024-02-23 19:59:01
国乒罕见连败日本!马琳用人引大质疑 弃用王曼昱自尝苦果

国乒罕见连败日本!马琳用人引大质疑 弃用王曼昱自尝苦果

厝边人侃体育
2024-02-24 21:18:13
南京城里的一场大火,戳穿了3.5亿电动车主的谎言,亲历者发声

南京城里的一场大火,戳穿了3.5亿电动车主的谎言,亲历者发声

坦然风云
2024-02-24 18:48:40
意外!伊万科维奇刚接手国足就给足协一个下马威,或拒绝留用郑智

意外!伊万科维奇刚接手国足就给足协一个下马威,或拒绝留用郑智

罗掌柜体育
2024-02-24 15:22:32
火爆冲突!巴特勒被锁喉,30人大混战,4人惨遭驱逐,NBA打起来了

火爆冲突!巴特勒被锁喉,30人大混战,4人惨遭驱逐,NBA打起来了

体育就你秀
2024-02-24 12:28:35
马琳快感谢孙颖莎吧!决赛独得2分成日本杀手,暴力连斩张本+早田

马琳快感谢孙颖莎吧!决赛独得2分成日本杀手,暴力连斩张本+早田

黑色柳丁
2024-02-24 21:55:39
惯子如杀子!熊孩子吃火锅致一家三口被团灭:孩子呛死,大人被杀

惯子如杀子!熊孩子吃火锅致一家三口被团灭:孩子呛死,大人被杀

古今档案
2024-02-23 01:48:28
打就完事了!官网更新中国男篮对阵日本12人名单:付豪替换余嘉豪

打就完事了!官网更新中国男篮对阵日本12人名单:付豪替换余嘉豪

直播吧
2024-02-24 18:17:26
破大防了!王晶导演拍了一辈子电影,还没贾玲一部电影票房高!

破大防了!王晶导演拍了一辈子电影,还没贾玲一部电影票房高!

静静时光
2024-02-23 20:52:01
又一家国产车企扛不住了?年终奖找理由拖着不发,公积金也没交

又一家国产车企扛不住了?年终奖找理由拖着不发,公积金也没交

可达鸭面面观
2024-02-24 18:39:45
澳洲政府败诉!新冠疫苗的黑暗秘密被揭开,13种严重副作用公布!澳洲男子接种后心脏受损,终获赔偿...

澳洲政府败诉!新冠疫苗的黑暗秘密被揭开,13种严重副作用公布!澳洲男子接种后心脏受损,终获赔偿...

澳洲红领巾
2024-02-23 14:23:38
2024-02-24 23:06:44
新智元
新智元
AI产业主平台领航智能+时代
10710文章数 65292关注度
往期回顾 全部

科技要闻

中国载人月球飞船,名字定了!

头条要闻

俄军在阿夫杰耶夫卡"大规模"受降 绍伊古听取战果回报

头条要闻

俄军在阿夫杰耶夫卡"大规模"受降 绍伊古听取战果回报

体育要闻

普尔这赛季有多烂?拿1.28亿,沦为替补

娱乐要闻

王阳高斯登顶热搜,一家同框幸福满溢

财经要闻

巴菲特致敬芒格:永远的伯克希尔建筑师

汽车要闻

后排体验全面升级 新款智己L7售29.99万起

态度原创

房产
本地
亲子
家居
军事航空

房产要闻

35亿!北京住总摘得昌平百善镇0004等地块

本地新闻

寻年味 过大年| 元宵节来永清,一起赏百米神龙和特色灯会

亲子要闻

爱就是要保护好自己!

家居要闻

精简设计,用美学感知空间

军事要闻

俄防长绍伊古赴俄乌冲突前线视察部队

无障碍浏览 进入关怀版