Axiom Math是Jacob文章中另一个关键角色的东家——24岁华裔创始人洪乐潼从斯坦福退学创业，公司估值已达110亿元。其产品AxiomProver基于Lean形式化语言，采用「AI生成+机器验证」双保险机制：生成器提出证明思路，Lean编译器逐行强制校验，逻辑差一个符号都不通过。2025年该系统在Putnam数学竞赛拿下120分满分（人类历史最佳110分），并攻克多道悬置数十年的Erdős难题。创始人请来自己的导师、数学家小野健担任「创始数学家」——这正是AI公司争夺顶尖数学家的典型案例。

本文提到的数学家「投奔AI」并非孤立事件，而是2026年AI数学能力密集突破的必然结果。5月OpenAI用推理模型证伪了80年历史的单位距离猜想，成果被独立数学家验证为「首个完全由AI产出的研究级成果」；6月16位数学家发布《莱顿宣言》呼吁警惕AI对学科本质的侵蚀；7月Anthropic的Claude Fable 5顺手找到雅可比猜想反例。从AI一年多前在IMO拿银牌，到如今能独立产出期刊级证明，这条加速曲线解释了为什么菲尔兹奖得主会认为「两年内AI就能在定理证明上超过人类」。

新晋菲尔兹奖得主选择加入AI公司，不代表数学界达成共识。2026年6月，16位顶尖数学家联名发布《莱顿宣言》，警告AI自动化会威胁数学的「人文本质」——创造力、理解力、协作精神，且AI生成的低质论文正让同行评审系统不堪重负。宣言合著者、哥伦比亚大学数学家Michael Harris直言：「科技行业的商业逻辑与数学价值观背道而驰。」而另一边，陶哲轩则冷静指出AI更像工具链——擅长检索和形式化验证，但「数学的灵魂活仍离不开人类」。同一场变革，有人看到危机，有人看到工具升级，两面都值得听。

AI数学证明的「可信度瓶颈」正在被打破。AxiomProver能在24小时内输出经Lean机器验证的完整证明，将审稿周期从数年压缩到一天。北大AI4Math团队也用双智能体框架解决了安德森猜想，完成了19000行Lean代码的形式化验证，效率比人类专家提升10倍。当前能看到的关键变量是：Lean等证明助手正在成为数学界的「新标准」——博士必修课和期刊接收流程都在向它靠拢。一旦形式化验证成为论文发表的门槛，传统依赖「人肉审稿」的信用体系将被彻底重构，速度会倒逼更多数学家拥抱AI，而非抵抗它。

Jacob Tsimerman已停止招收数学博士生，理由是2030年毕业时「传统数学职业可能不存在了」。但这话值得追问：他说的「数学职业」具体指什么？如果数学研究从「人手工证明」转向「人设计难题给AI解、人解读AI的证明、人判断什么值得证」，那数学家的角色不是消失，而是向「AI数学研究的设计师」转型。真正值得跟踪的不是「数学家会不会失业」，而是「哪类数学能力会升值，哪类会被AI取代」——小野健加入Axiom Math给AI出题，就是一个信号。