AI 用 48 小时写 2 万行 Lean 代码,攻克 98 年未解的数学难题

量子位 · wechat · 2026-09-06

浙江大学 AI 方向博士生、无界AI联合创始人马千里,借助多智能体系统在 48 小时内解决了 1928 年提出的 Colombo 行列式问题中近百年无证明的情形,预印本论文与约 2 万行 Lean 形式化代码均已公开。

他组建了由 GPT-5.6、Fable5、DeepSeek 等模型分工的科研 Agent 系统:查文献、挑错审核、形式化证明各司其职,并专门搭建了 WUJIEAI AGENT 平台。AI 前后提出 8 条证明路线,其中一条「p=m-1」路线耗 11 小时、4.7 万行产物仍未收敛,由人类叫停后转向 p=m-2,2 小时 23 分后证明跑通。文章还呈现了 AI 辅助数学研究的新范式:人负责选题、评估路线、决定何时放弃,并指出帮助科学家构建科研 Harness 是创业机会。