陶哲轩油管首秀：33分钟，AI速证「人类需要写满一页纸」的证明

白交 一水 发自 凹非寺 量子位 | 公众号 QbitAI 快来围观，陶哲轩当视频博主了。 第一个产出就很炸裂： 人类需要写满一页纸的证明，结果借助AI 33分钟就搞定了？！ 整个过程看起来一气呵成，还是全程 "盲证" 不用过脑子那种。 对于这一操作，网友们惊呆：这具有足够的历史意义。 在没有明显引导、宣传之下，他的订阅数一天时间已经有900+，观看数超两千，目前仍然在高速增长中。 大家赶在爆火之前留言： 今天我们相聚在这里，就是为了见证伟大数学频道的诞生。 具体来看看是如何做到？ 33分钟盲证定理 陶哲轩这次选取了泛代数中的一个命题，即 证明Magma方程E1689蕴含E2 。 方程具体是什么不重要，我们只需要了解，即使是方程理论项目的合作者Bruno Le Floch，也足足人工花了一页纸才完成证明。 而用上AI后，整个证明过程仅用时 33分钟 ： 具体而言，陶哲轩尝试完全基于Bruno Le Floch的草稿，逐行进行形式化。 他将草稿拆分为微小逻辑单元，交由 GitHub Copilot生成代码骨架，再以Lean的canonical策略匹配填补细节 ，过程中也涉及部分手动补 全。 最终，整个形式化证明 ...