数学人生， 庾信平生最萧瑟，暮年诗赋动江关。 查看知乎原文 这个问题的答案，历史已经替我们回答过一次了。 1966 年，Lander 和 Parkin 在 CDC 6600 计算机上跑了一分钟，找到了 这个反例，把欧拉 1769 年提出的幂和猜想一锤定音地推翻了。两百年间无数数学家用纸笔徒劳地尝试证明它正确，结果一分钟 CPU 就给判了死刑。这不是孤例，这是序曲。从那一刻起，”机器摘果子”这件事就在数学各个角落反复上演，只不过当年摘果子的是晶体管和暴力穷举，今天摘果子的是大模型和形式化验证。把这两段历史摆在一起看，规律清晰得有点残忍——所谓”低垂的果实”，从来不是会不会被摘走的问题，而是被谁、用多快的速度摘走的问题。 计算机时代的第一轮收割，覆盖面比大多数人记忆中的要广得多。四色定理 1976 年被 Appel 和 Haken 用 IBM 370 算了 1200 小时证明，成为人类历史上第一个”无法用纸笔验证”的重要定理，直接引爆了数学界对”什么才算证明”的哲学大讨论（ Four color theorem ）。Mertens 猜想——一旦成立就能推出黎曼猜想的百年命题——1985 年被 Odlyzko 和 te Riele 用计算数论方法证明反例存在，虽然具体反例值至今没找到，但整个猜想的”正确性信仰”在一夜之间崩塌（ Mertens conjecture ）。1989 年 Clement Lam 团队烧掉相当于 2000 小时超算时间，证明了 10 阶有限射影平面不存在——这种”证无”的问题，人类手算在可预见的未来都做不到（ Lam 论文 ）。Keller 猜想在 8 维和 7 维分别于 1992 年和 2002 年被计算机构造的反例推翻，那些反例的复杂度同样是人类手工无法触及的（ Keller’s conjecture ）。 定理证明器登场之后，机器不再只是找反例，开始正面攻克猜想本身。1996 年 McCune 的自动定理证明器 EQP 独立证明了 Robbins 猜想——连塔尔斯基都没解决的代数问题，机器自己搞定（ Robbins conjecture ）。1998 年 Hales 用计算机证明开普勒猜想，2014 年 Flyspeck 项目用 HOL Light 和 Isabelle 完成形式化验证，机器证完再由机器复查，完成了”证明的证明”（ Kepler conjecture ）。2016 年布尔毕达哥拉斯三元组问题被 SAT 求解器判定，证明文件压缩后仍有 200TB，是迄今为止人类产出的最大证明（ arXiv:1605.00723 ）。数论里的”地毯式轰炸”就更系统了：黎曼ζ函数临界线上的前 个零点已被 Gourdon（2004）逐一验证（ ζ零点验证 ），哥德巴赫猜想验证到 ，考拉兹猜想验证到约 ，GIMPS 分布式项目 1996 年至今找到了 18 个梅森素数包括目前已知最大的 （ GIMPS ）。这些问题的”计算可及部分”早已被机器摘得干干净净，人类再想靠手算在这些方向上刷出新结果，基本不可能了。 而现在，AI 开始了第二轮收割，速度快了一个数量级。 2026 年 1 月，DeepMind 的 AlphaEvolve 在置换群中找到了 50 年未被发现的 64 维超立方体结构，解决组合群论开放问题。2025 年 10 月，UCLA 数学家借助 GPT 攻克了搁置 42 年的涅斯捷罗夫猜想。5 月 20 日，OpenAI 的通用推理模型完全自主地证伪了悬置 80 年的埃尔德什平面单位距离猜想，由 9 位顶尖数学家核验——菲尔兹奖得主 Gowers 的评价直截了当：”此前没有任何 AI 生成的证明能接近这个水准”（ 核验论文 arXiv:2605.20695 ）。仅仅一天后，DeepMind 发布 AlphaProof Nexus，用 Lean 形式语言自主证明 9 道埃尔德什开放问题，其中包括两道悬置 56 年的，外加 44 条 OEIS 整数序列猜想、一个代数几何 15 年悬案、一个极小极大优化 7 年悬案，全程无需人类质检（ arXiv:2602.10177 ）。7 月 20 日，哈佛的 Levent Alpöge 看世界杯决赛的时候，让 Anthropic 的 Fable 5 找到了雅可比猜想的反例——凯勒 1939 年提出、位列斯梅尔 21 世纪难题清单的 87 年悬案，被一行 216 字符的公式推翻。值得一提的是，张益唐当年的博士论文题目正是雅可比猜想，论文的不顺直接导致了他后来多年的潦倒。这件事的戏剧性，小说都不敢这么写（ New Scientist ）。到了 8 月，一位名叫 Lech Mazur 的创业公司 CEO——不是职业数学家——用 GPT-5.6 Pro 证明了森多夫猜想，68 年悬案，配 9 万行 Lean 4 验证代码。陶哲轩花了数天时间消化这份证明，把它压缩到 1.5 万行，而且在整理过程中发现它实际上证明了一个更强的命题，1972 年的 Phelps-Rodriguez 猜想作为推论直接得证，精简版代码已在 GitHub 开源（ 陶哲轩博客 ）。 数学家们的反应值得细看。陶哲轩在国际数学家大会上公开警告，AI 正在引发数学界”前所未有的价值观危机”；但在森多夫猜想事件中，他展示了人类的新角色——不做证明的机器，而做证明的消化者。9 万行机器代码，他压缩成 1.5 万行人类可读的论证，还从中提炼出机器自己都没意识到的更强定理。他强调”因为证明的最终消费者是人类，数学家仍然是必要的”，但同时也坦承用 AI 攻击博尔查猜想等其余问题”尚未取得显著成功”——机器的能力边界依然清晰。普林斯顿的张寿武打了个很妙的比方：”AI 就像汽车和飞机，非常强大但也很危险，不坐是不可能的，但要学会在安全的意义下用它。”他同时承认 AI 找到雅可比猜想反例”非常了不起”。北大的李欣意提出了一个”凸包”理论：如果人类的数学知识是一个有凹有凸的多边形，外部是未知，那么顶尖数学家是在尖角上把边界推向远处，而目前的 AI 只是在”取凸包”——补齐已知知识的内部，还不会向外探索。彼得·舒尔茨的态度最为决绝：”数学思想就像孩子，需要悉心呵护，历经岁月成长。正如我不希望我的孩子由 AI 来教育，我也在不借助 AI 的情况下独立思考数学问题，并尽力避免阅读 AI 生成的文本。”2026 年 6 月 2 日，来自 15 所大学的 16 位数学家发布了获国际数学联盟正式背书的《莱顿人工智能与数学宣言》，系统性地警告 AI 正在威胁数学的正确性标准、署名秩序、公平性与研究自主性，要求研究者公开 AI 使用情况、坚持同行评审、建设独立于商业公司的公共计算设施（ 宣言官网 ）。 回到最初的问题：低垂的果实会被摘光吗？已经在摘了，而且摘得比大多数人预想的快得多。但历史同样给出了另一半答案——1966 年机器推翻欧拉幂和猜想之后，数论没有死，反而因为机器提供的反例和数据，长出了计算数论、随机矩阵关联这些全新的枝叶。四色定理的机器证明没有杀死图论，而是催生了形式化验证整个领域。果实摘完之后，真正剩下的问题恰恰是最难的：什么问题值得问，什么是好的定义，怎样从一堆正确答案里看出该建什么理论。这些目前还在人类手里。陶哲轩那句”证明的最终消费者是人类”，大概就是这场收割季里，人类数学家最后的、也是最难被机器摘走的那颗果子。 查看知乎讨论
- 情报分类：开源项目与落地
- 分类依据：内容涉及项目实践、创业、副业或变现
- 信息来源：资讯 / 知乎日报
- 发布时间：2026/9/18 07:00:00
- 暂无回复