首页时事民生政务教育文化科技财富体娱健康情感

旅行百科职场楼市企业乐活学术汽车时尚创业美食幽默美体文摘

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

学术 2024-11-24 18:21 北京

内容来自：量子位

作者：鱼羊一水

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的等式包括：

而等式理论计划，就是要找出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 Copilot大加赞赏：

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

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

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

他还提到：

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

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

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

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

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

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

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

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

除了陶哲轩之外，项目的主要维护人还有意大利数学家Pietro Monticone和Shreyas Srinivas。

两位都是Lean重度爱好者。

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

GitHub：

https://github.com/teorth/equational_theories

参考链接：

https://mathstodon.xyz/@tao/113522452070896956

https://teorth.github.io/equational_theories/

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

http://mp.weixin.qq.com/s?__biz=Mzg4MDE3OTA5NA==&mid=2247594054&idx=1&sn=3c1b94d2c8e2a3b0ca6aa2bfcb3f3861

致力于学术传播和科学普及，重点关注AI4Science/大模型等前沿科学进展。

最新文章

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

李德毅院士：认知机器的结构和激活

OpenAI 同日发布两篇论文：「外部」和「自动」红队测试新进展

Science重磅：AI完成定向蛋白质进化，特性提升100倍

首个端到端车载 VLM 框架；谷歌提出「无启发式多教师学习」方法｜大模型日报

谷歌AlphaQubit重磅发布，实时为量子计算机纠错，研究登上Nature

机器人「手转」钢笔，100% 成功率；文继荣团队：通过奖励引导树搜索增强 LLM 推理｜大模型日报

五大建议！OpenAI最强竞对Anthropic：正确的大模型评测应该是怎样的？

大模型后训练新范式，中科院、阿里和小红书团队提出“验证器工程”｜大模型日报

清华、北大团队推出LLaVA-o1：让视觉语言模型逐步推理；快手推出检索框架KuaiFormer｜大模型日报

大揭密！马斯克与 OpenAI 的「混乱分手」内幕：人才争夺、AGI、权力斗争

Mistral 发布开源多模态模型 Pixtral Large，聊天助手 Le Chat 全面对标 ChatGPT

清华姚班校友马腾宇，发布了他的首个多模态嵌入模型：「多模态检索」实现SOTA

综述：智能体的安全、隐私和道德威胁；FinVision：用于股市预测的多智能体框架｜大模型日报

AI反诈“奶奶”上线，24小时花式套路诈骗分子；AMD 全球裁员4%，约1000人｜一周热门

性能提升在即！吴恩达谈 LLM 新方向：优化智能体工作流

国防科技大学推出 AI 材料科学家 MatPilot；Anthropic 提出 LLM 越狱缓解新方法｜大模型日报

Science最新封面：AI大模型跨越物种边界、解码生命“密码全书”，基因组学进入全新时代

深度访谈｜AI 如何改变预测科学？看看统计学家怎么说

AI斩获6枚金牌！华为Kaggle大师级智能体诞生，自主解决数据科学难题

OpenAI官方指南：12条实用建议，手把手教学生用ChatGPT写作

Stability AI出官方教程了，带你轻松玩转Stable Diffusion 3.5

哈佛、MIT提出「精度感知」Scaling Laws；首个金融LLM综合双语基准｜大模型日报

OpenAI首位投资者《时代》刊文：AI将重新定义「人类的意义」

华为科学智能体 Agent K v1.0已达 Kaggle 大师水平；Meta团队提出自一致性偏好优化ScPO｜大模型日报

终于，AlphaFold3 开源了！代码免费下载，可用于非商业用途

OpenAI大改下代大模型方向，scaling law撞墙？AI社区炸锅了

清华、国科大、智谱团队提出LongReward：利用AI反馈改进长文本大语言模型

创纪录！首幅人形机器人绘制作品拍出108万美元；王慧文回归美团，带队探索AI应用｜一周热门

智谱「新清影」是怎样炼成的？CogVideoX+CogSound 技术详解

AI 的「phone use」竟是这样练成的，清华、智谱团队发布 AutoGLM 技术报告

清华、北大团队推出「安卓智能体」训练评估新框架 AndroidLab

Nature重磅：AI化学家再升级！大幅提升实验效率，推动化学合成进入“智能化”新阶段

研究实锤：别让大模型「想」太多，OpenAI o1准确率竟下降36.3%

清华、北大团队推出「安卓智能体」训练评估框架AndroidLab；Meta提出视频生成加速方法AdaCache｜大模型日报

科研人神器！接入5000万篇正版文献，知乎直答「专业搜索」太能打了

Meta 推出全新视频扩散模型 MarDini；周靖人团队：扩散 Transformer 的上下文 LoRA｜大模型日报

NeurIPS 2024｜清华、加州理工重磅研究：强化自训练方法 ReST-MCTS*，让大模型持续“升级”

港大打造 LightRAG：让大模型 RAG 高效又便宜

深夜重磅！ChatGPT可以“AI搜索”了，但并不完美

OpenAI最新研究：「打假高手」大模型事实性基准SimpleQA来了，已开源

小语言模型SLM综述｜大模型论文日报

大模型已过时、小模型SLM才是未来？苹果正在研究这个

超出人类思维的「系统0」：AI正在创造一种新的思维方式吗？

中国AI大模型出海，如何应对美国管制？最新报告给出了5个建议｜附下载链接

Nature封面：“揭穿”一切！Google DeepMind为AI大模型添加了“隐形指纹”

困扰18亿人的“全球干旱”，被AI更准确预测了

OpenAI又有高管走了，还发了篇长文

前OpenAI研究员：我必须离开；a16z创始合伙人：当前AI发展就像“卖大米”｜一周热门

刚刚，智谱推出情感语音模型 GLM-4-Voice，懂你的情绪，人人可用

分类

原创标签

时事社会财经军事教育体育科技汽车科学房产搞笑综艺明星音乐动漫游戏时尚健康旅游美食生活摄影宠物职场育儿情感小说曲艺文化历史三农文学娱乐电影视频图片新闻宗教电视剧纪录片广告创意壁纸头像心灵鸡汤星座命理教育培训艺术文化金融财经健康医疗美妆时尚餐饮美食母婴育儿社会新闻工业农业时事政治星座占卜幽默笑话独立短篇连载作品文化历史科技互联网

发布位置

广东北京山东江苏河南浙江山西福建河北上海四川陕西湖南安徽湖北内蒙古江西云南广西甘肃辽宁黑龙江贵州新疆重庆吉林天津海南青海宁夏西藏香港澳门台湾美国加拿大澳大利亚日本新加坡英国西班牙新西兰韩国泰国法国德国意大利缅甸菲律宾马来西亚越南荷兰柬埔寨俄罗斯巴西智利卢森堡芬兰瑞典比利时瑞士土耳其斐济挪威朝鲜尼日利亚阿根廷匈牙利爱尔兰印度老挝葡萄牙乌克兰印度尼西亚哈萨克斯坦塔吉克斯坦希腊南非蒙古奥地利肯尼亚加纳丹麦津巴布韦埃及坦桑尼亚捷克阿联酋安哥拉