https://www.qbitai.com/2024/11/222842.html 陶哲轩宣布「等式理论计画」成功，57天完成2200万+数学关系证明 一水 专案进度比陶哲轩预期更快 57天， 人类和AI合作 搞定了4694个等式之间22028942个蕴含关系！ 大神陶哲轩激动宣布： 等式理论计划 ，成功。 “等式理论计划”，由陶哲轩本人在2024年9月25日发起，目的是探索按蕴含关系排序的 原群（magma）等式理论空间。 特别的是，在这个计画里，陶哲轩不仅集合了人类数学家的力量，还把 AI工具 纳入了合 作者的范围，包括 ChatGPT 、 Claude 和 GitHub Copilot 。 计画发起当日就正式启动，仅仅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的等式包括： https://www.qbitai.com/wp-content/uploads/replace/61f72f9841578d4672fe7bb14a473497.jpeg 而等式理论计划，就是要找出magma中不同等式之间的等价、推出与非推出关系。 就拿上面这11个等式来看，最终的关系图be like： https://www.qbitai.com/wp-content/uploads/replace/7f5721c969934397beca04d568a59483.jpeg 可以看出，常量公理等式（1）蕴含了其他所有等式，即如果1成立，那麽其他等式也自动 成立；而反身公理等式（11）由於最宽松（x=x），几乎所有的magma都满足这个公理。 回到计画本身，陶哲轩等人在初始阶段集中研究了那些 只包含一个方程式的magma定律 ，这些方程式最多包含四个magma操作（即二元运算）。 举个例子，如果我们有一个magma（M，^，其中M是元素的集合，O定义在M上的二元 运算。 则一个「最多四次使用magma操作」的表达式如下： https://imgur.com/rMowiSn 其中,,,,都是集合M中的元素，每次*的使用都算一次magma操作。 这样的等式定律有 4694个 ，由於每个定律都可能蕴含其他4693个定律（一个定律不能蕴 含自身），因此总共有4694*(4694-1) = 22,028,942个可能的蕴含关系需要被证明或反驳 。 这里的蕴含关系包括“蕴含”和“反蕴含”，其中“蕴含”关系又涉及两种类型： 已证明的蕴含：在Lean中已验证 推测的蕴含：尚未在Lean中验证，可能由人或电脑生成 更多项目细节，陶哲轩在专案日志中，留下了非常详细的记录—— 9天进度99.866%，大模型有用但“表现低於预期” 简单总结「等式理论计画」的进度，就是一个字： 快 。 陶哲轩本人都说： 这个专案的进度远远超出我的预期。 有多快？ 仅仅 48小时 ，很大一部分蕴含关系就已「解决在望」。 计画启动 第5天 ，计画参与者们已从最初的约2,200万条蕴含关系中解决了大量简单蕴含 ，只剩下约300万的数量尚待解决。 项目启动 第9天 ，随着首次重大重构的完成——合作者们改进了magma的运算符号，以使 Lean代码的编译速度显着加快，以及一些研究问题的推进，项目完成度一举从 87% 跃升 到了 99.866% 。 第19天 ，专案进度来到 99.9963% 。陶哲轩在他的部落格文章中提及，写论文的事已经 提上日程，并且可能包含数十名作者。 GitHub显示此专案有45位贡献者： https://www.qbitai.com/wp-content/uploads/replace/e9faa5cee56f713e751926baedf02acd.jpeg 到了11月21日，也就是专案 第57天 ，随着主专案最後一个未解决的蕴含关系被搞定（待 验证），「等式理论计画」目标已宣告达成。 论文可以正式开写了。 陶哲轩透露，论文的框架早已拟好，但後续还需要大量工作来更新，并转换为可以提交的 形式。 日志中也详细谈到了大模型工具所发挥的作用。 第一天，陶哲轩就对GitHub Copilot大加赞赏： GitHub Copilot在处理日常任务时非常有用，例如输入需要证明的新Lean定理， 或更新蓝图来整合最新的PR结果。 他具体举了个例子：要将Lean转换为LaTeX，把Lean程式码贴为注释，开始敲LaTeX， GitHub Copilot就会自动补全剩下的内容。 不过，陶哲轩也坦率表示， 大模型们在专案中的表现“低於预期” ，更多的时候，数学 家们用到的还是“经典AI”，比如自动定理证明器Vampire等。 他也提到： 计画的参与者非常多元化，包括处於职业生涯各个阶段的数学家和电脑科学家，学生 和业余爱好者。 Lean在整合人类和机器生成的贡献方面表现出色。机器产生的部分在数 量上是贡献的最主要来源，不过，许多自动产生的结果最初是人类在特殊情况下得出的， 之後被进一步推广和形式化。 具体到专案中，GitHub Copilot的主要作用还是加快程式码的编写，而Claude则被用来帮 忙创建视觉化工具，例如这个「等式浏览器」： https://www.qbitai.com/wp-content/uploads/replace/1507c4b2f9c361314d206e9e5807a3c6.jpeg ChatGPT则更多扮演激发数学家们灵感的小助手角色。 对陶哲轩来说，ChatGPT能帮他快速掌握通用代数的一些细节。 而lyphyser、Daniel Weber、Fan Zheng和Bhavik Mehta这几位计画参与者，也透过跟 ChatGPT的讨论，证明1659这个等式可能具有非平凡的合流性。 主项目里程碑达成，不过「等式理论计画」的其他衍生项目仍在进行中，例如研究在有限 原群限制下的类似蕴含图、对蕴含图进行资料分析等等。 陶哲轩也再次强调了这个计画和AI的连结： 希望专案中的蕴含关系能够作为未来AI数学工具的基准测试。 除了陶哲轩之外，专案的主要维护人还有义大利数学家Pietro Monticone和Shreyas Srinivas。 两位都是Lean重度爱好者。 △Shreyas Srinivas主页 Pietro Monticone也和他特伦托大学的同事们一起搞过指数3的费马大定理的Lean版证明 。 --

※ 发信站: 批踢踢实业坊(ptt.cc), 来自: 111.253.138.68 (台湾) ※ 文章网址: https://webptt.com/cn.aspx?n=bbs/Math/M.1732348314.A.995.html