过去几年,LLM 在数学能力上经历了三级跳。从 2025 年夏 DeepMind 与 OpenAI 同台拿下 IMO 金牌,到 2026 年初 DeepMind 实验系统 Aletheia 自主产出可发表的博士级研究,再到 OpenAI 推翻组合几何的重要猜想,机器正在从「随机鹦鹉」跃升为严肃的「数学推理引擎」。但更具结构性意义的变化,发生在 LLM 与证明助手的融合上。Lean、Isabelle、Rocq 这类形式化系统已存在十余年,过去把非形式化证明翻译成机器可验证代码是最痛苦的瓶颈;现在,LLM 正在把这一流程自动化。最具代表性的案例是 Math, Inc. 的 Gauss:它在数天内辅助数学家完成了 2022 年 Fields Medal 得主 Viazovska 八维球堆积证明的形式化,又在两周内自主完成了更难的 24 维情形。 陶哲轩把这条路径提炼为他所谓的「Big Mathematics」:去中心化、人机协作、形式化可验证。真正被改变的其实是数学共同体内部的信任机制——当一段证明被 Lean 检查通过,信任就不再依赖作者声誉或同行关系,而是依赖代码的机械验证。这让来自匿名研究者甚至业余爱好者的想法都能被严肃审视。论文作者名单从世纪初的单作者,演化到当代动辄几十人合作,未来可能走向人机混编的「分布式解题」。 但隐忧同样真实:工具可及性差距可能让数学变成「只有付得起闭源模型许可的组织才能玩的精英游戏」;当 AI 把「艰难求索」也外包后,数学家身份本身的意义正在被重新定义——这是技术流程的胜利,也是学科文化的拐点。