推文

@0x99DaDa · 2026-10-12 22:18

同样是 AI 做数学，DeepMind 选了另一条路：少做、过审、证明公开。 10 月 8 日，《Science》刊登了 Google DeepMind 的 AlphaProof Nexus 论文。系统用 Gemini 写形式化证明语言 Lean 的代码，每改一步就过编译器查错，错了再改。试了 353 道尚未解决的 Erdős 问题，自主解出 9 道，其中两道悬了 56 年；另外还证了整数数列百科 OEIS 里 44 道未证猜想。论文写，每道题的推理成本大约几百美元。 🔹 核心不是「模型一次想对」，而是「写完必须过编译」——编译器当裁判，人主要看最后几条过关的证明 🔹 最简配（只靠 Gemini + Lean 循环、不叫专业证明工具）也能解出那 9 道，只是难题上更贵 🔹 证明和部分自然语言说明已挂在 GitHub，陶哲轩维护的「AI 对 Erdős 题贡献」维基也记了账 🔹 353 里只解出 9 道，大约 2.5%，和陶哲轩说的「AI 在 Erdős 题上大概 1%–2% 成功率」同一量级 对照一下：本月早些时候 OpenAI 往 GitHub 一次性公开了七百多篇内部模型写的数学手稿，没走期刊审稿。今天上午写过丘成桐在清华拉起千人「数学×AI」联盟，说这是「最兴奋也最危险的时代」。DeepMind 这边的选择是：结果少一点，但每条都过了 Lean，再过《Science》同行评审。 机器暂时解不了大多数难题。但「写完就过编译」至少先帮人筛出哪几条值得花时间看——比堆一堆没人审的手稿，好懂一点。

曝光 323 · 评论 2 · 点赞 3 · 书签 0 · 曝光/时 19.288772364007887