公司核心事件 - 世界级顶尖数学家小野肯（Ken Ono）辞去终身教职，全职加入AI初创公司Axiom，担任创始数学家[2][5][6] - 小野肯的加入标志着其从对AI持怀疑态度到积极投身AI数学领域的重大转变[12][17][18] - Axiom公司由小野肯的24岁学生、斯坦福数学博士辍学的华人女生洪乐潼（Carina Letong Hong）创办[2][7] 公司业务与目标 - 公司核心目标是为量化对冲基金公司开发能够解决实际数学问题的AI[24] - 具体方法是让AI学习严格的逻辑推理和数学证明过程，构建和验证形式化证明，保证结果的准确性和严谨性[24] - 产品旨在帮助对冲基金和量化交易公司快速解决投资、股市等金融领域的复杂数学问题[25] 公司技术成就与实力 - 公司近期在数学界表现亮眼，解决了Erdős问题 124和 481[26] - 对于124问题，AxiomProver模型将验证推进到了基础公理层面，超越了同行仅完成简化版证明和Lean形式化验证的工作[28][29] - 对于481问题，公司确实完成了解决工作，并借助Lean形式化完成了所有的类型检查，而此前OpenAI的GPT-5仅被指出是检索现有文献[31][32] - 公司团队规模小但精英云集，除小野肯外，还包括前Meta研究员François Charton等顶尖AI和数学专家[34] - François Charton的研究（如让Transformer模型解微分方程）被视为让神经网络理解数学结构的先驱成果[34] 公司融资与估值 - 公司在仅有0产品0用户的情况下，于首轮融资实现了3亿美元估值[7][36] - 公司的投资人中包括B Capital等顶级风险投资机构[36] 创始人背景 - 创始人洪乐潼是公认的数学少年天才，用3年时间完成麻省理工学院数学和物理本科双学位[7][42] - 本科期间发表了9篇涉及多个数学领域的论文，刊登在《美国数学会会报》、《拉马努金期刊》等顶级期刊上[42][43] - 曾获得2022年度中国罗德学者荣誉，是仅有的4名中国获奖者之一[7][45] - 在麻省理工学院期间师从小野肯，解决了拉马努金理论中的部分猜想，并获得了拉马努金精神奖学金[44][45] - 2024年获得斯坦福数学博士录取offer，但选择辍学创业[46][48] - 最近被评为2026年福布斯30位30岁以下的AI精英[49] 行业意义与展望 - 小野肯与洪乐潼的师生合作，被类比为数学史上的黄金师徒哈代和拉马努金，旨在携手逼近数学界的“GPT时刻”[52] - 公司致力于寻找数学公理，破解困扰人类数个世纪的难题[49]

核心观点 - 谷歌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]