来源丨量子位（ID：QbitAI） 作者丨鹭羽 图源丨WSJ 确实也是轰动数学和AI两界了。 因为就在最近，世界级顶尖数学家宣布辞职，前往硅谷，全职加入AI初创公司——这家公司，还是自己学生创办的—— 一个24 岁00后华人女生 。 这个数学家，正是被誉为"最懂拉马努金的当代数论学者"的 小野肯 （Ken Ono） 。 一辈子都扑在纯数学上，拿奖拿到手软、荣誉满身的他，如今脱掉学者长衫，带着学生一块儿辞职创业，其抉择堪称激进。 吸引他的这家公司，也不是等闲之辈，而是硅谷新贵——Axiom，一家 主打AI数学 的明星公司。 几个月前，凭借0产品0用户就实现了3亿美元估值，创始人24岁、斯坦福数学博士辍学，名叫 洪乐潼 （Carina Letong Hong） 。 洪是公认的数学少年天才、三年MIT数学和物理双学位、2022年度中国罗德学者，也是仅有的4名中国获奖者之一…… 如今师生搭档，创业之路再获强大助力。 最不可能做AI的人做AI了 据悉，小野肯将作为该公司的第15位员工加入，职位是 创始数学家 。 他主要的工作是推动内部AI模型达到性能极限，通过设计出只有深度理解数学原理才能够解决的数学问题，以及制定衡量 ...

核心观点 - 谷歌DeepMind研发的AI系统AlphaProof在国际数学奥林匹克竞赛（IMO）中取得28分（满分42分），达到银牌水平，距离金牌线仅差1分，这是AI首次在此类顶级数学赛事中获得奖牌级成绩 [3][4][18] 技术方法 - AlphaProof结合了预训练大语言模型的直觉和AlphaZero强化学习算法的探索能力，其核心是将AI思维“硬化”成可被计算机逐行检验的形式化证明语言Lean [8][6][7] - 系统首先利用谷歌Gemini模型将近一百万道自然语言数学题翻译成Lean代码，构建了约8000万条形式化数学命题的题库供AI练习 [10] - 训练过程分为两步：先通过监督学习微调掌握基本证明技巧，再进入强化学习阶段，通过类似AlphaGo的自我对弈在数百万次问题证明中不断进步 [10] - 在解题搜索中采用类似蒙特卡罗树搜索的策略，智能拆解复杂问题为子目标，避免了暴力穷举 [11][16][17] 竞赛表现 - AlphaProof与专攻几何的AlphaGeometry 2联手，在2024年IMO的6道题中解出4道，获得28分，处于银牌段顶端 [18] - AlphaProof单独解决了3题（包括2道代数题和1道数论题），其中整场最难的第6题在600多名顶尖学生中仅5人满分解决 [18] - 剩余1道几何题由AlphaGeometry 2完成，而两道组合数学题因难以形式化和搜索爆炸等原因未能攻克 [18] 当前局限 - 解题效率较低：人类选手需在4.5小时内完成3题，而AlphaProof解决3题耗费了将近3天时间 [21] - 通用性不足：未能解决两道组合数学题，这类高度非结构化创新思维的问题仍对AI构成挑战 [21] - 无法自主读题：需要人工先将题目翻译成Lean形式化表达，不具备自然语言理解能力 [21] 未来方向 - 研发方向包括让AI直接阅读理解自然语言表述的数学题，并给出形式化证明 [23] - 针对不同类别数学问题（如组合数学或几何）引入更专业策略，如融合符号计算、知识库或分领域训练模型 [24] - 未来可能实现数学家与AI证明助手协同工作，AI负责快速验证猜想和尝试思路，人类专注于提出问题和宏观构想 [24] - 其形式化推理能力对AI安全和可靠性有启发意义，输出的每一步推理可追溯、验证，有助于减少大模型的荒诞臆测 [25]