给124个点连线,要求图中既不能出现三角形,也不能出现四边形,这就是图论中经典的极值构造问题。此前数学界公认的参考纪录是629条边,普遍认为已经接近理论极限。而月之暗面旗下的Kimi K3在这次任务中构造出了包含630条边的图,并通过程序验证。只多出一条边,听起来似乎微不足道,但在组合数学中,每多塞进一条边,都意味着要在全部124个点之间重新完成一次精密的结构大重构,牵一发而动全身。
这项成果来自图灵奖得主、中科院院士、清华大学交叉信息研究院院长姚期智与月之暗面创始人杨植麟等人的联合研究。一位是中国理论计算机科学的奠基者之一,一位是大模型创业一线操盘手,两代人首次联合署名,本身就释放出明确信号:AI做科研已不再是实验室里的猜想,而是需要理论计算机科学家与大模型团队共同定义“什么才算做出来了”。团队真正想回答的问题是,AI究竟能不能从事数学研究,而不只是解答数学题。
争议也随之而来:多构造一条边算不算真正的科学突破,会不会只是暴力搜索蒙对的个例,AI是否真的理解背后的数学机理。为区分“运气好撞上”和“逻辑上证明”,团队没有在传统基准上打转,而是搭建了名为TCSExam的评测系统,用100项理论计算机科学科研任务,测试前沿AI智能体能否证明定理、开发求解器、构造数学对象,甚至挑战长期未解决的猜想。该框架通过Lean 4、程序检查器和检查点机制,分别验证数学证明、算法表现及中间推导,避免把局部进展误判为完整成果。
从行业意义看,这次多出的一条边,标志着AI首次在“极值构造”这类研究级任务上把人类参考纪录向前推进了一步,其价值不在于数字本身,而在于提供了一条可验证、可复现的AI参与真实科研的技术路径。对数学界而言,AI正从解题工具转变为可能产出新构造的研究伙伴;对大模型行业而言,如何让模型输出经得起形式化检验,也将成为下一阶段竞争的关键分水岭。
