核心事件与人物 - 世界级顶尖数学家小野肯（Ken Ono）辞去终身教职，全职加入AI初创公司Axiom，担任创始数学家[1][2][4][5] - 吸引小野肯加入的Axiom公司由他24岁的学生、华人女生洪乐潼（Carina Letong Hong）创办[2][7] - 此次事件被描述为轰动数学和AI两界，标志着一位纯数学领域的领军人物转向AI产业[1][5] 公司Axiom概况 - 公司定位为一家主打AI数学的明星初创公司，核心目标是为量化对冲基金开发能解决实际数学问题的AI[6][27] - 公司在仅有0产品0用户的情况下，于几个月前完成首轮融资，估值达到3亿美元[7][37] - 公司团队规模小，起步晚，员工仅十余名，但已吸引多位顶尖AI和数学专家加入[35][53] 创始人洪乐潼背景 - 创始人洪乐潼为24岁00后，斯坦福数学博士辍学创业，是IMO金牌得主[7][9] - 她仅用3年时间完成MIT数学和物理本科双学位，本科期间已发表9篇广泛领域的学术论文[9][44] - 她曾是小野肯在MIT的学生，在其指导下解决拉马努金理论中的部分猜想，并获得多项顶级学术荣誉[46][47] - 她被提名为2022年度中国罗德学者（仅4名中国获奖者之一），近期被评为2026年福布斯30位30岁以下AI精英[9][51] 数学家小野肯的背景与角色转变 - 小野肯被誉为“最懂拉马努金的当代数论学者”，是数学领域举足轻重的人物，拥有弗吉尼亚大学终身教职[4][17][19] - 他此前对AI领域持怀疑态度，但去年春天参加AI模型测试研讨会后，观念发生转变，认为AI在某些数学领域已遥遥领先[14][15][21] - 他在Axiom的角色是创始数学家，负责为AI模型“绘制地图”，即设计高难度数学问题、制定性能基准并指导模型优化[10][12] 公司技术方向与产品目标 - 公司致力于开发能够进行严格逻辑推理和数学证明的AI，构建和验证形式化证明，保证结果的准确严谨[27] - 产品主要面向对冲基金和量化交易公司，帮助其快速解决金融领域的复杂数学问题[28] 公司已取得的技术成果 - Axiom的AxiomProver模型近期解决了数学界两个著名难题：Erdős问题 124 和 481[29] - Erdős问题 124 是一个30年前的加法数论问题，Axiom不仅解决了问题，还将其验证到基础公理层面[30][31] - Erdős问题 481 源自45年前，OpenAI的GPT-5曾声称解决但被指仅是检索文献，而Axiom确实完成解决并借助Lean完成了形式化验证[33][34] 团队与人才吸引力 - 除小野肯外，公司还吸引了前Meta研究员François Charton等顶尖AI专家加入[35] - François Charton的研究（如让Transformer模型解微分方程）被视为让神经网络理解数学结构的先驱成果[35] - 小野肯在加入Axiom前，曾连续拒绝多家其他硅谷公司的邀请[36] 行业意义与愿景 - 此次合作被类比为数学界的“黄金师徒”哈代和拉马努金，旨在携手逼近数学界的“GPT时刻”[54] - 公司从建立之初就立志寻找数学公理，破解困扰人类数个世纪的难题[51]