多些数学，少些ego（谈谈AI和数学）by 埃里克·德梅因（Erik Demaine）2026-10-29

★置顶zzllrr小乐公众号，追踪《小乐数学科普》系列报道，参与数学 vs AI投票！

坚持不炒作的数学与AI报道，投稿信箱zzllrr@gmail.com

多些数学，少些ego（谈谈AI和数学）

译者注：标题中的ego暂无中文统一译法，意为自我、自负、自尊、以自我为中心、傲慢、我执、我慢等，事实上没有绝对的褒贬之意。

作者：埃里克·德梅因（Erik Demaine）

MIT计算机科学家、数学家。

日期：2026-10-29

我想聊聊我一直在开发的一套工具，初衷是让数学家能够和AI、计算机协同研究。我今天核心想讲的一点是：如果我们放下“数学必须由我们人类亲手攻克”这种执念，把数学研究看作一场协作，我们就能做出更多成果。

大家都知道，数学领域正在发生剧变，新闻里各种报道有喜有忧。有人满怀期待，也有人惧怕这场我称之为数学末日（mathpocalypse）的新变局。

这份清单汇总了今年由AI取得的重磅数学成果。其中最重量级的一项，至少从理论计算机科学角度来看，是几天前指数时间假设（Exponential Time Hypothesis，ETH）被证伪，属于重大突破。

还有就是几周前OpenAI一次性放出七百多条结果，不过其中三条后来撤回了。所以这套系统远非完美，但足够振奋人心，涌现出大量重要进展。

首先我想谈谈这类研究是怎么做出来的，以及我们如何进一步推进。

早期大家都在尝试埃尔德什问题，一部分原因是有很完善的埃尔德什问题题库。后来研究范围拓展到其他问题，包括千禧年大奖难题——这也是优质的问题来源，很多知名成果都围绕它们展开。相关工作很多，但这类研究到底是怎么落地的？

各大实验室很少公开详细流程，不过我们能拼凑出大致思路：批量拿下一大堆问题，比如说全部700个埃尔德什问题，最后只把真正解出来的成果对外发布。就像OpenAI几周前那次发布，他们说一共挑战了约4000个问题，最终解决大约700个。从这个角度看，成果的含金量就要打一点折扣。

能解出一部分问题固然激动人心，但显然，并不是所有尝试的问题都能成功。有些问题对人类和AI而言都太难了；我们现在找到的，只是在不同意义下“可处理”的那一批。

我一方面想亲自体验这套流程，看看哪些问题容易、哪些棘手；另一方面也希望其他人也能做同样的探索。

于是我开发了一套开源软件系统，名叫Loose Ends（遗留问题）。它名字的含义，是帮你处理自己过往论文里遗留下来的待解问题；更广义上，它面向所有人，提供基于大模型的公开猜想自动求解能力。

除了方便我们摸清规律、开展实验，这套工具还有一个很大的价值：研究者可以聚焦自己真正关心的问题，而不是那些容易引爆舆论、大厂天然优先追逐的热门难题。我希望借助大模型做数学的潮流，重新回归数学家本身。

我们的思路就是批量搜集公开猜想，依靠这些强大的新工具，从中筛选出那些容易摘到的“低垂果实”。而我们发现一个瓶颈：该怎么挑选值得研究的问题？Loose Ends的底层构想是：利用你自己的论文，或是文献库里已发表的所有论文。

几乎每一篇论文结尾都会留下一堆开放问题，这正是优质素材，而且和你关心的研究方向高度契合。你选定感兴趣的论文（包括你自己写的），系统自动提取其中的开放问题——既有作者明确写出来的猜想，也有文本里暗含的待研究方向，之后再尝试求解。猜想储备越多，产出新结果的可能性就越大。

下面是Loose Ends的完整工作流，包含多个模块，其中大部分模块本质上就是精心撰写的大模型提示词。

1 Survey（调查）

流程从比较机械的文献拉取开始：最简单的用法，输入你的姓名，系统自动下载你在arXiv上的所有论文，同时拿到PDF和源码文件——源码更适合大模型处理，当然只上传PDF文件也可以运行。

第一个核心大模型环节：文献解析，重点提取开放猜想，同时抽取论文里已有的结论与技术方法。逻辑是：如果给模型的不只是待解问题本身，还有前人解决同类问题用到的手段，模型成功求解的概率会更高。

之后你可以选择让大模型做优先级分诊（triage）：评估每个问题好不好下手、能不能解。后面我会展示这个评估的效果，准确度还不错；模型在这个阶段就会开始构思解题思路。

有一步非常关键：很多猜想提出之后，其实已经有人后续解决了。所以系统会自动检索文献。大模型在检索后续相关工作、判断猜想是否已被证明这件事上，表现出乎意料地好。

2 Solve（求解）

重头戏：批量发起求解。你可以选中所有关心的问题，或是分诊标记为优先尝试的问题。大模型读取论文信息、分诊得到的思路、检索到的相关文献，开始尝试证明。哪怕最后没能解出来，检索到的相关文献本身也是有用输入。

求解完成后，我们要核验结论是否合理。现阶段还没有接入Lean形式化核验证明，只是依靠大模型评审，判断命题的可信度。输出结果包含它给出的解答，以及可信度评分。如果求解失败，可以反复重试，比如设定最多五轮求解尝试。

3 Write（撰写）

拿到一批候选结果之后，由人来筛选。人工浏览全部结果，再让模型撰写论文。这份文稿不是直接拿去投稿的终稿，而是整理成一份更适合人类阅读的版本。它依然远谈不上完美，但我花了不少功夫调教，让它贴合我自己的写作习惯：引言讲清相关工作、成果在领域里的定位，再陈述结论、简述证明思路。

文稿往往漏洞不少，所以内置了审稿环节：自动审阅文稿，润色文字，再次核验正确性。这个过程循环多轮，直到生成一份大体通顺的稿件，交给人审阅。

以上就是整套系统的全貌。

接下来我演示它实际运行的效果。我开发Loose Ends最初是用来跑自己论文里的问题，但为了做更严谨的对照实验，我选取了今年夏天两场会议的论文。

第一场是SoCG，计算几何顶会，也是我最初深耕的领域，收录该方向最顶尖的成果，一共约100篇论文。对照的是另一个几何会议CCCG，加拿大计算几何会议，也是我早年参加过的会议。这场会议覆盖面更广，更鼓励学生参与、偏向探索性实验工作，不一定追逐最火热的难题，创新性实验成果更多，录用率更高，一共约50篇论文。

这两组样本可以代表理论计算机/数学领域不同风格的研究。平均每篇论文附带大约3个开放猜想，合计450个：SoCG 300个，CCCG 150个。

这里展示分诊评估的输出分类：【强烈建议尝试Attempt】【可以试试Maybe】【大概率跳过Skip】。大部分落在“可以试试”这一档。下一步文献回溯：有意思的是，哪怕这些猜想是今年夏天刚提出来的，有一部分已经被解决了。CCCG这批猜想暂时没有找到已被证明的；SoCG的猜想关注度更高，大约5%已经有后续解答。

我举几个例子，同时展示系统界面。Loose Ends自带网页端，可以浏览全部猜想、结果以及文献检索记录。

这里筛选出16个已经在文献里找到完整解答的猜想。其中一个是埃尔德什问题，最早是OpenAI给出的结果，后来由阿隆等人正式整理发表。

还有一个例子：温克勒（Winkler）单调简单维恩图猜想。这个猜想写在SoCG论文的arXiv第三版里，论文作者后续自己完成了证明，更新到arXiv第四版。这类信息靠人工很容易漏掉，由模型持续追踪更新非常好用。

文献视图里是全部144篇入库论文，按字母排序，每篇下面附带提取出来的开放猜想。列表里这篇CCCG论文就是我自己的，方便我做测试。

点开第二个开放猜想，进入研究详情页：模型声称已经解出这个问题。我不展开细说这个问题，大致是刻画一类边界补全的可行性条件。模型给出了一个有限的充要判定条件。从字面意义上说，它确实解决了问题；但并不完全是我们想要的答案。这套判定算法复杂度是nⁿ，效率极低，只是在形式上满足了猜想的要求。

这也给我们一个教训：提出猜想的时候，要精准描述自己真正想解决的问题。当然这个结果本身仍然有价值。

这套系统支持交互，你可以点【再次求解】，指令它：能不能把复杂度优化成多项式级别？这才是我们真正想要的。提交任务之后，后台会启动批量任务调度，多进程并行处理。

我这台机器最多同时跑8个任务，并行执行各项检索与求解。现在它正在重试这个问题。最后耗时39分钟，花费约2美元，再次返回一个解答。它一共尝试了三次，这次有进步，复杂度降到2ⁿ，虽然还没到多项式，但已经优化了一步。

这就是人机交互的方式：人可以引导研究方向。

如果你对某个结果感兴趣，想细看细节，就调用文稿生成模块，最多循环五轮写作与修改，产出一份草稿。

这是这份16页文稿的节选。摘要写得不错，交代了问题背景和主要结论。

我写论文很喜欢放对比表格，清晰区分已知结论和新成果，这份文稿里也有，给出了2ⁿ复杂度算法，还有一些固定参数算法。

文稿读起来依然不算轻松，大模型的写作能力还有短板，但相比原始输出，可读性已经好很多。

最核心的问题：整体求解率怎么样？我做了两轮实验。第一轮用GPT 6.1 Sol（目前公开可访问的OpenAI模型，公认数学能力略弱于Astra）。整体求解率大约20%。蓝色是SoCG，青绿色是CCCG。SoCG的猜想被更多人持续研究，所以更难求解；CCCG猜想更容易突破一点，但两组都接近20%。

剩下几组柱状图体现分诊评估的效果：标记【强烈建议尝试】的猜想，求解率大约40%，SoCG样本甚至更高；标记【可以试试】和【跳过】的求解率更低，大概13%、9%。

一个有意思的点：只要token预算充足，所有猜想都值得一试。哪怕被标记“跳过”，它也解出来8个结果，其中有些可能很有价值，我还没有全部审核。分诊的意义更多是优先级排序，想快速拿到成果，可以优先跑【强烈建议尝试】的问题。

成本方面：8个并行任务，实际耗时大概一天半，折合API费用约800美元，得到88个完整求解结果。性价比很不错。而且这还只是88个完整解，还有大量有价值的部分结果。开销大头在求解环节，分诊、文献检索更快，花费更少。如果你有OpenAI订阅套餐、token补贴力度大，这笔开销大概相当于一周的额度。

如果换成Astra模型，效果会更好。我没有从头完整复现对照实验，而是采用更贴合真实研究习惯的方案：先用Sol跑完全部问题，没有彻底解决的那些，再交给Astra二次攻坚。

当然，这种方式有叠加效应：Sol产出的中间结果、部分结论会输入给Astra，相当于给它提供了更多线索。开销上涨不少，大约是原来三倍，对应每月200美元订阅下三周的token额度，但成果也更多。浅色柱是Astra带来的增量。原先整体求解率20%，现在接近25%；【强烈建议尝试】那一组的求解率接近50%。这个结果很鼓舞人。

当然，其中一部分解答只是字面满足猜想，和研究者原本想要的内涵有偏差，但不少结论本身很有意思，具备发表潜力。剩下的工作就是人工逐一核验。现在任何人都可以用这套工具，自动攻克自己关心的猜想。

下一步规划：最首要的就是接入形式化证明。目前就算经过大模型审稿，结论依然有可能出错；Lean核验能给我们极高的可信度——你只需要确认Lean证明的定理陈述，就是你想要证明的命题。稍后我会再多说这点。还有不少拓展方向：现在Loose Ends大多是单篇论文独立处理，如果能把同一个领域所有相关论文关联打通，潜力会更大。

协作层面也有很大空间：AI产出了一大堆潜在有趣的结果，需要大量研究者筛选甄别、整理成文。我认为需要配套工具，支持多人协同，一起判断哪些结果有价值。我非常看重人机深度协作。当前版本里人的介入还比较有限，未来在批量工作流里，让人持续参与：判断什么时候需要人类介入破局、贡献新思路，或是由人来判断一项成果重不重要。

人类目前最擅长的环节，大概率就是提出猜想、撰写阐释、判断价值。模型在这三点上表现平平，所以要么继续迭代模型补齐短板，要么依靠人类协同。我还没有深入研究AI自主提出猜想，不过我在持续研究文稿生成和价值评判。

还有一点：现在模型大多只负责底层苦活、执行求解；由人决定研究对象、安排重试策略。未来可以让智能体更多参与决策，比如自主判断“这个结果只差一步，值得继续攻坚”。但归根结底，判断一件研究值不值得做，必须由人来把关。

以上就是Loose Ends项目的全貌。接下来我把它放到更大的脉络里聊聊。

我把这种人机协作，看作多人协作模式的延伸，我自己称之为超级协作（supercollaboration）。我几乎所有研究都是这套模式，已经坚持几十年了。

过去超级协作只有人类参与者，现在我们尝试加入AI。形式可以是研讨会（我已经办过几十场），也可以是课堂，组织麻省理工本科生组队攻克开放猜想。我发现这种集体头脑风暴想要成功，关键是营造包容正向的氛围，并且保证每一位贡献者都能获得署名认可。

超级协作产出的论文署名规则非常宽松：只要你有实质贡献，就可以成为作者，由参与者自己判断；为了简单统一，作者名单按字母排序——这在数学界很常见，规则提前说好。

我们还搭建了配套网站，分享办超级协作研讨会的经验，也开发了协作软件Coauthor（共同作者），现在全球数千名数学家在用，用来记录研究进展。很多成果是零散想法汇聚而成，大家可以上传草稿、草图、思路，在小组私密讨论区交流。

我现在正在开发Coauthor的API，目标是让AI成为这个协作生态里的正式参与者。人类上传猜想、阶段性进展之后，AI可以跟进反馈，比如“我检验了你这个猜想，找到了反例”。目前我们开会时已经会这么做：提出猜想，丢给大模型测试。如果把这个能力原生集成到进度平台里，会非常有前景。当然也要把控尺度，不能让讨论区充斥大量低质量AI输出，人机协同的边界还需要摸索。

下一个议题：Loose Ends产出了一堆结果之后，我们该怎么写成论文？OpenAI、Anthropic接连放出大量AI成果之后，一个棘手的困境浮现：怎么发表以AI推导为主的论文？

AI解数学题的速度，已经快过人类理解证明的速度，而且大模型写论文的能力目前并不理想——或许以后会变好，也可能一直如此。

一方面，只要我们确信结论正确，尽快公开成果是有价值的。Lean在这里至关重要：最好等Lean核验通过之后再对外发布。哪怕你还没有打磨出流畅的人类可读文稿，只要有Lean验证过的证明，就可以先公布结果，方便同行跟进拓展。我后面举一个实例。

但另一方面，如果我们自己没有吃透证明，就写不出连贯、数学家愿意细读的文章。于是就出现一种张力：一类是AI生成、文字粗糙，但能宣告结论、至少AI自己能读懂的文稿；另一类是人类数学家真正愿意研读的完整论文。

为此我们提出一种混合发表方案，弥合二者的矛盾。一份成果产出两份材料：第一份由人撰写，面向人类读者，概述结论，讲清它在领域里的位置，附上证明梗概，解释它如何在Lean里形式化，让读者确信形式化过程没有偏差；正式证明代码放在GitHub仓库。仓库里同时存放AI生成的详细草稿（哪怕文笔粗糙），这份材料主要供给其他大模型读取。随着人类慢慢吃透证明细节，我们再把完整证明逐步补进正式文稿。

我们已经用这个模式发表过一篇关于三维空间密铺的论文。问题是：给定单一形状，能否用它密铺三维空间？这个问题是不可判定的——不存在通用算法判定任意形状能否密铺空间。我们研究这个问题很久了。OpenAI发布成果两天之后，也就是10月8号，他们的一批结果里证明了这个问题至少存在非周期密铺，这是不可判定性的必要条件，但弱得多。

看到这个结果之后，我们尝试让大模型把结论推广到不可判定性，五分钟之内它给出了证明梗概。我们想尽快公开这个结论，因为很可能其他人也会独立发现。虽然我们还没有完全吃透证明细节，只有大致思路，但结论本身已经足够激动人心。

于是我们采用这套混合发表方案。我们搭建网页介绍成果，配套论文梳理它在文献中的定位。

绿色是已知算法结论，红色是已知复杂度下界，新结论在这里：三维及以上空间，单形状密铺问题是不可判定的。顺便说一句，还有一个遗留猜想：二维、两块形状的情形，我们尚且不知道是否存在判定算法。这是一个重大进展。

想要确信Lean证明的就是我们关心的命题，我们提出了Lean摘要（Lean abstract）的思路：提炼出最简的定义和定理陈述。

人只需要核验这一小段内容，不需要通读十几万行证明代码。只要你信任Lean系统本身可靠，你只需要核对定理陈述有没有写错。页面右侧就是读懂主结论所需要的全部定义与定理，篇幅很短。我们还并排放上数学家自然语言版本和Lean形式化版本对照。

举个例子：三维两点相邻，定义为L₁距离等于1；对应的Lean代码就是各分量差值绝对值之和等于1。逐行对照核验即可。这里有一个更强结论，叫co-RE完全性（co-RE-complete），Mathlib库里没有这个定义，我们在lean-wang库单独实现，这就需要读者多一层信任。

所以我们同时提供一个稍微弱化、依赖更少前置定义的版本。这套做法的目标，是把读者需要信任的内容压缩到最少。这种人类文本和Lean形式化文本对照互审的模式，我之前很少见到。

沿着这个方向，我还做了一个实验性原型系统，名叫Mean，用来表达Lean代码的语义。它是构建在Lean之上的一层语言，你可以写出类似这样的定义：

定义：简单图G是预连通的，当且仅当对G中任意顶点u、v，都存在一条u到v的路径。

写法几乎和数学家的自然语言一模一样，但它本身就是合法Lean代码，等价于标准的预连通定义。目标是让定义和定理陈述极易读懂，哪怕不懂Lean语法也能看懂含义。当然风险在于中间有一层翻译，翻译层本身必须经过严格审查。我不知道这条路最终能不能走通，但非常值得一试。

最后，我谈谈我对AI与数学未来的看法，观点可能会有点争议。

我对数学的未来满怀期待，当下变局丛生，机遇也遍地都是。很多我本来以为这辈子都看不到解答的难题，每周都有新突破。这种震撼难以形容，但也让人无比兴奋。很多我自己卡住很久的问题，现在有大模型这个新搭档融入我的工作流，我得以攻克不少自己关心的猜想。

Loose Ends只是一个缩影。我认为我们所有人都应该持续开发工具，优化人机协同的模式，而这和形式化数学相辅相成。形式化证明在去年还不具备普及条件，现在我希望自己每一篇论文都能在Lean里形式化验证。这件事已经变得可行。

我后台一直让大模型帮我把论文转成Lean。传统数学写作本身一直带有非正式、不严谨的地方，审稿人也不是万能的。我自己的论文出过漏洞，文献里也藏着不少错误。现在我们有机会校正、形式化所有成果，真正确信我们认定为真的命题确实成立。

我的核心观点：我们正处在重塑数学研究范式的时代，这是非常难得的机遇。数学的撰写方式正在改变，也就是刚才说的混合发表模式；阐释方式也会改变，交互式系统或许会比传统静态论文强大得多；审稿核验的方式也在变，Lean可以接管正确性核验，人类只需要判断哪些成果有价值、值得关注。

还有很多问题悬而未决：新的出版体系该是什么样？当数学家拥有AI这样强大的合作者之后，我们该如何评价研究者的贡献？但最重要的一句话：人类数学家和AI联手，可以做到任何一方单独都做不到的事，产出更多数学成果。我们唯一要做的，就是放下执念，不必执着于“这个证明是我独立完成”。

求点赞

求分享

求喜欢

参考资料

https://www.youtube.com/watch?v=Gdc1yll04qI

小乐数学科普历年合集

《小乐数学科普》2026年10月精选文章目录

《小乐数学科普》2026年Q3精选文章目录

zzllrr小乐微信公众号栏目《小乐数学科普》2026年6月文章精选

zzllrr小乐微信公众号《小乐数学科普》2026年5月文章精选

《小乐数学科普》2026年4月文章精选

2026Q1《小乐数学科普》精选文章合集目录

近三月《小乐数学科普》精选文章合集目录202512—202602

2026年01月《小乐数学科普》精选文章合集目录索引

2025年《小乐数学科普》精选文章合集目录索引

《小乐数学科普》2024年合集

· 开放 · 友好 · 多元 · 普适 · 守拙 ·

让数学

更加

易学易练

易教易研

易赏易玩

易见易得

易传易及

欢迎评论、点赞、在看、在听

收藏、分享、转载、投稿

点击左下角 阅读原文

查看原始文章出处

点击底部一起捐

助力腾讯公益

点击zzllrr小乐

公众号主页

右上角

置顶★加星

数学科普不迷路！

原标题：《多些数学，少些ego（谈谈AI和数学）by 埃里克·德梅因（Erik Demaine）2026-10-29》

阅读原文