多1条边引热议：Kimi刷新图论纪录，AI做科研获突破

组合数学领域的一项突破引发关注——针对124个点的无三角形、无四边形图的边数纪录，被AI团队刷新。此前该领域的参考极限为629条边，而Kimi K3构造出了630条边的符合约束的图，并通过程序验证。这看似仅增加1条边的成果，背后是理论计算机科学家与大模型团队的跨界合作，也让“AI能否真正开展数学研究”的议题再次被讨论。

这项成果来自图灵奖得主、清华大学交叉信息研究院院长姚期智与大模型企业月之暗面创始人杨植麟等人的联合研究。两代研究者的结合，指向的核心疑问是：AI是否能从“解题工具”进阶为“科研合作者”，产出可独立验证的原创研究成果？

外界对此成果的质疑，集中在“多1条边是否真的是科学突破”“是否只是暴力搜索的巧合”“AI是否真的理解背后的数学机理”。为此，研究团队搭建了一套名为TCSExam的评测系统，试图解决这些核心问题。

TCSExam的核心设计思路，是将AI科研能力拆解为四条可验证的任务轨道，覆盖理论计算机科学的不同研究方向：

• 定理证明轨道：包含20项任务，要求模型提交Lean 4形式化证明，覆盖13个理论计算机科学领域；
• Solver工程轨道：包含30项任务，要求开发可重复运行的算法程序，在独立测试实例和统一资源限制下评测；
• 数学构造轨道：包含20项任务，考察模型生成符合严格约束的图、纠错码等数学对象的能力；
• 开放猜想轨道：包含30项任务，允许模型从证明成立或寻找反例两个方向展开研究。

为避免任务定义偏差导致的评测失效，团队建立了任务编写与独立审核机制：编写者根据研究材料构建形式化命题、提交接口和验证程序，审查者核对定义、量词及参数条件，并通过边界样例和试运行排查问题，研究领域专家负责审定任务的研究意义。开发过程中，超过40道候选任务因试运行阶段已被解决而退出题库。

TCSExam的底层设计利用了理论计算机科学“找解难，验解易”的特点，将AI的探索结果整理成验证器能够检查的研究证书，以此区分局部进展与完整成果。对于定理证明，证书是Lean代码，由内核根据形式逻辑规则检查推导，系统还会审计证明依赖，排除未完成证明占位符和未经允许的额外公理。

为了更精准分析模型的能力缺口，TCSExam设计了Checkpoint机制，把复杂证明拆分为多个中间目标，验证其中一个Checkpoint时，系统会暂时把其他Checkpoint的命题作为假设，检查模型能否在这些条件下完成当前推导。这种处理既可以评估模型的局部进展，又能避免循环依赖导致的误判。

实验中，GPT-6 Astra在TCSExam中取得了显著进展：它在20项研究级定理中完成14项，还将Alon–Jaeger–Tarsi猜想的证明范围从五元有限域的8维推进到9维。这一过程中，Astra通过构造两组10×10的非负整数数组，结合矩阵可逆性、有限傅里叶恒等式等条件，将复杂的矩阵问题转化为204个变量的整数线性系统，最终选取143条方程组合出矛盾关系，证明了9维反例不存在。这份成果被整理成包含71个Lean模块的项目，通过了独立环境的重新编译和公理依赖检查。

这次实验最值得关注的不是边数或维度的微小提升，而是AI已经能产出可机器核验的原创科研结果。它标志着AI在科研领域的应用，从辅助性的“查文献、写代码”，向独立完成部分研究级任务迈进。对数学界而言，TCSExam提供了一套可复用的评测框架；对AI科研来说，这是“AI for Science”的重要实践，也为未来的AI科研 Agent发展奠定了基础。